:: CARD_3 semantic presentation

bool omega is non empty non trivial non empty-membered non finite V56() V58() V59() set

is non empty trivial functional finite V52() 1 -element set

X is set
proj1 x is set
x . X is set

X is set

A is set
proj1 (x | X) is set
(x | X) . A is set
x . A is set
proj1 x is set
() /\ X is set
x is set

{X} is non empty trivial finite 1 -element set

bool [:x,{X}:] is non empty V56() V58() V59() set
A is set
proj1 (x --> X) is set
(x --> X) . A is set
dom (x --> X) is Element of bool x
bool x is non empty V56() V58() V59() set
x is set

{x} is non empty trivial finite 1 -element set

{X} is non empty trivial finite 1 -element set
[:{x},{X}:] is non empty Relation-like finite set
bool [:{x},{X}:] is non empty finite V52() V56() V58() V59() set
F1() is set

proj1 x is set
X is set
x . X is set

proj1 X is set
A is set
X . A is set

proj1 x is set

proj1 X is set

proj1 A is set
Y is set
X . Y is set
x . Y is set

A . Y is set

proj1 X is set

proj1 A is set
Y is set
X . Y is set
x . Y is set
{Y} is non empty trivial finite 1 -element set
[:(x . Y),{Y}:] is Relation-like set
A . Y is set
proj2 x is set
union () is set
Funcs ((),(union ())) is set
X is set
A is set

proj1 Y is set
proj2 Y is set
Y is set
Y is set
Y . Y is set
x . Y is set
X is set
A is set

(x) is Relation-like Function-like () set
X is set
proj1 x is set
x . X is set

x is set
X is set

{X} is non empty trivial finite 1 -element set

bool [:x,{X}:] is non empty V56() V58() V59() set
((x --> X)) is Relation-like Function-like () set

{(card X)} is non empty trivial finite 1 -element set
[:x,{(card X)}:] is Relation-like set
bool [:x,{(card X)}:] is non empty V56() V58() V59() set
proj1 ((x --> X)) is set
dom (x --> X) is Element of bool x
bool x is non empty V56() V58() V59() set
dom (x --> (card X)) is Element of bool x
A is set
((x --> X)) . A is set
(x --> X) . A is set

(x --> (card X)) . A is set

proj1 ({}) is set
x is set
{x} is non empty trivial finite 1 -element set
X is set

{X} is non empty trivial finite 1 -element set
[:{x},{X}:] is non empty Relation-like finite set
bool [:{x},{X}:] is non empty finite V52() V56() V58() V59() set
((x .--> X)) is Relation-like Function-like set

{[:X,{x}:]} is non empty trivial finite 1 -element set
[:{x},{[:X,{x}:]}:] is non empty Relation-like finite set
bool [:{x},{[:X,{x}:]}:] is non empty finite V52() V56() V58() V59() set
(({x} --> X)) is Relation-like Function-like set
proj1 (({x} --> X)) is set
dom ({x} --> X) is non empty trivial finite 1 -element Element of bool {x}
bool {x} is non empty finite V52() V56() V58() V59() set
dom ({x} --> [:X,{x}:]) is non empty trivial finite 1 -element Element of bool {x}
A is set
(({x} --> X)) . A is set
({x} --> X) . A is set
{A} is non empty trivial finite 1 -element set
[:(({x} --> X) . A),{A}:] is Relation-like set
({x} --> [:X,{x}:]) . A is set
x is set
X is set

proj1 A is set

(A) . x is set
(A) . X is set
((A) . x) /\ ((A) . X) is set
the Element of ((A) . x) /\ ((A) . X) is Element of ((A) . x) /\ ((A) . X)
A . x is set
{x} is non empty trivial finite 1 -element set
[:(A . x),{x}:] is Relation-like set
A . X is set
{X} is non empty trivial finite 1 -element set
[:(A . X),{X}:] is Relation-like set
the Element of ((A) . x) /\ ((A) . X) `2 is set
x is set
X is set

{X} is non empty trivial finite 1 -element set

bool [:x,{X}:] is non empty V56() V58() V59() set
((x --> X)) is set
proj2 (x --> X) is trivial finite set
union (proj2 (x --> X)) is set
A is set
rng (x --> X) is trivial finite Element of bool {X}
bool {X} is non empty finite V52() V56() V58() V59() set
Y is set
dom (x --> X) is Element of bool x
bool x is non empty V56() V58() V59() set
Y is set
(x --> X) . Y is set
x is set
X is set

{X} is non empty trivial finite 1 -element set

bool [:x,{X}:] is non empty V56() V58() V59() set
((x --> X)) is set
proj2 (x --> X) is trivial finite set
union (proj2 (x --> X)) is set
the Element of x is Element of x
dom (x --> X) is Element of bool x
bool x is non empty V56() V58() V59() set
(x --> X) . the Element of x is set
rng (x --> X) is trivial finite Element of bool {X}
bool {X} is non empty finite V52() V56() V58() V59() set
x is set
X is set

{x} is non empty trivial finite 1 -element set

{X} is non empty trivial finite 1 -element set
[:{x},{X}:] is non empty Relation-like finite set
bool [:{x},{X}:] is non empty finite V52() V56() V58() V59() set
((x .--> X)) is set
proj2 (x .--> X) is trivial finite set
union (proj2 (x .--> X)) is set

proj1 x is set

(X) is set
proj1 X is set
A is set
x . A is set
X . A is set

proj1 Y is set
({}) is set
x is set

proj1 X is set
x is set
X is set

x is set
X is set
Funcs (x,X) is set

{X} is non empty trivial finite 1 -element set

bool [:x,{X}:] is non empty V56() V58() V59() set
((x --> X)) is set
dom (x --> X) is Element of bool x
bool x is non empty V56() V58() V59() set
Y is set

proj1 Y is set
proj2 Y is set
Y is set
(x --> X) . Y is set
Y . Y is set
Y is set

proj1 Y is set
proj2 Y is set
Y is set
c7 is set
Y . c7 is set
(x --> X) . c7 is set
x is set
X is set
A is set
Y is set

Y . x is set

proj1 Y is set
proj2 Y is set
Y is set
Y is set
Y . Y is set

c7 . x is set

Y . x is set
Y . Y is set

c7 . x is set
A is set
Y is set
x is set

proj1 X is set
(X) is set
(x,(X)) is set
X . x is set
A is set

Y . x is set
the Element of (X) is Element of (X)

proj1 Y is set
Y is set

proj1 Y is set
c7 is set
Y . c7 is set
Y . c7 is set
X . c7 is set
Y . x is set
x is set
(x,{}) is set
the Element of (x,{}) is Element of (x,{})

A . x is set
x is set

(x,{X}) is set
X . x is set
{(X . x)} is non empty trivial finite 1 -element set
A is set

Y . x is set
A is set
x is set

X . x is set

{X,A} is non empty functional finite set
(x,{X,A}) is set
A . x is set
{(X . x),(A . x)} is non empty finite set
Y is set

Y . x is set
Y is set
x is set
X is set
x \/ X is set
A is set
(A,(x \/ X)) is set
(A,x) is set
(A,X) is set
(A,x) \/ (A,X) is set
Y is set

Y . A is set
Y is set

Y . A is set

Y . A is set
x is set
X is set
x /\ X is set
A is set
(A,(x /\ X)) is set
(A,x) is set
(A,X) is set
(A,x) /\ (A,X) is set
Y is set

Y . A is set
x is set
X is set
(X,x) is set
A is set
(X,A) is set
(X,x) \ (X,A) is Element of bool (X,x)
bool (X,x) is non empty V56() V58() V59() set
x \ A is Element of bool x
bool x is non empty V56() V58() V59() set
(X,(x \ A)) is set
Y is set

Y . X is set
x is set
X is set
(X,x) is set
A is set
(X,A) is set
(X,x) \+\ (X,A) is set
(X,x) \ (X,A) is set
(X,A) \ (X,x) is set
((X,x) \ (X,A)) \/ ((X,A) \ (X,x)) is set
x \+\ A is set
x \ A is set
A \ x is set
(x \ A) \/ (A \ x) is set
(X,(x \+\ A)) is set
(X,x) \ (X,A) is Element of bool (X,x)
bool (X,x) is non empty V56() V58() V59() set
x \ A is Element of bool x
bool x is non empty V56() V58() V59() set
(X,(x \ A)) is set
(X,A) \ (X,x) is Element of bool (X,A)
bool (X,A) is non empty V56() V58() V59() set
A \ x is Element of bool A
bool A is non empty V56() V58() V59() set
(X,(A \ x)) is set
(X,(x \ A)) \/ (X,(A \ x)) is set
(x \ A) \/ (A \ x) is set
(X,((x \ A) \/ (A \ x))) is set
x is set

X is set
(X,x) is set

A is set
Y is set

Y . X is set

proj1 Y is set
Y is set
proj2 Y is set
Y is set
Y . Y is set

c7 . X is set

Y . X is set
Y . Y is set

c7 . X is set

Y is set
x is set

((X)) is set
proj2 (X) is set
union (proj2 (X)) is set
A is set
proj1 (X) is set
Y is set
(X) . Y is set
proj1 X is set
X . Y is set
{Y} is non empty trivial finite 1 -element set
[:(X . Y),{Y}:] is Relation-like set
x is set
x `2 is set
x `1 is set
[(x `1),(x `2)] is V35() set
{(x `1),(x `2)} is non empty finite set
{(x `1)} is non empty trivial finite 1 -element set
{{(x `1),(x `2)},{(x `1)}} is non empty with_non-empty_elements non empty-membered finite V52() set

((X)) is set
proj2 (X) is set
union (proj2 (X)) is set
proj1 X is set
X . (x `2) is set
A is set
proj1 (X) is set
Y is set
(X) . Y is set
X . Y is set
{Y} is non empty trivial finite 1 -element set
[:(X . Y),{Y}:] is Relation-like set
(X) . (x `2) is set
{(x `2)} is non empty trivial finite 1 -element set
[:(X . (x `2)),{(x `2)}:] is Relation-like set
proj1 (X) is set

proj1 x is set
proj1 X is set
proj1 (x) is set
proj1 (X) is set
A is set
(x) . A is set
x . A is set
{A} is non empty trivial finite 1 -element set
[:(x . A),{A}:] is Relation-like set
X . A is set
(X) . A is set

(x) is set
proj2 x is set
union () is set

(X) is set
proj2 X is set
union () is set
proj1 x is set
proj1 X is set
A is set
Y is set
Y is set
x . Y is set
X . Y is set
x is set
X is set

{X} is non empty trivial finite 1 -element set

bool [:x,{X}:] is non empty V56() V58() V59() set
((x --> X)) is Relation-like Function-like set
(((x --> X))) is set
proj2 ((x --> X)) is set
union (proj2 ((x --> X))) is set
[:X,x:] is Relation-like set
dom (x --> X) is Element of bool x
bool x is non empty V56() V58() V59() set
Y is set
Y is set
proj1 ((x --> X)) is set
Y is set
((x --> X)) . Y is set
(x --> X) . Y is set
{Y} is non empty trivial finite 1 -element set
[:((x --> X) . Y),{Y}:] is Relation-like set
Y is set
Y is set
[Y,Y] is V35() set
{Y,Y} is non empty finite set
{Y} is non empty trivial finite 1 -element set
{{Y,Y},{Y}} is non empty with_non-empty_elements non empty-membered finite V52() set
(x --> X) . Y is set
((x --> X)) . Y is set
{Y} is non empty trivial finite 1 -element set
[:((x --> X) . Y),{Y}:] is Relation-like set
proj1 ((x --> X)) is set

(x) is set
proj2 x is set
proj1 x is set
X is set
x . X is set
X is non empty set
A is set

proj1 A is set

proj1 Y is set
Y is set
x . Y is set
Y . Y is set
A . (x . Y) is set
proj1 x is set
the Element of (x) is Element of (x)

proj1 A is set
Y is set
x . Y is set

proj1 x is set
(x) is set

proj1 X is set
(X) is set
A is set

proj1 Y is set
Y is set
Y . Y is set
x . Y is set
X . Y is set

proj1 x is set
X is set
x . X is set

proj1 x is set

X is set
(x) . X is set

x . X is set

{X} is non empty trivial finite 1 -element set

((x)) is set
proj2 (x) is set
union (proj2 (x)) is set

(x) is set

proj1 x is set

((x)) is set
proj2 (x) is set
union (proj2 (x)) is set

proj1 X is set

((X)) is set
proj2 (X) is set
union (proj2 (X)) is set

A is set
Y is set
proj1 (x) is set
Y is set
(x) . Y is set
x . Y is set
X . Y is set
{Y} is non empty trivial finite 1 -element set
[:(x . Y),{Y}:] is Relation-like set
(X) . Y is set
[:(X . Y),{Y}:] is Relation-like set
proj1 (X) is set

proj2 x is set

(x) is set

proj1 x is set

proj1 X is set

(x) is set

(X) is set

((x)) is set
proj2 (x) is set
union (proj2 (x)) is set

((X)) is set
proj2 (X) is set
union (proj2 (X)) is set

(x) is set

proj2 X is set

(X) is set

proj1 x is set
proj1 X is set

proj1 A is set
proj2 A is set
Y is set

proj1 Y is set
the Element of (X) is Element of (X)

proj1 c7 is set

proj1 a is set
x is set
a . x is set
Y . x is set
x . x is set
X . x is set
c7 . x is set
A . a is set

proj1 (a | ()) is set
x is set
(a | ()) . x is set
a . x is set
Y . x is set

{x} is non empty trivial finite 1 -element set

bool [:{},{x}:] is non empty finite V52() V56() V58() V59() set

(()) is Relation-like Function-like set
((())) is set
proj2 (()) is set
union (proj2 (())) is set

bool {} is non empty finite V52() V56() V58() V59() set
proj1 (()) is set

{x} is non empty trivial finite 1 -element set

bool [:{},{x}:] is non empty finite V52() V56() V58() V59() set

(()) is set

X is set

{X} is non empty trivial finite 1 -element set

{x} is non empty trivial finite 1 -element set
[:{X},{x}:] is non empty Relation-like finite set
bool [:{X},{x}:] is non empty finite V52() V56() V58() V59() set

((X .--> x)) is Relation-like Function-like set
(((X .--> x))) is set
proj2 ((X .--> x)) is set
union (proj2 ((X .--> x))) is set

{[:x,{X}:]} is non empty trivial finite 1 -element set
[:{X},{[:x,{X}:]}:] is non empty Relation-like finite set
bool [:{X},{[:x,{X}:]}:] is non empty finite V52() V56() V58() V59() set
((X .--> [:x,{X}:])) is set
proj2 (X .--> [:x,{X}:]) is trivial finite set
union (proj2 (X .--> [:x,{X}:])) is set

X is set

{X} is non empty trivial finite 1 -element set

{x} is non empty trivial finite 1 -element set
[:{X},{x}:] is non empty Relation-like finite set
bool [:{X},{x}:] is non empty finite V52() V56() V58() V59() set

((X .--> x)) is set

Funcs ({X},x) is set

(x) is set
proj2 x is set
union () is set

(x) is Relation-like Function-like () set

((x)) is Relation-like Function-like set
(((x))) is set
proj2 ((x)) is set
union (proj2 ((x))) is set

proj1 x is set
X is set
x . X is set

Funcs ((card (x . X)),(x . X)) is set
A is set
Y is set
Y is set

proj2 Y is set

proj1 X is set
proj2 X is set
Y is set
A is non empty set
Y is set
X . Y is set
x . Y is set

proj1 Y is set
proj2 Y is set
Funcs ((card (x . Y)),(x . Y)) is set

proj1 Y is set
Y is set
Y `2 is set
X . (Y `2) is set
Y . (X . (Y `2)) is set
Y `1 is set
c7 is set
proj1 ((x)) is set
a is set
((x)) . a is set
proj1 (x) is set
(x) . a is set
{a} is non empty trivial finite 1 -element set
[:((x) . a),{a}:] is Relation-like set
x . (Y `2) is set

Funcs ((card (x . (Y `2))),(x . (Y `2))) is set

proj1 x is set
proj2 x is set
x . (Y `1) is set

proj1 Y is set
proj2 Y is set
c7 is set
a is set
x is set
x . x is set
X . x is set
Y . (X . x) is set

Funcs ((card (x . x)),(x . x)) is set

proj1 y is set
proj2 y is set

proj2 B is set
B is set
y . B is set
(x) . x is set
proj1 (x) is set
((x)) . x is set
{x} is non empty trivial finite 1 -element set
[:(),{x}:] is Relation-like set
proj1 ((x)) is set
[B,x] is V35() set
{B,x} is non empty finite set
{B} is non empty trivial finite 1 -element set
{{B,x},{B}} is non empty with_non-empty_elements non empty-membered finite V52() set
[B,x] `1 is set
[B,x] `2 is set
Y . [B,x] is set

y . B is set

(x) is set
proj2 x is set
union () is set

((x)) is set
proj2 (x) is set
union (proj2 (x)) is set

(x) is Relation-like Function-like () set

proj1 x is set

((x)) is set
proj2 (x) is set
union (proj2 (x)) is set

proj1 X is set

(X) is set

proj1 A is set
proj2 A is set
Y is set
A . Y is set
x . Y is set
X . Y is set

Y \ Y is Element of bool Y
bool Y is non empty V56() V58() V59() set
(A) is set
the Element of (A) is Element of (A)

proj1 Y is set
Y is set
Y `2 is set
Y `1 is set

proj1 c7 is set
a is set
x is set
c7 . x is set
Y . x is set

proj1 Y is set
c7 is set
Y . c7 is set
a is set
Y . a is set
c7 `2 is set
c7 `1 is set

proj1 x is set
a `2 is set
a `1 is set

proj1 y is set
x . (a `2) is set
[(c7 `1),(c7 `2)] is V35() set
{(c7 `1),(c7 `2)} is non empty finite set
{(c7 `1)} is non empty trivial finite 1 -element set
{{(c7 `1),(c7 `2)},{(c7 `1)}} is non empty with_non-empty_elements non empty-membered finite V52() set
B is set
y is set
[B,y] is V35() set
{B,y} is non empty finite set
{B} is non empty trivial finite 1 -element set
{{B,y},{B}} is non empty with_non-empty_elements non empty-membered finite V52() set
[(a `1),(a `2)] is V35() set
{(a `1),(a `2)} is non empty finite set
{(a `1)} is non empty trivial finite 1 -element set
{{(a `1),(a `2)},{(a `1)}} is non empty with_non-empty_elements non empty-membered finite V52() set
B is set
y is set
[B,y] is V35() set
{B,y} is non empty finite set
{B} is non empty trivial finite 1 -element set
{{B,y},{B}} is non empty with_non-empty_elements non empty-membered finite V52() set
y . (a `2) is set
x . (a `2) is set
Y . (a `2) is set
A . (a `2) is set
X . (a `2) is set
(X . (a `2)) \ (x . (a `2)) is Element of bool (X . (a `2))
bool (X . (a `2)) is non empty V56() V58() V59() set
x . (c7 `2) is set
y . (c7 `2) is set
proj2 Y is set
c7 is set
a is set
Y . a is set
a `2 is set
a `1 is set

proj1 x is set
y is set
X . y is set
x . y is set

x . y is set
Y . y is set
A . y is set
B \ y is Element of bool B
bool B is non empty V56() V58() V59() set
x . (a `2) is set

proj1 c7 is set
proj2 c7 is set

proj1 a is set
proj2 a is set
x is set
a . x is set
X . x is set
(x) . x is set
c7 .: ((x) . x) is set
(x,(c7 .: ((x) . x))) is set
(X . x) \ (x,(c7 .: ((x) . x))) is Element of bool (X . x)
bool (X . x) is non empty V56() V58() V59() set
x . x is set
card (x,(c7 .: ((x) . x))) is epsilon-transitive epsilon-connected ordinal cardinal set
card (c7 .: ((x) . x)) is epsilon-transitive epsilon-connected ordinal cardinal set

(a) is set
the Element of (a) is Element of (a)

proj1 y is set
B is set
a . B is set
X . B is set
(x) . B is set
c7 .: ((x) . B) is set
(B,(c7 .: ((x) . B))) is set
(X . B) \ (B,(c7 .: ((x) . B))) is Element of bool (X . B)
bool (X . B) is non empty V56() V58() V59() set
B is set
c7 . B is set
y is set
proj1 (x) is set
Z2 is set
(x) . Z2 is set
c7 .: y is set
y . Z2 is set
c7 .: ((x) . Z2) is set
(Z2,(c7 .: ((x) . Z2))) is set
X . Z2 is set
(X . Z2) \ (Z2,(c7 .: ((x) . Z2))) is Element of bool (X . Z2)
bool (X . Z2) is non empty V56() V58() V59() set
a . Z2 is set
F1() is set
x is set
F2(x) is set
X is set
A is set
Y is set
x is set

field X is set
proj1 X is set
proj2 X is set
() \/ () is set
x is set

x is set
union x is set

[:x,x:] is Relation-like set
X /\ [:x,x:] is Relation-like set
field (X |_2 x) is set
proj1 (X |_2 x) is set
proj2 (X |_2 x) is set
(proj1 (X |_2 x)) \/ (proj2 (X |_2 x)) is set

RelIncl (order_type_of (X |_2 x)) is Relation-like set

field (RelIncl (order_type_of (X |_2 x))) is set
proj1 (RelIncl (order_type_of (X |_2 x))) is set
proj2 (RelIncl (order_type_of (X |_2 x))) is set
(proj1 (RelIncl (order_type_of (X |_2 x)))) \/ (proj2 (RelIncl (order_type_of (X |_2 x)))) is set
proj1 A is set
proj2 A is set
Y is set
A .: Y is set
Y is set
union Y is set
Y is set
c7 is set
a is set
A . a is set

A . y is set

A . y is set
A . B is set
Y is set
the Element of Y is Element of Y
a is set
A . a is set

A . y is set
B is set
y is set
Z2 is set
A . Z2 is set

X is set
union X is set

A is set
union A is set
Y is set
Y is set

field Y is set
proj1 Y is set
proj2 Y is set
() \/ () is set
Y is set
c7 is set
[Y,c7] is V35() set
{Y,c7} is non empty finite set
{Y} is non empty trivial finite 1 -element set
{{Y,c7},{Y}} is non empty with_non-empty_elements non empty-membered finite V52() set
a is set
[a,Y] is V35() set
{a,Y} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,Y},{a}} is non empty with_non-empty_elements non empty-membered finite V52() set
Y is set
[Y,Y] is V35() set
{Y,Y} is non empty finite set
{Y} is non empty trivial finite 1 -element set
{{Y,Y},{Y}} is non empty with_non-empty_elements non empty-membered finite V52() set
c7 is set
Y is set
[Y,Y] is V35() set
{Y,Y} is non empty finite set
{Y} is non empty trivial finite 1 -element set
{{Y,Y},{Y}} is non empty with_non-empty_elements non empty-membered finite V52() set
c7 is set
Y is set
c7 is set
[Y,c7] is V35() set
{Y,c7} is non empty finite set
{Y} is non empty trivial finite 1 -element set
{{Y,c7},{Y}} is non empty with_non-empty_elements non empty-membered finite V52() set
a is set
[c7,a] is V35() set
{c7,a} is non empty finite set
{c7} is non empty trivial finite 1 -element set
{{c7,a},{c7}} is non empty with_non-empty_elements non empty-membered finite V52() set
[Y,a] is V35() set
{Y,a} is non empty finite set
{{Y,a},{Y}} is non empty with_non-empty_elements non empty-membered finite V52() set
x is set
y is set
x is set
x is set
x is set
x is set
y is set
B is set
y is set
Y is set
c7 is set
[Y,c7] is V35() set
{Y,c7} is non empty finite set
{Y} is non empty trivial finite 1 -element set
{{Y,c7},{Y}} is non empty with_non-empty_elements non empty-membered finite V52() set
[c7,Y] is V35() set
{c7,Y} is non empty finite set
{c7} is non empty trivial finite 1 -element set
{{c7,Y},{c7}} is non empty with_non-empty_elements non empty-membered finite V52() set
a is set
a is set
a is set
x is set
a is set
x is set
Y is set
c7 is set
[Y,c7] is V35() set
{Y,c7} is non empty finite set
{Y} is non empty trivial finite 1 -element set
{{Y,c7},{Y}} is non empty with_non-empty_elements non empty-membered finite V52() set
[c7,Y] is V35() set
{c7,Y} is non empty finite set
{c7} is non empty trivial finite 1 -element set
{{c7,Y},{c7}} is non empty with_non-empty_elements non empty-membered finite V52() set
a is set
a is set
Y is set
c7 is set
a is set
the Element of Y is Element of Y
x is set
x /\ Y is set
y is set
y /\ Y is set
B is set
Y -Seg B is set
Coim (Y,B) is set
{B} is non empty trivial finite 1 -element set
Y " {B} is set
(Coim (Y,B)) \ {B} is Element of bool (Coim (Y,B))
bool (Coim (Y,B)) is non empty V56() V58() V59() set
(Y -Seg B) /\ Y is set
the Element of (Y -Seg B) /\ Y is Element of (Y -Seg B) /\ Y
[ the Element of (Y -Seg B) /\ Y,B] is V35() set
{ the Element of (Y -Seg B) /\ Y,B} is non empty finite set
{ the Element of (Y -Seg B) /\ Y} is non empty trivial finite 1 -element set
{{ the Element of (Y -Seg B) /\ Y,B},{ the Element of (Y -Seg B) /\ Y}} is non empty with_non-empty_elements non empty-membered finite V52() set
Z2 is set
Z2 /\ Y is set
[B, the Element of (Y -Seg B) /\ Y] is V35() set
{B, the Element of (Y -Seg B) /\ Y} is non empty finite set
{{B, the Element of (Y -Seg B) /\ Y},{B}} is non empty with_non-empty_elements non empty-membered finite V52() set

field () is set
proj1 () is set
proj2 () is set
(proj1 ()) \/ (proj2 ()) is set
proj1 Y is set
proj2 Y is set
c7 is set
a is set
Y -Seg a is set
Coim (Y,a) is set
{a} is non empty trivial finite 1 -element set
Y " {a} is set
(Coim (Y,a)) \ {a} is Element of bool (Coim (Y,a))
bool (Coim (Y,a)) is non empty V56() V58() V59() set
x is set
[x,a] is V35() set
{x,a} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,a},{x}} is non empty with_non-empty_elements non empty-membered finite V52() set
y is set

Y . c7 is set
Y -Seg (Y . c7) is set
Coim (Y,(Y . c7)) is set
{(Y . c7)} is non empty trivial finite 1 -element set
Y " {(Y . c7)} is set
(Coim (Y,(Y . c7))) \ {(Y . c7)} is Element of bool (Coim (Y,(Y . c7)))
bool (Coim (Y,(Y . c7))) is non empty V56() V58() V59() set

proj1 a is set
proj2 a is set
x is set
y is set
a . y is set

[B,c7] is V35() set
{B,c7} is non empty finite set
{B} is non empty trivial finite 1 -element set
{{B,c7},{B}} is non empty with_non-empty_elements non empty-membered finite V52() set
Y . B is set
[x,(Y . c7)] is V35() set
{x,(Y . c7)} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,(Y . c7)},{x}} is non empty with_non-empty_elements non empty-membered finite V52() set
x is set
[x,(Y . c7)] is V35() set
{x,(Y . c7)} is non empty finite set
{x} is non empty trivial finite 1 -element set
{{x,(Y . c7)},{x}} is non empty with_non-empty_elements non empty-membered finite V52() set
y is set
Y . y is set

[B,c7] is V35() set
{B,c7} is non empty finite set
{B} is non empty trivial finite 1 -element set
{{B,c7},{B}} is non empty with_non-empty_elements non empty-membered finite V52() set

Y . c7 is set
x is set
Y -Seg (Y . c7) is set
Coim (Y,(Y . c7)) is set
{(Y . c7)} is non empty trivial finite 1 -element set
Y " {(Y . c7)} is set
(Coim (Y,(Y . c7))) \ {(Y . c7)} is Element of bool (Coim (Y,(Y . c7)))
bool (Coim (Y,(Y . c7))) is non empty V56() V58() V59() set

(x) is set
A is set
proj1 x is set

proj1 Y is set
x is set

[:x,X:] is Relation-like set
bool [:x,X:] is non empty V56() V58() V59() set

rng A is Element of bool X
bool X is non empty V56() V58() V59() set

(x) is functional set

x is set
X is set
A is set
{A} is non empty trivial finite 1 -element set
Y is set
{Y} is non empty trivial finite 1 -element set
(x,X) --> ({A},{Y}) is Relation-like Function-like finite set
(((x,X) --> ({A},{Y}))) is functional set
(x,X) --> (A,Y) is Relation-like Function-like finite set
{((x,X) --> (A,Y))} is non empty trivial functional finite V52() 1 -element set
proj1 ((x,X) --> ({A},{Y})) is finite set
{x,X} is non empty finite set
c7 is set

x is set
a . x is set
((x,X) --> ({A},{Y})) . x is set
a . x is set
((x,X) --> ({A},{Y})) . x is set
a . X is set
((x,X) --> ({A},{Y})) . X is set

proj1 a is set
a . x is set
((x,X) --> ({A},{Y})) . x is set
a . X is set
((x,X) --> ({A},{Y})) . X is set
x is set

(X) is functional set

proj1 x is set
proj2 x is set
union () is set
PFuncs ((),(union ())) is set
X is set
A is set

proj1 Y is set
proj2 Y is set
Y is set
Y is set
Y . Y is set
x . Y is set
X is set
A is set

(x) is set
proj1 x is set
proj2 x is set
union () is set
PFuncs ((),(union ())) is set
X is set
[:(),(union ()):] is Relation-like set
bool [:(),(union ()):] is non empty V56() V58() V59() set
A is set

x . A is set
A is set

proj1 Y is set
Y is set
A is non empty functional set

proj1 Y is set
proj2 Y is set
Y is set
c7 is set
Y . c7 is set
x . c7 is set

proj1 x is set

(X) is non empty functional set
proj1 X is set
A is set
x . A is set
X . A is set

proj1 Y is set

(x) is non empty functional set
proj1 x is set
X is set

x . X is set

(x) is non empty functional set

(x) is functional set
(x) is non empty functional set
X is set
proj1 x is set

proj1 A is set
x is set

(X) is non empty functional set
proj1 X is set
proj2 X is set
union () is set
[:(),(union ()):] is Relation-like set
bool [:(),(union ()):] is non empty V56() V58() V59() set

proj1 A is set
proj2 A is set
Y is set
Y is set
A . Y is set
X . Y is set

(X) is functional set
(X) is non empty functional set

proj1 x is set
proj1 X is set
proj1 A is set
() \/ () is set
proj1 (x +* A) is set
Y is set
() \ () is Element of bool ()
bool () is non empty V56() V58() V59() set
(() \ ()) \/ () is set
(x +* A) . Y is set
x . Y is set
(x +* A) . Y is set
A . Y is set
(x +* A) . Y is set
x . Y is set
A . Y is set
(x +* A) . Y is set
x . Y is set
A . Y is set
X . Y is set

(x) is functional set
(x) is non empty functional set

the Relation-like Function-like Element of (x) is Relation-like Function-like Element of (x)

proj1 A is set
proj1 x is set
proj1 X is set
Y is set
X . Y is set
A . Y is set
x . Y is set

(x) is non empty functional set
proj1 x is set
proj2 x is set
union () is set
PFuncs ((),(union ())) is set
X is set
[:(),(union ()):] is Relation-like set
bool [:(),(union ()):] is non empty V56() V58() V59() set

(x) is non empty functional set

(X) is non empty functional set
proj1 x is set
proj1 X is set
A is set

proj1 Y is set
Y is set
x . Y is set
X . Y is set
Y . Y is set
({}) is non empty functional set
PFuncs ({},{}) is set
x is set
x is set
X is set
PFuncs (x,X) is set

{X} is non empty trivial finite 1 -element set

bool [:x,{X}:] is non empty V56() V58() V59() set
((x --> X)) is non empty functional set

bool [:{},{X}:] is non empty finite V52() V56() V58() V59() set
rng (x --> X) is trivial finite Element of bool {X}
bool {X} is non empty finite V52() V56() V58() V59() set
dom (x --> X) is Element of bool x
bool x is non empty V56() V58() V59() set
union (rng (x --> X)) is set
A is set

proj1 Y is set
proj2 Y is set
Y is set
Y . Y is set
(x --> X) . Y is set
x is non empty set
X is non empty set
[:x,X:] is non empty Relation-like set
bool [:x,X:] is non empty V56() V58() V59() set

(A) is non empty functional set
{ b1 where b1 is Element of x : not A . b1 = {} } is set
A | { b1 where b1 is Element of x : not A . b1 = {} } is Relation-like x -defined { b1 where b1 is Element of x : not A . b1 = {} } -defined x -defined X -valued Function-like Element of bool [:x,X:]
((A | { b1 where b1 is Element of x : not A . b1 = {} } )) is non empty functional set
Y is set
dom A is Element of bool x
bool x is non empty V56() V58() V59() set

proj1 Y is set
c7 is set
a is Element of x
A . a is Element of X
c7 is set
(dom A) /\ { b1 where b1 is Element of x : not A . b1 = {} } is Element of bool x
dom (A | { b1 where b1 is Element of x : not A . b1 = {} } ) is Element of bool x
c7 is set
c7 is set
Y . c7 is set
A . c7 is set
(A | { b1 where b1 is Element of x : not A . b1 = {} } ) . c7 is set
x is set
X is set

{x} is non empty trivial finite 1 -element set

{X} is non empty trivial finite 1 -element set
[:{x},{X}:] is non empty Relation-like finite set
bool [:{x},{X}:] is non empty finite V52() V56() V58() V59() set

proj1 A is set
A . x is set
(A) is non empty functional set
dom (x .--> X) is trivial finite Element of bool {x}
bool {x} is non empty finite V52() V56() V58() V59() set
Y is set
(x .--> X) . Y is set
A . Y is set

(x) is non empty functional set
proj1 x is set
X is set
x . X is set
the Element of x . X is Element of x . X

{X} is non empty trivial finite 1 -element set
{X} --> the Element of x . X is non empty Relation-like {X} -defined { the Element of x . X} -valued Function-like constant total quasi_total finite Element of bool [:{X},{ the Element of x . X}:]
{ the Element of x . X} is non empty trivial finite 1 -element set
[:{X},{ the Element of x . X}:] is non empty Relation-like finite set
bool [:{X},{ the Element of x . X}:] is non empty finite V52() V56() V58() V59() set
X is set

proj1 A is set
the Element of proj1 A is Element of proj1 A
x . the Element of proj1 A is set

(x) is non empty functional set
X is set
union X is set

proj1 A is set
proj1 x is set
Y is set
Y is set
[Y,Y] is V35() set
{Y,Y} is non empty finite set
{Y} is non empty trivial finite 1 -element set
{{Y,Y},{Y}} is non empty with_non-empty_elements non empty-membered finite V52() set
Y is set

proj1 c7 is set
Y is set
Y is set
[Y,Y] is V35() set
{Y,Y} is non empty finite set
{Y} is non empty trivial finite 1 -element set
{{Y,Y},{Y}} is non empty with_non-empty_elements non empty-membered finite V52() set
Y is set

proj1 c7 is set
c7 . Y is set
A . Y is set
x . Y is set

(A) is non empty functional set
{x,X} is non empty functional finite set

union {x,X} is set
x is set

(A) is non empty functional set

proj1 Y is set
proj1 X is set
proj1 A is set
Y is set
X . Y is set
A . Y is set
Y . Y is set

(X) is non empty functional set
A is set

(X) is non empty functional set
A is set

((X | A)) is non empty functional set
proj1 (x | A) is set
proj1 x is set
() /\ A is set
proj1 (X | A) is set
proj1 X is set
() /\ A is set
Y is set
(x | A) . Y is set
x . Y is set
(X | A) . Y is set
X . Y is set

(X) is non empty functional set

((X +* A)) is non empty functional set
(A) is non empty functional set
proj1 X is set
proj1 A is set
() \ () is Element of bool ()
bool () is non empty V56() V58() V59() set
x | (() \ ()) is Relation-like Function-like set

(x | (() \ ())) +* (x | ()) is Relation-like Function-like set
(X +* A) | (() \ ()) is Relation-like Function-like set
(((X +* A) | (() \ ()))) is non empty functional set
(X +* A) | () is Relation-like Function-like set
proj1 x is set
proj1 (X +* A) is set
() \/ () is set
(() \ ()) \/ () is set

proj1 x is set
(x) is non empty functional set

(X) is non empty functional set

((X +* x)) is non empty functional set

proj1 A is set

proj1 Y is set
() \ () is Element of bool ()
bool () is non empty V56() V58() V59() set

proj1 X is set
() \/ () is set
() \/ () is set
proj1 (A +* Y) is set
proj1 (X +* x) is set
Y is set
(A +* Y) . Y is set
(X +* x) . Y is set
(() \ ()) \/ () is set
Y . Y is set
x . Y is set
A . Y is set
X . Y is set
x . Y is set
X . Y is set
x . Y is set
X . Y is set