:: A Model of ZF Set Theory Language :: by Grzegorz Bancerek :: :: Received April 4, 1989 :: Copyright (c) 1990-2012 Association of Mizar Users begin :: :: The Construction of ZF Set Theory Language :: :: The set and the mode of ZF-language variables definition func VAR -> Subset of NAT equals :: ZF_LANG:def 1 { k where k is Element of NAT : 5 <= k } ; coherence { k where k is Element of NAT : 5 <= k } is Subset of NAT proofend; end; :: deftheorem defines VAR ZF_LANG:def_1_:_ VAR = { k where k is Element of NAT : 5 <= k } ; registration cluster VAR -> non empty ; coherence not VAR is empty proofend; end; definition mode Variable is Element of VAR ; end; definition let n be Element of NAT ; func x. n -> Variable equals :: ZF_LANG:def 2 5 + n; coherence 5 + n is Variable proofend; end; :: deftheorem defines x. ZF_LANG:def_2_:_ for n being Element of NAT holds x. n = 5 + n; :: The operations to make ZF-formulae definition let x be Variable; :: original:<* redefine func<*x*> -> FinSequence of NAT ; coherence <*x*> is FinSequence of NAT proofend; end; definition let x, y be Variable; funcx '=' y -> FinSequence of NAT equals :: ZF_LANG:def 3 (<*0*> ^ <*x*>) ^ <*y*>; coherence (<*0*> ^ <*x*>) ^ <*y*> is FinSequence of NAT ; funcx 'in' y -> FinSequence of NAT equals :: ZF_LANG:def 4 (<*1*> ^ <*x*>) ^ <*y*>; coherence (<*1*> ^ <*x*>) ^ <*y*> is FinSequence of NAT ; end; :: deftheorem defines '=' ZF_LANG:def_3_:_ for x, y being Variable holds x '=' y = (<*0*> ^ <*x*>) ^ <*y*>; :: deftheorem defines 'in' ZF_LANG:def_4_:_ for x, y being Variable holds x 'in' y = (<*1*> ^ <*x*>) ^ <*y*>; theorem :: ZF_LANG:1 for x, y, z, t being Variable st x '=' y = z '=' t holds ( x = z & y = t ) proofend; theorem :: ZF_LANG:2 for x, y, z, t being Variable st x 'in' y = z 'in' t holds ( x = z & y = t ) proofend; definition let p be FinSequence of NAT ; func 'not' p -> FinSequence of NAT equals :: ZF_LANG:def 5 <*2*> ^ p; coherence <*2*> ^ p is FinSequence of NAT ; let q be FinSequence of NAT ; funcp '&' q -> FinSequence of NAT equals :: ZF_LANG:def 6 (<*3*> ^ p) ^ q; coherence (<*3*> ^ p) ^ q is FinSequence of NAT ; end; :: deftheorem defines 'not' ZF_LANG:def_5_:_ for p being FinSequence of NAT holds 'not' p = <*2*> ^ p; :: deftheorem defines '&' ZF_LANG:def_6_:_ for p, q being FinSequence of NAT holds p '&' q = (<*3*> ^ p) ^ q; definition let x be Variable; let p be FinSequence of NAT ; func All (x,p) -> FinSequence of NAT equals :: ZF_LANG:def 7 (<*4*> ^ <*x*>) ^ p; coherence (<*4*> ^ <*x*>) ^ p is FinSequence of NAT ; end; :: deftheorem defines All ZF_LANG:def_7_:_ for x being Variable for p being FinSequence of NAT holds All (x,p) = (<*4*> ^ <*x*>) ^ p; theorem Th3: :: ZF_LANG:3 for p, q being FinSequence of NAT for x, y being Variable st All (x,p) = All (y,q) holds ( x = y & p = q ) proofend; :: The set of all well formed formulae of ZF-language definition func WFF -> non empty set means :Def8: :: ZF_LANG:def 8 ( ( for a being set st a in it holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in it & x 'in' y in it ) ) & ( for p being FinSequence of NAT st p in it holds 'not' p in it ) & ( for p, q being FinSequence of NAT st p in it & q in it holds p '&' q in it ) & ( for x being Variable for p being FinSequence of NAT st p in it holds All (x,p) in it ) & ( for D being non empty set st ( for a being set st a in D holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds 'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p '&' q in D ) & ( for x being Variable for p being FinSequence of NAT st p in D holds All (x,p) in D ) holds it c= D ) ); existence ex b1 being non empty set st ( ( for a being set st a in b1 holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in b1 & x 'in' y in b1 ) ) & ( for p being FinSequence of NAT st p in b1 holds 'not' p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds p '&' q in b1 ) & ( for x being Variable for p being FinSequence of NAT st p in b1 holds All (x,p) in b1 ) & ( for D being non empty set st ( for a being set st a in D holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds 'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p '&' q in D ) & ( for x being Variable for p being FinSequence of NAT st p in D holds All (x,p) in D ) holds b1 c= D ) ) proofend; uniqueness for b1, b2 being non empty set st ( for a being set st a in b1 holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in b1 & x 'in' y in b1 ) ) & ( for p being FinSequence of NAT st p in b1 holds 'not' p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds p '&' q in b1 ) & ( for x being Variable for p being FinSequence of NAT st p in b1 holds All (x,p) in b1 ) & ( for D being non empty set st ( for a being set st a in D holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds 'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p '&' q in D ) & ( for x being Variable for p being FinSequence of NAT st p in D holds All (x,p) in D ) holds b1 c= D ) & ( for a being set st a in b2 holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in b2 & x 'in' y in b2 ) ) & ( for p being FinSequence of NAT st p in b2 holds 'not' p in b2 ) & ( for p, q being FinSequence of NAT st p in b2 & q in b2 holds p '&' q in b2 ) & ( for x being Variable for p being FinSequence of NAT st p in b2 holds All (x,p) in b2 ) & ( for D being non empty set st ( for a being set st a in D holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds 'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p '&' q in D ) & ( for x being Variable for p being FinSequence of NAT st p in D holds All (x,p) in D ) holds b2 c= D ) holds b1 = b2 proofend; end; :: deftheorem Def8 defines WFF ZF_LANG:def_8_:_ for b1 being non empty set holds ( b1 = WFF iff ( ( for a being set st a in b1 holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in b1 & x 'in' y in b1 ) ) & ( for p being FinSequence of NAT st p in b1 holds 'not' p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds p '&' q in b1 ) & ( for x being Variable for p being FinSequence of NAT st p in b1 holds All (x,p) in b1 ) & ( for D being non empty set st ( for a being set st a in D holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds 'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p '&' q in D ) & ( for x being Variable for p being FinSequence of NAT st p in D holds All (x,p) in D ) holds b1 c= D ) ) ); definition let IT be FinSequence of NAT ; attrIT is ZF-formula-like means :Def9: :: ZF_LANG:def 9 IT is Element of WFF ; end; :: deftheorem Def9 defines ZF-formula-like ZF_LANG:def_9_:_ for IT being FinSequence of NAT holds ( IT is ZF-formula-like iff IT is Element of WFF ); registration cluster Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like ZF-formula-like for FinSequence of NAT ; existence ex b1 being FinSequence of NAT st b1 is ZF-formula-like proofend; end; definition mode ZF-formula is ZF-formula-like FinSequence of NAT ; end; theorem :: ZF_LANG:4 for a being set holds ( a is ZF-formula iff a in WFF ) proofend; registration let x, y be Variable; clusterx '=' y -> ZF-formula-like ; coherence x '=' y is ZF-formula-like proofend; clusterx 'in' y -> ZF-formula-like ; coherence x 'in' y is ZF-formula-like proofend; end; registration let H be ZF-formula; cluster 'not' H -> ZF-formula-like ; coherence 'not' H is ZF-formula-like proofend; let G be ZF-formula; clusterH '&' G -> ZF-formula-like ; coherence H '&' G is ZF-formula-like proofend; end; registration let x be Variable; let H be ZF-formula; cluster All (x,H) -> ZF-formula-like ; coherence All (x,H) is ZF-formula-like proofend; end; :: :: The Properties of ZF-formulae :: definition let H be ZF-formula; attrH is being_equality means :Def10: :: ZF_LANG:def 10 ex x, y being Variable st H = x '=' y; attrH is being_membership means :Def11: :: ZF_LANG:def 11 ex x, y being Variable st H = x 'in' y; attrH is negative means :Def12: :: ZF_LANG:def 12 ex H1 being ZF-formula st H = 'not' H1; attrH is conjunctive means :Def13: :: ZF_LANG:def 13 ex F, G being ZF-formula st H = F '&' G; attrH is universal means :Def14: :: ZF_LANG:def 14 ex x being Variable ex H1 being ZF-formula st H = All (x,H1); end; :: deftheorem Def10 defines being_equality ZF_LANG:def_10_:_ for H being ZF-formula holds ( H is being_equality iff ex x, y being Variable st H = x '=' y ); :: deftheorem Def11 defines being_membership ZF_LANG:def_11_:_ for H being ZF-formula holds ( H is being_membership iff ex x, y being Variable st H = x 'in' y ); :: deftheorem Def12 defines negative ZF_LANG:def_12_:_ for H being ZF-formula holds ( H is negative iff ex H1 being ZF-formula st H = 'not' H1 ); :: deftheorem Def13 defines conjunctive ZF_LANG:def_13_:_ for H being ZF-formula holds ( H is conjunctive iff ex F, G being ZF-formula st H = F '&' G ); :: deftheorem Def14 defines universal ZF_LANG:def_14_:_ for H being ZF-formula holds ( H is universal iff ex x being Variable ex H1 being ZF-formula st H = All (x,H1) ); theorem :: ZF_LANG:5 for H being ZF-formula holds ( ( H is being_equality implies ex x, y being Variable st H = x '=' y ) & ( ex x, y being Variable st H = x '=' y implies H is being_equality ) & ( H is being_membership implies ex x, y being Variable st H = x 'in' y ) & ( ex x, y being Variable st H = x 'in' y implies H is being_membership ) & ( H is negative implies ex H1 being ZF-formula st H = 'not' H1 ) & ( ex H1 being ZF-formula st H = 'not' H1 implies H is negative ) & ( H is conjunctive implies ex F, G being ZF-formula st H = F '&' G ) & ( ex F, G being ZF-formula st H = F '&' G implies H is conjunctive ) & ( H is universal implies ex x being Variable ex H1 being ZF-formula st H = All (x,H1) ) & ( ex x being Variable ex H1 being ZF-formula st H = All (x,H1) implies H is universal ) ) by Def10, Def11, Def12, Def13, Def14; definition let H be ZF-formula; attrH is atomic means :Def15: :: ZF_LANG:def 15 ( H is being_equality or H is being_membership ); end; :: deftheorem Def15 defines atomic ZF_LANG:def_15_:_ for H being ZF-formula holds ( H is atomic iff ( H is being_equality or H is being_membership ) ); definition let F, G be ZF-formula; funcF 'or' G -> ZF-formula equals :: ZF_LANG:def 16 'not' (('not' F) '&' ('not' G)); coherence 'not' (('not' F) '&' ('not' G)) is ZF-formula ; funcF => G -> ZF-formula equals :: ZF_LANG:def 17 'not' (F '&' ('not' G)); coherence 'not' (F '&' ('not' G)) is ZF-formula ; end; :: deftheorem defines 'or' ZF_LANG:def_16_:_ for F, G being ZF-formula holds F 'or' G = 'not' (('not' F) '&' ('not' G)); :: deftheorem defines => ZF_LANG:def_17_:_ for F, G being ZF-formula holds F => G = 'not' (F '&' ('not' G)); definition let F, G be ZF-formula; funcF <=> G -> ZF-formula equals :: ZF_LANG:def 18 (F => G) '&' (G => F); coherence (F => G) '&' (G => F) is ZF-formula ; end; :: deftheorem defines <=> ZF_LANG:def_18_:_ for F, G being ZF-formula holds F <=> G = (F => G) '&' (G => F); definition let x be Variable; let H be ZF-formula; func Ex (x,H) -> ZF-formula equals :: ZF_LANG:def 19 'not' (All (x,('not' H))); coherence 'not' (All (x,('not' H))) is ZF-formula ; end; :: deftheorem defines Ex ZF_LANG:def_19_:_ for x being Variable for H being ZF-formula holds Ex (x,H) = 'not' (All (x,('not' H))); definition let H be ZF-formula; attrH is disjunctive means :Def20: :: ZF_LANG:def 20 ex F, G being ZF-formula st H = F 'or' G; attrH is conditional means :Def21: :: ZF_LANG:def 21 ex F, G being ZF-formula st H = F => G; attrH is biconditional means :Def22: :: ZF_LANG:def 22 ex F, G being ZF-formula st H = F <=> G; attrH is existential means :Def23: :: ZF_LANG:def 23 ex x being Variable ex H1 being ZF-formula st H = Ex (x,H1); end; :: deftheorem Def20 defines disjunctive ZF_LANG:def_20_:_ for H being ZF-formula holds ( H is disjunctive iff ex F, G being ZF-formula st H = F 'or' G ); :: deftheorem Def21 defines conditional ZF_LANG:def_21_:_ for H being ZF-formula holds ( H is conditional iff ex F, G being ZF-formula st H = F => G ); :: deftheorem Def22 defines biconditional ZF_LANG:def_22_:_ for H being ZF-formula holds ( H is biconditional iff ex F, G being ZF-formula st H = F <=> G ); :: deftheorem Def23 defines existential ZF_LANG:def_23_:_ for H being ZF-formula holds ( H is existential iff ex x being Variable ex H1 being ZF-formula st H = Ex (x,H1) ); theorem :: ZF_LANG:6 for H being ZF-formula holds ( ( H is disjunctive implies ex F, G being ZF-formula st H = F 'or' G ) & ( ex F, G being ZF-formula st H = F 'or' G implies H is disjunctive ) & ( H is conditional implies ex F, G being ZF-formula st H = F => G ) & ( ex F, G being ZF-formula st H = F => G implies H is conditional ) & ( H is biconditional implies ex F, G being ZF-formula st H = F <=> G ) & ( ex F, G being ZF-formula st H = F <=> G implies H is biconditional ) & ( H is existential implies ex x being Variable ex H1 being ZF-formula st H = Ex (x,H1) ) & ( ex x being Variable ex H1 being ZF-formula st H = Ex (x,H1) implies H is existential ) ) by Def20, Def21, Def22, Def23; definition let x, y be Variable; let H be ZF-formula; func All (x,y,H) -> ZF-formula equals :: ZF_LANG:def 24 All (x,(All (y,H))); coherence All (x,(All (y,H))) is ZF-formula ; func Ex (x,y,H) -> ZF-formula equals :: ZF_LANG:def 25 Ex (x,(Ex (y,H))); coherence Ex (x,(Ex (y,H))) is ZF-formula ; end; :: deftheorem defines All ZF_LANG:def_24_:_ for x, y being Variable for H being ZF-formula holds All (x,y,H) = All (x,(All (y,H))); :: deftheorem defines Ex ZF_LANG:def_25_:_ for x, y being Variable for H being ZF-formula holds Ex (x,y,H) = Ex (x,(Ex (y,H))); theorem :: ZF_LANG:7 for x, y being Variable for H being ZF-formula holds ( All (x,y,H) = All (x,(All (y,H))) & Ex (x,y,H) = Ex (x,(Ex (y,H))) ) ; definition let x, y, z be Variable; let H be ZF-formula; func All (x,y,z,H) -> ZF-formula equals :: ZF_LANG:def 26 All (x,(All (y,z,H))); coherence All (x,(All (y,z,H))) is ZF-formula ; func Ex (x,y,z,H) -> ZF-formula equals :: ZF_LANG:def 27 Ex (x,(Ex (y,z,H))); coherence Ex (x,(Ex (y,z,H))) is ZF-formula ; end; :: deftheorem defines All ZF_LANG:def_26_:_ for x, y, z being Variable for H being ZF-formula holds All (x,y,z,H) = All (x,(All (y,z,H))); :: deftheorem defines Ex ZF_LANG:def_27_:_ for x, y, z being Variable for H being ZF-formula holds Ex (x,y,z,H) = Ex (x,(Ex (y,z,H))); theorem :: ZF_LANG:8 for x, y, z being Variable for H being ZF-formula holds ( All (x,y,z,H) = All (x,(All (y,z,H))) & Ex (x,y,z,H) = Ex (x,(Ex (y,z,H))) ) ; theorem Th9: :: ZF_LANG:9 for H being ZF-formula holds ( H is being_equality or H is being_membership or H is negative or H is conjunctive or H is universal ) proofend; theorem Th10: :: ZF_LANG:10 for H being ZF-formula holds ( H is atomic or H is negative or H is conjunctive or H is universal ) proofend; theorem Th11: :: ZF_LANG:11 for H being ZF-formula st H is atomic holds len H = 3 proofend; theorem Th12: :: ZF_LANG:12 for H being ZF-formula holds ( H is atomic or ex H1 being ZF-formula st (len H1) + 1 <= len H ) proofend; theorem Th13: :: ZF_LANG:13 for H being ZF-formula holds 3 <= len H proofend; theorem :: ZF_LANG:14 for H being ZF-formula st len H = 3 holds H is atomic proofend; theorem Th15: :: ZF_LANG:15 for x, y being Variable holds ( (x '=' y) . 1 = 0 & (x 'in' y) . 1 = 1 ) proofend; theorem Th16: :: ZF_LANG:16 for F, G being ZF-formula holds (F '&' G) . 1 = 3 proofend; theorem Th17: :: ZF_LANG:17 for x being Variable for H being ZF-formula holds (All (x,H)) . 1 = 4 proofend; theorem Th18: :: ZF_LANG:18 for H being ZF-formula st H is being_equality holds H . 1 = 0 proofend; theorem Th19: :: ZF_LANG:19 for H being ZF-formula st H is being_membership holds H . 1 = 1 proofend; theorem Th20: :: ZF_LANG:20 for H being ZF-formula st H is negative holds H . 1 = 2 proofend; theorem Th21: :: ZF_LANG:21 for H being ZF-formula st H is conjunctive holds H . 1 = 3 proofend; theorem Th22: :: ZF_LANG:22 for H being ZF-formula st H is universal holds H . 1 = 4 proofend; theorem Th23: :: ZF_LANG:23 for H being ZF-formula holds ( ( H is being_equality & H . 1 = 0 ) or ( H is being_membership & H . 1 = 1 ) or ( H is negative & H . 1 = 2 ) or ( H is conjunctive & H . 1 = 3 ) or ( H is universal & H . 1 = 4 ) ) proofend; theorem :: ZF_LANG:24 for H being ZF-formula st H . 1 = 0 holds H is being_equality by Th23; theorem :: ZF_LANG:25 for H being ZF-formula st H . 1 = 1 holds H is being_membership by Th23; theorem :: ZF_LANG:26 for H being ZF-formula st H . 1 = 2 holds H is negative by Th23; theorem :: ZF_LANG:27 for H being ZF-formula st H . 1 = 3 holds H is conjunctive by Th23; theorem :: ZF_LANG:28 for H being ZF-formula st H . 1 = 4 holds H is universal by Th23; theorem Th29: :: ZF_LANG:29 for H, F being ZF-formula for sq being FinSequence st H = F ^ sq holds H = F proofend; theorem Th30: :: ZF_LANG:30 for H, G, H1, G1 being ZF-formula st H '&' G = H1 '&' G1 holds ( H = H1 & G = G1 ) proofend; theorem Th31: :: ZF_LANG:31 for F, G, F1, G1 being ZF-formula st F 'or' G = F1 'or' G1 holds ( F = F1 & G = G1 ) proofend; theorem Th32: :: ZF_LANG:32 for F, G, F1, G1 being ZF-formula st F => G = F1 => G1 holds ( F = F1 & G = G1 ) proofend; theorem Th33: :: ZF_LANG:33 for F, G, F1, G1 being ZF-formula st F <=> G = F1 <=> G1 holds ( F = F1 & G = G1 ) proofend; theorem Th34: :: ZF_LANG:34 for x, y being Variable for H, G being ZF-formula st Ex (x,H) = Ex (y,G) holds ( x = y & H = G ) proofend; :: :: The Select Function of ZF-fomrulae :: definition let H be ZF-formula; assume A1: H is atomic ; func Var1 H -> Variable equals :Def28: :: ZF_LANG:def 28 H . 2; coherence H . 2 is Variable proofend; func Var2 H -> Variable equals :Def29: :: ZF_LANG:def 29 H . 3; coherence H . 3 is Variable proofend; end; :: deftheorem Def28 defines Var1 ZF_LANG:def_28_:_ for H being ZF-formula st H is atomic holds Var1 H = H . 2; :: deftheorem Def29 defines Var2 ZF_LANG:def_29_:_ for H being ZF-formula st H is atomic holds Var2 H = H . 3; theorem :: ZF_LANG:35 for H being ZF-formula st H is atomic holds ( Var1 H = H . 2 & Var2 H = H . 3 ) by Def28, Def29; theorem Th36: :: ZF_LANG:36 for H being ZF-formula st H is being_equality holds H = (Var1 H) '=' (Var2 H) proofend; theorem Th37: :: ZF_LANG:37 for H being ZF-formula st H is being_membership holds H = (Var1 H) 'in' (Var2 H) proofend; definition let H be ZF-formula; assume A1: H is negative ; func the_argument_of H -> ZF-formula means :Def30: :: ZF_LANG:def 30 'not' it = H; existence ex b1 being ZF-formula st 'not' b1 = H by A1, Def12; uniqueness for b1, b2 being ZF-formula st 'not' b1 = H & 'not' b2 = H holds b1 = b2 by FINSEQ_1:33; end; :: deftheorem Def30 defines the_argument_of ZF_LANG:def_30_:_ for H being ZF-formula st H is negative holds for b2 being ZF-formula holds ( b2 = the_argument_of H iff 'not' b2 = H ); definition let H be ZF-formula; assume A1: ( H is conjunctive or H is disjunctive ) ; func the_left_argument_of H -> ZF-formula means :Def31: :: ZF_LANG:def 31 ex H1 being ZF-formula st it '&' H1 = H if H is conjunctive otherwise ex H1 being ZF-formula st it 'or' H1 = H; existence ( ( H is conjunctive implies ex b1, H1 being ZF-formula st b1 '&' H1 = H ) & ( not H is conjunctive implies ex b1, H1 being ZF-formula st b1 'or' H1 = H ) ) by A1, Def13, Def20; uniqueness for b1, b2 being ZF-formula holds ( ( H is conjunctive & ex H1 being ZF-formula st b1 '&' H1 = H & ex H1 being ZF-formula st b2 '&' H1 = H implies b1 = b2 ) & ( not H is conjunctive & ex H1 being ZF-formula st b1 'or' H1 = H & ex H1 being ZF-formula st b2 'or' H1 = H implies b1 = b2 ) ) by Th30, Th31; consistency for b1 being ZF-formula holds verum ; func the_right_argument_of H -> ZF-formula means :Def32: :: ZF_LANG:def 32 ex H1 being ZF-formula st H1 '&' it = H if H is conjunctive otherwise ex H1 being ZF-formula st H1 'or' it = H; existence ( ( H is conjunctive implies ex b1, H1 being ZF-formula st H1 '&' b1 = H ) & ( not H is conjunctive implies ex b1, H1 being ZF-formula st H1 'or' b1 = H ) ) proofend; uniqueness for b1, b2 being ZF-formula holds ( ( H is conjunctive & ex H1 being ZF-formula st H1 '&' b1 = H & ex H1 being ZF-formula st H1 '&' b2 = H implies b1 = b2 ) & ( not H is conjunctive & ex H1 being ZF-formula st H1 'or' b1 = H & ex H1 being ZF-formula st H1 'or' b2 = H implies b1 = b2 ) ) by Th30, Th31; consistency for b1 being ZF-formula holds verum ; end; :: deftheorem Def31 defines the_left_argument_of ZF_LANG:def_31_:_ for H being ZF-formula st ( H is conjunctive or H is disjunctive ) holds for b2 being ZF-formula holds ( ( H is conjunctive implies ( b2 = the_left_argument_of H iff ex H1 being ZF-formula st b2 '&' H1 = H ) ) & ( not H is conjunctive implies ( b2 = the_left_argument_of H iff ex H1 being ZF-formula st b2 'or' H1 = H ) ) ); :: deftheorem Def32 defines the_right_argument_of ZF_LANG:def_32_:_ for H being ZF-formula st ( H is conjunctive or H is disjunctive ) holds for b2 being ZF-formula holds ( ( H is conjunctive implies ( b2 = the_right_argument_of H iff ex H1 being ZF-formula st H1 '&' b2 = H ) ) & ( not H is conjunctive implies ( b2 = the_right_argument_of H iff ex H1 being ZF-formula st H1 'or' b2 = H ) ) ); theorem :: ZF_LANG:38 for H, F being ZF-formula st H is conjunctive holds ( ( F = the_left_argument_of H implies ex G being ZF-formula st F '&' G = H ) & ( ex G being ZF-formula st F '&' G = H implies F = the_left_argument_of H ) & ( F = the_right_argument_of H implies ex G being ZF-formula st G '&' F = H ) & ( ex G being ZF-formula st G '&' F = H implies F = the_right_argument_of H ) ) by Def31, Def32; theorem Th39: :: ZF_LANG:39 for H, F being ZF-formula st H is disjunctive holds ( ( F = the_left_argument_of H implies ex G being ZF-formula st F 'or' G = H ) & ( ex G being ZF-formula st F 'or' G = H implies F = the_left_argument_of H ) & ( F = the_right_argument_of H implies ex G being ZF-formula st G 'or' F = H ) & ( ex G being ZF-formula st G 'or' F = H implies F = the_right_argument_of H ) ) proofend; theorem Th40: :: ZF_LANG:40 for H being ZF-formula st H is conjunctive holds H = (the_left_argument_of H) '&' (the_right_argument_of H) proofend; theorem :: ZF_LANG:41 for H being ZF-formula st H is disjunctive holds H = (the_left_argument_of H) 'or' (the_right_argument_of H) proofend; definition let H be ZF-formula; assume A1: ( H is universal or H is existential ) ; func bound_in H -> Variable means :Def33: :: ZF_LANG:def 33 ex H1 being ZF-formula st All (it,H1) = H if H is universal otherwise ex H1 being ZF-formula st Ex (it,H1) = H; existence ( ( H is universal implies ex b1 being Variable ex H1 being ZF-formula st All (b1,H1) = H ) & ( not H is universal implies ex b1 being Variable ex H1 being ZF-formula st Ex (b1,H1) = H ) ) by A1, Def14, Def23; uniqueness for b1, b2 being Variable holds ( ( H is universal & ex H1 being ZF-formula st All (b1,H1) = H & ex H1 being ZF-formula st All (b2,H1) = H implies b1 = b2 ) & ( not H is universal & ex H1 being ZF-formula st Ex (b1,H1) = H & ex H1 being ZF-formula st Ex (b2,H1) = H implies b1 = b2 ) ) by Th3, Th34; consistency for b1 being Variable holds verum ; func the_scope_of H -> ZF-formula means :Def34: :: ZF_LANG:def 34 ex x being Variable st All (x,it) = H if H is universal otherwise ex x being Variable st Ex (x,it) = H; existence ( ( H is universal implies ex b1 being ZF-formula ex x being Variable st All (x,b1) = H ) & ( not H is universal implies ex b1 being ZF-formula ex x being Variable st Ex (x,b1) = H ) ) proofend; uniqueness for b1, b2 being ZF-formula holds ( ( H is universal & ex x being Variable st All (x,b1) = H & ex x being Variable st All (x,b2) = H implies b1 = b2 ) & ( not H is universal & ex x being Variable st Ex (x,b1) = H & ex x being Variable st Ex (x,b2) = H implies b1 = b2 ) ) by Th3, Th34; consistency for b1 being ZF-formula holds verum ; end; :: deftheorem Def33 defines bound_in ZF_LANG:def_33_:_ for H being ZF-formula st ( H is universal or H is existential ) holds for b2 being Variable holds ( ( H is universal implies ( b2 = bound_in H iff ex H1 being ZF-formula st All (b2,H1) = H ) ) & ( not H is universal implies ( b2 = bound_in H iff ex H1 being ZF-formula st Ex (b2,H1) = H ) ) ); :: deftheorem Def34 defines the_scope_of ZF_LANG:def_34_:_ for H being ZF-formula st ( H is universal or H is existential ) holds for b2 being ZF-formula holds ( ( H is universal implies ( b2 = the_scope_of H iff ex x being Variable st All (x,b2) = H ) ) & ( not H is universal implies ( b2 = the_scope_of H iff ex x being Variable st Ex (x,b2) = H ) ) ); theorem :: ZF_LANG:42 for x being Variable for H, H1 being ZF-formula st H is universal holds ( ( x = bound_in H implies ex H1 being ZF-formula st All (x,H1) = H ) & ( ex H1 being ZF-formula st All (x,H1) = H implies x = bound_in H ) & ( H1 = the_scope_of H implies ex x being Variable st All (x,H1) = H ) & ( ex x being Variable st All (x,H1) = H implies H1 = the_scope_of H ) ) by Def33, Def34; theorem Th43: :: ZF_LANG:43 for x being Variable for H, H1 being ZF-formula st H is existential holds ( ( x = bound_in H implies ex H1 being ZF-formula st Ex (x,H1) = H ) & ( ex H1 being ZF-formula st Ex (x,H1) = H implies x = bound_in H ) & ( H1 = the_scope_of H implies ex x being Variable st Ex (x,H1) = H ) & ( ex x being Variable st Ex (x,H1) = H implies H1 = the_scope_of H ) ) proofend; theorem Th44: :: ZF_LANG:44 for H being ZF-formula st H is universal holds H = All ((bound_in H),(the_scope_of H)) proofend; theorem :: ZF_LANG:45 for H being ZF-formula st H is existential holds H = Ex ((bound_in H),(the_scope_of H)) proofend; definition let H be ZF-formula; assume A1: H is conditional ; func the_antecedent_of H -> ZF-formula means :Def35: :: ZF_LANG:def 35 ex H1 being ZF-formula st H = it => H1; existence ex b1, H1 being ZF-formula st H = b1 => H1 by A1, Def21; uniqueness for b1, b2 being ZF-formula st ex H1 being ZF-formula st H = b1 => H1 & ex H1 being ZF-formula st H = b2 => H1 holds b1 = b2 by Th32; func the_consequent_of H -> ZF-formula means :Def36: :: ZF_LANG:def 36 ex H1 being ZF-formula st H = H1 => it; existence ex b1, H1 being ZF-formula st H = H1 => b1 proofend; uniqueness for b1, b2 being ZF-formula st ex H1 being ZF-formula st H = H1 => b1 & ex H1 being ZF-formula st H = H1 => b2 holds b1 = b2 by Th32; end; :: deftheorem Def35 defines the_antecedent_of ZF_LANG:def_35_:_ for H being ZF-formula st H is conditional holds for b2 being ZF-formula holds ( b2 = the_antecedent_of H iff ex H1 being ZF-formula st H = b2 => H1 ); :: deftheorem Def36 defines the_consequent_of ZF_LANG:def_36_:_ for H being ZF-formula st H is conditional holds for b2 being ZF-formula holds ( b2 = the_consequent_of H iff ex H1 being ZF-formula st H = H1 => b2 ); theorem :: ZF_LANG:46 for H, F being ZF-formula st H is conditional holds ( ( F = the_antecedent_of H implies ex G being ZF-formula st H = F => G ) & ( ex G being ZF-formula st H = F => G implies F = the_antecedent_of H ) & ( F = the_consequent_of H implies ex G being ZF-formula st H = G => F ) & ( ex G being ZF-formula st H = G => F implies F = the_consequent_of H ) ) by Def35, Def36; theorem :: ZF_LANG:47 for H being ZF-formula st H is conditional holds H = (the_antecedent_of H) => (the_consequent_of H) proofend; definition let H be ZF-formula; assume A1: H is biconditional ; func the_left_side_of H -> ZF-formula means :Def37: :: ZF_LANG:def 37 ex H1 being ZF-formula st H = it <=> H1; existence ex b1, H1 being ZF-formula st H = b1 <=> H1 by A1, Def22; uniqueness for b1, b2 being ZF-formula st ex H1 being ZF-formula st H = b1 <=> H1 & ex H1 being ZF-formula st H = b2 <=> H1 holds b1 = b2 by Th33; func the_right_side_of H -> ZF-formula means :Def38: :: ZF_LANG:def 38 ex H1 being ZF-formula st H = H1 <=> it; existence ex b1, H1 being ZF-formula st H = H1 <=> b1 proofend; uniqueness for b1, b2 being ZF-formula st ex H1 being ZF-formula st H = H1 <=> b1 & ex H1 being ZF-formula st H = H1 <=> b2 holds b1 = b2 by Th33; end; :: deftheorem Def37 defines the_left_side_of ZF_LANG:def_37_:_ for H being ZF-formula st H is biconditional holds for b2 being ZF-formula holds ( b2 = the_left_side_of H iff ex H1 being ZF-formula st H = b2 <=> H1 ); :: deftheorem Def38 defines the_right_side_of ZF_LANG:def_38_:_ for H being ZF-formula st H is biconditional holds for b2 being ZF-formula holds ( b2 = the_right_side_of H iff ex H1 being ZF-formula st H = H1 <=> b2 ); theorem :: ZF_LANG:48 for H, F being ZF-formula st H is biconditional holds ( ( F = the_left_side_of H implies ex G being ZF-formula st H = F <=> G ) & ( ex G being ZF-formula st H = F <=> G implies F = the_left_side_of H ) & ( F = the_right_side_of H implies ex G being ZF-formula st H = G <=> F ) & ( ex G being ZF-formula st H = G <=> F implies F = the_right_side_of H ) ) by Def37, Def38; theorem :: ZF_LANG:49 for H being ZF-formula st H is biconditional holds H = (the_left_side_of H) <=> (the_right_side_of H) proofend; :: :: The Immediate Constituents of ZF-formulae :: definition let H, F be ZF-formula; predH is_immediate_constituent_of F means :Def39: :: ZF_LANG:def 39 ( F = 'not' H or ex H1 being ZF-formula st ( F = H '&' H1 or F = H1 '&' H ) or ex x being Variable st F = All (x,H) ); end; :: deftheorem Def39 defines is_immediate_constituent_of ZF_LANG:def_39_:_ for H, F being ZF-formula holds ( H is_immediate_constituent_of F iff ( F = 'not' H or ex H1 being ZF-formula st ( F = H '&' H1 or F = H1 '&' H ) or ex x being Variable st F = All (x,H) ) ); theorem Th50: :: ZF_LANG:50 for x, y being Variable for H being ZF-formula holds not H is_immediate_constituent_of x '=' y proofend; theorem Th51: :: ZF_LANG:51 for x, y being Variable for H being ZF-formula holds not H is_immediate_constituent_of x 'in' y proofend; theorem Th52: :: ZF_LANG:52 for F, H being ZF-formula holds ( F is_immediate_constituent_of 'not' H iff F = H ) proofend; theorem Th53: :: ZF_LANG:53 for F, G, H being ZF-formula holds ( F is_immediate_constituent_of G '&' H iff ( F = G or F = H ) ) proofend; theorem Th54: :: ZF_LANG:54 for x being Variable for F, H being ZF-formula holds ( F is_immediate_constituent_of All (x,H) iff F = H ) proofend; theorem :: ZF_LANG:55 for H, F being ZF-formula st H is atomic holds not F is_immediate_constituent_of H proofend; theorem Th56: :: ZF_LANG:56 for H, F being ZF-formula st H is negative holds ( F is_immediate_constituent_of H iff F = the_argument_of H ) proofend; theorem Th57: :: ZF_LANG:57 for H, F being ZF-formula st H is conjunctive holds ( F is_immediate_constituent_of H iff ( F = the_left_argument_of H or F = the_right_argument_of H ) ) proofend; theorem Th58: :: ZF_LANG:58 for H, F being ZF-formula st H is universal holds ( F is_immediate_constituent_of H iff F = the_scope_of H ) proofend; definition let H, F be ZF-formula; predH is_subformula_of F means :Def40: :: ZF_LANG:def 40 ex n being Element of NAT ex L being FinSequence st ( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Element of NAT st 1 <= k & k < n holds ex H1, F1 being ZF-formula st ( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ); end; :: deftheorem Def40 defines is_subformula_of ZF_LANG:def_40_:_ for H, F being ZF-formula holds ( H is_subformula_of F iff ex n being Element of NAT ex L being FinSequence st ( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Element of NAT st 1 <= k & k < n holds ex H1, F1 being ZF-formula st ( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) ); theorem Th59: :: ZF_LANG:59 for H being ZF-formula holds H is_subformula_of H proofend; definition let H, F be ZF-formula; predH is_proper_subformula_of F means :Def41: :: ZF_LANG:def 41 ( H is_subformula_of F & H <> F ); end; :: deftheorem Def41 defines is_proper_subformula_of ZF_LANG:def_41_:_ for H, F being ZF-formula holds ( H is_proper_subformula_of F iff ( H is_subformula_of F & H <> F ) ); theorem Th60: :: ZF_LANG:60 for H, F being ZF-formula st H is_immediate_constituent_of F holds len H < len F proofend; theorem Th61: :: ZF_LANG:61 for H, F being ZF-formula st H is_immediate_constituent_of F holds H is_proper_subformula_of F proofend; theorem Th62: :: ZF_LANG:62 for H, F being ZF-formula st H is_proper_subformula_of F holds len H < len F proofend; theorem Th63: :: ZF_LANG:63 for H, F being ZF-formula st H is_proper_subformula_of F holds ex G being ZF-formula st G is_immediate_constituent_of F proofend; theorem Th64: :: ZF_LANG:64 for F, G, H being ZF-formula st F is_proper_subformula_of G & G is_proper_subformula_of H holds F is_proper_subformula_of H proofend; theorem Th65: :: ZF_LANG:65 for F, G, H being ZF-formula st F is_subformula_of G & G is_subformula_of H holds F is_subformula_of H proofend; theorem :: ZF_LANG:66 for G, H being ZF-formula st G is_subformula_of H & H is_subformula_of G holds G = H proofend; theorem Th67: :: ZF_LANG:67 for x, y being Variable for F being ZF-formula holds not F is_proper_subformula_of x '=' y proofend; theorem Th68: :: ZF_LANG:68 for x, y being Variable for F being ZF-formula holds not F is_proper_subformula_of x 'in' y proofend; theorem Th69: :: ZF_LANG:69 for F, H being ZF-formula st F is_proper_subformula_of 'not' H holds F is_subformula_of H proofend; theorem Th70: :: ZF_LANG:70 for F, G, H being ZF-formula holds ( not F is_proper_subformula_of G '&' H or F is_subformula_of G or F is_subformula_of H ) proofend; theorem Th71: :: ZF_LANG:71 for x being Variable for F, H being ZF-formula st F is_proper_subformula_of All (x,H) holds F is_subformula_of H proofend; theorem :: ZF_LANG:72 for H, F being ZF-formula st H is atomic holds not F is_proper_subformula_of H proofend; theorem :: ZF_LANG:73 for H being ZF-formula st H is negative holds the_argument_of H is_proper_subformula_of H proofend; theorem :: ZF_LANG:74 for H being ZF-formula st H is conjunctive holds ( the_left_argument_of H is_proper_subformula_of H & the_right_argument_of H is_proper_subformula_of H ) proofend; theorem :: ZF_LANG:75 for H being ZF-formula st H is universal holds the_scope_of H is_proper_subformula_of H proofend; theorem Th76: :: ZF_LANG:76 for x, y being Variable for H being ZF-formula holds ( H is_subformula_of x '=' y iff H = x '=' y ) proofend; theorem Th77: :: ZF_LANG:77 for x, y being Variable for H being ZF-formula holds ( H is_subformula_of x 'in' y iff H = x 'in' y ) proofend; :: :: The Set of Subformulae of ZF-formulae :: definition let H be ZF-formula; func Subformulae H -> set means :Def42: :: ZF_LANG:def 42 for a being set holds ( a in it iff ex F being ZF-formula st ( F = a & F is_subformula_of H ) ); existence ex b1 being set st for a being set holds ( a in b1 iff ex F being ZF-formula st ( F = a & F is_subformula_of H ) ) proofend; uniqueness for b1, b2 being set st ( for a being set holds ( a in b1 iff ex F being ZF-formula st ( F = a & F is_subformula_of H ) ) ) & ( for a being set holds ( a in b2 iff ex F being ZF-formula st ( F = a & F is_subformula_of H ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def42 defines Subformulae ZF_LANG:def_42_:_ for H being ZF-formula for b2 being set holds ( b2 = Subformulae H iff for a being set holds ( a in b2 iff ex F being ZF-formula st ( F = a & F is_subformula_of H ) ) ); theorem Th78: :: ZF_LANG:78 for G, H being ZF-formula st G in Subformulae H holds G is_subformula_of H proofend; theorem :: ZF_LANG:79 for F, H being ZF-formula st F is_subformula_of H holds Subformulae F c= Subformulae H proofend; theorem Th80: :: ZF_LANG:80 for x, y being Variable holds Subformulae (x '=' y) = {(x '=' y)} proofend; theorem Th81: :: ZF_LANG:81 for x, y being Variable holds Subformulae (x 'in' y) = {(x 'in' y)} proofend; theorem Th82: :: ZF_LANG:82 for H being ZF-formula holds Subformulae ('not' H) = (Subformulae H) \/ {('not' H)} proofend; theorem Th83: :: ZF_LANG:83 for H, F being ZF-formula holds Subformulae (H '&' F) = ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} proofend; theorem Th84: :: ZF_LANG:84 for x being Variable for H being ZF-formula holds Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))} proofend; theorem :: ZF_LANG:85 for H being ZF-formula holds ( H is atomic iff Subformulae H = {H} ) proofend; theorem :: ZF_LANG:86 for H being ZF-formula st H is negative holds Subformulae H = (Subformulae (the_argument_of H)) \/ {H} proofend; theorem :: ZF_LANG:87 for H being ZF-formula st H is conjunctive holds Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H} proofend; theorem :: ZF_LANG:88 for H being ZF-formula st H is universal holds Subformulae H = (Subformulae (the_scope_of H)) \/ {H} proofend; theorem :: ZF_LANG:89 for H, G, F being ZF-formula st ( H is_immediate_constituent_of G or H is_proper_subformula_of G or H is_subformula_of G ) & G in Subformulae F holds H in Subformulae F proofend; scheme :: ZF_LANG:sch 1 ZFInd{ P1[ ZF-formula] } : for H being ZF-formula holds P1[H] provided A1: for H being ZF-formula st H is atomic holds P1[H] and A2: for H being ZF-formula st H is negative & P1[ the_argument_of H] holds P1[H] and A3: for H being ZF-formula st H is conjunctive & P1[ the_left_argument_of H] & P1[ the_right_argument_of H] holds P1[H] and A4: for H being ZF-formula st H is universal & P1[ the_scope_of H] holds P1[H] proofend; scheme :: ZF_LANG:sch 2 ZFCompInd{ P1[ ZF-formula] } : for H being ZF-formula holds P1[H] provided A1: for H being ZF-formula st ( for F being ZF-formula st F is_proper_subformula_of H holds P1[F] ) holds P1[H] proofend;