### The Mizar article:

### Lattice of Substitutions is a Heyting Algebra

**by****Adam Grabowski**

- Received December 31, 1998
Copyright (c) 1998 Association of Mizar Users

- MML identifier: HEYTING2
- [ MML identifier index ]

environ vocabulary SUBSTLAT, FUNCT_1, RELAT_1, PARTFUN1, FRAENKEL, BOOLE, FINSET_1, FINSUB_1, FINSEQ_1, NORMFORM, TARSKI, ARYTM_1, LATTICES, FUNCT_2, HEYTING1, BINOP_1, FDIFF_1, LATTICE2, SETWISEO, FUNCOP_1, FILTER_0, ZF_LANG, HEYTING2; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, FUNCOP_1, BINOP_1, FINSET_1, FINSUB_1, FUNCT_2, FRAENKEL, PARTFUN1, LATTICES, STRUCT_0, SUBSTLAT, SETWISEO, HEYTING1, LATTICE2, FILTER_0; constructors SETWISEO, GRCAT_1, SUBSTLAT, LATTICE2, FILTER_0, HEYTING1, MEMBERED; clusters RELSET_1, FINSET_1, FINSUB_1, SETWISEO, SUBSTLAT, MONOID_1, STRUCT_0, RFINSEQ, SUBSET_1, RELAT_1, FUNCT_1, WELLFND1, FRAENKEL, FINSEQ_1; requirements SUBSET, BOOLE; definitions TARSKI, FILTER_0, XBOOLE_0; theorems ZFMISC_1, TARSKI, FINSUB_1, FINSET_1, PARTFUN1, BINOP_1, LATTICES, LATTICE2, RELAT_1, FUNCT_1, GRFUNC_1, FUNCT_2, SUBSTLAT, SETWISEO, AMI_1, FUNCOP_1, FILTER_0, HEYTING1, RELSET_1, XBOOLE_0, XBOOLE_1; schemes FRAENKEL, BINOP_1, LATTICE3, PRE_CIRC, FUNCT_1, FUNCT_2, XBOOLE_0; begin :: Preliminaries reserve V, C, x, a, b for set; reserve A, B for Element of SubstitutionSet (V, C); definition let a, b be set; cluster {[a, b]} -> Function-like Relation-like; coherence proof set X = {[a, b]}; A1:[:{a},{b}:] = X by ZFMISC_1:35; for x,y1,y2 be set st [x,y1] in X & [x,y2] in X holds y1 = y2 proof let x,y1,y2 be set such that A2: [x,y1] in X and A3: [x,y2] in X; y1 = b & y2 = b by A1,A2,A3,ZFMISC_1:34; hence thesis; end; hence X is Function-like by FUNCT_1:def 1; thus X is Relation-like by RELAT_1:4; end; end; theorem for V, C being non empty set ex f be Element of PFuncs (V, C) st f <> {} proof let V, C be non empty set; consider a be set such that A1: a in V by XBOOLE_0:def 1; consider b be set such that A2: b in C by XBOOLE_0:def 1; set f = {[a,b]}; {a} c= V & {b} c= C by A1,A2,ZFMISC_1:37; then dom f c= V & rng f c= C by RELAT_1:23; then reconsider f as Element of PFuncs (V, C) by PARTFUN1:def 5; f <> {}; hence thesis; end; theorem Th2: for a, b being set st b in SubstitutionSet (V, C) & a in b holds a is finite Function proof let a, b be set; assume A1: b in SubstitutionSet (V, C) & a in b; then b in { A where A is Element of Fin PFuncs (V,C) : ( for u being set st u in A holds u is finite ) & for s1, t being Element of PFuncs (V, C) holds ( s1 in A & t in A & s1 c= t implies s1 = t ) } by SUBSTLAT:def 1; then consider A being Element of Fin PFuncs (V,C) such that A2: A = b & ( for u being set st u in A holds u is finite ) & for s, t being Element of PFuncs (V, C) holds ( s in A & t in A & s c= t implies s = t ); a is Element of PFuncs (V, C) by A1,SETWISEO:14; hence thesis by A1,A2; end; theorem Th3: for f being Element of PFuncs (V, C), g being set st g c= f holds g in PFuncs (V, C) proof let f be Element of PFuncs (V, C), g be set; assume A1: g c= f; consider f1 be Function such that A2: f1 = f & dom f1 c= V & rng f1 c= C by PARTFUN1:def 5; reconsider g' = g as Function by A1,GRFUNC_1:6; dom g' c= dom f1 & rng g' c= rng f1 by A1,A2,RELAT_1:25; then dom g' c= V & rng g' c= C by A2,XBOOLE_1:1; hence thesis by PARTFUN1:def 5; end; Lm1: for A, B, C be set st A = B \/ C & A c= B holds A = B proof let A, B, C be set; assume A1: A = B \/ C & A c= B; then B c= A by XBOOLE_1:7; hence thesis by A1,XBOOLE_0:def 10; end; theorem Th4: PFuncs(V,C) c= bool [:V,C:] proof let x be set; assume x in PFuncs(V,C); then consider f being Function such that A1: x = f and A2: dom f c= V & rng f c= C by PARTFUN1:def 5; A3: f c= [: dom f, rng f:] by RELAT_1:21; [:dom f, rng f:] c= [:V,C:] by A2,ZFMISC_1:119; then f c= [:V,C:] by A3,XBOOLE_1:1; hence x in bool [:V,C:] by A1; end; theorem Th5: V is finite & C is finite implies PFuncs (V, C) is finite proof A1: PFuncs(V,C) c= bool [:V,C:] by Th4; assume V is finite & C is finite; then [:V,C:] is finite by FINSET_1:19; then bool [:V,C:] is finite by FINSET_1:24; hence PFuncs(V,C) is finite by A1,FINSET_1:13; end; definition cluster functional finite non empty set; existence proof consider A, B be finite non empty set; take P = PFuncs(A,B); thus P is functional; thus P is finite by Th5; thus thesis; end; end; begin :: Some properties of sets of substitutions theorem Th6: for a being finite Element of PFuncs (V, C) holds {a} in SubstitutionSet (V, C) proof let a be finite Element of PFuncs (V, C); A1: for u being set st u in {a} holds u is finite by TARSKI:def 1; for s, t being Element of PFuncs (V,C) holds ( s in { a } & t in { a } & s c= t implies s = t ) proof let s, t be Element of PFuncs (V,C); assume s in { a } & t in { a } & s c= t; then s = a & t = a by TARSKI:def 1; hence s = t; end; then { a } in { A where A is Element of Fin PFuncs (V,C) : ( for u being set st u in A holds u is finite ) & for s, t being Element of PFuncs (V, C) holds ( s in A & t in A & s c= t implies s = t ) } by A1; hence thesis by SUBSTLAT:def 1; end; theorem A ^ B = A implies for a be set st a in A ex b be set st b in B & b c= a proof assume A1: A ^ B = A; let a be set; assume a in A; then consider b,c be set such that A2: b in A & c in B & a = b \/ c by A1,SUBSTLAT:15; take c; thus thesis by A2,XBOOLE_1:7; end; theorem Th8: mi (A ^ B) = A implies for a be set st a in A ex b be set st b in B & b c= a proof assume A1: mi (A ^ B) = A; let a be set; A2: mi (A ^ B) c= A ^ B by SUBSTLAT:8; assume a in A; then consider b,c be set such that A3: b in A & c in B & a = b \/ c by A1,A2,SUBSTLAT:15; take c; thus thesis by A3,XBOOLE_1:7; end; theorem Th9: (for a be set st a in A ex b be set st b in B & b c= a) implies mi (A ^ B) = A proof assume A1: for a be set st a in A ex b be set st b in B & b c= a; A2: mi (A ^ B) c= A ^ B by SUBSTLAT:8; thus mi (A ^ B) c= A proof let a be set; assume A3: a in mi (A ^ B); then consider b, c be set such that A4: b in A & c in B & a = b \/ c by A2,SUBSTLAT:15; consider b1 be set such that A5: b1 in B & b1 c= b by A1,A4; B c= PFuncs (V, C) & A c= PFuncs (V, C) by FINSUB_1:def 5; then reconsider b' = b, b1' = b1 as Element of PFuncs (V, C) by A4,A5; A6: b1' tolerates b' by A5,PARTFUN1:135; b = b1 \/ b by A5,XBOOLE_1:12; then A7: b in A ^ B by A4,A5,A6,SUBSTLAT:16; b c= a by A4,XBOOLE_1:7; hence thesis by A3,A4,A7,SUBSTLAT:6; end; thus A c= mi (A ^ B) proof let a be set; assume A8: a in A; then consider b be set such that A9: b in B & b c= a by A1; A10: a in mi A by A8,SUBSTLAT:11; A11: a is finite by A8,Th2; B c= PFuncs (V, C) & A c= PFuncs (V, C) by FINSUB_1:def 5; then reconsider a' = a, b' = b as Element of PFuncs (V, C) by A8,A9; A12: a' = a' \/ b' by A9,XBOOLE_1:12; a' tolerates b' by A9,PARTFUN1:135; then A13:a' in A ^ B by A8,A9,A12,SUBSTLAT:16; for b be finite set st b in A ^ B & b c= a holds b = a proof let b be finite set; assume A14: b in A ^ B & b c= a; then consider c, d be set such that A15: c in A & d in B & b = c \/ d by SUBSTLAT:15; c c= b by A15,XBOOLE_1:7; then c c= a by A14,XBOOLE_1:1; then c = a by A10,A15,SUBSTLAT:6; hence thesis by A14,A15,Lm1; end; hence thesis by A11,A13,SUBSTLAT:7; end; end; definition let V be set, C be finite set; let A be Element of Fin PFuncs (V, C); func Involved A means :Def1: x in it iff ex f being finite Function st f in A & x in dom f; existence proof defpred P[set] means ex f being finite Function st f in A & $1 in dom f; consider X be set such that A1: x in X iff x in V & P[x] from Separation; take X; let x be set; thus x in X implies ex f being finite Function st f in A & x in dom f by A1; given f being finite Function such that A2: f in A & x in dom f; A c= PFuncs (V, C) by FINSUB_1:def 5; then consider f1 being Function such that A3: f = f1 & dom f1 c= V & rng f1 c= C by A2,PARTFUN1:def 5; thus thesis by A1,A2,A3; end; uniqueness proof defpred P[set] means ex f being finite Function st f in A & $1 in dom f; A4: for X1,X2 being set st (for x being set holds x in X1 iff P[x]) & (for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq; let r,s be set such that A5: x in r iff ex f being finite Function st f in A & x in dom f and A6: x in s iff ex f being finite Function st f in A & x in dom f; thus r=s by A4,A5,A6; end; end; reserve C for finite set; theorem Th10: for V being set, C be finite set, A being Element of Fin PFuncs (V, C) holds Involved A c= V proof let V be set, C be finite set, A be Element of Fin PFuncs (V, C); let a be set; assume a in Involved A; then consider f being finite Function such that A1: f in A & a in dom f by Def1; A c= PFuncs (V, C) by FINSUB_1:def 5; then consider f1 being Function such that A2: f = f1 & dom f1 c= V & rng f1 c= C by A1,PARTFUN1:def 5; thus thesis by A1,A2; end; Lm2: for V being set, C be finite set, A being non empty Element of Fin PFuncs (V, C) holds Involved A is finite proof let V be set, C be finite set, A be non empty Element of Fin PFuncs (V, C); deffunc F(Function)=dom $1; defpred P[set] means $1 in A & $1 is finite; defpred Q[set] means $1 in A; set X = { F(f) where f is Element of PFuncs(V, C) : P[f]}; A1: for g being Element of PFuncs(V, C) holds P[g] implies Q[g]; A2: X c= { F(f) where f is Element of PFuncs(V, C) : Q[f]} from Fraenkel5'(A1); A3: A is finite; A4: { F(f) where f is Element of PFuncs(V, C) : f in A } is finite from FraenkelFin(A3); x in Involved A iff ex Y be set st x in Y & Y in X proof hereby assume x in Involved A; then consider f being finite Function such that A5: f in A & x in dom f by Def1; A c= PFuncs (V,C) by FINSUB_1:def 5; then dom f in X by A5; hence ex Y be set st x in Y & Y in X by A5; end; given Y be set such that A6: x in Y & Y in X; consider f1 being Element of PFuncs(V, C) such that A7: Y = dom f1 & f1 in A & f1 is finite by A6; thus thesis by A6,A7,Def1; end; then A8: Involved A = union X by TARSKI:def 4; A9: X is finite by A2,A4,FINSET_1:13; for x be set st x in X holds x is finite proof let x be set; assume x in X; then consider f1 being Element of PFuncs(V, C) such that A10: x = dom f1 & f1 in A & f1 is finite; thus thesis by A10,AMI_1:21; end; hence thesis by A8,A9,FINSET_1:25; end; theorem Th11: for V being set, C being finite set, A being Element of Fin PFuncs (V, C) st A = {} holds Involved A = {} proof let V be set, C be finite set, A be Element of Fin PFuncs (V, C); assume A1: A = {}; assume Involved A <> {}; then consider x be set such that A2: x in Involved A by XBOOLE_0:def 1; consider f being finite Function such that A3: f in A & x in dom f by A2,Def1; thus thesis by A1,A3; end; theorem Th12: for V being set, C being finite set, A being Element of Fin PFuncs (V, C) holds Involved A is finite proof let V be set, C be finite set, A be Element of Fin PFuncs (V, C); per cases; suppose A is non empty; hence thesis by Lm2; suppose A is empty; hence thesis by Th11; end; theorem for C being finite set, A being Element of Fin PFuncs ({}, C) holds Involved A = {} proof let C be finite set, A be Element of Fin PFuncs ({}, C); Involved A c= {} by Th10; hence thesis by XBOOLE_1:3; end; definition let V be set, C be finite set; let A be Element of Fin PFuncs (V, C); func -A -> Element of Fin PFuncs (V, C) equals :Def2: { f where f is Element of PFuncs (Involved A, C) : for g be Element of PFuncs (V, C) st g in A holds not f tolerates g }; coherence proof set M = { f where f is Element of PFuncs (Involved A, C) : for g be Element of PFuncs (V, C) st g in A holds not f tolerates g }; defpred P[Element of PFuncs (Involved A, C)] means for h be Element of PFuncs (V, C) st h in A holds not $1 tolerates h; defpred Q[set] means not contradiction; A1: for v being Element of PFuncs (Involved A, C) holds P[v] implies Q[v]; deffunc F(set)=$1; A2: { F(f) where f is Element of PFuncs (Involved A, C) : P[f] } c= { F(f) where f is Element of PFuncs (Involved A, C) : Q[f] } from Fraenkel5'(A1); Involved A is finite by Th12; then A3: PFuncs (Involved A, C) is finite by Th5; { f where f is Element of PFuncs (Involved A, C) : not contradiction } c= PFuncs (Involved A, C) proof let a be set; assume a in { f where f is Element of PFuncs (Involved A, C) : not contradiction }; then consider f1 be Element of PFuncs (Involved A, C) such that A4: f1 = a & not contradiction; thus thesis by A4; end; then { f where f is Element of PFuncs (Involved A, C) : not contradiction } is finite by A3,FINSET_1:13; then A5: M is finite by A2,FINSET_1:13; M c= PFuncs (V, C) proof let a be set; assume a in M; then consider f1 be Element of PFuncs (Involved A, C) such that A6: f1 = a & for g be Element of PFuncs (V, C) st g in A holds not f1 tolerates g; Involved A c= V by Th10; then A7: PFuncs (Involved A, C) c= PFuncs (V, C) by PARTFUN1:125; a in PFuncs (Involved A, C) by A6; hence thesis by A7; end; hence thesis by A5,FINSUB_1:def 5; end; end; theorem Th14: A ^ -A = {} proof assume A ^ -A <> {}; then consider x be set such that A1: x in A ^ -A by XBOOLE_0:def 1; x in { s \/ t where s, t is Element of PFuncs (V,C) : s in A & t in -A & s tolerates t } by A1,SUBSTLAT:def 3; then consider s1, t1 be Element of PFuncs (V,C) such that A2: x = s1 \/ t1 & s1 in A & t1 in -A & s1 tolerates t1; t1 in { f where f is Element of PFuncs (Involved A, C) : for g be Element of PFuncs (V, C) st g in A holds not f tolerates g } by A2,Def2; then consider f1 be Element of PFuncs (Involved A, C) such that A3: f1 = t1 & for g be Element of PFuncs (V, C) st g in A holds not f1 tolerates g; thus thesis by A2,A3; end; theorem Th15: A = {} implies -A = { {} } proof assume A1: A = {}; A2:-A = { f where f is Element of PFuncs (Involved A, C) : for g be Element of PFuncs (V, C) st g in A holds not f tolerates g } by Def2; defpred P[Element of PFuncs (Involved A, C)] means for g be Element of PFuncs (V, C) st g in A holds not $1 tolerates g; { xx where xx is Element of PFuncs (Involved A, C) : P[xx]} c= PFuncs (Involved A, C) from Fr_Set0; then -A c= PFuncs ({}, C) by A1,A2,Th11; then A3: -A c= { {} } by PARTFUN1:122; {} in -A proof {} in { {} } by TARSKI:def 1; then {} in PFuncs ({}, C) by PARTFUN1:122; then A4: {} in PFuncs (Involved A, C) by A1,Th11; for g be Element of PFuncs (V, C) st g in A holds not {} tolerates g by A1 ; hence thesis by A2,A4; end; then { {} } c= -A by ZFMISC_1:37; hence thesis by A3,XBOOLE_0:def 10; end; theorem A = { {} } implies -A = {} proof assume A = {{}}; then A1:-A = { f where f is Element of PFuncs (Involved A, C) : for g be Element of PFuncs (V, C) st g in {{}} holds not f tolerates g } by Def2; assume -A <> {}; then consider x1 be set such that A2: x1 in -A by XBOOLE_0:def 1; consider f1 being Element of PFuncs (Involved A, C) such that A3: x1 = f1 & for g be Element of PFuncs (V, C) st g in {{}} holds not f1 tolerates g by A1,A2; {} is PartFunc of V, C by PARTFUN1:56; then A4: {} in PFuncs (V, C) by PARTFUN1:119; A5: {} in {{}} by TARSKI:def 1; f1 tolerates {} by PARTFUN1:141; hence thesis by A3,A4,A5; end; theorem Th17: for V being set, C being finite set for A being Element of SubstitutionSet (V, C) holds mi (A ^ -A) = Bottom SubstLatt (V,C) proof let V be set, C be finite set, A be Element of SubstitutionSet (V, C); A ^ -A = {} by Th14; then mi (A ^ -A) = {} by SUBSTLAT:9 .= Bottom SubstLatt (V,C) by SUBSTLAT:26; hence thesis; end; theorem for V being non empty set, C being finite non empty set for A being Element of SubstitutionSet (V, C) st A = {} holds mi -A = Top SubstLatt (V,C) proof let V be non empty set, C be finite non empty set, A be Element of SubstitutionSet (V, C); assume A = {}; then A1: -A = { {} } by Th15; then -A in SubstitutionSet (V, C) by SUBSTLAT:2; then mi -A = { {} } by A1,SUBSTLAT:11; hence thesis by SUBSTLAT:27; end; theorem Th19: for V being set, C being finite set for A being Element of SubstitutionSet (V, C), a being Element of PFuncs (V, C), B being Element of SubstitutionSet (V, C) st B = { a } holds A ^ B = {} implies ex b being finite set st b in -A & b c= a proof let V, C; let A be Element of SubstitutionSet (V, C); let a be Element of PFuncs (V, C); let B be Element of SubstitutionSet (V, C) such that A1: B = { a }; assume A2: A ^ B = {}; per cases; suppose A3: A is non empty; then A4: A = [A] by HEYTING1:def 2; defpred P[Element of PFuncs (V, C),set] means $2 in dom $1 /\ dom a & $1.$2 <> a.$2; A5: now let s be Element of PFuncs (V, C) such that A6: s in A; not s tolerates a proof assume A7: s tolerates a; a in B by A1,TARSKI:def 1; then s \/ a in { s1 \/ t1 where s1,t1 is Element of PFuncs (V,C) : s1 in A & t1 in B & s1 tolerates t1 } by A6,A7; hence thesis by A2,SUBSTLAT:def 3; end; then consider x be set such that A8: x in dom s /\ dom a & s.x <> a.x by PARTFUN1:def 6; consider a' be Function such that A9: a' = a & dom a' c= V & rng a' c= C by PARTFUN1:def 5; dom s /\ dom a c= dom a' by A9,XBOOLE_1:17; then dom s /\ dom a c= V by A9,XBOOLE_1:1; then reconsider x as Element of [V] by A8,HEYTING1:def 2; take x; thus P[s,x] by A8; end; consider g be Element of Funcs (PFuncs (V, C), [V]) such that A10: for s be Element of PFuncs (V, C) st s in A holds P[s,g.s] from FuncsChoice(A5); deffunc G(set)=g.$1; defpred P[set] means not contradiction; reconsider AA = A as finite non empty set by A3; { G(b) where b is Element of AA : P[b] } is finite from FraenkelFinIm; then reconsider UKA = { g.b where b is Element of [A] : not contradiction } as finite set by A4; set f = a|UKA; A11: rng f c= rng a by RELAT_1:99; consider kk be Function such that A12: kk = a & dom kk c= V & rng kk c= C by PARTFUN1:def 5; A13: f c= kk by A12,RELAT_1:88; A14: dom f c= Involved A proof let x be set; assume x in dom f; then x in UKA by RELAT_1:86; then consider b be Element of [A] such that A15: x = g.b; reconsider b as finite Function by A4,Th2; reconsider b' = b as Element of PFuncs (V, C) by A4,SETWISEO:14; g.b' in dom b' /\ dom a by A4,A10; then x in dom b by A15,XBOOLE_0:def 3; hence thesis by A4,Def1; end; rng f c= C by A11,A12,XBOOLE_1:1; then reconsider f' = f as Element of PFuncs (Involved A, C) by A14,PARTFUN1:def 5; for g be Element of PFuncs (V, C) st g in A holds not f tolerates g proof let g1 be Element of PFuncs (V, C); reconsider g' = g1 as Function; assume A16: g1 in A; ex z be set st z in dom g1 /\ dom f & g'.z <> f.z proof set z = g.g1; A17: g1.(g.g1) <> a.(g.g1) & z in dom g1 /\ dom a by A10,A16; A18: g1.z <> a.z by A10,A16; A19: z in dom a & z in dom g1 by A17,XBOOLE_0:def 3; take z; z in { g.b1 where b1 is Element of [A] : not contradiction } by A4,A16; then z in dom a /\ UKA by A19,XBOOLE_0:def 3; then A20: z in dom f by RELAT_1:90; hence z in dom g1 /\ dom f by A19,XBOOLE_0:def 3; thus thesis by A18,A20,FUNCT_1:70; end; hence thesis by PARTFUN1:def 6; end; then f' in { f1 where f1 is Element of PFuncs (Involved A, C) : for g be Element of PFuncs (V, C) st g in A holds not f1 tolerates g }; then f in -A by Def2; hence thesis by A12,A13; suppose A is empty; then A21: -A = {{}} by Th15; reconsider K = {} as finite set; take K; thus thesis by A21,TARSKI:def 1,XBOOLE_1:2; end; definition let V be set, C be finite set; let A, B be Element of Fin PFuncs (V, C); func A =>> B -> Element of Fin PFuncs (V, C) equals :Def3: PFuncs (V, C) /\ { union {f.i \ i where i is Element of PFuncs (V, C) : i in A} where f is Element of PFuncs (A, B) : dom f = A }; coherence proof set Z = { union {f.i \ i where i is Element of PFuncs (V, C) : i in A} where f is Element of PFuncs (A, B) : dom f = A}; set K = PFuncs (V, C) /\ Z; A1: K c= PFuncs (V, C) by XBOOLE_1:17; A2: Z = { union {f.i \ i where i is Element of PFuncs (V, C) : i in A} where f is Element of PFuncs (A, B) : f in PFuncs(A,B) & dom f = A} proof thus Z c= { union {f.i \ i where i is Element of PFuncs (V, C) : i in A } where f is Element of PFuncs (A, B) : f in PFuncs(A,B) & dom f = A } proof let z be set; assume z in Z; then consider f1 be Element of PFuncs (A, B) such that A3: z = union {f1.i \ i where i is Element of PFuncs (V, C) : i in A} & dom f1 = A; thus thesis by A3; end; thus { union {f.i \ i where i is Element of PFuncs (V, C) : i in A} where f is Element of PFuncs (A, B) : f in PFuncs(A,B) & dom f = A } c= Z proof let z be set; assume z in { union {f.i \ i where i is Element of PFuncs (V, C) : i in A} where f is Element of PFuncs (A, B) : f in PFuncs(A,B) & dom f = A}; then consider f1 be Element of PFuncs (A, B) such that A4: z = union {f1.i \ i where i is Element of PFuncs (V, C) : i in A} & f1 in PFuncs (A, B) & dom f1 = A; thus thesis by A4; end; end; reconsider PF = PFuncs (A, B) as functional finite non empty set by Th5; deffunc F(Element of PF)= union {$1.i \ i where i is Element of PFuncs (V, C) : i in A}; defpred P[Element of PF] means $1 in PFuncs(A,B) & dom $1 = A; { F(f) where f is Element of PF : P[f]} is finite from FraenkelFinIm; then K is finite by A2,FINSET_1:15; hence thesis by A1,FINSUB_1:def 5; end; end; theorem Th20: for A, B being Element of Fin PFuncs (V, C), s being set st s in A =>> B holds ex f being PartFunc of A, B st s = union {f.i \ i where i is Element of PFuncs (V, C) : i in A} & dom f = A proof let A, B be Element of Fin PFuncs (V, C), s be set; assume s in A =>> B; then s in PFuncs (V, C) /\ { union {f.i \ i where i is Element of PFuncs (V, C) : i in A} where f is Element of PFuncs (A, B) : dom f = A } by Def3; then s in { union {f.i \ i where i is Element of PFuncs (V, C) : i in A} where f is Element of PFuncs (A, B) : dom f = A} by XBOOLE_0:def 3; then consider f be Element of PFuncs (A, B) such that A1: s = union {f.i \ i where i is Element of PFuncs (V, C) : i in A} & dom f = A; f is PartFunc of A, B by PARTFUN1:121; hence thesis by A1; end; Lm3: for V be set, C be finite set, A be Element of Fin PFuncs (V, C), K be Element of SubstitutionSet (V, C) holds a in A ^ (A =>> K) implies ex b st b in K & b c= a proof let V be set, C be finite set, A be Element of Fin PFuncs (V, C), K be Element of SubstitutionSet (V, C); assume a in A ^ (A =>> K); then consider b,c be set such that A1: b in A and A2: c in A =>> K and A3: a = b \/ c by SUBSTLAT:15; consider f be PartFunc of A, K such that A4: c = union {f.i \ i where i is Element of PFuncs (V, C) : i in A } & dom f = A by A2,Th20; A5: f.b in K by A1,A4,PARTFUN1:27; K c= PFuncs (V, C) by FINSUB_1:def 5; then reconsider d = f.b as Element of PFuncs (V, C) by A5; take d; thus d in K by A1,A4,PARTFUN1:27; A c= PFuncs (V, C) by FINSUB_1:def 5; then reconsider b' = b as Element of PFuncs (V, C) by A1; d \ b' in {f.i \ i where i is Element of PFuncs (V, C) : i in A} by A1; then d \ b c= c by A4,ZFMISC_1:92; hence d c= a by A3,XBOOLE_1:44; end; theorem for V being set, C being finite set, A being Element of Fin PFuncs (V, C) st A = {} holds A =>> A = {{}} proof let V be set, C be finite set, A be Element of Fin PFuncs (V, C); assume A1: A = {}; defpred P[Function] means dom $1 = A; deffunc F(Element of PFuncs (A, A))= union {$1.i \ i where i is Element of PFuncs (V, C) : i in A}; deffunc G(set)={}; now let f be Element of PFuncs (A, A); not ex x be set st x in {f.i \ i where i is Element of PFuncs (V, C) : i in A} proof given x be set such that A2: x in {f.i \ i where i is Element of PFuncs (V, C) : i in A}; consider x1 being Element of PFuncs (V, C) such that A3: x = f.x1 \ x1 & x1 in A by A2; thus contradiction by A1,A3; end; hence {f.i \ i where i is Element of PFuncs (V, C) : i in A} = {} by XBOOLE_0:def 1; end; then A4: for v being Element of PFuncs (A, A) st P[v] holds F(v) = G(v) by ZFMISC_1:2; A5:{ F(f) where f is Element of PFuncs (A, A) : P[f]} = { G(f) where f is Element of PFuncs (A, A) : P[f] } from FraenkelF'R (A4); A6: ex a being Element of PFuncs (A, A) st P[a] proof reconsider e = id A as Element of PFuncs (A, A) by PARTFUN1:119; take e; thus thesis by RELAT_1:71; end; A7: { {} where f is Element of PFuncs (A, A) : P[f] } = {{}} from SingleFraenkel (A6); {} is PartFunc of V,C by PARTFUN1:56; then {} in PFuncs (V,C) by PARTFUN1:119; then A8: {{}} c= PFuncs (V,C) by ZFMISC_1:37; A =>> A = PFuncs (V,C) /\ {{}} by A5,A7,Def3 .= {{}} by A8,XBOOLE_1:28; hence thesis; end; reserve u, v for Element of SubstLatt (V, C); reserve s, t, a, b for Element of PFuncs (V,C); reserve K, L for Element of SubstitutionSet (V, C); Lm4: for X being set st X c= K holds X in SubstitutionSet (V, C) proof let X be set; assume A1: X c= K; K c= PFuncs (V, C) & K is finite by FINSUB_1:def 5; then X c= PFuncs (V, C) & X is finite by A1,FINSET_1:13,XBOOLE_1:1; then reconsider B = X as Element of Fin PFuncs (V, C) by FINSUB_1:def 5; A2: for x be set st x in X holds x is finite by A1,Th2; for a,b st a in B & b in B & a c= b holds a = b by A1,SUBSTLAT:5; then X in { A where A is Element of Fin PFuncs (V,C) : ( for u being set st u in A holds u is finite ) & for s, t being Element of PFuncs (V, C) holds ( s in A & t in A & s c= t implies s = t ) } by A2; hence X in SubstitutionSet (V, C) by SUBSTLAT:def 1; end; theorem Th22: for X being set st X c= u holds X is Element of SubstLatt (V, C) proof let X be set; reconsider u' = u as Element of SubstitutionSet (V, C) by SUBSTLAT:def 4; assume X c= u; then X c= u'; then X in SubstitutionSet (V, C) by Lm4; hence X is Element of SubstLatt (V, C) by SUBSTLAT:def 4; end; begin :: Lattice of substitutions is implicative definition let V, C; func pseudo_compl (V, C) -> UnOp of the carrier of SubstLatt (V, C) means :Def4: for u' being Element of SubstitutionSet (V, C) st u' = u holds it.u = mi(-u'); existence proof deffunc F(Element of SubstitutionSet (V, C))=mi(-$1); consider IT being Function of SubstitutionSet (V, C), SubstitutionSet (V, C) such that A1: for u being Element of SubstitutionSet (V, C) holds IT.u = F(u) from LambdaD; SubstitutionSet (V, C) = the carrier of SubstLatt (V, C) by SUBSTLAT:def 4; then reconsider IT as UnOp of the carrier of SubstLatt (V, C); take IT; thus thesis by A1; end; correctness proof let IT,IT' be UnOp of the carrier of SubstLatt (V, C); assume that A2: for u' being Element of SubstitutionSet (V, C) st u' = u holds IT.u = mi (-u') and A3: for u' being Element of SubstitutionSet (V, C) st u' = u holds IT'.u = mi (-u'); now let u; reconsider u' = u as Element of SubstitutionSet (V, C) by SUBSTLAT:def 4; thus IT.u = mi (-u') by A2 .= IT'.u by A3; end; hence IT = IT' by FUNCT_2:113; end; func StrongImpl(V, C) -> BinOp of the carrier of SubstLatt (V, C) means :Def5: for u', v' being Element of SubstitutionSet (V, C) st u' = u & v' = v holds it.(u,v) = mi (u' =>> v'); existence proof defpred P[set, set, set] means for u', v' being Element of SubstitutionSet (V, C) st u' = $1 & v' = $2 holds $3 = mi (u' =>> v'); set ZA = the carrier of SubstLatt (V, C); A4: for x,y being Element of ZA ex z being Element of ZA st P[x,y,z] proof let x,y be Element of ZA; reconsider x' = x, y' = y as Element of SubstitutionSet (V, C) by SUBSTLAT:def 4; reconsider z = mi (x' =>> y') as Element of ZA by SUBSTLAT:def 4; take z; let u', v' be Element of SubstitutionSet (V, C); assume u' = x & v' = y; hence thesis; end; consider o being BinOp of the carrier of SubstLatt (V, C) such that A5: for a,b being Element of SubstLatt (V, C) holds P[a,b,o.(a,b)] from BinOpEx(A4); take o; let u,v; let u', v' be Element of SubstitutionSet (V, C); assume u' = u & v' = v; hence o.(u,v) = mi (u' =>> v') by A5; end; correctness proof let IT1,IT2 be BinOp of the carrier of SubstLatt (V, C); assume that A6: for u', v' being Element of SubstitutionSet (V, C) st u' = u & v' = v holds IT1.(u,v) = mi (u' =>> v') and A7: for u', v' being Element of SubstitutionSet (V, C) st u' = u & v' = v holds IT2.(u,v) = mi (u' =>> v'); now let u, v; reconsider u' = u, v' = v as Element of SubstitutionSet (V, C) by SUBSTLAT:def 4; thus IT1.(u,v) = mi (u' =>> v') by A6 .= IT2.(u,v) by A7; end; hence IT1 = IT2 by BINOP_1:2; end; let u; func SUB u -> Element of Fin the carrier of SubstLatt (V, C) equals :Def6: bool u; coherence proof reconsider u' = u as Element of SubstitutionSet (V, C) by SUBSTLAT:def 4; u' is finite; then A8: bool u is finite by FINSET_1:24; bool u c= the carrier of SubstLatt (V, C) proof let x be set; assume x in bool u; then x is Element of SubstLatt (V, C) by Th22; hence thesis; end; hence thesis by A8,FINSUB_1:def 5; end; correctness; func diff(u) -> UnOp of the carrier of SubstLatt (V, C) means :Def7: it.v = u \ v; existence proof u in the carrier of SubstLatt (V, C); then A9: u in SubstitutionSet (V, C) by SUBSTLAT:def 4; deffunc F(set)=u \ $1; consider IT being Function such that A10: dom IT = the carrier of SubstLatt (V, C) & for v be set st v in the carrier of SubstLatt (V, C) holds IT.v = F(v) from Lambda; for x be set st x in the carrier of SubstLatt (V, C) holds IT.x in Fin PFuncs (V, C) proof let x be set; assume x in the carrier of SubstLatt (V, C); then A11: IT.x = u \ x by A10; u \ x c= u by XBOOLE_1:36; then u \ x in SubstitutionSet (V,C) by A9,Lm4; hence thesis by A11; end; then reconsider IT as Function of the carrier of SubstLatt (V, C), Fin PFuncs (V, C) by A10,FUNCT_2:5; now let v be Element of SubstLatt (V, C); u \ v c= u by XBOOLE_1:36; then u \ v in SubstitutionSet (V,C) by A9,Lm4; then IT.v in SubstitutionSet (V,C) by A10; hence IT.v in the carrier of SubstLatt (V, C) by SUBSTLAT:def 4; end; then reconsider IT as UnOp of the carrier of SubstLatt (V, C) by HEYTING1:1; take IT; let v; thus IT.v = u \ v by A10; end; correctness proof let IT,IT' be UnOp of the carrier of SubstLatt (V, C); assume that A12: IT.v = u \ v and A13: IT'.v = u \ v; now let v be Element of SubstLatt (V, C); thus IT.v = u \ v by A12 .= IT'.v by A13; end; hence IT = IT' by FUNCT_2:113; end; end; Lm5: v in SUB u implies v "\/" (diff u).v = u proof assume v in SUB u; then A1: v in bool u by Def6; A2: u \ v = (diff u).v by Def7; reconsider u' = u, v' = v, dv = (diff u).v as Element of SubstitutionSet (V, C) by SUBSTLAT:def 4; thus v "\/" (diff u).v = (the L_join of SubstLatt (V,C)).(v, (diff u).v) by LATTICES:def 1 .= mi ( v' \/ dv ) by SUBSTLAT:def 4 .= mi u' by A1,A2,XBOOLE_1:45 .= u by SUBSTLAT:11; end; Lm6: for K be Element of Fin PFuncs (V, C) st a is finite & K = {a} holds ex v be Element of SubstitutionSet (V,C) st v in SUB u & v ^ K = {} & for b st b in (diff u).v holds b tolerates a proof let K be Element of Fin PFuncs (V, C) such that A1: a is finite & K = {a}; defpred P[Element of PFuncs (V, C)] means $1 is finite & not $1 tolerates a; deffunc F(set)=$1; set M = { F(s) where s is Element of PFuncs (V, C): F(s) in u & P[s] }; A2: M c= u from FrSet_1; then reconsider v = M as Element of SubstLatt (V, C) by Th22; reconsider v as Element of SubstitutionSet (V,C) by SUBSTLAT:def 4; take v; v in bool u by A2; hence v in SUB u by Def6; deffunc F(Element of PFuncs (V, C),Element of PFuncs (V, C))=$1 \/ $2; defpred P[Element of PFuncs (V, C),Element of PFuncs (V, C)] means $1 in M & $2 in { a } & $1 tolerates $2; defpred Q[Element of PFuncs (V, C),Element of PFuncs (V, C)] means $2 = a & $1 in M & $1 tolerates $2; A3: P[s,t] iff Q[s,t] by TARSKI:def 1; A4: { F(s,t): P[s,t] } = { F(s',t') where s', t' is Element of PFuncs (V, C) : Q[s',t'] } from Fraenkel6''(A3); defpred P[Element of PFuncs (V, C)] means $1 in M & $1 tolerates a; defpred Q[Element of PFuncs (V, C)] means not $1 tolerates a & $1 in u & $1 tolerates a; s in M iff s is finite & not s tolerates a & s in u proof thus s in M implies s is finite & not s tolerates a & s in u proof assume s in M; then consider s2 be Element of PFuncs (V, C) such that A5: s2 = s & s2 in u & s2 is finite & not s2 tolerates a; thus thesis by A5; end; thus s is finite & not s tolerates a & s in u implies s in M; end; then A6: P[s] iff Q[s]; deffunc F1(Element of PFuncs (V, C),Element of PFuncs (V, C))=$1 \/ $2; defpred P1[Element of PFuncs (V, C),Element of PFuncs (V, C)] means $1 in M & $1 tolerates $2; A7: { F1(s,t) where t is Element of PFuncs (V, C) : t = a & P1[s,t]} = { F1(s',a) where s' is Element of PFuncs (V, C) : P1[s',a]} from FrEqua2; deffunc F(Element of PFuncs (V, C))=$1 \/ a; { F(s') where s' is Element of PFuncs (V, C) : P[s']} = { F(s): Q[s]} from Fraenkel6'(A6); then A8: v ^ K = { s \/ a: not s tolerates a & s in u & s tolerates a } by A1,A4,A7,SUBSTLAT:def 3; thus v ^ K = {} proof assume v ^ K <> {}; then consider x be set such that A9: x in v ^ K by XBOOLE_0:def 1; consider s1 be Element of PFuncs (V, C) such that A10: x = s1 \/ a & not s1 tolerates a & s1 in u & s1 tolerates a by A8,A9; thus thesis by A10; end; let b; assume b in (diff u).v; then b in u \ v by Def7; then A11: b in u & not b in M by XBOOLE_0:def 4; u in the carrier of SubstLatt (V, C); then u in SubstitutionSet (V, C) by SUBSTLAT:def 4; then b is finite by A11,Th2; hence b tolerates a by A11; end; definition let V, C; func Atom(V, C) -> Function of PFuncs (V, C), the carrier of SubstLatt (V, C) means :Def8: for a being Element of PFuncs (V,C) holds it.a = mi { a }; existence proof A1: the carrier of SubstLatt (V, C) = SubstitutionSet (V, C) by SUBSTLAT:def 4; deffunc F(Element of PFuncs (V, C))= mi {$1}; consider f be Function of PFuncs (V, C), SubstitutionSet (V, C) such that A2: for a be Element of PFuncs (V, C) holds f.a = F(a) from LambdaD; A3: now let x be set; assume x in PFuncs (V, C); then reconsider a = x as Element of PFuncs (V, C); f.a = mi { a } by A2; hence f.x in the carrier of SubstLatt (V, C) by A1; end; dom f = PFuncs (V, C) by FUNCT_2:def 1; then reconsider f as Function of PFuncs (V, C), the carrier of SubstLatt (V , C) by A3,FUNCT_2:5; take f; thus thesis by A2; end; correctness proof let IT1,IT2 be Function of PFuncs (V, C), the carrier of SubstLatt (V, C) such that A4: (for a holds IT1.a = mi { a }) & for a holds IT2.a = mi { a }; now let a; IT1.a = mi { a } & IT2.a = mi { a } by A4; hence IT1.a = IT2.a; end; hence thesis by FUNCT_2:113; end; end; Lm7: for a be Element of PFuncs (V, C) st a is finite holds Atom (V, C).a = {a} proof let a be Element of PFuncs (V, C); assume A1: a is finite; { a } in SubstitutionSet (V, C) proof A2: for u being set st u in { a } holds u is finite by A1,TARSKI:def 1; for s, t being Element of PFuncs (V,C) holds ( s in { a } & t in { a } & s c= t implies s = t ) proof let s, t be Element of PFuncs (V,C); assume s in { a } & t in { a } & s c= t; then s = a & t = a by TARSKI:def 1; hence s = t; end; then { a } in { A where A is Element of Fin PFuncs (V,C) : ( for u being set st u in A holds u is finite ) & for s, t being Element of PFuncs (V, C) holds ( s in A & t in A & s c= t implies s = t ) } by A2; hence thesis by SUBSTLAT:def 1; end; then {a} = mi {a} by SUBSTLAT:11 .= Atom (V, C).a by Def8; hence thesis; end; theorem Th23: FinJoin (K, Atom(V, C)) = FinUnion(K, singleton PFuncs (V, C)) proof A1: the L_join of SubstLatt (V, C) is commutative by LATTICE2:27; A2: the L_join of SubstLatt (V, C) is associative by LATTICE2:29; A3: the L_join of SubstLatt (V, C) is idempotent by LATTICE2:26; A4: the L_join of SubstLatt (V, C) has_a_unity by LATTICE2:67; deffunc F(Element of Fin PFuncs (V, C))= mi $1; consider g being Function of Fin PFuncs (V, C), SubstitutionSet (V,C) such that A5: for B be Element of Fin PFuncs (V, C) holds g.B = F(B) from LambdaD; the carrier of SubstLatt (V, C) = SubstitutionSet (V,C) by SUBSTLAT:def 4 ; then reconsider g as Function of Fin PFuncs (V, C), the carrier of SubstLatt (V, C); A6: g.{}.PFuncs (V, C) = mi {}.PFuncs (V, C) by A5 .= {} by SUBSTLAT:9 .= Bottom SubstLatt (V, C) by SUBSTLAT:26 .= the_unity_wrt the L_join of SubstLatt (V, C) by A4,LATTICE2:28; A7: now let x,y be Element of Fin PFuncs (V, C); A8: g.x = mi x by A5; A9: g.y = mi y by A5; thus g.(x \/ y) = mi (x \/ y) by A5 .= mi (mi x \/ y) by SUBSTLAT:13 .= mi (mi x \/ mi y) by SUBSTLAT:13 .= (the L_join of SubstLatt (V, C)).(g.x,g.y) by A8,A9,SUBSTLAT:def 4; end; A10: K c= PFuncs (V, C) by FINSUB_1:def 5; then A11: K c= dom (Atom(V, C)) by FUNCT_2:def 1; A12: dom singleton PFuncs (V, C) = PFuncs (V, C) by FUNCT_2:def 1; A13: rng singleton PFuncs (V, C) c= Fin PFuncs (V, C); dom g = Fin PFuncs (V, C) by FUNCT_2:def 1; then dom ((g*singleton PFuncs (V, C))) = dom singleton PFuncs (V, C) by A13,RELAT_1:46; then A14: dom (Atom(V, C)|K) = K & dom ((g*singleton PFuncs (V, C))|K) = K by A10,A11,A12,RELAT_1:91; now let a be set; assume A15: a in K; then reconsider a' = a as Element of PFuncs (V, C) by SETWISEO:14; A16: a' is finite by A15,Th2; then reconsider KL = {a'} as Element of SubstitutionSet (V,C) by Th6; thus ((g*singleton PFuncs (V, C))|K).a = (g*singleton PFuncs (V, C)).a by A15,FUNCT_1:72 .= g.(singleton PFuncs (V, C) .a') by FUNCT_2:21 .= g.{a} by SETWISEO:67 .= mi KL by A5 .= KL by SUBSTLAT:11 .= Atom (V, C).a' by A16,Lm7 .= (Atom (V, C)|K).a by A15,FUNCT_1:72; end; then A17: Atom(V, C)|K = (g*singleton PFuncs (V, C))|K by A14,FUNCT_1:9; A18: mi (FinUnion(K,singleton PFuncs (V, C))) c= FinUnion(K,singleton PFuncs (V, C)) by SUBSTLAT:8; A19: FinUnion(K,singleton PFuncs (V, C)) c= mi (FinUnion(K,singleton PFuncs (V, C))) proof let a be set; assume A20: a in FinUnion(K,singleton PFuncs (V, C)); then consider b be Element of PFuncs (V, C) such that A21: b in K and A22: a in (singleton PFuncs (V, C)).b by SETWISEO:70; A23: a = b by A22,SETWISEO:68; then A24: a is finite by A21,Th2; now let s be finite set; assume that A25: s in FinUnion(K,singleton PFuncs (V, C)) and A26: s c= a; consider t such that A27: t in K and A28: s in (singleton PFuncs (V, C)).t by A25,SETWISEO:70; A29: s = t by A28,SETWISEO:68; K in SubstitutionSet (V, C); then K in { A where A is Element of Fin PFuncs (V,C) : ( for u being set st u in A holds u is finite ) & for s, t being Element of PFuncs (V, C) holds ( s in A & t in A & s c= t implies s = t ) } by SUBSTLAT:def 1; then ex AA be Element of Fin PFuncs (V,C) st K = AA & ( for u being set st u in AA holds u is finite ) & for s, t being Element of PFuncs (V, C) holds ( s in AA & t in AA & s c= t implies s = t ); hence s = a by A21,A23,A26,A27,A29; end; hence a in mi (FinUnion(K,singleton PFuncs (V, C))) by A20,A24,SUBSTLAT:7; end; reconsider gs = g*singleton PFuncs (V, C) as Function of PFuncs (V, C), the carrier of SubstLatt (V, C) by FUNCT_2:19; thus FinJoin(K, Atom (V, C)) = FinJoin(K, gs) by A17,LATTICE2:69 .= (the L_join of SubstLatt (V, C)) $$(K,gs) by LATTICE2:def 3 .= g.(FinUnion(K,singleton PFuncs (V, C))) by A1,A2,A3,A4,A6,A7,SETWISEO:65 .= mi (FinUnion(K,singleton PFuncs (V, C))) by A5 .= FinUnion(K,singleton PFuncs (V, C)) by A18,A19,XBOOLE_0:def 10; end; theorem Th24: for u being Element of SubstitutionSet (V, C) holds u = FinJoin(u, Atom (V, C)) proof let u be Element of SubstitutionSet (V, C); thus u = FinUnion(u, singleton PFuncs (V, C)) by SETWISEO:71 .= FinJoin(u, Atom(V, C)) by Th23; end; Lm8: (for a be set st a in u ex b be set st b in v & b c= a) implies u [= v proof assume A1: for a be set st a in u ex b be set st b in v & b c= a; reconsider u' = u, v' = v as Element of SubstitutionSet (V, C) by SUBSTLAT:def 4; u "/\" v = (the L_meet of SubstLatt (V, C)).(u', v') by LATTICES:def 2 .= mi (u' ^ v') by SUBSTLAT:def 4 .= u' by A1,Th9; hence u [= v by LATTICES:21; end; theorem Th25: (diff u).v [= u proof (diff u).v = u \ v by Def7; then (diff u).v c= u by XBOOLE_1:36; then for a be set st a in (diff u).v ex b be set st b in u & b c= a; hence thesis by Lm8; end; theorem Th26: for a being Element of PFuncs (V, C) st a is finite for c being set st c in Atom(V, C).a holds c = a proof let a be Element of PFuncs (V, C); assume a is finite; then Atom(V, C).a = { a } by Lm7; hence thesis by TARSKI:def 1; end; theorem Th27: for a being Element of PFuncs (V, C) st K = {a} & L = u & L ^ K = {} holds Atom(V, C).a [= pseudo_compl(V, C).u proof let a be Element of PFuncs (V, C); assume A1: K = {a} & L = u & L ^ K = {}; then a in K by TARSKI:def 1; then A2: a is finite by Th2; now let c be set; assume A3: c in Atom(V, C).a; then A4: c = a by A2,Th26; reconsider c' = c as Element of PFuncs (V, C) by A2,A3,Th26; consider b be finite set such that A5: b in -L and A6: b c= c' by A1,A4,Th19; consider d be set such that A7: d c= b and A8: d in mi(-L) by A5,SUBSTLAT:10; take e = d; thus e in pseudo_compl(V, C).u by A1,A8,Def4; thus e c= c by A6,A7,XBOOLE_1:1; end; hence Atom(V, C).a [= pseudo_compl(V, C).u by Lm8; end; theorem Th28: for a being finite Element of PFuncs (V,C) holds a in Atom(V, C).a proof let a be finite Element of PFuncs (V,C); Atom(V, C).a = { a } by Lm7; hence thesis by TARSKI:def 1; end; Lm9: u [= v implies for x be set st x in u ex b be set st b in v & b c= x proof reconsider u' = u, v' = v as Element of SubstitutionSet (V, C) by SUBSTLAT:def 4; assume u [= v; then u = u "/\" v by LATTICES:21 .= (the L_meet of SubstLatt (V, C)).(u,v) by LATTICES:def 2 .= mi (u' ^ v') by SUBSTLAT:def 4; hence thesis by Th8; end; theorem Th29: for u, v being Element of SubstitutionSet (V, C) holds ((for c being set st c in u ex b being set st b in v & b c= c \/ a) implies ex b being set st b in u =>> v & b c= a ) proof let u, v be Element of SubstitutionSet (V, C); reconsider u' = u as Element of SubstLatt (V, C) by SUBSTLAT:def 4; assume that A1: for b be set st b in u ex c be set st c in v & c c= b \/ a; defpred P[set,set] means $2 in v & $2 c= $1 \/ a; A2: now let b be Element of PFuncs (V, C); assume b in u; then consider c be set such that A3: c in v & c c= b \/ a by A1; v c= PFuncs (V, C) by FINSUB_1:def 5; then reconsider c as Element of PFuncs (V, C) by A3; take x = c; thus P[b,x] by A3; end; consider f' be Element of Funcs(PFuncs (V, C), PFuncs (V, C)) such that A4: b in u implies P[b,f'.b] from FuncsChoice(A2); consider f2 be Function such that A5: f' = f2 & dom f2 = PFuncs (V, C) & rng f2 c= PFuncs (V, C) by FUNCT_2:def 2; set g = f'|u; A6: for b be set st b in u' holds g.b c= b \/ a proof let b be set; assume A7: b in u'; u c= PFuncs (V, C) by FINSUB_1:def 5; then reconsider b' = b as Element of PFuncs (V, C) by A7; g.b' = f2.b' by A5,A7,FUNCT_1:72; hence thesis by A4,A5,A7; end; A8: for b be set st b in u holds g.b in v proof let b be set; assume A9: b in u; u c= PFuncs (V, C) by FINSUB_1:def 5; then reconsider b' = b as Element of PFuncs (V, C) by A9; g.b' = f2.b' by A5,A9,FUNCT_1:72; hence thesis by A4,A5,A9; end; u c= PFuncs (V, C) by FINSUB_1:def 5; then g is Function of u, PFuncs (V, C) by FUNCT_2:38; then A10: dom g = u by FUNCT_2:def 1; then g is Function of u, v by A8,FUNCT_2:5; then rng g c= v by RELSET_1:12; then reconsider g as Element of PFuncs (u, v) by A10,PARTFUN1:def 5; set d = union {g.i \ i where i is Element of PFuncs (V, C) : i in u'}; A11: d c= a proof let x be set; assume x in d; then consider Y be set such that A12: x in Y & Y in {g.i \ i where i is Element of PFuncs (V, C) : i in u'} by TARSKI:def 4; consider j be Element of PFuncs (V, C) such that A13: Y = g.j \ j & j in u' by A12; g.j c= j \/ a by A6,A13; then g.j \j c= a by XBOOLE_1:43; hence thesis by A12,A13; end; then reconsider d as Element of PFuncs (V, C) by Th3; take d; d in { union {f.i \ i where i is Element of PFuncs (V, C) : i in u} where f is Element of PFuncs (u, v) : dom f = u } by A10; then d in PFuncs (V, C) /\ { union {f.i \ i where i is Element of PFuncs (V, C) : i in u} where f is Element of PFuncs (u, v) : dom f = u } by XBOOLE_0:def 3; hence d in u =>> v by Def3; thus thesis by A11; end; theorem Th30: for a being finite Element of PFuncs (V,C) st (for b being Element of PFuncs (V, C) st b in u holds b tolerates a ) & u "/\" Atom(V, C).a [= v holds Atom(V, C).a [= StrongImpl(V, C).(u, v) proof let a be finite Element of PFuncs (V,C); assume that A1: for b be Element of PFuncs (V, C) st b in u holds b tolerates a and A2: u "/\" Atom(V, C).a [= v; reconsider u' = u, v' = v, Aa = (Atom(V, C).a) as Element of SubstitutionSet (V, C) by SUBSTLAT:def 4; A3: now let c be set; assume A4: c in u; then A5: c in u'; then reconsider c' = c as Element of PFuncs (V, C) by SETWISEO:14; A6: a in Aa by Th28; A7: c' tolerates a by A1,A4; c is finite by A5,Th2; then A8: c \/ a is finite by FINSET_1:14; c \/ a in { s1 \/ t1 where s1,t1 is Element of PFuncs (V,C) : s1 in u' & t1 in Aa & s1 tolerates t1 } by A4,A6,A7; then c \/ a in u' ^ Aa by SUBSTLAT:def 3; then consider b be set such that A9: b c= c \/ a and A10: b in mi(u' ^ Aa) by A8,SUBSTLAT:10; b in (the L_meet of SubstLatt (V, C)).(u, Atom(V, C).a) by A10,SUBSTLAT:def 4; then b in u "/\" (Atom (V, C).a) by LATTICES:def 2; then consider d be set such that A11: d in v and A12: d c= b by A2,Lm9; take e = d; thus e in v by A11; thus e c= c \/ a by A9,A12,XBOOLE_1:1; end; now let c be set; assume A13: c in Atom(V, C).a; then c = a by Th26; then consider b be set such that A14: b in u' =>> v' and A15: b c= c by A3,Th29; c in Aa by A13; then c is finite by Th2; then b is finite by A15,FINSET_1:13; then consider d be set such that A16: d c= b and A17: d in mi(u' =>> v') by A14,SUBSTLAT:10; take e = d; thus e in (StrongImpl(V, C).(u, v)) by A17,Def5; thus e c= c by A15,A16,XBOOLE_1:1; end; hence Atom(V, C).a [= StrongImpl(V, C).(u, v) by Lm8; end; deffunc M(set, set) = the L_meet of SubstLatt ($1, $2); theorem Th31: u "/\" pseudo_compl(V, C).u = Bottom SubstLatt (V, C) proof reconsider u' = u as Element of SubstitutionSet (V, C) by SUBSTLAT:def 4; thus u "/\" pseudo_compl(V, C).u = M(V, C).(u, pseudo_compl(V, C).u) by LATTICES:def 2 .= M(V, C).(u, mi(-u')) by Def4 .= mi(u' ^ mi(-u')) by SUBSTLAT:def 4 .= mi(u' ^ -u') by SUBSTLAT:20 .= Bottom SubstLatt (V, C) by Th17; end; theorem Th32: u "/\" StrongImpl(V, C).(u, v) [= v proof now let a be set; reconsider u' = u, v' = v as Element of SubstitutionSet (V, C) by SUBSTLAT:def 4; A1: u "/\" StrongImpl(V, C).(u, v) = M(V, C).(u, StrongImpl(V, C).(u, v)) by LATTICES:def 2 .= M(V, C).(u, mi(u' =>> v')) by Def5 .= mi(u' ^ mi(u' =>> v')) by SUBSTLAT:def 4 .= mi(u' ^ (u' =>> v')) by SUBSTLAT:20; assume a in u "/\" StrongImpl(V, C).(u, v); then a in u' ^ (u' =>> v') by A1,SUBSTLAT:6; hence ex b be set st b in v & b c= a by Lm3; end; hence thesis by Lm8; end; Lm10: now let V, C, u, v; deffunc IMPL(Element of SubstLatt (V, C), Element of SubstLatt (V, C)) = FinJoin(SUB $1, M(V, C).:(pseudo_compl(V, C), StrongImpl(V, C)[:](diff $1, $2))); set Psi = M(V, C).:(pseudo_compl(V, C), StrongImpl(V, C)[:](diff u, v)); A1: now let w be Element of SubstLatt (V, C); set u2 = (diff u).w, pc = pseudo_compl(V, C).w, si = StrongImpl(V, C).(u2, v); assume w in SUB u; then A2: w "\/" u2 = u by Lm5; A3: w "/\" (pc "/\" si) = (w "/\" pc) "/\" si by LATTICES:def 7 .= Bottom SubstLatt (V, C) "/\" si by Th31 .= Bottom SubstLatt (V, C) by LATTICES:40; A4: u2 "/\" si [= v by Th32; M(V, C)[;](u, Psi).w = M(V, C).(u, Psi.w) by FUNCOP_1:66 .= u "/\" Psi.w by LATTICES:def 2 .= u "/\" M(V, C).(pc, StrongImpl(V, C)[:](diff u, v).w) by FUNCOP_1:48 .= u "/\" (pc "/\" StrongImpl(V, C)[:](diff u, v).w) by LATTICES:def 2 .= u "/\" (pc "/\" si) by FUNCOP_1:60 .= (w "/\" (pc "/\" si)) "\/" (u2 "/\" (pc "/\" si)) by A2,LATTICES:def 11 .= u2 "/\" (si "/\" pc) by A3,LATTICES:39 .= (u2 "/\" si) "/\" pc by LATTICES:def 7; then M(V, C)[;](u, Psi).w [= u2 "/\" si by LATTICES:23; hence M(V, C)[;](u, Psi).w [= v by A4,LATTICES:25; end; u "/\" IMPL(u,v) = FinJoin(SUB u, M(V, C)[;](u, Psi)) by LATTICE2:83; hence u "/\" IMPL(u,v) [= v by A1,LATTICE2:70; let w be Element of SubstLatt (V, C); reconsider v' = v as Element of SubstitutionSet (V, C) by SUBSTLAT:def 4; A5: v = FinJoin(v', Atom(V, C)) by Th24; then A6: u "/\" v = FinJoin(v', M(V, C)[;](u, Atom(V, C))) by LATTICE2:83; assume A7: u "/\" v [= w; now let a be Element of PFuncs (V, C); assume A8: a in v'; then M(V, C)[;](u, Atom(V, C)).a [= w by A6,A7,LATTICE2:46; then M(V, C).(u, Atom(V, C).a) [= w by FUNCOP_1:66; then A9: u "/\" Atom(V, C).a [= w by LATTICES:def 2; reconsider SA = {a} as Element of Fin PFuncs (V, C); A10: a is finite by A8,Th2; then reconsider SS = {a} as Element of SubstitutionSet (V, C) by Th6; consider v be Element of SubstitutionSet (V, C) such that A11: v in SUB u and A12: v ^ SA = {} and A13: for b be Element of PFuncs (V, C) st b in (diff u).v holds b tolerates a by A10,Lm6; A14: v ^ SS = {} by A12; reconsider v' = v as Element of SubstLatt (V, C) by SUBSTLAT:def 4; set dv = (diff u).v'; dv [= u by Th25; then dv "/\" Atom(V, C).a [= u "/\" Atom(V, C).a by LATTICES:27; then A15: dv "/\" Atom(V, C).a [= w by A9,LATTICES:25; set pf = pseudo_compl(V, C), sf = StrongImpl(V, C)[:](diff u, w); A16: a is finite by A8,Th2; A17: Atom(V, C).a [= pf.v' by A14,Th27; Atom(V, C).a [= StrongImpl(V, C).((diff u).v', w) by A13,A15,A16,Th30; then A18: Atom(V, C).a [= sf.v' by FUNCOP_1:60; pf.v'"/\" sf.v' = M(V, C).(pf.v', sf.v') by LATTICES:def 2 .= M(V, C).:(pf, sf).v' by FUNCOP_1:48; then Atom(V, C).a [= M(V, C).:(pf, sf).v' by A17,A18,FILTER_0:7; hence Atom(V, C).a [= IMPL(u,w) by A11,LATTICE2:44; end; hence v [= IMPL(u,w) by A5,LATTICE2:70; end; Lm11: SubstLatt (V, C) is implicative proof let p,q be Element of SubstLatt (V, C); take r = FinJoin(SUB p,M(V, C).:(pseudo_compl(V, C), StrongImpl(V, C)[:](diff p, q))); thus p "/\" r [= q & for r1 being Element of SubstLatt (V, C) st p "/\" r1 [= q holds r1 [= r by Lm10; end; definition let V, C; cluster SubstLatt (V, C) -> implicative; coherence by Lm11; end; theorem u => v = FinJoin(SUB u, (the L_meet of SubstLatt (V, C)).:(pseudo_compl(V, C), StrongImpl(V, C)[:](diff u, v))) proof deffunc IMPL(Element of SubstLatt (V, C), Element of SubstLatt (V, C)) = FinJoin(SUB $1,M(V, C).:(pseudo_compl(V, C), StrongImpl(V, C)[:](diff $1, $2))); u "/\" IMPL(u,v) [= v & for w be Element of SubstLatt (V, C) st u "/\" w [= v holds w [= IMPL(u,v) by Lm10; hence thesis by FILTER_0:def 8; end;

Back to top