:: ORDINAL3 semantic presentation
begin
theorem
:: ORDINAL3:1
for
X
being ( ( ) ( )
set
) holds
X
: ( ( ) ( )
set
)
c=
succ
X
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ;
theorem
:: ORDINAL3:2
for
X
,
Y
being ( ( ) ( )
set
) st
succ
X
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
)
c=
Y
: ( ( ) ( )
set
) holds
X
: ( ( ) ( )
set
)
c=
Y
: ( ( ) ( )
set
) ;
theorem
:: ORDINAL3:3
for
A
,
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) iff
succ
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
set
)
in
succ
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
set
) ) ;
theorem
:: ORDINAL3:4
for
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
for
X
being ( ( ) ( )
set
) st
X
: ( ( ) ( )
set
)
c=
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
union
X
: ( ( ) ( )
set
) : ( ( ) ( )
set
) is ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ;
theorem
:: ORDINAL3:5
for
X
being ( ( ) ( )
set
) holds
union
(
On
X
: ( ( ) ( )
set
)
)
: ( ( ) ( )
set
) : ( ( ) ( )
set
) is ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ;
theorem
:: ORDINAL3:6
for
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
for
X
being ( ( ) ( )
set
) st
X
: ( ( ) ( )
set
)
c=
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
On
X
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
=
X
: ( ( ) ( )
set
) ;
theorem
:: ORDINAL3:7
for
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
On
{
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
}
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
)
=
{
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
}
: ( ( ) ( non
empty
)
set
) ;
theorem
:: ORDINAL3:8
for
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
<>
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) holds
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
)
in
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ;
theorem
:: ORDINAL3:9
for
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
inf
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) ;
theorem
:: ORDINAL3:10
for
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
inf
{
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
}
: ( ( ) ( non
empty
)
set
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ;
theorem
:: ORDINAL3:11
for
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
for
X
being ( ( ) ( )
set
) st
X
: ( ( ) ( )
set
)
c=
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
meet
X
: ( ( ) ( )
set
) : ( ( ) ( )
set
) is ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ;
registration
let
A
,
B
be ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ;
cluster
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
\/
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) : ( ( ) ( )
set
)
->
ordinal
;
cluster
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
/\
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) : ( ( ) ( )
set
)
->
ordinal
;
end;
theorem
:: ORDINAL3:12
for
A
,
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
\/
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) or
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
\/
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ) ;
theorem
:: ORDINAL3:13
for
A
,
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
/\
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) or
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
/\
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ) ;
theorem
:: ORDINAL3:14
for
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
)
Element
of
omega
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
set
) ) holds
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) ;
theorem
:: ORDINAL3:15
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
)
Element
of
omega
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
set
) )
=
{
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
)
}
: ( ( ) ( non
empty
)
set
) ;
theorem
:: ORDINAL3:16
for
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
( not
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
c=
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
)
Element
of
omega
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
set
) ) or
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) or
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
)
Element
of
omega
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
set
) ) ) ;
theorem
:: ORDINAL3:17
for
A
,
B
,
C
,
D
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
) or
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ) &
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
D
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
in
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
D
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ;
theorem
:: ORDINAL3:18
for
A
,
B
,
C
,
D
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
) &
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
c=
D
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
c=
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
D
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ;
theorem
:: ORDINAL3:19
for
A
,
B
,
C
,
D
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) & ( (
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
c=
D
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) &
D
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
<>
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) ) or
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
D
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ) holds
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
in
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
D
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ;
theorem
:: ORDINAL3:20
for
A
,
B
,
C
,
D
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
) &
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
c=
D
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
c=
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
D
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ;
theorem
:: ORDINAL3:21
for
B
,
C
,
D
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
D
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) holds
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
D
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ;
theorem
:: ORDINAL3:22
for
B
,
C
,
D
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
in
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
D
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) holds
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
D
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ;
theorem
:: ORDINAL3:23
for
B
,
C
,
D
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
c=
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
D
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) holds
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
c=
D
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ;
theorem
:: ORDINAL3:24
for
A
,
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
c=
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) &
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
c=
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ) ;
theorem
:: ORDINAL3:25
for
A
,
B
,
C
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) &
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ) ;
theorem
:: ORDINAL3:26
for
A
,
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) holds
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) &
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) ) ;
theorem
:: ORDINAL3:27
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
ex
C
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ;
theorem
:: ORDINAL3:28
for
A
,
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
ex
C
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
(
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) &
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
<>
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) ) ;
theorem
:: ORDINAL3:29
for
A
,
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
<>
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) &
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) is
limit_ordinal
holds
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) is
limit_ordinal
;
theorem
:: ORDINAL3:30
for
A
,
B
,
C
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
+^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
(
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ;
theorem
:: ORDINAL3:31
for
A
,
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
( not
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) or
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) or
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) ) ;
theorem
:: ORDINAL3:32
for
A
,
B
,
C
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) &
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
<>
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) holds
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) &
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ) ;
theorem
:: ORDINAL3:33
for
B
,
A
,
C
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) &
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
<>
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) holds
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ;
theorem
:: ORDINAL3:34
for
B
,
A
,
C
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
in
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) holds
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ;
theorem
:: ORDINAL3:35
for
B
,
A
,
C
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
c=
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) &
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
<>
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) holds
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
c=
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ;
theorem
:: ORDINAL3:36
for
B
,
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
<>
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) holds
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
c=
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) &
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
c=
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ) ;
theorem
:: ORDINAL3:37
for
A
,
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
)
Element
of
omega
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
set
) ) holds
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
)
Element
of
omega
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
set
) ) &
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
)
Element
of
omega
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
set
) ) ) ;
theorem
:: ORDINAL3:38
for
A
,
B
,
C
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
( not
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) or
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) or ex
D
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
(
D
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) &
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
D
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ) ) ;
definition
let
C
be ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ;
let
fi
be ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
) ;
func
C
+^
fi
->
( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
)
means
:: ORDINAL3:def 1
(
dom
it
: ( ( ) ( )
Element
of
K10
(
C
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
=
dom
fi
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) : ( ( ) ( )
set
) & ( for
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
dom
fi
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) : ( ( ) ( )
set
) holds
it
: ( ( ) ( )
Element
of
K10
(
C
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
.
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( ( ) ( )
set
)
=
C
: ( ( ) ( )
set
)
+^
(
fi
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
.
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( ( ) ( )
set
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ) );
func
fi
+^
C
->
( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
)
means
:: ORDINAL3:def 2
(
dom
it
: ( ( ) ( )
Element
of
K10
(
C
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
=
dom
fi
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) : ( ( ) ( )
set
) & ( for
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
dom
fi
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) : ( ( ) ( )
set
) holds
it
: ( ( ) ( )
Element
of
K10
(
C
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
.
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( ( ) ( )
set
)
=
(
fi
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
.
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( ( ) ( )
set
)
+^
C
: ( ( ) ( )
set
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ) );
func
C
*^
fi
->
( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
)
means
:: ORDINAL3:def 3
(
dom
it
: ( ( ) ( )
Element
of
K10
(
C
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
=
dom
fi
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) : ( ( ) ( )
set
) & ( for
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
dom
fi
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) : ( ( ) ( )
set
) holds
it
: ( ( ) ( )
Element
of
K10
(
C
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
.
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( ( ) ( )
set
)
=
C
: ( ( ) ( )
set
)
*^
(
fi
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
.
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( ( ) ( )
set
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ) );
func
fi
*^
C
->
( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
)
means
:: ORDINAL3:def 4
(
dom
it
: ( ( ) ( )
Element
of
K10
(
C
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
=
dom
fi
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) : ( ( ) ( )
set
) & ( for
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
dom
fi
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) : ( ( ) ( )
set
) holds
it
: ( ( ) ( )
Element
of
K10
(
C
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
.
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( ( ) ( )
set
)
=
(
fi
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
.
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( ( ) ( )
set
)
*^
C
: ( ( ) ( )
set
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ) );
end;
theorem
:: ORDINAL3:39
for
fi
,
psi
being ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
)
for
C
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
)
<>
dom
fi
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) &
dom
fi
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
dom
psi
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) & ( for
A
,
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
dom
fi
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) &
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
fi
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
)
.
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) holds
psi
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
)
.
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ) holds
sup
psi
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
(
sup
fi
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ;
theorem
:: ORDINAL3:40
for
A
,
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) is
limit_ordinal
holds
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) is
limit_ordinal
;
theorem
:: ORDINAL3:41
for
A
,
B
,
C
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) &
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) is
limit_ordinal
holds
ex
D
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
(
D
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) &
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
D
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ) ;
theorem
:: ORDINAL3:42
for
fi
,
psi
being ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
)
for
C
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
dom
fi
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
dom
psi
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) &
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
<>
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) &
sup
fi
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) is
limit_ordinal
& ( for
A
,
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
dom
fi
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) &
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
fi
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
)
.
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) holds
psi
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
)
.
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ) holds
sup
psi
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
(
sup
fi
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
*^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ;
theorem
:: ORDINAL3:43
for
fi
being ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
)
for
C
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
)
<>
dom
fi
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) holds
sup
(
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
fi
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
)
)
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
(
sup
fi
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ;
theorem
:: ORDINAL3:44
for
fi
being ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
)
for
C
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
)
<>
dom
fi
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) &
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
<>
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) &
sup
fi
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) is
limit_ordinal
holds
sup
(
fi
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
)
*^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
(
sup
fi
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
*^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ;
theorem
:: ORDINAL3:45
for
B
,
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
<>
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) holds
union
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
(
union
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ;
theorem
:: ORDINAL3:46
for
A
,
B
,
C
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
*^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
+^
(
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ;
theorem
:: ORDINAL3:47
for
A
,
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
<>
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) holds
ex
C
,
D
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
(
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
(
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
+^
D
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) &
D
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ) ;
theorem
:: ORDINAL3:48
for
A
,
C1
,
D1
,
C2
,
D2
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
(
C1
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
+^
D1
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
(
C2
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
+^
D2
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) &
D1
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) &
D2
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
(
C1
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
C2
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) &
D1
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
D2
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ) ;
theorem
:: ORDINAL3:49
for
B
,
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st 1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
)
Element
of
omega
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
set
) )
in
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) &
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
<>
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) &
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) is
limit_ordinal
holds
for
fi
being ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
) st
dom
fi
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) & ( for
C
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
fi
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
)
.
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ) holds
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
sup
fi
: ( (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
) (
T-Sequence-like
Relation-like
Function-like
Ordinal-yielding
)
Ordinal-Sequence
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ;
theorem
:: ORDINAL3:50
for
A
,
B
,
C
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
*^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
=
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
(
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ;
definition
let
A
,
B
be ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ;
func
A
-^
B
->
( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
means
:: ORDINAL3:def 5
A
: ( ( ) ( )
set
)
=
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
+^
it
: ( ( ) ( )
Element
of
K10
(
A
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
if
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
c=
A
: ( ( ) ( )
set
)
otherwise
it
: ( ( ) ( )
Element
of
K10
(
A
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
=
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) ;
func
A
div^
B
->
( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
means
:: ORDINAL3:def 6
ex
C
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
(
A
: ( ( ) ( )
set
)
=
(
it
: ( ( ) ( )
Element
of
K10
(
A
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
*^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
+^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) &
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) )
if
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
<>
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
)
otherwise
it
: ( ( ) ( )
Element
of
K10
(
A
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
=
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) ;
end;
definition
let
A
,
B
be ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ;
func
A
mod^
B
->
( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
equals
:: ORDINAL3:def 7
A
: ( ( ) ( )
set
)
-^
(
(
A
: ( ( ) ( )
set
)
div^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ;
end;
theorem
:: ORDINAL3:51
for
A
,
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
(
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
-^
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ;
theorem
:: ORDINAL3:52
for
A
,
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
-^
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ;
theorem
:: ORDINAL3:53
for
A
,
B
,
C
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) & (
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
c=
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) or
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ) holds
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
-^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
-^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ;
theorem
:: ORDINAL3:54
for
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
-^
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) ;
theorem
:: ORDINAL3:55
for
A
,
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
(
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
-^
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
<>
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) &
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
)
in
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
-^
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ) ;
theorem
:: ORDINAL3:56
for
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
-^
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) &
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
)
-^
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) ) ;
theorem
:: ORDINAL3:57
for
A
,
B
,
C
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
-^
(
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
-^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
-^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ;
theorem
:: ORDINAL3:58
for
A
,
B
,
C
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
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
-^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
c=
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
-^
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ;
theorem
:: ORDINAL3:59
for
A
,
B
,
C
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
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
-^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
c=
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
-^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ;
theorem
:: ORDINAL3:60
for
C
,
A
,
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
<>
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) &
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) holds
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
-^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ;
theorem
:: ORDINAL3:61
for
A
,
B
,
C
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
in
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
-^
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ;
theorem
:: ORDINAL3:62
for
A
,
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
c=
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
-^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ;
theorem
:: ORDINAL3:63
for
A
,
C
,
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
-^
(
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
-^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ;
theorem
:: ORDINAL3:64
for
A
,
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
div^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
c=
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ;
theorem
:: ORDINAL3:65
for
A
,
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
(
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
div^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
+^
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
mod^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ;
theorem
:: ORDINAL3:66
for
A
,
B
,
C
,
D
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
(
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
+^
D
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) &
D
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
(
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
div^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) &
D
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
mod^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ) ;
theorem
:: ORDINAL3:67
for
A
,
B
,
C
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) holds
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
div^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) &
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
mod^
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
C
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ) ;
theorem
:: ORDINAL3:68
for
B
,
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
<>
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) holds
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
div^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ;
theorem
:: ORDINAL3:69
for
A
,
B
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
)
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
mod^
B
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) ;
theorem
:: ORDINAL3:70
for
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
(
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
)
div^
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) &
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
)
mod^
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) &
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
mod^
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) ) ;
theorem
:: ORDINAL3:71
for
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
(
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
div^
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
)
Element
of
omega
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
set
) ) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) &
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
mod^
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
)
Element
of
omega
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
set
) ) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
=
{}
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
)
set
) ) ;
begin
theorem
:: ORDINAL3:72
for
X
being ( ( ) ( )
set
) holds
sup
X
: ( ( ) ( )
set
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
c=
succ
(
union
(
On
X
: ( ( ) ( )
set
)
)
: ( ( ) ( )
set
)
)
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ;
theorem
:: ORDINAL3:73
for
A
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) holds
succ
A
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
set
)
is_cofinal_with
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
)
Element
of
omega
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
set
) ) ;
theorem
:: ORDINAL3:74
for
a
,
b
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
a
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
+^
b
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) is
natural
holds
(
a
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
omega
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
set
) &
b
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
omega
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
set
) ) ;
registration
let
a
,
b
be ( (
ordinal
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
)
Ordinal
) ;
cluster
a
: ( (
ordinal
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
)
set
)
-^
b
: ( (
ordinal
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
)
set
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
->
ordinal
natural
;
cluster
a
: ( (
ordinal
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
)
set
)
*^
b
: ( (
ordinal
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
)
set
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
)
->
ordinal
natural
;
end;
theorem
:: ORDINAL3:75
for
a
,
b
being ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) st
a
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
b
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) is
natural
& not
a
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
*^
b
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) is
empty
holds
(
a
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
omega
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
set
) &
b
: ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
Ordinal
)
in
omega
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
set
) ) ;
definition
let
a
,
b
be ( (
ordinal
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
)
Ordinal
) ;
:: original:
+^
redefine
func
a
+^
b
->
( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ;
commutativity
for
a
,
b
being ( (
ordinal
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
)
Ordinal
) holds
a
: ( (
ordinal
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
)
set
)
+^
b
: ( (
ordinal
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
)
set
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
natural
)
set
)
=
b
: ( (
ordinal
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
)
set
)
+^
a
: ( (
ordinal
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
)
set
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
natural
)
set
)
;
end;
definition
let
a
,
b
be ( (
ordinal
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
)
Ordinal
) ;
:: original:
*^
redefine
func
a
*^
b
->
( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
)
set
) ;
commutativity
for
a
,
b
being ( (
ordinal
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
)
Ordinal
) holds
a
: ( (
ordinal
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
)
set
)
*^
b
: ( (
ordinal
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
)
set
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
natural
)
set
)
=
b
: ( (
ordinal
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
)
set
)
*^
a
: ( (
ordinal
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
)
set
) : ( (
ordinal
) (
epsilon-transitive
epsilon-connected
ordinal
natural
)
set
)
;
end;