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

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

theorem Th2: :: ZF_REFLE:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Universe holds W |= the_axiom_of_pairs
proof end;

theorem Th3: :: ZF_REFLE:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Universe holds W |= the_axiom_of_unions
proof end;

theorem Th4: :: ZF_REFLE:4  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
W |= the_axiom_of_infinity
proof end;

theorem Th5: :: ZF_REFLE:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Universe holds W |= the_axiom_of_power_sets
proof end;

theorem Th6: :: ZF_REFLE:6  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 H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
W |= the_axiom_of_substitution_for H
proof end;

theorem :: ZF_REFLE:7  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
W is_a_model_of_ZF
proof end;

definition
let A, B be Ordinal;
redefine pred A c= B means :: ZF_REFLE:def 1
for C being Ordinal st C in A holds
C in B;
compatibility
( A c= B iff for C being Ordinal st C in A holds
C in B )
proof end;
end;

:: deftheorem defines c= ZF_REFLE:def 1 :
for A, B being Ordinal holds
( A c= B iff for C being Ordinal st C in A holds
C in B );

scheme :: ZF_REFLE:sch 1
ALFA{ F1() -> non empty set , P1[ set , set ] } :
ex F being Function st
( dom F = F1() & ( for d being Element of F1() ex A being Ordinal st
( A = F . d & P1[d,A] & ( for B being Ordinal st P1[d,B] holds
A c= B ) ) ) )
provided
A1: for d being Element of F1() ex A being Ordinal st P1[d,A]
proof end;

scheme :: ZF_REFLE:sch 2
ALFA'Universe{ F1() -> Universe, F2() -> non empty set , P1[ set , set ] } :
ex F being Function st
( dom F = F2() & ( for d being Element of F2() ex a being Ordinal of F1() st
( a = F . d & P1[d,a] & ( for b being Ordinal of F1() st P1[d,b] holds
a c= b ) ) ) )
provided
A1: for d being Element of F2() ex a being Ordinal of F1() st P1[d,a]
proof end;

theorem Th8: :: ZF_REFLE:8  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 x being set holds
( x is Ordinal of W iff x in On W )
proof end;

scheme :: ZF_REFLE:sch 3
OrdSeqOfUnivEx{ F1() -> Universe, P1[ set , set ] } :
ex phi being Ordinal-Sequence of F1() st
for a being Ordinal of F1() holds P1[a,phi . a]
provided
A1: for a, b1, b2 being Ordinal of F1() st P1[a,b1] & P1[a,b2] holds
b1 = b2 and
A2: for a being Ordinal of F1() ex b being Ordinal of F1() st P1[a,b]
proof end;

scheme :: ZF_REFLE:sch 4
UOSExist{ F1() -> Universe, F2() -> Ordinal of F1(), F3( Ordinal, Ordinal) -> Ordinal of F1(), F4( Ordinal, T-Sequence) -> Ordinal of F1() } :
ex phi being Ordinal-Sequence of F1() st
( phi . (0-element_of F1()) = F2() & ( for a being Ordinal of F1() holds phi . (succ a) = F3(a,(phi . a)) ) & ( for a being Ordinal of F1() st a <> 0-element_of F1() & a is_limit_ordinal holds
phi . a = F4(a,(phi | a)) ) )
proof end;

scheme :: ZF_REFLE:sch 5
UniverseInd{ F1() -> Universe, P1[ Ordinal] } :
for a being Ordinal of F1() holds P1[a]
provided
A1: P1[ 0-element_of F1()] and
A2: for a being Ordinal of F1() st P1[a] holds
P1[ succ a] and
A3: for a being Ordinal of F1() st a <> 0-element_of F1() & a is_limit_ordinal & ( for b being Ordinal of F1() st b in a holds
P1[b] ) holds
P1[a]
proof end;

definition
let f be Function;
let W be Universe;
let a be Ordinal of W;
func union f,a -> set equals :: ZF_REFLE:def 2
Union (W | (f | (Rank a)));
correctness
coherence
Union (W | (f | (Rank a))) is set
;
;
end;

:: deftheorem defines union ZF_REFLE:def 2 :
for f being Function
for W being Universe
for a being Ordinal of W holds union f,a = Union (W | (f | (Rank a)));

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

theorem Th10: :: ZF_REFLE:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being T-Sequence
for A being Ordinal holds L | (Rank A) is T-Sequence
proof end;

theorem Th11: :: ZF_REFLE:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Ordinal-Sequence
for A being Ordinal holds L | (Rank A) is Ordinal-Sequence
proof end;

theorem :: ZF_REFLE:12  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 Union psi is Ordinal
proof end;

theorem Th13: :: ZF_REFLE:13  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 psi being Ordinal-Sequence holds Union (X | psi) is Ordinal
proof end;

theorem Th14: :: ZF_REFLE:14  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 On (Rank A) = A
proof end;

theorem Th15: :: ZF_REFLE:15  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 holds psi | (Rank A) = psi | A
proof end;

definition
let phi be Ordinal-Sequence;
let W be Universe;
let a be Ordinal of W;
:: original: union
redefine func union phi,a -> Ordinal of W;
coherence
union phi,a is Ordinal of W
proof end;
end;

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

theorem Th17: :: ZF_REFLE:17  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 holds
( union phi,a = Union (phi | a) & union (phi | a),a = Union (phi | a) )
proof end;

definition
let W be Universe;
let a, b be Ordinal of W;
:: original: \/
redefine func a \/ b -> Ordinal of W;
coherence
a \/ b is Ordinal of W
proof end;
end;

registration
let W be Universe;
cluster non empty Element of W;
existence
not for b1 being Element of W holds b1 is empty
proof end;
end;

definition
let W be Universe;
mode Subclass of W is non empty Subset of W;
end;

definition
let W be Universe;
let IT be T-Sequence of W;
canceled;
canceled;
attr IT is DOMAIN-yielding means :Def5: :: ZF_REFLE:def 5
dom IT = On W;
end;

:: deftheorem ZF_REFLE:def 3 :
canceled;

:: deftheorem ZF_REFLE:def 4 :
canceled;

:: deftheorem Def5 defines DOMAIN-yielding ZF_REFLE:def 5 :
for W being Universe
for IT being T-Sequence of W holds
( IT is DOMAIN-yielding iff dom IT = On W );

registration
let W be Universe;
cluster non-empty DOMAIN-yielding T-Sequence of W;
existence
ex b1 being T-Sequence of W st
( b1 is DOMAIN-yielding & b1 is non-empty )
proof end;
end;

definition
let W be Universe;
mode DOMAIN-Sequence of W is non-empty DOMAIN-yielding T-Sequence of W;
end;

Lm1: for X, Y being set st X <> {} & X c= Y holds
Y <> {}
proof end;

definition
let W be Universe;
let L be DOMAIN-Sequence of W;
:: original: Union
redefine func Union L -> Subclass of W;
coherence
Union L is Subclass of W
proof end;
let a be Ordinal of W;
:: original: .
redefine func L . a -> non empty Element of W;
coherence
L . a is non empty Element of W
proof end;
end;

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

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

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

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

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

theorem Th23: :: ZF_REFLE:23  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 L being DOMAIN-Sequence of W holds a in dom L
proof end;

theorem Th24: :: ZF_REFLE:24  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 L being DOMAIN-Sequence of W holds L . a c= Union L
proof end;

theorem Th25: :: ZF_REFLE:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
NAT , VAR are_equipotent
proof end;

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

theorem Th27: :: ZF_REFLE:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set holds sup X c= succ (union (On X))
proof end;

theorem Th28: :: ZF_REFLE:28  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 X being set st X in W holds
sup X in W
proof end;

theorem :: ZF_REFLE: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 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
for H being ZF-formula 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
for f being Function of VAR ,L . a holds
( Union L,(Union L) ! f |= H iff L . a,f |= H ) ) )
proof end;