REAL is set
NAT is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal limit_cardinal countable denumerable Element of bool REAL
bool REAL is set
NAT is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal limit_cardinal countable denumerable set
bool NAT is non empty non finite set
{} is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty finite cardinal {} -element countable set
1 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable Element of NAT
Rank {} is epsilon-transitive set
card {} is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty finite cardinal {} -element countable set
2 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal countable Element of NAT
0 is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty finite cardinal {} -element countable Element of NAT
union {} is epsilon-transitive epsilon-connected ordinal set
dom {} is set
rng {} is set
M is epsilon-transitive epsilon-connected ordinal set
M is epsilon-transitive epsilon-connected ordinal set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set
card M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set
the epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non limit_cardinal non countable regular set is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non limit_cardinal non countable regular set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
bool M is non empty non finite set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
bool M is non empty non finite set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
bool M is non empty non finite set
X is Element of bool M
sup X is epsilon-transitive epsilon-connected ordinal set
R is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
X /\ R is Element of bool M
sup (X /\ R) is epsilon-transitive epsilon-connected ordinal set
sup X is epsilon-transitive epsilon-connected ordinal set
R is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
X /\ R is Element of bool M
sup (X /\ R) is epsilon-transitive epsilon-connected ordinal set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
bool M is non empty non finite set
X is Element of bool M
sup X is epsilon-transitive epsilon-connected ordinal set
R is set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
bool M is non empty non finite set
X is Element of bool M
sup X is epsilon-transitive epsilon-connected ordinal set
R is epsilon-transitive epsilon-connected ordinal set
succ R is epsilon-transitive epsilon-connected ordinal non empty set
{R} is non empty trivial 1 -element set
R \/ {R} is non empty set
X1 is epsilon-transitive epsilon-connected ordinal set
RANKS is epsilon-transitive epsilon-connected ordinal set
X1 is set
R is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
bool M is non empty non finite set
X is Element of bool M
sup X is epsilon-transitive epsilon-connected ordinal set
sup M is epsilon-transitive epsilon-connected ordinal set
R is epsilon-transitive epsilon-connected ordinal set
sup R is epsilon-transitive epsilon-connected ordinal set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
bool M is non empty non finite set
X is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
R is Element of bool M
R /\ X is Element of bool M
sup (R /\ X) is epsilon-transitive epsilon-connected ordinal set
bool X is non empty non finite set
X1 is Element of bool X
RANKS is epsilon-transitive epsilon-connected ordinal set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
bool M is non empty non finite set
X is Element of bool M
R is epsilon-transitive epsilon-connected ordinal set
X1 is set
RANKS is epsilon-transitive epsilon-connected ordinal Element of M
R is epsilon-transitive epsilon-connected ordinal set
X1 is epsilon-transitive epsilon-connected ordinal set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
bool M is non empty non finite set
X is Element of bool M
the epsilon-transitive epsilon-connected ordinal Element of M is epsilon-transitive epsilon-connected ordinal Element of M
X1 is epsilon-transitive epsilon-connected ordinal set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
bool M is non empty non finite set
X is epsilon-transitive epsilon-connected ordinal set
R is Element of bool M
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : ( b1 in R & X in b1 ) } is set
succ X is epsilon-transitive epsilon-connected ordinal non empty set
{X} is non empty trivial 1 -element set
X \/ {X} is non empty set
X1 is epsilon-transitive epsilon-connected ordinal set
RANKS is epsilon-transitive epsilon-connected ordinal Element of M
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
bool M is non empty non finite set
X is Element of bool M
R is epsilon-transitive epsilon-connected ordinal set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : ( b1 in X & R in b1 ) } is set
inf { b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : ( b1 in X & R in b1 ) } is epsilon-transitive epsilon-connected ordinal set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : S1[b1] } is set
inf { b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : S1[b1] } is epsilon-transitive epsilon-connected ordinal set
RANKS is epsilon-transitive epsilon-connected ordinal Element of M
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
bool M is non empty non finite set
X is epsilon-transitive epsilon-connected ordinal set
R is Element of bool M
(M,R,X) is Element of R
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : S1[b1] } is set
RANKS is set
inf { b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : S1[b1] } is epsilon-transitive epsilon-connected ordinal set
On { b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : S1[b1] } is set
meet (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : S1[b1] } ) is set
meet { b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : S1[b1] } is set
RANKS is epsilon-transitive epsilon-connected ordinal Element of M
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
[#] M is Element of bool M
bool M is non empty non finite set
X is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
([#] M) /\ X is Element of bool M
sup (([#] M) /\ X) is epsilon-transitive epsilon-connected ordinal set
sup ([#] M) is epsilon-transitive epsilon-connected ordinal set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
bool M is non empty non finite set
X is epsilon-transitive epsilon-connected ordinal set
R is Element of bool M
R \ X is Element of bool M
X1 is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
(R \ X) /\ X1 is Element of bool M
sup ((R \ X) /\ X1) is epsilon-transitive epsilon-connected ordinal set
R /\ X1 is Element of bool M
sup (R /\ X1) is epsilon-transitive epsilon-connected ordinal set
sup X1 is epsilon-transitive epsilon-connected ordinal set
R \ X1 is Element of bool M
X1 is epsilon-transitive epsilon-connected ordinal set
RANKS is epsilon-transitive epsilon-connected ordinal set
RANKS is epsilon-transitive epsilon-connected ordinal set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
X is epsilon-transitive epsilon-connected ordinal set
M \ X is Element of bool M
bool M is non empty non finite set
[#] M is Element of bool M
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
bool M is non empty non finite set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
bool M is non empty non finite set
X is Element of bool M
R is Element of bool M
X1 is Element of bool M
R /\ X1 is Element of bool M
X /\ X1 is Element of bool M
RANKS is set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
X is set
R is set
bool M is non empty non finite set
RANKS1 is Element of bool M
X /\ RANKS1 is Element of bool M
X1 is Element of bool M
RANKS is Element of bool M
RANKS1 is Element of bool M
RANKS /\ RANKS1 is Element of bool M
M is set
bool M is set
bool (bool M) is set
X is Element of bool (bool M)
R is Element of X
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
bool M is non empty non finite set
X is Element of bool M
R is epsilon-transitive epsilon-connected ordinal set
M \ R is Element of bool M
(M \ R) /\ X is Element of bool M
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
bool M is non empty non finite set
X is Element of bool M
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : ( not b1 is finite & b1 is limit_ordinal & sup (X /\ b1) = b1 ) } is set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : S1[b1] } is set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
bool M is non empty non finite set
X is epsilon-transitive epsilon-connected ordinal set
R is epsilon-transitive epsilon-connected ordinal set
succ R is epsilon-transitive epsilon-connected ordinal non empty set
{R} is non empty trivial 1 -element set
R \/ {R} is non empty set
X1 is Element of bool M
X1 /\ X is Element of bool M
(M,X1) is Element of bool M
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : ( not b1 is finite & b1 is limit_ordinal & sup (X1 /\ b1) = b1 ) } is set
X /\ (M,X1) is Element of bool M
RANKS is set
RANKS1 is epsilon-transitive epsilon-connected ordinal Element of X
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : S1[b1] } is set
X1 /\ RANKS1 is Element of bool M
sup (X1 /\ RANKS1) is epsilon-transitive epsilon-connected ordinal set
N1 is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
bool N1 is non empty non finite set
X1 /\ N1 is Element of bool M
x is Element of bool N1
C is epsilon-transitive epsilon-connected ordinal set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
bool M is non empty non finite set
X is epsilon-transitive epsilon-connected ordinal set
succ X is epsilon-transitive epsilon-connected ordinal non empty set
{X} is non empty trivial 1 -element set
X \/ {X} is non empty set
R is Element of bool M
(M,R) is Element of bool M
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : ( not b1 is finite & b1 is limit_ordinal & sup (R /\ b1) = b1 ) } is set
R /\ M is Element of bool M
M /\ (M,R) is Element of bool M
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
bool M is non empty non finite set
X is Element of bool M
(M,X) is Element of bool M
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : ( not b1 is finite & b1 is limit_ordinal & sup (X /\ b1) = b1 ) } is set
R is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
(M,X) /\ R is Element of bool M
sup ((M,X) /\ R) is epsilon-transitive epsilon-connected ordinal set
X /\ R is Element of bool M
sup (X /\ R) is epsilon-transitive epsilon-connected ordinal set
RANKS is epsilon-transitive epsilon-connected ordinal set
succ RANKS is epsilon-transitive epsilon-connected ordinal non empty set
{RANKS} is non empty trivial 1 -element set
RANKS \/ {RANKS} is non empty set
sup (succ RANKS) is epsilon-transitive epsilon-connected ordinal set
X1 is epsilon-transitive epsilon-connected ordinal Element of M
X /\ X1 is Element of bool M
sup (X /\ X1) is epsilon-transitive epsilon-connected ordinal set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
bool M is non empty non finite set
X is Element of bool M
(M,X) is Element of bool M
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : ( not b1 is finite & b1 is limit_ordinal & sup (X /\ b1) = b1 ) } is set
R is epsilon-transitive epsilon-connected ordinal set
{ (succ b1) where b1 is epsilon-transitive epsilon-connected ordinal Element of M : ( b1 in X & R in succ b1 ) } is set
RANKS is set
RANKS1 is epsilon-transitive epsilon-connected ordinal Element of M
succ RANKS1 is epsilon-transitive epsilon-connected ordinal non empty set
{RANKS1} is non empty trivial 1 -element set
RANKS1 \/ {RANKS1} is non empty set
RANKS is Element of bool M
RANKS1 is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
RANKS /\ RANKS1 is Element of bool M
sup (RANKS /\ RANKS1) is epsilon-transitive epsilon-connected ordinal set
the epsilon-transitive epsilon-connected ordinal Element of RANKS1 is epsilon-transitive epsilon-connected ordinal Element of RANKS1
C is epsilon-transitive epsilon-connected ordinal set
X /\ RANKS1 is Element of bool M
sup (X /\ RANKS1) is epsilon-transitive epsilon-connected ordinal set
B5 is epsilon-transitive epsilon-connected ordinal set
succ B5 is epsilon-transitive epsilon-connected ordinal non empty set
{B5} is non empty trivial 1 -element set
B5 \/ {B5} is non empty set
succ (succ B5) is epsilon-transitive epsilon-connected ordinal non empty set
{(succ B5)} is non empty trivial 1 -element set
(succ B5) \/ {(succ B5)} is non empty set
B6 is epsilon-transitive epsilon-connected ordinal set
C3 is epsilon-transitive epsilon-connected ordinal Element of M
succ C3 is epsilon-transitive epsilon-connected ordinal non empty set
{C3} is non empty trivial 1 -element set
C3 \/ {C3} is non empty set
N1 is epsilon-transitive epsilon-connected ordinal Element of M
B5 is epsilon-transitive epsilon-connected ordinal Element of M
succ B5 is epsilon-transitive epsilon-connected ordinal non empty set
{B5} is non empty trivial 1 -element set
B5 \/ {B5} is non empty set
RANKS1 is epsilon-transitive epsilon-connected ordinal set
RANKS1 \/ R is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal set
succ x is epsilon-transitive epsilon-connected ordinal non empty set
{x} is non empty trivial 1 -element set
x \/ {x} is non empty set
sup RANKS is epsilon-transitive epsilon-connected ordinal set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set
bool M is non empty non finite set
cf M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set
X is Element of bool M
card X is epsilon-transitive epsilon-connected ordinal cardinal set
sup X is epsilon-transitive epsilon-connected ordinal set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set
bool M is non empty non finite set
bool (bool M) is non empty non finite set
X is Element of bool (bool M)
meet X is Element of bool M
R is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
(meet X) /\ R is Element of bool M
sup ((meet X) /\ R) is epsilon-transitive epsilon-connected ordinal set
X1 is set
RANKS is (M,X)
RANKS /\ R is Element of bool M
sup (RANKS /\ R) is epsilon-transitive epsilon-connected ordinal set
sup R is epsilon-transitive epsilon-connected ordinal set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set
bool M is non empty non finite set
cf M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set
X is Element of bool M
[:NAT,X:] is set
bool [:NAT,X:] is set
R is Relation-like NAT -defined X -valued Function-like V32( NAT ,X) Element of bool [:NAT,X:]
rng R is set
sup (rng R) is epsilon-transitive epsilon-connected ordinal set
card NAT is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set
dom R is set
card (rng R) is epsilon-transitive epsilon-connected ordinal cardinal set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set
cf M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set
bool M is non empty non finite set
bool (bool M) is non empty non finite set
X is non empty Element of bool (bool M)
card X is epsilon-transitive epsilon-connected ordinal non empty cardinal set
meet X is Element of bool M
R is epsilon-transitive epsilon-connected ordinal set
{ (M,b1,a1) where b1 is (M,X) : b1 in X } is set
[#] M is Element of bool M
{ (M,b1,a1) where b1 is (M,X) : b1 in X } /\ ([#] M) is Element of bool M
{ (M,b1,a2) where b1 is (M,X) : b1 in X } is set
{ (M,b1,a2) where b1 is (M,X) : b1 in X } /\ ([#] M) is Element of bool M
RANKS is epsilon-transitive epsilon-connected ordinal Element of M
{ (M,b1,RANKS) where b1 is (M,X) : b1 in X } is set
{ (M,b1,RANKS) where b1 is (M,X) : b1 in X } /\ ([#] M) is Element of bool M
N1 is set
x is (M,X)
(M,x,RANKS) is Element of x
RANKS is epsilon-transitive epsilon-connected ordinal Element of M
{ (M,b1,RANKS) where b1 is (M,X) : b1 in X } is set
{ (M,b1,RANKS) where b1 is (M,X) : b1 in X } /\ ([#] M) is Element of bool M
sup H1(RANKS) is epsilon-transitive epsilon-connected ordinal set
{ H2(b1) where b1 is (M,X) : b1 in X } is set
card { H2(b1) where b1 is (M,X) : b1 in X } is epsilon-transitive epsilon-connected ordinal cardinal set
card H1(RANKS) is epsilon-transitive epsilon-connected ordinal cardinal set
the (M,X) is (M,X)
(M, the (M,X),RANKS) is Element of the (M,X)
N1 is epsilon-transitive epsilon-connected ordinal Element of M
RANKS is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable Element of NAT
RANKS1 is epsilon-transitive epsilon-connected ordinal Element of M
{ (M,b1,RANKS1) where b1 is (M,X) : b1 in X } is set
{ (M,b1,RANKS1) where b1 is (M,X) : b1 in X } /\ ([#] M) is Element of bool M
sup H1(RANKS1) is epsilon-transitive epsilon-connected ordinal set
N1 is epsilon-transitive epsilon-connected ordinal Element of M
[:NAT,M:] is non empty non finite set
bool [:NAT,M:] is non empty non finite set
X1 is epsilon-transitive epsilon-connected ordinal Element of M
RANKS is Relation-like NAT -defined M -valued Function-like V32( NAT ,M) Element of bool [:NAT,M:]
RANKS . 0 is epsilon-transitive epsilon-connected ordinal Element of M
[:NAT,([#] M):] is set
bool [:NAT,([#] M):] is set
rng RANKS is set
sup (rng RANKS) is epsilon-transitive epsilon-connected ordinal set
N1 is Element of bool M
x is epsilon-transitive epsilon-connected ordinal set
dom RANKS is set
C is set
RANKS . C is set
B5 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable Element of NAT
B5 + 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable Element of NAT
RANKS . (B5 + 1) is epsilon-transitive epsilon-connected ordinal Element of M
B6 is epsilon-transitive epsilon-connected ordinal set
RANKS1 is Relation-like NAT -defined [#] M -valued Function-like V32( NAT , [#] M) Element of bool [:NAT,([#] M):]
rng RANKS1 is set
sup (rng RANKS1) is epsilon-transitive epsilon-connected ordinal set
sup N1 is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite Element of M
C is set
B5 is (M,X)
B5 /\ x is Element of bool M
sup (B5 /\ x) is epsilon-transitive epsilon-connected ordinal set
sup x is epsilon-transitive epsilon-connected ordinal set
B6 is epsilon-transitive epsilon-connected ordinal set
dom RANKS is set
C3 is set
RANKS . C3 is set
c13 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable Element of NAT
RANKS . c13 is epsilon-transitive epsilon-connected ordinal Element of M
(M,B5,(RANKS . c13)) is Element of B5
{ (M,b1,(RANKS . c13)) where b1 is (M,X) : b1 in X } is set
{ (M,b1,(RANKS . c13)) where b1 is (M,X) : b1 in X } /\ ([#] M) is Element of bool M
LBY is epsilon-transitive epsilon-connected ordinal Element of M
sup H1(RANKS . c13) is epsilon-transitive epsilon-connected ordinal set
c13 + 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable Element of NAT
RANKS . (c13 + 1) is epsilon-transitive epsilon-connected ordinal Element of M
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set
bool M is non empty non finite set
cf M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set
X is Element of bool M
(M,X) is Element of bool M
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : ( not b1 is finite & b1 is limit_ordinal & sup (X /\ b1) = b1 ) } is set
X1 is epsilon-transitive epsilon-connected ordinal set
R is non empty Element of bool M
(M,R,X1) is Element of R
RANKS1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable Element of NAT
N1 is Element of R
x is epsilon-transitive epsilon-connected ordinal Element of M
succ x is epsilon-transitive epsilon-connected ordinal non empty set
{x} is non empty trivial 1 -element set
x \/ {x} is non empty set
C is epsilon-transitive epsilon-connected ordinal set
B5 is Element of R
[:NAT,R:] is non empty non finite set
bool [:NAT,R:] is non empty non finite set
RANKS is Element of R
RANKS1 is Relation-like NAT -defined R -valued Function-like V32( NAT ,R) Element of bool [:NAT,R:]
RANKS1 . 0 is Element of R
dom RANKS1 is set
rng RANKS1 is set
x is epsilon-transitive epsilon-connected ordinal Element of M
sup (rng RANKS1) is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
B5 is set
RANKS1 . B5 is set
B6 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable Element of NAT
B6 + 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable Element of NAT
RANKS1 . (B6 + 1) is Element of R
C3 is epsilon-transitive epsilon-connected ordinal Element of M
C is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite Element of M
X /\ C is Element of bool M
sup (X /\ C) is epsilon-transitive epsilon-connected ordinal set
B5 is epsilon-transitive epsilon-connected ordinal set
B6 is epsilon-transitive epsilon-connected ordinal set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set
bool M is non empty non finite set
cf M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set
X is Element of bool M
(M,X) is Element of bool M
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : ( not b1 is finite & b1 is limit_ordinal & sup (X /\ b1) = b1 ) } is set
R is epsilon-transitive epsilon-connected ordinal set
X1 is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal Element of M : b1 is strongly_inaccessible } is set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal Element of M : b1 is regular } is set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set
cf M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal Element of M : b1 is regular } is set
X is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom X is epsilon-transitive epsilon-connected ordinal set
rng X is set
sup X is epsilon-transitive epsilon-connected ordinal set
bool M is non empty non finite set
R is Element of bool M
card R is epsilon-transitive epsilon-connected ordinal cardinal set
card (cf M) is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set
sup R is epsilon-transitive epsilon-connected ordinal set
(M,R) is Element of bool M
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : ( not b1 is finite & b1 is limit_ordinal & sup (R /\ b1) = b1 ) } is set
X1 is epsilon-transitive epsilon-connected ordinal set
{ (succ b1) where b1 is epsilon-transitive epsilon-connected ordinal Element of M : ( b1 in R & X1 in succ b1 ) } is set
RANKS1 is Element of bool M
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal Element of M : b1 is regular } /\ RANKS1 is Element of bool M
RANKS1 /\ { b1 where b1 is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal Element of M : b1 is regular } is Element of bool M
N1 is set
x is epsilon-transitive epsilon-connected ordinal Element of M
succ x is epsilon-transitive epsilon-connected ordinal non empty set
{x} is non empty trivial 1 -element set
x \/ {x} is non empty set
C is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal Element of M
succ (cf M) is epsilon-transitive epsilon-connected ordinal non empty set
{(cf M)} is non empty trivial 1 -element set
(cf M) \/ {(cf M)} is non empty set
(M,R) \ (succ (cf M)) is Element of bool M
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal Element of M : b1 is regular } /\ ((M,R) \ (succ (cf M))) is Element of bool M
((M,R) \ (succ (cf M))) /\ { b1 where b1 is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal Element of M : b1 is regular } is Element of bool M
X1 is set
RANKS is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal Element of M
bool RANKS is non empty non finite set
RANKS /\ R is Element of bool M
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of M : S1[b1] } is set
R /\ RANKS is Element of bool M
sup (R /\ RANKS) is epsilon-transitive epsilon-connected ordinal set
RANKS1 is Element of bool RANKS
cf RANKS is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set
card RANKS1 is epsilon-transitive epsilon-connected ordinal cardinal set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal Element of M : b1 is regular } is set
bool M is non empty non finite set
R is epsilon-transitive epsilon-connected ordinal cardinal set
nextcard R is epsilon-transitive epsilon-connected ordinal cardinal set
succ R is epsilon-transitive epsilon-connected ordinal non empty set
{R} is non empty trivial 1 -element set
R \/ {R} is non empty set
M \ (succ R) is Element of bool M
X is Element of bool M
X /\ (M \ (succ R)) is Element of bool M
X1 is set
RANKS is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal Element of M
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal Element of M : b1 is strongly_inaccessible } is set
bool M is non empty non finite set
R is epsilon-transitive epsilon-connected ordinal cardinal set
exp (2,R) is epsilon-transitive epsilon-connected ordinal cardinal set
succ R is epsilon-transitive epsilon-connected ordinal non empty set
{R} is non empty trivial 1 -element set
R \/ {R} is non empty set
M \ (succ R) is Element of bool M
X is Element of bool M
X /\ (M \ (succ R)) is Element of bool M
X1 is set
RANKS is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal Element of M
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set
M is set
union M is set
X is set
R is set
X1 is set
RANKS is epsilon-transitive epsilon-connected ordinal cardinal set
X is epsilon-transitive epsilon-connected ordinal set
card X is epsilon-transitive epsilon-connected ordinal cardinal set
R is set
X1 is epsilon-transitive epsilon-connected ordinal set
RANKS is set
RANKS1 is set
N1 is epsilon-transitive epsilon-connected ordinal cardinal set
card N1 is epsilon-transitive epsilon-connected ordinal cardinal set
M is set
card M is epsilon-transitive epsilon-connected ordinal cardinal set
union M is set
card (union M) is epsilon-transitive epsilon-connected ordinal cardinal set
X is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set
cf X is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set
R is non empty set
{ H1(b1) where b1 is Element of R : b1 in R } is set
card { H1(b1) where b1 is Element of R : b1 in R } is epsilon-transitive epsilon-connected ordinal cardinal set
card R is epsilon-transitive epsilon-connected ordinal non empty cardinal set
RANKS is set
RANKS1 is Element of R
card RANKS1 is epsilon-transitive epsilon-connected ordinal cardinal set
RANKS is set
union { H1(b1) where b1 is Element of R : b1 in R } is set
RANKS1 is set
RANKS is epsilon-transitive epsilon-connected ordinal cardinal set
(card R) *` RANKS is epsilon-transitive epsilon-connected ordinal cardinal set
(cf X) *` X is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set
RANKS1 is set
card RANKS1 is epsilon-transitive epsilon-connected ordinal cardinal set
union R is set
card (union R) is epsilon-transitive epsilon-connected ordinal cardinal set
X *` X is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set
X is epsilon-transitive epsilon-connected ordinal set
Rank X is epsilon-transitive set
card (Rank X) is epsilon-transitive epsilon-connected ordinal cardinal set
R is epsilon-transitive epsilon-connected ordinal set
Rank R is epsilon-transitive set
card (Rank R) is epsilon-transitive epsilon-connected ordinal cardinal set
succ R is epsilon-transitive epsilon-connected ordinal non empty set
{R} is non empty trivial 1 -element set
R \/ {R} is non empty set
Rank (succ R) is epsilon-transitive set
card (Rank (succ R)) is epsilon-transitive epsilon-connected ordinal cardinal set
exp (2,(card (Rank R))) is epsilon-transitive epsilon-connected ordinal cardinal set
bool (Rank R) is Element of bool (bool (Rank R))
bool (Rank R) is set
bool (bool (Rank R)) is set
cf M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set
R is epsilon-transitive epsilon-connected ordinal set
Rank R is epsilon-transitive set
card (Rank R) is epsilon-transitive epsilon-connected ordinal cardinal set
X1 is Relation-like T-Sequence-like Function-like set
dom X1 is epsilon-transitive epsilon-connected ordinal set
rng X1 is set
card (rng X1) is epsilon-transitive epsilon-connected ordinal cardinal set
card R is epsilon-transitive epsilon-connected ordinal cardinal set
RANKS is set
card RANKS is epsilon-transitive epsilon-connected ordinal cardinal set
RANKS1 is set
X1 . RANKS1 is set
N1 is epsilon-transitive epsilon-connected ordinal Element of R
Rank N1 is epsilon-transitive set
Union X1 is set
union (rng X1) is set
card (Rank {}) is epsilon-transitive epsilon-connected ordinal cardinal set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set
Rank M is epsilon-transitive set
card (Rank M) is epsilon-transitive epsilon-connected ordinal cardinal set
X is Relation-like T-Sequence-like Function-like set
dom X is epsilon-transitive epsilon-connected ordinal set
rng X is set
R is set
X1 is set
RANKS is set
X . RANKS is set
RANKS1 is set
X . RANKS1 is set
x is epsilon-transitive epsilon-connected ordinal set
Rank x is epsilon-transitive set
N1 is epsilon-transitive epsilon-connected ordinal set
Rank N1 is epsilon-transitive set
card M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set
Union X is set
union (rng X) is set
R is set
X1 is set
X . X1 is set
RANKS is epsilon-transitive epsilon-connected ordinal set
Rank RANKS is epsilon-transitive set
card (Rank RANKS) is epsilon-transitive epsilon-connected ordinal cardinal set
card R is epsilon-transitive epsilon-connected ordinal cardinal set
card (union (rng X)) is epsilon-transitive epsilon-connected ordinal cardinal set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set
Rank M is epsilon-transitive set
X is set
R is set
X is set
bool X is Element of bool (bool X)
bool X is set
bool (bool X) is set
R is epsilon-transitive epsilon-connected ordinal set
Rank R is epsilon-transitive set
succ R is epsilon-transitive epsilon-connected ordinal non empty set
{R} is non empty trivial 1 -element set
R \/ {R} is non empty set
Rank (succ R) is epsilon-transitive set
cf M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal set
X is set
card X is epsilon-transitive epsilon-connected ordinal cardinal set
the_rank_of X is epsilon-transitive epsilon-connected ordinal set
card (Rank M) is epsilon-transitive epsilon-connected ordinal cardinal set
X1 is non empty set
{ H2(b1) where b1 is Element of X1 : b1 in X1 } is set
RANKS1 is set
RANKS1 is set
N1 is Element of X1
the_rank_of N1 is epsilon-transitive epsilon-connected ordinal set
bool M is non empty non finite set
N1 is epsilon-transitive epsilon-connected ordinal set
x is set
the_rank_of x is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
RANKS1 is Element of bool M
card RANKS1 is epsilon-transitive epsilon-connected ordinal cardinal set
card { H2(b1) where b1 is Element of X1 : b1 in X1 } is epsilon-transitive epsilon-connected ordinal cardinal set
card X1 is epsilon-transitive epsilon-connected ordinal non empty cardinal set
N1 is epsilon-transitive epsilon-connected ordinal set
N1 is epsilon-transitive epsilon-connected ordinal set
M is epsilon-transitive epsilon-connected ordinal non empty set
Rank M is epsilon-transitive set
M is epsilon-transitive epsilon-connected ordinal non empty set
Rank M is epsilon-transitive set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non finite cardinal non countable set
Rank M is epsilon-transitive non empty set