:: ZF_REFLE semantic presentation

theorem :: ZF_REFLE:1

canceled;

theorem Th2: :: ZF_REFLE:2

for W being Universe holds W |= the_axiom_of_pairs

proof end;

theorem Th3: :: ZF_REFLE:3

for W being Universe holds W |= the_axiom_of_unions

proof end;

theorem Th4: :: ZF_REFLE:4

for W being Universe st omega in W holds
W |= the_axiom_of_infinity

proof end;

theorem Th5: :: ZF_REFLE:5

for W being Universe holds W |= the_axiom_of_power_sets

proof end;

theorem Th6: :: ZF_REFLE:6

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

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

proof end;

end;

:: deftheorem defines c= ZF_REFLE:def 1 :

scheme :: ZF_REFLE:sch 1
ALFA{ F₁() -> non empty set , P₁[ set , set ] } :

ex F being Function st
( dom F = F₁() & ( for d being Element of F₁() ex A being Ordinal st
( A = F . d & P₁[d,A] & ( for B being Ordinal st P₁[d,B] holds
A c= B ) ) ) )

provided

A1: for d being Element of F₁() ex A being Ordinal st P₁[d,A]

proof end;

scheme :: ZF_REFLE:sch 2
ALFA'Universe{ F₁() -> Universe, F₂() -> non empty set , P₁[ set , set ] } :

ex F being Function st
( dom F = F₂() & ( for d being Element of F₂() ex a being Ordinal of F₁() st
( a = F . d & P₁[d,a] & ( for b being Ordinal of F₁() st P₁[d,b] holds
a c= b ) ) ) )

provided

A1: for d being Element of F₂() ex a being Ordinal of F₁() st P₁[d,a]

proof end;

theorem Th8: :: ZF_REFLE:8

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{ F₁() -> Universe, P₁[ set , set ] } :

ex phi being Ordinal-Sequence of F₁() st
for a being Ordinal of F₁() holds P₁[a,phi . a]

provided

A1: for a, b1, b2 being Ordinal of F₁() st P₁[a,b1] & P₁[a,b2] holds
b1 = b2 and
A2: for a being Ordinal of F₁() ex b being Ordinal of F₁() st P₁[a,b]

proof end;

scheme :: ZF_REFLE:sch 4
UOSExist{ F₁() -> Universe, F₂() -> Ordinal of F₁(), F₃( Ordinal, Ordinal) -> Ordinal of F₁(), F₄( Ordinal, T-Sequence) -> Ordinal of F₁() } :

ex phi being Ordinal-Sequence of F₁() st
( phi . (0-element_of F₁()) = F₂() & ( for a being Ordinal of F₁() holds phi . (succ a) = F₃(a,(phi . a)) ) & ( for a being Ordinal of F₁() st a <> 0-element_of F₁() & a is_limit_ordinal holds
phi . a = F₄(a,(phi | a)) ) )

proof end;

scheme :: ZF_REFLE:sch 5
UniverseInd{ F₁() -> Universe, P₁[ Ordinal] } :

for a being Ordinal of F₁() holds P₁[a]

provided

A1: P₁[ 0-element_of F₁()] and
A2: for a being Ordinal of F₁() st P₁[a] holds
P₁[ succ a] and
A3: for a being Ordinal of F₁() st a <> 0-element_of F₁() & a is_limit_ordinal & ( for b being Ordinal of F₁() st b in a holds
P₁[b] ) holds
P₁[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 ;

end;

:: deftheorem defines union ZF_REFLE:def 2 :

theorem :: ZF_REFLE:9

canceled;

theorem Th10: :: ZF_REFLE:10

for L being T-Sequence
for A being Ordinal holds L | (Rank A) is T-Sequence

proof end;

theorem Th11: :: ZF_REFLE:11

for L being Ordinal-Sequence
for A being Ordinal holds L | (Rank A) is Ordinal-Sequence

proof end;

theorem :: ZF_REFLE:12

for psi being Ordinal-Sequence holds Union psi is Ordinal

proof end;

theorem Th13: :: ZF_REFLE:13

for X being set
for psi being Ordinal-Sequence holds Union (X | psi) is Ordinal

proof end;

theorem Th14: :: ZF_REFLE:14

for A being Ordinal holds On (Rank A) = A

proof end;

theorem Th15: :: ZF_REFLE:15

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

proof end;

end;

theorem :: ZF_REFLE:16

canceled;

theorem Th17: :: ZF_REFLE:17

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

proof end;

end;

registration

let W be Universe;
cluster non empty Element of W;
existence

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 :

:: deftheorem ZF_REFLE:def 4 :

:: deftheorem Def5 defines DOMAIN-yielding ZF_REFLE:def 5 :

registration

let W be Universe;
cluster non-empty DOMAIN-yielding T-Sequence of W;
existence

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

proof end;

let a be Ordinal of W;
:: original: .
redefine func L . a -> non empty Element of W;
coherence

proof end;

end;

theorem :: ZF_REFLE:18

canceled;

theorem :: ZF_REFLE:19

canceled;

theorem :: ZF_REFLE:20

canceled;

theorem :: ZF_REFLE:21

canceled;

theorem :: ZF_REFLE:22

canceled;

theorem Th23: :: ZF_REFLE:23

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

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

NAT , VAR are_equipotent

proof end;

theorem :: ZF_REFLE:26

canceled;

theorem Th27: :: ZF_REFLE:27

for X being set holds sup X c= succ (union (On X))

proof end;

theorem Th28: :: ZF_REFLE:28

for W being Universe
for X being set st X in W holds
sup X in W

proof end;

theorem :: ZF_REFLE:29

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;