:: ZF_REFLE semantic presentation

theorem Th1: :: ZF_REFLE:1
canceled;

theorem Th2: :: ZF_REFLE:2
for b1 being Universe holds b1 |= the_axiom_of_pairs
proof end;

theorem Th3: :: ZF_REFLE:3
for b1 being Universe holds b1 |= the_axiom_of_unions
proof end;

theorem Th4: :: ZF_REFLE:4
for b1 being Universe st omega in b1 holds
b1 |= the_axiom_of_infinity
proof end;

theorem Th5: :: ZF_REFLE:5
for b1 being Universe holds b1 |= the_axiom_of_power_sets
proof end;

theorem Th6: :: ZF_REFLE:6
for b1 being Universe
for b2 being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free b2 holds
b1 |= the_axiom_of_substitution_for b2
proof end;

theorem Th7: :: ZF_REFLE:7
for b1 being Universe st omega in b1 holds
b1 is_a_model_of_ZF
proof end;

definition
let c1, c2 be Ordinal;
redefine pred c1 c= c2 means :: ZF_REFLE:def 1
for b1 being Ordinal st b1 in a1 holds
b1 in a2;
compatibility
( c1 c= c2 iff for b1 being Ordinal st b1 in c1 holds
b1 in c2 )
proof end;
end;

:: deftheorem Def1 defines c= ZF_REFLE:def 1 :
for b1, b2 being Ordinal holds
( b1 c= b2 iff for b3 being Ordinal st b3 in b1 holds
b3 in b2 );

scheme :: ZF_REFLE:sch 1
s1{ F1() -> non empty set , P1[ set , set ] } :
ex b1 being Function st
( dom b1 = F1() & ( for b2 being Element of F1() ex b3 being Ordinal st
( b3 = b1 . b2 & P1[b2,b3] & ( for b4 being Ordinal st P1[b2,b4] holds
b3 c= b4 ) ) ) )
provided
E6: for b1 being Element of F1() ex b2 being Ordinal st P1[b1,b2]
proof end;

scheme :: ZF_REFLE:sch 2
s2{ F1() -> Universe, F2() -> non empty set , P1[ set , set ] } :
ex b1 being Function st
( dom b1 = F2() & ( for b2 being Element of F2() ex b3 being Ordinal of F1() st
( b3 = b1 . b2 & P1[b2,b3] & ( for b4 being Ordinal of F1() st P1[b2,b4] holds
b3 c= b4 ) ) ) )
provided
E6: for b1 being Element of F2() ex b2 being Ordinal of F1() st P1[b1,b2]
proof end;

theorem Th8: :: ZF_REFLE:8
for b1 being Universe
for b2 being set holds
( b2 is Ordinal of b1 iff b2 in On b1 )
proof end;

scheme :: ZF_REFLE:sch 3
s3{ F1() -> Universe, P1[ set , set ] } :
ex b1 being Ordinal-Sequence of F1() st
for b2 being Ordinal of F1() holds P1[b2,b1 . b2]
provided
E7: for b1, b2, b3 being Ordinal of F1() st P1[b1,b2] & P1[b1,b3] holds
b2 = b3 and
E8: for b1 being Ordinal of F1() ex b2 being Ordinal of F1() st P1[b1,b2]
proof end;

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

scheme :: ZF_REFLE:sch 5
s5{ F1() -> Universe, P1[ Ordinal] } :
for b1 being Ordinal of F1() holds P1[b1]
provided
E7: P1[ 0-element_of F1()] and
E8: for b1 being Ordinal of F1() st P1[b1] holds
P1[ succ b1] and
E9: for b1 being Ordinal of F1() st b1 <> 0-element_of F1() & b1 is_limit_ordinal & ( for b2 being Ordinal of F1() st b2 in b1 holds
P1[b2] ) holds
P1[b1]
proof end;

definition
let c1 be Function;
let c2 be Universe;
let c3 be Ordinal of c2;
func union c1,c3 -> set equals :: ZF_REFLE:def 2
 Union (a2 | (a1 | (Rank a3)));
correctness
coherence
Union (c2 | (c1 | (Rank c3))) is set ;
;
end;

:: deftheorem Def2 defines union ZF_REFLE:def 2 :
for b1 being Function
for b2 being Universe
for b3 being Ordinal of b2 holds union b1,b3 = Union (b2 | (b1 | (Rank b3)));

theorem Th9: :: ZF_REFLE:9
canceled;

theorem Th10: :: ZF_REFLE:10
for b1 being T-Sequence
for b2 being Ordinal holds b1 | (Rank b2) is T-Sequence
proof end;

theorem Th11: :: ZF_REFLE:11
for b1 being Ordinal-Sequence
for b2 being Ordinal holds b1 | (Rank b2) is Ordinal-Sequence
proof end;

theorem Th12: :: ZF_REFLE:12
for b1 being Ordinal-Sequence holds Union b1 is Ordinal
proof end;

theorem Th13: :: ZF_REFLE:13
for b1 being set
for b2 being Ordinal-Sequence holds Union (b1 | b2) is Ordinal
proof end;

theorem Th14: :: ZF_REFLE:14
for b1 being Ordinal holds On (Rank b1) = b1
proof end;

theorem Th15: :: ZF_REFLE:15
for b1 being Ordinal
for b2 being Ordinal-Sequence holds b2 | (Rank b1) = b2 | b1
proof end;

definition
let c1 be Ordinal-Sequence;
let c2 be Universe;
let c3 be Ordinal of c2;
redefine func union as union c1,c3 -> Ordinal of a2;
coherence
union c1,c3 is Ordinal of c2
proof end;
end;

theorem Th16: :: ZF_REFLE:16
canceled;

theorem Th17: :: ZF_REFLE:17
for b1 being Universe
for b2 being Ordinal of b1
for b3 being Ordinal-Sequence of b1 holds
( union b3,b2 = Union (b3 | b2) & union (b3 | b2),b2 = Union (b3 | b2) )
proof end;

definition
let c1 be Universe;
let c2, c3 be Ordinal of c1;
redefine func \/ as c2 \/ c3 -> Ordinal of a1;
coherence
c2 \/ c3 is Ordinal of c1
proof end;
end;

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

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

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

:: deftheorem Def3 ZF_REFLE:def 3 :
canceled;

:: deftheorem Def4 ZF_REFLE:def 4 :
canceled;

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

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

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

Lemma14: for b1, b2 being set st b1 <> {} & b1 c= b2 holds
b2 <> {}
proof end;

definition
let c1 be Universe;
let c2 be DOMAIN-Sequence of c1;
redefine func Union as Union c2 -> Subclass of a1;
coherence
Union c2 is Subclass of c1
proof end;
let c3 be Ordinal of c1;
redefine func . as c2 . c3 -> non empty Element of a1;
coherence
c2 . c3 is non empty Element of c1
proof end;
end;

theorem Th18: :: ZF_REFLE:18
canceled;

theorem Th19: :: ZF_REFLE:19
canceled;

theorem Th20: :: ZF_REFLE:20
canceled;

theorem Th21: :: ZF_REFLE:21
canceled;

theorem Th22: :: ZF_REFLE:22
canceled;

theorem Th23: :: ZF_REFLE:23
for b1 being Universe
for b2 being Ordinal of b1
for b3 being DOMAIN-Sequence of b1 holds b2 in dom b3
proof end;

theorem Th24: :: ZF_REFLE:24
for b1 being Universe
for b2 being Ordinal of b1
for b3 being DOMAIN-Sequence of b1 holds b3 . b2 c= Union b3
proof end;

theorem Th25: :: ZF_REFLE:25
NAT , VAR are_equipotent
proof end;

theorem Th26: :: ZF_REFLE:26
canceled;

theorem Th27: :: ZF_REFLE:27
for b1 being set holds sup b1 c= succ (union (On b1))
proof end;

theorem Th28: :: ZF_REFLE:28
for b1 being Universe
for b2 being set st b2 in b1 holds
sup b2 in b1
proof end;

theorem Th29: :: ZF_REFLE:29
for b1 being Universe
for b2 being DOMAIN-Sequence of b1 st omega in b1 & ( for b3, b4 being Ordinal of b1 st b3 in b4 holds
b2 . b3 c= b2 . b4 ) & ( for b3 being Ordinal of b1 st b3 <> {} & b3 is_limit_ordinal holds
b2 . b3 = Union (b2 | b3) ) holds
for b3 being ZF-formula ex b4 being Ordinal-Sequence of b1 st
( b4 is increasing & b4 is continuous & ( for b5 being Ordinal of b1 st b4 . b5 = b5 & {} <> b5 holds
for b6 being Function of VAR ,b2 . b5 holds
( Union b2,(Union b2) ! b6 |= b3 iff b2 . b5,b6 |= b3 ) ) )
proof end;