:: ZF_COLLA semantic presentation

definition

let c₁ be non empty set ;
let c₂ be Ordinal;
deffunc H₁( T-Sequence) -> set = { b₁ where B is Element of c₁ : for b₁ being Element of c₁ st b₂ in b₁ holds
ex b₂ being Ordinal st
( b₃ in dom a₁ & b₂ in union {(a₁ . b₃)} ) } ;
func Collapse c₁,c₂ -> set means :Def1: :: ZF_COLLA:def 1
ex b₁ being T-Sequence st
( a₃ = { b₂ where B is Element of a₁ : for b₁ being Element of a₁ st b₃ in b₂ holds
ex b₂ being Ordinal st
( b₄ in dom b₁ & b₃ in union {(b₁ . b₄)} ) } & dom b₁ = a₂ & ( for b₂ being Ordinal st b₂ in a₂ holds
b₁ . b₂ = { b₃ where B is Element of a₁ : for b₁ being Element of a₁ st b₄ in b₃ holds
ex b₂ being Ordinal st
( b₅ in dom (b₁ | b₂) & b₄ in union {((b₁ | b₂) . b₅)} ) } ) );
existence

proof end;

proof end;

end;

:: deftheorem Def1 defines Collapse ZF_COLLA:def 1 :

theorem Th1: :: ZF_COLLA:1

for b₁ being non empty set
for b₂ being Ordinal holds Collapse b₁,b₂ = { b₃ where B is Element of b₁ : for b₁ being Element of b₁ st b₄ in b₃ holds
ex b₂ being Ordinal st
( b₅ in b₂ & b₄ in Collapse b₁,b₅ ) }

proof end;

theorem Th2: :: ZF_COLLA:2

for b₁ being non empty set
for b₂ being Element of b₁ holds
( ( for b₃ being Element of b₁ holds not b₃ in b₂ ) iff b₂ in Collapse b₁,{} )

proof end;

theorem Th3: :: ZF_COLLA:3

for b₁ being non empty set
for b₂ being Ordinal
for b₃ being Element of b₁ holds
( b₃ /\ b₁ c= Collapse b₁,b₂ iff b₃ in Collapse b₁,(succ b₂) )

proof end;

theorem Th4: :: ZF_COLLA:4

for b₁ being non empty set
for b₂, b₃ being Ordinal st b₂ c= b₃ holds
Collapse b₁,b₂ c= Collapse b₁,b₃

proof end;

theorem Th5: :: ZF_COLLA:5

for b₁ being non empty set
for b₂ being Element of b₁ ex b₃ being Ordinal st b₂ in Collapse b₁,b₃

proof end;

theorem Th6: :: ZF_COLLA:6

for b₁ being non empty set
for b₂ being Ordinal
for b₃, b₄ being Element of b₁ st b₃ in b₄ & b₄ in Collapse b₁,b₂ holds
( b₃ in Collapse b₁,b₂ & ex b₅ being Ordinal st
( b₅ in b₂ & b₃ in Collapse b₁,b₅ ) )

proof end;

theorem Th7: :: ZF_COLLA:7

for b₁ being non empty set
for b₂ being Ordinal holds Collapse b₁,b₂ c= b₁

proof end;

theorem Th8: :: ZF_COLLA:8

for b₁ being non empty set ex b₂ being Ordinal st b₁ = Collapse b₁,b₂

proof end;

theorem Th9: :: ZF_COLLA:9

for b₁ being non empty set ex b₂ being Function st
( dom b₂ = b₁ & ( for b₃ being Element of b₁ holds b₂ . b₃ = b₂ .: b₃ ) )

proof end;

definition

let c₁ be Function;
let c₂, c₃ be set ;
pred c₁ is_epsilon-isomorphism_of c₂,c₃ means :: ZF_COLLA:def 2
( dom a₁ = a₂ & rng a₁ = a₃ & a₁ is one-to-one & ( for b₁, b₂ being set st b₁ in a₂ & b₂ in a₂ holds
( ex b₃ being set st
( b₃ = b₂ & b₁ in b₃ ) iff ex b₃ being set st
( a₁ . b₂ = b₃ & a₁ . b₁ in b₃ ) ) ) );

end;

:: deftheorem Def2 defines is_epsilon-isomorphism_of ZF_COLLA:def 2 :

definition

let c₁, c₂ be set ;
pred c₁,c₂ are_epsilon-isomorphic means :: ZF_COLLA:def 3
ex b₁ being Function st b₁ is_epsilon-isomorphism_of a₁,a₂;

end;

:: deftheorem Def3 defines are_epsilon-isomorphic ZF_COLLA:def 3 :

theorem Th10: :: ZF_COLLA:10

canceled;

theorem Th11: :: ZF_COLLA:11

canceled;

theorem Th12: :: ZF_COLLA:12

for b₁ being non empty set
for b₂ being Function st dom b₂ = b₁ & ( for b₃ being Element of b₁ holds b₂ . b₃ = b₂ .: b₃ ) holds
rng b₂ is epsilon-transitive

proof end;

theorem Th13: :: ZF_COLLA:13

for b₁ being non empty set st b₁ |= the_axiom_of_extensionality holds
for b₂, b₃ being Element of b₁ st ( for b₄ being Element of b₁ holds
( b₄ in b₂ iff b₄ in b₃ ) ) holds
b₂ = b₃

proof end;

theorem Th14: :: ZF_COLLA:14

for b₁ being non empty set st b₁ |= the_axiom_of_extensionality holds
ex b₂ being set st
( b₂ is epsilon-transitive & b₁,b₂ are_epsilon-isomorphic )

proof end;