begin
Lm1:
{} in omega
by ORDINAL1:def 12;
Lm2:
omega is limit_ordinal
by ORDINAL1:def 12;
:: deftheorem Def1 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 );
:: 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 ) );
:: 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 ) ) ) );
defpred S1[ set ] means ( $1 = the_axiom_of_extensionality or $1 = the_axiom_of_pairs or $1 = the_axiom_of_unions or $1 = the_axiom_of_infinity or $1 = the_axiom_of_power_sets or ex H being ZF-formula st
( {(x. 0),(x. 1),(x. 2)} misses Free H & $1 = the_axiom_of_substitution_for H ) );
:: deftheorem Def4 defines ZF-axioms ZFREFLE1:def 4 :
for b1 being set holds
( b1 = ZF-axioms iff for e being set holds
( e in b1 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 ) ) ) ) );
theorem
theorem
theorem
theorem Th4:
theorem Th5:
theorem Th6:
theorem
theorem Th8:
theorem Th9:
theorem Th10:
theorem
canceled;
theorem Th12:
theorem
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem
canceled;
theorem
theorem
theorem
theorem Th22:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem
theorem
theorem Th40:
theorem Th41:
theorem
theorem