:: ZF_COLLA semantic presentation
begin
definition
let
E
be ( ( non
empty
) ( non
empty
)
set
) ;
let
A
be ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ;
func
Collapse
(
E
,
A
)
->
( ( ) ( )
set
)
means
:: ZF_COLLA:def 1
ex
L
being ( (
T-Sequence-like
Relation-like
Function-like
) (
T-Sequence-like
Relation-like
Function-like
)
T-Sequence
) st
(
it
: ( (
Function-like
V29
(
E
: ( (
ZF-formula-like
) (
Relation-like
Function-like
V47
()
ZF-formula-like
)
M6
(
K32
() : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V32
()
V33
()
V34
()
V35
()
V36
()
V37
()
V38
() )
Element
of
K6
(
K28
() : ( ( ) (
V32
()
V33
()
V34
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) )) ,
A
: ( ( non
empty
) ( non
empty
)
set
) ) ) (
Relation-like
E
: ( (
ZF-formula-like
) (
Relation-like
Function-like
V47
()
ZF-formula-like
)
M6
(
K32
() : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V32
()
V33
()
V34
()
V35
()
V36
()
V37
()
V38
() )
Element
of
K6
(
K28
() : ( ( ) (
V32
()
V33
()
V34
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) ))
-defined
A
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V29
(
E
: ( (
ZF-formula-like
) (
Relation-like
Function-like
V47
()
ZF-formula-like
)
M6
(
K32
() : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V32
()
V33
()
V34
()
V35
()
V36
()
V37
()
V38
() )
Element
of
K6
(
K28
() : ( ( ) (
V32
()
V33
()
V34
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) )) ,
A
: ( ( non
empty
) ( non
empty
)
set
) ) )
Element
of
K6
(
K7
(
E
: ( (
ZF-formula-like
) (
Relation-like
Function-like
V47
()
ZF-formula-like
)
M6
(
K32
() : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V32
()
V33
()
V34
()
V35
()
V36
()
V37
()
V38
() )
Element
of
K6
(
K28
() : ( ( ) (
V32
()
V33
()
V34
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) )) ,
A
: ( ( non
empty
) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
=
{
d
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) where
d
is ( ( ) ( )
Element
of
E
: ( (
ZF-formula-like
) (
Relation-like
Function-like
V47
()
ZF-formula-like
)
M6
(
K32
() : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V32
()
V33
()
V34
()
V35
()
V36
()
V37
()
V38
() )
Element
of
K6
(
K28
() : ( ( ) (
V32
()
V33
()
V34
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) )) ) : for
d1
being ( ( ) ( )
Element
of
E
: ( (
ZF-formula-like
) (
Relation-like
Function-like
V47
()
ZF-formula-like
)
M6
(
K32
() : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V32
()
V33
()
V34
()
V35
()
V36
()
V37
()
V38
() )
Element
of
K6
(
K28
() : ( ( ) (
V32
()
V33
()
V34
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) )) ) st
d1
: ( ( ) ( )
Element
of
E
: ( ( non
empty
) ( non
empty
)
set
) )
in
d
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
ex
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
(
B
: ( ( ) ( )
Element
of
E
: ( ( non
empty
) ( non
empty
)
set
) )
in
dom
L
: ( (
T-Sequence-like
Relation-like
Function-like
) (
T-Sequence-like
Relation-like
Function-like
)
T-Sequence
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) &
d1
: ( ( ) ( )
Element
of
E
: ( ( non
empty
) ( non
empty
)
set
) )
in
union
{
(
L
: ( (
T-Sequence-like
Relation-like
Function-like
) (
T-Sequence-like
Relation-like
Function-like
)
T-Sequence
)
.
B
: ( ( ) ( )
Element
of
E
: ( ( non
empty
) ( non
empty
)
set
) )
)
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) )
}
&
dom
L
: ( (
T-Sequence-like
Relation-like
Function-like
) (
T-Sequence-like
Relation-like
Function-like
)
T-Sequence
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
A
: ( ( non
empty
) ( non
empty
)
set
) & ( for
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
A
: ( ( non
empty
) ( non
empty
)
set
) holds
L
: ( (
T-Sequence-like
Relation-like
Function-like
) (
T-Sequence-like
Relation-like
Function-like
)
T-Sequence
)
.
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( ( ) ( )
set
)
=
{
d1
: ( ( ) ( )
Element
of
E
: ( ( non
empty
) ( non
empty
)
set
) ) where
d1
is ( ( ) ( )
Element
of
E
: ( (
ZF-formula-like
) (
Relation-like
Function-like
V47
()
ZF-formula-like
)
M6
(
K32
() : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V32
()
V33
()
V34
()
V35
()
V36
()
V37
()
V38
() )
Element
of
K6
(
K28
() : ( ( ) (
V32
()
V33
()
V34
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) )) ) : for
d
being ( ( ) ( )
Element
of
E
: ( (
ZF-formula-like
) (
Relation-like
Function-like
V47
()
ZF-formula-like
)
M6
(
K32
() : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V32
()
V33
()
V34
()
V35
()
V36
()
V37
()
V38
() )
Element
of
K6
(
K28
() : ( ( ) (
V32
()
V33
()
V34
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) )) ) st
d
: ( ( ) ( )
Element
of
E
: ( ( non
empty
) ( non
empty
)
set
) )
in
d1
: ( ( ) ( )
Element
of
E
: ( ( non
empty
) ( non
empty
)
set
) ) holds
ex
C
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
(
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
dom
(
L
: ( (
T-Sequence-like
Relation-like
Function-like
) (
T-Sequence-like
Relation-like
Function-like
)
T-Sequence
)
|
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
Relation-like
) (
T-Sequence-like
Relation-like
rng
b
1
: ( (
T-Sequence-like
Relation-like
Function-like
) (
T-Sequence-like
Relation-like
Function-like
)
T-Sequence
) : ( ( ) ( )
set
)
-valued
Function-like
)
set
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) &
d
: ( ( ) ( )
Element
of
E
: ( ( non
empty
) ( non
empty
)
set
) )
in
union
{
(
(
L
: ( (
T-Sequence-like
Relation-like
Function-like
) (
T-Sequence-like
Relation-like
Function-like
)
T-Sequence
)
|
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
Relation-like
) (
T-Sequence-like
Relation-like
rng
b
1
: ( (
T-Sequence-like
Relation-like
Function-like
) (
T-Sequence-like
Relation-like
Function-like
)
T-Sequence
) : ( ( ) ( )
set
)
-valued
Function-like
)
set
)
.
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) )
}
) );
end;
theorem
:: ZF_COLLA:1
for
E
being ( ( non
empty
) ( non
empty
)
set
)
for
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
Collapse
(
E
: ( ( non
empty
) ( non
empty
)
set
) ,
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ) : ( ( ) ( )
set
)
=
{
d
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) where
d
is ( ( ) ( )
Element
of
E
: ( ( non
empty
) ( non
empty
)
set
) ) : for
d1
being ( ( ) ( )
Element
of
E
: ( ( non
empty
) ( non
empty
)
set
) ) st
d1
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
in
d
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) holds
ex
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
(
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) &
d1
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
in
Collapse
(
E
: ( ( non
empty
) ( non
empty
)
set
) ,
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ) : ( ( ) ( )
set
) )
}
;
theorem
:: ZF_COLLA:2
for
E
being ( ( non
empty
) ( non
empty
)
set
)
for
d
being ( ( ) ( )
Element
of
E
: ( ( non
empty
) ( non
empty
)
set
) ) holds
( ( for
d1
being ( ( ) ( )
Element
of
E
: ( ( non
empty
) ( non
empty
)
set
) ) holds not
d1
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
in
d
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) iff
d
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
in
Collapse
(
E
: ( ( non
empty
) ( non
empty
)
set
) ,
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
Function-like
functional
V32
()
V33
()
V34
()
V35
()
V36
()
V37
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: ZF_COLLA:3
for
E
being ( ( non
empty
) ( non
empty
)
set
)
for
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
for
d
being ( ( ) ( )
Element
of
E
: ( ( non
empty
) ( non
empty
)
set
) ) holds
(
d
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
/\
E
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
)
c=
Collapse
(
E
: ( ( non
empty
) ( non
empty
)
set
) ,
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ) : ( ( ) ( )
set
) iff
d
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
in
Collapse
(
E
: ( ( non
empty
) ( non
empty
)
set
) ,
(
succ
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: ZF_COLLA:4
for
E
being ( ( non
empty
) ( non
empty
)
set
)
for
A
,
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
c=
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
Collapse
(
E
: ( ( non
empty
) ( non
empty
)
set
) ,
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ) : ( ( ) ( )
set
)
c=
Collapse
(
E
: ( ( non
empty
) ( non
empty
)
set
) ,
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ) : ( ( ) ( )
set
) ;
theorem
:: ZF_COLLA:5
for
E
being ( ( non
empty
) ( non
empty
)
set
)
for
d
being ( ( ) ( )
Element
of
E
: ( ( non
empty
) ( non
empty
)
set
) ) ex
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
d
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
in
Collapse
(
E
: ( ( non
empty
) ( non
empty
)
set
) ,
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ) : ( ( ) ( )
set
) ;
theorem
:: ZF_COLLA:6
for
E
being ( ( non
empty
) ( non
empty
)
set
)
for
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
for
d9
,
d
being ( ( ) ( )
Element
of
E
: ( ( non
empty
) ( non
empty
)
set
) ) st
d9
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
in
d
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) &
d
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
in
Collapse
(
E
: ( ( non
empty
) ( non
empty
)
set
) ,
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ) : ( ( ) ( )
set
) holds
(
d9
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
in
Collapse
(
E
: ( ( non
empty
) ( non
empty
)
set
) ,
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ) : ( ( ) ( )
set
) & ex
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
(
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) &
d9
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
in
Collapse
(
E
: ( ( non
empty
) ( non
empty
)
set
) ,
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: ZF_COLLA:7
for
E
being ( ( non
empty
) ( non
empty
)
set
)
for
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
Collapse
(
E
: ( ( non
empty
) ( non
empty
)
set
) ,
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ) : ( ( ) ( )
set
)
c=
E
: ( ( non
empty
) ( non
empty
)
set
) ;
theorem
:: ZF_COLLA:8
for
E
being ( ( non
empty
) ( non
empty
)
set
) ex
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
E
: ( ( non
empty
) ( non
empty
)
set
)
=
Collapse
(
E
: ( ( non
empty
) ( non
empty
)
set
) ,
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ) : ( ( ) ( )
set
) ;
theorem
:: ZF_COLLA:9
for
E
being ( ( non
empty
) ( non
empty
)
set
) ex
f
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) st
(
dom
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
)
=
E
: ( ( non
empty
) ( non
empty
)
set
) & ( for
d
being ( ( ) ( )
Element
of
E
: ( ( non
empty
) ( non
empty
)
set
) ) holds
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
d
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) : ( ( ) ( )
set
)
=
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.:
d
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ) ;
definition
let
f
be ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) ;
let
X
,
Y
be ( ( ) ( )
set
) ;
pred
f
is_epsilon-isomorphism_of
X
,
Y
means
:: ZF_COLLA:def 2
(
dom
f
: ( (
ZF-formula-like
) (
Relation-like
Function-like
V47
()
ZF-formula-like
)
M6
(
K32
() : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V32
()
V33
()
V34
()
V35
()
V36
()
V37
()
V38
() )
Element
of
K6
(
K28
() : ( ( ) (
V32
()
V33
()
V34
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) )) : ( ( ) ( )
set
)
=
X
: ( ( non
empty
) ( non
empty
)
set
) &
rng
f
: ( (
ZF-formula-like
) (
Relation-like
Function-like
V47
()
ZF-formula-like
)
M6
(
K32
() : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V32
()
V33
()
V34
()
V35
()
V36
()
V37
()
V38
() )
Element
of
K6
(
K28
() : ( ( ) (
V32
()
V33
()
V34
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) )) : ( ( ) ( )
set
)
=
Y
: ( (
Function-like
V29
(
f
: ( (
ZF-formula-like
) (
Relation-like
Function-like
V47
()
ZF-formula-like
)
M6
(
K32
() : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V32
()
V33
()
V34
()
V35
()
V36
()
V37
()
V38
() )
Element
of
K6
(
K28
() : ( ( ) (
V32
()
V33
()
V34
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) )) ,
X
: ( ( non
empty
) ( non
empty
)
set
) ) ) (
Relation-like
f
: ( (
ZF-formula-like
) (
Relation-like
Function-like
V47
()
ZF-formula-like
)
M6
(
K32
() : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V32
()
V33
()
V34
()
V35
()
V36
()
V37
()
V38
() )
Element
of
K6
(
K28
() : ( ( ) (
V32
()
V33
()
V34
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) ))
-defined
X
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V29
(
f
: ( (
ZF-formula-like
) (
Relation-like
Function-like
V47
()
ZF-formula-like
)
M6
(
K32
() : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V32
()
V33
()
V34
()
V35
()
V36
()
V37
()
V38
() )
Element
of
K6
(
K28
() : ( ( ) (
V32
()
V33
()
V34
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) )) ,
X
: ( ( non
empty
) ( non
empty
)
set
) ) )
Element
of
K6
(
K7
(
f
: ( (
ZF-formula-like
) (
Relation-like
Function-like
V47
()
ZF-formula-like
)
M6
(
K32
() : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V32
()
V33
()
V34
()
V35
()
V36
()
V37
()
V38
() )
Element
of
K6
(
K28
() : ( ( ) (
V32
()
V33
()
V34
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) )) ,
X
: ( ( non
empty
) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) &
f
: ( (
ZF-formula-like
) (
Relation-like
Function-like
V47
()
ZF-formula-like
)
M6
(
K32
() : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V32
()
V33
()
V34
()
V35
()
V36
()
V37
()
V38
() )
Element
of
K6
(
K28
() : ( ( ) (
V32
()
V33
()
V34
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) )) is
one-to-one
& ( for
x
,
y
being ( ( ) ( )
set
) st
x
: ( ( ) ( )
set
)
in
X
: ( ( non
empty
) ( non
empty
)
set
) &
y
: ( ( ) ( )
set
)
in
X
: ( ( non
empty
) ( non
empty
)
set
) holds
( ex
Z
being ( ( ) ( )
set
) st
(
Z
: ( ( ) ( )
set
)
=
y
: ( ( ) ( )
set
) &
x
: ( ( ) ( )
set
)
in
Z
: ( ( ) ( )
set
) ) iff ex
Z
being ( ( ) ( )
set
) st
(
f
: ( (
ZF-formula-like
) (
Relation-like
Function-like
V47
()
ZF-formula-like
)
M6
(
K32
() : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V32
()
V33
()
V34
()
V35
()
V36
()
V37
()
V38
() )
Element
of
K6
(
K28
() : ( ( ) (
V32
()
V33
()
V34
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) ))
.
y
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
=
Z
: ( ( ) ( )
set
) &
f
: ( (
ZF-formula-like
) (
Relation-like
Function-like
V47
()
ZF-formula-like
)
M6
(
K32
() : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V32
()
V33
()
V34
()
V35
()
V36
()
V37
()
V38
() )
Element
of
K6
(
K28
() : ( ( ) (
V32
()
V33
()
V34
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) ))
.
x
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
in
Z
: ( ( ) ( )
set
) ) ) ) );
end;
definition
let
X
,
Y
be ( ( ) ( )
set
) ;
pred
X
,
Y
are_epsilon-isomorphic
means
:: ZF_COLLA:def 3
ex
f
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) st
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
is_epsilon-isomorphism_of
X
: ( (
ZF-formula-like
) (
Relation-like
Function-like
V47
()
ZF-formula-like
)
M6
(
K32
() : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V32
()
V33
()
V34
()
V35
()
V36
()
V37
()
V38
() )
Element
of
K6
(
K28
() : ( ( ) (
V32
()
V33
()
V34
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) )) ,
Y
: ( ( non
empty
) ( non
empty
)
set
) ;
end;
theorem
:: ZF_COLLA:10
for
E
being ( ( non
empty
) ( non
empty
)
set
)
for
f
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) st
dom
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
)
=
E
: ( ( non
empty
) ( non
empty
)
set
) & ( for
d
being ( ( ) ( )
Element
of
E
: ( ( non
empty
) ( non
empty
)
set
) ) holds
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
d
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) : ( ( ) ( )
set
)
=
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.:
d
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) holds
rng
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( ( ) ( )
set
) is
epsilon-transitive
;
theorem
:: ZF_COLLA:11
for
E
being ( ( non
empty
) ( non
empty
)
set
) st
E
: ( ( non
empty
) ( non
empty
)
set
)
|=
the_axiom_of_extensionality
: ( (
ZF-formula-like
) (
Relation-like
K32
() : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V32
()
V33
()
V34
()
V35
()
V36
()
V37
()
V38
() )
Element
of
K6
(
K28
() : ( ( ) (
V32
()
V33
()
V34
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
-defined
K32
() : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V32
()
V33
()
V34
()
V35
()
V36
()
V37
()
V38
() )
Element
of
K6
(
K28
() : ( ( ) (
V32
()
V33
()
V34
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
-valued
Function-like
V47
()
ZF-formula-like
)
M7
(
K32
() : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V32
()
V33
()
V34
()
V35
()
V36
()
V37
()
V38
() )
Element
of
K6
(
K28
() : ( ( ) (
V32
()
V33
()
V34
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) )) holds
for
u
,
v
being ( ( ) ( )
Element
of
E
: ( ( non
empty
) ( non
empty
)
set
) ) st ( for
w
being ( ( ) ( )
Element
of
E
: ( ( non
empty
) ( non
empty
)
set
) ) holds
(
w
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
in
u
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) iff
w
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
in
v
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ) ) holds
u
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
=
v
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) ;
theorem
:: ZF_COLLA:12
for
E
being ( ( non
empty
) ( non
empty
)
set
) st
E
: ( ( non
empty
) ( non
empty
)
set
)
|=
the_axiom_of_extensionality
: ( (
ZF-formula-like
) (
Relation-like
K32
() : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V32
()
V33
()
V34
()
V35
()
V36
()
V37
()
V38
() )
Element
of
K6
(
K28
() : ( ( ) (
V32
()
V33
()
V34
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
-defined
K32
() : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V32
()
V33
()
V34
()
V35
()
V36
()
V37
()
V38
() )
Element
of
K6
(
K28
() : ( ( ) (
V32
()
V33
()
V34
()
V38
() )
set
) ) : ( ( ) ( )
set
) )
-valued
Function-like
V47
()
ZF-formula-like
)
M7
(
K32
() : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
V32
()
V33
()
V34
()
V35
()
V36
()
V37
()
V38
() )
Element
of
K6
(
K28
() : ( ( ) (
V32
()
V33
()
V34
()
V38
() )
set
) ) : ( ( ) ( )
set
) ) )) holds
ex
X
being ( ( ) ( )
set
) st
(
X
: ( ( ) ( )
set
) is
epsilon-transitive
&
E
: ( ( non
empty
) ( non
empty
)
set
) ,
X
: ( ( ) ( )
set
)
are_epsilon-isomorphic
) ;