:: CARD_3 semantic presentation

omega is non empty non trivial non empty-membered epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set

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

{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V42() finite finite-yielding V52() cardinal {} -element set

the empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V42() finite finite-yielding V52() cardinal {} -element set is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V42() finite finite-yielding V52() cardinal {} -element set

1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal Element of omega

union {} is epsilon-transitive epsilon-connected ordinal natural finite cardinal set

proj1 {} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V42() finite finite-yielding V52() cardinal {} -element set

proj2 {} is empty trivial with_non-empty_elements Relation-like non-empty empty-yielding Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V42() finite finite-yielding V52() cardinal {} -element set

card {} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V42() finite finite-yielding V52() cardinal {} -element set

card omega is non empty non trivial non empty-membered epsilon-transitive epsilon-connected ordinal non finite cardinal set

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

x is Relation-like Function-like set

X is set

proj1 x is set

x . X is set

x is Relation-like Function-like () set

X is set

x | X is Relation-like Function-like set

A is set

proj1 (x | X) is set

(x | X) . A is set

x . A is set

proj1 x is set

(proj1 x) /\ X is set

x is set

X is epsilon-transitive epsilon-connected ordinal cardinal set

x --> X is Relation-like x -defined {X} -valued Function-like constant total quasi_total Element of bool [:x,{X}:]

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

[:x,{X}:] is Relation-like 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 epsilon-transitive epsilon-connected ordinal cardinal set

x .--> X is trivial Relation-like {x} -defined Function-like one-to-one constant finite set

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

{x} --> X is non empty Relation-like {x} -defined {X} -valued Function-like constant total quasi_total finite () Element of bool [:{x},{X}:]

{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

F

x is Relation-like Function-like set

proj1 x is set

X is set

x . X is set

F

X is Relation-like Function-like () set

proj1 X is set

A is set

X . A is set

F

x is Relation-like Function-like set

proj1 x is set

X is Relation-like Function-like () set

proj1 X is set

A is Relation-like Function-like () set

proj1 A is set

Y is set

X . Y is set

x . Y is set

card (x . Y) is epsilon-transitive epsilon-connected ordinal cardinal set

A . Y is set

X is Relation-like Function-like set

proj1 X is set

A is Relation-like Function-like 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 (proj2 x) is set

Funcs ((proj1 x),(union (proj2 x))) is set

X is set

A is set

Y is Relation-like Function-like 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 Relation-like Function-like () set

X is set

proj1 x is set

x . X is set

A is epsilon-transitive epsilon-connected ordinal cardinal set

card A is epsilon-transitive epsilon-connected ordinal cardinal set

card (x . X) is epsilon-transitive epsilon-connected ordinal cardinal set

x is set

X is set

x --> X is Relation-like x -defined {X} -valued Function-like constant total quasi_total Element of bool [:x,{X}:]

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

[:x,{X}:] is Relation-like set

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

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

card X is epsilon-transitive epsilon-connected ordinal cardinal set

x --> (card X) is Relation-like x -defined {(card X)} -valued Function-like constant total quasi_total () Element of bool [:x,{(card X)}:]

{(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

card ((x --> X) . A) is epsilon-transitive epsilon-connected ordinal cardinal set

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

({}) is Relation-like Function-like set

proj1 ({}) is set

x is set

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

X is set

x .--> X is trivial Relation-like {x} -defined Function-like one-to-one constant finite set

{x} --> X is non empty Relation-like {x} -defined {X} -valued Function-like constant total quasi_total finite Element of bool [:{x},{X}:]

{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 Relation-like set

x .--> [:X,{x}:] is trivial Relation-like {x} -defined Function-like one-to-one constant finite set

{x} --> [:X,{x}:] is non empty Relation-like {x} -defined {[:X,{x}:]} -valued Function-like constant total quasi_total finite Element of bool [:{x},{[:X,{x}:]}:]

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

A is Relation-like Function-like set

proj1 A is set

(A) is Relation-like Function-like 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 --> X is Relation-like x -defined {X} -valued Function-like constant total quasi_total Element of bool [:x,{X}:]

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

[:x,{X}:] is Relation-like 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 --> X is Relation-like x -defined {X} -valued Function-like constant total quasi_total Element of bool [:x,{X}:]

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

[:x,{X}:] is Relation-like 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 .--> X is trivial Relation-like {x} -defined Function-like one-to-one constant finite set

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

{x} --> X is non empty Relation-like {x} -defined {X} -valued Function-like constant total quasi_total finite Element of bool [:{x},{X}:]

{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

x is Relation-like Function-like set

proj1 x is set

X is Relation-like Function-like set

(X) is set

proj1 X is set

A is set

x . A is set

X . A is set

Y is Relation-like Function-like set

proj1 Y is set

({}) is set

x is set

X is Relation-like Function-like set

proj1 X is set

x is set

X is set

{} . X is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V42() finite finite-yielding V52() cardinal {} -element () set

x is set

X is set

Funcs (x,X) is set

x --> X is Relation-like x -defined {X} -valued Function-like constant total quasi_total Element of bool [:x,{X}:]

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

[:x,{X}:] is Relation-like 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

Y is Relation-like Function-like set

proj1 Y is set

proj2 Y is set

Y is set

(x --> X) . Y is set

Y . Y is set

Y is set

Y is Relation-like Function-like set

proj1 Y is set

proj2 Y is set

Y is set

c

Y . c

(x --> X) . c

x is set

X is set

A is set

Y is set

Y is Relation-like Function-like set

Y . x is set

Y is Relation-like Function-like set

proj1 Y is set

proj2 Y is set

Y is set

Y is set

Y . Y is set

c

c

Y is Relation-like Function-like set

Y . x is set

Y . Y is set

c

c

A is set

Y is set

x is set

X is Relation-like Function-like set

proj1 X is set

(X) is set

(x,(X)) is set

X . x is set

A is set

Y is Relation-like Function-like set

Y . x is set

the Element of (X) is Element of (X)

Y is Relation-like Function-like set

proj1 Y is set

Y is set

Y is Relation-like Function-like set

proj1 Y is set

c

Y . c

Y . c

X . c

Y . x is set

x is set

(x,{}) is set

the Element of (x,{}) is Element of (x,{})

A is Relation-like Function-like set

A . x is set

x is set

X is Relation-like Function-like set

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

(x,{X}) is set

X . x is set

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

A is set

Y is Relation-like Function-like set

Y . x is set

A is set

x is set

X is Relation-like Function-like set

X . x is set

A is Relation-like Function-like 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 is Relation-like Function-like 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 is Relation-like Function-like set

Y . A is set

Y is set

Y is Relation-like Function-like set

Y . A is set

Y is Relation-like Function-like 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 is Relation-like Function-like 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 is Relation-like Function-like 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

card x is epsilon-transitive epsilon-connected ordinal cardinal set

X is set

(X,x) is set

card (X,x) is epsilon-transitive epsilon-connected ordinal cardinal set

A is set

Y is set

Y is Relation-like Function-like set

Y . X is set

Y is Relation-like Function-like set

proj1 Y is set

Y is set

proj2 Y is set

Y is set

Y . Y is set

c

c

Y is Relation-like Function-like set

Y . X is set

Y . Y is set

c

c

card A is epsilon-transitive epsilon-connected ordinal cardinal set

Y is set

x 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

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 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 . (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

x is Relation-like Function-like set

(x) is Relation-like Function-like set

X is Relation-like Function-like set

(X) is Relation-like Function-like 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 Relation-like Function-like set

(x) is set

proj2 x is set

union (proj2 x) is set

X is Relation-like Function-like set

(X) is set

proj2 X is set

union (proj2 X) 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 --> X is Relation-like x -defined {X} -valued Function-like constant total quasi_total Element of bool [:x,{X}:]

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

[:x,{X}:] is Relation-like 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 Relation-like Function-like 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

A is Relation-like Function-like set

proj1 A is set

Y is Relation-like Function-like 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)

A is Relation-like Function-like set

proj1 A is set

Y is set

x . Y is set

x is Relation-like Function-like set

proj1 x is set

(x) is set

X is Relation-like Function-like set

proj1 X is set

(X) is set

A is set

Y is Relation-like Function-like set

proj1 Y is set

Y is set

Y . Y is set

x . Y is set

X . Y is set

x is Relation-like Function-like () set

proj1 x is set

X is set

x . X is set

card (x . X) is epsilon-transitive epsilon-connected ordinal cardinal set

A is epsilon-transitive epsilon-connected ordinal cardinal set

card A is epsilon-transitive epsilon-connected ordinal cardinal set

x is Relation-like Function-like () set

proj1 x is set

(x) is Relation-like Function-like set

X is set

(x) . X is set

card ((x) . X) is epsilon-transitive epsilon-connected ordinal cardinal set

x . X is set

A is epsilon-transitive epsilon-connected ordinal cardinal set

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

[:A,{X}:] is Relation-like set

card [:A,{X}:] is epsilon-transitive epsilon-connected ordinal cardinal 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

card ((x)) is epsilon-transitive epsilon-connected ordinal cardinal set

(x) is set

card (x) is epsilon-transitive epsilon-connected ordinal cardinal set

x is Relation-like Function-like () set

proj1 x is set

(x) is epsilon-transitive epsilon-connected ordinal cardinal set

(x) is Relation-like Function-like set

((x)) is set

proj2 (x) is set

union (proj2 (x)) is set

card ((x)) is epsilon-transitive epsilon-connected ordinal cardinal set

X is Relation-like Function-like () set

proj1 X is set

(X) is epsilon-transitive epsilon-connected ordinal cardinal set

(X) is Relation-like Function-like set

((X)) is set

proj2 (X) is set

union (proj2 (X)) is set

card ((X)) is epsilon-transitive epsilon-connected ordinal cardinal 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

x is Relation-like Function-like () set

proj2 x is set

(x) is epsilon-transitive epsilon-connected ordinal cardinal set

(x) is set

card (x) is epsilon-transitive epsilon-connected ordinal cardinal set

x is Relation-like Function-like () set

proj1 x is set

X is Relation-like Function-like () set

proj1 X is set

(x) is epsilon-transitive epsilon-connected ordinal cardinal set

(x) is set

card (x) is epsilon-transitive epsilon-connected ordinal cardinal set

(X) is epsilon-transitive epsilon-connected ordinal cardinal set

(X) is set

card (X) is epsilon-transitive epsilon-connected ordinal cardinal set

x is Relation-like Function-like () set

(x) is epsilon-transitive epsilon-connected ordinal cardinal set

(x) is Relation-like Function-like set

((x)) is set

proj2 (x) is set

union (proj2 (x)) is set

card ((x)) is epsilon-transitive epsilon-connected ordinal cardinal set

X is Relation-like Function-like () set

(X) is epsilon-transitive epsilon-connected ordinal cardinal set

(X) is Relation-like Function-like set

((X)) is set

proj2 (X) is set

union (proj2 (X)) is set

card ((X)) is epsilon-transitive epsilon-connected ordinal cardinal set

x is Relation-like Function-like () set

(x) is epsilon-transitive epsilon-connected ordinal cardinal set

(x) is set

card (x) is epsilon-transitive epsilon-connected ordinal cardinal set

X is Relation-like Function-like () set

proj2 X is set

(X) is epsilon-transitive epsilon-connected ordinal cardinal set

(X) is set

card (X) is epsilon-transitive epsilon-connected ordinal cardinal set

proj1 x is set

proj1 X is set

A is Relation-like Function-like set

proj1 A is set

proj2 A is set

Y is set

Y is Relation-like Function-like set

proj1 Y is set

the Element of (X) is Element of (X)

c

proj1 c

a is Relation-like Function-like set

proj1 a is set

x is set

a . x is set

Y . x is set

x . x is set

X . x is set

c

A . a is set

a | (proj1 x) is Relation-like Function-like set

proj1 (a | (proj1 x)) is set

x is set

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

a . x is set

Y . x is set

x is epsilon-transitive epsilon-connected ordinal cardinal set

{} --> x is empty Relation-like non-empty empty-yielding {} -defined {x} -valued Function-like one-to-one constant functional total epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural quasi_total Function-yielding V42() finite finite-yielding V52() cardinal {} -element () Element of bool [:{},{x}:]

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

[:{},{x}:] is Relation-like finite set

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

(({} --> x)) is epsilon-transitive epsilon-connected ordinal cardinal set

(({} --> x)) is Relation-like Function-like set

((({} --> x))) is set

proj2 (({} --> x)) is set

union (proj2 (({} --> x))) is set

card ((({} --> x))) is epsilon-transitive epsilon-connected ordinal cardinal set

dom ({} --> x) is empty non proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V42() finite finite-yielding V52() cardinal {} -element () Element of bool {}

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

proj1 (({} --> x)) is set

x is epsilon-transitive epsilon-connected ordinal cardinal set

{} --> x is empty Relation-like non-empty empty-yielding {} -defined {x} -valued Function-like one-to-one constant functional total epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural quasi_total Function-yielding V42() finite finite-yielding V52() cardinal {} -element () Element of bool [:{},{x}:]

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

[:{},{x}:] is Relation-like finite set

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

(({} --> x)) is epsilon-transitive epsilon-connected ordinal cardinal set

(({} --> x)) is set

card (({} --> x)) is epsilon-transitive epsilon-connected ordinal cardinal set

x is epsilon-transitive epsilon-connected ordinal cardinal set

X is set

X .--> x is trivial Relation-like {X} -defined Function-like one-to-one constant finite () set

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

{X} --> x is non empty Relation-like {X} -defined {x} -valued Function-like constant total quasi_total finite () Element of bool [:{X},{x}:]

{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 epsilon-transitive epsilon-connected ordinal cardinal set

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

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

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

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

card (((X .--> x))) is epsilon-transitive epsilon-connected ordinal cardinal set

[:x,{X}:] is Relation-like set

X .--> [:x,{X}:] is trivial Relation-like {X} -defined Function-like one-to-one constant finite set

{X} --> [:x,{X}:] is non empty Relation-like {X} -defined {[:x,{X}:]} -valued Function-like constant total quasi_total finite Element of bool [:{X},{[:x,{X}:]}:]

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

card ((X .--> [:x,{X}:])) is epsilon-transitive epsilon-connected ordinal cardinal set

card [:x,{X}:] is epsilon-transitive epsilon-connected ordinal cardinal set

card x is epsilon-transitive epsilon-connected ordinal cardinal set

x is epsilon-transitive epsilon-connected ordinal cardinal set

X is set

X .--> x is trivial Relation-like {X} -defined Function-like one-to-one constant finite () set

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

{X} --> x is non empty Relation-like {X} -defined {x} -valued Function-like constant total quasi_total finite () Element of bool [:{X},{x}:]

{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 epsilon-transitive epsilon-connected ordinal cardinal set

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

card ((X .--> x)) is epsilon-transitive epsilon-connected ordinal cardinal set

Funcs ({X},x) is set

card (Funcs ({X},x)) is epsilon-transitive epsilon-connected ordinal cardinal set

card x is epsilon-transitive epsilon-connected ordinal cardinal set

x is Relation-like Function-like set

(x) is set

proj2 x is set

union (proj2 x) is set

card (x) is epsilon-transitive epsilon-connected ordinal cardinal set

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

((x)) is epsilon-transitive epsilon-connected ordinal cardinal set

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

(((x))) is set

proj2 ((x)) is set

union (proj2 ((x))) is set

card (((x))) is epsilon-transitive epsilon-connected ordinal cardinal set

proj1 x is set

X is set

x . X is set

card (x . X) is epsilon-transitive epsilon-connected ordinal cardinal set

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

A is set

Y is set

Y is set

Y is Relation-like Function-like set

proj2 Y is set

X is Relation-like Function-like 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

card (x . Y) is epsilon-transitive epsilon-connected ordinal cardinal set

Y is Relation-like Function-like set

proj1 Y is set

proj2 Y is set

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

Y is Relation-like Function-like 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

c

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

card (x . (Y `2)) is epsilon-transitive epsilon-connected ordinal cardinal set

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

x is Relation-like Function-like set

proj1 x is set

proj2 x is set

x . (Y `1) is set

Y is Relation-like Function-like set

proj1 Y is set

proj2 Y is set

c

a is set

x is set

x . x is set

X . x is set

Y . (X . x) is set

card (x . x) is epsilon-transitive epsilon-connected ordinal cardinal set

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

y is Relation-like Function-like set

proj1 y is set

proj2 y is set

B is Relation-like Function-like 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

[:(proj1 y),{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 is Relation-like Function-like set

y . B is set

x is Relation-like Function-like () set

(x) is set

proj2 x is set

union (proj2 x) is set

card (x) is epsilon-transitive epsilon-connected ordinal cardinal set

(x) is epsilon-transitive epsilon-connected ordinal cardinal set

(x) is Relation-like Function-like set

((x)) is set

proj2 (x) is set

union (proj2 (x)) is set

card ((x)) is epsilon-transitive epsilon-connected ordinal cardinal set

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

x is Relation-like Function-like () set

proj1 x is set

(x) is epsilon-transitive epsilon-connected ordinal cardinal set

(x) is Relation-like Function-like set

((x)) is set

proj2 (x) is set

union (proj2 (x)) is set

card ((x)) is epsilon-transitive epsilon-connected ordinal cardinal set

X is Relation-like Function-like () set

proj1 X is set

(X) is epsilon-transitive epsilon-connected ordinal cardinal set

(X) is set

card (X) is epsilon-transitive epsilon-connected ordinal cardinal set

A is Relation-like Function-like 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 is epsilon-transitive epsilon-connected ordinal cardinal set

Y is epsilon-transitive epsilon-connected ordinal cardinal 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)

Y is Relation-like Function-like set

proj1 Y is set

Y is set

Y `2 is set

Y `1 is set

c

proj1 c

a is set

x is set

c

Y . x is set

Y is Relation-like Function-like set

proj1 Y is set

c

Y . c

a is set

Y . a is set

c

c

x is Relation-like Function-like set

proj1 x is set

a `2 is set

a `1 is set

y is Relation-like Function-like set

proj1 y is set

x . (a `2) is set

[(c

{(c

{(c

{{(c

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 . (c

y . (c

proj2 Y is set

c

a is set

Y . a is set

a `2 is set

a `1 is set

x is Relation-like Function-like set

proj1 x is set

y is set

X . y is set

x . y is set

y is epsilon-transitive epsilon-connected ordinal cardinal set

B is epsilon-transitive epsilon-connected ordinal cardinal 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

c

proj1 c

proj2 c

a is Relation-like Function-like set

proj1 a is set

proj2 a is set

x is set

a . x is set

X . x is set

(x) . x is set

c

(x,(c

(X . x) \ (x,(c

bool (X . x) is non empty V56() V58() V59() set

x . x is set

card (x,(c

card (c

card ((x) . x) is epsilon-transitive epsilon-connected ordinal cardinal set

y is epsilon-transitive epsilon-connected ordinal cardinal set

B is epsilon-transitive epsilon-connected ordinal cardinal set

card B is epsilon-transitive epsilon-connected ordinal cardinal set

(a) is set

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

y is Relation-like Function-like set

proj1 y is set

B is set

a . B is set

X . B is set

(x) . B is set

c

(B,(c

(X . B) \ (B,(c

bool (X . B) is non empty V56() V58() V59() set

B is set

c

y is set

proj1 (x) is set

Z2 is set

(x) . Z2 is set

c

y . Z2 is set

c

(Z2,(c

X . Z2 is set

(X . Z2) \ (Z2,(c

bool (X . Z2) is non empty V56() V58() V59() set

a . Z2 is set

F

x is set

F

X is set

A is set

Y is set

x is set

X is Relation-like set

field X is set

proj1 X is set

proj2 X is set

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

x is set

card x is epsilon-transitive epsilon-connected ordinal cardinal set

X is epsilon-transitive epsilon-connected ordinal natural finite cardinal set

card X is epsilon-transitive epsilon-connected ordinal natural finite cardinal Element of omega

x is epsilon-transitive epsilon-connected ordinal set

card x is epsilon-transitive epsilon-connected ordinal cardinal set

X is epsilon-transitive epsilon-connected ordinal set

card X is epsilon-transitive epsilon-connected ordinal cardinal set

x is epsilon-transitive epsilon-connected ordinal set

card x is epsilon-transitive epsilon-connected ordinal cardinal set

X is epsilon-transitive epsilon-connected ordinal cardinal set

card X is epsilon-transitive epsilon-connected ordinal cardinal set

x is set

union x is set

X is Relation-like set

X |_2 x is Relation-like 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

order_type_of (X |_2 x) is epsilon-transitive epsilon-connected ordinal set

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

A is Relation-like Function-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

c

a is set

A . a is set

x is epsilon-transitive epsilon-connected ordinal set

y is epsilon-transitive epsilon-connected ordinal set

A . y is set

y is epsilon-transitive epsilon-connected ordinal set

B is epsilon-transitive epsilon-connected ordinal 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

x is epsilon-transitive epsilon-connected ordinal set

y is epsilon-transitive epsilon-connected ordinal set

A . y is set

B is set

y is set

Z2 is set

A . Z2 is set

y is epsilon-transitive epsilon-connected ordinal set

x is epsilon-transitive epsilon-connected ordinal cardinal set

X is set

union X is set

card (union X) is epsilon-transitive epsilon-connected ordinal cardinal set

A is set

union A is set

Y is set

Y is set

Y is Relation-like set

Y is Relation-like set

field Y is set

proj1 Y is set

proj2 Y is set

(proj1 Y) \/ (proj2 Y) is set

Y is set

c

[Y,c

{Y,c

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

{{Y,c

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

c

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

c

Y is set

c

[Y,c

{Y,c

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

{{Y,c

a is set

[c

{c

{c

{{c

[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

c

[Y,c

{Y,c

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

{{Y,c

[c

{c

{c

{{c

a is set

a is set

a is set

x is set

a is set

x is set

Y is set

c

[Y,c

{Y,c

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

{{Y,c

[c

{c

{c

{{c

a is set

a is set

Y is set

c

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

order_type_of Y is epsilon-transitive epsilon-connected ordinal set

RelIncl (order_type_of Y) is Relation-like set

Y is Relation-like Function-like set

field (RelIncl (order_type_of Y)) is set

proj1 (RelIncl (order_type_of Y)) is set

proj2 (RelIncl (order_type_of Y)) is set

(proj1 (RelIncl (order_type_of Y))) \/ (proj2 (RelIncl (order_type_of Y))) is set

proj1 Y is set

proj2 Y is set

c

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

c

card c

Y . c

Y -Seg (Y . c

Coim (Y,(Y . c

{(Y . c

Y " {(Y . c

(Coim (Y,(Y . c

bool (Coim (Y,(Y . c

card (Y -Seg (Y . c

Y | c

a is Relation-like Function-like set

proj1 a is set

proj2 a is set

x is set

y is set

a . y is set

B is epsilon-transitive epsilon-connected ordinal set

[B,c

{B,c

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

{{B,c

Y . B is set

[x,(Y . c

{x,(Y . c

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

{{x,(Y . c

x is set

[x,(Y . c

{x,(Y . c

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

{{x,(Y . c

y is set

Y . y is set

B is epsilon-transitive epsilon-connected ordinal set

[B,c

{B,c

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

{{B,c

c

Y . c

x is set

Y -Seg (Y . c

Coim (Y,(Y . c

{(Y . c

Y " {(Y . c

(Coim (Y,(Y . c

bool (Coim (Y,(Y . c

card (Y -Seg (Y . c

card x is epsilon-transitive epsilon-connected ordinal cardinal set

a is epsilon-transitive epsilon-connected ordinal set

card a is epsilon-transitive epsilon-connected ordinal cardinal set

card (order_type_of Y) is epsilon-transitive epsilon-connected ordinal cardinal set

card x is epsilon-transitive epsilon-connected ordinal cardinal set

x is Relation-like Function-like set

(x) is set

A is set

proj1 x is set

Y is Relation-like Function-like set

proj1 Y is set

x is set

X is with_non-empty_elements set

[:x,X:] is Relation-like set

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

A is Relation-like x -defined X -valued Function-like quasi_total Element of bool [:x,X:]

rng A is Element of bool X

bool X is non empty V56() V58() V59() set

x is Relation-like non-empty Function-like set

(x) is functional set

proj2 x is with_non-empty_elements 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

c

a is Relation-like Function-like finite set

proj1 a is finite 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

a is Relation-like Function-like 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 Relation-like Function-like set

(X) is functional set

x is Relation-like Function-like set

proj1 x is set

proj2 x is set

union (proj2 x) is set

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

X is set

A is set

Y is Relation-like Function-like 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

proj2 x is set

union (proj2 x) is set

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

X is set

[:(proj1 x),(union (proj2 x)):] is Relation-like set

bool [:(proj1 x),(union (proj2 x)):] is non empty V56() V58() V59() set

A is set

{} . A is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V42() finite finite-yielding V52() cardinal {} -element () set

x . A is set

A is set

Y is Relation-like Function-like set

proj1 Y is set

Y is set

A is non empty functional set

Y is Relation-like Function-like set

proj1 Y is set

proj2 Y is set

Y is set

c

Y . c

x . c

x is Relation-like Function-like set

proj1 x is set

X is Relation-like Function-like set

(X) is non empty functional set

proj1 X is set

A is set

x . A is set

X . A is set

Y is Relation-like Function-like set

proj1 Y is set

x is Relation-like Function-like set

(x) is non empty functional set

proj1 x is set

X is set

{} . X is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V42() finite finite-yielding V52() cardinal {} -element () set

x . X is set

x is Relation-like Function-like set

(x) is non empty functional set

x is Relation-like Function-like set

(x) is functional set

(x) is non empty functional set

X is set

proj1 x is set

A is Relation-like Function-like set

proj1 A is set

x is set

X is Relation-like Function-like set

(X) is non empty functional set

proj1 X is set

proj2 X is set

union (proj2 X) is set

[:(proj1 X),(union (proj2 X)):] is Relation-like set

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

A is Relation-like Function-like 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 Relation-like Function-like set

X is Relation-like Function-like set

(X) is functional set

(X) is non empty functional set

A is Relation-like Function-like set

x +* A is Relation-like Function-like set

proj1 x is set

proj1 X is set

proj1 A is set

(proj1 x) \/ (proj1 A) is set

proj1 (x +* A) is set

Y is set

(proj1 x) \ (proj1 A) is Element of bool (proj1 x)

bool (proj1 x) is non empty V56() V58() V59() set

((proj1 x) \ (proj1 A)) \/ (proj1 A) 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 Relation-like Function-like set

(x) is functional set

(x) is non empty functional set

X is Relation-like Function-like set

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

Y is Relation-like Function-like set

Y +* X is Relation-like Function-like set

A is Relation-like Function-like set

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 Relation-like Function-like set

(x) is non empty functional set

proj1 x is set

proj2 x is set

union (proj2 x) is set

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

X is set

[:(proj1 x),(union (proj2 x)):] is Relation-like set

bool [:(proj1 x),(union (proj2 x)):] is non empty V56() V58() V59() set

x is Relation-like Function-like set

(x) is non empty functional set

X is Relation-like Function-like set

(X) is non empty functional set

proj1 x is set

proj1 X is set

A is set

Y is Relation-like Function-like 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 --> X is Relation-like x -defined {X} -valued Function-like constant total quasi_total Element of bool [:x,{X}:]

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

[:x,{X}:] is Relation-like set

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

((x --> X)) is non empty functional set

{} --> X is empty Relation-like non-empty empty-yielding {} -defined {X} -valued Function-like one-to-one constant functional total epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural quasi_total Function-yielding V42() finite finite-yielding V52() cardinal {} -element () Element of bool [:{},{X}:]

[:{},{X}:] is Relation-like finite 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

Y is Relation-like Function-like 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 Relation-like x -defined X -valued Function-like quasi_total Element of bool [:x,X:]

(A) is non empty functional set

{ b

A | { b

((A | { b

Y is set

dom A is Element of bool x

bool x is non empty V56() V58() V59() set

Y is Relation-like Function-like set

proj1 Y is set

c

a is Element of x

A . a is Element of X

c

(dom A) /\ { b

dom (A | { b

c

c

Y . c

A . c

(A | { b

x is set

X is set

x .--> X is trivial Relation-like {x} -defined Function-like one-to-one constant finite set

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

{x} --> X is non empty Relation-like {x} -defined {X} -valued Function-like constant total quasi_total finite Element of bool [:{x},{X}:]

{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

A is Relation-like Function-like 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 Relation-like Function-like 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 .--> the Element of x . X is trivial Relation-like {X} -defined Function-like one-to-one constant finite set

{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

A is Relation-like Function-like 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 Relation-like Function-like set

(x) is non empty functional set

X is set

union X is set

A is Relation-like Function-like 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

c

proj1 c

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

c

proj1 c

c

A . Y is set

x . Y is set

x is Relation-like Function-like set

X is Relation-like Function-like set

x \/ X is Relation-like set

A is Relation-like Function-like set

(A) is non empty functional set

{x,X} is non empty functional finite set

Y is Relation-like Function-like set

Y is Relation-like Function-like set

union {x,X} is set

x is set

X is Relation-like Function-like set

A is Relation-like Function-like set

(A) is non empty functional set

Y is Relation-like Function-like 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 Relation-like Function-like set

X is Relation-like Function-like set

(X) is non empty functional set

A is set

x | A is Relation-like Function-like set

x is Relation-like Function-like set

X is Relation-like Function-like set

(X) is non empty functional set

A is set

x | A is Relation-like Function-like set

X | A is Relation-like Function-like set

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

proj1 (x | A) is set

proj1 x is set

(proj1 x) /\ A is set

proj1 (X | A) is set

proj1 X is set

(proj1 X) /\ 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 Relation-like Function-like set

X is Relation-like Function-like set

(X) is non empty functional set

A is Relation-like Function-like set

X +* A is Relation-like Function-like set

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

(A) is non empty functional set

proj1 X is set

proj1 A is set

(proj1 X) \ (proj1 A) is Element of bool (proj1 X)

bool (proj1 X) is non empty V56() V58() V59() set

x | ((proj1 X) \ (proj1 A)) is Relation-like Function-like set

x | (proj1 A) is Relation-like Function-like set

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

(X +* A) | ((proj1 X) \ (proj1 A)) is Relation-like Function-like set

(((X +* A) | ((proj1 X) \ (proj1 A)))) is non empty functional set

(X +* A) | (proj1 A) is Relation-like Function-like set

proj1 x is set

proj1 (X +* A) is set

(proj1 X) \/ (proj1 A) is set

((proj1 X) \ (proj1 A)) \/ (proj1 A) is set

x is Relation-like Function-like set

proj1 x is set

(x) is non empty functional set

X is Relation-like Function-like set

(X) is non empty functional set

X +* x is Relation-like Function-like set

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

A is Relation-like Function-like set

proj1 A is set

Y is Relation-like Function-like set

proj1 Y is set

(proj1 A) \ (proj1 Y) is Element of bool (proj1 A)

bool (proj1 A) is non empty V56() V58() V59() set

A +* Y is Relation-like Function-like set

proj1 X is set

(proj1 A) \/ (proj1 Y) is set

(proj1 X) \/ (proj1 x) 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

((proj1 A) \ (proj1 Y)) \/ (proj1 Y) 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

x is Relation-like Function-like