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