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
F1() is set
x is Relation-like Function-like set
proj1 x is set
X is set
x . X is set
F2(X) is epsilon-transitive epsilon-connected ordinal cardinal set
X is Relation-like Function-like () set
proj1 X is set
A is set
X . A is set
F2(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
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
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 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
c7 is Relation-like Function-like set
c7 . x is set
Y is Relation-like Function-like set
Y . x is set
Y . Y is set
c7 is Relation-like Function-like set
c7 . x is set
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
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 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
c7 is Relation-like Function-like set
c7 . X is set
Y is Relation-like Function-like set
Y . X is set
Y . Y is set
c7 is Relation-like Function-like set
c7 . X is set
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)
c7 is Relation-like Function-like set
proj1 c7 is set
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
c7 . x is set
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
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
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
c7 is set
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
c7 is Relation-like Function-like set
proj1 c7 is set
a is set
x is set
c7 . x is set
Y . x is set
Y is Relation-like Function-like 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
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
[(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
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
c7 is Relation-like Function-like set
proj1 c7 is set
proj2 c7 is set
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
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
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
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
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
c7 is set
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
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
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
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
c7 is epsilon-transitive epsilon-connected ordinal set
card c7 is epsilon-transitive epsilon-connected ordinal cardinal 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
card (Y -Seg (Y . c7)) is epsilon-transitive epsilon-connected ordinal cardinal set
Y | c7 is Relation-like Function-like set
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,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 is epsilon-transitive epsilon-connected ordinal 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
c7 is epsilon-transitive epsilon-connected ordinal 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
card (Y -Seg (Y . c7)) is epsilon-transitive epsilon-connected ordinal cardinal set
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
c7 is set
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
c7 is set
Y . c7 is set
x . c7 is set
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
{ 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
Y is Relation-like Function-like 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 .--> 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
c7 is Relation-like Function-like 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
c7 is Relation-like Function-like set
proj1 c7 is set
c7 . 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 \/ 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 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 x) \ (proj1 Y) is Element of bool (proj1 x)
bool (proj1 x) is non empty V56() V58() V59() set
A +* Y is Relation-like Function-like set
(proj1 A) \ (proj1 Y) is Element of bool (proj1 A)
bool (proj1 A) is non empty V56() V58() V59() 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
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
A . Y is set
X . Y is set
(x +* A) . Y is set
x . Y is set
X . Y is set
(x +* A) . 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
proj1 x is set
(x) is non empty functional set
X is set
Y is set
x . X is set
A is set
Y is set
x . A is set
(X,A) --> (Y,Y) is Relation-like Function-like finite set
X .--> Y is trivial Relation-like {X} -defined Function-like one-to-one constant finite set
{X} is non empty trivial finite 1 -element set
{X} --> Y is non empty Relation-like {X} -defined {Y} -valued Function-like constant total quasi_total finite Element of bool [:{X},{Y}:]
{Y} is non empty trivial finite 1 -element set
[:{X},{Y}:] is non empty Relation-like finite set
bool [:{X},{Y}:] is non empty finite V52() V56() V58() V59() set
A .--> Y is trivial Relation-like {A} -defined Function-like one-to-one constant finite set
{A} is non empty trivial finite 1 -element set
{A} --> Y is non empty Relation-like {A} -defined {Y} -valued Function-like constant total quasi_total finite Element of bool [:{A},{Y}:]
{Y} is non empty trivial finite 1 -element set
[:{A},{Y}:] is non empty Relation-like finite set
bool [:{A},{Y}:] is non empty finite V52() V56() V58() V59() set
(X .--> Y) +* (A .--> Y) is Relation-like Function-like finite set
the Relation-like Function-like set is Relation-like Function-like set
{ the Relation-like Function-like set } is non empty trivial functional finite 1 -element set
X is non empty trivial functional finite 1 -element set
A is Relation-like Function-like set
Y is Relation-like Function-like set
proj1 A is set
proj1 Y is set
x is Relation-like Function-like set
{x} is non empty trivial functional finite 1 -element set
X is Relation-like Function-like set
A is Relation-like Function-like set
proj1 X is set
proj1 A is set
x is functional set
{ (proj1 b1) where b1 is Relation-like Function-like Element of x : verum } is set
meet { (proj1 b1) where b1 is Relation-like Function-like Element of x : verum } is set
x is functional () set
(x) is set
{ (proj1 b1) where b1 is Relation-like Function-like Element of x : verum } is set
meet { (proj1 b1) where b1 is Relation-like Function-like Element of x : verum } is set
A is Relation-like Function-like set
proj1 A is set
{(proj1 A)} is non empty trivial finite 1 -element set
Y is set
Y is Relation-like Function-like Element of x
proj1 Y is set
x is functional () set
(x) is set
{ (proj1 b1) where b1 is Relation-like Function-like Element of x : verum } is set
meet { (proj1 b1) where b1 is Relation-like Function-like Element of x : verum } 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
{ (proj1 b1) where b1 is Relation-like Function-like Element of x : verum } is set
meet { (proj1 b1) where b1 is Relation-like Function-like Element of x : verum } is set
A is set
Y is Relation-like Function-like epsilon-transitive epsilon-connected ordinal natural finite cardinal Element of x
proj1 Y is finite set
A is set
the Relation-like Function-like epsilon-transitive epsilon-connected ordinal natural finite cardinal Element of x is Relation-like Function-like epsilon-transitive epsilon-connected ordinal natural finite cardinal Element of x
proj1 the Relation-like Function-like epsilon-transitive epsilon-connected ordinal natural finite cardinal Element of x is finite set
x is functional set
(x) is set
{ (proj1 b1) where b1 is Relation-like Function-like Element of x : verum } is set
meet { (proj1 b1) where b1 is Relation-like Function-like Element of x : verum } 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 non empty functional set
{ (proj1 b1) where b1 is Relation-like Function-like Element of X : verum } is set
meet { (proj1 b1) where b1 is Relation-like Function-like Element of X : verum } is set
Y is set
(Y,x) is set
Y is Relation-like Function-like set
proj1 Y is set
Y is set
Y . Y is set
(Y,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
A . Y is set
(Y,x) is set
x is non empty functional set
(x) is Relation-like Function-like set
proj1 (x) is set
X is set
(x) . X is set
{ (b1 . X) where b1 is Relation-like Function-like Element of x : verum } is set
A is set
(X,x) is set
Y is Relation-like Function-like set
Y . X is set
A is set
Y is Relation-like Function-like Element of x
Y . X is set
x is Relation-like Function-like set
(x) is functional set
x is set
X is Relation-like Function-like set
(X) is functional () set
A is Relation-like Function-like set
Y is Relation-like Function-like set
proj1 A is set
proj1 Y is set
proj1 X is set
the with_non-empty_elements set is with_non-empty_elements set
[:{}, the with_non-empty_elements set :] is Relation-like set
bool [:{}, the with_non-empty_elements set :] is non empty V56() V58() V59() set
the empty Relation-like non-empty empty-yielding {} -defined the with_non-empty_elements set -valued Function-like one-to-one constant functional 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 [:{}, the with_non-empty_elements set :] is empty Relation-like non-empty empty-yielding {} -defined the with_non-empty_elements set -valued Function-like one-to-one constant functional 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 [:{}, the with_non-empty_elements set :]
( the empty Relation-like non-empty empty-yielding {} -defined the with_non-empty_elements set -valued Function-like one-to-one constant functional 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 [:{}, the with_non-empty_elements set :]) is non empty functional () () set
x is functional () set
(x) is Relation-like Function-like set
((x)) is functional () () set
X is set
A is Relation-like Function-like Element of x
proj1 A is set
(x) is set
{ (proj1 b1) where b1 is Relation-like Function-like Element of x : verum } is set
meet { (proj1 b1) where b1 is Relation-like Function-like Element of x : verum } is set
proj1 (x) is set
Y is set
A . Y is set
(x) . Y is set
(Y,x) is set
x is non empty functional () () set
(x) is Relation-like Function-like set
((x)) is functional () () set
X is set
proj1 (x) is set
A is Relation-like Function-like set
proj1 A is set
Y is Relation-like Function-like set
(Y) is functional () () set
the Relation-like Function-like Element of x is Relation-like Function-like Element of x
(x) is set
{ (proj1 b1) where b1 is Relation-like Function-like Element of x : verum } is set
meet { (proj1 b1) where b1 is Relation-like Function-like Element of x : verum } is set
proj1 the Relation-like Function-like Element of x is set
proj1 Y is set
Y is set
A . Y is set
Y . Y is set
(x) . Y is set
(Y,x) is set
c7 is Relation-like Function-like set
c7 . Y is set
x is Relation-like Function-like set
(x) is functional () () set
X is Relation-like Function-like Element of (x)
A is Relation-like Function-like Element of (x)
Y is set
A | Y is Relation-like Function-like set
X +* (A | Y) is Relation-like Function-like set
(x) is non empty functional set
proj2 x is set
x is Relation-like non-empty Function-like set
(x) is non empty functional set
(x) is non empty functional () () set
X is Relation-like Function-like Element of (x)
the Relation-like Function-like Element of (x) is Relation-like Function-like Element of (x)
the Relation-like Function-like Element of (x) +* X is Relation-like Function-like set
Y is Relation-like Function-like Element of (x)
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 set
x | A is Relation-like Function-like set
x is Relation-like non-empty Function-like set
(x) is non empty functional () () set
X is Relation-like Function-like Element of (x)
A is set
X | A is Relation-like Function-like set
(x) is non empty functional set
x is Relation-like non-empty Function-like set
(x) is non empty functional () () set
A is Relation-like Function-like Element of (x)
X is Relation-like Function-like Element of (x)
Y is set
(x,X,Y) is Relation-like Function-like Element of (x)
(x) is non empty functional set
A +* (x,X,Y) is Relation-like Function-like set
(A +* (x,X,Y)) | Y is Relation-like Function-like set
proj1 X is set
proj1 x is set
proj1 A is set
Y /\ (proj1 A) is set
Y /\ (proj1 X) is set
X is Relation-like Function-like set
x is Relation-like Function-like set
(x) is functional () () set
A is Relation-like Function-like set
A * X is Relation-like Function-like set
A * x is Relation-like Function-like set
((A * x)) is functional () () set
proj1 x is set
proj1 (A * X) is set
proj1 (A * x) is set
Y is Relation-like Function-like set
proj1 Y is set
Y is set
proj1 A is set
A . Y is set
(A * X) . Y is set
X . (A . Y) is set
(A * x) . Y is set
x . (A . Y) is set
c7 is Relation-like Function-like set
proj1 c7 is set
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 epsilon-transitive epsilon-connected ordinal set
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
proj1 X is set
proj2 X is set
X .: omega is set
A is set
card A is epsilon-transitive epsilon-connected ordinal cardinal set
X | omega is Relation-like Function-like set
proj1 (X | omega) is set
proj2 (X | omega) is set
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
nextcard x is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
card X is epsilon-transitive epsilon-connected ordinal cardinal set
nextcard X is epsilon-transitive epsilon-connected ordinal cardinal set
x is epsilon-transitive epsilon-connected ordinal cardinal set
nextcard x is epsilon-transitive epsilon-connected ordinal cardinal set
X is epsilon-transitive epsilon-connected ordinal cardinal set
nextcard X 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
x is epsilon-transitive epsilon-connected ordinal cardinal set
nextcard 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 epsilon-transitive epsilon-connected ordinal cardinal set
X is epsilon-transitive epsilon-connected ordinal cardinal set
nextcard X 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
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 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
card x is epsilon-transitive epsilon-connected ordinal cardinal set
x is set
card 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
proj1 X is set
proj2 X is set
x is () set
bool x is non empty V56() V58() V59() set
X is Element of bool x
card X is epsilon-transitive epsilon-connected ordinal cardinal set
card x is epsilon-transitive epsilon-connected ordinal cardinal set
x is set
X is set
x is set
X is set
x /\ X is set
x is set
X is set
x \ X is Element of bool x
bool x is non empty V56() V58() V59() set
x is non empty () set
[:omega,x:] is non empty non trivial non empty-membered Relation-like non finite set
bool [:omega,x:] is non empty non trivial non empty-membered non finite V56() V58() V59() set
X is Relation-like Function-like set
proj1 X is set
proj2 X is set
A is set
X " x is set
X | (X " x) is Relation-like Function-like set
omega \ (X " x) is () Element of bool omega
(omega \ (X " x)) --> A is Relation-like omega \ (X " x) -defined {A} -valued Function-like constant total quasi_total Element of bool [:(omega \ (X " x)),{A}:]
{A} is non empty trivial finite 1 -element () set
[:(omega \ (X " x)),{A}:] is Relation-like set
bool [:(omega \ (X " x)),{A}:] is non empty V56() V58() V59() set
(X | (X " x)) +* ((omega \ (X " x)) --> A) is Relation-like Function-like set
proj2 ((X | (X " x)) +* ((omega \ (X " x)) --> A)) is set
proj1 ((X | (X " x)) +* ((omega \ (X " x)) --> A)) is set
proj1 (X | (X " x)) is set
omega /\ (X " x) is set
dom ((omega \ (X " x)) --> A) is () Element of bool (omega \ (X " x))
bool (omega \ (X " x)) is non empty V56() V58() V59() set
(proj1 (X | (X " x))) /\ (dom ((omega \ (X " x)) --> A)) is () Element of bool (omega \ (X " x))
(X | (X " x)) \/ ((omega \ (X " x)) --> A) is Relation-like set
proj2 (X | (X " x)) is set
rng ((omega \ (X " x)) --> A) is trivial finite () Element of bool {A}
bool {A} is non empty finite V52() V56() V58() V59() () set
(proj2 (X | (X " x))) \/ (rng ((omega \ (X " x)) --> A)) is set
(proj2 (X | (X " x))) \/ {} is set
X .: (X " x) is set
(proj1 (X | (X " x))) \/ (dom ((omega \ (X " x)) --> A)) is set
(proj1 (X | (X " x))) \/ {} is set
dom ((omega \ (X " x)) --> A) is () Element of bool (omega \ (X " x))
bool (omega \ (X " x)) is non empty V56() V58() V59() set
(X | (X " x)) \/ ((omega \ (X " x)) --> A) is Relation-like set
proj2 (X | (X " x)) is set
rng ((omega \ (X " x)) --> A) is trivial finite () Element of bool {A}
bool {A} is non empty finite V52() V56() V58() V59() () set
(proj2 (X | (X " x))) \/ (rng ((omega \ (X " x)) --> A)) is set
(proj2 (X | (X " x))) \/ {A} is non empty set
X .: (X " x) is set
(X .: (X " x)) \/ {A} is non empty set
x \/ {A} is non empty set
(proj1 (X | (X " x))) \/ (dom ((omega \ (X " x)) --> A)) is set
(omega /\ (X " x)) \/ (omega \ (X " x)) is set
Y is Relation-like omega -defined x -valued Function-like quasi_total Element of bool [:omega,x:]
rng Y 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 non empty functional () () set
X is Relation-like non-empty Function-like set
(X) is non empty functional () () set
x +* X is Relation-like non-empty Function-like set
((x +* X)) is non empty functional () () set
A is Relation-like Function-like Element of (x)
Y is Relation-like Function-like Element of (X)
A +* Y is Relation-like Function-like set
proj1 A is set
proj1 x is set
proj1 Y is set
proj1 X is set
proj1 (A +* Y) is set
(proj1 x) \/ (proj1 X) is set
proj1 (x +* X) is set
Y is set
(A +* Y) . Y is set
A . Y is set
(x +* X) . Y is set
x . Y is set
Y . Y is set
X . Y is set
x is Relation-like non-empty Function-like set
X is Relation-like non-empty Function-like set
x +* X is Relation-like non-empty Function-like set
((x +* X)) is non empty functional () () set
proj1 X is set
(X) is non empty functional () () set
A is Relation-like Function-like Element of ((x +* X))
((x +* X),A,(proj1 X)) is Relation-like Function-like Element of ((x +* X))
((x +* X)) is non empty functional set
proj1 A is set
proj1 (x +* X) is set
proj1 x is set
(proj1 x) \/ (proj1 X) is set
proj1 ((x +* X),A,(proj1 X)) is set
Y is set
((x +* X),A,(proj1 X)) . Y is set
A . Y is set
(x +* X) . Y is set
X . Y is set
x is Relation-like non-empty Function-like set
X is Relation-like non-empty Function-like set
x +* X is Relation-like non-empty Function-like set
((x +* X)) is non empty functional () () set
proj1 x is set
(x) is non empty functional () () set
A is Relation-like Function-like Element of ((x +* X))
((x +* X),A,(proj1 x)) is Relation-like Function-like Element of ((x +* X))
((x +* X)) is non empty functional set
proj1 A is set
proj1 (x +* X) is set
proj1 X is set
(proj1 x) \/ (proj1 X) is set
proj1 ((x +* X),A,(proj1 x)) is set
Y is set
((x +* X),A,(proj1 x)) . Y is set
A . Y is set
(x +* X) . Y is set
x . Y is set
x is functional () 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 set
{ (proj1 b1) where b1 is Relation-like Function-like Element of x : verum } is set
meet { (proj1 b1) where b1 is Relation-like Function-like Element of x : verum } is set
x is functional set
(x) is Relation-like Function-like set
proj1 (x) is set
X is Relation-like Function-like set
A is set
X . A is set
(x) . A is set
{ (b1 . A) where b1 is Relation-like Function-like Element of x : verum } is set
x is functional () set
(x) is Relation-like Function-like set
X is Relation-like Function-like set
proj1 X is set
A is set
X . A is set
(x) . A is set
proj1 (x) is set
x is () set
bool x is non empty V56() V58() V59() set
X is Element of bool x
A is Relation-like Function-like set
Y is Relation-like Function-like set
proj1 A is set
proj1 Y is set
x is Relation-like Function-like set
(x) is functional () () set
X is set
A is set
Y is Relation-like Function-like set
Y . X is set
Y is set
Y is Relation-like Function-like set
Y . X is set
A is Relation-like Function-like set
proj1 A is set
Y is Relation-like Function-like set
A . Y is set
Y . X 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
A . Y is set
Y is Relation-like Function-like set
Y . X is set
Y . Y is set
x is Relation-like Function-like set
(x) is functional () () set
X is set
(x,X) is Relation-like Function-like set
proj1 (x,X) is set
x is Relation-like Function-like set
(x) is functional () () set
X is set
(x,X) is Relation-like (x) -defined Function-like set
dom (x,X) is functional () Element of bool (x)
bool (x) is non empty V56() V58() V59() set
x is Relation-like non-empty Function-like set
(x) is non empty functional () () set
X is Relation-like Function-like Element of (x)
A is set
proj1 X is set
X . A is set
x . A is set
proj1 x is set
x is set
X is Relation-like non-empty x -defined Function-like set
(X) is non empty functional () () set
A is Relation-like x -defined Function-like X -compatible Element of (X)
x is Relation-like Function-like set
(x) is non empty functional set
X is Relation-like Function-like Element of (x)
A is set
proj1 X is set
X . A is set
x . A is set
x is set
X is Relation-like x -defined Function-like set
(X) is non empty functional set
A is Relation-like x -defined Function-like X -compatible Element of (X)
x is set
X is Relation-like non-empty x -defined Function-like total set
(X) is non empty functional () () set
A is Relation-like x -defined Function-like X -compatible Element of (X)
dom A is Element of bool x
bool x is non empty V56() V58() V59() set
dom X is Element of bool x
x is set
X is Relation-like non-empty x -defined Function-like set
(X) is non empty functional set
A is Relation-like x -defined Function-like X -compatible set
dom A is Element of bool x
bool x is non empty V56() V58() V59() set
dom X is Element of bool x
Y is set
A . Y is set
X . Y is set
x is set
X is Relation-like non-empty x -defined Function-like set
(X) is non empty functional () () set
A is Relation-like x -defined Function-like X -compatible set
(X) is non empty functional set
the Relation-like x -defined Function-like X -compatible Element of (X) is Relation-like x -defined Function-like X -compatible Element of (X)
Y is Relation-like x -defined Function-like X -compatible Element of (X)
the Relation-like x -defined Function-like X -compatible Element of (X) +* Y is Relation-like x -defined Function-like X -compatible set
Y is Relation-like x -defined Function-like X -compatible Element of (X)
x is non empty non trivial non empty-membered non finite set
X is set
x --> X is non empty 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 non empty non trivial non empty-membered Relation-like non finite set
bool [:x,{X}:] is non empty non trivial non empty-membered non finite V56() V58() V59() set
omega --> {} is non empty non trivial non empty-membered Relation-like omega -defined {{}} -valued Function-like constant total quasi_total Function-yielding V42() non finite () Element of bool [:omega,{{}}:]
[:omega,{{}}:] is non empty non trivial non empty-membered Relation-like non finite set
bool [:omega,{{}}:] is non empty non trivial non empty-membered non finite V56() V58() V59() set
x is non empty non trivial non empty-membered Relation-like non finite set
field x is set
proj1 x is non empty set
proj2 x is non empty set
(proj1 x) \/ (proj2 x) is non empty set
x is non empty non trivial non empty-membered non finite set
RelIncl x is Relation-like set
x is Relation-like set
X is Relation-like set
A is Relation-like Function-like set
field x is set
proj1 x is set
proj2 x is set
(proj1 x) \/ (proj2 x) is set
proj1 A is set
proj2 A is set
field X is set
proj1 X is set
proj2 X is set
(proj1 X) \/ (proj2 X) is set
({{}}) is Relation-like Function-like set
proj1 ({{}}) is set
({{}}) is set
{ (proj1 b1) where b1 is Relation-like Function-like Element of {{}} : verum } is set
meet { (proj1 b1) where b1 is Relation-like Function-like Element of {{}} : verum } is set
x is set
X is Relation-like non-empty x -defined Function-like total set
(X) is non empty functional () () set
A is Relation-like x -defined Function-like X -compatible total set
dom A is Element of bool x
bool x is non empty V56() V58() V59() set
dom X is Element of bool x
Y is set
A . Y is set
X . Y is set
x is set
X is Relation-like non-empty x -defined Function-like total set
(X) is non empty functional () () set
A is Relation-like x -defined Function-like X -compatible total Element of (X)
x is set
X is Relation-like non-empty x -defined Function-like total set
A is Relation-like x -defined Function-like X -compatible total set
(X) is non empty functional () () set
X is Relation-like Function-like set
x is functional () set
proj1 X is set
(x) is set
{ (proj1 b1) where b1 is Relation-like Function-like Element of x : verum } is set
meet { (proj1 b1) where b1 is Relation-like Function-like Element of x : verum } is set
x is set
X is non empty functional set
(X) is set
{ (proj1 b1) where b1 is Relation-like Function-like Element of X : verum } is set
meet { (proj1 b1) where b1 is Relation-like Function-like Element of X : verum } is set
Y is set
Y is Relation-like Function-like set
proj1 Y is set
Y is set
c7 is Relation-like Function-like Element of X
proj1 c7 is set