:: ZF_COLLA semantic presentation

definition

let E be non empty set ;
let A be Ordinal;
deffunc H₁( T-Sequence) -> set = { d where d is Element of E : for d1 being Element of E st d1 in d holds
ex C being Ordinal st
( C in dom $1 & d1 in union {($1 . C)} ) } ;
func Collapse E,A -> set means :Def1: :: ZF_COLLA:def 1
ex L being T-Sequence st
( it = { d where d is Element of E : for d1 being Element of E st d1 in d holds
ex B being Ordinal st
( B in dom L & d1 in union {(L . B)} ) } & dom L = A & ( for B being Ordinal st B in A holds
L . B = { d1 where d1 is Element of E : for d being Element of E st d in d1 holds
ex C being Ordinal st
( C in dom (L | B) & d in union {((L | B) . C)} ) } ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Collapse ZF_COLLA:def 1 :

theorem Th1: :: ZF_COLLA:1

for E being non empty set
for A being Ordinal holds Collapse E,A = { d where d is Element of E : for d1 being Element of E st d1 in d holds
ex B being Ordinal st
( B in A & d1 in Collapse E,B ) }

proof end;

theorem :: ZF_COLLA:2

for E being non empty set
for d being Element of E holds
( ( for d1 being Element of E holds not d1 in d ) iff d in Collapse E,{} )

proof end;

theorem :: ZF_COLLA:3

for E being non empty set
for A being Ordinal
for d being Element of E holds
( d /\ E c= Collapse E,A iff d in Collapse E,(succ A) )

proof end;

theorem Th4: :: ZF_COLLA:4

for E being non empty set
for A, B being Ordinal st A c= B holds
Collapse E,A c= Collapse E,B

proof end;

theorem Th5: :: ZF_COLLA:5

for E being non empty set
for d being Element of E ex A being Ordinal st d in Collapse E,A

proof end;

theorem Th6: :: ZF_COLLA:6

for E being non empty set
for A being Ordinal
for d', d being Element of E st d' in d & d in Collapse E,A holds
( d' in Collapse E,A & ex B being Ordinal st
( B in A & d' in Collapse E,B ) )

proof end;

theorem Th7: :: ZF_COLLA:7

for E being non empty set
for A being Ordinal holds Collapse E,A c= E

proof end;

theorem Th8: :: ZF_COLLA:8

for E being non empty set ex A being Ordinal st E = Collapse E,A

proof end;

theorem Th9: :: ZF_COLLA:9

for E being non empty set ex f being Function st
( dom f = E & ( for d being Element of E holds f . d = f .: d ) )

proof end;

definition

let f be Function;
let X, Y be set ;
pred f is_epsilon-isomorphism_of X,Y means :: ZF_COLLA:def 2
( dom f = X & rng f = Y & f is one-to-one & ( for x, y being set st x in X & y in X holds
( ex Z being set st
( Z = y & x in Z ) iff ex Z being set st
( f . y = Z & f . x in Z ) ) ) );

end;

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

definition

let X, Y be set ;
pred X,Y are_epsilon-isomorphic means :: ZF_COLLA:def 3
ex f being Function st f is_epsilon-isomorphism_of X,Y;

end;

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

theorem :: ZF_COLLA:10

canceled;

theorem :: ZF_COLLA:11

canceled;

theorem Th12: :: ZF_COLLA:12

for E being non empty set
for f being Function st dom f = E & ( for d being Element of E holds f . d = f .: d ) holds
rng f is epsilon-transitive

proof end;

theorem Th13: :: ZF_COLLA:13

for E being non empty set st E |= the_axiom_of_extensionality holds
for u, v being Element of E st ( for w being Element of E holds
( w in u iff w in v ) ) holds
u = v

proof end;

theorem :: ZF_COLLA:14

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

proof end;