REAL is set
NAT is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal countable denumerable V54() Element of bool REAL
bool REAL is non empty cup-closed diff-closed preBoolean set
omega is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal countable denumerable V54() set
bool omega is non empty non trivial non finite V54() cup-closed diff-closed preBoolean set
{} is Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty trivial Function-yielding V29() ext-real V36() V37() finite finite-yielding V42() cardinal {} -element Cardinal-yielding countable set
the Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty trivial Function-yielding V29() ext-real V36() V37() finite finite-yielding V42() cardinal {} -element Cardinal-yielding countable set is Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty trivial Function-yielding V29() ext-real V36() V37() finite finite-yielding V42() cardinal {} -element Cardinal-yielding countable set
1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of NAT
{{}} is functional non empty trivial finite V42() 1 -element with_common_domain countable set
card {} is Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty trivial Function-yielding V29() ext-real V36() V37() finite finite-yielding V42() cardinal {} -element Cardinal-yielding countable set
card omega is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal V54() set
2 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of NAT
{{},1} is non empty finite V42() countable set
0 is Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty trivial Function-yielding V29() ext-real V36() V37() finite finite-yielding V42() cardinal {} -element Cardinal-yielding countable Element of NAT
union {} is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
Rank {} is set
F is set
g is set
x is set
x is Relation-like Function-like set
proj1 x is set
proj2 x is set
x . F is set
F is set
bool F is non empty cup-closed diff-closed preBoolean set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
bool (card F) is non empty cup-closed diff-closed preBoolean set
card (bool F) is epsilon-transitive epsilon-connected ordinal non empty cardinal set
card (bool (card F)) is epsilon-transitive epsilon-connected ordinal non empty cardinal set
g is Relation-like Function-like set
proj1 g is set
proj2 g is set
x is Relation-like Function-like set
proj1 x is set
proj2 x is set
x is set
x . x is set
A is set
x . A is set
g .: x is set
g .: A is set
x9 is set
g . x9 is set
f9 is set
g . f9 is set
x9 is set
g . x9 is set
f9 is set
g . f9 is set
x is set
A is set
x . A is set
g .: A is set
x is set
g " x is set
g .: (g " x) is set
x . (g " x) is set
F is set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
g is set
card g is epsilon-transitive epsilon-connected ordinal cardinal set
x is set
Funcs (g,x) is functional set
x is Relation-like Function-like set
proj1 x is set
proj2 x is set
A is Relation-like Function-like set
proj1 A is set
proj2 A is set
x9 is set
A . x9 is set
f9 is set
A . f9 is set
x9 `1 is set
f9 `1 is set
f9 `2 is set
[(f9 `1),(f9 `2)] is non empty V22() set
{(f9 `1),(f9 `2)} is non empty finite countable set
{(f9 `1)} is non empty trivial finite 1 -element countable set
{{(f9 `1),(f9 `2)},{(f9 `1)}} is non empty finite V42() countable V53() V54() set
N is set
K is set
[N,K] is non empty V22() set
{N,K} is non empty finite countable set
{N} is non empty trivial finite 1 -element countable set
{{N,K},{N}} is non empty finite V42() countable V53() V54() set
x9 `2 is set
[(x9 `1),(x9 `2)] is non empty V22() set
{(x9 `1),(x9 `2)} is non empty finite countable set
{(x9 `1)} is non empty trivial finite 1 -element countable set
{{(x9 `1),(x9 `2)},{(x9 `1)}} is non empty finite V42() countable V53() V54() set
N is set
K is set
[N,K] is non empty V22() set
{N,K} is non empty finite countable set
{N} is non empty trivial finite 1 -element countable set
{{N,K},{N}} is non empty finite V42() countable V53() V54() set
x . (x9 `1) is set
x9 is set
f9 is set
A . f9 is set
f9 `1 is set
f9 `2 is set
[(f9 `1),(f9 `2)] is non empty V22() set
{(f9 `1),(f9 `2)} is non empty finite countable set
{(f9 `1)} is non empty trivial finite 1 -element countable set
{{(f9 `1),(f9 `2)},{(f9 `1)}} is non empty finite V42() countable V53() V54() set
N is set
K is set
[N,K] is non empty V22() set
{N,K} is non empty finite countable set
{N} is non empty trivial finite 1 -element countable set
{{N,K},{N}} is non empty finite V42() countable V53() V54() set
x9 is set
x . x9 is set
[x9,(x . x9)] is non empty V22() set
{x9,(x . x9)} is non empty finite countable set
{x9} is non empty trivial finite 1 -element countable set
{{x9,(x . x9)},{x9}} is non empty finite V42() countable V53() V54() set
A . [x9,(x . x9)] is set
[x9,(x . x9)] `1 is set
F is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
F +^ g is epsilon-transitive epsilon-connected ordinal set
card (F +^ g) is epsilon-transitive epsilon-connected ordinal cardinal set
x is set
{x} is non empty trivial finite 1 -element countable set
[:F,{x}:] is Relation-like set
x is set
{x} is non empty trivial finite 1 -element countable set
[:g,{x}:] is Relation-like set
[:F,{x}:] \/ [:g,{x}:] is Relation-like set
card ([:F,{x}:] \/ [:g,{x}:]) is epsilon-transitive epsilon-connected ordinal cardinal set
A is Relation-like Function-like set
proj1 A is set
proj2 A is set
x9 is set
A . x9 is set
f9 is set
A . f9 is set
[x9,x] is non empty V22() set
{x9,x} is non empty finite countable set
{x9} is non empty trivial finite 1 -element countable set
{{x9,x},{x9}} is non empty finite V42() countable V53() V54() set
[x9,x] `1 is set
N is epsilon-transitive epsilon-connected ordinal set
A . N is set
K is epsilon-transitive epsilon-connected ordinal set
A . K is set
[f9,x] is non empty V22() set
{f9,x} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,x},{f9}} is non empty finite V42() countable V53() V54() set
N is epsilon-transitive epsilon-connected ordinal set
N -^ F is epsilon-transitive epsilon-connected ordinal set
[(N -^ F),x] is non empty V22() set
{(N -^ F),x} is non empty finite countable set
{(N -^ F)} is non empty trivial finite 1 -element countable set
{{(N -^ F),x},{(N -^ F)}} is non empty finite V42() countable V53() V54() set
[(N -^ F),x] `1 is set
K is epsilon-transitive epsilon-connected ordinal set
K -^ F is epsilon-transitive epsilon-connected ordinal set
[(K -^ F),x] is non empty V22() set
{(K -^ F),x} is non empty finite countable set
{(K -^ F)} is non empty trivial finite 1 -element countable set
{{(K -^ F),x},{(K -^ F)}} is non empty finite V42() countable V53() V54() set
F +^ (N -^ F) is epsilon-transitive epsilon-connected ordinal set
[x9,x] is non empty V22() set
{x9,x} is non empty finite countable set
{x9} is non empty trivial finite 1 -element countable set
{{x9,x},{x9}} is non empty finite V42() countable V53() V54() set
[x9,x] `2 is set
K is epsilon-transitive epsilon-connected ordinal set
K -^ F is epsilon-transitive epsilon-connected ordinal set
[(K -^ F),x] is non empty V22() set
{(K -^ F),x} is non empty finite countable set
{(K -^ F)} is non empty trivial finite 1 -element countable set
{{(K -^ F),x},{(K -^ F)}} is non empty finite V42() countable V53() V54() set
[f9,x] is non empty V22() set
{f9,x} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,x},{f9}} is non empty finite V42() countable V53() V54() set
[f9,x] `2 is set
N is epsilon-transitive epsilon-connected ordinal set
N -^ F is epsilon-transitive epsilon-connected ordinal set
[(N -^ F),x] is non empty V22() set
{(N -^ F),x} is non empty finite countable set
{(N -^ F)} is non empty trivial finite 1 -element countable set
{{(N -^ F),x},{(N -^ F)}} is non empty finite V42() countable V53() V54() set
x9 is set
f9 is set
A . f9 is set
N is epsilon-transitive epsilon-connected ordinal set
[N,x] is non empty V22() set
{N,x} is non empty finite countable set
{N} is non empty trivial finite 1 -element countable set
{{N,x},{N}} is non empty finite V42() countable V53() V54() set
N is epsilon-transitive epsilon-connected ordinal set
N -^ F is epsilon-transitive epsilon-connected ordinal set
F +^ (N -^ F) is epsilon-transitive epsilon-connected ordinal set
[(N -^ F),x] is non empty V22() set
{(N -^ F),x} is non empty finite countable set
{(N -^ F)} is non empty trivial finite 1 -element countable set
{{(N -^ F),x},{(N -^ F)}} is non empty finite V42() countable V53() V54() set
x9 is set
f9 is set
N is set
[f9,N] is non empty V22() set
{f9,N} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,N},{f9}} is non empty finite V42() countable V53() V54() set
K is epsilon-transitive epsilon-connected ordinal set
F +^ K is epsilon-transitive epsilon-connected ordinal set
(F +^ K) -^ F is epsilon-transitive epsilon-connected ordinal set
A . (F +^ K) is set
f9 is set
N is set
[f9,N] is non empty V22() set
{f9,N} is non empty finite countable set
{f9} is non empty trivial finite 1 -element countable set
{{f9,N},{f9}} is non empty finite V42() countable V53() V54() set
A . f9 is set
{0} is functional non empty trivial finite V42() 1 -element with_common_domain countable set
{1} is non empty trivial finite V42() 1 -element countable V53() V54() set
F is set
g is set
[:F,g:] is Relation-like set
[:g,F:] is Relation-like set
card [:F,g:] is epsilon-transitive epsilon-connected ordinal cardinal set
card [:g,F:] is epsilon-transitive epsilon-connected ordinal cardinal set
x is Relation-like Function-like set
proj1 x is set
proj2 x is set
x is set
x . x is set
A is set
x . A is set
x `1 is set
x `2 is set
[(x `1),(x `2)] is non empty V22() set
{(x `1),(x `2)} is non empty finite countable set
{(x `1)} is non empty trivial finite 1 -element countable set
{{(x `1),(x `2)},{(x `1)}} is non empty finite V42() countable V53() V54() set
A `1 is set
A `2 is set
[(A `1),(A `2)] is non empty V22() set
{(A `1),(A `2)} is non empty finite countable set
{(A `1)} is non empty trivial finite 1 -element countable set
{{(A `1),(A `2)},{(A `1)}} is non empty finite V42() countable V53() V54() set
[(x `2),(x `1)] is non empty V22() set
{(x `2),(x `1)} is non empty finite countable set
{(x `2)} is non empty trivial finite 1 -element countable set
{{(x `2),(x `1)},{(x `2)}} is non empty finite V42() countable V53() V54() set
[(A `2),(A `1)] is non empty V22() set
{(A `2),(A `1)} is non empty finite countable set
{(A `2)} is non empty trivial finite 1 -element countable set
{{(A `2),(A `1)},{(A `2)}} is non empty finite V42() countable V53() V54() set
x is set
A is set
x . A is set
A `2 is set
A `1 is set
[(A `2),(A `1)] is non empty V22() set
{(A `2),(A `1)} is non empty finite countable set
{(A `2)} is non empty trivial finite 1 -element countable set
{{(A `2),(A `1)},{(A `2)}} is non empty finite V42() countable V53() V54() set
x is set
x `2 is set
x `1 is set
[(x `2),(x `1)] is non empty V22() set
{(x `2),(x `1)} is non empty finite countable set
{(x `2)} is non empty trivial finite 1 -element countable set
{{(x `2),(x `1)},{(x `2)}} is non empty finite V42() countable V53() V54() set
[(x `2),(x `1)] `1 is set
[(x `2),(x `1)] `2 is set
[(x `1),(x `2)] is non empty V22() set
{(x `1),(x `2)} is non empty finite countable set
{(x `1)} is non empty trivial finite 1 -element countable set
{{(x `1),(x `2)},{(x `1)}} is non empty finite V42() countable V53() V54() set
x . [(x `2),(x `1)] is set
F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal cardinal set
F +^ g is epsilon-transitive epsilon-connected ordinal set
card (F +^ g) is epsilon-transitive epsilon-connected ordinal cardinal set
x is epsilon-transitive epsilon-connected ordinal cardinal set
x is epsilon-transitive epsilon-connected ordinal cardinal set
A is epsilon-transitive epsilon-connected ordinal cardinal set
x +^ A is epsilon-transitive epsilon-connected ordinal set
card (x +^ A) is epsilon-transitive epsilon-connected ordinal cardinal set
A +^ x is epsilon-transitive epsilon-connected ordinal set
card (A +^ x) is epsilon-transitive epsilon-connected ordinal cardinal set
[:A,{0}:] is Relation-like set
[:x,{1}:] is Relation-like set
[:A,{0}:] \/ [:x,{1}:] is Relation-like set
card H2(A,x) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,g:] is Relation-like set
card [:F,g:] is epsilon-transitive epsilon-connected ordinal cardinal set
x is epsilon-transitive epsilon-connected ordinal cardinal set
x is epsilon-transitive epsilon-connected ordinal cardinal set
A is epsilon-transitive epsilon-connected ordinal cardinal set
[:x,A:] is Relation-like set
card [:x,A:] is epsilon-transitive epsilon-connected ordinal cardinal set
[:A,x:] is Relation-like set
card [:A,x:] is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (g,F) is functional set
card (Funcs (g,F)) is epsilon-transitive epsilon-connected ordinal cardinal set
F is set
g is set
[:F,g:] is Relation-like set
[:g,F:] is Relation-like set
x is set
x is set
[:x,x:] is Relation-like set
card [:x,x:] is epsilon-transitive epsilon-connected ordinal cardinal set
[:x,x:] is Relation-like set
card [:x,x:] is epsilon-transitive epsilon-connected ordinal cardinal set
F is set
g is set
[:F,g:] is Relation-like set
x is set
[:[:F,g:],x:] is Relation-like set
[:g,x:] is Relation-like set
[:F,[:g,x:]:] is Relation-like set
card [:[:F,g:],x:] is epsilon-transitive epsilon-connected ordinal cardinal set
card [:F,[:g,x:]:] is epsilon-transitive epsilon-connected ordinal cardinal set
x is Relation-like Function-like set
proj1 x is set
proj2 x is set
A is set
x . A is set
x9 is set
x . x9 is set
A `1 is set
A `2 is set
[(A `1),(A `2)] is non empty V22() set
{(A `1),(A `2)} is non empty finite countable set
{(A `1)} is non empty trivial finite 1 -element countable set
{{(A `1),(A `2)},{(A `1)}} is non empty finite V42() countable V53() V54() set
x9 `1 is set
x9 `2 is set
[(x9 `1),(x9 `2)] is non empty V22() set
{(x9 `1),(x9 `2)} is non empty finite countable set
{(x9 `1)} is non empty trivial finite 1 -element countable set
{{(x9 `1),(x9 `2)},{(x9 `1)}} is non empty finite V42() countable V53() V54() set
(A `1) `1 is set
(A `1) `2 is set
[((A `1) `1),((A `1) `2)] is non empty V22() set
{((A `1) `1),((A `1) `2)} is non empty finite countable set
{((A `1) `1)} is non empty trivial finite 1 -element countable set
{{((A `1) `1),((A `1) `2)},{((A `1) `1)}} is non empty finite V42() countable V53() V54() set
[((A `1) `2),(A `2)] is non empty V22() set
{((A `1) `2),(A `2)} is non empty finite countable set
{((A `1) `2)} is non empty trivial finite 1 -element countable set
{{((A `1) `2),(A `2)},{((A `1) `2)}} is non empty finite V42() countable V53() V54() set
[((A `1) `1),[((A `1) `2),(A `2)]] is non empty V22() set
{((A `1) `1),[((A `1) `2),(A `2)]} is non empty finite countable set
{{((A `1) `1),[((A `1) `2),(A `2)]},{((A `1) `1)}} is non empty finite V42() countable V53() V54() set
(x9 `1) `1 is set
(x9 `1) `2 is set
[((x9 `1) `2),(x9 `2)] is non empty V22() set
{((x9 `1) `2),(x9 `2)} is non empty finite countable set
{((x9 `1) `2)} is non empty trivial finite 1 -element countable set
{{((x9 `1) `2),(x9 `2)},{((x9 `1) `2)}} is non empty finite V42() countable V53() V54() set
[((x9 `1) `1),[((x9 `1) `2),(x9 `2)]] is non empty V22() set
{((x9 `1) `1),[((x9 `1) `2),(x9 `2)]} is non empty finite countable set
{((x9 `1) `1)} is non empty trivial finite 1 -element countable set
{{((x9 `1) `1),[((x9 `1) `2),(x9 `2)]},{((x9 `1) `1)}} is non empty finite V42() countable V53() V54() set
[((x9 `1) `1),((x9 `1) `2)] is non empty V22() set
{((x9 `1) `1),((x9 `1) `2)} is non empty finite countable set
{{((x9 `1) `1),((x9 `1) `2)},{((x9 `1) `1)}} is non empty finite V42() countable V53() V54() set
A is set
x9 is set
x . x9 is set
x9 `1 is set
(x9 `1) `2 is set
x9 `2 is set
[((x9 `1) `2),(x9 `2)] is non empty V22() set
{((x9 `1) `2),(x9 `2)} is non empty finite countable set
{((x9 `1) `2)} is non empty trivial finite 1 -element countable set
{{((x9 `1) `2),(x9 `2)},{((x9 `1) `2)}} is non empty finite V42() countable V53() V54() set
(x9 `1) `1 is set
[((x9 `1) `1),[((x9 `1) `2),(x9 `2)]] is non empty V22() set
{((x9 `1) `1),[((x9 `1) `2),(x9 `2)]} is non empty finite countable set
{((x9 `1) `1)} is non empty trivial finite 1 -element countable set
{{((x9 `1) `1),[((x9 `1) `2),(x9 `2)]},{((x9 `1) `1)}} is non empty finite V42() countable V53() V54() set
A is set
A `1 is set
A `2 is set
(A `2) `1 is set
[(A `1),((A `2) `1)] is non empty V22() set
{(A `1),((A `2) `1)} is non empty finite countable set
{(A `1)} is non empty trivial finite 1 -element countable set
{{(A `1),((A `2) `1)},{(A `1)}} is non empty finite V42() countable V53() V54() set
[(A `1),((A `2) `1)] `1 is set
[(A `1),((A `2) `1)] `2 is set
(A `2) `2 is set
[[(A `1),((A `2) `1)],((A `2) `2)] is non empty V22() set
{[(A `1),((A `2) `1)],((A `2) `2)} is non empty finite countable set
{[(A `1),((A `2) `1)]} is Relation-like Function-like constant non empty trivial finite 1 -element countable V53() V54() set
{{[(A `1),((A `2) `1)],((A `2) `2)},{[(A `1),((A `2) `1)]}} is non empty finite V42() countable V53() V54() set
[[(A `1),((A `2) `1)],((A `2) `2)] `1 is set
[[(A `1),((A `2) `1)],((A `2) `2)] `2 is set
[((A `2) `1),((A `2) `2)] is non empty V22() set
{((A `2) `1),((A `2) `2)} is non empty finite countable set
{((A `2) `1)} is non empty trivial finite 1 -element countable set
{{((A `2) `1),((A `2) `2)},{((A `2) `1)}} is non empty finite V42() countable V53() V54() set
[(A `1),(A `2)] is non empty V22() set
{(A `1),(A `2)} is non empty finite countable set
{{(A `1),(A `2)},{(A `1)}} is non empty finite V42() countable V53() V54() set
x . [[(A `1),((A `2) `1)],((A `2) `2)] is set
F is set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
g is set
{g} is non empty trivial finite 1 -element countable set
[:F,{g}:] is Relation-like set
card [:F,{g}:] is epsilon-transitive epsilon-connected ordinal cardinal set
x is Relation-like Function-like set
proj1 x is set
proj2 x is set
x is set
x . x is set
A is set
x . A is set
[x,g] is non empty V22() set
{x,g} is non empty finite countable set
{x} is non empty trivial finite 1 -element countable set
{{x,g},{x}} is non empty finite V42() countable V53() V54() set
[x,g] `1 is set
[A,g] is non empty V22() set
{A,g} is non empty finite countable set
{A} is non empty trivial finite 1 -element countable set
{{A,g},{A}} is non empty finite V42() countable V53() V54() set
x is set
A is set
x . A is set
[A,g] is non empty V22() set
{A,g} is non empty finite countable set
{A} is non empty trivial finite 1 -element countable set
{{A,g},{A}} is non empty finite V42() countable V53() V54() set
x is set
A is set
x9 is set
[A,x9] is non empty V22() set
{A,x9} is non empty finite countable set
{A} is non empty trivial finite 1 -element countable set
{{A,x9},{A}} is non empty finite V42() countable V53() V54() set
x . A is set
F is set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
g is set
[:F,g:] is Relation-like set
[:(card F),g:] is Relation-like set
x is Relation-like Function-like set
proj1 x is set
proj2 x is set
x is Relation-like Function-like set
proj1 x is set
proj2 x is set
A is set
x . A is set
x9 is set
x . x9 is set
A `1 is set
x9 `1 is set
x . (A `1) is set
A `2 is set
[(x . (A `1)),(A `2)] is non empty V22() set
{(x . (A `1)),(A `2)} is non empty finite countable set
{(x . (A `1))} is non empty trivial finite 1 -element countable set
{{(x . (A `1)),(A `2)},{(x . (A `1))}} is non empty finite V42() countable V53() V54() set
x . (x9 `1) is set
x9 `2 is set
[(x . (x9 `1)),(x9 `2)] is non empty V22() set
{(x . (x9 `1)),(x9 `2)} is non empty finite countable set
{(x . (x9 `1))} is non empty trivial finite 1 -element countable set
{{(x . (x9 `1)),(x9 `2)},{(x . (x9 `1))}} is non empty finite V42() countable V53() V54() set
[(A `1),(A `2)] is non empty V22() set
{(A `1),(A `2)} is non empty finite countable set
{(A `1)} is non empty trivial finite 1 -element countable set
{{(A `1),(A `2)},{(A `1)}} is non empty finite V42() countable V53() V54() set
[(x9 `1),(x9 `2)] is non empty V22() set
{(x9 `1),(x9 `2)} is non empty finite countable set
{(x9 `1)} is non empty trivial finite 1 -element countable set
{{(x9 `1),(x9 `2)},{(x9 `1)}} is non empty finite V42() countable V53() V54() set
A is set
x9 is set
x . x9 is set
x9 `1 is set
x . (x9 `1) is set
x9 `2 is set
[(x . (x9 `1)),(x9 `2)] is non empty V22() set
{(x . (x9 `1)),(x9 `2)} is non empty finite countable set
{(x . (x9 `1))} is non empty trivial finite 1 -element countable set
{{(x . (x9 `1)),(x9 `2)},{(x . (x9 `1))}} is non empty finite V42() countable V53() V54() set
A is set
A `1 is set
x9 is set
x . x9 is set
A `2 is set
[(A `1),(A `2)] is non empty V22() set
{(A `1),(A `2)} is non empty finite countable set
{(A `1)} is non empty trivial finite 1 -element countable set
{{(A `1),(A `2)},{(A `1)}} is non empty finite V42() countable V53() V54() set
[x9,(A `2)] is non empty V22() set
{x9,(A `2)} is non empty finite countable set
{x9} is non empty trivial finite 1 -element countable set
{{x9,(A `2)},{x9}} is non empty finite V42() countable V53() V54() set
[x9,(A `2)] `1 is set
[x9,(A `2)] `2 is set
x . [x9,(A `2)] is set
F is set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
g is set
[:F,g:] is Relation-like set
[:(card F),g:] is Relation-like set
card g is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,(card g):] is Relation-like set
[:(card F),(card g):] is Relation-like set
card [:F,g:] is epsilon-transitive epsilon-connected ordinal cardinal set
card [:(card F),g:] is epsilon-transitive epsilon-connected ordinal cardinal set
card [:F,(card g):] is epsilon-transitive epsilon-connected ordinal cardinal set
card [:(card F),(card g):] is epsilon-transitive epsilon-connected ordinal cardinal set
[:g,F:] is Relation-like set
[:(card g),F:] is Relation-like set
F is set
g is set
x is set
[:F,x:] is Relation-like set
card [:F,x:] is epsilon-transitive epsilon-connected ordinal cardinal set
x is set
[:g,x:] is Relation-like set
card [:g,x:] is epsilon-transitive epsilon-connected ordinal cardinal set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
card g is epsilon-transitive epsilon-connected ordinal cardinal set
card x is epsilon-transitive epsilon-connected ordinal cardinal set
card x is epsilon-transitive epsilon-connected ordinal cardinal set
[:(card F),(card x):] is Relation-like set
[:(card g),(card x):] is Relation-like set
x is set
x is set
F is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
F +^ g is epsilon-transitive epsilon-connected ordinal set
{x} is non empty trivial finite 1 -element countable set
[:F,{x}:] is Relation-like set
{x} is non empty trivial finite 1 -element countable set
[:g,{x}:] is Relation-like set
[:F,{x}:] \/ [:g,{x}:] is Relation-like set
card (F +^ g) is epsilon-transitive epsilon-connected ordinal cardinal set
card ([:F,{x}:] \/ [:g,{x}:]) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal cardinal set
(F,g) is epsilon-transitive epsilon-connected ordinal cardinal set
F +^ g is epsilon-transitive epsilon-connected ordinal set
card (F +^ g) is epsilon-transitive epsilon-connected ordinal cardinal set
x is set
{x} is non empty trivial finite 1 -element countable set
[:F,{x}:] is Relation-like set
x is set
{x} is non empty trivial finite 1 -element countable set
[:g,{x}:] is Relation-like set
[:F,{x}:] \/ [:g,{x}:] is Relation-like set
card ([:F,{x}:] \/ [:g,{x}:]) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
F *^ g is epsilon-transitive epsilon-connected ordinal set
[:F,g:] is Relation-like set
card (F *^ g) is epsilon-transitive epsilon-connected ordinal cardinal set
card [:F,g:] is epsilon-transitive epsilon-connected ordinal cardinal set
x is set
x `1 is set
x `2 is set
x is epsilon-transitive epsilon-connected ordinal set
x *^ g is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(x *^ g) +^ A is epsilon-transitive epsilon-connected ordinal set
x is Relation-like Function-like set
proj1 x is set
proj2 x is set
x is set
x . x is set
A is set
x . A is set
x `2 is set
A `2 is set
x `1 is set
A `1 is set
[(x `1),(x `2)] is non empty V22() set
{(x `1),(x `2)} is non empty finite countable set
{(x `1)} is non empty trivial finite 1 -element countable set
{{(x `1),(x `2)},{(x `1)}} is non empty finite V42() countable V53() V54() set
[(A `1),(A `2)] is non empty V22() set
{(A `1),(A `2)} is non empty finite countable set
{(A `1)} is non empty trivial finite 1 -element countable set
{{(A `1),(A `2)},{(A `1)}} is non empty finite V42() countable V53() V54() set
x9 is epsilon-transitive epsilon-connected ordinal set
f9 is epsilon-transitive epsilon-connected ordinal set
N is epsilon-transitive epsilon-connected ordinal set
K is epsilon-transitive epsilon-connected ordinal set
N *^ g is epsilon-transitive epsilon-connected ordinal set
(N *^ g) +^ K is epsilon-transitive epsilon-connected ordinal set
M is epsilon-transitive epsilon-connected ordinal set
M is epsilon-transitive epsilon-connected ordinal set
M *^ g is epsilon-transitive epsilon-connected ordinal set
(M *^ g) +^ M is epsilon-transitive epsilon-connected ordinal set
N is epsilon-transitive epsilon-connected ordinal set
K is epsilon-transitive epsilon-connected ordinal set
N *^ g is epsilon-transitive epsilon-connected ordinal set
(N *^ g) +^ K is epsilon-transitive epsilon-connected ordinal set
M is epsilon-transitive epsilon-connected ordinal set
M is epsilon-transitive epsilon-connected ordinal set
M *^ g is epsilon-transitive epsilon-connected ordinal set
(M *^ g) +^ M is epsilon-transitive epsilon-connected ordinal set
x is set
1 *^ g is epsilon-transitive epsilon-connected ordinal set
A is set
x . A is set
A `1 is set
A `2 is set
x9 is epsilon-transitive epsilon-connected ordinal set
f9 is epsilon-transitive epsilon-connected ordinal set
x9 *^ g is epsilon-transitive epsilon-connected ordinal set
(x9 *^ g) +^ f9 is epsilon-transitive epsilon-connected ordinal set
x9 +^ 1 is epsilon-transitive epsilon-connected ordinal set
succ x9 is epsilon-transitive epsilon-connected ordinal non empty set
{x9} is non empty trivial finite 1 -element countable set
x9 \/ {x9} is non empty set
(x9 *^ g) +^ (1 *^ g) is epsilon-transitive epsilon-connected ordinal set
(succ x9) *^ g is epsilon-transitive epsilon-connected ordinal set
x is set
A is epsilon-transitive epsilon-connected ordinal set
A div^ g is epsilon-transitive epsilon-connected ordinal set
(A div^ g) *^ g is epsilon-transitive epsilon-connected ordinal set
A mod^ g is epsilon-transitive epsilon-connected ordinal set
((A div^ g) *^ g) +^ (A mod^ g) is epsilon-transitive epsilon-connected ordinal set
[(A div^ g),(A mod^ g)] is non empty V22() set
{(A div^ g),(A mod^ g)} is non empty finite countable set
{(A div^ g)} is non empty trivial finite 1 -element countable set
{{(A div^ g),(A mod^ g)},{(A div^ g)}} is non empty finite V42() countable V53() V54() set
[(A div^ g),(A mod^ g)] `1 is set
[(A div^ g),(A mod^ g)] `2 is set
x . [(A div^ g),(A mod^ g)] is set
x9 is epsilon-transitive epsilon-connected ordinal set
f9 is epsilon-transitive epsilon-connected ordinal set
x9 *^ g is epsilon-transitive epsilon-connected ordinal set
(x9 *^ g) +^ f9 is epsilon-transitive epsilon-connected ordinal set
F is set
g is set
x is set
x is set
A is set
{A} is non empty trivial finite 1 -element countable set
[:F,{A}:] is Relation-like set
x9 is set
{x9} is non empty trivial finite 1 -element countable set
[:x,{x9}:] is Relation-like set
[:F,{A}:] \/ [:x,{x9}:] is Relation-like set
card ([:F,{A}:] \/ [:x,{x9}:]) is epsilon-transitive epsilon-connected ordinal cardinal set
f9 is set
{f9} is non empty trivial finite 1 -element countable set
[:g,{f9}:] is Relation-like set
N is set
{N} is non empty trivial finite 1 -element countable set
[:x,{N}:] is Relation-like set
[:g,{f9}:] \/ [:x,{N}:] is Relation-like set
card ([:g,{f9}:] \/ [:x,{N}:]) is epsilon-transitive epsilon-connected ordinal cardinal set
K is set
K `2 is set
K is set
K `2 is set
F is epsilon-transitive epsilon-connected ordinal set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal set
F +^ g is epsilon-transitive epsilon-connected ordinal set
card (F +^ g) is epsilon-transitive epsilon-connected ordinal cardinal set
card g is epsilon-transitive epsilon-connected ordinal cardinal set
((card F),(card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
(card F) +^ (card g) is epsilon-transitive epsilon-connected ordinal set
card ((card F) +^ (card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,{0}:] is Relation-like set
[:g,{1}:] is Relation-like set
[:F,{0}:] \/ [:g,{1}:] is Relation-like set
[:(card F),{0}:] is Relation-like set
[:(card g),{1}:] is Relation-like set
[:(card F),{0}:] \/ [:(card g),{1}:] is Relation-like set
F is epsilon-transitive epsilon-connected ordinal set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal set
F *^ g is epsilon-transitive epsilon-connected ordinal set
card (F *^ g) is epsilon-transitive epsilon-connected ordinal cardinal set
card g is epsilon-transitive epsilon-connected ordinal cardinal set
((card F),(card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
[:(card F),(card g):] is Relation-like set
card [:(card F),(card g):] is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,g:] is Relation-like set
card [:F,g:] is epsilon-transitive epsilon-connected ordinal cardinal set
F is set
[:F,{0}:] is Relation-like set
g is set
[:g,{1}:] is Relation-like set
[:F,{0}:] \/ [:g,{1}:] is Relation-like set
[:g,{0}:] is Relation-like set
[:F,{1}:] is Relation-like set
[:g,{0}:] \/ [:F,{1}:] is Relation-like set
x is set
[:x,{0}:] is Relation-like set
x is set
[:x,{1}:] is Relation-like set
[:x,{0}:] \/ [:x,{1}:] is Relation-like set
card ([:x,{0}:] \/ [:x,{1}:]) is epsilon-transitive epsilon-connected ordinal cardinal set
[:x,{0}:] is Relation-like set
[:x,{1}:] is Relation-like set
[:x,{0}:] \/ [:x,{1}:] is Relation-like set
card ([:x,{0}:] \/ [:x,{1}:]) is epsilon-transitive epsilon-connected ordinal cardinal set
F is set
g is set
[:F,g:] is Relation-like set
[:g,F:] is Relation-like set
x is set
x is set
[:x,x:] is Relation-like set
[:F,g:] \/ [:x,x:] is Relation-like set
[:x,x:] is Relation-like set
[:g,F:] \/ [:x,x:] is Relation-like set
card ([:F,g:] \/ [:x,x:]) is epsilon-transitive epsilon-connected ordinal cardinal set
card ([:g,F:] \/ [:x,x:]) is epsilon-transitive epsilon-connected ordinal cardinal set
A is Relation-like Function-like set
proj1 A is set
proj2 A is set
x9 is set
A . x9 is set
f9 is set
A . f9 is set
x9 `1 is set
x9 `2 is set
[(x9 `1),(x9 `2)] is non empty V22() set
{(x9 `1),(x9 `2)} is non empty finite countable set
{(x9 `1)} is non empty trivial finite 1 -element countable set
{{(x9 `1),(x9 `2)},{(x9 `1)}} is non empty finite V42() countable V53() V54() set
f9 `1 is set
f9 `2 is set
[(f9 `1),(f9 `2)] is non empty V22() set
{(f9 `1),(f9 `2)} is non empty finite countable set
{(f9 `1)} is non empty trivial finite 1 -element countable set
{{(f9 `1),(f9 `2)},{(f9 `1)}} is non empty finite V42() countable V53() V54() set
[(x9 `2),(x9 `1)] is non empty V22() set
{(x9 `2),(x9 `1)} is non empty finite countable set
{(x9 `2)} is non empty trivial finite 1 -element countable set
{{(x9 `2),(x9 `1)},{(x9 `2)}} is non empty finite V42() countable V53() V54() set
[(f9 `2),(f9 `1)] is non empty V22() set
{(f9 `2),(f9 `1)} is non empty finite countable set
{(f9 `2)} is non empty trivial finite 1 -element countable set
{{(f9 `2),(f9 `1)},{(f9 `2)}} is non empty finite V42() countable V53() V54() set
x9 is set
f9 is set
A . f9 is set
f9 `1 is set
f9 `2 is set
[(f9 `2),(f9 `1)] is non empty V22() set
{(f9 `2),(f9 `1)} is non empty finite countable set
{(f9 `2)} is non empty trivial finite 1 -element countable set
{{(f9 `2),(f9 `1)},{(f9 `2)}} is non empty finite V42() countable V53() V54() set
x9 is set
x9 `2 is set
x9 `1 is set
[(x9 `2),(x9 `1)] is non empty V22() set
{(x9 `2),(x9 `1)} is non empty finite countable set
{(x9 `2)} is non empty trivial finite 1 -element countable set
{{(x9 `2),(x9 `1)},{(x9 `2)}} is non empty finite V42() countable V53() V54() set
[(x9 `2),(x9 `1)] `1 is set
[(x9 `2),(x9 `1)] `2 is set
[(x9 `1),(x9 `2)] is non empty V22() set
{(x9 `1),(x9 `2)} is non empty finite countable set
{(x9 `1)} is non empty trivial finite 1 -element countable set
{{(x9 `1),(x9 `2)},{(x9 `1)}} is non empty finite V42() countable V53() V54() set
A . [(x9 `2),(x9 `1)] is set
F is set
{F} is non empty trivial finite 1 -element countable set
g is set
{g} is non empty trivial finite 1 -element countable set
x is set
card x is epsilon-transitive epsilon-connected ordinal cardinal set
[:x,{F}:] is Relation-like set
x is set
card x is epsilon-transitive epsilon-connected ordinal cardinal set
((card x),(card x)) is epsilon-transitive epsilon-connected ordinal cardinal set
(card x) +^ (card x) is epsilon-transitive epsilon-connected ordinal set
card ((card x) +^ (card x)) is epsilon-transitive epsilon-connected ordinal cardinal set
[:x,{g}:] is Relation-like set
[:x,{F}:] \/ [:x,{g}:] is Relation-like set
card ([:x,{F}:] \/ [:x,{g}:]) is epsilon-transitive epsilon-connected ordinal cardinal set
card H4(x,x,F,g) is epsilon-transitive epsilon-connected ordinal cardinal set
[:(card x),{F}:] is Relation-like set
[:(card x),{g}:] is Relation-like set
[:(card x),{F}:] \/ [:(card x),{g}:] is Relation-like set
card H4( card x, card x,F,g) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
(F,0) is epsilon-transitive epsilon-connected ordinal cardinal set
F +^ 0 is epsilon-transitive epsilon-connected ordinal set
card (F +^ 0) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,{0}:] is Relation-like set
[:{},{1}:] is Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty trivial Function-yielding V29() ext-real V36() V37() finite finite-yielding V42() cardinal {} -element Cardinal-yielding countable set
[:F,{0}:] \/ [:{},{1}:] is Relation-like set
card H3(F, {} ) is epsilon-transitive epsilon-connected ordinal cardinal set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
F is set
{F} is non empty trivial finite 1 -element countable set
g is set
{g} is non empty trivial finite 1 -element countable set
x is set
[:x,{F}:] is Relation-like set
x is set
[:x,{g}:] is Relation-like set
A is set
A `2 is set
F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal cardinal set
(F,g) is epsilon-transitive epsilon-connected ordinal cardinal set
F +^ g is epsilon-transitive epsilon-connected ordinal set
card (F +^ g) is epsilon-transitive epsilon-connected ordinal cardinal set
x is epsilon-transitive epsilon-connected ordinal cardinal set
((F,g),x) is epsilon-transitive epsilon-connected ordinal cardinal set
(F,g) +^ x is epsilon-transitive epsilon-connected ordinal set
card ((F,g) +^ x) is epsilon-transitive epsilon-connected ordinal cardinal set
(g,x) is epsilon-transitive epsilon-connected ordinal cardinal set
g +^ x is epsilon-transitive epsilon-connected ordinal set
card (g +^ x) is epsilon-transitive epsilon-connected ordinal cardinal set
(F,(g,x)) is epsilon-transitive epsilon-connected ordinal cardinal set
F +^ (g,x) is epsilon-transitive epsilon-connected ordinal set
card (F +^ (g,x)) is epsilon-transitive epsilon-connected ordinal cardinal set
card ((F,g),x) is epsilon-transitive epsilon-connected ordinal cardinal set
[:(F,g),{0}:] is Relation-like set
{2} is non empty trivial finite V42() 1 -element countable V53() V54() set
[:x,{2}:] is Relation-like set
[:(F,g),{0}:] \/ [:x,{2}:] is Relation-like set
[:g,{1}:] is Relation-like set
[:g,{1}:] /\ [:x,{2}:] is Relation-like set
[:F,{0}:] is Relation-like set
[:F,{0}:] /\ [:x,{2}:] is Relation-like set
[:F,{0}:] \/ [:g,{1}:] is Relation-like set
([:F,{0}:] \/ [:g,{1}:]) /\ [:x,{2}:] is Relation-like set
{} \/ {} is Relation-like finite V42() countable set
[:F,{0}:] /\ [:g,{1}:] is Relation-like set
[:g,{1}:] \/ [:x,{2}:] is Relation-like set
[:F,{0}:] /\ ([:g,{1}:] \/ [:x,{2}:]) is Relation-like set
[:(g,x),{2}:] is Relation-like set
[:F,{0}:] \/ ([:g,{1}:] \/ [:x,{2}:]) is Relation-like set
[:F,{0}:] \/ [:(g,x),{2}:] is Relation-like set
([:F,{0}:] \/ [:g,{1}:]) \/ [:x,{2}:] is Relation-like set
F is epsilon-transitive epsilon-connected ordinal cardinal set
(F,0) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,0:] is Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty trivial Function-yielding V29() ext-real V36() V37() finite finite-yielding V42() cardinal {} -element Cardinal-yielding countable set
card [:F,0:] is Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty trivial Function-yielding V29() ext-real V36() V37() finite finite-yielding V42() cardinal {} -element Cardinal-yielding countable set
F is epsilon-transitive epsilon-connected ordinal cardinal set
(F,1) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,1:] is Relation-like set
card [:F,1:] is epsilon-transitive epsilon-connected ordinal cardinal set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal cardinal set
(F,g) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,g:] is Relation-like set
card [:F,g:] is epsilon-transitive epsilon-connected ordinal cardinal set
x is epsilon-transitive epsilon-connected ordinal cardinal set
((F,g),x) is epsilon-transitive epsilon-connected ordinal cardinal set
[:(F,g),x:] is Relation-like set
card [:(F,g),x:] is epsilon-transitive epsilon-connected ordinal cardinal set
(g,x) is epsilon-transitive epsilon-connected ordinal cardinal set
[:g,x:] is Relation-like set
card [:g,x:] is epsilon-transitive epsilon-connected ordinal cardinal set
(F,(g,x)) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,(g,x):] is Relation-like set
card [:F,(g,x):] is epsilon-transitive epsilon-connected ordinal cardinal set
[:[:F,g:],x:] is Relation-like set
card [:[:F,g:],x:] is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,[:g,x:]:] is Relation-like set
card [:F,[:g,x:]:] is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
(2,F) is epsilon-transitive epsilon-connected ordinal cardinal set
[:2,F:] is Relation-like set
card [:2,F:] is epsilon-transitive epsilon-connected ordinal cardinal set
(F,F) is epsilon-transitive epsilon-connected ordinal cardinal set
F +^ F is epsilon-transitive epsilon-connected ordinal set
card (F +^ F) is epsilon-transitive epsilon-connected ordinal cardinal set
[:{{}},F:] is Relation-like set
[:{1},F:] is Relation-like set
[:{{}},F:] \/ [:{1},F:] is Relation-like set
card ([:{{}},F:] \/ [:{1},F:]) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,{{}}:] is Relation-like set
[:F,{1}:] is Relation-like set
[:F,{{}}:] \/ [:F,{1}:] is Relation-like set
card ([:F,{{}}:] \/ [:F,{1}:]) is epsilon-transitive epsilon-connected ordinal cardinal set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
((card F),(card F)) is epsilon-transitive epsilon-connected ordinal cardinal set
(card F) +^ (card F) is epsilon-transitive epsilon-connected ordinal set
card ((card F) +^ (card F)) is epsilon-transitive epsilon-connected ordinal cardinal set
(F,(card F)) is epsilon-transitive epsilon-connected ordinal cardinal set
F +^ (card F) is epsilon-transitive epsilon-connected ordinal set
card (F +^ (card F)) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal cardinal set
(F,g) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,g:] is Relation-like set
card [:F,g:] is epsilon-transitive epsilon-connected ordinal cardinal set
x is epsilon-transitive epsilon-connected ordinal cardinal set
(g,x) is epsilon-transitive epsilon-connected ordinal cardinal set
g +^ x is epsilon-transitive epsilon-connected ordinal set
card (g +^ x) is epsilon-transitive epsilon-connected ordinal cardinal set
(F,(g,x)) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,(g,x):] is Relation-like set
card [:F,(g,x):] is epsilon-transitive epsilon-connected ordinal cardinal set
(F,x) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,x:] is Relation-like set
card [:F,x:] is epsilon-transitive epsilon-connected ordinal cardinal set
((F,g),(F,x)) is epsilon-transitive epsilon-connected ordinal cardinal set
(F,g) +^ (F,x) is epsilon-transitive epsilon-connected ordinal set
card ((F,g) +^ (F,x)) is epsilon-transitive epsilon-connected ordinal cardinal set
[:(card [:F,g:]),{0}:] is Relation-like set
[:[:F,g:],{0}:] is Relation-like set
[:g,{0}:] is Relation-like set
[:F,[:g,{0}:]:] is Relation-like set
[:(card [:F,x:]),{1}:] is Relation-like set
[:[:F,x:],{1}:] is Relation-like set
[:x,{1}:] is Relation-like set
[:F,[:x,{1}:]:] is Relation-like set
[:g,{0}:] \/ [:x,{1}:] is Relation-like set
card H3(g,x) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,(card H3(g,x)):] is Relation-like set
card [:F,(card H3(g,x)):] is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,H3(g,x):] is Relation-like set
card [:F,H3(g,x):] is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,[:g,{0}:]:] \/ [:F,[:x,{1}:]:] is Relation-like set
card ([:F,[:g,{0}:]:] \/ [:F,[:x,{1}:]:]) is epsilon-transitive epsilon-connected ordinal cardinal set
[:(card [:F,g:]),{0}:] \/ [:(card [:F,x:]),{1}:] is Relation-like set
card ([:(card [:F,g:]),{0}:] \/ [:(card [:F,x:]),{1}:]) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
(F,0) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (0,F) is functional set
card (Funcs (0,F)) is epsilon-transitive epsilon-connected ordinal cardinal set
card {{}} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
F is epsilon-transitive epsilon-connected ordinal cardinal set
(0,F) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (F,0) is functional set
card (Funcs (F,0)) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
(F,1) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (1,F) is functional set
card (Funcs (1,F)) is epsilon-transitive epsilon-connected ordinal cardinal set
(1,F) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (F,1) is functional non empty set
card (Funcs (F,1)) is epsilon-transitive epsilon-connected ordinal non empty cardinal set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
F --> {} is Relation-like F -defined {{}} -valued Function-like constant V21(F) quasi_total Function-yielding V29() Cardinal-yielding Element of bool [:F,{{}}:]
[:F,{{}}:] is Relation-like set
bool [:F,{{}}:] is non empty cup-closed diff-closed preBoolean set
{(F --> {})} is functional non empty trivial finite 1 -element with_common_domain countable set
card {(F --> {})} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal cardinal set
(F,g) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (g,F) is functional set
card (Funcs (g,F)) is epsilon-transitive epsilon-connected ordinal cardinal set
x is epsilon-transitive epsilon-connected ordinal cardinal set
(g,x) is epsilon-transitive epsilon-connected ordinal cardinal set
g +^ x is epsilon-transitive epsilon-connected ordinal set
card (g +^ x) is epsilon-transitive epsilon-connected ordinal cardinal set
(F,(g,x)) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs ((g,x),F) is functional set
card (Funcs ((g,x),F)) is epsilon-transitive epsilon-connected ordinal cardinal set
(F,x) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (x,F) is functional set
card (Funcs (x,F)) is epsilon-transitive epsilon-connected ordinal cardinal set
((F,g),(F,x)) is epsilon-transitive epsilon-connected ordinal cardinal set
[:(F,g),(F,x):] is Relation-like set
card [:(F,g),(F,x):] is epsilon-transitive epsilon-connected ordinal cardinal set
[:g,{0}:] is Relation-like set
[:x,{1}:] is Relation-like set
Funcs ([:g,{0}:],F) is functional set
Funcs ([:x,{1}:],F) is functional set
[:g,{0}:] \/ [:x,{1}:] is Relation-like set
Funcs (([:g,{0}:] \/ [:x,{1}:]),F) is functional set
card (Funcs (([:g,{0}:] \/ [:x,{1}:]),F)) is epsilon-transitive epsilon-connected ordinal cardinal set
[:(Funcs ([:g,{0}:],F)),(Funcs ([:x,{1}:],F)):] is Relation-like set
card [:(Funcs ([:g,{0}:],F)),(Funcs ([:x,{1}:],F)):] is epsilon-transitive epsilon-connected ordinal cardinal set
[:(Funcs (g,F)),(Funcs (x,F)):] is Relation-like set
card [:(Funcs (g,F)),(Funcs (x,F)):] is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal cardinal set
(F,g) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,g:] is Relation-like set
card [:F,g:] is epsilon-transitive epsilon-connected ordinal cardinal set
x is epsilon-transitive epsilon-connected ordinal cardinal set
((F,g),x) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (x,(F,g)) is functional set
card (Funcs (x,(F,g))) is epsilon-transitive epsilon-connected ordinal cardinal set
(F,x) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (x,F) is functional set
card (Funcs (x,F)) is epsilon-transitive epsilon-connected ordinal cardinal set
(g,x) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (x,g) is functional set
card (Funcs (x,g)) is epsilon-transitive epsilon-connected ordinal cardinal set
((F,x),(g,x)) is epsilon-transitive epsilon-connected ordinal cardinal set
[:(F,x),(g,x):] is Relation-like set
card [:(F,x),(g,x):] is epsilon-transitive epsilon-connected ordinal cardinal set
card (F,g) is epsilon-transitive epsilon-connected ordinal cardinal set
card x is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (x,[:F,g:]) is functional set
card (Funcs (x,[:F,g:])) is epsilon-transitive epsilon-connected ordinal cardinal set
[:(Funcs (x,F)),(Funcs (x,g)):] is Relation-like set
card [:(Funcs (x,F)),(Funcs (x,g)):] is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal cardinal set
(F,g) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (g,F) is functional set
card (Funcs (g,F)) is epsilon-transitive epsilon-connected ordinal cardinal set
x is epsilon-transitive epsilon-connected ordinal cardinal set
(g,x) is epsilon-transitive epsilon-connected ordinal cardinal set
[:g,x:] is Relation-like set
card [:g,x:] is epsilon-transitive epsilon-connected ordinal cardinal set
(F,(g,x)) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs ((g,x),F) is functional set
card (Funcs ((g,x),F)) is epsilon-transitive epsilon-connected ordinal cardinal set
((F,g),x) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (x,(F,g)) is functional set
card (Funcs (x,(F,g))) is epsilon-transitive epsilon-connected ordinal cardinal set
[:x,g:] is Relation-like set
Funcs ([:x,g:],F) is functional set
card (Funcs ([:x,g:],F)) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (x,(Funcs (g,F))) is functional set
card (Funcs (x,(Funcs (g,F)))) is epsilon-transitive epsilon-connected ordinal cardinal set
F is set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
(2,(card F)) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs ((card F),2) is functional non empty set
card (Funcs ((card F),2)) is epsilon-transitive epsilon-connected ordinal non empty cardinal set
bool F is non empty cup-closed diff-closed preBoolean set
card (bool F) is epsilon-transitive epsilon-connected ordinal non empty cardinal set
card (card F) is epsilon-transitive epsilon-connected ordinal cardinal set
card 2 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
card {{},1} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
Funcs (F,{{},1}) is functional non empty FUNCTION_DOMAIN of F,{{},1}
card (Funcs (F,{{},1})) is epsilon-transitive epsilon-connected ordinal non empty cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
(F,2) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (2,F) is functional set
card (Funcs (2,F)) is epsilon-transitive epsilon-connected ordinal cardinal set
(F,F) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,F:] is Relation-like set
card [:F,F:] is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
(F,F) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,F:] is Relation-like set
card [:F,F:] is epsilon-transitive epsilon-connected ordinal cardinal set
(2,F) is epsilon-transitive epsilon-connected ordinal cardinal set
[:2,F:] is Relation-like set
card [:2,F:] is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal cardinal set
(F,g) is epsilon-transitive epsilon-connected ordinal cardinal set
F +^ g is epsilon-transitive epsilon-connected ordinal set
card (F +^ g) is epsilon-transitive epsilon-connected ordinal cardinal set
((F,g),2) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (2,(F,g)) is functional set
card (Funcs (2,(F,g))) is epsilon-transitive epsilon-connected ordinal cardinal set
((2,F),g) is epsilon-transitive epsilon-connected ordinal cardinal set
[:(2,F),g:] is Relation-like set
card [:(2,F),g:] is epsilon-transitive epsilon-connected ordinal cardinal set
((F,F),((2,F),g)) is epsilon-transitive epsilon-connected ordinal cardinal set
(F,F) +^ ((2,F),g) is epsilon-transitive epsilon-connected ordinal set
card ((F,F) +^ ((2,F),g)) is epsilon-transitive epsilon-connected ordinal cardinal set
(g,g) is epsilon-transitive epsilon-connected ordinal cardinal set
[:g,g:] is Relation-like set
card [:g,g:] is epsilon-transitive epsilon-connected ordinal cardinal set
(((F,F),((2,F),g)),(g,g)) is epsilon-transitive epsilon-connected ordinal cardinal set
((F,F),((2,F),g)) +^ (g,g) is epsilon-transitive epsilon-connected ordinal set
card (((F,F),((2,F),g)) +^ (g,g)) is epsilon-transitive epsilon-connected ordinal cardinal set
((F,g),(F,g)) is epsilon-transitive epsilon-connected ordinal cardinal set
[:(F,g),(F,g):] is Relation-like set
card [:(F,g),(F,g):] is epsilon-transitive epsilon-connected ordinal cardinal set
(F,(F,g)) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,(F,g):] is Relation-like set
card [:F,(F,g):] is epsilon-transitive epsilon-connected ordinal cardinal set
(g,(F,g)) is epsilon-transitive epsilon-connected ordinal cardinal set
[:g,(F,g):] is Relation-like set
card [:g,(F,g):] is epsilon-transitive epsilon-connected ordinal cardinal set
((F,(F,g)),(g,(F,g))) is epsilon-transitive epsilon-connected ordinal cardinal set
(F,(F,g)) +^ (g,(F,g)) is epsilon-transitive epsilon-connected ordinal set
card ((F,(F,g)) +^ (g,(F,g))) is epsilon-transitive epsilon-connected ordinal cardinal set
(F,g) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,g:] is Relation-like set
card [:F,g:] is epsilon-transitive epsilon-connected ordinal cardinal set
((F,F),(F,g)) is epsilon-transitive epsilon-connected ordinal cardinal set
(F,F) +^ (F,g) is epsilon-transitive epsilon-connected ordinal set
card ((F,F) +^ (F,g)) is epsilon-transitive epsilon-connected ordinal cardinal set
(((F,F),(F,g)),(g,(F,g))) is epsilon-transitive epsilon-connected ordinal cardinal set
((F,F),(F,g)) +^ (g,(F,g)) is epsilon-transitive epsilon-connected ordinal set
card (((F,F),(F,g)) +^ (g,(F,g))) is epsilon-transitive epsilon-connected ordinal cardinal set
(g,F) is epsilon-transitive epsilon-connected ordinal cardinal set
[:g,F:] is Relation-like set
card [:g,F:] is epsilon-transitive epsilon-connected ordinal cardinal set
((g,F),(g,g)) is epsilon-transitive epsilon-connected ordinal cardinal set
(g,F) +^ (g,g) is epsilon-transitive epsilon-connected ordinal set
card ((g,F) +^ (g,g)) is epsilon-transitive epsilon-connected ordinal cardinal set
(((F,F),(F,g)),((g,F),(g,g))) is epsilon-transitive epsilon-connected ordinal cardinal set
((F,F),(F,g)) +^ ((g,F),(g,g)) is epsilon-transitive epsilon-connected ordinal set
card (((F,F),(F,g)) +^ ((g,F),(g,g))) is epsilon-transitive epsilon-connected ordinal cardinal set
(((F,F),(F,g)),(F,g)) is epsilon-transitive epsilon-connected ordinal cardinal set
((F,F),(F,g)) +^ (F,g) is epsilon-transitive epsilon-connected ordinal set
card (((F,F),(F,g)) +^ (F,g)) is epsilon-transitive epsilon-connected ordinal cardinal set
((((F,F),(F,g)),(F,g)),(g,g)) is epsilon-transitive epsilon-connected ordinal cardinal set
(((F,F),(F,g)),(F,g)) +^ (g,g) is epsilon-transitive epsilon-connected ordinal set
card ((((F,F),(F,g)),(F,g)) +^ (g,g)) is epsilon-transitive epsilon-connected ordinal cardinal set
((F,g),(F,g)) is epsilon-transitive epsilon-connected ordinal cardinal set
(F,g) +^ (F,g) is epsilon-transitive epsilon-connected ordinal set
card ((F,g) +^ (F,g)) is epsilon-transitive epsilon-connected ordinal cardinal set
((F,F),((F,g),(F,g))) is epsilon-transitive epsilon-connected ordinal cardinal set
(F,F) +^ ((F,g),(F,g)) is epsilon-transitive epsilon-connected ordinal set
card ((F,F) +^ ((F,g),(F,g))) is epsilon-transitive epsilon-connected ordinal cardinal set
(((F,F),((F,g),(F,g))),(g,g)) is epsilon-transitive epsilon-connected ordinal cardinal set
((F,F),((F,g),(F,g))) +^ (g,g) is epsilon-transitive epsilon-connected ordinal set
card (((F,F),((F,g),(F,g))) +^ (g,g)) is epsilon-transitive epsilon-connected ordinal cardinal set
(2,(F,g)) is epsilon-transitive epsilon-connected ordinal cardinal set
[:2,(F,g):] is Relation-like set
card [:2,(F,g):] is epsilon-transitive epsilon-connected ordinal cardinal set
((F,F),(2,(F,g))) is epsilon-transitive epsilon-connected ordinal cardinal set
(F,F) +^ (2,(F,g)) is epsilon-transitive epsilon-connected ordinal set
card ((F,F) +^ (2,(F,g))) is epsilon-transitive epsilon-connected ordinal cardinal set
(((F,F),(2,(F,g))),(g,g)) is epsilon-transitive epsilon-connected ordinal cardinal set
((F,F),(2,(F,g))) +^ (g,g) is epsilon-transitive epsilon-connected ordinal set
card (((F,F),(2,(F,g))) +^ (g,g)) is epsilon-transitive epsilon-connected ordinal cardinal set
F is set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
g is set
F \/ g is set
card (F \/ g) is epsilon-transitive epsilon-connected ordinal cardinal set
card g is epsilon-transitive epsilon-connected ordinal cardinal set
((card F),(card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
(card F) +^ (card g) is epsilon-transitive epsilon-connected ordinal set
card ((card F) +^ (card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,{0}:] is Relation-like set
[:g,{1}:] is Relation-like set
[:F,{0}:] \/ [:g,{1}:] is Relation-like set
x is Relation-like Function-like set
proj1 x is set
proj2 x is set
x is set
[x,0] is non empty V22() set
{x,0} is non empty finite countable set
{x} is non empty trivial finite 1 -element countable set
{{x,0},{x}} is non empty finite V42() countable V53() V54() set
[x,0] `1 is set
x . [x,0] is set
[x,1] is non empty V22() set
{x,1} is non empty finite countable set
{x} is non empty trivial finite 1 -element countable set
{{x,1},{x}} is non empty finite V42() countable V53() V54() set
[x,1] `1 is set
x . [x,1] is set
card H3(F,g) is epsilon-transitive epsilon-connected ordinal cardinal set
F is set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
g is set
F \/ g is set
card (F \/ g) is epsilon-transitive epsilon-connected ordinal cardinal set
card g is epsilon-transitive epsilon-connected ordinal cardinal set
((card F),(card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
(card F) +^ (card g) is epsilon-transitive epsilon-connected ordinal set
card ((card F) +^ (card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,{0}:] is Relation-like set
[:(card F),{0}:] is Relation-like set
[:g,{1}:] is Relation-like set
[:(card g),{1}:] is Relation-like set
[:(card F),{0}:] \/ [:(card g),{1}:] is Relation-like set
card ([:(card F),{0}:] \/ [:(card g),{1}:]) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
F + g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
F +^ g is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
F + x is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
F +^ x is epsilon-transitive epsilon-connected ordinal set
x + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
F + (x + 1) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
F +^ (x + 1) is epsilon-transitive epsilon-connected ordinal set
(F + x) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
succ (F +^ x) is epsilon-transitive epsilon-connected ordinal non empty set
{(F +^ x)} is non empty trivial finite 1 -element countable set
(F +^ x) \/ {(F +^ x)} is non empty set
succ x is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable set
{x} is non empty trivial finite V42() 1 -element countable set
x \/ {x} is non empty finite countable set
F +^ (succ x) is epsilon-transitive epsilon-connected ordinal set
F + 0 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
F +^ 0 is epsilon-transitive epsilon-connected ordinal set
F is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
F * g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
F *^ g is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
x * g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
x *^ g is epsilon-transitive epsilon-connected ordinal set
x + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
(x + 1) * g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
(x + 1) *^ g is epsilon-transitive epsilon-connected ordinal set
1 * g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
(x * g) + (1 * g) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
(x *^ g) +^ g is epsilon-transitive epsilon-connected ordinal set
1 *^ g is epsilon-transitive epsilon-connected ordinal set
(x *^ g) +^ (1 *^ g) is epsilon-transitive epsilon-connected ordinal set
x +^ 1 is epsilon-transitive epsilon-connected ordinal set
(x +^ 1) *^ g is epsilon-transitive epsilon-connected ordinal set
succ x is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable set
{x} is non empty trivial finite V42() 1 -element countable set
x \/ {x} is non empty finite countable set
(succ x) *^ g is epsilon-transitive epsilon-connected ordinal set
0 * g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
0 *^ g is epsilon-transitive epsilon-connected ordinal set
F is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
card F is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
F + g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
card (F + g) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
((card F),(card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
(card F) +^ (card g) is epsilon-transitive epsilon-connected ordinal set
card ((card F) +^ (card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
F +^ g is epsilon-transitive epsilon-connected ordinal set
card (F +^ g) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
card F is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
F * g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
card (F * g) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
((card F),(card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
[:(card F),(card g):] is Relation-like finite countable set
card [:(card F),(card g):] is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
F *^ g is epsilon-transitive epsilon-connected ordinal set
card (F *^ g) is epsilon-transitive epsilon-connected ordinal cardinal set
F is finite countable set
g is finite countable set
F \/ g is finite countable set
card (F \/ g) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card F is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
(card F) + (card g) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
card (card (F \/ g)) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card (card F) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card (card g) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
((card (card F)),(card (card g))) is epsilon-transitive epsilon-connected ordinal cardinal set
(card (card F)) +^ (card (card g)) is epsilon-transitive epsilon-connected ordinal set
card ((card (card F)) +^ (card (card g))) is epsilon-transitive epsilon-connected ordinal cardinal set
card ((card F) + (card g)) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
F is set
{F} is non empty trivial finite 1 -element countable set
g is finite countable set
g \/ {F} is non empty finite countable set
card (g \/ {F}) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
card g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
(card g) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
card {F} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
F is set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
card {0} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
g is set
{g} is non empty trivial finite 1 -element countable set
F is finite countable set
g is finite countable set
F \/ g is finite countable set
card (F \/ g) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card F is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
(card F) + (card g) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
card (card F) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card (card g) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
((card F),(card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
(card F) +^ (card g) is epsilon-transitive epsilon-connected ordinal set
card ((card F) +^ (card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
card ((card F) + (card g)) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card (card (F \/ g)) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
g is finite countable set
F is finite countable set
F \ g is finite countable Element of bool F
bool F is non empty finite V42() countable cup-closed diff-closed preBoolean set
card (F \ g) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card F is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
(card F) - (card g) is ext-real V36() V37() set
(card F) - 0 is ext-real V36() V37() set
F \ {} is finite countable Element of bool F
x is set
x is set
{x} is non empty trivial finite 1 -element countable set
x \/ {x} is non empty set
card {x} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
A is finite countable set
F \ A is finite countable Element of bool F
card (F \ A) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card A is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
(card F) - (card A) is ext-real V36() V37() set
F \ x is finite countable Element of bool F
A is finite countable set
F \ A is finite countable Element of bool F
card (F \ A) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card A is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
(card F) - (card A) is ext-real V36() V37() set
card (F \ x) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
A is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
A + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
F \ (x \/ {x}) is finite countable Element of bool F
(F \ x) \ {x} is finite countable Element of bool F
x9 is finite countable set
card x9 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
(card x9) + (card {x}) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
x9 \/ {x} is non empty finite countable set
card (x9 \/ {x}) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
f9 is finite countable set
F \ f9 is finite countable Element of bool F
card (F \ f9) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card f9 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
(card F) - (card f9) is ext-real V36() V37() set
succ A is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable set
{A} is non empty trivial finite V42() 1 -element countable set
A \/ {A} is non empty finite countable set
(A + 1) \ {A} is finite countable Element of bool (A + 1)
bool (A + 1) is non empty finite V42() countable cup-closed diff-closed preBoolean set
card (F \ (x \/ {x})) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
(card F) - (card (x9 \/ {x})) is ext-real V36() V37() set
f9 is finite countable set
F \ f9 is finite countable Element of bool F
card (F \ f9) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card f9 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
(card F) - (card f9) is ext-real V36() V37() set
x is finite countable set
F \ x is finite countable Element of bool F
card (F \ x) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card x is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
(card F) - (card x) is ext-real V36() V37() set
F is finite countable set
g is finite countable set
F \/ g is finite countable set
card (F \/ g) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card F is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
(card F) + (card g) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
F /\ g is finite countable set
card (F /\ g) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
((card F) + (card g)) - (card (F /\ g)) is ext-real V36() V37() set
g \ F is finite countable Element of bool g
bool g is non empty finite V42() countable cup-closed diff-closed preBoolean set
g \ (F /\ g) is finite countable Element of bool g
card (g \ F) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
(card g) - (card (F /\ g)) is ext-real V36() V37() set
F \/ (g \ F) is finite countable set
card (F \/ (g \ F)) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
(card F) + (card (g \ F)) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
F is finite countable set
g is finite countable set
[:F,g:] is Relation-like finite countable set
card [:F,g:] is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card F is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
(card F) * (card g) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
card (card [:F,g:]) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card (card F) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card (card g) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
((card (card F)),(card (card g))) is epsilon-transitive epsilon-connected ordinal cardinal set
[:(card (card F)),(card (card g)):] is Relation-like finite countable set
card [:(card (card F)),(card (card g)):] is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
card ((card F) * (card g)) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
F is Relation-like Function-like finite countable set
proj2 F is finite countable set
card (proj2 F) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
proj1 F is finite countable set
card (proj1 F) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
F is finite countable set
g is finite countable set
card g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card F is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
g \ F is finite countable Element of bool g
bool g is non empty finite V42() countable cup-closed diff-closed preBoolean set
F \/ (g \ F) is finite countable set
card (g \ F) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
(card F) + (card (g \ F)) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
F is set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
g is set
card g is epsilon-transitive epsilon-connected ordinal cardinal set
F is set
g is set
{F,g} is non empty finite countable set
card {F,g} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
{F} is non empty trivial finite 1 -element countable set
{g} is non empty trivial finite 1 -element countable set
{F} \/ {g} is non empty finite countable set
1 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
card {F} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
card {g} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
3 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of NAT
F is set
g is set
x is set
{F,g,x} is non empty finite countable set
card {F,g,x} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
{g,x} is non empty finite countable set
card {g,x} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
1 + (card {g,x}) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
1 + 2 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
{F} is non empty trivial finite 1 -element countable set
card {F} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
{F} \/ {g,x} is non empty finite countable set
4 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of NAT
F is set
g is set
x is set
x is set
{F,g,x,x} is non empty finite countable set
card {F,g,x,x} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
{g,x,x} is non empty finite countable set
card {g,x,x} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
1 + (card {g,x,x}) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
1 + 3 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
{F} is non empty trivial finite 1 -element countable set
card {F} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
{F} \/ {g,x,x} is non empty finite countable set
5 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of NAT
F is set
g is set
x is set
x is set
A is set
{F,g,x,x,A} is non empty finite countable set
card {F,g,x,x,A} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
{g,x,x,A} is non empty finite countable set
card {g,x,x,A} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
1 + (card {g,x,x,A}) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
1 + 4 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
{F} is non empty trivial finite 1 -element countable set
card {F} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
{F} \/ {g,x,x,A} is non empty finite countable set
6 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of NAT
F is set
g is set
x is set
x is set
A is set
x9 is set
{F,g,x,x,A,x9} is non empty finite countable set
card {F,g,x,x,A,x9} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
{g,x,x,A,x9} is non empty finite countable set
card {g,x,x,A,x9} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
1 + (card {g,x,x,A,x9}) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
1 + 5 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
{F} is non empty trivial finite 1 -element countable set
card {F} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
{F} \/ {g,x,x,A,x9} is non empty finite countable set
7 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of NAT
F is set
g is set
x is set
x is set
A is set
x9 is set
f9 is set
{F,g,x,x,A,x9,f9} is non empty finite countable set
card {F,g,x,x,A,x9,f9} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
{g,x,x,A,x9,f9} is non empty finite countable set
card {g,x,x,A,x9,f9} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
1 + (card {g,x,x,A,x9,f9}) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
1 + 6 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
{F} is non empty trivial finite 1 -element countable set
card {F} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
{F} \/ {g,x,x,A,x9,f9} is non empty finite countable set
8 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of NAT
F is set
g is set
x is set
x is set
A is set
x9 is set
f9 is set
N is set
{F,g,x,x,A,x9,f9,N} is non empty finite countable set
card {F,g,x,x,A,x9,f9,N} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
{g,x,x,A,x9,f9,N} is non empty finite countable set
card {g,x,x,A,x9,f9,N} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
1 + (card {g,x,x,A,x9,f9,N}) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
1 + 7 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
{F} is non empty trivial finite 1 -element countable set
{F} \/ {g,x,x,A,x9,f9,N} is non empty finite countable set
card {F} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
F is set
g is set
{F,g} is non empty finite countable set
card {F,g} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
{F} is non empty trivial finite 1 -element countable set
card {F} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
{g} is non empty trivial finite 1 -element countable set
card {g} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
{F} \/ {g} is non empty finite countable set
1 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
F is set
g is set
x is set
{F,g,x} is non empty finite countable set
card {F,g,x} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
{F,g} is non empty finite countable set
card {F,g} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
{x} is non empty trivial finite 1 -element countable set
{F,g} \/ {x} is non empty finite countable set
2 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
F is set
g is set
x is set
x is set
{F,g,x,x} is non empty finite countable set
card {F,g,x,x} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
{F,g,x} is non empty finite countable set
card {F,g,x} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
{x} is non empty trivial finite 1 -element countable set
{F,g,x} \/ {x} is non empty finite countable set
3 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
F is set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
g is set
{g} is non empty trivial finite 1 -element countable set
F \ {g} is Element of bool F
bool F is non empty cup-closed diff-closed preBoolean set
card (F \ {g}) is epsilon-transitive epsilon-connected ordinal cardinal set
x is finite countable set
card x is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card {g} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
(card x) - (card {g}) is ext-real V36() V37() set
2 - 1 is ext-real V36() V37() set
x is set
{x} is non empty trivial finite 1 -element countable set
{g,x} is non empty finite countable set
A is set
A is set
F is Relation-like Function-like set
proj2 F is set
card (proj2 F) is epsilon-transitive epsilon-connected ordinal cardinal set
proj1 F is set
card (proj1 F) is epsilon-transitive epsilon-connected ordinal cardinal set
F .: (proj1 F) is set
F is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
g is finite countable set
card g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
F + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
the Element of g is Element of g
x is set
{x} is non empty trivial finite 1 -element countable set
union g is set
{ the Element of g} is non empty trivial finite 1 -element countable set
g \ { the Element of g} is finite countable Element of bool g
bool g is non empty finite V42() countable cup-closed diff-closed preBoolean set
A is finite countable set
card A is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card { the Element of g} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
(F + 1) - (card { the Element of g}) is ext-real V36() V37() set
(F + 1) - 1 is ext-real V36() V37() set
x9 is set
f9 is set
union A is set
(g \ { the Element of g}) \/ { the Element of g} is non empty finite countable set
x9 is set
x9 is set
union g is set
union { the Element of g} is set
(union A) \/ (union { the Element of g}) is set
(union A) \/ the Element of g is set
F is finite countable set
union F is set
card F is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
g is finite countable set
card g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
union g is set
g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
x is finite countable set
card x is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
g + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
union x is set
F is set
union F is set
F is set
g is set
x is set
x is set
A is set
{F,g,x,x,A} is non empty finite countable set
card {F,g,x,x,A} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
{F,g,x,x} is non empty finite countable set
{A} is non empty trivial finite 1 -element countable set
{F,g,x,x} \/ {A} is non empty finite countable set
card {F,g,x,x} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
4 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
F is set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
g is set
card g is epsilon-transitive epsilon-connected ordinal cardinal set
F is set
g is set
[F,g] is non empty V22() set
{F,g} is non empty finite countable set
{F} is non empty trivial finite 1 -element countable set
{{F,g},{F}} is non empty finite V42() countable V53() V54() set
x is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
card x is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal cardinal set
F --> g is Relation-like F -defined {g} -valued Function-like constant V21(F) quasi_total Cardinal-yielding Element of bool [:F,{g}:]
{g} is non empty trivial finite 1 -element countable set
[:F,{g}:] is Relation-like set
bool [:F,{g}:] is non empty cup-closed diff-closed preBoolean set
Sum (F --> g) is epsilon-transitive epsilon-connected ordinal cardinal set
disjoin (F --> g) is Relation-like Function-like set
Union (disjoin (F --> g)) is set
proj2 (disjoin (F --> g)) is set
union (proj2 (disjoin (F --> g))) is set
card (Union (disjoin (F --> g))) is epsilon-transitive epsilon-connected ordinal cardinal set
(F,g) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,g:] is Relation-like set
card [:F,g:] is epsilon-transitive epsilon-connected ordinal cardinal set
[:g,F:] is Relation-like set
card [:g,F:] is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal cardinal set
F --> g is Relation-like F -defined {g} -valued Function-like constant V21(F) quasi_total Cardinal-yielding Element of bool [:F,{g}:]
{g} is non empty trivial finite 1 -element countable set
[:F,{g}:] is Relation-like set
bool [:F,{g}:] is non empty cup-closed diff-closed preBoolean set
Product (F --> g) is epsilon-transitive epsilon-connected ordinal cardinal set
product (F --> g) is functional with_common_domain product-like set
card (product (F --> g)) is epsilon-transitive epsilon-connected ordinal cardinal set
(g,F) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (F,g) is functional set
card (Funcs (F,g)) is epsilon-transitive epsilon-connected ordinal cardinal set
F1() is finite countable set
F is finite countable set
card F is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
F is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
F + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
g is finite countable set
card g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
the Element of g is Element of g
{ the Element of g} is non empty trivial finite 1 -element countable set
g \ { the Element of g} is finite countable Element of bool g
bool g is non empty finite V42() countable cup-closed diff-closed preBoolean set
x is set
card (g \ { the Element of g}) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card { the Element of g} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
(F + 1) - (card { the Element of g}) is ext-real V36() V37() set
x is set
A is set
A is set
A is set
x9 is set
x is set
A is set
card F1() is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
F1() is finite countable set
F is finite countable set
card F is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
F is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
F + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
g is finite countable set
card g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
the Element of g is Element of g
{ the Element of g} is non empty trivial finite 1 -element countable set
g \ { the Element of g} is finite countable Element of bool g
bool g is non empty finite V42() countable cup-closed diff-closed preBoolean set
x is set
card (g \ { the Element of g}) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card { the Element of g} is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
(F + 1) - (card { the Element of g}) is ext-real V36() V37() set
x is set
A is set
x9 is set
x is set
A is set
card F1() is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
F is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
Rank F is set
F + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
Rank (F + 1) is set
succ F is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable set
{F} is non empty trivial finite V42() 1 -element countable set
F \/ {F} is non empty finite countable set
bool (Rank F) is non empty cup-closed diff-closed preBoolean set
card 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
card 2 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
F is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
Rank F is set
Rank 0 is set
g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
Rank g is set
g + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
Rank (g + 1) is set
F is epsilon-transitive epsilon-connected ordinal cardinal set
0 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
card 0 is Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty trivial Function-yielding V29() ext-real V36() V37() finite finite-yielding V42() cardinal {} -element Cardinal-yielding countable Element of omega
nextcard (card 0) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
1 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
nextcard (card 1) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
g +^ x is epsilon-transitive epsilon-connected ordinal set
g +^ 0 is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
g +^ x is epsilon-transitive epsilon-connected ordinal set
x + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
g +^ (x + 1) is epsilon-transitive epsilon-connected ordinal set
succ x is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable set
{x} is non empty trivial finite V42() 1 -element countable set
x \/ {x} is non empty finite countable set
succ (g +^ x) is epsilon-transitive epsilon-connected ordinal non empty set
{(g +^ x)} is non empty trivial finite 1 -element countable set
(g +^ x) \/ {(g +^ x)} is non empty set
g is epsilon-transitive epsilon-connected ordinal set
g +^ 1 is epsilon-transitive epsilon-connected ordinal set
succ g is epsilon-transitive epsilon-connected ordinal non empty set
{g} is non empty trivial finite 1 -element countable set
g \/ {g} is non empty set
F is epsilon-transitive epsilon-connected ordinal set
succ F is epsilon-transitive epsilon-connected ordinal non empty set
{F} is non empty trivial finite 1 -element countable set
F \/ {F} is non empty set
g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
succ g is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable set
{g} is non empty trivial finite V42() 1 -element countable set
g \/ {g} is non empty finite countable set
F +^ (succ g) is epsilon-transitive epsilon-connected ordinal set
(succ F) +^ g is epsilon-transitive epsilon-connected ordinal set
g + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
F +^ (g + 1) is epsilon-transitive epsilon-connected ordinal set
succ 0 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable set
0 \/ {0} is non empty finite V42() countable set
F +^ (succ 0) is epsilon-transitive epsilon-connected ordinal set
(succ F) +^ 0 is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
succ x is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable set
{x} is non empty trivial finite V42() 1 -element countable set
x \/ {x} is non empty finite countable set
F +^ (succ x) is epsilon-transitive epsilon-connected ordinal set
(succ F) +^ x is epsilon-transitive epsilon-connected ordinal set
x + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
succ (x + 1) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable set
{(x + 1)} is non empty trivial finite V42() 1 -element countable set
(x + 1) \/ {(x + 1)} is non empty finite countable set
F +^ (succ (x + 1)) is epsilon-transitive epsilon-connected ordinal set
(succ F) +^ (x + 1) is epsilon-transitive epsilon-connected ordinal set
succ ((succ F) +^ x) is epsilon-transitive epsilon-connected ordinal non empty set
{((succ F) +^ x)} is non empty trivial finite 1 -element countable set
((succ F) +^ x) \/ {((succ F) +^ x)} is non empty set
((succ F) +^ x) +^ 1 is epsilon-transitive epsilon-connected ordinal set
x +^ 1 is epsilon-transitive epsilon-connected ordinal set
(succ F) +^ (x +^ 1) is epsilon-transitive epsilon-connected ordinal set
succ 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable set
1 \/ {1} is non empty finite countable set
F is epsilon-transitive epsilon-connected ordinal set
F *^ (succ 1) is epsilon-transitive epsilon-connected ordinal set
{} +^ {} is epsilon-transitive epsilon-connected ordinal set
0 *^ 2 is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
g *^ 2 is epsilon-transitive epsilon-connected ordinal set
succ g is epsilon-transitive epsilon-connected ordinal non empty set
{g} is non empty trivial finite 1 -element countable set
g \/ {g} is non empty set
(succ g) *^ 2 is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
g +^ x is epsilon-transitive epsilon-connected ordinal set
x + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
(succ g) +^ (x + 1) is epsilon-transitive epsilon-connected ordinal set
(g *^ 2) +^ 2 is epsilon-transitive epsilon-connected ordinal set
g *^ (succ 1) is epsilon-transitive epsilon-connected ordinal set
(g *^ (succ 1)) +^ 1 is epsilon-transitive epsilon-connected ordinal set
succ ((g *^ (succ 1)) +^ 1) is epsilon-transitive epsilon-connected ordinal non empty set
{((g *^ (succ 1)) +^ 1)} is non empty trivial finite 1 -element countable set
((g *^ (succ 1)) +^ 1) \/ {((g *^ (succ 1)) +^ 1)} is non empty set
succ (g +^ x) is epsilon-transitive epsilon-connected ordinal non empty set
{(g +^ x)} is non empty trivial finite 1 -element countable set
(g +^ x) \/ {(g +^ x)} is non empty set
succ (succ (g +^ x)) is epsilon-transitive epsilon-connected ordinal non empty set
{(succ (g +^ x))} is non empty trivial finite 1 -element countable V53() V54() set
(succ (g +^ x)) \/ {(succ (g +^ x))} is non empty set
succ x is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable set
{x} is non empty trivial finite V42() 1 -element countable set
x \/ {x} is non empty finite countable set
g +^ (succ x) is epsilon-transitive epsilon-connected ordinal set
succ (g +^ (succ x)) is epsilon-transitive epsilon-connected ordinal non empty set
{(g +^ (succ x))} is non empty trivial finite 1 -element countable set
(g +^ (succ x)) \/ {(g +^ (succ x))} is non empty set
g +^ (x + 1) is epsilon-transitive epsilon-connected ordinal set
succ (g +^ (x + 1)) is epsilon-transitive epsilon-connected ordinal non empty set
{(g +^ (x + 1))} is non empty trivial finite 1 -element countable set
(g +^ (x + 1)) \/ {(g +^ (x + 1))} is non empty set
succ (x + 1) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable set
{(x + 1)} is non empty trivial finite V42() 1 -element countable set
(x + 1) \/ {(x + 1)} is non empty finite countable set
g +^ (succ (x + 1)) is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
g *^ 2 is epsilon-transitive epsilon-connected ordinal set
g +^ 0 is epsilon-transitive epsilon-connected ordinal set
x is Relation-like T-Sequence-like Function-like Ordinal-yielding set
proj1 x is epsilon-transitive epsilon-connected ordinal set
sup x is epsilon-transitive epsilon-connected ordinal set
union (sup x) is epsilon-transitive epsilon-connected ordinal set
proj2 x is set
sup (proj2 x) is epsilon-transitive epsilon-connected ordinal set
union (sup (proj2 x)) is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal set
A is set
x9 is epsilon-transitive epsilon-connected ordinal set
f9 is epsilon-transitive epsilon-connected ordinal set
N is set
x . N is set
K is epsilon-transitive epsilon-connected ordinal set
K *^ 2 is epsilon-transitive epsilon-connected ordinal set
M is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
K +^ M is epsilon-transitive epsilon-connected ordinal set
g +^ {} is epsilon-transitive epsilon-connected ordinal set
g *^ 1 is epsilon-transitive epsilon-connected ordinal set
F is epsilon-transitive epsilon-connected ordinal set
F *^ (succ 1) is epsilon-transitive epsilon-connected ordinal set
F *^ 2 is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
F +^ g is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
x + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
succ x is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable set
{x} is non empty trivial finite V42() 1 -element countable set
x \/ {x} is non empty finite countable set
F +^ x is epsilon-transitive epsilon-connected ordinal set
succ (F +^ x) is epsilon-transitive epsilon-connected ordinal non empty set
{(F +^ x)} is non empty trivial finite 1 -element countable set
(F +^ x) \/ {(F +^ x)} is non empty set
F is epsilon-transitive epsilon-connected ordinal set
1 +^ F is epsilon-transitive epsilon-connected ordinal set
g is Relation-like T-Sequence-like Function-like Ordinal-yielding set
proj1 g is epsilon-transitive epsilon-connected ordinal set
1 +^ omega is epsilon-transitive epsilon-connected ordinal set
sup g is epsilon-transitive epsilon-connected ordinal set
proj2 g is set
sup (proj2 g) is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal set
A is set
g . A is set
x9 is epsilon-transitive epsilon-connected ordinal set
N is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
1 +^ N is epsilon-transitive epsilon-connected ordinal set
succ N is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable set
{N} is non empty trivial finite V42() 1 -element countable set
N \/ {N} is non empty finite countable set
x is epsilon-transitive epsilon-connected ordinal set
omega +^ x is epsilon-transitive epsilon-connected ordinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal set
succ g is epsilon-transitive epsilon-connected ordinal non empty set
{g} is non empty trivial finite 1 -element countable set
g \/ {g} is non empty set
g +^ 1 is epsilon-transitive epsilon-connected ordinal set
card (g +^ 1) is epsilon-transitive epsilon-connected ordinal cardinal set
card g is epsilon-transitive epsilon-connected ordinal cardinal set
((card 1),(card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
(card 1) +^ (card g) is epsilon-transitive epsilon-connected ordinal set
card ((card 1) +^ (card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
1 +^ g is epsilon-transitive epsilon-connected ordinal set
card (1 +^ g) is epsilon-transitive epsilon-connected ordinal cardinal set
card (succ g) is epsilon-transitive epsilon-connected ordinal non empty cardinal set
x is epsilon-transitive epsilon-connected ordinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
(F,F) is epsilon-transitive epsilon-connected ordinal cardinal set
F +^ F is epsilon-transitive epsilon-connected ordinal set
card (F +^ F) is epsilon-transitive epsilon-connected ordinal cardinal set
F *^ (succ 1) is epsilon-transitive epsilon-connected ordinal set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
((card 2),(card F)) is epsilon-transitive epsilon-connected ordinal cardinal set
[:(card 2),(card F):] is Relation-like set
card [:(card 2),(card F):] is epsilon-transitive epsilon-connected ordinal cardinal set
(succ 1) *^ F is epsilon-transitive epsilon-connected ordinal set
card ((succ 1) *^ F) is epsilon-transitive epsilon-connected ordinal cardinal set
1 *^ F is epsilon-transitive epsilon-connected ordinal set
(1 *^ F) +^ F is epsilon-transitive epsilon-connected ordinal set
card ((1 *^ F) +^ F) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal cardinal set
(F,g) is epsilon-transitive epsilon-connected ordinal cardinal set
F +^ g is epsilon-transitive epsilon-connected ordinal set
card (F +^ g) is epsilon-transitive epsilon-connected ordinal cardinal set
(g,F) is epsilon-transitive epsilon-connected ordinal cardinal set
g +^ F is epsilon-transitive epsilon-connected ordinal set
card (g +^ F) is epsilon-transitive epsilon-connected ordinal cardinal set
(F,F) is epsilon-transitive epsilon-connected ordinal cardinal set
F +^ F is epsilon-transitive epsilon-connected ordinal set
card (F +^ F) is epsilon-transitive epsilon-connected ordinal cardinal set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
F is set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
g is set
F \/ g is set
card (F \/ g) is epsilon-transitive epsilon-connected ordinal cardinal set
card g is epsilon-transitive epsilon-connected ordinal cardinal set
((card F),(card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
(card F) +^ (card g) is epsilon-transitive epsilon-connected ordinal set
card ((card F) +^ (card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
F is set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
g is set
F \/ g is set
card (F \/ g) is epsilon-transitive epsilon-connected ordinal cardinal set
card g is epsilon-transitive epsilon-connected ordinal cardinal set
((card F),(card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
(card F) +^ (card g) is epsilon-transitive epsilon-connected ordinal set
card ((card F) +^ (card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
F is set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
g is set
card g is epsilon-transitive epsilon-connected ordinal cardinal set
F \/ g is set
card (F \/ g) is epsilon-transitive epsilon-connected ordinal cardinal set
((card F),(card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
(card F) +^ (card g) is epsilon-transitive epsilon-connected ordinal set
card ((card F) +^ (card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
(F,g) is epsilon-transitive epsilon-connected ordinal cardinal set
F +^ g is epsilon-transitive epsilon-connected ordinal set
card (F +^ g) is epsilon-transitive epsilon-connected ordinal cardinal set
card F is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
(card F) + (card g) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
card ((card F) + (card g)) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal cardinal set
(F,g) is epsilon-transitive epsilon-connected ordinal cardinal set
F +^ g is epsilon-transitive epsilon-connected ordinal set
card (F +^ g) is epsilon-transitive epsilon-connected ordinal cardinal set
(g,F) is epsilon-transitive epsilon-connected ordinal cardinal set
g +^ F is epsilon-transitive epsilon-connected ordinal set
card (g +^ F) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
(F,g) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,g:] is Relation-like finite countable set
card [:F,g:] is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal cardinal set
x is epsilon-transitive epsilon-connected ordinal cardinal set
(F,x) is epsilon-transitive epsilon-connected ordinal cardinal set
F +^ x is epsilon-transitive epsilon-connected ordinal set
card (F +^ x) is epsilon-transitive epsilon-connected ordinal cardinal set
(x,F) is epsilon-transitive epsilon-connected ordinal cardinal set
x +^ F is epsilon-transitive epsilon-connected ordinal set
card (x +^ F) is epsilon-transitive epsilon-connected ordinal cardinal set
x is epsilon-transitive epsilon-connected ordinal cardinal set
(g,x) is epsilon-transitive epsilon-connected ordinal cardinal set
g +^ x is epsilon-transitive epsilon-connected ordinal set
card (g +^ x) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal cardinal set
x is epsilon-transitive epsilon-connected ordinal cardinal set
(x,F) is epsilon-transitive epsilon-connected ordinal cardinal set
x +^ F is epsilon-transitive epsilon-connected ordinal set
card (x +^ F) is epsilon-transitive epsilon-connected ordinal cardinal set
(x,g) is epsilon-transitive epsilon-connected ordinal cardinal set
x +^ g is epsilon-transitive epsilon-connected ordinal set
card (x +^ g) is epsilon-transitive epsilon-connected ordinal cardinal set
(g,x) is epsilon-transitive epsilon-connected ordinal cardinal set
g +^ x is epsilon-transitive epsilon-connected ordinal set
card (g +^ x) is epsilon-transitive epsilon-connected ordinal cardinal set
(F,x) is epsilon-transitive epsilon-connected ordinal cardinal set
F +^ x is epsilon-transitive epsilon-connected ordinal set
card (F +^ x) is epsilon-transitive epsilon-connected ordinal cardinal set
F is set
g is set
F \/ g is set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
card g is epsilon-transitive epsilon-connected ordinal cardinal set
card (F \/ g) is epsilon-transitive epsilon-connected ordinal cardinal set
((card F),(card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
(card F) +^ (card g) is epsilon-transitive epsilon-connected ordinal set
card ((card F) +^ (card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
(omega,omega) is epsilon-transitive epsilon-connected ordinal cardinal set
omega +^ omega is epsilon-transitive epsilon-connected ordinal set
card (omega +^ omega) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal cardinal set
(F,g) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,g:] is Relation-like set
card [:F,g:] is epsilon-transitive epsilon-connected ordinal cardinal set
x is Relation-like Function-like set
proj1 x is set
card (proj1 x) is epsilon-transitive epsilon-connected ordinal cardinal set
Union x is set
proj2 x is set
union (proj2 x) is set
card (Union x) is epsilon-transitive epsilon-connected ordinal cardinal set
Card x is Relation-like Function-like Cardinal-yielding set
Sum (Card x) is epsilon-transitive epsilon-connected ordinal cardinal set
disjoin (Card x) is Relation-like Function-like set
Union (disjoin (Card x)) is set
proj2 (disjoin (Card x)) is set
union (proj2 (disjoin (Card x))) is set
card (Union (disjoin (Card x))) is epsilon-transitive epsilon-connected ordinal cardinal set
proj1 (Card x) is set
(proj1 x) --> g is Relation-like proj1 x -defined {g} -valued Function-like constant V21( proj1 x) quasi_total Cardinal-yielding Element of bool [:(proj1 x),{g}:]
{g} is non empty trivial finite 1 -element countable set
[:(proj1 x),{g}:] is Relation-like set
bool [:(proj1 x),{g}:] is non empty cup-closed diff-closed preBoolean set
dom ((proj1 x) --> g) is Element of bool (proj1 x)
bool (proj1 x) is non empty cup-closed diff-closed preBoolean set
x is set
(Card x) . x is set
x . x is set
card (x . x) is epsilon-transitive epsilon-connected ordinal cardinal set
((proj1 x) --> g) . x is set
Sum ((proj1 x) --> g) is epsilon-transitive epsilon-connected ordinal cardinal set
disjoin ((proj1 x) --> g) is Relation-like Function-like set
Union (disjoin ((proj1 x) --> g)) is set
proj2 (disjoin ((proj1 x) --> g)) is set
union (proj2 (disjoin ((proj1 x) --> g))) is set
card (Union (disjoin ((proj1 x) --> g))) is epsilon-transitive epsilon-connected ordinal cardinal set
[:(card (proj1 x)),g:] is Relation-like set
[:g,(proj1 x):] is Relation-like set
card [:g,(proj1 x):] is epsilon-transitive epsilon-connected ordinal cardinal set
[:g,(card (proj1 x)):] is Relation-like set
card [:g,(card (proj1 x)):] is epsilon-transitive epsilon-connected ordinal cardinal set
card [:(card (proj1 x)),g:] is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal cardinal set
(F,g) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,g:] is Relation-like set
card [:F,g:] is epsilon-transitive epsilon-connected ordinal cardinal set
x is set
card x is epsilon-transitive epsilon-connected ordinal cardinal set
union x is set
card (union x) is epsilon-transitive epsilon-connected ordinal cardinal set
x is set
id x is Relation-like x -defined x -valued Function-like one-to-one set
dom (id x) is Element of bool x
bool x is non empty cup-closed diff-closed preBoolean set
(id x) . x is set
card ((id x) . x) is epsilon-transitive epsilon-connected ordinal cardinal set
Union (id x) is set
proj2 (id x) is set
union (proj2 (id x)) is set
card (Union (id x)) is epsilon-transitive epsilon-connected ordinal cardinal set
F is Relation-like Function-like set
proj1 F is set
Union F is set
proj2 F is set
union (proj2 F) is set
g is finite countable set
x is set
F . x is set
card (F . x) is epsilon-transitive epsilon-connected ordinal cardinal set
x is set
F . x is set
card (F . x) is epsilon-transitive epsilon-connected ordinal cardinal set
x is set
F . x is set
card (F . x) is epsilon-transitive epsilon-connected ordinal cardinal set
x is set
F . x is set
card (F . x) is epsilon-transitive epsilon-connected ordinal cardinal set
A is set
F . A is set
card (F . A) is epsilon-transitive epsilon-connected ordinal cardinal set
x is set
F . x is set
card (F . x) is epsilon-transitive epsilon-connected ordinal cardinal set
card (Union F) is epsilon-transitive epsilon-connected ordinal cardinal set
card g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card (card g) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
((card (card g)),(card (F . x))) is epsilon-transitive epsilon-connected ordinal cardinal set
[:(card (card g)),(card (F . x)):] is Relation-like set
card [:(card (card g)),(card (F . x)):] is epsilon-transitive epsilon-connected ordinal cardinal set
x is finite countable set
card x is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card (card x) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
(card g) * (card x) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
card ((card g) * (card x)) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
F is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
card F is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
(omega,(card F)) is epsilon-transitive epsilon-connected ordinal cardinal set
[:omega,(card F):] is Relation-like set
card [:omega,(card F):] is epsilon-transitive epsilon-connected ordinal cardinal set
((card F),omega) is epsilon-transitive epsilon-connected ordinal cardinal set
[:(card F),omega:] is Relation-like set
card [:(card F),omega:] is epsilon-transitive epsilon-connected ordinal cardinal set
card 0 is Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty trivial Function-yielding V29() ext-real V36() V37() finite finite-yielding V42() cardinal {} -element Cardinal-yielding countable Element of omega
(omega,(card 0)) is epsilon-transitive epsilon-connected ordinal cardinal set
[:omega,(card 0):] is Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty trivial Function-yielding V29() ext-real V36() V37() finite finite-yielding V42() cardinal {} -element Cardinal-yielding countable set
card [:omega,(card 0):] is Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty trivial Function-yielding V29() ext-real V36() V37() finite finite-yielding V42() cardinal {} -element Cardinal-yielding countable set
g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
card g is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
(omega,(card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
[:omega,(card g):] is Relation-like set
card [:omega,(card g):] is epsilon-transitive epsilon-connected ordinal cardinal set
g + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
card (g + 1) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
(omega,(card (g + 1))) is epsilon-transitive epsilon-connected ordinal cardinal set
[:omega,(card (g + 1)):] is Relation-like set
card [:omega,(card (g + 1)):] is epsilon-transitive epsilon-connected ordinal cardinal set
succ g is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable set
{g} is non empty trivial finite V42() 1 -element countable set
g \/ {g} is non empty finite countable set
card (succ g) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V36() V37() finite cardinal countable Element of omega
(succ g) *^ omega is epsilon-transitive epsilon-connected ordinal set
card ((succ g) *^ omega) is epsilon-transitive epsilon-connected ordinal cardinal set
g *^ omega is epsilon-transitive epsilon-connected ordinal set
(g *^ omega) +^ omega is epsilon-transitive epsilon-connected ordinal set
card ((g *^ omega) +^ omega) is epsilon-transitive epsilon-connected ordinal cardinal set
card (g *^ omega) is epsilon-transitive epsilon-connected ordinal cardinal set
((card (g *^ omega)),omega) is epsilon-transitive epsilon-connected ordinal cardinal set
(card (g *^ omega)) +^ omega is epsilon-transitive epsilon-connected ordinal set
card ((card (g *^ omega)) +^ omega) is epsilon-transitive epsilon-connected ordinal cardinal set
((omega,(card g)),omega) is epsilon-transitive epsilon-connected ordinal cardinal set
(omega,(card g)) +^ omega is epsilon-transitive epsilon-connected ordinal set
card ((omega,(card g)) +^ omega) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal cardinal set
x is epsilon-transitive epsilon-connected ordinal cardinal set
(F,x) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,x:] is Relation-like set
card [:F,x:] is epsilon-transitive epsilon-connected ordinal cardinal set
(x,F) is epsilon-transitive epsilon-connected ordinal cardinal set
[:x,F:] is Relation-like set
card [:x,F:] is epsilon-transitive epsilon-connected ordinal cardinal set
x is epsilon-transitive epsilon-connected ordinal cardinal set
(g,x) is epsilon-transitive epsilon-connected ordinal cardinal set
[:g,x:] is Relation-like set
card [:g,x:] is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal cardinal set
x is epsilon-transitive epsilon-connected ordinal cardinal set
(x,F) is epsilon-transitive epsilon-connected ordinal cardinal set
[:x,F:] is Relation-like set
card [:x,F:] is epsilon-transitive epsilon-connected ordinal cardinal set
(x,g) is epsilon-transitive epsilon-connected ordinal cardinal set
[:x,g:] is Relation-like set
card [:x,g:] is epsilon-transitive epsilon-connected ordinal cardinal set
(g,x) is epsilon-transitive epsilon-connected ordinal cardinal set
[:g,x:] is Relation-like set
card [:g,x:] is epsilon-transitive epsilon-connected ordinal cardinal set
(F,x) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,x:] is Relation-like set
card [:F,x:] is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal cardinal set
x is epsilon-transitive epsilon-connected ordinal cardinal set
(F,x) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (x,F) is functional set
card (Funcs (x,F)) is epsilon-transitive epsilon-connected ordinal cardinal set
x is epsilon-transitive epsilon-connected ordinal cardinal set
(g,x) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (x,g) is functional set
card (Funcs (x,g)) is epsilon-transitive epsilon-connected ordinal cardinal set
x \ x is Element of bool x
bool x is non empty cup-closed diff-closed preBoolean set
Funcs ((x \ x),g) is functional set
card (Funcs ((x \ x),g)) is epsilon-transitive epsilon-connected ordinal cardinal set
card 0 is Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty trivial Function-yielding V29() ext-real V36() V37() finite finite-yielding V42() cardinal {} -element Cardinal-yielding countable Element of omega
nextcard (card 0) is epsilon-transitive epsilon-connected ordinal cardinal set
0 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
x \/ (x \ x) is set
Funcs (x,g) is functional set
card (Funcs (x,g)) is epsilon-transitive epsilon-connected ordinal cardinal set
[:(Funcs (x,g)),(Funcs ((x \ x),g)):] is Relation-like set
card [:(Funcs (x,g)),(Funcs ((x \ x),g)):] is epsilon-transitive epsilon-connected ordinal cardinal set
[:(card (Funcs (x,g))),(card (Funcs ((x \ x),g))):] is Relation-like set
card [:(card (Funcs (x,g))),(card (Funcs ((x \ x),g))):] is epsilon-transitive epsilon-connected ordinal cardinal set
((card (Funcs (x,g))),(card (Funcs ((x \ x),g)))) is epsilon-transitive epsilon-connected ordinal cardinal set
(1,(card (Funcs (x,g)))) is epsilon-transitive epsilon-connected ordinal cardinal set
[:1,(card (Funcs (x,g))):] is Relation-like set
card [:1,(card (Funcs (x,g))):] is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal cardinal set
x is epsilon-transitive epsilon-connected ordinal cardinal set
(x,F) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (F,x) is functional set
card (Funcs (F,x)) is epsilon-transitive epsilon-connected ordinal cardinal set
(x,g) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (g,x) is functional set
card (Funcs (g,x)) is epsilon-transitive epsilon-connected ordinal cardinal set
(F,x) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (x,F) is functional set
card (Funcs (x,F)) is epsilon-transitive epsilon-connected ordinal cardinal set
(g,x) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (x,g) is functional set
card (Funcs (x,g)) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal cardinal set
(F,g) is epsilon-transitive epsilon-connected ordinal cardinal set
F +^ g is epsilon-transitive epsilon-connected ordinal set
card (F +^ g) is epsilon-transitive epsilon-connected ordinal cardinal set
card g is epsilon-transitive epsilon-connected ordinal cardinal set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal cardinal set
(g,F) is epsilon-transitive epsilon-connected ordinal cardinal set
[:g,F:] is Relation-like set
card [:g,F:] is epsilon-transitive epsilon-connected ordinal cardinal set
(F,g) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,g:] is Relation-like set
card [:F,g:] is epsilon-transitive epsilon-connected ordinal cardinal set
card g is epsilon-transitive epsilon-connected ordinal cardinal set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
g *^ F is epsilon-transitive epsilon-connected ordinal set
card (g *^ F) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal cardinal set
x is epsilon-transitive epsilon-connected ordinal cardinal set
(F,x) is epsilon-transitive epsilon-connected ordinal cardinal set
F +^ x is epsilon-transitive epsilon-connected ordinal set
card (F +^ x) is epsilon-transitive epsilon-connected ordinal cardinal set
(x,F) is epsilon-transitive epsilon-connected ordinal cardinal set
x +^ F is epsilon-transitive epsilon-connected ordinal set
card (x +^ F) is epsilon-transitive epsilon-connected ordinal cardinal set
x is epsilon-transitive epsilon-connected ordinal cardinal set
(g,x) is epsilon-transitive epsilon-connected ordinal cardinal set
g +^ x is epsilon-transitive epsilon-connected ordinal set
card (g +^ x) is epsilon-transitive epsilon-connected ordinal cardinal set
A is epsilon-transitive epsilon-connected ordinal cardinal set
x9 is epsilon-transitive epsilon-connected ordinal cardinal set
f9 is epsilon-transitive epsilon-connected ordinal cardinal set
(A,f9) is epsilon-transitive epsilon-connected ordinal cardinal set
A +^ f9 is epsilon-transitive epsilon-connected ordinal set
card (A +^ f9) is epsilon-transitive epsilon-connected ordinal cardinal set
N is epsilon-transitive epsilon-connected ordinal cardinal set
(x9,N) is epsilon-transitive epsilon-connected ordinal cardinal set
x9 +^ N is epsilon-transitive epsilon-connected ordinal set
card (x9 +^ N) is epsilon-transitive epsilon-connected ordinal cardinal set
K is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
card K is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
M is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
card M is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
M is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
card M is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
K is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
card K is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
(K,M) is epsilon-transitive epsilon-connected ordinal cardinal set
K +^ M is epsilon-transitive epsilon-connected ordinal set
card (K +^ M) is epsilon-transitive epsilon-connected ordinal cardinal set
(card K) + (card M) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
card ((card K) + (card M)) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
(M,K) is epsilon-transitive epsilon-connected ordinal cardinal set
M +^ K is epsilon-transitive epsilon-connected ordinal set
card (M +^ K) is epsilon-transitive epsilon-connected ordinal cardinal set
(card M) + (card K) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
card ((card M) + (card K)) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
K is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
card K is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
M is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable set
card M is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
(K,M) is epsilon-transitive epsilon-connected ordinal cardinal set
K +^ M is epsilon-transitive epsilon-connected ordinal set
card (K +^ M) is epsilon-transitive epsilon-connected ordinal cardinal set
(card K) + (card M) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
card ((card K) + (card M)) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal cardinal set
(F,g) is epsilon-transitive epsilon-connected ordinal cardinal set
F +^ g is epsilon-transitive epsilon-connected ordinal set
card (F +^ g) is epsilon-transitive epsilon-connected ordinal cardinal set
x is epsilon-transitive epsilon-connected ordinal cardinal set
(F,x) is epsilon-transitive epsilon-connected ordinal cardinal set
F +^ x is epsilon-transitive epsilon-connected ordinal set
card (F +^ x) is epsilon-transitive epsilon-connected ordinal cardinal set
F is set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
g is set
card g is epsilon-transitive epsilon-connected ordinal cardinal set
((card F),(card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
(card F) +^ (card g) is epsilon-transitive epsilon-connected ordinal set
card ((card F) +^ (card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
F \ g is Element of bool F
bool F is non empty cup-closed diff-closed preBoolean set
card (F \ g) is epsilon-transitive epsilon-connected ordinal cardinal set
F \/ g is set
card (F \/ g) is epsilon-transitive epsilon-connected ordinal cardinal set
(F \ g) \/ g is set
((card (F \ g)),(card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
(card (F \ g)) +^ (card g) is epsilon-transitive epsilon-connected ordinal set
card ((card (F \ g)) +^ (card g)) is epsilon-transitive epsilon-connected ordinal cardinal set
((card F),(card F)) is epsilon-transitive epsilon-connected ordinal cardinal set
(card F) +^ (card F) is epsilon-transitive epsilon-connected ordinal set
card ((card F) +^ (card F)) is epsilon-transitive epsilon-connected ordinal cardinal set
x is finite countable set
card x is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card (card x) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
x is finite countable set
card x is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
(card x) + (card x) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
card ((card x) + (card x)) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
card (card x) is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of omega
(card x) + 0 is epsilon-transitive epsilon-connected ordinal natural ext-real V36() V37() finite cardinal countable Element of NAT
F is epsilon-transitive epsilon-connected ordinal cardinal set
g is epsilon-transitive epsilon-connected ordinal cardinal set
(F,g) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,g:] is Relation-like set
card [:F,g:] is epsilon-transitive epsilon-connected ordinal cardinal set
x is epsilon-transitive epsilon-connected ordinal cardinal set
(F,x) is epsilon-transitive epsilon-connected ordinal cardinal set
[:F,x:] is Relation-like set
card [:F,x:] is epsilon-transitive epsilon-connected ordinal cardinal set
F is set
g is set
F \+\ g is set
F \ g is set
g \ F is set
(F \ g) \/ (g \ F) is set
F \ g is Element of bool F
bool F is non empty cup-closed diff-closed preBoolean set
g \ F is Element of bool g
bool g is non empty cup-closed diff-closed preBoolean set
F is finite countable set
g is set
Fin g is non empty cup-closed diff-closed preBoolean set
[:F,(Fin g):] is Relation-like set
bool [:F,(Fin g):] is non empty cup-closed diff-closed preBoolean set
x is Relation-like F -defined Fin g -valued Function-like V21(F) quasi_total finite countable Element of bool [:F,(Fin g):]
Union x is set
proj2 x is finite countable set
union (proj2 x) is set
x is set
dom x is finite countable Element of bool F
bool F is non empty finite V42() countable cup-closed diff-closed preBoolean set
A is non empty set
[:A,(Fin g):] is Relation-like non empty set
bool [:A,(Fin g):] is non empty cup-closed diff-closed preBoolean set
f9 is Relation-like A -defined Fin g -valued Function-like non empty V21(A) quasi_total Element of bool [:A,(Fin g):]
x9 is Element of A
f9 . x9 is finite countable Element of Fin g
x . x is set
F is Relation-like Function-like finite finite-yielding countable set
product F is functional with_common_domain product-like set
proj1 F is finite countable set
Union F is set
proj2 F is finite V42() countable set
union (proj2 F) is finite countable set
Funcs ((proj1 F),(Union F)) is functional set
F is Relation-like Function-like set
proj1 F is set
proj2 F is set
g is Relation-like Function-like set
proj1 g is set
Union g is set
proj2 g is set
union (proj2 g) is set
x is set
F . x is set
g . (F . x) is set
{(F . x)} is non empty trivial finite 1 -element countable set
F " {(F . x)} is set
x is set
g . x is set
{x} is non empty trivial finite 1 -element countable set
F " {x} is set