:: CARD_2 semantic presentation

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 H

[: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 H

[:(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 H

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 H

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 H

[:F,(card H

card [:F,(card H

[:F,H

card [:F,H

[: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