:: by Grzegorz Bancerek

::

:: Received August 13, 1990

:: Copyright (c) 1990-2019 Association of Mizar Users

Lm1: {} in omega

by ORDINAL1:def 11;

Lm2: omega is limit_ordinal

by ORDINAL1:def 11;

:: deftheorem defines |= ZFREFLE1:def 1 :

for M being non empty set

for F being Subset of WFF holds

( M |= F iff for H being ZF-formula st H in F holds

M |= H );

for M being non empty set

for F being Subset of WFF holds

( M |= F iff for H being ZF-formula st H in F holds

M |= H );

definition

let M1, M2 be non empty set ;

for M1 being non empty set

for H being ZF-formula st Free H = {} holds

( M1 |= H iff M1 |= H ) ;

symmetry

for M1, M2 being non empty set st ( for H being ZF-formula st Free H = {} holds

( M1 |= H iff M2 |= H ) ) holds

for H being ZF-formula st Free H = {} holds

( M2 |= H iff M1 |= H ) ;

for M1 being non empty set holds

( M1 c= M1 & ( for H being ZF-formula

for v being Function of VAR,M1 holds

( M1,v |= H iff M1,M1 ! v |= H ) ) ) by ZF_LANG1:def 1;

end;
pred M1 <==> M2 means :: ZFREFLE1:def 2

for H being ZF-formula st Free H = {} holds

( M1 |= H iff M2 |= H );

reflexivity for H being ZF-formula st Free H = {} holds

( M1 |= H iff M2 |= H );

for M1 being non empty set

for H being ZF-formula st Free H = {} holds

( M1 |= H iff M1 |= H ) ;

symmetry

for M1, M2 being non empty set st ( for H being ZF-formula st Free H = {} holds

( M1 |= H iff M2 |= H ) ) holds

for H being ZF-formula st Free H = {} holds

( M2 |= H iff M1 |= H ) ;

pred M1 is_elementary_subsystem_of M2 means :: ZFREFLE1:def 3

( M1 c= M2 & ( for H being ZF-formula

for v being Function of VAR,M1 holds

( M1,v |= H iff M2,M2 ! v |= H ) ) );

reflexivity ( M1 c= M2 & ( for H being ZF-formula

for v being Function of VAR,M1 holds

( M1,v |= H iff M2,M2 ! v |= H ) ) );

for M1 being non empty set holds

( M1 c= M1 & ( for H being ZF-formula

for v being Function of VAR,M1 holds

( M1,v |= H iff M1,M1 ! v |= H ) ) ) by ZF_LANG1:def 1;

:: deftheorem defines <==> ZFREFLE1:def 2 :

for M1, M2 being non empty set holds

( M1 <==> M2 iff for H being ZF-formula st Free H = {} holds

( M1 |= H iff M2 |= H ) );

for M1, M2 being non empty set holds

( M1 <==> M2 iff for H being ZF-formula st Free H = {} holds

( M1 |= H iff M2 |= H ) );

:: deftheorem defines is_elementary_subsystem_of ZFREFLE1:def 3 :

for M1, M2 being non empty set holds

( M1 is_elementary_subsystem_of M2 iff ( M1 c= M2 & ( for H being ZF-formula

for v being Function of VAR,M1 holds

( M1,v |= H iff M2,M2 ! v |= H ) ) ) );

for M1, M2 being non empty set holds

( M1 is_elementary_subsystem_of M2 iff ( M1 c= M2 & ( for H being ZF-formula

for v being Function of VAR,M1 holds

( M1,v |= H iff M2,M2 ! v |= H ) ) ) );

defpred S

( {(x. 0),(x. 1),(x. 2)} misses Free H & $1 = the_axiom_of_substitution_for H ) );

definition

ex b_{1} being set st

for e being object holds

( e in b_{1} iff ( e in WFF & ( e = the_axiom_of_extensionality or e = the_axiom_of_pairs or e = the_axiom_of_unions or e = the_axiom_of_infinity or e = the_axiom_of_power_sets or ex H being ZF-formula st

( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) )

for b_{1}, b_{2} being set st ( for e being object holds

( e in b_{1} iff ( e in WFF & ( e = the_axiom_of_extensionality or e = the_axiom_of_pairs or e = the_axiom_of_unions or e = the_axiom_of_infinity or e = the_axiom_of_power_sets or ex H being ZF-formula st

( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) ) ) & ( for e being object holds

( e in b_{2} iff ( e in WFF & ( e = the_axiom_of_extensionality or e = the_axiom_of_pairs or e = the_axiom_of_unions or e = the_axiom_of_infinity or e = the_axiom_of_power_sets or ex H being ZF-formula st

( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) ) ) holds

b_{1} = b_{2}
end;

func ZF-axioms -> set means :Def4: :: ZFREFLE1:def 4

for e being object holds

( e in it iff ( e in WFF & ( e = the_axiom_of_extensionality or e = the_axiom_of_pairs or e = the_axiom_of_unions or e = the_axiom_of_infinity or e = the_axiom_of_power_sets or ex H being ZF-formula st

( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) );

existence for e being object holds

( e in it iff ( e in WFF & ( e = the_axiom_of_extensionality or e = the_axiom_of_pairs or e = the_axiom_of_unions or e = the_axiom_of_infinity or e = the_axiom_of_power_sets or ex H being ZF-formula st

( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) );

ex b

for e being object holds

( e in b

( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) )

proof end;

uniqueness for b

( e in b

( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) ) ) & ( for e being object holds

( e in b

( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) ) ) holds

b

proof end;

:: deftheorem Def4 defines ZF-axioms ZFREFLE1:def 4 :

for b_{1} being set holds

( b_{1} = ZF-axioms iff for e being object holds

( e in b_{1} iff ( e in WFF & ( e = the_axiom_of_extensionality or e = the_axiom_of_pairs or e = the_axiom_of_unions or e = the_axiom_of_infinity or e = the_axiom_of_power_sets or ex H being ZF-formula st

( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) ) );

for b

( b

( e in b

( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) ) );

definition

:: original: ZF-axioms

redefine func ZF-axioms -> Subset of WFF;

coherence

ZF-axioms is Subset of WFF

end;
redefine func ZF-axioms -> Subset of WFF;

coherence

ZF-axioms is Subset of WFF

proof end;

theorem :: ZFREFLE1:2

theorem Th5: :: ZFREFLE1:5

for M being non empty set st M |= ZF-axioms & M is epsilon-transitive holds

M is being_a_model_of_ZF

M is being_a_model_of_ZF

proof end;

theorem Th6: :: ZFREFLE1:6

for H being ZF-formula ex S being ZF-formula st

( Free S = {} & ( for M being non empty set holds

( M |= S iff M |= H ) ) )

( Free S = {} & ( for M being non empty set holds

( M |= S iff M |= H ) ) )

proof end;

theorem :: ZFREFLE1:7

for M1, M2 being non empty set holds

( M1 <==> M2 iff for H being ZF-formula holds

( M1 |= H iff M2 |= H ) )

( M1 <==> M2 iff for H being ZF-formula holds

( M1 |= H iff M2 |= H ) )

proof end;

theorem Th8: :: ZFREFLE1:8

for M1, M2 being non empty set holds

( M1 <==> M2 iff for F being Subset of WFF holds

( M1 |= F iff M2 |= F ) )

( M1 <==> M2 iff for F being Subset of WFF holds

( M1 |= F iff M2 |= F ) )

proof end;

theorem Th10: :: ZFREFLE1:10

for M1, M2 being non empty set st M1 is being_a_model_of_ZF & M1 <==> M2 & M2 is epsilon-transitive holds

M2 is being_a_model_of_ZF

M2 is being_a_model_of_ZF

proof end;

theorem :: ZFREFLE1:12

for X, Y being set st ( X,Y are_equipotent or card X = card Y ) holds

( bool X, bool Y are_equipotent & card (bool X) = card (bool Y) )

( bool X, bool Y are_equipotent & card (bool X) = card (bool Y) )

proof end;

theorem Th13: :: ZFREFLE1:13

for W being Universe

for D being non empty set

for Phi being Function of D,(Funcs ((On W),(On W))) st card D in card W holds

ex phi being Ordinal-Sequence of W st

( phi is increasing & phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds

phi . a = sup (phi | a) ) )

for D being non empty set

for Phi being Function of D,(Funcs ((On W),(On W))) st card D in card W holds

ex phi being Ordinal-Sequence of W st

( phi is increasing & phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds

phi . a = sup (phi | a) ) )

proof end;

theorem Th14: :: ZFREFLE1:14

for C being Ordinal

for phi being Ordinal-Sequence st phi is increasing holds

C +^ phi is increasing

for phi being Ordinal-Sequence st phi is increasing holds

C +^ phi is increasing

proof end;

theorem Th16: :: ZFREFLE1:16

for C being Ordinal

for phi being Ordinal-Sequence st phi is increasing & phi is continuous holds

C +^ phi is continuous

for phi being Ordinal-Sequence st phi is increasing & phi is continuous holds

C +^ phi is continuous

proof end;

theorem :: ZFREFLE1:17

theorem :: ZFREFLE1:19

for A, B, C being Ordinal st A is_cofinal_with B & B is_cofinal_with C holds

A is_cofinal_with C by ORDINAL4:37;

A is_cofinal_with C by ORDINAL4:37;

theorem :: ZFREFLE1:21

theorem :: ZFREFLE1:22

for A being Ordinal

for psi being Ordinal-Sequence st dom psi <> {} & dom psi is limit_ordinal & psi is increasing & A is_limes_of psi holds

A is_cofinal_with dom psi

for psi being Ordinal-Sequence st dom psi <> {} & dom psi is limit_ordinal & psi is increasing & A is_limes_of psi holds

A is_cofinal_with dom psi

proof end;

theorem :: ZFREFLE1:25

for A, B being Ordinal st A is_cofinal_with B holds

( A is limit_ordinal iff B is limit_ordinal ) by ORDINAL4:38;

( A is limit_ordinal iff B is limit_ordinal ) by ORDINAL4:38;

theorem Th28: :: ZFREFLE1:28

for W being Universe

for a being Ordinal of W

for phi being Ordinal-Sequence of W st omega in W & phi is increasing & phi is continuous holds

ex b being Ordinal of W st

( a in b & phi . b = b )

for a being Ordinal of W

for phi being Ordinal-Sequence of W st omega in W & phi is increasing & phi is continuous holds

ex b being Ordinal of W st

( a in b & phi . b = b )

proof end;

theorem Th29: :: ZFREFLE1:29

for W being Universe

for b being Ordinal of W

for phi being Ordinal-Sequence of W st omega in W & phi is increasing & phi is continuous holds

ex a being Ordinal of W st

( b in a & phi . a = a & a is_cofinal_with omega )

for b being Ordinal of W

for phi being Ordinal-Sequence of W st omega in W & phi is increasing & phi is continuous holds

ex a being Ordinal of W st

( b in a & phi . a = a & a is_cofinal_with omega )

proof end;

theorem Th30: :: ZFREFLE1:30

for W being Universe

for L being DOMAIN-Sequence of W st omega in W & ( for a, b being Ordinal of W st a in b holds

L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds

L . a = Union (L | a) ) holds

ex phi being Ordinal-Sequence of W st

( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds

L . a is_elementary_subsystem_of Union L ) )

for L being DOMAIN-Sequence of W st omega in W & ( for a, b being Ordinal of W st a in b holds

L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds

L . a = Union (L | a) ) holds

ex phi being Ordinal-Sequence of W st

( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds

L . a is_elementary_subsystem_of Union L ) )

proof end;

theorem Th32: :: ZFREFLE1:32

for W being Universe

for a being Ordinal of W st a <> {} holds

Rank a is non empty Element of W by Th31, CLASSES1:36, ORDINAL3:8;

for a being Ordinal of W st a <> {} holds

Rank a is non empty Element of W by Th31, CLASSES1:36, ORDINAL3:8;

theorem Th33: :: ZFREFLE1:33

for W being Universe st omega in W holds

ex phi being Ordinal-Sequence of W st

( phi is increasing & phi is continuous & ( for a being Ordinal of W

for M being non empty set st phi . a = a & {} <> a & M = Rank a holds

M is_elementary_subsystem_of W ) )

ex phi being Ordinal-Sequence of W st

( phi is increasing & phi is continuous & ( for a being Ordinal of W

for M being non empty set st phi . a = a & {} <> a & M = Rank a holds

M is_elementary_subsystem_of W ) )

proof end;

theorem Th34: :: ZFREFLE1:34

for W being Universe

for a being Ordinal of W st omega in W holds

ex b being Ordinal of W ex M being non empty set st

( a in b & M = Rank b & M is_elementary_subsystem_of W )

for a being Ordinal of W st omega in W holds

ex b being Ordinal of W ex M being non empty set st

( a in b & M = Rank b & M is_elementary_subsystem_of W )

proof end;

theorem Th35: :: ZFREFLE1:35

for W being Universe st omega in W holds

ex a being Ordinal of W ex M being non empty set st

( a is_cofinal_with omega & M = Rank a & M is_elementary_subsystem_of W )

ex a being Ordinal of W ex M being non empty set st

( a is_cofinal_with omega & M = Rank a & M is_elementary_subsystem_of W )

proof end;

theorem :: ZFREFLE1:36

for W being Universe

for L being DOMAIN-Sequence of W st omega in W & ( for a, b being Ordinal of W st a in b holds

L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds

L . a = Union (L | a) ) holds

ex phi being Ordinal-Sequence of W st

( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds

L . a <==> Union L ) )

for L being DOMAIN-Sequence of W st omega in W & ( for a, b being Ordinal of W st a in b holds

L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds

L . a = Union (L | a) ) holds

ex phi being Ordinal-Sequence of W st

( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds

L . a <==> Union L ) )

proof end;

theorem :: ZFREFLE1:37

for W being Universe st omega in W holds

ex phi being Ordinal-Sequence of W st

( phi is increasing & phi is continuous & ( for a being Ordinal of W

for M being non empty set st phi . a = a & {} <> a & M = Rank a holds

M <==> W ) )

ex phi being Ordinal-Sequence of W st

( phi is increasing & phi is continuous & ( for a being Ordinal of W

for M being non empty set st phi . a = a & {} <> a & M = Rank a holds

M <==> W ) )

proof end;

theorem Th38: :: ZFREFLE1:38

for W being Universe

for a being Ordinal of W st omega in W holds

ex b being Ordinal of W ex M being non empty set st

( a in b & M = Rank b & M <==> W )

for a being Ordinal of W st omega in W holds

ex b being Ordinal of W ex M being non empty set st

( a in b & M = Rank b & M <==> W )

proof end;

theorem Th39: :: ZFREFLE1:39

for W being Universe st omega in W holds

ex a being Ordinal of W ex M being non empty set st

( a is_cofinal_with omega & M = Rank a & M <==> W )

ex a being Ordinal of W ex M being non empty set st

( a is_cofinal_with omega & M = Rank a & M <==> W )

proof end;

theorem :: ZFREFLE1:40

for W being Universe st omega in W holds

ex a being Ordinal of W ex M being non empty set st

( a is_cofinal_with omega & M = Rank a & M is being_a_model_of_ZF )

ex a being Ordinal of W ex M being non empty set st

( a is_cofinal_with omega & M = Rank a & M is being_a_model_of_ZF )

proof end;

theorem :: ZFREFLE1:41

for X being set

for W being Universe st omega in W & X in W holds

ex M being non empty set st

( X in M & M in W & M is being_a_model_of_ZF )

for W being Universe st omega in W & X in W holds

ex M being non empty set st

( X in M & M in W & M is being_a_model_of_ZF )

proof end;