:: ZF_FUND2 semantic presentation
begin
definition
let
H
be ( (
ZF-formula-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-defined
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-valued
Function-like
V43
()
ZF-formula-like
)
ZF-formula
) ;
let
M
be ( ( non
empty
) ( non
empty
)
set
) ;
let
v
be ( (
Function-like
quasi_total
) (
Relation-like
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) )
-defined
M
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
quasi_total
)
Function
of
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) ) ,
M
: ( ( non
empty
) ( non
empty
)
set
) ) ;
func
Section
(
H
,
v
)
->
( ( ) ( )
Subset
of ( ( ) ( )
set
) )
equals
:: ZF_FUND2:def 1
{
m
: ( ( ) ( )
Element
of
M
: ( ( non
empty
) ( non
empty
)
set
) ) where
m
is ( ( ) ( )
Element
of
M
: ( (
ext-real
) (
ext-real
)
set
) ) :
M
: ( (
ext-real
) (
ext-real
)
set
) ,
v
: ( ( ) ( )
set
)
/
(
(
x.
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
V28
()
V29
()
V35
()
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) ) ) ,
m
: ( ( ) ( )
Element
of
M
: ( ( non
empty
) ( non
empty
)
set
) ) ) : ( (
Function-like
quasi_total
) (
Relation-like
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) )
-defined
M
: ( (
ext-real
) (
ext-real
)
set
)
-valued
Function-like
quasi_total
)
Element
of
bool
[:
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) ) ,
M
: ( (
ext-real
) (
ext-real
)
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
|=
H
: ( (
ext-real
) (
ext-real
)
set
)
}
if
x.
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
V28
()
V29
()
V35
()
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Element
of
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) ) )
in
Free
H
: ( (
ext-real
) (
ext-real
)
set
) : ( ( ) ( )
Element
of
bool
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) ) : ( ( ) ( )
set
) )
otherwise
{}
: ( ( ) ( )
set
) ;
end;
definition
let
M
be ( ( non
empty
) ( non
empty
)
set
) ;
attr
M
is
predicatively_closed
means
:: ZF_FUND2:def 2
for
H
being ( (
ZF-formula-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-defined
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-valued
Function-like
V43
()
ZF-formula-like
)
ZF-formula
)
for
E
being ( ( non
empty
) ( non
empty
)
set
)
for
f
being ( (
Function-like
quasi_total
) (
Relation-like
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) )
-defined
b
2
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
quasi_total
)
Function
of
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) ) ,
E
: ( ( non
empty
) ( non
empty
)
set
) ) st
E
: ( ( non
empty
) ( non
empty
)
set
)
in
M
: ( (
ext-real
) (
ext-real
)
set
) holds
Section
(
H
: ( (
ZF-formula-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-defined
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-valued
Function-like
V43
()
ZF-formula-like
)
ZF-formula
) ,
f
: ( (
Function-like
quasi_total
) (
Relation-like
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) )
-defined
b
2
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
quasi_total
)
Function
of
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) ) ,
b
2
: ( ( non
empty
) ( non
empty
)
set
) ) ) : ( ( ) ( )
Subset
of ( ( ) ( )
set
) )
in
M
: ( (
ext-real
) (
ext-real
)
set
) ;
end;
theorem
:: ZF_FUND2:1
for
E
being ( ( non
empty
) ( non
empty
)
set
)
for
e
being ( ( ) ( )
Element
of
E
: ( ( non
empty
) ( non
empty
)
set
) )
for
f
being ( (
Function-like
quasi_total
) (
Relation-like
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) )
-defined
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
quasi_total
)
Function
of
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) ) ,
E
: ( ( non
empty
) ( non
empty
)
set
) ) st
E
: ( ( non
empty
) ( non
empty
)
set
) is
epsilon-transitive
holds
Section
(
(
All
(
(
x.
2 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
V28
()
V29
()
V35
()
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) ) ) ,
(
(
(
x.
2 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
V28
()
V29
()
V35
()
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) ) )
'in'
(
x.
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
V28
()
V29
()
V35
()
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) ) )
)
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-defined
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-valued
Function-like
V43
()
ZF-formula-like
)
M7
(
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ))
=>
(
(
x.
2 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
V28
()
V29
()
V35
()
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) ) )
'in'
(
x.
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
V28
()
V29
()
V35
()
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) ) )
)
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-defined
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-valued
Function-like
V43
()
ZF-formula-like
)
M7
(
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ))
)
: ( (
ZF-formula-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-defined
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-valued
Function-like
V43
()
ZF-formula-like
)
M7
(
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )) )
)
: ( ( ) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-defined
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-valued
Function-like
V43
()
ZF-formula-like
)
M7
(
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )) ,
(
f
: ( (
Function-like
quasi_total
) (
Relation-like
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) )
-defined
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
quasi_total
)
Function
of
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) ) ,
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
/
(
(
x.
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
V28
()
V29
()
V35
()
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) ) ) ,
e
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) ) )
)
: ( (
Function-like
quasi_total
) (
Relation-like
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) )
-defined
b
1
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
quasi_total
)
Element
of
bool
[:
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) ) ,
b
1
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
Subset
of ( ( ) ( )
set
) )
=
E
: ( ( non
empty
) ( non
empty
)
set
)
/\
(
bool
e
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
)
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ;
theorem
:: ZF_FUND2:2
for
W
being ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
for
L
being ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
W
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) st ( for
a
,
b
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
of
W
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) st
a
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
in
b
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) holds
L
: ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
.
a
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) : ( ( non
empty
) ( non
empty
)
Element
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
c=
L
: ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
.
b
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) : ( ( non
empty
) ( non
empty
)
Element
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) ) & ( for
a
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
of
W
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) holds
(
L
: ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
.
a
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) : ( ( non
empty
) ( non
empty
)
Element
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
in
Union
L
: ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) : ( ( non
empty
) ( non
empty
)
Element
of
bool
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) : ( ( ) ( )
set
) ) &
L
: ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
.
a
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) : ( ( non
empty
) ( non
empty
)
Element
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) is
epsilon-transitive
) ) &
Union
L
: ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) : ( ( non
empty
) ( non
empty
)
Element
of
bool
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) : ( ( ) ( )
set
) ) is
predicatively_closed
holds
Union
L
: ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) : ( ( non
empty
) ( non
empty
)
Element
of
bool
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) : ( ( ) ( )
set
) )
|=
the_axiom_of_power_sets
: ( (
ZF-formula-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-defined
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-valued
Function-like
V43
()
ZF-formula-like
)
M7
(
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )) ;
theorem
:: ZF_FUND2:3
for
W
being ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
for
L
being ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
W
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) st
omega
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
set
)
in
W
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) & ( for
a
,
b
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
of
W
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) st
a
: ( (
ZF-formula-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-defined
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-valued
Function-like
V43
()
ZF-formula-like
)
ZF-formula
)
in
b
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) holds
L
: ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
.
a
: ( (
ZF-formula-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-defined
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-valued
Function-like
V43
()
ZF-formula-like
)
ZF-formula
) : ( ( non
empty
) ( non
empty
)
Element
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
c=
L
: ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
.
b
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) : ( ( non
empty
) ( non
empty
)
Element
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) ) & ( for
a
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
of
W
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) st
a
: ( (
ZF-formula-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-defined
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-valued
Function-like
V43
()
ZF-formula-like
)
ZF-formula
)
<>
{}
: ( ( ) ( )
set
) &
a
: ( (
ZF-formula-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-defined
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-valued
Function-like
V43
()
ZF-formula-like
)
ZF-formula
) is
limit_ordinal
holds
L
: ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
.
a
: ( (
ZF-formula-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-defined
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-valued
Function-like
V43
()
ZF-formula-like
)
ZF-formula
) : ( ( non
empty
) ( non
empty
)
Element
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
=
Union
(
L
: ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
|
a
: ( (
ZF-formula-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-defined
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-valued
Function-like
V43
()
ZF-formula-like
)
ZF-formula
)
)
: ( (
Relation-like
) (
Relation-like
Function-like
)
set
) : ( ( ) ( )
set
) ) & ( for
a
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
of
W
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) holds
(
L
: ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
.
a
: ( (
ZF-formula-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-defined
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-valued
Function-like
V43
()
ZF-formula-like
)
ZF-formula
) : ( ( non
empty
) ( non
empty
)
Element
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
in
Union
L
: ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) : ( ( non
empty
) ( non
empty
)
Element
of
bool
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) : ( ( ) ( )
set
) ) &
L
: ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
.
a
: ( (
ZF-formula-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-defined
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-valued
Function-like
V43
()
ZF-formula-like
)
ZF-formula
) : ( ( non
empty
) ( non
empty
)
Element
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) is
epsilon-transitive
) ) &
Union
L
: ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) : ( ( non
empty
) ( non
empty
)
Element
of
bool
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) : ( ( ) ( )
set
) ) is
predicatively_closed
holds
for
H
being ( (
ZF-formula-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-defined
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-valued
Function-like
V43
()
ZF-formula-like
)
ZF-formula
) st
{
(
x.
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
V28
()
V29
()
V35
()
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) ) ) ,
(
x.
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
V28
()
V29
()
V35
()
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) ) ) ,
(
x.
2 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
V28
()
V29
()
V35
()
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Element
of
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) ) )
}
: ( ( ) (
V35
() )
set
)
misses
Free
H
: ( (
ZF-formula-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-defined
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-valued
Function-like
V43
()
ZF-formula-like
)
ZF-formula
) : ( ( ) (
V35
() )
Element
of
bool
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) ) : ( ( ) ( )
set
) ) holds
Union
L
: ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) : ( ( non
empty
) ( non
empty
)
Element
of
bool
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) : ( ( ) ( )
set
) )
|=
the_axiom_of_substitution_for
H
: ( (
ZF-formula-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-defined
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-valued
Function-like
V43
()
ZF-formula-like
)
ZF-formula
) : ( (
ZF-formula-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-defined
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-valued
Function-like
V43
()
ZF-formula-like
)
M7
(
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )) ;
theorem
:: ZF_FUND2:4
for
H
being ( (
ZF-formula-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-defined
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-valued
Function-like
V43
()
ZF-formula-like
)
ZF-formula
)
for
M
being ( ( non
empty
) ( non
empty
)
set
)
for
v
being ( (
Function-like
quasi_total
) (
Relation-like
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) )
-defined
b
2
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
quasi_total
)
Function
of
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) ) ,
M
: ( ( non
empty
) ( non
empty
)
set
) ) holds
Section
(
H
: ( (
ZF-formula-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-defined
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-valued
Function-like
V43
()
ZF-formula-like
)
ZF-formula
) ,
v
: ( (
Function-like
quasi_total
) (
Relation-like
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) )
-defined
b
2
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
quasi_total
)
Function
of
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) ) ,
b
2
: ( ( non
empty
) ( non
empty
)
set
) ) ) : ( ( ) ( )
Subset
of ( ( ) ( )
set
) )
=
{
m
: ( ( ) ( )
Element
of
b
2
: ( ( non
empty
) ( non
empty
)
set
) ) where
m
is ( ( ) ( )
Element
of
M
: ( ( non
empty
) ( non
empty
)
set
) ) :
{
[
{}
: ( ( ) ( )
set
) ,
m
: ( ( ) ( )
Element
of
b
2
: ( ( non
empty
) ( non
empty
)
set
) )
]
: ( ( ) ( )
set
)
}
: ( ( ) (
Function-like
non
empty
trivial
V35
() 1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
V28
()
V29
()
V35
()
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
-element
)
set
)
\/
(
(
v
: ( (
Function-like
quasi_total
) (
Relation-like
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) )
-defined
b
2
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
quasi_total
)
Function
of
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) ) ,
b
2
: ( ( non
empty
) ( non
empty
)
set
) )
*
decode
: ( (
Function-like
quasi_total
) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
set
)
-defined
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) )
-valued
Function-like
quasi_total
)
Element
of
bool
[:
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
set
) ,
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) )
:]
: ( ( ) ( non
trivial
V35
() )
set
) : ( ( ) ( non
trivial
V35
() )
set
) )
)
: ( (
Function-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
set
)
-defined
b
2
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
)
Element
of
bool
[:
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
set
) ,
b
2
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( non
trivial
V35
() )
set
) : ( ( ) ( non
trivial
V35
() )
set
) )
|
(
(
code
(
Free
H
: ( (
ZF-formula-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-defined
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-valued
Function-like
V43
()
ZF-formula-like
)
ZF-formula
)
)
: ( ( ) (
V35
() )
Element
of
bool
VAR
: ( ( ) ( non
empty
)
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) : ( ( ) ( non
trivial
V35
() )
set
) ) : ( ( ) ( )
set
) )
)
: ( ( ) (
V35
() )
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
set
) : ( ( ) ( non
trivial
V35
() )
set
) )
\
{
{}
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
V35
() 1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
ext-real
positive
V28
()
V29
()
V35
()
cardinal
)
Element
of
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
-element
)
set
)
)
: ( ( ) (
V35
() )
Element
of
bool
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
set
) : ( ( ) ( non
trivial
V35
() )
set
) )
)
: ( (
Function-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
set
)
-defined
b
2
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V35
() )
Element
of
bool
[:
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
set
) ,
b
2
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( non
trivial
V35
() )
set
) : ( ( ) ( non
trivial
V35
() )
set
) ) : ( ( ) (
V35
() )
set
)
in
Diagram
(
H
: ( (
ZF-formula-like
) (
Relation-like
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-defined
NAT
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
Element
of
bool
REAL
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
-valued
Function-like
V43
()
ZF-formula-like
)
ZF-formula
) ,
M
: ( ( non
empty
) ( non
empty
)
set
) ) : ( ( ) ( )
set
)
}
;
theorem
:: ZF_FUND2:5
for
W
being ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
for
Y
being ( ( non
empty
) ( non
empty
)
Subclass
of ( ( ) ( )
set
) ) st
Y
: ( ( non
empty
) ( non
empty
)
Subclass
of ( ( ) ( )
set
) ) is
closed_wrt_A1-A7
&
Y
: ( ( non
empty
) ( non
empty
)
Subclass
of ( ( ) ( )
set
) ) is
epsilon-transitive
holds
Y
: ( ( non
empty
) ( non
empty
)
Subclass
of ( ( ) ( )
set
) ) is
predicatively_closed
;
theorem
:: ZF_FUND2:6
for
W
being ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
for
L
being ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
W
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) st
omega
: ( ( ) ( non
empty
non
trivial
epsilon-transitive
epsilon-connected
ordinal
V35
()
cardinal
limit_cardinal
)
set
)
in
W
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) & ( for
a
,
b
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
of
W
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) st
a
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
in
b
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) holds
L
: ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
.
a
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) : ( ( non
empty
) ( non
empty
)
Element
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
c=
L
: ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
.
b
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) : ( ( non
empty
) ( non
empty
)
Element
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) ) & ( for
a
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
of
W
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) st
a
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
<>
{}
: ( ( ) ( )
set
) &
a
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) is
limit_ordinal
holds
L
: ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
.
a
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) : ( ( non
empty
) ( non
empty
)
Element
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
=
Union
(
L
: ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
|
a
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
)
: ( (
Relation-like
) (
Relation-like
rng
b
2
: ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) : ( ( ) (
V68
() )
set
)
-valued
Function-like
T-Sequence-like
)
set
) : ( ( ) ( )
set
) ) & ( for
a
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
of
W
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) holds
(
L
: ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
.
a
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) : ( ( non
empty
) ( non
empty
)
Element
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
in
Union
L
: ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) : ( ( non
empty
) ( non
empty
)
Element
of
bool
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) : ( ( ) ( )
set
) ) &
L
: ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) )
.
a
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) : ( ( non
empty
) ( non
empty
)
Element
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) is
epsilon-transitive
) ) &
Union
L
: ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) : ( ( non
empty
) ( non
empty
)
Element
of
bool
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) : ( ( ) ( )
set
) ) is
closed_wrt_A1-A7
holds
Union
L
: ( (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
) (
Relation-like
non-empty
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
)
-valued
Function-like
T-Sequence-like
DOMAIN-yielding
)
DOMAIN-Sequence
of
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) ) : ( ( non
empty
) ( non
empty
)
Element
of
bool
b
1
: ( ( non
empty
universal
) ( non
empty
epsilon-transitive
V33
()
V34
()
universal
)
Universe
) : ( ( ) ( )
set
) ) is
being_a_model_of_ZF
;