:: ZFREFLE1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let M be non empty set ;
let F be Subset of WFF ;
pred M |= F means :Def1: :: ZFREFLE1:def 1
for H being ZF-formula st H in F holds
M |= H;
end;

:: 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 );

definition
let M1, M2 be non empty set ;
pred M1 <==> M2 means :: ZFREFLE1:def 2
for H being ZF-formula st Free H = {} holds
( M1 |= H iff M2 |= H );
reflexivity
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
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 2;
end;

:: 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 ) );

definition
func ZF-axioms -> set means :Def4: :: ZFREFLE1:def 4
for e being set 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
ex b1 being set st
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 ) ) ) )
proof end;
uniqueness
for b1, b2 being set st ( 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 ) ) ) ) ) & ( for e being set holds
( e in b2 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
b1 = b2
proof end;
end;

:: 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 ) ) ) ) );

definition
:: original: ZF-axioms
redefine func ZF-axioms -> Subset of WFF ;
coherence
ZF-axioms is Subset of WFF
proof end;
end;

theorem :: ZFREFLE1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty set holds M |= {} WFF
proof end;

theorem :: ZFREFLE1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty set
for F1, F2 being Subset of WFF st F1 c= F2 & M |= F2 holds
M |= F1
proof end;

theorem :: ZFREFLE1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty set
for F1, F2 being Subset of WFF st M |= F1 & M |= F2 holds
M |= F1 \/ F2
proof end;

theorem Th4: :: ZFREFLE1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty set st M is_a_model_of_ZF holds
M |= ZF-axioms
proof end;

theorem Th5: :: ZFREFLE1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty set st M |= ZF-axioms & M is epsilon-transitive holds
M is_a_model_of_ZF
proof end;

theorem Th6: :: ZFREFLE1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) ) )
proof end;

theorem :: ZFREFLE1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M1, M2 being non empty set holds
( M1 <==> M2 iff for H being ZF-formula holds
( M1 |= H iff M2 |= H ) )
proof end;

theorem Th8: :: ZFREFLE1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M1, M2 being non empty set holds
( M1 <==> M2 iff for F being Subset of WFF holds
( M1 |= F iff M2 |= F ) )
proof end;

theorem Th9: :: ZFREFLE1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M1, M2 being non empty set st M1 is_elementary_subsystem_of M2 holds
M1 <==> M2
proof end;

theorem Th10: :: ZFREFLE1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M1, M2 being non empty set st M1 is_a_model_of_ZF & M1 <==> M2 & M2 is epsilon-transitive holds
M2 is_a_model_of_ZF
proof end;

scheme :: ZFREFLE1:sch 1
NonUniqFuncEx{ F1() -> set , P1[ set , set ] } :
ex f being Function st
( dom f = F1() & ( for e being set st e in F1() holds
P1[e,f . e] ) )
provided
A1: for e being set st e in F1() holds
ex u being set st P1[e,u]
proof end;

theorem :: ZFREFLE1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th12: :: ZFREFLE1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function
for W being Universe st dom f in W & rng f c= W holds
rng f in W
proof end;

theorem :: ZFREFLE1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem Th14: :: ZFREFLE1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Universe
for D being non empty set
for Phi being Function of D, Funcs (On W),(On W) st Card D <` 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 Th15: :: ZFREFLE1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Ordinal
for phi being Ordinal-Sequence st phi is increasing holds
C +^ phi is increasing
proof end;

theorem Th16: :: ZFREFLE1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C, A being Ordinal
for xi being Ordinal-Sequence holds (C +^ xi) | A = C +^ (xi | A)
proof end;

theorem Th17: :: ZFREFLE1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Ordinal
for phi being Ordinal-Sequence st phi is increasing & phi is continuous holds
C +^ phi is continuous
proof end;

definition
let A, B be Ordinal;
pred A is_cofinal_with B means :: ZFREFLE1:def 5
ex xi being Ordinal-Sequence st
( dom xi = B & rng xi c= A & xi is increasing & A = sup xi );
reflexivity
for A being Ordinal ex xi being Ordinal-Sequence st
( dom xi = A & rng xi c= A & xi is increasing & A = sup xi )
proof end;
end;

:: deftheorem defines is_cofinal_with ZFREFLE1:def 5 :
for A, B being Ordinal holds
( A is_cofinal_with B iff ex xi being Ordinal-Sequence st
( dom xi = B & rng xi c= A & xi is increasing & A = sup xi ) );

theorem :: ZFREFLE1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th19: :: ZFREFLE1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for e being set
for psi being Ordinal-Sequence st e in rng psi holds
e is Ordinal
proof end;

theorem Th20: :: ZFREFLE1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for psi being Ordinal-Sequence holds rng psi c= sup psi
proof end;

theorem :: ZFREFLE1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being Ordinal st A is_cofinal_with B & B is_cofinal_with C holds
A is_cofinal_with C
proof end;

theorem Th22: :: ZFREFLE1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being Ordinal st A is_cofinal_with B holds
B c= A
proof end;

theorem :: ZFREFLE1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being Ordinal st A is_cofinal_with B & B is_cofinal_with A holds
A = B
proof end;

theorem :: ZFREFLE1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: ZFREFLE1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal holds succ A is_cofinal_with one
proof end;

theorem :: ZFREFLE1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being Ordinal st A is_cofinal_with succ B holds
ex C being Ordinal st A = succ C
proof end;

theorem :: ZFREFLE1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being Ordinal st A is_cofinal_with B holds
( A is_limit_ordinal iff B is_limit_ordinal )
proof end;

theorem :: ZFREFLE1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Ordinal st A is_cofinal_with {} holds
A = {}
proof end;

theorem :: ZFREFLE1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Universe
for a being Ordinal of W holds not On W is_cofinal_with a
proof end;

theorem Th30: :: ZFREFLE1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th31: :: ZFREFLE1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th32: :: ZFREFLE1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem Th33: :: ZFREFLE1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Universe
for a being Ordinal of W holds Rank a in W
proof end;

theorem Th34: :: ZFREFLE1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Universe
for a being Ordinal of W st a <> {} holds
Rank a is non empty Element of W
proof end;

theorem Th35: :: ZFREFLE1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem Th36: :: ZFREFLE1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th37: :: ZFREFLE1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: ZFREFLE1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem :: ZFREFLE1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem Th40: :: ZFREFLE1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th41: :: ZFREFLE1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: ZFREFLE1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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_a_model_of_ZF )
proof end;

theorem :: ZFREFLE1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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_a_model_of_ZF )
proof end;