:: Properties of ZF Models :: by Grzegorz Bancerek :: :: Received July 5, 1989 :: Copyright (c) 1990-2012 Association of Mizar Users begin set x0 = x. 0; set x1 = x. 1; set x2 = x. 2; set x3 = x. 3; set x4 = x. 4; theorem :: ZFMODEL1:1 for E being non empty set st E is epsilon-transitive holds E |= the_axiom_of_extensionality proofend; theorem Th2: :: ZFMODEL1:2 for E being non empty set st E is epsilon-transitive holds ( E |= the_axiom_of_pairs iff for u, v being Element of E holds {u,v} in E ) proofend; theorem :: ZFMODEL1:3 for E being non empty set st E is epsilon-transitive holds ( E |= the_axiom_of_pairs iff for X, Y being set st X in E & Y in E holds {X,Y} in E ) proofend; theorem Th4: :: ZFMODEL1:4 for E being non empty set st E is epsilon-transitive holds ( E |= the_axiom_of_unions iff for u being Element of E holds union u in E ) proofend; theorem :: ZFMODEL1:5 for E being non empty set st E is epsilon-transitive holds ( E |= the_axiom_of_unions iff for X being set st X in E holds union X in E ) proofend; theorem Th6: :: ZFMODEL1:6 for E being non empty set st E is epsilon-transitive holds ( E |= the_axiom_of_infinity iff ex u being Element of E st ( u <> {} & ( for v being Element of E st v in u holds ex w being Element of E st ( v c< w & w in u ) ) ) ) proofend; theorem :: ZFMODEL1:7 for E being non empty set st E is epsilon-transitive holds ( E |= the_axiom_of_infinity iff ex X being set st ( X in E & X <> {} & ( for Y being set st Y in X holds ex Z being set st ( Y c< Z & Z in X ) ) ) ) proofend; theorem Th8: :: ZFMODEL1:8 for E being non empty set st E is epsilon-transitive holds ( E |= the_axiom_of_power_sets iff for u being Element of E holds E /\ (bool u) in E ) proofend; theorem :: ZFMODEL1:9 for E being non empty set st E is epsilon-transitive holds ( E |= the_axiom_of_power_sets iff for X being set st X in E holds E /\ (bool X) in E ) proofend; defpred S1[ Nat] means for x being Variable for E being non empty set for H being ZF-formula for f being Function of VAR,E st len H = $1 & not x in Free H & E,f |= H holds E,f |= All (x,H); Lm1: for n being Nat st ( for k being Nat st k < n holds S1[k] ) holds S1[n] proofend; theorem Th10: :: ZFMODEL1:10 for x being Variable for H being ZF-formula for E being non empty set for f being Function of VAR,E st not x in Free H & E,f |= H holds E,f |= All (x,H) proofend; Lm2: for x being Variable for H being ZF-formula holds ( the_scope_of (All (x,H)) = H & bound_in (All (x,H)) = x ) proofend; theorem Th11: :: ZFMODEL1:11 for x, y being Variable for H being ZF-formula for E being non empty set for f being Function of VAR,E st {x,y} misses Free H & E,f |= H holds E,f |= All (x,y,H) proofend; theorem :: ZFMODEL1:12 for x, y, z being Variable for H being ZF-formula for E being non empty set for f being Function of VAR,E st {x,y,z} misses Free H & E,f |= H holds E,f |= All (x,y,z,H) proofend; definition let H be ZF-formula; let E be non empty set ; let val be Function of VAR,E; assume that A1: not x. 0 in Free H and A2: E,val |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ; func def_func' (H,val) -> Function of E,E means :Def1: :: ZFMODEL1:def 1 for g being Function of VAR,E st ( for y being Variable holds ( not g . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) holds ( E,g |= H iff it . (g . (x. 3)) = g . (x. 4) ); existence ex b1 being Function of E,E st for g being Function of VAR,E st ( for y being Variable holds ( not g . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) holds ( E,g |= H iff b1 . (g . (x. 3)) = g . (x. 4) ) proofend; uniqueness for b1, b2 being Function of E,E st ( for g being Function of VAR,E st ( for y being Variable holds ( not g . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) holds ( E,g |= H iff b1 . (g . (x. 3)) = g . (x. 4) ) ) & ( for g being Function of VAR,E st ( for y being Variable holds ( not g . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) holds ( E,g |= H iff b2 . (g . (x. 3)) = g . (x. 4) ) ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines def_func' ZFMODEL1:def_1_:_ for H being ZF-formula for E being non empty set for val being Function of VAR,E st not x. 0 in Free H & E,val |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds for b4 being Function of E,E holds ( b4 = def_func' (H,val) iff for g being Function of VAR,E st ( for y being Variable holds ( not g . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) holds ( E,g |= H iff b4 . (g . (x. 3)) = g . (x. 4) ) ); theorem Th13: :: ZFMODEL1:13 for E being non empty set for H being ZF-formula for f, g being Function of VAR,E st ( for x being Variable st f . x <> g . x holds not x in Free H ) & E,f |= H holds E,g |= H proofend; definition let H be ZF-formula; let E be non empty set ; assume that A1: Free H c= {(x. 3),(x. 4)} and A2: E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ; func def_func (H,E) -> Function of E,E means :Def2: :: ZFMODEL1:def 2 for g being Function of VAR,E holds ( E,g |= H iff it . (g . (x. 3)) = g . (x. 4) ); existence ex b1 being Function of E,E st for g being Function of VAR,E holds ( E,g |= H iff b1 . (g . (x. 3)) = g . (x. 4) ) proofend; uniqueness for b1, b2 being Function of E,E st ( for g being Function of VAR,E holds ( E,g |= H iff b1 . (g . (x. 3)) = g . (x. 4) ) ) & ( for g being Function of VAR,E holds ( E,g |= H iff b2 . (g . (x. 3)) = g . (x. 4) ) ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines def_func ZFMODEL1:def_2_:_ for H being ZF-formula for E being non empty set st Free H c= {(x. 3),(x. 4)} & E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds for b3 being Function of E,E holds ( b3 = def_func (H,E) iff for g being Function of VAR,E holds ( E,g |= H iff b3 . (g . (x. 3)) = g . (x. 4) ) ); definition let F be Function; let E be non empty set ; predF is_definable_in E means :: ZFMODEL1:def 3 ex H being ZF-formula st ( Free H c= {(x. 3),(x. 4)} & E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & F = def_func (H,E) ); predF is_parametrically_definable_in E means :Def4: :: ZFMODEL1:def 4 ex H being ZF-formula ex f being Function of VAR,E st ( {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & F = def_func' (H,f) ); end; :: deftheorem defines is_definable_in ZFMODEL1:def_3_:_ for F being Function for E being non empty set holds ( F is_definable_in E iff ex H being ZF-formula st ( Free H c= {(x. 3),(x. 4)} & E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & F = def_func (H,E) ) ); :: deftheorem Def4 defines is_parametrically_definable_in ZFMODEL1:def_4_:_ for F being Function for E being non empty set holds ( F is_parametrically_definable_in E iff ex H being ZF-formula ex f being Function of VAR,E st ( {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & F = def_func' (H,f) ) ); theorem :: ZFMODEL1:14 for E being non empty set for F being Function st F is_definable_in E holds F is_parametrically_definable_in E proofend; theorem Th15: :: ZFMODEL1:15 for E being non empty set st E is epsilon-transitive holds ( ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds E |= the_axiom_of_substitution_for H ) iff for H being ZF-formula for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds for u being Element of E holds (def_func' (H,f)) .: u in E ) proofend; theorem :: ZFMODEL1:16 for E being non empty set st E is epsilon-transitive holds ( ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds E |= the_axiom_of_substitution_for H ) iff for F being Function st F is_parametrically_definable_in E holds for X being set st X in E holds F .: X in E ) proofend; Lm3: for E being non empty set st E is epsilon-transitive holds for u, v being Element of E st ( for w being Element of E holds ( w in u iff w in v ) ) holds u = v proofend; theorem :: ZFMODEL1:17 for E being non empty set st E is being_a_model_of_ZF holds ( E is epsilon-transitive & ( for u, v being Element of E st ( for w being Element of E holds ( w in u iff w in v ) ) holds u = v ) & ( for u, v being Element of E holds {u,v} in E ) & ( for u being Element of E holds union u in E ) & ex u being Element of E st ( u <> {} & ( for v being Element of E st v in u holds ex w being Element of E st ( v c< w & w in u ) ) ) & ( for u being Element of E holds E /\ (bool u) in E ) & ( for H being ZF-formula for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds for u being Element of E holds (def_func' (H,f)) .: u in E ) ) proofend; theorem :: ZFMODEL1:18 for E being non empty set st E is epsilon-transitive & ( for u, v being Element of E holds {u,v} in E ) & ( for u being Element of E holds union u in E ) & ex u being Element of E st ( u <> {} & ( for v being Element of E st v in u holds ex w being Element of E st ( v c< w & w in u ) ) ) & ( for u being Element of E holds E /\ (bool u) in E ) & ( for H being ZF-formula for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds for u being Element of E holds (def_func' (H,f)) .: u in E ) holds E is being_a_model_of_ZF proofend;