:: RAMSEY_1 semantic presentation

REAL is V129() V130() V131() V135() set
NAT is epsilon-transitive epsilon-connected ordinal non empty V14() non finite cardinal limit_cardinal V129() V130() V131() V132() V133() V134() V135() V143() V144() Element of K26(REAL)
K26(REAL) is non empty set
COMPLEX is V129() V135() set
omega is epsilon-transitive epsilon-connected ordinal non empty V14() non finite cardinal limit_cardinal V129() V130() V131() V132() V133() V134() V135() V143() V144() set
K26(omega) is non empty V14() non finite set
K26(NAT) is non empty V14() non finite set
RAT is V129() V130() V131() V132() V135() set
INT is V129() V130() V131() V132() V133() V135() set
K27(REAL,REAL) is Relation-like set
K26(K27(REAL,REAL)) is non empty set
{} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V16() V17() Function-like one-to-one constant functional finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V129() V130() V131() V132() V133() V134() V135() V140() V143() set
1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
2 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
3 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
len {} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V16() V17() Function-like one-to-one constant functional finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V129() V130() V131() V132() V133() V134() V135() V140() V143() set
len omega is epsilon-transitive epsilon-connected ordinal non empty V14() non finite cardinal set
0 is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V16() V17() V18() Function-like one-to-one constant functional finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V118() V129() V130() V131() V132() V133() V134() V135() V140() V143() Element of NAT
Seg 1 is non empty V14() finite 1 -element V129() V130() V131() V132() V133() V134() V143() Element of K26(NAT)
{1} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
Seg 2 is non empty finite 2 -element V129() V130() V131() V132() V133() V134() V143() Element of K26(NAT)
{1,2} is non empty finite V36() V129() V130() V131() V132() V133() V134() V143() set
m is set
K26(m) is non empty set
r is set
the_subsets_of_card (r,m) is Element of K26(K26(m))
K26(K26(m)) is non empty set
{ b₁ where b₁ is Element of K26(m) : len b₁ = r } is set
r is V14() non finite set
m is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
the_subsets_of_card (m,r) is Element of K26(K26(r))
K26(r) is non empty V14() non finite set
K26(K26(r)) is non empty V14() non finite set
{ b₁ where b₁ is Element of K26(r) : len b₁ = m } is set
len r is epsilon-transitive epsilon-connected ordinal V14() non finite cardinal set
card m is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
r is set
X is set
K27(r,X) is Relation-like set
K26(K27(r,X)) is non empty set
P is Relation-like r -defined X -valued Function-like quasi_total Element of K26(K27(r,X))
m is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
card m is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
len r is epsilon-transitive epsilon-connected ordinal cardinal set
the_subsets_of_card (m,r) is Element of K26(K26(r))
K26(r) is non empty set
K26(K26(r)) is non empty set
{ b₁ where b₁ is Element of K26(r) : len b₁ = m } is set
the_subsets_of_card (m,X) is Element of K26(K26(X))
K26(X) is non empty set
K26(K26(X)) is non empty set
{ b₁ where b₁ is Element of K26(X) : len b₁ = m } is set
K27((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X))) is Relation-like set
K26(K27((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X)))) is non empty set
P9 is non empty set
F1 is Relation-like Function-like set
dom F1 is set
rng F1 is set
F1 is set
F is set
F1 . F is set
F is Element of P9
P .: F is set
Funcs (r,X) is functional set
rng P is set
h is Relation-like Function-like set
dom h is set
rng h is set
h is Relation-like Function-like set
dom h is set
rng h is set
S is Element of K26(X)
len S is epsilon-transitive epsilon-connected ordinal cardinal set
h is Element of K26(r)
len h is epsilon-transitive epsilon-connected ordinal cardinal set
F1 is Relation-like the_subsets_of_card (m,r) -defined the_subsets_of_card (m,X) -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X))))
F is Element of the_subsets_of_card (m,r)
F1 . F is set
P .: F is set
X9 is Relation-like the_subsets_of_card (m,r) -defined the_subsets_of_card (m,X) -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X))))
P9 is Relation-like the_subsets_of_card (m,r) -defined the_subsets_of_card (m,X) -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X))))
F1 is set
X9 . F1 is set
F1 is Element of the_subsets_of_card (m,r)
P .: F1 is set
P9 . F1 is set
m is set
r is set
X is set
the_subsets_of_card (X,m) is Element of K26(K26(m))
K26(m) is non empty set
K26(K26(m)) is non empty set
{ b₁ where b₁ is Element of K26(m) : len b₁ = X } is set
the_subsets_of_card (X,r) is Element of K26(K26(r))
K26(r) is non empty set
K26(K26(r)) is non empty set
{ b₁ where b₁ is Element of K26(r) : len b₁ = X } is set
P is set
X9 is Element of K26(m)
len X9 is epsilon-transitive epsilon-connected ordinal cardinal set
P9 is Element of K26(r)
m is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
card m is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
r is set
K26(r) is non empty set
len r is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
K27(r,X) is Relation-like set
K26(K27(r,X)) is non empty set
P is Relation-like r -defined X -valued Function-like quasi_total Element of K26(K27(r,X))
(m,r,X,P) is Relation-like the_subsets_of_card (m,r) -defined the_subsets_of_card (m,X) -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X))))
the_subsets_of_card (m,r) is Element of K26(K26(r))
K26(K26(r)) is non empty set
{ b₁ where b₁ is Element of K26(r) : len b₁ = m } is set
the_subsets_of_card (m,X) is Element of K26(K26(X))
K26(X) is non empty set
K26(K26(X)) is non empty set
{ b₁ where b₁ is Element of K26(X) : len b₁ = m } is set
K27((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X))) is Relation-like set
K26(K27((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X)))) is non empty set
X9 is Element of K26(r)
P .: X9 is set
the_subsets_of_card (m,(P .: X9)) is Element of K26(K26((P .: X9)))
K26((P .: X9)) is non empty set
K26(K26((P .: X9))) is non empty set
{ b₁ where b₁ is Element of K26((P .: X9)) : len b₁ = m } is set
the_subsets_of_card (m,X9) is Element of K26(K26(X9))
K26(X9) is non empty set
K26(K26(X9)) is non empty set
{ b₁ where b₁ is Element of K26(X9) : len b₁ = m } is set
(m,r,X,P) .: (the_subsets_of_card (m,X9)) is set
P9 is Relation-like Function-like set
P9 .: r is set
Funcs (r,X) is functional set
len X is epsilon-transitive epsilon-connected ordinal cardinal set
F1 is Relation-like Function-like set
dom F1 is set
rng F1 is set
F1 is Relation-like Function-like set
F1 .: X is set
P9 .: (F1 .: X) is set
F1 * P9 is Relation-like Function-like set
(F1 * P9) .: X is set
Funcs ((the_subsets_of_card (m,r)),(the_subsets_of_card (m,X))) is functional set
F1 is set
rng P is set
dom (m,r,X,P) is Element of K26((the_subsets_of_card (m,r)))
K26((the_subsets_of_card (m,r))) is non empty set
P " F1 is set
(m,r,X,P) . (P " F1) is set
dom P is Element of K26(r)
P .: (P " F1) is set
F is Element of K26(X9)
len F is epsilon-transitive epsilon-connected ordinal cardinal set
S is Element of K26((P .: X9))
len S is epsilon-transitive epsilon-connected ordinal cardinal set
S is Relation-like Function-like set
dom S is set
rng S is set
F is set
(m,r,X,P) . F is set
F is set
(m,r,X,P) . F is set
F is Element of the_subsets_of_card (m,r)
P .: F is set
h is Relation-like Function-like set
dom h is set
rng h is set
S is Element of K26((P .: X9))
len S is epsilon-transitive epsilon-connected ordinal cardinal set
h is Element of K26(X9)
len h is epsilon-transitive epsilon-connected ordinal cardinal set
{0} is non empty V14() functional finite V36() 1 -element V129() V130() V131() V132() V133() V134() V141() V143() set
m is set
the_subsets_of_card (0,m) is Element of K26(K26(m))
K26(m) is non empty set
K26(K26(m)) is non empty set
{ b₁ where b₁ is Element of K26(m) : len b₁ = 0 } is set
r is set
X is Element of K26(m)
len X is epsilon-transitive epsilon-connected ordinal cardinal set
X is Element of K26(m)
len X is epsilon-transitive epsilon-connected ordinal cardinal set
r is finite V143() set
card r is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
m is finite V143() set
the_subsets_of_card (m,r) is finite V36() V143() Element of K26(K26(r))
K26(r) is non empty finite V36() V143() set
K26(K26(r)) is non empty finite V36() V143() set
{ b₁ where b₁ is Element of K26(r) : len b₁ = m } is set
{r} is non empty V14() finite V36() 1 -element V143() set
X is set
P is finite V143() Element of K26(r)
card P is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
X9 is finite V143() Element of K26(r)
r \ X9 is finite V143() Element of K26(r)
card (r \ X9) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
card X9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
(card r) - (card X9) is V16() V17() ext-real set
P is finite V143() Element of K26(r)
m is set
len m is epsilon-transitive epsilon-connected ordinal cardinal set
m is set
r is set
m \/ r is set
len m is epsilon-transitive epsilon-connected ordinal cardinal set
len (m \/ r) is epsilon-transitive epsilon-connected ordinal cardinal set
m is set
r is set
m \ r is Element of K26(m)
K26(m) is non empty set
m \/ r is set
(m \ r) \/ r is set
m is V14() non finite set
r is set
m \/ r is set
m is V14() non finite set
r is finite V143() set
m \ r is Element of K26(m)
K26(m) is non empty V14() non finite set
m is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
r is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
X is set
the_subsets_of_card (m,X) is Element of K26(K26(X))
K26(X) is non empty set
K26(K26(X)) is non empty set
{ b₁ where b₁ is Element of K26(X) : len b₁ = m } is set
K27((the_subsets_of_card (m,X)),r) is Relation-like set
K26(K27((the_subsets_of_card (m,X)),r)) is non empty set
len X is epsilon-transitive epsilon-connected ordinal cardinal set
P is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
P + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
P9 is set
the_subsets_of_card ((P + 1),P9) is Element of K26(K26(P9))
K26(P9) is non empty set
K26(K26(P9)) is non empty set
{ b₁ where b₁ is Element of K26(P9) : len b₁ = P + 1 } is set
X9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
K27((the_subsets_of_card ((P + 1),P9)),X9) is Relation-like set
K26(K27((the_subsets_of_card ((P + 1),P9)),X9)) is non empty set
len P9 is epsilon-transitive epsilon-connected ordinal cardinal set
the_subsets_of_card (omega,P9) is Element of K26(K26(P9))
{ b₁ where b₁ is Element of K26(P9) : len b₁ = omega } is set
F1 is non empty set
F1 is Relation-like the_subsets_of_card ((P + 1),P9) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card ((P + 1),P9)),X9))
min* P9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S is set
len S is epsilon-transitive epsilon-connected ordinal cardinal set
h is Element of S
{h} is non empty V14() finite 1 -element V143() set
S \ {h} is Element of K26(S)
K26(S) is non empty set
the_subsets_of_card (P,(S \ {h})) is Element of K26(K26((S \ {h})))
K26((S \ {h})) is non empty set
K26(K26((S \ {h}))) is non empty set
{ b₁ where b₁ is Element of K26((S \ {h})) : len b₁ = P } is set
K27((the_subsets_of_card (P,(S \ {h}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,(S \ {h}))),X9)) is non empty set
E is non empty set
E is Element of E
E \/ {h} is non empty set
F1 . (E \/ {h}) is set
x is Element of K26((S \ {h}))
len x is epsilon-transitive epsilon-connected ordinal cardinal set
(S \ {h}) \/ {h} is non empty set
S \/ {h} is non empty set
x99 is finite V143() set
x9 is Element of K26(S)
len x9 is epsilon-transitive epsilon-connected ordinal cardinal set
the_subsets_of_card ((P + 1),S) is Element of K26(K26(S))
K26(K26(S)) is non empty set
{ b₁ where b₁ is Element of K26(S) : len b₁ = P + 1 } is set
K27(E,X9) is Relation-like set
K26(K27(E,X9)) is non empty set
E is Relation-like E -defined X9 -valued Function-like quasi_total Element of K26(K27(E,X9))
len (S \ {h}) is epsilon-transitive epsilon-connected ordinal cardinal set
x is Relation-like the_subsets_of_card (P,(S \ {h})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(S \ {h}))),X9))
x9 is Element of K26((S \ {h}))
the_subsets_of_card (P,x9) is Element of K26(K26(x9))
K26(x9) is non empty set
K26(K26(x9)) is non empty set
{ b₁ where b₁ is Element of K26(x9) : len b₁ = P } is set
x | (the_subsets_of_card (P,x9)) is Relation-like the_subsets_of_card (P,(S \ {h})) -defined the_subsets_of_card (P,x9) -defined the_subsets_of_card (P,(S \ {h})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(S \ {h}))),X9))
x99 is Element of the_subsets_of_card (P,(S \ {h}))
x . x99 is set
x99 \/ {h} is non empty set
F1 . (x99 \/ {h}) is set
S is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h is Element of F1
h is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
E is Element of h
{E} is non empty V14() finite 1 -element V143() set
h \ {E} is Element of K26(h)
K26(h) is non empty set
the_subsets_of_card (P,(h \ {E})) is Element of K26(K26((h \ {E})))
K26((h \ {E})) is non empty set
K26(K26((h \ {E}))) is non empty set
{ b₁ where b₁ is Element of K26((h \ {E})) : len b₁ = P } is set
K27((the_subsets_of_card (P,(h \ {E}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,(h \ {E}))),X9)) is non empty set
E is Element of K26(P9)
len E is epsilon-transitive epsilon-connected ordinal cardinal set
x is Element of K26((h \ {E}))
E is Relation-like the_subsets_of_card (P,(h \ {E})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(h \ {E}))),X9))
the_subsets_of_card (P,x) is Element of K26(K26(x))
K26(x) is non empty set
K26(K26(x)) is non empty set
{ b₁ where b₁ is Element of K26(x) : len b₁ = P } is set
E | (the_subsets_of_card (P,x)) is Relation-like the_subsets_of_card (P,(h \ {E})) -defined the_subsets_of_card (P,x) -defined the_subsets_of_card (P,(h \ {E})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(h \ {E}))),X9))
len x is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ( not b₁ <= h & b₁ in x ) } is set
min* { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ( not b₁ <= h & b₁ in x ) } is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
x9 is Element of F1
F9 is Element of F1
S9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
S9 is Element of F1
S99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
{S9} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
F9 \ {S9} is Element of K26(F9)
K26(F9) is non empty set
the_subsets_of_card (P,(F9 \ {S9})) is Element of K26(K26((F9 \ {S9})))
K26((F9 \ {S9})) is non empty set
K26(K26((F9 \ {S9}))) is non empty set
{ b₁ where b₁ is Element of K26((F9 \ {S9})) : len b₁ = P } is set
K27((the_subsets_of_card (P,(F9 \ {S9}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,(F9 \ {S9}))),X9)) is non empty set
x is Relation-like the_subsets_of_card (P,(F9 \ {S9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(F9 \ {S9}))),X9))
S99 is Element of K26((F9 \ {S9}))
the_subsets_of_card (P,S99) is Element of K26(K26(S99))
K26(S99) is non empty set
K26(K26(S99)) is non empty set
{ b₁ where b₁ is Element of K26(S99) : len b₁ = P } is set
x | (the_subsets_of_card (P,S99)) is Relation-like the_subsets_of_card (P,(F9 \ {S9})) -defined the_subsets_of_card (P,S99) -defined the_subsets_of_card (P,(F9 \ {S9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(F9 \ {S9}))),X9))
S999 is set
s1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
S999 is V129() V130() V131() V132() V133() V134() V143() Element of K26(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ( b₁ <= h & b₁ in x ) } is set
s2 is set
S999 \/ { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ( b₁ <= h & b₁ in x ) } is set
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
s2 is set
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
h + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
Segm (h + 1) is V129() V130() V131() V132() V133() V134() V143() Element of K26(omega)
s2 is set
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
{ b₂ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ( b₂ <= h & b₂ in x ) } is set
S999 \/ { b₂ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ( b₂ <= h & b₂ in x ) } is set
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
{ b₂ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ( b₂ <= h & b₂ in x ) } is set
S999 \/ { b₂ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ( b₂ <= h & b₂ in x ) } is set
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
{ b₂ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ( b₂ <= h & b₂ in x ) } is set
S999 \/ { b₂ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ( b₂ <= h & b₂ in x ) } is set
s1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
s1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
s1 is Element of the_subsets_of_card (P,(F9 \ {S9}))
x . s1 is set
s1 \/ {S9} is non empty set
F1 . (s1 \/ {S9}) is set
s1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
S99 is Element of F1
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
c₂₄ is Element of F1
S999 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
{x} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
S99 \ {x} is Element of K26(S99)
K26(S99) is non empty set
the_subsets_of_card (P,(S99 \ {x})) is Element of K26(K26((S99 \ {x})))
K26((S99 \ {x})) is non empty set
K26(K26((S99 \ {x}))) is non empty set
{ b₁ where b₁ is Element of K26((S99 \ {x})) : len b₁ = P } is set
K27((the_subsets_of_card (P,(S99 \ {x}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,(S99 \ {x}))),X9)) is non empty set
F9 is Element of F1
S9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
S9 is Element of F1
S99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
{S9} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
F9 \ {S9} is Element of K26(F9)
K26(F9) is non empty set
the_subsets_of_card (P,(F9 \ {S9})) is Element of K26(K26((F9 \ {S9})))
K26((F9 \ {S9})) is non empty set
K26(K26((F9 \ {S9}))) is non empty set
{ b₁ where b₁ is Element of K26((F9 \ {S9})) : len b₁ = P } is set
K27((the_subsets_of_card (P,(F9 \ {S9}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,(F9 \ {S9}))),X9)) is non empty set
E is Element of F1
E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x is Element of F1
x99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x9 is Element of F1
F9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
{x99} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
x \ {x99} is Element of K26(x)
K26(x) is non empty set
the_subsets_of_card (P,(x \ {x99})) is Element of K26(K26((x \ {x99})))
K26((x \ {x99})) is non empty set
K26(K26((x \ {x99}))) is non empty set
{ b₁ where b₁ is Element of K26((x \ {x99})) : len b₁ = P } is set
K27((the_subsets_of_card (P,(x \ {x99}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,(x \ {x99}))),X9)) is non empty set
K27(NAT,F1) is Relation-like non empty V14() non finite set
K26(K27(NAT,F1)) is non empty V14() non finite set
K27(NAT,omega) is Relation-like non empty V14() non finite set
K26(K27(NAT,omega)) is non empty V14() non finite set
F is Element of F1
S is Relation-like NAT -defined F1 -valued non empty Function-like V25( NAT ) quasi_total Element of K26(K27(NAT,F1))
S . 0 is Element of F1
h is Relation-like NAT -defined omega -valued non empty Function-like V25( NAT ) quasi_total Element of K26(K27(NAT,omega))
h . 0 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
h . 0 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h . (0 + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
S . (0 + 1) is Element of F1
S . 0 is Element of F1
E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S . E is Element of F1
E + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S . (E + 1) is Element of F1
h . E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
h . (E + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
E is Element of F1
{x9} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
E \ {x9} is Element of K26(E)
K26(E) is non empty set
the_subsets_of_card (P,(E \ {x9})) is Element of K26(K26((E \ {x9})))
K26((E \ {x9})) is non empty set
K26(K26((E \ {x9}))) is non empty set
{ b₁ where b₁ is Element of K26((E \ {x9})) : len b₁ = P } is set
K27((the_subsets_of_card (P,(E \ {x9}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9)) is non empty set
x is Element of F1
x99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h . (0 + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
S9 is Element of K26((E \ {x9}))
F9 is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))
the_subsets_of_card (P,S9) is Element of K26(K26(S9))
K26(S9) is non empty set
K26(K26(S9)) is non empty set
{ b₁ where b₁ is Element of K26(S9) : len b₁ = P } is set
F9 | (the_subsets_of_card (P,S9)) is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined the_subsets_of_card (P,S9) -defined the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))
S . (0 + 1) is Element of F1
S9 is Element of K26((E \ {x9}))
F9 is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))
the_subsets_of_card (P,S9) is Element of K26(K26(S9))
K26(S9) is non empty set
K26(K26(S9)) is non empty set
{ b₁ where b₁ is Element of K26(S9) : len b₁ = P } is set
F9 | (the_subsets_of_card (P,S9)) is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined the_subsets_of_card (P,S9) -defined the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))
S9 is Element of K26((E \ {x9}))
F9 is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))
the_subsets_of_card (P,S9) is Element of K26(K26(S9))
K26(S9) is non empty set
K26(K26(S9)) is non empty set
{ b₁ where b₁ is Element of K26(S9) : len b₁ = P } is set
F9 | (the_subsets_of_card (P,S9)) is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined the_subsets_of_card (P,S9) -defined the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))
S9 is Element of K26((E \ {x9}))
F9 is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))
the_subsets_of_card (P,S9) is Element of K26(K26(S9))
K26(S9) is non empty set
K26(K26(S9)) is non empty set
{ b₁ where b₁ is Element of K26(S9) : len b₁ = P } is set
F9 | (the_subsets_of_card (P,S9)) is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined the_subsets_of_card (P,S9) -defined the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))
h is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
h . h is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
h + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h . (h + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
S . (h + 1) is Element of F1
S . h is Element of F1
h . (h + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
(h + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h . ((h + 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
S . ((h + 1) + 1) is Element of F1
S . (h + 1) is Element of F1
E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S . E is Element of F1
E + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S . (E + 1) is Element of F1
h . E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
h . (E + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
E is Element of F1
x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
{x9} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
E \ {x9} is Element of K26(E)
K26(E) is non empty set
the_subsets_of_card (P,(E \ {x9})) is Element of K26(K26((E \ {x9})))
K26((E \ {x9})) is non empty set
K26(K26((E \ {x9}))) is non empty set
{ b₁ where b₁ is Element of K26((E \ {x9})) : len b₁ = P } is set
K27((the_subsets_of_card (P,(E \ {x9}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9)) is non empty set
x is Element of F1
x99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
S9 is Element of K26((E \ {x9}))
F9 is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))
the_subsets_of_card (P,S9) is Element of K26(K26(S9))
K26(S9) is non empty set
K26(K26(S9)) is non empty set
{ b₁ where b₁ is Element of K26(S9) : len b₁ = P } is set
F9 | (the_subsets_of_card (P,S9)) is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined the_subsets_of_card (P,S9) -defined the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))
S9 is Element of K26((E \ {x9}))
F9 is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))
the_subsets_of_card (P,S9) is Element of K26(K26(S9))
K26(S9) is non empty set
K26(K26(S9)) is non empty set
{ b₁ where b₁ is Element of K26(S9) : len b₁ = P } is set
F9 | (the_subsets_of_card (P,S9)) is Relation-like the_subsets_of_card (P,(E \ {x9})) -defined the_subsets_of_card (P,S9) -defined the_subsets_of_card (P,(E \ {x9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(E \ {x9}))),X9))
h is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
h + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
(h + 1) + E is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal ext-real positive non negative V143() set
S . E is Element of F1
S . E is Element of F1
h . E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
h . E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
E + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(h + 1) + E is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h + (E + 1) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S . (E + 1) is Element of F1
h . (E + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
x99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
x99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
F9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
h is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
0 + E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
S . h is Element of F1
S . E is Element of F1
E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
h . h is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
h . E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
h is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
S . h is Element of F1
S . E is Element of F1
h . h is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
h . E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
E + E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
E is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
E + x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
h is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S . h is Element of F1
h . h is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
{(h . h)} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
(S . h) \ {(h . h)} is Element of K26((S . h))
K26((S . h)) is non empty set
the_subsets_of_card (P,((S . h) \ {(h . h)})) is Element of K26(K26(((S . h) \ {(h . h)})))
K26(((S . h) \ {(h . h)})) is non empty set
K26(K26(((S . h) \ {(h . h)}))) is non empty set
{ b₁ where b₁ is Element of K26(((S . h) \ {(h . h)})) : len b₁ = P } is set
K27((the_subsets_of_card (P,((S . h) \ {(h . h)}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,((S . h) \ {(h . h)}))),X9)) is non empty set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= h ) } is set
h + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S . (h + 1) is Element of F1
E is set
the_subsets_of_card (P,E) is Element of K26(K26(E))
K26(E) is non empty set
K26(K26(E)) is non empty set
{ b₁ where b₁ is Element of K26(E) : len b₁ = P } is set
E is Relation-like the_subsets_of_card (P,((S . h) \ {(h . h)})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,((S . h) \ {(h . h)}))),X9))
E | (the_subsets_of_card (P,E)) is Relation-like the_subsets_of_card (P,((S . h) \ {(h . h)})) -defined the_subsets_of_card (P,E) -defined the_subsets_of_card (P,((S . h) \ {(h . h)})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,((S . h) \ {(h . h)}))),X9))
h . (h + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x is Element of F1
x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x99 is Element of F1
F9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
{F9} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
x99 \ {F9} is Element of K26(x99)
K26(x99) is non empty set
the_subsets_of_card (P,(x99 \ {F9})) is Element of K26(K26((x99 \ {F9})))
K26((x99 \ {F9})) is non empty set
K26(K26((x99 \ {F9}))) is non empty set
{ b₁ where b₁ is Element of K26((x99 \ {F9})) : len b₁ = P } is set
K27((the_subsets_of_card (P,(x99 \ {F9}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,(x99 \ {F9}))),X9)) is non empty set
S9 is Element of K26((x99 \ {F9}))
S9 is Relation-like the_subsets_of_card (P,(x99 \ {F9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(x99 \ {F9}))),X9))
the_subsets_of_card (P,S9) is Element of K26(K26(S9))
K26(S9) is non empty set
K26(K26(S9)) is non empty set
{ b₁ where b₁ is Element of K26(S9) : len b₁ = P } is set
S9 | (the_subsets_of_card (P,S9)) is Relation-like the_subsets_of_card (P,(x99 \ {F9})) -defined the_subsets_of_card (P,S9) -defined the_subsets_of_card (P,(x99 \ {F9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(x99 \ {F9}))),X9))
S9 is Element of K26((x99 \ {F9}))
S9 is Relation-like the_subsets_of_card (P,(x99 \ {F9})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,(x99 \ {F9}))),X9))
the_subsets_of_card (P,S9) is Element of K26(K26(S9))
K26(S9) is non empty set
K26(K26(S9)) is non empty set
{ b₁ where b₁ is Element of K26(S9) : len b₁ = P } is set
S9 | (the_subsets_of_card (P,S9)) is Relation-like the_subsets_of_card (P,(x99 \ {F9})) -defined the_subsets_of_card (P,S9) -defined the_subsets_of_card (P,(x99 \ {F9})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,(x99 \ {F9}))),X9))
S99 is Relation-like the_subsets_of_card (P,((S . h) \ {(h . h)})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,((S . h) \ {(h . h)}))),X9))
S99 is Element of the_subsets_of_card (P,((S . h) \ {(h . h)}))
S99 . S99 is set
E . S99 is set
S99 \/ {(h . h)} is non empty set
F1 . (S99 \/ {(h . h)}) is set
the_subsets_of_card (P,(S . (h + 1))) is Element of K26(K26((S . (h + 1))))
K26((S . (h + 1))) is non empty set
K26(K26((S . (h + 1)))) is non empty set
{ b₁ where b₁ is Element of K26((S . (h + 1))) : len b₁ = P } is set
E | (the_subsets_of_card (P,(S . (h + 1)))) is Relation-like the_subsets_of_card (P,((S . h) \ {(h . h)})) -defined the_subsets_of_card (P,(S . (h + 1))) -defined the_subsets_of_card (P,((S . h) \ {(h . h)})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,((S . h) \ {(h . h)}))),X9))
S99 is set
c₂₄ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h . x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
c₂₄ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h . c₂₄ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
S . c₂₄ is Element of F1
dom (E | (the_subsets_of_card (P,E))) is Element of K26((the_subsets_of_card (P,E)))
K26((the_subsets_of_card (P,E))) is non empty set
S99 is set
c₂₄ is set
(E | (the_subsets_of_card (P,E))) . S99 is set
(E | (the_subsets_of_card (P,E))) . c₂₄ is set
dom E is Element of K26((the_subsets_of_card (P,((S . h) \ {(h . h)}))))
K26((the_subsets_of_card (P,((S . h) \ {(h . h)})))) is non empty set
dom (E | (the_subsets_of_card (P,(S . (h + 1))))) is Element of K26((the_subsets_of_card (P,((S . h) \ {(h . h)}))))
(E | (the_subsets_of_card (P,(S . (h + 1))))) | (the_subsets_of_card (P,E)) is Relation-like the_subsets_of_card (P,((S . h) \ {(h . h)})) -defined the_subsets_of_card (P,E) -defined the_subsets_of_card (P,((S . h) \ {(h . h)})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,((S . h) \ {(h . h)}))),X9))
((E | (the_subsets_of_card (P,(S . (h + 1))))) | (the_subsets_of_card (P,E))) . S99 is set
(E | (the_subsets_of_card (P,(S . (h + 1))))) . S99 is set
(E | (the_subsets_of_card (P,(S . (h + 1))))) . c₂₄ is set
((E | (the_subsets_of_card (P,(S . (h + 1))))) | (the_subsets_of_card (P,E))) . c₂₄ is set
dom h is non empty V129() V130() V131() V132() V133() V134() V143() Element of K26(NAT)
h is set
E is set
h . h is set
h . E is set
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h . x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h . E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
x99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
x99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= h ) } is set
len { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= h ) } is epsilon-transitive epsilon-connected ordinal cardinal set
E is set
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h . x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
h + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
Segm (h + 1) is V129() V130() V131() V132() V133() V134() V143() Element of K26(omega)
NAT \ (Segm (h + 1)) is V129() V130() V131() V132() V133() V134() Element of K26(REAL)
h | (NAT \ (Segm (h + 1))) is Relation-like NAT -defined NAT \ (Segm (h + 1)) -defined NAT -defined omega -valued Function-like Element of K26(K27(NAT,omega))
dom (h | (NAT \ (Segm (h + 1)))) is V129() V130() V131() V132() V133() V134() Element of K26((NAT \ (Segm (h + 1))))
K26((NAT \ (Segm (h + 1)))) is non empty set
(dom h) /\ (NAT \ (Segm (h + 1))) is V129() V130() V131() V132() V133() V134() Element of K26(REAL)
NAT /\ (NAT \ (Segm (h + 1))) is V129() V130() V131() V132() V133() V134() Element of K26(REAL)
NAT /\ NAT is V129() V130() V131() V132() V133() V134() Element of K26(REAL)
(NAT /\ NAT) \ (Segm (h + 1)) is V129() V130() V131() V132() V133() V134() Element of K26(REAL)
rng (h | (NAT \ (Segm (h + 1)))) is set
E is set
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h . x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h . x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x is set
(h | (NAT \ (Segm (h + 1)))) . x is set
x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h . x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
h is set
E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S . E is Element of F1
h . E is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
E + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S . (E + 1) is Element of F1
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= E ) } is set
x is Element of S . E
{x} is non empty V14() finite 1 -element V143() set
(S . E) \ {x} is Element of K26((S . E))
K26((S . E)) is non empty set
the_subsets_of_card (P,((S . E) \ {x})) is Element of K26(K26(((S . E) \ {x})))
K26(((S . E) \ {x})) is non empty set
K26(K26(((S . E) \ {x}))) is non empty set
{ b₁ where b₁ is Element of K26(((S . E) \ {x})) : len b₁ = P } is set
K27((the_subsets_of_card (P,((S . E) \ {x}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,((S . E) \ {x}))),X9)) is non empty set
x99 is Element of K26(P9)
len x99 is epsilon-transitive epsilon-connected ordinal cardinal set
F9 is Element of K26(((S . E) \ {x}))
x99 is Relation-like the_subsets_of_card (P,((S . E) \ {x})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,((S . E) \ {x}))),X9))
the_subsets_of_card (P,F9) is Element of K26(K26(F9))
K26(F9) is non empty set
K26(K26(F9)) is non empty set
{ b₁ where b₁ is Element of K26(F9) : len b₁ = P } is set
x99 | (the_subsets_of_card (P,F9)) is Relation-like the_subsets_of_card (P,((S . E) \ {x})) -defined the_subsets_of_card (P,F9) -defined the_subsets_of_card (P,((S . E) \ {x})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,((S . E) \ {x}))),X9))
S9 is set
{(h . E)} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
(S . E) \ {(h . E)} is Element of K26((S . E))
the_subsets_of_card (P, { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= E ) } ) is Element of K26(K26( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= E ) } ))
K26( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= E ) } ) is non empty set
K26(K26( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= E ) } )) is non empty set
{ b₁ where b₁ is Element of K26( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= E ) } ) : len b₁ = P } is set
x99 | (the_subsets_of_card (P, { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= E ) } )) is Relation-like the_subsets_of_card (P,((S . E) \ {x})) -defined the_subsets_of_card (P, { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= E ) } ) -defined the_subsets_of_card (P,((S . E) \ {x})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,((S . E) \ {x}))),X9))
K27((the_subsets_of_card (P, { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= E ) } )),X9) is Relation-like set
K26(K27((the_subsets_of_card (P, { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= E ) } )),X9)) is non empty set
len { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= E ) } is epsilon-transitive epsilon-connected ordinal cardinal set
card P is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
rng (x99 | (the_subsets_of_card (P, { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= E ) } ))) is set
S9 is epsilon-transitive epsilon-connected ordinal Element of X9
{S9} is non empty V14() finite 1 -element V143() set
S9 is set
S99 is set
the_subsets_of_card (P,S99) is Element of K26(K26(S99))
K26(S99) is non empty set
K26(K26(S99)) is non empty set
{ b₁ where b₁ is Element of K26(S99) : len b₁ = P } is set
c₂₄ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S . c₂₄ is Element of F1
h . c₂₄ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
{(h . c₂₄)} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
(S . c₂₄) \ {(h . c₂₄)} is Element of K26((S . c₂₄))
K26((S . c₂₄)) is non empty set
the_subsets_of_card (P,((S . c₂₄) \ {(h . c₂₄)})) is Element of K26(K26(((S . c₂₄) \ {(h . c₂₄)})))
K26(((S . c₂₄) \ {(h . c₂₄)})) is non empty set
K26(K26(((S . c₂₄) \ {(h . c₂₄)}))) is non empty set
{ b₁ where b₁ is Element of K26(((S . c₂₄) \ {(h . c₂₄)})) : len b₁ = P } is set
K27((the_subsets_of_card (P,((S . c₂₄) \ {(h . c₂₄)}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,((S . c₂₄) \ {(h . c₂₄)}))),X9)) is non empty set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= c₂₄ ) } is set
x is Relation-like the_subsets_of_card (P,((S . c₂₄) \ {(h . c₂₄)})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,((S . c₂₄) \ {(h . c₂₄)}))),X9))
x | (the_subsets_of_card (P,S99)) is Relation-like the_subsets_of_card (P,S99) -defined the_subsets_of_card (P,((S . c₂₄) \ {(h . c₂₄)})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,((S . c₂₄) \ {(h . c₂₄)}))),X9))
rng (x | (the_subsets_of_card (P,S99))) is set
S99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S999 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
{S999} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
s1 is Element of the_subsets_of_card (P,((S . c₂₄) \ {(h . c₂₄)}))
x99 . s1 is set
x . s1 is set
s1 \/ {(h . c₂₄)} is non empty set
F1 . (s1 \/ {(h . c₂₄)}) is set
S99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S . S99 is Element of F1
h . S99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
{(h . S99)} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
(S . S99) \ {(h . S99)} is Element of K26((S . S99))
K26((S . S99)) is non empty set
the_subsets_of_card (P,((S . S99) \ {(h . S99)})) is Element of K26(K26(((S . S99) \ {(h . S99)})))
K26(((S . S99) \ {(h . S99)})) is non empty set
K26(K26(((S . S99) \ {(h . S99)}))) is non empty set
{ b₁ where b₁ is Element of K26(((S . S99) \ {(h . S99)})) : len b₁ = P } is set
K27((the_subsets_of_card (P,((S . S99) \ {(h . S99)}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,((S . S99) \ {(h . S99)}))),X9)) is non empty set
S99 is set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= S99 ) } is set
c₂₄ is Relation-like the_subsets_of_card (P,((S . S99) \ {(h . S99)})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,((S . S99) \ {(h . S99)}))),X9))
the_subsets_of_card (P,S99) is Element of K26(K26(S99))
K26(S99) is non empty set
K26(K26(S99)) is non empty set
{ b₁ where b₁ is Element of K26(S99) : len b₁ = P } is set
c₂₄ | (the_subsets_of_card (P,S99)) is Relation-like the_subsets_of_card (P,((S . S99) \ {(h . S99)})) -defined the_subsets_of_card (P,S99) -defined the_subsets_of_card (P,((S . S99) \ {(h . S99)})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,((S . S99) \ {(h . S99)}))),X9))
rng (c₂₄ | (the_subsets_of_card (P,S99))) is set
K27(NAT,X9) is Relation-like set
K26(K27(NAT,X9)) is non empty set
h is Relation-like NAT -defined X9 -valued Function-like quasi_total Element of K26(K27(NAT,X9))
Funcs (NAT,X9) is functional set
rng h is set
E is Relation-like Function-like set
dom E is set
rng E is set
E is set
{E} is non empty V14() finite 1 -element V143() set
h " {E} is set
h .: (h " {E}) is set
dom h is V129() V130() V131() V132() V133() V134() V143() Element of K26(NAT)
len (h " {E}) is epsilon-transitive epsilon-connected ordinal cardinal set
len (h .: (h " {E})) is epsilon-transitive epsilon-connected ordinal cardinal set
x is set
x9 is set
[x9,x] is set
h . x9 is set
x99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S . x99 is Element of F1
x is Element of K26(P9)
x9 is Element of K26(P9)
the_subsets_of_card ((P + 1),x9) is Element of K26(K26(x9))
K26(x9) is non empty set
K26(K26(x9)) is non empty set
{ b₁ where b₁ is Element of K26(x9) : len b₁ = P + 1 } is set
F1 | (the_subsets_of_card ((P + 1),x9)) is Relation-like the_subsets_of_card ((P + 1),P9) -defined the_subsets_of_card ((P + 1),x9) -defined the_subsets_of_card ((P + 1),P9) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card ((P + 1),P9)),X9))
dom (F1 | (the_subsets_of_card ((P + 1),x9))) is Element of K26((the_subsets_of_card ((P + 1),P9)))
K26((the_subsets_of_card ((P + 1),P9))) is non empty set
x99 is set
(F1 | (the_subsets_of_card ((P + 1),x9))) . x99 is set
F9 is Element of K26(x9)
len F9 is epsilon-transitive epsilon-connected ordinal cardinal set
min* F9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
{(min* F9)} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
x99 \ {(min* F9)} is Element of K26(x99)
K26(x99) is non empty set
S99 is set
h . S99 is set
S99 is set
[S99,S99] is set
h . S99 is set
c₂₄ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= c₂₄ ) } is set
h . c₂₄ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
{(h . c₂₄)} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
(x99 \ {(min* F9)}) \/ {(h . c₂₄)} is non empty set
S . c₂₄ is Element of F1
S999 is Element of S . c₂₄
{S999} is non empty V14() finite 1 -element V143() set
(S . c₂₄) \ {S999} is Element of K26((S . c₂₄))
K26((S . c₂₄)) is non empty set
the_subsets_of_card (P,((S . c₂₄) \ {S999})) is Element of K26(K26(((S . c₂₄) \ {S999})))
K26(((S . c₂₄) \ {S999})) is non empty set
K26(K26(((S . c₂₄) \ {S999}))) is non empty set
{ b₁ where b₁ is Element of K26(((S . c₂₄) \ {S999})) : len b₁ = P } is set
K27((the_subsets_of_card (P,((S . c₂₄) \ {S999}))),X9) is Relation-like set
K26(K27((the_subsets_of_card (P,((S . c₂₄) \ {S999}))),X9)) is non empty set
s1 is Element of K26(P9)
len s1 is epsilon-transitive epsilon-connected ordinal cardinal set
s2 is Element of K26(((S . c₂₄) \ {S999}))
s1 is Relation-like the_subsets_of_card (P,((S . c₂₄) \ {S999})) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (P,((S . c₂₄) \ {S999}))),X9))
the_subsets_of_card (P,s2) is Element of K26(K26(s2))
K26(s2) is non empty set
K26(K26(s2)) is non empty set
{ b₁ where b₁ is Element of K26(s2) : len b₁ = P } is set
s1 | (the_subsets_of_card (P,s2)) is Relation-like the_subsets_of_card (P,((S . c₂₄) \ {S999})) -defined the_subsets_of_card (P,s2) -defined the_subsets_of_card (P,((S . c₂₄) \ {S999})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,((S . c₂₄) \ {S999}))),X9))
len (x99 \ {(min* F9)}) is epsilon-transitive epsilon-connected ordinal cardinal set
x is finite V143() set
card x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
c₂₄ + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S . (c₂₄ + 1) is Element of F1
Y9 is set
j is set
h . j is set
x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
j is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h . j is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
j is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
h . j is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
K26( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= c₂₄ ) } ) is non empty set
Y99 is finite V143() set
card Y99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
(card Y99) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
the_subsets_of_card (P, { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= c₂₄ ) } ) is Element of K26(K26( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= c₂₄ ) } ))
K26(K26( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= c₂₄ ) } )) is non empty set
{ b₁ where b₁ is Element of K26( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= c₂₄ ) } ) : len b₁ = P } is set
h . c₂₄ is epsilon-transitive epsilon-connected ordinal Element of X9
s1 | (the_subsets_of_card (P, { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= c₂₄ ) } )) is Relation-like the_subsets_of_card (P,((S . c₂₄) \ {S999})) -defined the_subsets_of_card (P, { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= c₂₄ ) } ) -defined the_subsets_of_card (P,((S . c₂₄) \ {S999})) -defined X9 -valued Function-like Element of K26(K27((the_subsets_of_card (P,((S . c₂₄) \ {S999}))),X9))
rng (s1 | (the_subsets_of_card (P, { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= c₂₄ ) } ))) is set
Y9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
{Y9} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= c₂₄ ) } \ {(h . c₂₄)} is Element of K26( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= c₂₄ ) } )
(S . c₂₄) \ {(h . c₂₄)} is Element of K26((S . c₂₄))
the_subsets_of_card (P,((S . c₂₄) \ {(h . c₂₄)})) is Element of K26(K26(((S . c₂₄) \ {(h . c₂₄)})))
K26(((S . c₂₄) \ {(h . c₂₄)})) is non empty set
K26(K26(((S . c₂₄) \ {(h . c₂₄)}))) is non empty set
{ b₁ where b₁ is Element of K26(((S . c₂₄) \ {(h . c₂₄)})) : len b₁ = P } is set
Y9 is Element of the_subsets_of_card (P,((S . c₂₄) \ {(h . c₂₄)}))
dom s1 is Element of K26((the_subsets_of_card (P,((S . c₂₄) \ {S999}))))
K26((the_subsets_of_card (P,((S . c₂₄) \ {S999})))) is non empty set
dom (s1 | (the_subsets_of_card (P, { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= c₂₄ ) } ))) is Element of K26((the_subsets_of_card (P,((S . c₂₄) \ {S999}))))
(s1 | (the_subsets_of_card (P, { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega : ex b₂ being epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT st
( h . b₂ = b₁ & not b₂ <= c₂₄ ) } ))) . Y9 is set
s1 . Y9 is set
Y9 \/ {(h . c₂₄)} is non empty set
F1 . (Y9 \/ {(h . c₂₄)}) is set
x99 is set
F9 is set
(F1 | (the_subsets_of_card ((P + 1),x9))) . x99 is set
(F1 | (the_subsets_of_card ((P + 1),x9))) . F9 is set
P9 is set
the_subsets_of_card ((P + 1),P9) is Element of K26(K26(P9))
K26(P9) is non empty set
K26(K26(P9)) is non empty set
{ b₁ where b₁ is Element of K26(P9) : len b₁ = P + 1 } is set
X9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
K27((the_subsets_of_card ((P + 1),P9)),X9) is Relation-like set
K26(K27((the_subsets_of_card ((P + 1),P9)),X9)) is non empty set
len P9 is epsilon-transitive epsilon-connected ordinal cardinal set
F1 is Relation-like the_subsets_of_card ((P + 1),P9) -defined X9 -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card ((P + 1),P9)),X9))
P is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
X9 is set
the_subsets_of_card (0,X9) is Element of K26(K26(X9))
K26(X9) is non empty set
K26(K26(X9)) is non empty set
{ b₁ where b₁ is Element of K26(X9) : len b₁ = 0 } is set
K27((the_subsets_of_card (0,X9)),P) is Relation-like set
K26(K27((the_subsets_of_card (0,X9)),P)) is non empty set
len X9 is epsilon-transitive epsilon-connected ordinal cardinal set
F1 is Relation-like the_subsets_of_card (0,X9) -defined P -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (0,X9)),P))
F1 is Element of K26(X9)
the_subsets_of_card (0,F1) is Element of K26(K26(F1))
K26(F1) is non empty set
K26(K26(F1)) is non empty set
{ b₁ where b₁ is Element of K26(F1) : len b₁ = 0 } is set
F1 | (the_subsets_of_card (0,F1)) is Relation-like the_subsets_of_card (0,X9) -defined the_subsets_of_card (0,F1) -defined the_subsets_of_card (0,X9) -defined P -valued Function-like Element of K26(K27((the_subsets_of_card (0,X9)),P))
dom (F1 | (the_subsets_of_card (0,F1))) is Element of K26((the_subsets_of_card (0,X9)))
K26((the_subsets_of_card (0,X9))) is non empty set
F is set
F is set
(F1 | (the_subsets_of_card (0,F1))) . F is set
(F1 | (the_subsets_of_card (0,F1))) . F is set
F1 | {0} is Relation-like {0} -defined the_subsets_of_card (0,X9) -defined P -valued Function-like finite V143() Element of K26(K27((the_subsets_of_card (0,X9)),P))
dom (F1 | {0}) is V14() functional finite V36() V129() V130() V131() V132() V133() V134() V141() V143() Element of K26({0})
K26({0}) is non empty finite V36() V143() set
dom F1 is Element of K26((the_subsets_of_card (0,X9)))
(dom F1) /\ {0} is finite V129() V130() V131() V132() V133() V134() V143() Element of K26((the_subsets_of_card (0,X9)))
P is Relation-like the_subsets_of_card (m,X) -defined r -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (m,X)),r))
m is set
the_subsets_of_card (0,m) is Element of K26(K26(m))
K26(m) is non empty set
K26(K26(m)) is non empty set
{ b₁ where b₁ is Element of K26(m) : len b₁ = 0 } is set
m is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
r is finite V143() set
card r is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
the_subsets_of_card (m,r) is finite V36() V143() Element of K26(K26(r))
K26(r) is non empty finite V36() V143() set
K26(K26(r)) is non empty finite V36() V143() set
{ b₁ where b₁ is Element of K26(r) : len b₁ = m } is set
Seg m is finite m -element V129() V130() V131() V132() V133() V134() V143() Element of K26(NAT)
card (Seg m) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
X is set
P is finite V143() Element of K26(r)
card P is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
m is set
r is set
X is set
the_subsets_of_card (X,m) is Element of K26(K26(m))
K26(m) is non empty set
K26(K26(m)) is non empty set
{ b₁ where b₁ is Element of K26(m) : len b₁ = X } is set
the_subsets_of_card (X,r) is Element of K26(K26(r))
K26(r) is non empty set
K26(K26(r)) is non empty set
{ b₁ where b₁ is Element of K26(r) : len b₁ = X } is set
m is set
r is set
len r is epsilon-transitive epsilon-connected ordinal cardinal set
the_subsets_of_card (m,r) is Element of K26(K26(r))
K26(r) is non empty set
K26(K26(r)) is non empty set
{ b₁ where b₁ is Element of K26(r) : len b₁ = m } is set
{r} is non empty V14() finite 1 -element V143() set
m is set
r is set
K27(m,r) is Relation-like set
K26(K27(m,r)) is non empty set
X is Relation-like m -defined r -valued Function-like quasi_total Element of K26(K27(m,r))
rng X is set
P is Element of r
{P} is non empty V14() finite 1 -element V143() set
m is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
r is finite V143() set
card r is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
K26(r) is non empty finite V36() V143() set
card m is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
X is set
len X is epsilon-transitive epsilon-connected ordinal cardinal set
P is finite V143() Element of K26(r)
card P is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
m is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
r is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
r + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
r + m is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
(r + m) choose m is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
X + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
X9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
P9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
P9 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
P9 + X9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(P9 + X9) choose X9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
P9 + X is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(P9 + X) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
((P9 + X) + 1) choose (X + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(P9 + X) choose (X + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(P9 + X) choose X is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
((P9 + X) choose (X + 1)) + ((P9 + X) choose X) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(P9 + 1) + ((P9 + X) choose (X + 1)) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
0 + (P9 + 1) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
((P9 + X) choose (X + 1)) + (P9 + 1) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
P9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
P9 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
P9 + (X + 1) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(P9 + (X + 1)) choose (X + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
X9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
X9 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
X9 + 0 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(X9 + 0) choose 0 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
X + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
P is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
X + P is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(X + P) choose P is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
m + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
r + m is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
(r + m) choose m is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
X9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
X9 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
X9 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(X9 + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
F1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
F1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
F1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
F1 + F1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(F1 + F1) choose F1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
F1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
F1 + X9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(F1 + X9) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
((F1 + X9) + 1) choose (X9 + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(F1 + X9) choose (X9 + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(F1 + X9) choose X9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
((F1 + X9) choose (X9 + 1)) + ((F1 + X9) choose X9) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
F1 -' 1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(F1 -' 1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(F1 -' 1) + (X9 + 1) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
((F1 -' 1) + (X9 + 1)) choose (X9 + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
1 - 1 is V16() V17() ext-real set
F1 - 1 is V16() V17() ext-real set
1 + (X9 + 1) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
((F1 + X9) choose (X9 + 1)) + (X9 + 1) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(X9 + 1) + ((F1 + X9) choose (X9 + 1)) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
F1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
F1 + (X9 + 1) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(F1 + (X9 + 1)) choose (X9 + 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
X9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
X9 + 0 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(X9 + 0) choose 0 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
P is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
P + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
X + P is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(X + P) choose P is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
m is non empty set
K26(m) is non empty set
r is Element of m
X is Element of m
P is non empty V40() a_partition of m
proj P is Relation-like non-empty m -defined P -valued non empty Function-like V25(m) quasi_total Element of K26(K27(m,P))
K27(m,P) is Relation-like non empty set
K26(K27(m,P)) is non empty set
(proj P) . r is Element of P
(proj P) . X is Element of P
X9 is Element of P
union P is set
P9 is set
F1 is Element of P
X9 /\ X9 is Element of K26(m)
m is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
r is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
X is set
the_subsets_of_card (m,X) is Element of K26(K26(X))
K26(X) is non empty set
K26(K26(X)) is non empty set
{ b₁ where b₁ is Element of K26(X) : len b₁ = m } is set
K27((the_subsets_of_card (m,X)),r) is Relation-like set
K26(K27((the_subsets_of_card (m,X)),r)) is non empty set
P is Relation-like the_subsets_of_card (m,X) -defined r -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (m,X)),r))
Funcs ((the_subsets_of_card (m,X)),r) is functional set
X9 is set
len X9 is epsilon-transitive epsilon-connected ordinal cardinal set
P9 is non empty set
F1 is Relation-like Function-like set
dom F1 is set
rng F1 is set
K27(omega,P9) is Relation-like non empty V14() non finite set
K26(K27(omega,P9)) is non empty V14() non finite set
len P9 is epsilon-transitive epsilon-connected ordinal non empty cardinal set
card m is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
the_subsets_of_card (m,P9) is Element of K26(K26(P9))
K26(P9) is non empty set
K26(K26(P9)) is non empty set
{ b₁ where b₁ is Element of K26(P9) : len b₁ = m } is set
F1 is Relation-like omega -defined P9 -valued non empty Function-like V25( omega ) quasi_total Element of K26(K27(omega,P9))
(m,omega,P9,F1) is Relation-like the_subsets_of_card (m,omega) -defined the_subsets_of_card (m,P9) -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (m,omega)),(the_subsets_of_card (m,P9))))
the_subsets_of_card (m,omega) is non empty Element of K26(K26(omega))
K26(K26(omega)) is non empty V14() non finite set
{ b₁ where b₁ is Element of K26(omega) : len b₁ = m } is set
K27((the_subsets_of_card (m,omega)),(the_subsets_of_card (m,P9))) is Relation-like set
K26(K27((the_subsets_of_card (m,omega)),(the_subsets_of_card (m,P9)))) is non empty set
Funcs ((the_subsets_of_card (m,omega)),(the_subsets_of_card (m,P9))) is functional set
P * (m,omega,P9,F1) is Relation-like the_subsets_of_card (m,omega) -defined r -valued Function-like Element of K26(K27((the_subsets_of_card (m,omega)),r))
K27((the_subsets_of_card (m,omega)),r) is Relation-like set
K26(K27((the_subsets_of_card (m,omega)),r)) is non empty set
dom (P * (m,omega,P9,F1)) is Element of K26((the_subsets_of_card (m,omega)))
K26((the_subsets_of_card (m,omega))) is non empty set
F is Relation-like Function-like set
dom F is set
rng F is set
S is Relation-like Function-like set
dom S is set
rng S is set
rng (P * (m,omega,P9,F1)) is set
rng P is set
F is Relation-like Function-like set
dom F is set
rng F is set
S is Relation-like Function-like set
dom S is set
rng S is set
F is Relation-like the_subsets_of_card (m,omega) -defined r -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (m,omega)),r))
S is V129() V130() V131() V132() V133() V134() V143() Element of K26(omega)
the_subsets_of_card (m,S) is Element of K26(K26(S))
K26(S) is non empty set
K26(K26(S)) is non empty set
{ b₁ where b₁ is Element of K26(S) : len b₁ = m } is set
F | (the_subsets_of_card (m,S)) is Relation-like the_subsets_of_card (m,omega) -defined the_subsets_of_card (m,S) -defined the_subsets_of_card (m,omega) -defined r -valued Function-like Element of K26(K27((the_subsets_of_card (m,omega)),r))
rng (F | (the_subsets_of_card (m,S))) is set
rng F is set
F1 .: S is set
rng F1 is non empty set
h is Element of K26(X)
the_subsets_of_card (m,h) is Element of K26(K26(h))
K26(h) is non empty set
K26(K26(h)) is non empty set
{ b₁ where b₁ is Element of K26(h) : len b₁ = m } is set
P | (the_subsets_of_card (m,h)) is Relation-like the_subsets_of_card (m,X) -defined the_subsets_of_card (m,h) -defined the_subsets_of_card (m,X) -defined r -valued Function-like Element of K26(K27((the_subsets_of_card (m,X)),r))
dom (F | (the_subsets_of_card (m,S))) is Element of K26((the_subsets_of_card (m,S)))
K26((the_subsets_of_card (m,S))) is non empty set
K27((the_subsets_of_card (m,S)),r) is Relation-like set
K26(K27((the_subsets_of_card (m,S)),r)) is non empty set
E is epsilon-transitive epsilon-connected ordinal Element of r
{E} is non empty V14() finite 1 -element V143() set
rng (P | (the_subsets_of_card (m,h))) is set
P .: (the_subsets_of_card (m,h)) is set
(m,omega,P9,F1) .: (the_subsets_of_card (m,S)) is set
P .: ((m,omega,P9,F1) .: (the_subsets_of_card (m,S))) is set
F .: (the_subsets_of_card (m,S)) is set
E is epsilon-transitive epsilon-connected ordinal Element of r
{E} is non empty V14() finite 1 -element V143() set
m is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
r is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
X is V14() non finite set
the_subsets_of_card (m,X) is non empty Element of K26(K26(X))
K26(X) is non empty V14() non finite set
K26(K26(X)) is non empty V14() non finite set
{ b₁ where b₁ is Element of K26(X) : len b₁ = m } is set
P is non empty V40() a_partition of the_subsets_of_card (m,X)
len P is epsilon-transitive epsilon-connected ordinal non empty cardinal set
X9 is Relation-like Function-like set
dom X9 is set
rng X9 is set
K27(P,r) is Relation-like set
K26(K27(P,r)) is non empty set
proj P is Relation-like non-empty the_subsets_of_card (m,X) -defined P -valued non empty Function-like V25( the_subsets_of_card (m,X)) quasi_total Element of K26(K27((the_subsets_of_card (m,X)),P))
K27((the_subsets_of_card (m,X)),P) is Relation-like non empty set
K26(K27((the_subsets_of_card (m,X)),P)) is non empty set
P9 is Relation-like P -defined r -valued Function-like quasi_total Element of K26(K27(P,r))
P9 * (proj P) is Relation-like the_subsets_of_card (m,X) -defined r -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (m,X)),r))
K27((the_subsets_of_card (m,X)),r) is Relation-like set
K26(K27((the_subsets_of_card (m,X)),r)) is non empty set
F1 is Relation-like the_subsets_of_card (m,X) -defined r -valued Function-like quasi_total Element of K26(K27((the_subsets_of_card (m,X)),r))
F is Element of K26(X)
the_subsets_of_card (m,F) is Element of K26(K26(F))
K26(F) is non empty set
K26(K26(F)) is non empty set
{ b₁ where b₁ is Element of K26(F) : len b₁ = m } is set
F1 | (the_subsets_of_card (m,F)) is Relation-like the_subsets_of_card (m,X) -defined the_subsets_of_card (m,F) -defined the_subsets_of_card (m,X) -defined r -valued Function-like Element of K26(K27((the_subsets_of_card (m,X)),r))
the Element of the_subsets_of_card (m,F) is Element of the_subsets_of_card (m,F)
S is Element of the_subsets_of_card (m,X)
EqClass (S,P) is Element of K26((the_subsets_of_card (m,X)))
K26((the_subsets_of_card (m,X))) is non empty set
h is Element of P
E is set
dom F1 is Element of K26((the_subsets_of_card (m,X)))
(dom F1) /\ (the_subsets_of_card (m,F)) is Element of K26(K26(F))
dom (F1 | (the_subsets_of_card (m,F))) is Element of K26((the_subsets_of_card (m,X)))
E is Element of the_subsets_of_card (m,X)
F1 . E is epsilon-transitive epsilon-connected ordinal Element of r
(F1 | (the_subsets_of_card (m,F))) . E is set
(F1 | (the_subsets_of_card (m,F))) . S is set
F1 . S is epsilon-transitive epsilon-connected ordinal Element of r
(proj P) . E is Element of P
P9 . ((proj P) . E) is epsilon-transitive epsilon-connected ordinal Element of r
(P9 * (proj P)) . S is epsilon-transitive epsilon-connected ordinal Element of r
(proj P) . S is Element of P
P9 . ((proj P) . S) is epsilon-transitive epsilon-connected ordinal Element of r
m is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
m + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
X is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
r + X is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
r - 1 is V16() V17() ext-real set
X - 1 is V16() V17() ext-real set
P is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
P + X is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
X9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
X9 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
r + X9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
P + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
X is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
r + X is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
m is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
r is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
m + r is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
X9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
P9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
X9 + P9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
P is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
X9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
P9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
X9 + P9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
{2} is non empty V14() finite V36() 1 -element V129() V130() V131() V132() V133() V134() V143() set
m is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
m -' 1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
m + r is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
(m + r) -' 2 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
((m + r) -' 2) choose (m -' 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
X + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
P is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
(X + 1) -' 1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(X + 1) + P is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal ext-real positive non negative V143() set
((X + 1) + P) -' 2 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(((X + 1) + P) -' 2) choose ((X + 1) -' 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
P + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
X -' 1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
X + (P + 1) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal ext-real positive non negative V143() set
(X + (P + 1)) -' 2 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
((X + (P + 1)) -' 2) choose (X -' 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(X + 1) + (P + 1) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() finite cardinal ext-real positive non negative V143() set
((X + 1) + (P + 1)) -' 2 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(((X + 1) + (P + 1)) -' 2) choose ((X + 1) -' 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
2 + 2 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(X + 1) + (P + 1) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
4 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
4 - 2 is V16() V17() ext-real set
((X + 1) + (P + 1)) - 2 is V16() V17() ext-real set
X + P is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
((X + 1) + (P + 1)) -' 2 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
2 - 1 is V16() V17() ext-real set
(X + 1) - 1 is V16() V17() ext-real set
(((X + 1) + (P + 1)) -' 2) choose ((X + 1) -' 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
P9 is finite V143() set
the_subsets_of_card (2,P9) is finite V36() V143() Element of K26(K26(P9))
K26(P9) is non empty finite V36() V143() set
K26(K26(P9)) is non empty finite V36() V143() set
{ b₁ where b₁ is Element of K26(P9) : len b₁ = 2 } is set
K27((the_subsets_of_card (2,P9)),(Seg 2)) is Relation-like finite V143() set
K26(K27((the_subsets_of_card (2,P9)),(Seg 2))) is non empty finite V36() V143() set
card P9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
F1 is Relation-like the_subsets_of_card (2,P9) -defined Seg 2 -valued Function-like V25( the_subsets_of_card (2,P9)) quasi_total finite V143() Element of K26(K27((the_subsets_of_card (2,P9)),(Seg 2)))
Funcs ((the_subsets_of_card (2,P9)),(Seg 2)) is non empty functional FUNCTION_DOMAIN of the_subsets_of_card (2,P9), Seg 2
rng F1 is finite V143() set
F1 is finite V143() Element of K26(P9)
card F1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
card 2 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
the_subsets_of_card (2,F1) is finite V36() V143() Element of K26(K26(F1))
K26(F1) is non empty finite V36() V143() set
K26(K26(F1)) is non empty finite V36() V143() set
{ b₁ where b₁ is Element of K26(F1) : len b₁ = 2 } is set
F1 | (the_subsets_of_card (2,F1)) is Relation-like the_subsets_of_card (2,P9) -defined the_subsets_of_card (2,F1) -defined the_subsets_of_card (2,P9) -defined Seg 2 -valued Function-like finite V143() Element of K26(K27((the_subsets_of_card (2,P9)),(Seg 2)))
rng (F1 | (the_subsets_of_card (2,F1))) is finite V143() set
F is Relation-like Function-like set
dom F is set
rng F is set
F is Relation-like Function-like set
dom F is set
rng F is set
F is set
F is set
rng F1 is finite V143() set
dom F1 is finite V36() V143() Element of K26((the_subsets_of_card (2,P9)))
K26((the_subsets_of_card (2,P9))) is non empty finite V36() V143() set
F1 is set
F1 . F1 is set
{ b₁ where b₁ is finite V143() Element of K26(P9) : card b₁ = 2 } is set
F is finite V143() Element of K26(P9)
card F is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
F is finite V143() Element of K26(P9)
the_subsets_of_card (2,F) is finite V36() V143() Element of K26(K26(F))
K26(F) is non empty finite V36() V143() set
K26(K26(F)) is non empty finite V36() V143() set
{ b₁ where b₁ is Element of K26(F) : len b₁ = 2 } is set
{F} is non empty V14() finite V36() 1 -element V143() set
F is finite V143() Element of K26(P9)
card F is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
F1 | (the_subsets_of_card (2,F)) is Relation-like the_subsets_of_card (2,P9) -defined the_subsets_of_card (2,F) -defined the_subsets_of_card (2,P9) -defined Seg 2 -valued Function-like finite V143() Element of K26(K27((the_subsets_of_card (2,P9)),(Seg 2)))
(F1 | (the_subsets_of_card (2,F))) . F is set
card F is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
rng (F1 | (the_subsets_of_card (2,F))) is finite V143() set
dom (F1 | (the_subsets_of_card (2,F))) is finite V36() V143() Element of K26((the_subsets_of_card (2,P9)))
(dom F1) /\ (the_subsets_of_card (2,F)) is finite V36() V143() Element of K26(K26(F))
(dom F1) /\ {F} is finite V36() V143() Element of K26((the_subsets_of_card (2,P9)))
F is finite V143() Element of K26(P9)
card F is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
F is finite V143() Element of K26(P9)
card F is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
rng F1 is finite V143() set
2 - 1 is V16() V17() ext-real set
(P + 1) - 1 is V16() V17() ext-real set
2 + 2 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(X + 1) + (P + 1) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
4 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
4 - 2 is V16() V17() ext-real set
((X + 1) + (P + 1)) - 2 is V16() V17() ext-real set
X + P is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
((X + 1) + (P + 1)) -' 2 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(X + 1) - 1 is V16() V17() ext-real set
(((X + 1) + (P + 1)) -' 2) choose ((X + 1) -' 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
P9 is finite V143() set
the_subsets_of_card (2,P9) is finite V36() V143() Element of K26(K26(P9))
K26(P9) is non empty finite V36() V143() set
K26(K26(P9)) is non empty finite V36() V143() set
{ b₁ where b₁ is Element of K26(P9) : len b₁ = 2 } is set
K27((the_subsets_of_card (2,P9)),(Seg 2)) is Relation-like finite V143() set
K26(K27((the_subsets_of_card (2,P9)),(Seg 2))) is non empty finite V36() V143() set
card P9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
F1 is Relation-like the_subsets_of_card (2,P9) -defined Seg 2 -valued Function-like V25( the_subsets_of_card (2,P9)) quasi_total finite V143() Element of K26(K27((the_subsets_of_card (2,P9)),(Seg 2)))
Funcs ((the_subsets_of_card (2,P9)),(Seg 2)) is non empty functional FUNCTION_DOMAIN of the_subsets_of_card (2,P9), Seg 2
rng F1 is finite V143() set
F1 is finite V143() Element of K26(P9)
card F1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
card 2 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
the_subsets_of_card (2,F1) is finite V36() V143() Element of K26(K26(F1))
K26(F1) is non empty finite V36() V143() set
K26(K26(F1)) is non empty finite V36() V143() set
{ b₁ where b₁ is Element of K26(F1) : len b₁ = 2 } is set
F1 | (the_subsets_of_card (2,F1)) is Relation-like the_subsets_of_card (2,P9) -defined the_subsets_of_card (2,F1) -defined the_subsets_of_card (2,P9) -defined Seg 2 -valued Function-like finite V143() Element of K26(K27((the_subsets_of_card (2,P9)),(Seg 2)))
rng (F1 | (the_subsets_of_card (2,F1))) is finite V143() set
F is Relation-like Function-like set
dom F is set
rng F is set
F is Relation-like Function-like set
dom F is set
rng F is set
F is set
F is set
rng F1 is finite V143() set
dom F1 is finite V36() V143() Element of K26((the_subsets_of_card (2,P9)))
K26((the_subsets_of_card (2,P9))) is non empty finite V36() V143() set
F1 is set
F1 . F1 is set
{ b₁ where b₁ is finite V143() Element of K26(P9) : card b₁ = 2 } is set
F is finite V143() Element of K26(P9)
card F is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
F is finite V143() Element of K26(P9)
the_subsets_of_card (2,F) is finite V36() V143() Element of K26(K26(F))
K26(F) is non empty finite V36() V143() set
K26(K26(F)) is non empty finite V36() V143() set
{ b₁ where b₁ is Element of K26(F) : len b₁ = 2 } is set
{F} is non empty V14() finite V36() 1 -element V143() set
F is finite V143() Element of K26(P9)
card F is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
F1 | (the_subsets_of_card (2,F)) is Relation-like the_subsets_of_card (2,P9) -defined the_subsets_of_card (2,F) -defined the_subsets_of_card (2,P9) -defined Seg 2 -valued Function-like finite V143() Element of K26(K27((the_subsets_of_card (2,P9)),(Seg 2)))
(F1 | (the_subsets_of_card (2,F))) . F is set
card F is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
rng (F1 | (the_subsets_of_card (2,F))) is finite V143() set
dom (F1 | (the_subsets_of_card (2,F))) is finite V36() V143() Element of K26((the_subsets_of_card (2,P9)))
(dom F1) /\ (the_subsets_of_card (2,F)) is finite V36() V143() Element of K26(K26(F))
(dom F1) /\ {F} is finite V36() V143() Element of K26((the_subsets_of_card (2,P9)))
F is finite V143() Element of K26(P9)
card F is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
F is finite V143() Element of K26(P9)
card F is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
rng F1 is finite V143() set
X + P is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
(X + P) -' 1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
2 - 2 is V16() V17() ext-real set
(X + 1) - 2 is V16() V17() ext-real set
X - 1 is V16() V17() ext-real set
(X -' 1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
2 + 2 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(X + 1) + (P + 1) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
4 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
4 - 3 is V16() V17() ext-real set
(X + P) + 2 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
((X + P) + 2) - 3 is V16() V17() ext-real set
(X + P) - 1 is V16() V17() ext-real set
(X + P) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
((X + P) + 1) -' 2 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
((X + P) + 1) - 2 is V16() V17() ext-real set
((X + 1) + (P + 1)) -' 2 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
((X + 1) + (P + 1)) - 2 is V16() V17() ext-real set
((X + P) -' 1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
X + (P + 1) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(X + (P + 1)) -' 2 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
((X + (P + 1)) -' 2) choose (X -' 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
F1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
F1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
(X + 1) + P is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
((X + 1) + P) -' 2 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(((X + 1) + P) -' 2) choose ((X + 1) -' 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
F1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
F1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
F1 + F1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
((((X + 1) + P) -' 2) choose ((X + 1) -' 1)) + (((X + (P + 1)) -' 2) choose (X -' 1)) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
(((X + 1) + (P + 1)) -' 2) choose ((X + 1) -' 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
0 + 2 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
F is finite V143() set
the_subsets_of_card (2,F) is finite V36() V143() Element of K26(K26(F))
K26(F) is non empty finite V36() V143() set
K26(K26(F)) is non empty finite V36() V143() set
{ b₁ where b₁ is Element of K26(F) : len b₁ = 2 } is set
K27((the_subsets_of_card (2,F)),(Seg 2)) is Relation-like finite V143() set
K26(K27((the_subsets_of_card (2,F)),(Seg 2))) is non empty finite V36() V143() set
card F is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
S is Relation-like the_subsets_of_card (2,F) -defined Seg 2 -valued Function-like V25( the_subsets_of_card (2,F)) quasi_total finite V143() Element of K26(K27((the_subsets_of_card (2,F)),(Seg 2)))
h is finite V143() Element of K26(F)
card h is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
h is set
dom S is finite V36() V143() Element of K26((the_subsets_of_card (2,F)))
K26((the_subsets_of_card (2,F))) is non empty finite V36() V143() set
{ b₁ where b₁ is Element of h : ( S . {h,b₁} = 2 & {h,b₁} in dom S ) } is set
{ b₁ where b₁ is Element of h : ( S . {h,b₁} = 1 & {h,b₁} in dom S ) } is set
Funcs ((the_subsets_of_card (2,F)),(Seg 2)) is non empty functional FUNCTION_DOMAIN of the_subsets_of_card (2,F), Seg 2
{ b₁ where b₁ is Element of h : ( S . {h,b₁} = 1 & {h,b₁} in dom S ) } \/ { b₁ where b₁ is Element of h : ( S . {h,b₁} = 2 & {h,b₁} in dom S ) } is set
{h} is non empty V14() finite 1 -element V143() set
h \ {h} is finite V143() Element of K26(F)
x is set
x9 is Element of h
{h,x9} is non empty finite V143() set
S . {h,x9} is set
{x9} is non empty V14() finite 1 -element V143() set
{h} \/ {x9} is non empty finite V143() set
x99 is finite V143() Element of K26(F)
card x99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x9 is Element of h
{h,x9} is non empty finite V143() set
S . {h,x9} is set
{x9} is non empty V14() finite 1 -element V143() set
{h} \/ {x9} is non empty finite V143() set
x99 is finite V143() Element of K26(F)
card x99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x9 is Element of h
{h,x9} is non empty finite V143() set
card {h,x9} is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
x99 is Relation-like Function-like set
dom x99 is set
rng x99 is set
S . {h,x9} is set
rng S is finite V143() set
x99 is Relation-like Function-like set
dom x99 is set
rng x99 is set
{ b₁ where b₁ is Element of h : ( S . {h,b₁} = 1 & {h,b₁} in dom S ) } /\ { b₁ where b₁ is Element of h : ( S . {h,b₁} = 2 & {h,b₁} in dom S ) } is set
x is set
x9 is Element of h
{h,x9} is non empty finite V143() set
S . {h,x9} is set
x99 is Element of h
{h,x99} is non empty finite V143() set
S . {h,x99} is set
card (h \ {h}) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
card {h} is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
(card h) - (card {h}) is V16() V17() ext-real set
(F1 + F1) - 1 is V16() V17() ext-real set
K26(h) is non empty finite V36() V143() set
x9 is finite V143() Element of K26(h)
x is finite V143() Element of K26(h)
x9 \/ x is finite V143() Element of K26(h)
card (x9 \/ x) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
card x9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
card x is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
(card x9) + (card x) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
card {} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V16() V17() V18() Function-like one-to-one constant functional finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V118() V129() V130() V131() V132() V133() V134() V135() V140() V143() Element of omega
((card x9) + (card x)) - (card {}) is V16() V17() ext-real non negative set
(card x9) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
F1 + F1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
((card x9) + 1) + (card x) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
the_subsets_of_card (2,x9) is finite V36() V143() Element of K26(K26(x9))
K26(x9) is non empty finite V36() V143() set
K26(K26(x9)) is non empty finite V36() V143() set
{ b₁ where b₁ is Element of K26(x9) : len b₁ = 2 } is set
S | (the_subsets_of_card (2,x9)) is Relation-like the_subsets_of_card (2,F) -defined the_subsets_of_card (2,x9) -defined the_subsets_of_card (2,F) -defined Seg 2 -valued Function-like finite V143() Element of K26(K27((the_subsets_of_card (2,F)),(Seg 2)))
(the_subsets_of_card (2,F)) /\ (the_subsets_of_card (2,x9)) is finite V36() V143() Element of K26(K26(x9))
dom (S | (the_subsets_of_card (2,x9))) is finite V36() V143() Element of K26((the_subsets_of_card (2,F)))
F9 is Relation-like Function-like set
dom F9 is set
rng F9 is set
rng (S | (the_subsets_of_card (2,x9))) is finite V143() set
rng S is finite V143() set
K27((the_subsets_of_card (2,x9)),(Seg 2)) is Relation-like finite V143() set
K26(K27((the_subsets_of_card (2,x9)),(Seg 2))) is non empty finite V36() V143() set
S9 is Relation-like Function-like set
dom S9 is set
rng S9 is set
F9 is Relation-like the_subsets_of_card (2,x9) -defined Seg 2 -valued Function-like V25( the_subsets_of_card (2,x9)) quasi_total finite V143() Element of K26(K27((the_subsets_of_card (2,x9)),(Seg 2)))
S9 is finite V143() Element of K26(x9)
card S9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
the_subsets_of_card (2,S9) is finite V36() V143() Element of K26(K26(S9))
K26(S9) is non empty finite V36() V143() set
K26(K26(S9)) is non empty finite V36() V143() set
{ b₁ where b₁ is Element of K26(S9) : len b₁ = 2 } is set
F9 | (the_subsets_of_card (2,S9)) is Relation-like the_subsets_of_card (2,x9) -defined the_subsets_of_card (2,S9) -defined the_subsets_of_card (2,x9) -defined Seg 2 -valued Function-like finite V143() Element of K26(K27((the_subsets_of_card (2,x9)),(Seg 2)))
rng (F9 | (the_subsets_of_card (2,S9))) is finite V143() set
S | (the_subsets_of_card (2,S9)) is Relation-like the_subsets_of_card (2,F) -defined the_subsets_of_card (2,S9) -defined the_subsets_of_card (2,F) -defined Seg 2 -valued Function-like finite V143() Element of K26(K27((the_subsets_of_card (2,F)),(Seg 2)))
S9 is finite V143() Element of K26(F)
card S9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
the_subsets_of_card (2,S9) is finite V36() V143() Element of K26(K26(S9))
K26(S9) is non empty finite V36() V143() set
K26(K26(S9)) is non empty finite V36() V143() set
{ b₁ where b₁ is Element of K26(S9) : len b₁ = 2 } is set
F9 | (the_subsets_of_card (2,S9)) is Relation-like the_subsets_of_card (2,x9) -defined the_subsets_of_card (2,S9) -defined the_subsets_of_card (2,x9) -defined Seg 2 -valued Function-like finite V143() Element of K26(K27((the_subsets_of_card (2,x9)),(Seg 2)))
rng (F9 | (the_subsets_of_card (2,S9))) is finite V143() set
S | (the_subsets_of_card (2,S9)) is Relation-like the_subsets_of_card (2,F) -defined the_subsets_of_card (2,S9) -defined the_subsets_of_card (2,F) -defined Seg 2 -valued Function-like finite V143() Element of K26(K27((the_subsets_of_card (2,F)),(Seg 2)))
rng (S | (the_subsets_of_card (2,S9))) is finite V143() set
S9 is finite V143() Element of K26(F)
card S9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
the_subsets_of_card (2,S9) is finite V36() V143() Element of K26(K26(S9))
K26(S9) is non empty finite V36() V143() set
K26(K26(S9)) is non empty finite V36() V143() set
{ b₁ where b₁ is Element of K26(S9) : len b₁ = 2 } is set
F9 | (the_subsets_of_card (2,S9)) is Relation-like the_subsets_of_card (2,x9) -defined the_subsets_of_card (2,S9) -defined the_subsets_of_card (2,x9) -defined Seg 2 -valued Function-like finite V143() Element of K26(K27((the_subsets_of_card (2,x9)),(Seg 2)))
rng (F9 | (the_subsets_of_card (2,S9))) is finite V143() set
S9 \/ {h} is non empty finite V143() set
S99 is finite V143() Element of K26(F)
the_subsets_of_card (2,S99) is finite V36() V143() Element of K26(K26(S99))
K26(S99) is non empty finite V36() V143() set
K26(K26(S99)) is non empty finite V36() V143() set
{ b₁ where b₁ is Element of K26(S99) : len b₁ = 2 } is set
S | (the_subsets_of_card (2,S9)) is Relation-like the_subsets_of_card (2,F) -defined the_subsets_of_card (2,S9) -defined the_subsets_of_card (2,F) -defined Seg 2 -valued Function-like finite V143() Element of K26(K27((the_subsets_of_card (2,F)),(Seg 2)))
rng (S | (the_subsets_of_card (2,S9))) is finite V143() set
S | (the_subsets_of_card (2,S99)) is Relation-like the_subsets_of_card (2,F) -defined the_subsets_of_card (2,S99) -defined the_subsets_of_card (2,F) -defined Seg 2 -valued Function-like finite V143() Element of K26(K27((the_subsets_of_card (2,F)),(Seg 2)))
rng (S | (the_subsets_of_card (2,S99))) is finite V143() set
c₂₄ is set
dom (S | (the_subsets_of_card (2,S99))) is finite V36() V143() Element of K26((the_subsets_of_card (2,F)))
x is set
(S | (the_subsets_of_card (2,S99))) . x is set
{ b₁ where b₁ is finite V143() Element of K26(S99) : card b₁ = 2 } is set
S999 is finite V143() Element of K26(S99)
card S999 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
s1 is set
s2 is set
{s1,s2} is non empty finite V143() set
x is finite V143() Element of K26(S9)
dom (S | (the_subsets_of_card (2,S9))) is finite V36() V143() Element of K26((the_subsets_of_card (2,F)))
(S | (the_subsets_of_card (2,S99))) | (the_subsets_of_card (2,S9)) is Relation-like the_subsets_of_card (2,F) -defined the_subsets_of_card (2,S9) -defined the_subsets_of_card (2,F) -defined Seg 2 -valued Function-like finite V143() Element of K26(K27((the_subsets_of_card (2,F)),(Seg 2)))
dom ((S | (the_subsets_of_card (2,S99))) | (the_subsets_of_card (2,S9))) is finite V36() V143() Element of K26((the_subsets_of_card (2,F)))
(S | (the_subsets_of_card (2,S9))) . x is set
((S | (the_subsets_of_card (2,S99))) | (the_subsets_of_card (2,S9))) . x is set
(S | (the_subsets_of_card (2,S99))) . x is set
{s1,h} is non empty finite V143() set
x is Element of h
{h,x} is non empty finite V143() set
S . {h,x} is set
S . x is set
x is Element of h
{h,x} is non empty finite V143() set
S . {h,x} is set
card S99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
{h,h} is non empty finite V143() set
{h} \/ {h} is non empty finite V143() set
c₂₄ is Element of h
{h,c₂₄} is non empty finite V143() set
S . {h,c₂₄} is set
c₂₄ is finite V143() Element of K26(F)
card c₂₄ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
(card S9) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S9 is finite V143() Element of K26(F)
card S9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
the_subsets_of_card (2,S9) is finite V36() V143() Element of K26(K26(S9))
K26(S9) is non empty finite V36() V143() set
K26(K26(S9)) is non empty finite V36() V143() set
{ b₁ where b₁ is Element of K26(S9) : len b₁ = 2 } is set
F9 | (the_subsets_of_card (2,S9)) is Relation-like the_subsets_of_card (2,x9) -defined the_subsets_of_card (2,S9) -defined the_subsets_of_card (2,x9) -defined Seg 2 -valued Function-like finite V143() Element of K26(K27((the_subsets_of_card (2,x9)),(Seg 2)))
rng (F9 | (the_subsets_of_card (2,S9))) is finite V143() set
the_subsets_of_card (2,x) is finite V36() V143() Element of K26(K26(x))
K26(x) is non empty finite V36() V143() set
K26(K26(x)) is non empty finite V36() V143() set
{ b₁ where b₁ is Element of K26(x) : len b₁ = 2 } is set
S | (the_subsets_of_card (2,x)) is Relation-like the_subsets_of_card (2,F) -defined the_subsets_of_card (2,x) -defined the_subsets_of_card (2,F) -defined Seg 2 -valued Function-like finite V143() Element of K26(K27((the_subsets_of_card (2,F)),(Seg 2)))
(the_subsets_of_card (2,F)) /\ (the_subsets_of_card (2,x)) is finite V36() V143() Element of K26(K26(x))
dom (S | (the_subsets_of_card (2,x))) is finite V36() V143() Element of K26((the_subsets_of_card (2,F)))
F9 is Relation-like Function-like set
dom F9 is set
rng F9 is set
rng (S | (the_subsets_of_card (2,x))) is finite V143() set
rng S is finite V143() set
K27((the_subsets_of_card (2,x)),(Seg 2)) is Relation-like finite V143() set
K26(K27((the_subsets_of_card (2,x)),(Seg 2))) is non empty finite V36() V143() set
S9 is Relation-like Function-like set
dom S9 is set
rng S9 is set
F9 is Relation-like the_subsets_of_card (2,x) -defined Seg 2 -valued Function-like V25( the_subsets_of_card (2,x)) quasi_total finite V143() Element of K26(K27((the_subsets_of_card (2,x)),(Seg 2)))
S9 is finite V143() Element of K26(x)
card S9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
the_subsets_of_card (2,S9) is finite V36() V143() Element of K26(K26(S9))
K26(S9) is non empty finite V36() V143() set
K26(K26(S9)) is non empty finite V36() V143() set
{ b₁ where b₁ is Element of K26(S9) : len b₁ = 2 } is set
F9 | (the_subsets_of_card (2,S9)) is Relation-like the_subsets_of_card (2,x) -defined the_subsets_of_card (2,S9) -defined the_subsets_of_card (2,x) -defined Seg 2 -valued Function-like finite V143() Element of K26(K27((the_subsets_of_card (2,x)),(Seg 2)))
rng (F9 | (the_subsets_of_card (2,S9))) is finite V143() set
S | (the_subsets_of_card (2,S9)) is Relation-like the_subsets_of_card (2,F) -defined the_subsets_of_card (2,S9) -defined the_subsets_of_card (2,F) -defined Seg 2 -valued Function-like finite V143() Element of K26(K27((the_subsets_of_card (2,F)),(Seg 2)))
S9 is finite V143() Element of K26(F)
card S9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
the_subsets_of_card (2,S9) is finite V36() V143() Element of K26(K26(S9))
K26(S9) is non empty finite V36() V143() set
K26(K26(S9)) is non empty finite V36() V143() set
{ b₁ where b₁ is Element of K26(S9) : len b₁ = 2 } is set
F9 | (the_subsets_of_card (2,S9)) is Relation-like the_subsets_of_card (2,x) -defined the_subsets_of_card (2,S9) -defined the_subsets_of_card (2,x) -defined Seg 2 -valued Function-like finite V143() Element of K26(K27((the_subsets_of_card (2,x)),(Seg 2)))
rng (F9 | (the_subsets_of_card (2,S9))) is finite V143() set
S | (the_subsets_of_card (2,S9)) is Relation-like the_subsets_of_card (2,F) -defined the_subsets_of_card (2,S9) -defined the_subsets_of_card (2,F) -defined Seg 2 -valued Function-like finite V143() Element of K26(K27((the_subsets_of_card (2,F)),(Seg 2)))
rng (S | (the_subsets_of_card (2,S9))) is finite V143() set
S9 is finite V143() Element of K26(F)
card S9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
the_subsets_of_card (2,S9) is finite V36() V143() Element of K26(K26(S9))
K26(S9) is non empty finite V36() V143() set
K26(K26(S9)) is non empty finite V36() V143() set
{ b₁ where b₁ is Element of K26(S9) : len b₁ = 2 } is set
F9 | (the_subsets_of_card (2,S9)) is Relation-like the_subsets_of_card (2,x) -defined the_subsets_of_card (2,S9) -defined the_subsets_of_card (2,x) -defined Seg 2 -valued Function-like finite V143() Element of K26(K27((the_subsets_of_card (2,x)),(Seg 2)))
rng (F9 | (the_subsets_of_card (2,S9))) is finite V143() set
S9 \/ {h} is non empty finite V143() set
S99 is finite V143() Element of K26(F)
the_subsets_of_card (2,S99) is finite V36() V143() Element of K26(K26(S99))
K26(S99) is non empty finite V36() V143() set
K26(K26(S99)) is non empty finite V36() V143() set
{ b₁ where b₁ is Element of K26(S99) : len b₁ = 2 } is set
S | (the_subsets_of_card (2,S9)) is Relation-like the_subsets_of_card (2,F) -defined the_subsets_of_card (2,S9) -defined the_subsets_of_card (2,F) -defined Seg 2 -valued Function-like finite V143() Element of K26(K27((the_subsets_of_card (2,F)),(Seg 2)))
rng (S | (the_subsets_of_card (2,S9))) is finite V143() set
S | (the_subsets_of_card (2,S99)) is Relation-like the_subsets_of_card (2,F) -defined the_subsets_of_card (2,S99) -defined the_subsets_of_card (2,F) -defined Seg 2 -valued Function-like finite V143() Element of K26(K27((the_subsets_of_card (2,F)),(Seg 2)))
rng (S | (the_subsets_of_card (2,S99))) is finite V143() set
c₂₄ is set
dom (S | (the_subsets_of_card (2,S99))) is finite V36() V143() Element of K26((the_subsets_of_card (2,F)))
x is set
(S | (the_subsets_of_card (2,S99))) . x is set
{ b₁ where b₁ is finite V143() Element of K26(S99) : card b₁ = 2 } is set
S999 is finite V143() Element of K26(S99)
card S999 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
s1 is set
s2 is set
{s1,s2} is non empty finite V143() set
x is finite V143() Element of K26(S9)
dom (S | (the_subsets_of_card (2,S9))) is finite V36() V143() Element of K26((the_subsets_of_card (2,F)))
(S | (the_subsets_of_card (2,S99))) | (the_subsets_of_card (2,S9)) is Relation-like the_subsets_of_card (2,F) -defined the_subsets_of_card (2,S9) -defined the_subsets_of_card (2,F) -defined Seg 2 -valued Function-like finite V143() Element of K26(K27((the_subsets_of_card (2,F)),(Seg 2)))
dom ((S | (the_subsets_of_card (2,S99))) | (the_subsets_of_card (2,S9))) is finite V36() V143() Element of K26((the_subsets_of_card (2,F)))
(S | (the_subsets_of_card (2,S9))) . x is set
((S | (the_subsets_of_card (2,S99))) | (the_subsets_of_card (2,S9))) . x is set
(S | (the_subsets_of_card (2,S99))) . x is set
{s1,h} is non empty finite V143() set
x is Element of h
{h,x} is non empty finite V143() set
S . {h,x} is set
S . x is set
x is Element of h
{h,x} is non empty finite V143() set
S . {h,x} is set
card S99 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
{h,h} is non empty finite V143() set
{h} \/ {h} is non empty finite V143() set
c₂₄ is Element of h
{h,c₂₄} is non empty finite V143() set
S . {h,c₂₄} is set
c₂₄ is finite V143() Element of K26(F)
card c₂₄ is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
(card S9) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
S9 is finite V143() Element of K26(F)
card S9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
the_subsets_of_card (2,S9) is finite V36() V143() Element of K26(K26(S9))
K26(S9) is non empty finite V36() V143() set
K26(K26(S9)) is non empty finite V36() V143() set
{ b₁ where b₁ is Element of K26(S9) : len b₁ = 2 } is set
F9 | (the_subsets_of_card (2,S9)) is Relation-like the_subsets_of_card (2,x) -defined the_subsets_of_card (2,S9) -defined the_subsets_of_card (2,x) -defined Seg 2 -valued Function-like finite V143() Element of K26(K27((the_subsets_of_card (2,x)),(Seg 2)))
rng (F9 | (the_subsets_of_card (2,S9))) is finite V143() set
0 -' 1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
0 + X is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
(0 + X) -' 2 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
((0 + X) -' 2) choose (0 -' 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
P is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
P -' 1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
P + 0 is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
(P + 0) -' 2 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
((P + 0) -' 2) choose (P -' 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
X is finite V143() set
the_subsets_of_card (2,X) is finite V36() V143() Element of K26(K26(X))
K26(X) is non empty finite V36() V143() set
K26(K26(X)) is non empty finite V36() V143() set
{ b₁ where b₁ is Element of K26(X) : len b₁ = 2 } is set
card X is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
P is finite V36() V40() V143() a_partition of the_subsets_of_card (2,X)
card P is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
X9 is set
{X9} is non empty V14() finite 1 -element V143() set
P9 is finite V143() Element of K26(X)
card P9 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
the_subsets_of_card (2,P9) is finite V36() V143() Element of K26(K26(P9))
K26(P9) is non empty finite V36() V143() set
K26(K26(P9)) is non empty finite V36() V143() set
{ b₁ where b₁ is Element of K26(P9) : len b₁ = 2 } is set
the finite V143() Element of P is finite V143() Element of P
F1 is finite V143() Element of P
m -' 1 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
m + m is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
(m + m) -' 2 is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
((m + m) -' 2) choose (m -' 1) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V16() V17() finite cardinal ext-real non negative V143() set
X is finite V143() set
the_subsets_of_card (2,X) is finite V36() V143() Element of K26(K26(X))
K26(X) is non empty finite V36() V143() set
K26(K26(X)) is non empty finite V36() V143() set
{ b₁ where b₁ is Element of K26(X) : len b₁ = 2 } is set
card X is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
P is finite V36() V40() V143() a_partition of the_subsets_of_card (2,X)
card P is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
card (Seg 2) is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
card 2 is epsilon-transitive epsilon-connected ordinal natural non empty V16() V17() V18() finite cardinal ext-real positive non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
X9 is non empty set
P9 is non empty V40() a_partition of X9
len P9 is epsilon-transitive epsilon-connected ordinal non empty cardinal set
F1 is Relation-like Function-like set
dom F1 is set
rng F1 is set
K27(P9,(Seg 2)) is Relation-like non empty set
K26(K27(P9,(Seg 2))) is non empty set
proj P9 is Relation-like non-empty X9 -defined P9 -valued non empty Function-like V25(X9) quasi_total Element of K26(K27(X9,P9))
K27(X9,P9) is Relation-like non empty set
K26(K27(X9,P9)) is non empty set
F1 is Relation-like P9 -defined Seg 2 -valued non empty Function-like V25(P9) quasi_total Element of K26(K27(P9,(Seg 2)))
F1 * (proj P9) is Relation-like X9 -defined Seg 2 -valued non empty Function-like V25(X9) quasi_total Element of K26(K27(X9,(Seg 2)))
K27(X9,(Seg 2)) is Relation-like non empty set
K26(K27(X9,(Seg 2))) is non empty set
K27((the_subsets_of_card (2,X)),(Seg 2)) is Relation-like finite V143() set
K26(K27((the_subsets_of_card (2,X)),(Seg 2))) is non empty finite V36() V143() set
F is Relation-like the_subsets_of_card (2,X) -defined Seg 2 -valued Function-like V25( the_subsets_of_card (2,X)) quasi_total finite V143() Element of K26(K27((the_subsets_of_card (2,X)),(Seg 2)))
S is finite V143() Element of K26(X)
card S is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V129() V130() V131() V132() V133() V134() V143() Element of omega
the_subsets_of_card (2,S) is finite V36() V143() Element of K26(K26(S))
K26(S) is non empty finite V36() V143() set
K26(K26(S)) is non empty finite V36() V143() set
{ b₁ where b₁ is Element of K26(S) : len b₁ = 2 } is set
F | (the_subsets_of_card (2,S)) is Relation-like the_subsets_of_card (2,X) -defined the_subsets_of_card (2,S) -defined the_subsets_of_card (2,X) -defined Seg 2 -valued Function-like finite V143() Element of K26(K27((the_subsets_of_card (2,X)),(Seg 2)))
rng (F | (the_subsets_of_card (2,S))) is finite V143() set
the finite V143() Element of the_subsets_of_card (2,S) is finite V143() Element of the_subsets_of_card (2,S)
h is Element of X9
EqClass (h,P9) is Element of K26(X9)
K26(X9) is non empty set
E is finite V143() Element of P
x is set
dom F is finite V36() V143() Element of K26((the_subsets_of_card (2,X)))
K26((the_subsets_of_card (2,X))) is non empty finite V36() V143() set
(dom F) /\ (the_subsets_of_card (2,S)) is finite V36() V143() Element of K26(K26(S))
dom (F | (the_subsets_of_card (2,S))) is finite V36() V143() Element of K26((the_subsets_of_card (2,X)))
x9 is finite V143() Element of the_subsets_of_card (2,X)
F . x9 is set
(F | (the_subsets_of_card (2,S))) . x9 is set
(F | (the_subsets_of_card (2,S))) . h is set
F . h is set
(proj P9) . x9 is set
F1 . ((proj P9) . x9) is set
(F1 * (proj P9)) . h is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V143() Element of Seg 2
(proj P9) . h is Element of P9
F1 . ((proj P9) . h) is epsilon-transitive epsilon-connected ordinal natural V16() V17() V18() finite cardinal ext-real non negative V118() V143() Element of Seg 2
x99 is Element of X9
(proj P9) . x99 is Element of P9