:: COH_SP semantic presentation

K132() is Element of bool K128()
K128() is set
bool K128() is non empty set
K114() is set
bool K114() is non empty set
bool K132() is non empty set
{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
the Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
bool {} is non empty set
{{}} is functional non empty set
union {} is set
[:{},{}:] is Relation-like set
bool [:{},{}:] is non empty set
X is functional non empty set
a is set
aa is set
a is set
union a is set
X is non empty subset-closed () set
a is set
aa is set
a \/ aa is set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
a is set
union a is set
aa is set
a is set
aa is set
X is set
{X} is non empty set
a is non empty subset-closed () set
union a is set
aa is set
X is non empty subset-closed () set
union X is set
[:(union X),(union X):] is Relation-like set
bool [:(union X),(union X):] is non empty set
a is set
{a} is non empty set
a is set
aa is set
ii is set
a is Relation-like union X -defined union X -valued total quasi_total V27() V29() Element of bool [:(union X),(union X):]
aa is set
ii is set
[aa,ii] is V15() set
{aa,ii} is non empty set
{aa} is non empty set
{{aa,ii},{aa}} is non empty set
ii is set
a is Relation-like union X -defined union X -valued total quasi_total V27() V29() Element of bool [:(union X),(union X):]
aa is Relation-like union X -defined union X -valued total quasi_total V27() V29() Element of bool [:(union X),(union X):]
X is non empty subset-closed () set
union X is set
[:(union X),(union X):] is Relation-like set
bool [:(union X),(union X):] is non empty set
(X) is Relation-like union X -defined union X -valued total quasi_total V27() V29() Element of bool [:(union X),(union X):]
a is Relation-like union X -defined union X -valued total quasi_total V27() V29() Element of bool [:(union X),(union X):]
aa is set
ii is set
[aa,ii] is V15() set
{aa,ii} is non empty set
{aa} is non empty set
{{aa,ii},{aa}} is non empty set
ii is set
aa is set
ii is set
[aa,ii] is V15() set
{aa,ii} is non empty set
{aa} is non empty set
{{aa,ii},{aa}} is non empty set
ii is set
X is set
a is non empty subset-closed () set
aa is set
ii is set
{aa,ii} is non empty set
aa is set
{aa} is non empty set
ii is set
ii is set
aa is set
ii is set
ii is set
ii \/ ii is set
c₆ is set
{c₆} is non empty set
gg is set
{gg} is non empty set
{gg,c₆} is non empty set
union aa is set
ii is set
ii is set
c₆ is set
{c₆} is non empty set
ii is set
{ii} is non empty set
ii is set
ii is set
{ii} is non empty set
{ii,ii} is non empty set
X is set
a is non empty subset-closed () set
(a) is Relation-like union a -defined union a -valued total quasi_total V27() V29() Element of bool [:(union a),(union a):]
union a is set
[:(union a),(union a):] is Relation-like set
bool [:(union a),(union a):] is non empty set
aa is set
ii is set
[aa,ii] is V15() set
{aa,ii} is non empty set
{aa} is non empty set
{{aa,ii},{aa}} is non empty set
aa is set
ii is set
[aa,ii] is V15() set
{aa,ii} is non empty set
{aa} is non empty set
{{aa,ii},{aa}} is non empty set
X is set
a is non empty subset-closed () set
union a is set
aa is set
{aa,aa} is non empty set
{aa} is non empty set
X is non empty subset-closed () set
(X) is Relation-like union X -defined union X -valued total quasi_total V27() V29() Element of bool [:(union X),(union X):]
union X is set
[:(union X),(union X):] is Relation-like set
bool [:(union X),(union X):] is non empty set
a is non empty subset-closed () set
(a) is Relation-like union a -defined union a -valued total quasi_total V27() V29() Element of bool [:(union a),(union a):]
union a is set
[:(union a),(union a):] is Relation-like set
bool [:(union a),(union a):] is non empty set
aa is set
ii is set
ii is set
[ii,ii] is V15() set
{ii,ii} is non empty set
{ii} is non empty set
{{ii,ii},{ii}} is non empty set
aa is set
ii is set
ii is set
[ii,ii] is V15() set
{ii,ii} is non empty set
{ii} is non empty set
{{ii,ii},{ii}} is non empty set
X is non empty subset-closed () set
union X is set
bool (union X) is non empty Element of bool (bool (union X))
bool (union X) is non empty set
bool (bool (union X)) is non empty set
a is set
X is non empty subset-closed () set
union X is set
bool (union X) is non empty Element of bool (bool (union X))
bool (union X) is non empty set
bool (bool (union X)) is non empty set
(X) is Relation-like union X -defined union X -valued total quasi_total V27() V29() Element of bool [:(union X),(union X):]
[:(union X),(union X):] is Relation-like set
bool [:(union X),(union X):] is non empty set
nabla (union X) is Relation-like union X -defined union X -valued total quasi_total V27() V29() V34() Element of bool [:(union X),(union X):]
aa is set
ii is set
[aa,ii] is V15() set
{aa,ii} is non empty set
{aa} is non empty set
{{aa,ii},{aa}} is non empty set
a is Relation-like union X -defined union X -valued total quasi_total V27() V29() Element of bool [:(union X),(union X):]
ii is set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
a is Relation-like X -defined X -valued total quasi_total V27() V29() Element of bool [:X,X:]
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
aa is set
ii is set
union ii is set
ii is set
c₆ is set
gg is set
aa is set
aa \/ gg is set
[ii,c₆] is V15() set
{ii,c₆} is non empty set
{ii} is non empty set
{{ii,c₆},{ii}} is non empty set
ii is set
ii is set
ii is set
c₆ is set
gg is set
[c₆,gg] is V15() set
{c₆,gg} is non empty set
{c₆} is non empty set
{{c₆,gg},{c₆}} is non empty set
ii is set
ii is set
[ii,ii] is V15() set
{ii,ii} is non empty set
{ii} is non empty set
{{ii,ii},{ii}} is non empty set
ii is non empty subset-closed () set
ii is set
c₆ is set
gg is set
[c₆,gg] is V15() set
{c₆,gg} is non empty set
{c₆} is non empty set
{{c₆,gg},{c₆}} is non empty set
aa is non empty subset-closed () set
ii is non empty subset-closed () set
ii is set
c₆ is set
gg is set
[c₆,gg] is V15() set
{c₆,gg} is non empty set
{c₆} is non empty set
{{c₆,gg},{c₆}} is non empty set
ii is set
c₆ is set
gg is set
[c₆,gg] is V15() set
{c₆,gg} is non empty set
{c₆} is non empty set
{{c₆,gg},{c₆}} is non empty set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
a is Relation-like X -defined X -valued total quasi_total V27() V29() Element of bool [:X,X:]
(X,a) is non empty subset-closed () set
((X,a)) is Relation-like union (X,a) -defined union (X,a) -valued total quasi_total V27() V29() Element of bool [:(union (X,a)),(union (X,a)):]
union (X,a) is set
[:(union (X,a)),(union (X,a)):] is Relation-like set
bool [:(union (X,a)),(union (X,a)):] is non empty set
aa is set
ii is set
[aa,ii] is V15() set
{aa,ii} is non empty set
{aa} is non empty set
{{aa,ii},{aa}} is non empty set
ii is set
c₆ is set
[ii,c₆] is V15() set
{ii,c₆} is non empty set
{ii} is non empty set
{{ii,c₆},{ii}} is non empty set
X is non empty subset-closed () set
union X is set
(X) is Relation-like union X -defined union X -valued total quasi_total V27() V29() Element of bool [:(union X),(union X):]
[:(union X),(union X):] is Relation-like set
bool [:(union X),(union X):] is non empty set
((union X),(X)) is non empty subset-closed () set
a is set
aa is set
ii is set
[aa,ii] is V15() set
{aa,ii} is non empty set
{aa} is non empty set
{{aa,ii},{aa}} is non empty set
a is set
aa is set
ii is set
[aa,ii] is V15() set
{aa,ii} is non empty set
{aa} is non empty set
{{aa,ii},{aa}} is non empty set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
a is set
aa is Relation-like X -defined X -valued total quasi_total V27() V29() Element of bool [:X,X:]
(X,aa) is non empty subset-closed () set
ii is set
ii is set
[ii,ii] is V15() set
{ii,ii} is non empty set
{ii} is non empty set
{{ii,ii},{ii}} is non empty set
ii is set
ii is set
[ii,ii] is V15() set
{ii,ii} is non empty set
{ii} is non empty set
{{ii,ii},{ii}} is non empty set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
a is Relation-like X -defined X -valued total quasi_total V27() V29() Element of bool [:X,X:]
(X,a) is non empty subset-closed () set
TolSets a is set
aa is set
aa is set
X is set
bool X is non empty set
bool (bool X) is non empty set
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
X is set
(X) is set
bool X is non empty set
bool (bool X) is non empty set
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
bool X is non empty Element of bool (bool X)
a is Element of bool (bool X)
X is set
(X) is non empty set
bool X is non empty set
bool (bool X) is non empty set
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
a is Element of (X)
aa is Element of bool (bool X)
X is set
(X) is non empty set
bool X is non empty set
bool (bool X) is non empty set
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
a is set
aa is set
{a,aa} is non empty set
ii is non empty subset-closed () Element of (X)
union ii is set
{a} is non empty set
{aa} is non empty set
X is set
(X) is non empty set
bool X is non empty set
bool (bool X) is non empty set
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
X is set
(X) is set
(X) is non empty set
bool X is non empty set
bool (bool X) is non empty set
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
bool X is non empty Element of bool (bool X)
a is Element of bool (bool X)
aa is non empty subset-closed () Element of (X)
union aa is set
id (union aa) is Relation-like union aa -defined union aa -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:(union aa),(union aa):]
[:(union aa),(union aa):] is Relation-like set
bool [:(union aa),(union aa):] is non empty set
Funcs ((union aa),(union aa)) is functional non empty set
c₆ is set
ii is non empty set
gg is set
aa is non empty subset-closed () Element of (X)
union aa is set
ii is non empty subset-closed () Element of (X)
union ii is set
Funcs ((union aa),(union ii)) is functional set
X is set
a is set
(a) is functional non empty set
(a) is non empty set
bool a is non empty set
bool (bool a) is non empty set
{ b₁ where b₁ is Element of bool (bool a) : b₁ is non empty subset-closed () set } is set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (a) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (a) : verum } is set
ii is set
ii is non empty subset-closed () Element of (a)
union ii is set
c₆ is non empty subset-closed () Element of (a)
union c₆ is set
Funcs ((union ii),(union c₆)) is functional set
[:(union ii),(union c₆):] is Relation-like set
bool [:(union ii),(union c₆):] is non empty set
ii is non empty subset-closed () Element of (a)
union ii is set
ii is non empty subset-closed () Element of (a)
union ii is set
[:(union ii),(union ii):] is Relation-like set
bool [:(union ii),(union ii):] is non empty set
Funcs ((union ii),(union ii)) is functional set
X is set
(X) is non empty set
bool X is non empty set
bool (bool X) is non empty set
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is non empty subset-closed () Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not union b₂ = {} or union b₁ = {} ) & b₃ is Relation-like union b₁ -defined union b₂ -valued Function-like quasi_total Element of bool [:(union b₁),(union b₂):] & ( for b₄, b₅ being set holds
( not {b₄,b₅} in b₁ or {(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) ) } is set
X is set
(X) is set
(X) is non empty set
bool X is non empty set
bool (bool X) is non empty set
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is non empty subset-closed () Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not union b₂ = {} or union b₁ = {} ) & b₃ is Relation-like union b₁ -defined union b₂ -valued Function-like quasi_total Element of bool [:(union b₁),(union b₂):] & ( for b₄, b₅ being set holds
( not {b₄,b₅} in b₁ or {(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) ) } is set
bool X is non empty Element of bool (bool X)
aa is Element of bool (bool X)
ii is non empty subset-closed () Element of (X)
union ii is set
id (union ii) is Relation-like union ii -defined union ii -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:(union ii),(union ii):]
[:(union ii),(union ii):] is Relation-like set
bool [:(union ii),(union ii):] is non empty set
[ii,ii] is V15() set
{ii,ii} is non empty set
{ii} is non empty set
{{ii,ii},{ii}} is non empty set
[[ii,ii],(id (union ii))] is V15() set
{[ii,ii],(id (union ii))} is non empty set
{[ii,ii]} is Relation-like Function-like non empty set
{{[ii,ii],(id (union ii))},{[ii,ii]}} is non empty set
aa is set
ii is set
{aa,ii} is non empty set
gg is Relation-like Function-like Element of (X)
gg . aa is set
gg . ii is set
{(gg . aa),(gg . ii)} is non empty set
c₆ is V15() set
aa is V15() set
X is set
(X) is non empty set
(X) is non empty set
bool X is non empty set
bool (bool X) is non empty set
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is non empty subset-closed () Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not union b₂ = {} or union b₁ = {} ) & b₃ is Relation-like union b₁ -defined union b₂ -valued Function-like quasi_total Element of bool [:(union b₁),(union b₂):] & ( for b₄, b₅ being set holds
( not {b₄,b₅} in b₁ or {(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) ) } is set
a is Element of (X)
aa is non empty subset-closed () Element of (X)
ii is non empty subset-closed () Element of (X)
[aa,ii] is V15() set
{aa,ii} is non empty set
{aa} is non empty set
{{aa,ii},{aa}} is non empty set
ii is Relation-like Function-like Element of (X)
[[aa,ii],ii] is V15() set
{[aa,ii],ii} is non empty set
{[aa,ii]} is Relation-like Function-like non empty set
{{[aa,ii],ii},{[aa,ii]}} is non empty set
union ii is set
union aa is set
[:(union aa),(union ii):] is Relation-like set
bool [:(union aa),(union ii):] is non empty set
X is set
(X) is non empty set
bool X is non empty set
bool (bool X) is non empty set
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
(X) is non empty set
(X) is functional non empty set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is non empty subset-closed () Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not union b₂ = {} or union b₁ = {} ) & b₃ is Relation-like union b₁ -defined union b₂ -valued Function-like quasi_total Element of bool [:(union b₁),(union b₂):] & ( for b₄, b₅ being set holds
( not {b₄,b₅} in b₁ or {(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) ) } is set
a is non empty subset-closed () Element of (X)
union a is set
aa is non empty subset-closed () Element of (X)
union aa is set
[:(union a),(union aa):] is Relation-like set
bool [:(union a),(union aa):] is non empty set
[a,aa] is V15() set
{a,aa} is non empty set
{a} is non empty set
{{a,aa},{a}} is non empty set
ii is Relation-like union a -defined union aa -valued Function-like quasi_total Element of bool [:(union a),(union aa):]
[[a,aa],ii] is V15() set
{[a,aa],ii} is non empty set
{[a,aa]} is Relation-like Function-like non empty set
{{[a,aa],ii},{[a,aa]}} is non empty set
ii is Relation-like Function-like Element of (X)
c₆ is set
gg is set
{c₆,gg} is non empty set
ii . c₆ is set
ii . gg is set
{(ii . c₆),(ii . gg)} is non empty set
X is set
(X) is non empty set
(X) is non empty set
bool X is non empty set
bool (bool X) is non empty set
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is non empty subset-closed () Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not union b₂ = {} or union b₁ = {} ) & b₃ is Relation-like union b₁ -defined union b₂ -valued Function-like quasi_total Element of bool [:(union b₁),(union b₂):] & ( for b₄, b₅ being set holds
( not {b₄,b₅} in b₁ or {(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) ) } is set
a is Element of (X)
a `2 is set
ii is non empty subset-closed () Element of (X)
ii is non empty subset-closed () Element of (X)
[ii,ii] is V15() set
{ii,ii} is non empty set
{ii} is non empty set
{{ii,ii},{ii}} is non empty set
aa is Relation-like Function-like Element of (X)
[[ii,ii],aa] is V15() set
{[ii,ii],aa} is non empty set
{[ii,ii]} is Relation-like Function-like non empty set
{{[ii,ii],aa},{[ii,ii]}} is non empty set
union ii is set
union ii is set
[:(union ii),(union ii):] is Relation-like set
bool [:(union ii),(union ii):] is non empty set
[[ii,ii],aa] `2 is set
X is set
(X) is non empty set
(X) is non empty set
bool X is non empty set
bool (bool X) is non empty set
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is non empty subset-closed () Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not union b₂ = {} or union b₁ = {} ) & b₃ is Relation-like union b₁ -defined union b₂ -valued Function-like quasi_total Element of bool [:(union b₁),(union b₂):] & ( for b₄, b₅ being set holds
( not {b₄,b₅} in b₁ or {(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) ) } is set
a is Element of (X)
a `1 is set
(a `1) `1 is set
ii is non empty subset-closed () Element of (X)
ii is non empty subset-closed () Element of (X)
[ii,ii] is V15() set
{ii,ii} is non empty set
{ii} is non empty set
{{ii,ii},{ii}} is non empty set
aa is Relation-like Function-like Element of (X)
[[ii,ii],aa] is V15() set
{[ii,ii],aa} is non empty set
{[ii,ii]} is Relation-like Function-like non empty set
{{[ii,ii],aa},{[ii,ii]}} is non empty set
union ii is set
union ii is set
[:(union ii),(union ii):] is Relation-like set
bool [:(union ii),(union ii):] is non empty set
[[ii,ii],aa] `1 is set
[ii,ii] `1 is set
(a `1) `2 is set
ii is non empty subset-closed () Element of (X)
ii is non empty subset-closed () Element of (X)
[ii,ii] is V15() set
{ii,ii} is non empty set
{ii} is non empty set
{{ii,ii},{ii}} is non empty set
aa is Relation-like Function-like Element of (X)
[[ii,ii],aa] is V15() set
{[ii,ii],aa} is non empty set
{[ii,ii]} is Relation-like Function-like non empty set
{{[ii,ii],aa},{[ii,ii]}} is non empty set
union ii is set
union ii is set
[:(union ii),(union ii):] is Relation-like set
bool [:(union ii),(union ii):] is non empty set
[[ii,ii],aa] `1 is set
[ii,ii] `2 is set
X is set
(X) is non empty set
(X) is non empty set
bool X is non empty set
bool (bool X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (bool X) : b<sub>1</sub> is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b<sub>1</sub>),(union b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b<sub>1</sub>),(union b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X) : verum } is set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X), b<sub>3</sub> is Relation-like Function-like Element of (X) : ( ( not union b<sub>2</sub> = {} or union b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like union b<sub>1</sub> -defined union b<sub>2</sub> -valued Function-like quasi_total Element of bool [:(union b<sub>1</sub>),(union b<sub>2</sub>):] & ( for b<sub>4</sub>, b<sub>5</sub> being set holds
( not {b<sub>4</sub>,b<sub>5</sub>} in b<sub>1</sub> or {(b<sub>3</sub> . b<sub>4</sub>),(b<sub>3</sub> . b<sub>5</sub>)} in b<sub>2</sub> ) ) ) } is set
a is Element of (X)
(X,a) is non empty subset-closed () Element of (X)
a `1 is set
(a `1) `1 is set
(X,a) is non empty subset-closed () Element of (X)
(a `1) `2 is set
[(X,a),(X,a)] is V15() set
{(X,a),(X,a)} is non empty set
{(X,a)} is non empty set
{{(X,a),(X,a)},{(X,a)}} is non empty set
a `2 is Relation-like Function-like set
[[(X,a),(X,a)],(a `2)] is V15() set
{[(X,a),(X,a)],(a `2)} is non empty set
{[(X,a),(X,a)]} is Relation-like Function-like non empty set
{{[(X,a),(X,a)],(a `2)},{[(X,a),(X,a)]}} is non empty set
ii is non empty subset-closed () Element of (X)
ii is non empty subset-closed () Element of (X)
[ii,ii] is V15() set
{ii,ii} is non empty set
{ii} is non empty set
{{ii,ii},{ii}} is non empty set
aa is Relation-like Function-like Element of (X)
[[ii,ii],aa] is V15() set
{[ii,ii],aa} is non empty set
{[ii,ii]} is Relation-like Function-like non empty set
{{[ii,ii],aa},{[ii,ii]}} is non empty set
union ii is set
union ii is set
[:(union ii),(union ii):] is Relation-like set
bool [:(union ii),(union ii):] is non empty set
[[ii,ii],aa] `1 is set
X is set
(X) is non empty set
(X) is non empty set
bool X is non empty set
bool (bool X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (bool X) : b<sub>1</sub> is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b<sub>1</sub>),(union b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b<sub>1</sub>),(union b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X) : verum } is set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X), b<sub>3</sub> is Relation-like Function-like Element of (X) : ( ( not union b<sub>2</sub> = {} or union b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like union b<sub>1</sub> -defined union b<sub>2</sub> -valued Function-like quasi_total Element of bool [:(union b<sub>1</sub>),(union b<sub>2</sub>):] & ( for b<sub>4</sub>, b<sub>5</sub> being set holds
( not {b<sub>4</sub>,b<sub>5</sub>} in b<sub>1</sub> or {(b<sub>3</sub> . b<sub>4</sub>),(b<sub>3</sub> . b<sub>5</sub>)} in b<sub>2</sub> ) ) ) } is set
a is Element of (X)
a `2 is Relation-like Function-like set
(X,a) is non empty subset-closed () Element of (X)
a `1 is set
(a `1) `1 is set
(X,a) is non empty subset-closed () Element of (X)
(a `1) `2 is set
aa is Element of (X)
aa `2 is Relation-like Function-like set
(X,aa) is non empty subset-closed () Element of (X)
aa `1 is set
(aa `1) `1 is set
(X,aa) is non empty subset-closed () Element of (X)
(aa `1) `2 is set
[(X,a),(X,a)] is V15() set
{(X,a),(X,a)} is non empty set
{(X,a)} is non empty set
{{(X,a),(X,a)},{(X,a)}} is non empty set
[[(X,a),(X,a)],(a `2)] is V15() set
{[(X,a),(X,a)],(a `2)} is non empty set
{[(X,a),(X,a)]} is Relation-like Function-like non empty set
{{[(X,a),(X,a)],(a `2)},{[(X,a),(X,a)]}} is non empty set
X is set
(X) is non empty set
bool X is non empty set
bool (bool X) is non empty set
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
a is non empty subset-closed () Element of (X)
[a,a] is V15() set
{a,a} is non empty set
{a} is non empty set
{{a,a},{a}} is non empty set
union a is set
id (union a) is Relation-like union a -defined union a -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:(union a),(union a):]
[:(union a),(union a):] is Relation-like set
bool [:(union a),(union a):] is non empty set
[[a,a],(id (union a))] is V15() set
{[a,a],(id (union a))} is non empty set
{[a,a]} is Relation-like Function-like non empty set
{{[a,a],(id (union a))},{[a,a]}} is non empty set
(X) is non empty set
(X) is functional non empty set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is non empty subset-closed () Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not union b₂ = {} or union b₁ = {} ) & b₃ is Relation-like union b₁ -defined union b₂ -valued Function-like quasi_total Element of bool [:(union b₁),(union b₂):] & ( for b₄, b₅ being set holds
( not {b₄,b₅} in b₁ or {(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) ) } is set
ii is set
ii is set
{ii,ii} is non empty set
(id (union a)) . ii is set
(id (union a)) . ii is set
{((id (union a)) . ii),((id (union a)) . ii)} is non empty set
X is set
aa is set
[X,aa] is V15() set
{X,aa} is non empty set
{X} is non empty set
{{X,aa},{X}} is non empty set
ii is set
[[X,aa],ii] is V15() set
{[X,aa],ii} is non empty set
{[X,aa]} is Relation-like Function-like non empty set
{{[X,aa],ii},{[X,aa]}} is non empty set
a is set
ii is set
[a,ii] is V15() set
{a,ii} is non empty set
{a} is non empty set
{{a,ii},{a}} is non empty set
c₆ is set
[[a,ii],c₆] is V15() set
{[a,ii],c₆} is non empty set
{[a,ii]} is Relation-like Function-like non empty set
{{[a,ii],c₆},{[a,ii]}} is non empty set
X is set
(X) is non empty set
(X) is non empty set
bool X is non empty set
bool (bool X) is non empty set
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is non empty subset-closed () Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not union b₂ = {} or union b₁ = {} ) & b₃ is Relation-like union b₁ -defined union b₂ -valued Function-like quasi_total Element of bool [:(union b₁),(union b₂):] & ( for b₄, b₅ being set holds
( not {b₄,b₅} in b₁ or {(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) ) } is set
a is Element of (X)
(X,a) is non empty subset-closed () Element of (X)
a `1 is set
(a `1) `2 is set
union (X,a) is set
(X,a) is non empty subset-closed () Element of (X)
(a `1) `1 is set
union (X,a) is set
a `2 is Relation-like Function-like set
[:(union (X,a)),(union (X,a)):] is Relation-like set
bool [:(union (X,a)),(union (X,a)):] is non empty set
ii is non empty subset-closed () Element of (X)
ii is non empty subset-closed () Element of (X)
[ii,ii] is V15() set
{ii,ii} is non empty set
{ii} is non empty set
{{ii,ii},{ii}} is non empty set
aa is Relation-like Function-like Element of (X)
[[ii,ii],aa] is V15() set
{[ii,ii],aa} is non empty set
{[ii,ii]} is Relation-like Function-like non empty set
{{[ii,ii],aa},{[ii,ii]}} is non empty set
union ii is set
union ii is set
[:(union ii),(union ii):] is Relation-like set
bool [:(union ii),(union ii):] is non empty set
[(X,a),(X,a)] is V15() set
{(X,a),(X,a)} is non empty set
{(X,a)} is non empty set
{{(X,a),(X,a)},{(X,a)}} is non empty set
[[(X,a),(X,a)],(a `2)] is V15() set
{[(X,a),(X,a)],(a `2)} is non empty set
{[(X,a),(X,a)]} is Relation-like Function-like non empty set
{{[(X,a),(X,a)],(a `2)},{[(X,a),(X,a)]}} is non empty set
c<sub>6</sub> is set
(a `2) . c₆ is set
gg is set
{c₆,gg} is non empty set
(a `2) . gg is set
{((a `2) . c₆),((a `2) . gg)} is non empty set
X is set
(X) is non empty set
(X) is non empty set
bool X is non empty set
bool (bool X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (bool X) : b<sub>1</sub> is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b<sub>1</sub>),(union b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b<sub>1</sub>),(union b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X) : verum } is set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X), b<sub>3</sub> is Relation-like Function-like Element of (X) : ( ( not union b<sub>2</sub> = {} or union b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like union b<sub>1</sub> -defined union b<sub>2</sub> -valued Function-like quasi_total Element of bool [:(union b<sub>1</sub>),(union b<sub>2</sub>):] & ( for b<sub>4</sub>, b<sub>5</sub> being set holds
( not {b<sub>4</sub>,b<sub>5</sub>} in b<sub>1</sub> or {(b<sub>3</sub> . b<sub>4</sub>),(b<sub>3</sub> . b<sub>5</sub>)} in b<sub>2</sub> ) ) ) } is set
a is Element of (X)
(X,a) is non empty subset-closed () Element of (X)
a `1 is set
(a `1) `2 is set
aa is Element of (X)
(X,aa) is non empty subset-closed () Element of (X)
aa `1 is set
(aa `1) `1 is set
(X,a) is non empty subset-closed () Element of (X)
(a `1) `1 is set
(X,aa) is non empty subset-closed () Element of (X)
(aa `1) `2 is set
[(X,a),(X,aa)] is V15() set
{(X,a),(X,aa)} is non empty set
{(X,a)} is non empty set
{{(X,a),(X,aa)},{(X,a)}} is non empty set
a `2 is Relation-like Function-like set
aa `2 is Relation-like Function-like set
(a `2) * (aa `2) is Relation-like Function-like set
[[(X,a),(X,aa)],((a `2) * (aa `2))] is V15() set
{[(X,a),(X,aa)],((a `2) * (aa `2))} is non empty set
{[(X,a),(X,aa)]} is Relation-like Function-like non empty set
{{[(X,a),(X,aa)],((a `2) * (aa `2))},{[(X,a),(X,aa)]}} is non empty set
union (X,aa) is set
union (X,aa) is set
union (X,a) is set
union (X,a) is set
[:(union (X,a)),(union (X,a)):] is Relation-like set
bool [:(union (X,a)),(union (X,a)):] is non empty set
ii is set
ii is set
{ii,ii} is non empty set
proj1 (a `2) is set
(a `2) . ii is set
(a `2) . ii is set
{((a `2) . ii),((a `2) . ii)} is non empty set
(aa `2) . ((a `2) . ii) is set
(aa `2) . ((a `2) . ii) is set
{((aa `2) . ((a `2) . ii)),((aa `2) . ((a `2) . ii))} is non empty set
((a `2) * (aa `2)) . ii is set
{(((a `2) * (aa `2)) . ii),((aa `2) . ((a `2) . ii))} is non empty set
((a `2) * (aa `2)) . ii is set
{(((a `2) * (aa `2)) . ii),(((a `2) * (aa `2)) . ii)} is non empty set
[:(union (X,aa)),(union (X,aa)):] is Relation-like set
bool [:(union (X,aa)),(union (X,aa)):] is non empty set
[:(union (X,a)),(union (X,aa)):] is Relation-like set
bool [:(union (X,a)),(union (X,aa)):] is non empty set
X is set
(X) is non empty set
(X) is non empty set
bool X is non empty set
bool (bool X) is non empty set
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is non empty subset-closed () Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not union b₂ = {} or union b₁ = {} ) & b₃ is Relation-like union b₁ -defined union b₂ -valued Function-like quasi_total Element of bool [:(union b₁),(union b₂):] & ( for b₄, b₅ being set holds
( not {b₄,b₅} in b₁ or {(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) ) } is set
a is Element of (X)
(X,a) is non empty subset-closed () Element of (X)
a `1 is set
(a `1) `1 is set
a `2 is Relation-like Function-like set
(X,a) is non empty subset-closed () Element of (X)
(a `1) `2 is set
aa is Element of (X)
(X,aa) is non empty subset-closed () Element of (X)
aa `1 is set
(aa `1) `2 is set
(X,aa,a) is Element of (X)
(X,aa,a) `2 is Relation-like Function-like set
aa `2 is Relation-like Function-like set
(aa `2) * (a `2) is Relation-like Function-like set
(X,(X,aa,a)) is non empty subset-closed () Element of (X)
(X,aa,a) `1 is set
((X,aa,a) `1) `1 is set
(X,aa) is non empty subset-closed () Element of (X)
(aa `1) `1 is set
(X,(X,aa,a)) is non empty subset-closed () Element of (X)
((X,aa,a) `1) `2 is set
[(X,aa),(X,a)] is V15() set
{(X,aa),(X,a)} is non empty set
{(X,aa)} is non empty set
{{(X,aa),(X,a)},{(X,aa)}} is non empty set
[[(X,aa),(X,a)],((aa `2) * (a `2))] is V15() set
{[(X,aa),(X,a)],((aa `2) * (a `2))} is non empty set
{[(X,aa),(X,a)]} is Relation-like Function-like non empty set
{{[(X,aa),(X,a)],((aa `2) * (a `2))},{[(X,aa),(X,a)]}} is non empty set
[(X,(X,aa,a)),(X,(X,aa,a))] is V15() set
{(X,(X,aa,a)),(X,(X,aa,a))} is non empty set
{(X,(X,aa,a))} is non empty set
{{(X,(X,aa,a)),(X,(X,aa,a))},{(X,(X,aa,a))}} is non empty set
[[(X,(X,aa,a)),(X,(X,aa,a))],((X,aa,a) `2)] is V15() set
{[(X,(X,aa,a)),(X,(X,aa,a))],((X,aa,a) `2)} is non empty set
{[(X,(X,aa,a)),(X,(X,aa,a))]} is Relation-like Function-like non empty set
{{[(X,(X,aa,a)),(X,(X,aa,a))],((X,aa,a) `2)},{[(X,(X,aa,a)),(X,(X,aa,a))]}} is non empty set
X is set
(X) is non empty set
(X) is non empty set
bool X is non empty set
bool (bool X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (bool X) : b<sub>1</sub> is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b<sub>1</sub>),(union b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b<sub>1</sub>),(union b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X) : verum } is set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X), b<sub>3</sub> is Relation-like Function-like Element of (X) : ( ( not union b<sub>2</sub> = {} or union b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like union b<sub>1</sub> -defined union b<sub>2</sub> -valued Function-like quasi_total Element of bool [:(union b<sub>1</sub>),(union b<sub>2</sub>):] & ( for b<sub>4</sub>, b<sub>5</sub> being set holds
( not {b<sub>4</sub>,b<sub>5</sub>} in b<sub>1</sub> or {(b<sub>3</sub> . b<sub>4</sub>),(b<sub>3</sub> . b<sub>5</sub>)} in b<sub>2</sub> ) ) ) } is set
a is Element of (X)
(X,a) is non empty subset-closed () Element of (X)
a `1 is set
(a `1) `1 is set
(X,a) is non empty subset-closed () Element of (X)
(a `1) `2 is set
aa is Element of (X)
(X,aa) is non empty subset-closed () Element of (X)
aa `1 is set
(aa `1) `2 is set
(X,aa,a) is Element of (X)
ii is Element of (X)
(X,ii) is non empty subset-closed () Element of (X)
ii `1 is set
(ii `1) `1 is set
(X,(X,aa,a),ii) is Element of (X)
(X,a,ii) is Element of (X)
(X,aa,(X,a,ii)) is Element of (X)
(X,(X,aa,a)) is non empty subset-closed () Element of (X)
(X,aa,a) `1 is set
((X,aa,a) `1) `2 is set
(X,aa,a) `2 is Relation-like Function-like set
aa `2 is Relation-like Function-like set
a `2 is Relation-like Function-like set
(aa `2) * (a `2) is Relation-like Function-like set
(X,(X,aa,a),ii) `2 is Relation-like Function-like set
ii `2 is Relation-like Function-like set
((aa `2) * (a `2)) * (ii `2) is Relation-like Function-like set
(X,(X,a,ii)) is non empty subset-closed () Element of (X)
(X,a,ii) `1 is set
((X,a,ii) `1) `1 is set
(X,(X,aa,(X,a,ii))) is non empty subset-closed () Element of (X)
(X,aa,(X,a,ii)) `1 is set
((X,aa,(X,a,ii)) `1) `1 is set
(X,aa) is non empty subset-closed () Element of (X)
(aa `1) `1 is set
(X,(X,aa,a)) is non empty subset-closed () Element of (X)
((X,aa,a) `1) `1 is set
(X,(X,(X,aa,a),ii)) is non empty subset-closed () Element of (X)
(X,(X,aa,a),ii) `1 is set
((X,(X,aa,a),ii) `1) `1 is set
(X,(X,a,ii)) is non empty subset-closed () Element of (X)
((X,a,ii) `1) `2 is set
(X,ii) is non empty subset-closed () Element of (X)
(ii `1) `2 is set
(X,(X,aa,(X,a,ii))) is non empty subset-closed () Element of (X)
((X,aa,(X,a,ii)) `1) `2 is set
(X,a,ii) `2 is Relation-like Function-like set
(a `2) * (ii `2) is Relation-like Function-like set
(X,aa,(X,a,ii)) `2 is Relation-like Function-like set
(aa `2) * ((a `2) * (ii `2)) is Relation-like Function-like set
(X,(X,(X,aa,a),ii)) is non empty subset-closed () Element of (X)
((X,(X,aa,a),ii) `1) `2 is set
X is set
(X) is non empty set
bool X is non empty set
bool (bool X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (bool X) : b<sub>1</sub> is non empty subset-closed () set } is set
a is non empty subset-closed () Element of (X)
(X,a) is Element of (X)
(X) is non empty set
(X) is functional non empty set
{ (Funcs ((union b<sub>1</sub>),(union b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b<sub>1</sub>),(union b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X) : verum } is set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X), b<sub>3</sub> is Relation-like Function-like Element of (X) : ( ( not union b<sub>2</sub> = {} or union b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like union b<sub>1</sub> -defined union b<sub>2</sub> -valued Function-like quasi_total Element of bool [:(union b<sub>1</sub>),(union b<sub>2</sub>):] & ( for b<sub>4</sub>, b<sub>5</sub> being set holds
( not {b<sub>4</sub>,b<sub>5</sub>} in b<sub>1</sub> or {(b<sub>3</sub> . b<sub>4</sub>),(b<sub>3</sub> . b<sub>5</sub>)} in b<sub>2</sub> ) ) ) } is set
[a,a] is V15() set
{a,a} is non empty set
{a} is non empty set
{{a,a},{a}} is non empty set
union a is set
id (union a) is Relation-like union a -defined union a -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:(union a),(union a):]
[:(union a),(union a):] is Relation-like set
bool [:(union a),(union a):] is non empty set
[[a,a],(id (union a))] is V15() set
{[a,a],(id (union a))} is non empty set
{[a,a]} is Relation-like Function-like non empty set
{{[a,a],(id (union a))},{[a,a]}} is non empty set
(X,a) `2 is Relation-like Function-like set
(X,(X,a)) is non empty subset-closed () Element of (X)
(X,a) `1 is set
((X,a) `1) `1 is set
(X,(X,a)) is non empty subset-closed () Element of (X)
((X,a) `1) `2 is set
[(X,(X,a)),(X,(X,a))] is V15() set
{(X,(X,a)),(X,(X,a))} is non empty set
{(X,(X,a))} is non empty set
{{(X,(X,a)),(X,(X,a))},{(X,(X,a))}} is non empty set
[[(X,(X,a)),(X,(X,a))],((X,a) `2)] is V15() set
{[(X,(X,a)),(X,(X,a))],((X,a) `2)} is non empty set
{[(X,(X,a)),(X,(X,a))]} is Relation-like Function-like non empty set
{{[(X,(X,a)),(X,(X,a))],((X,a) `2)},{[(X,(X,a)),(X,(X,a))]}} is non empty set
X is set
(X) is non empty set
(X) is non empty set
bool X is non empty set
bool (bool X) is non empty set
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is non empty subset-closed () Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not union b₂ = {} or union b₁ = {} ) & b₃ is Relation-like union b₁ -defined union b₂ -valued Function-like quasi_total Element of bool [:(union b₁),(union b₂):] & ( for b₄, b₅ being set holds
( not {b₄,b₅} in b₁ or {(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) ) } is set
a is Element of (X)
(X,a) is non empty subset-closed () Element of (X)
a `1 is set
(a `1) `1 is set
(X,(X,a)) is Element of (X)
[(X,a),(X,a)] is V15() set
{(X,a),(X,a)} is non empty set
{(X,a)} is non empty set
{{(X,a),(X,a)},{(X,a)}} is non empty set
union (X,a) is set
id (union (X,a)) is Relation-like union (X,a) -defined union (X,a) -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:(union (X,a)),(union (X,a)):]
[:(union (X,a)),(union (X,a)):] is Relation-like set
bool [:(union (X,a)),(union (X,a)):] is non empty set
[[(X,a),(X,a)],(id (union (X,a)))] is V15() set
{[(X,a),(X,a)],(id (union (X,a)))} is non empty set
{[(X,a),(X,a)]} is Relation-like Function-like non empty set
{{[(X,a),(X,a)],(id (union (X,a)))},{[(X,a),(X,a)]}} is non empty set
(X,(X,(X,a)),a) is Element of (X)
(X,a) is non empty subset-closed () Element of (X)
(a `1) `2 is set
(X,(X,a)) is Element of (X)
[(X,a),(X,a)] is V15() set
{(X,a),(X,a)} is non empty set
{(X,a)} is non empty set
{{(X,a),(X,a)},{(X,a)}} is non empty set
union (X,a) is set
id (union (X,a)) is Relation-like union (X,a) -defined union (X,a) -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:(union (X,a)),(union (X,a)):]
[:(union (X,a)),(union (X,a)):] is Relation-like set
bool [:(union (X,a)),(union (X,a)):] is non empty set
[[(X,a),(X,a)],(id (union (X,a)))] is V15() set
{[(X,a),(X,a)],(id (union (X,a)))} is non empty set
{[(X,a),(X,a)]} is Relation-like Function-like non empty set
{{[(X,a),(X,a)],(id (union (X,a)))},{[(X,a),(X,a)]}} is non empty set
(X,a,(X,(X,a))) is Element of (X)
(X,(X,a)) `2 is Relation-like Function-like set
(X,(X,(X,a))) is non empty subset-closed () Element of (X)
(X,(X,a)) `1 is set
((X,(X,a)) `1) `1 is set
a `2 is Relation-like Function-like set
[:(union (X,a)),(union (X,a)):] is Relation-like set
bool [:(union (X,a)),(union (X,a)):] is non empty set
proj2 (a `2) is set
proj1 (a `2) is set
(X,(X,(X,a))) is non empty subset-closed () Element of (X)
((X,(X,a)) `1) `2 is set
(X,(X,(X,(X,a)),a)) is non empty subset-closed () Element of (X)
(X,(X,(X,a)),a) `1 is set
((X,(X,(X,a)),a) `1) `2 is set
(X,(X,(X,a)),a) `2 is Relation-like Function-like set
((X,(X,a)) `2) * (a `2) is Relation-like Function-like set
(X,(X,(X,(X,a)),a)) is non empty subset-closed () Element of (X)
((X,(X,(X,a)),a) `1) `1 is set
(X,(X,a)) `2 is Relation-like Function-like set
(X,(X,(X,a))) is non empty subset-closed () Element of (X)
(X,(X,a)) `1 is set
((X,(X,a)) `1) `2 is set
(X,(X,(X,a))) is non empty subset-closed () Element of (X)
((X,(X,a)) `1) `1 is set
(X,(X,a,(X,(X,a)))) is non empty subset-closed () Element of (X)
(X,a,(X,(X,a))) `1 is set
((X,a,(X,(X,a))) `1) `2 is set
(X,a,(X,(X,a))) `2 is Relation-like Function-like set
(a `2) * ((X,(X,a)) `2) is Relation-like Function-like set
(X,(X,a,(X,(X,a)))) is non empty subset-closed () Element of (X)
((X,a,(X,(X,a))) `1) `1 is set
X is set
(X) is non empty set
(X) is non empty set
bool X is non empty set
bool (bool X) is non empty set
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
(X) is functional non empty set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is non empty subset-closed () Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not union b₂ = {} or union b₁ = {} ) & b₃ is Relation-like union b₁ -defined union b₂ -valued Function-like quasi_total Element of bool [:(union b₁),(union b₂):] & ( for b₄, b₅ being set holds
( not {b₄,b₅} in b₁ or {(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) ) } is set
[:(X),(X):] is Relation-like non empty set
bool [:(X),(X):] is non empty set
a is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]
aa is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]
ii is Element of (X)
a . ii is non empty subset-closed () Element of (X)
(X,ii) is non empty subset-closed () Element of (X)
ii `1 is set
(ii `1) `1 is set
aa . ii is non empty subset-closed () Element of (X)
a is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]
aa is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]
ii is Element of (X)
a . ii is non empty subset-closed () Element of (X)
(X,ii) is non empty subset-closed () Element of (X)
ii `1 is set
(ii `1) `2 is set
aa . ii is non empty subset-closed () Element of (X)
[:(X),(X):] is Relation-like non empty set
[:[:(X),(X):],(X):] is Relation-like non empty set
bool [:[:(X),(X):],(X):] is non empty set
a is set
aa is set
ii is set
ii is set
gg is Element of (X)
c₆ is Element of (X)
(X,gg,c₆) is Element of (X)
a is set
aa is set
ii is set
c₆ is Element of (X)
ii is Element of (X)
(X,c₆,ii) is Element of (X)
a is Relation-like [:(X),(X):] -defined (X) -valued Function-like Element of bool [:[:(X),(X):],(X):]
dom a is Relation-like (X) -defined (X) -valued Element of bool [:(X),(X):]
bool [:(X),(X):] is non empty set
aa is Element of (X)
(X,aa) is non empty subset-closed () Element of (X)
aa `1 is set
(aa `1) `1 is set
ii is Element of (X)
[aa,ii] is V15() set
{aa,ii} is non empty set
{aa} is non empty set
{{aa,ii},{aa}} is non empty set
(X,ii) is non empty subset-closed () Element of (X)
ii `1 is set
(ii `1) `2 is set
ii is set
(X,ii,aa) is Element of (X)
ii is Element of (X)
c₆ is Element of (X)
(X,ii) is non empty subset-closed () Element of (X)
ii `1 is set
(ii `1) `1 is set
(X,c<sub>6</sub>) is non empty subset-closed () Element of (X)
c<sub>6</sub> `1 is set
(c₆ `1) `2 is set
(X,c₆,ii) is Element of (X)
aa is Element of (X)
(X,aa) is non empty subset-closed () Element of (X)
aa `1 is set
(aa `1) `1 is set
ii is Element of (X)
(X,ii) is non empty subset-closed () Element of (X)
ii `1 is set
(ii `1) `2 is set
[aa,ii] is V15() set
{aa,ii} is non empty set
{aa} is non empty set
{{aa,ii},{aa}} is non empty set
a . [aa,ii] is set
(X,ii,aa) is Element of (X)
a . (aa,ii) is set
ii is Element of (X)
c₆ is Element of (X)
(X,ii) is non empty subset-closed () Element of (X)
ii `1 is set
(ii `1) `1 is set
(X,c<sub>6</sub>) is non empty subset-closed () Element of (X)
c<sub>6</sub> `1 is set
(c₆ `1) `2 is set
(X,c₆,ii) is Element of (X)
a is Relation-like [:(X),(X):] -defined (X) -valued Function-like Element of bool [:[:(X),(X):],(X):]
dom a is Relation-like (X) -defined (X) -valued Element of bool [:(X),(X):]
bool [:(X),(X):] is non empty set
aa is Relation-like [:(X),(X):] -defined (X) -valued Function-like Element of bool [:[:(X),(X):],(X):]
dom aa is Relation-like (X) -defined (X) -valued Element of bool [:(X),(X):]
ii is set
ii is set
[ii,ii] is V15() set
{ii,ii} is non empty set
{ii} is non empty set
{{ii,ii},{ii}} is non empty set
c₆ is Element of (X)
(X,c₆) is non empty subset-closed () Element of (X)
c₆ `1 is set
(c<sub>6</sub> `1) `1 is set
gg is Element of (X)
(X,gg) is non empty subset-closed () Element of (X)
gg `1 is set
(gg `1) `2 is set
c₆ is Element of (X)
(X,c₆) is non empty subset-closed () Element of (X)
c₆ `1 is set
(c<sub>6</sub> `1) `1 is set
gg is Element of (X)
(X,gg) is non empty subset-closed () Element of (X)
gg `1 is set
(gg `1) `2 is set
ii is Element of [:(X),(X):]
ii is Element of (X)
c₆ is Element of (X)
[ii,c₆] is V15() set
{ii,c₆} is non empty set
{ii} is non empty set
{{ii,c₆},{ii}} is non empty set
(X,ii) is non empty subset-closed () Element of (X)
ii `1 is set
(ii `1) `1 is set
(X,c<sub>6</sub>) is non empty subset-closed () Element of (X)
c<sub>6</sub> `1 is set
(c₆ `1) `2 is set
a . [ii,c₆] is set
(X,c₆,ii) is Element of (X)
a . ii is set
aa . ii is set
X is set
(X) is non empty set
bool X is non empty set
bool (bool X) is non empty set
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
(X) is non empty set
(X) is functional non empty set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is non empty subset-closed () Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not union b₂ = {} or union b₁ = {} ) & b₃ is Relation-like union b₁ -defined union b₂ -valued Function-like quasi_total Element of bool [:(union b₁),(union b₂):] & ( for b₄, b₅ being set holds
( not {b₄,b₅} in b₁ or {(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) ) } is set
(X) is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]
[:(X),(X):] is Relation-like non empty set
bool [:(X),(X):] is non empty set
(X) is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]
(X) is Relation-like [:(X),(X):] -defined (X) -valued Function-like Element of bool [:[:(X),(X):],(X):]
[:(X),(X):] is Relation-like non empty set
[:[:(X),(X):],(X):] is Relation-like non empty set
bool [:[:(X),(X):],(X):] is non empty set
CatStr(# (X),(X),(X),(X),(X) #) is non empty non void strict CatStr
X is set
(X) is non empty non void strict CatStr
(X) is non empty set
bool X is non empty set
bool (bool X) is non empty set
{ b₁ where b₁ is Element of bool (bool X) : b₁ is non empty subset-closed () set } is set
(X) is non empty set
(X) is functional non empty set
{ (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b₁),(union b₂))) where b₁, b₂ is non empty subset-closed () Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is non empty subset-closed () Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not union b₂ = {} or union b₁ = {} ) & b₃ is Relation-like union b₁ -defined union b₂ -valued Function-like quasi_total Element of bool [:(union b₁),(union b₂):] & ( for b₄, b₅ being set holds
( not {b₄,b₅} in b₁ or {(b₃ . b₄),(b₃ . b₅)} in b₂ ) ) ) } is set
(X) is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]
[:(X),(X):] is Relation-like non empty set
bool [:(X),(X):] is non empty set
(X) is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]
(X) is Relation-like [:(X),(X):] -defined (X) -valued Function-like Element of bool [:[:(X),(X):],(X):]
[:(X),(X):] is Relation-like non empty set
[:[:(X),(X):],(X):] is Relation-like non empty set
bool [:[:(X),(X):],(X):] is non empty set
CatStr(# (X),(X),(X),(X),(X) #) is non empty non void strict CatStr
the carrier' of (X) is set
aa is Element of the carrier' of (X)
gg is Element of the carrier' of (X)
[aa,gg] is V15() set
{aa,gg} is non empty set
{aa} is non empty set
{{aa,gg},{aa}} is non empty set
the Comp of (X) is Relation-like [: the carrier' of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like Element of bool [:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):]
[: the carrier' of (X), the carrier' of (X):] is Relation-like set
[:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):] is Relation-like set
bool [:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):] is non empty set
proj1 the Comp of (X) is Relation-like set
dom aa is Element of the carrier of (X)
the carrier of (X) is set
the Source of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
[: the carrier' of (X), the carrier of (X):] is Relation-like set
bool [: the carrier' of (X), the carrier of (X):] is non empty set
the Source of (X) . aa is Element of the carrier of (X)
cod gg is Element of the carrier of (X)
the Target of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
the Target of (X) . gg is Element of the carrier of (X)
(X) . aa is set
f is Element of (X)
(X,f) is non empty subset-closed () Element of (X)
f `1 is set
(f `1) `1 is set
(X) . gg is set
ii is Element of (X)
(X,ii) is non empty subset-closed () Element of (X)
ii `1 is set
(ii `1) `2 is set
the carrier' of (X) is set
aa is Element of the carrier' of (X)
dom aa is Element of the carrier of (X)
the carrier of (X) is set
the Source of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
[: the carrier' of (X), the carrier of (X):] is Relation-like set
bool [: the carrier' of (X), the carrier of (X):] is non empty set
the Source of (X) . aa is Element of the carrier of (X)
gg is Element of the carrier' of (X)
cod gg is Element of the carrier of (X)
the Target of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
the Target of (X) . gg is Element of the carrier of (X)
aa (*) gg is Element of the carrier' of (X)
dom (aa (*) gg) is Element of the carrier of (X)
the Source of (X) . (aa (*) gg) is Element of the carrier of (X)
dom gg is Element of the carrier of (X)
the Source of (X) . gg is Element of the carrier of (X)
cod (aa (*) gg) is Element of the carrier of (X)
the Target of (X) . (aa (*) gg) is Element of the carrier of (X)
cod aa is Element of the carrier of (X)
the Target of (X) . aa is Element of the carrier of (X)
[aa,gg] is V15() set
{aa,gg} is non empty set
{aa} is non empty set
{{aa,gg},{aa}} is non empty set
[: the carrier' of (X), the carrier' of (X):] is Relation-like set
the Comp of (X) is Relation-like [: the carrier' of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like Element of bool [:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):]
[:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):] is Relation-like set
bool [:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):] is non empty set
dom the Comp of (X) is Relation-like the carrier' of (X) -defined the carrier' of (X) -valued Element of bool [: the carrier' of (X), the carrier' of (X):]
bool [: the carrier' of (X), the carrier' of (X):] is non empty set
the Comp of (X) . (aa,gg) is set
the Comp of (X) . [aa,gg] is set
f is Element of (X)
(X) . f is non empty subset-closed () Element of (X)
(X,f) is non empty subset-closed () Element of (X)
f `1 is set
(f `1) `1 is set
ii is Element of (X)
(X) . ii is non empty subset-closed () Element of (X)
(X,ii) is non empty subset-closed () Element of (X)
ii `1 is set
(ii `1) `2 is set
[f,ii] is V15() set
{f,ii} is non empty set
{f} is non empty set
{{f,ii},{f}} is non empty set
(X) . [f,ii] is set
(X,ii,f) is Element of (X)
(X) . ii is non empty subset-closed () Element of (X)
(X,ii) is non empty subset-closed () Element of (X)
(ii `1) `1 is set
(X) . f is non empty subset-closed () Element of (X)
(X,f) is non empty subset-closed () Element of (X)
(f `1) `2 is set
(X,(X,ii,f)) is non empty subset-closed () Element of (X)
(X,ii,f) `1 is set
((X,ii,f) `1) `1 is set
(X,(X,ii,f)) is non empty subset-closed () Element of (X)
((X,ii,f) `1) `2 is set
the carrier' of (X) is set
ii is Element of the carrier' of (X)
dom ii is Element of the carrier of (X)
the carrier of (X) is set
the Source of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
[: the carrier' of (X), the carrier of (X):] is Relation-like set
bool [: the carrier' of (X), the carrier of (X):] is non empty set
the Source of (X) . ii is Element of the carrier of (X)
aa is Element of the carrier' of (X)
cod aa is Element of the carrier of (X)
the Target of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
the Target of (X) . aa is Element of the carrier of (X)
dom aa is Element of the carrier of (X)
the Source of (X) . aa is Element of the carrier of (X)
gg is Element of the carrier' of (X)
cod gg is Element of the carrier of (X)
the Target of (X) . gg is Element of the carrier of (X)
aa (*) gg is Element of the carrier' of (X)
ii (*) (aa (*) gg) is Element of the carrier' of (X)
ii (*) aa is Element of the carrier' of (X)
(ii (*) aa) (*) gg is Element of the carrier' of (X)
h is Element of (X)
(X,h) is non empty subset-closed () Element of (X)
h `1 is set
(h `1) `1 is set
(X) . h is non empty subset-closed () Element of (X)
g is Element of (X)
(X,g) is non empty subset-closed () Element of (X)
g `1 is set
(g `1) `2 is set
(X) . g is non empty subset-closed () Element of (X)
(X,g,h) is Element of (X)
(X,(X,g,h)) is non empty subset-closed () Element of (X)
(X,g,h) `1 is set
((X,g,h) `1) `1 is set
(X,g) is non empty subset-closed () Element of (X)
(g `1) `1 is set
(X) . g is non empty subset-closed () Element of (X)
f is Element of (X)
(X,f) is non empty subset-closed () Element of (X)
f `1 is set
(f `1) `2 is set
(X) . f is non empty subset-closed () Element of (X)
(X,f,g) is Element of (X)
(X,(X,f,g)) is non empty subset-closed () Element of (X)
(X,f,g) `1 is set
((X,f,g) `1) `2 is set
[ii,aa] is V15() set
{ii,aa} is non empty set
{ii} is non empty set
{{ii,aa},{ii}} is non empty set
[: the carrier' of (X), the carrier' of (X):] is Relation-like set
the Comp of (X) is Relation-like [: the carrier' of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like Element of bool [:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):]
[:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):] is Relation-like set
bool [:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):] is non empty set
dom the Comp of (X) is Relation-like the carrier' of (X) -defined the carrier' of (X) -valued Element of bool [: the carrier' of (X), the carrier' of (X):]
bool [: the carrier' of (X), the carrier' of (X):] is non empty set
the Comp of (X) . (ii,aa) is set
the Comp of (X) . [ii,aa] is set
dom (ii (*) aa) is Element of the carrier of (X)
the Source of (X) . (ii (*) aa) is Element of the carrier of (X)
[(ii (*) aa),gg] is V15() set
{(ii (*) aa),gg} is non empty set
{(ii (*) aa)} is non empty set
{{(ii (*) aa),gg},{(ii (*) aa)}} is non empty set
[aa,gg] is V15() set
{aa,gg} is non empty set
{aa} is non empty set
{{aa,gg},{aa}} is non empty set
the Comp of (X) . (aa,gg) is set
the Comp of (X) . [aa,gg] is set
cod (aa (*) gg) is Element of the carrier of (X)
the Target of (X) . (aa (*) gg) is Element of the carrier of (X)
[ii,(aa (*) gg)] is V15() set
{ii,(aa (*) gg)} is non empty set
{{ii,(aa (*) gg)},{ii}} is non empty set
the Comp of (X) . (ii,( the Comp of (X) . (aa,gg))) is set
[ii,( the Comp of (X) . (aa,gg))] is V15() set
{ii,( the Comp of (X) . (aa,gg))} is non empty set
{{ii,( the Comp of (X) . (aa,gg))},{ii}} is non empty set
the Comp of (X) . [ii,( the Comp of (X) . (aa,gg))] is set
[h,(X,f,g)] is V15() set
{h,(X,f,g)} is non empty set
{h} is non empty set
{{h,(X,f,g)},{h}} is non empty set
(X) . [h,(X,f,g)] is set
(X,(X,f,g),h) is Element of (X)
(X,f,(X,g,h)) is Element of (X)
[(X,g,h),f] is V15() set
{(X,g,h),f} is non empty set
{(X,g,h)} is non empty set
{{(X,g,h),f},{(X,g,h)}} is non empty set
(X) . [(X,g,h),f] is set
the Comp of (X) . (( the Comp of (X) . (ii,aa)),gg) is set
[( the Comp of (X) . (ii,aa)),gg] is V15() set
{( the Comp of (X) . (ii,aa)),gg} is non empty set
{( the Comp of (X) . (ii,aa))} is non empty set
{{( the Comp of (X) . (ii,aa)),gg},{( the Comp of (X) . (ii,aa))}} is non empty set
the Comp of (X) . [( the Comp of (X) . (ii,aa)),gg] is set
the carrier of (X) is set
gg is Element of the carrier of (X)
Hom (gg,gg) is Element of bool the carrier' of (X)
the carrier' of (X) is set
bool the carrier' of (X) is non empty set
{ b₁ where b₁ is Element of the carrier' of (X) : ( dom b₁ = gg & cod b₁ = gg ) } is set
aa is non empty subset-closed () Element of (X)
(X,aa) is Element of (X)
[aa,aa] is V15() set
{aa,aa} is non empty set
{aa} is non empty set
{{aa,aa},{aa}} is non empty set
union aa is set
id (union aa) is Relation-like union aa -defined union aa -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:(union aa),(union aa):]
[:(union aa),(union aa):] is Relation-like set
bool [:(union aa),(union aa):] is non empty set
[[aa,aa],(id (union aa))] is V15() set
{[aa,aa],(id (union aa))} is non empty set
{[aa,aa]} is Relation-like Function-like non empty set
{{[aa,aa],(id (union aa))},{[aa,aa]}} is non empty set
ii is Element of the carrier' of (X)
cod ii is Element of the carrier of (X)
the Target of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
[: the carrier' of (X), the carrier of (X):] is Relation-like set
bool [: the carrier' of (X), the carrier of (X):] is non empty set
the Target of (X) . ii is Element of the carrier of (X)
(X,(X,aa)) is non empty subset-closed () Element of (X)
(X,aa) `1 is set
((X,aa) `1) `2 is set
dom ii is Element of the carrier of (X)
the Source of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
the Source of (X) . ii is Element of the carrier of (X)
(X,(X,aa)) is non empty subset-closed () Element of (X)
((X,aa) `1) `1 is set
X is set
(X) is non empty non void strict Category-like transitive associative reflexive CatStr
(X) is non empty set
bool X is non empty set
bool (bool X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (bool X) : b<sub>1</sub> is non empty subset-closed () set } is set
(X) is non empty set
(X) is functional non empty set
{ (Funcs ((union b<sub>1</sub>),(union b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b<sub>1</sub>),(union b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X) : verum } is set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X), b<sub>3</sub> is Relation-like Function-like Element of (X) : ( ( not union b<sub>2</sub> = {} or union b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like union b<sub>1</sub> -defined union b<sub>2</sub> -valued Function-like quasi_total Element of bool [:(union b<sub>1</sub>),(union b<sub>2</sub>):] & ( for b<sub>4</sub>, b<sub>5</sub> being set holds
( not {b<sub>4</sub>,b<sub>5</sub>} in b<sub>1</sub> or {(b<sub>3</sub> . b<sub>4</sub>),(b<sub>3</sub> . b<sub>5</sub>)} in b<sub>2</sub> ) ) ) } is set
(X) is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]
[:(X),(X):] is Relation-like non empty set
bool [:(X),(X):] is non empty set
(X) is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]
(X) is Relation-like [:(X),(X):] -defined (X) -valued Function-like Element of bool [:[:(X),(X):],(X):]
[:(X),(X):] is Relation-like non empty set
[:[:(X),(X):],(X):] is Relation-like non empty set
bool [:[:(X),(X):],(X):] is non empty set
CatStr(# (X),(X),(X),(X),(X) #) is non empty non void strict CatStr
the carrier of (X) is set
a is Element of the carrier of (X)
aa is non empty subset-closed () Element of (X)
(X,aa) is Element of (X)
[aa,aa] is V15() set
{aa,aa} is non empty set
{aa} is non empty set
{{aa,aa},{aa}} is non empty set
union aa is set
id (union aa) is Relation-like union aa -defined union aa -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:(union aa),(union aa):]
[:(union aa),(union aa):] is Relation-like set
bool [:(union aa),(union aa):] is non empty set
[[aa,aa],(id (union aa))] is V15() set
{[aa,aa],(id (union aa))} is non empty set
{[aa,aa]} is Relation-like Function-like non empty set
{{[aa,aa],(id (union aa))},{[aa,aa]}} is non empty set
ii is Morphism of a,a
ii is Element of the carrier of (X)
Hom (a,ii) is Element of bool the carrier' of (X)
the carrier' of (X) is set
bool the carrier' of (X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier' of (X) : ( dom b<sub>1</sub> = a & cod b<sub>1</sub> = ii ) } is set
Hom (ii,a) is Element of bool the carrier' of (X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier' of (X) : ( dom b<sub>1</sub> = ii & cod b<sub>1</sub> = a ) } is set
c<sub>6</sub> is Morphism of a,ii
c<sub>6</sub> (*) ii is Element of the carrier' of (X)
Hom (a,a) is non empty Element of bool the carrier' of (X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier' of (X) : ( dom b<sub>1</sub> = a & cod b<sub>1</sub> = a ) } is set
cod ii is Element of the carrier of (X)
the Target of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
[: the carrier' of (X), the carrier of (X):] is Relation-like set
bool [: the carrier' of (X), the carrier of (X):] is non empty set
the Target of (X) . ii is Element of the carrier of (X)
dom c<sub>6</sub> is Element of the carrier of (X)
the Source of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
the Source of (X) . c<sub>6</sub> is Element of the carrier of (X)
gg is Element of (X)
(X,gg) is non empty subset-closed () Element of (X)
gg `1 is set
(gg `1) `1 is set
(X,(X,aa)) is non empty subset-closed () Element of (X)
(X,aa) `1 is set
((X,aa) `1) `2 is set
[c<sub>6</sub>,ii] is V15() set
{c<sub>6</sub>,ii} is non empty set
{c<sub>6</sub>} is non empty set
{{c<sub>6</sub>,ii},{c<sub>6</sub>}} is non empty set
[: the carrier' of (X), the carrier' of (X):] is Relation-like set
the Comp of (X) is Relation-like [: the carrier' of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like Element of bool [:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):]
[:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):] is Relation-like set
bool [:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):] is non empty set
dom the Comp of (X) is Relation-like the carrier' of (X) -defined the carrier' of (X) -valued Element of bool [: the carrier' of (X), the carrier' of (X):]
bool [: the carrier' of (X), the carrier' of (X):] is non empty set
the Comp of (X) . (c<sub>6</sub>,ii) is set
the Comp of (X) . [c<sub>6</sub>,ii] is set
(X,(X,aa),gg) is Element of (X)
c<sub>6</sub> is Morphism of ii,a
ii (*) c<sub>6</sub> is Element of the carrier' of (X)
Hom (a,a) is non empty Element of bool the carrier' of (X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier' of (X) : ( dom b<sub>1</sub> = a & cod b<sub>1</sub> = a ) } is set
dom ii is Element of the carrier of (X)
the Source of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
[: the carrier' of (X), the carrier of (X):] is Relation-like set
bool [: the carrier' of (X), the carrier of (X):] is non empty set
the Source of (X) . ii is Element of the carrier of (X)
cod c<sub>6</sub> is Element of the carrier of (X)
the Target of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
the Target of (X) . c<sub>6</sub> is Element of the carrier of (X)
gg is Element of (X)
(X,gg) is non empty subset-closed () Element of (X)
gg `1 is set
(gg `1) `2 is set
(X,(X,aa)) is non empty subset-closed () Element of (X)
(X,aa) `1 is set
((X,aa) `1) `1 is set
[ii,c<sub>6</sub>] is V15() set
{ii,c<sub>6</sub>} is non empty set
{ii} is non empty set
{{ii,c<sub>6</sub>},{ii}} is non empty set
[: the carrier' of (X), the carrier' of (X):] is Relation-like set
the Comp of (X) is Relation-like [: the carrier' of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like Element of bool [:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):]
[:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):] is Relation-like set
bool [:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):] is non empty set
dom the Comp of (X) is Relation-like the carrier' of (X) -defined the carrier' of (X) -valued Element of bool [: the carrier' of (X), the carrier' of (X):]
bool [: the carrier' of (X), the carrier' of (X):] is non empty set
the Comp of (X) . (ii,c<sub>6</sub>) is set
the Comp of (X) . [ii,c<sub>6</sub>] is set
(X,gg,(X,aa)) is Element of (X)
X is set
(X) is non empty non void strict Category-like transitive associative reflexive CatStr
(X) is non empty set
bool X is non empty set
bool (bool X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (bool X) : b<sub>1</sub> is non empty subset-closed () set } is set
(X) is non empty set
(X) is functional non empty set
{ (Funcs ((union b<sub>1</sub>),(union b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X) : verum } is set
union { (Funcs ((union b<sub>1</sub>),(union b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X) : verum } is set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is non empty subset-closed () Element of (X), b<sub>3</sub> is Relation-like Function-like Element of (X) : ( ( not union b<sub>2</sub> = {} or union b<sub>1</sub> = {} ) & b<sub>3</sub> is Relation-like union b<sub>1</sub> -defined union b<sub>2</sub> -valued Function-like quasi_total Element of bool [:(union b<sub>1</sub>),(union b<sub>2</sub>):] & ( for b<sub>4</sub>, b<sub>5</sub> being set holds
( not {b<sub>4</sub>,b<sub>5</sub>} in b<sub>1</sub> or {(b<sub>3</sub> . b<sub>4</sub>),(b<sub>3</sub> . b<sub>5</sub>)} in b<sub>2</sub> ) ) ) } is set
(X) is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]
[:(X),(X):] is Relation-like non empty set
bool [:(X),(X):] is non empty set
(X) is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]
(X) is Relation-like [:(X),(X):] -defined (X) -valued Function-like Element of bool [:[:(X),(X):],(X):]
[:(X),(X):] is Relation-like non empty set
[:[:(X),(X):],(X):] is Relation-like non empty set
bool [:[:(X),(X):],(X):] is non empty set
CatStr(# (X),(X),(X),(X),(X) #) is non empty non void strict CatStr
the carrier of (X) is set
a is Element of the carrier of (X)
the carrier' of (X) is set
aa is non empty subset-closed () Element of (X)
(X,aa) is Element of (X)
[aa,aa] is V15() set
{aa,aa} is non empty set
{aa} is non empty set
{{aa,aa},{aa}} is non empty set
union aa is set
id (union aa) is Relation-like union aa -defined union aa -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:(union aa),(union aa):]
[:(union aa),(union aa):] is Relation-like set
bool [:(union aa),(union aa):] is non empty set
[[aa,aa],(id (union aa))] is V15() set
{[aa,aa],(id (union aa))} is non empty set
{[aa,aa]} is Relation-like Function-like non empty set
{{[aa,aa],(id (union aa))},{[aa,aa]}} is non empty set
ii is Element of the carrier' of (X)
cod ii is Element of the carrier of (X)
the Target of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
[: the carrier' of (X), the carrier of (X):] is Relation-like set
bool [: the carrier' of (X), the carrier of (X):] is non empty set
the Target of (X) . ii is Element of the carrier of (X)
(X,(X,aa)) is non empty subset-closed () Element of (X)
(X,aa) `1 is set
((X,aa) `1) `2 is set
dom ii is Element of the carrier of (X)
the Source of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
the Source of (X) . ii is Element of the carrier of (X)
(X,(X,aa)) is non empty subset-closed () Element of (X)
((X,aa) `1) `1 is set
Hom (a,a) is non empty Element of bool the carrier' of (X)
bool the carrier' of (X) is non empty set
{ b₁ where b₁ is Element of the carrier' of (X) : ( dom b₁ = a & cod b₁ = a ) } is set
ii is Morphism of a,a
c₆ is Element of the carrier of (X)
aa is Element of the carrier of (X)
Hom (a,c₆) is Element of bool the carrier' of (X)
{ b₁ where b₁ is Element of the carrier' of (X) : ( dom b₁ = a & cod b₁ = c₆ ) } is set
gg is Morphism of a,c₆
gg (*) ii is Element of the carrier' of (X)
Hom (aa,a) is Element of bool the carrier' of (X)
{ b₁ where b₁ is Element of the carrier' of (X) : ( dom b₁ = aa & cod b₁ = a ) } is set
ii is Morphism of aa,a
ii (*) ii is Element of the carrier' of (X)
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
bool [:X,X:] is non empty Element of bool (bool [:X,X:])
bool (bool [:X,X:]) is non empty set
a is set
aa is set
a is set
aa is set
ii is set
X is set
(X) is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
the Relation-like X -defined X -valued total quasi_total V27() V29() Element of bool [:X,X:] is Relation-like X -defined X -valued total quasi_total V27() V29() Element of bool [:X,X:]
X is set
bool X is non empty set
{ (b₁) where b₁ is Element of bool X : verum } is set
union { (b₁) where b₁ is Element of bool X : verum } is set
X is set
(X) is set
bool X is non empty set
{ (b₁) where b₁ is Element of bool X : verum } is set
union { (b₁) where b₁ is Element of bool X : verum } is set
({}) is non empty set
X is set
a is set
(a) is non empty set
bool a is non empty set
{ (b₁) where b₁ is Element of bool a : verum } is set
union { (b₁) where b₁ is Element of bool a : verum } is set
ii is set
ii is Element of bool a
(ii) is non empty set
[:ii,ii:] is Relation-like set
bool [:ii,ii:] is non empty set
ii is set
[:ii,ii:] is Relation-like set
bool [:ii,ii:] is non empty set
ii is Element of bool a
(ii) is non empty set
X is set
nabla X is Relation-like X -defined X -valued total quasi_total V27() V29() V34() Element of bool [:X,X:]
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
(X) is non empty set
X is set
(X) is non empty set
bool X is non empty set
{ (b₁) where b₁ is Element of bool X : verum } is set
union { (b₁) where b₁ is Element of bool X : verum } is set
({}) is non empty set
X is set
nabla X is Relation-like X -defined X -valued total quasi_total V27() V29() V34() Element of bool [:X,X:]
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
a is set
(a) is non empty set
bool a is non empty set
{ (b₁) where b₁ is Element of bool a : verum } is set
union { (b₁) where b₁ is Element of bool a : verum } is set
(X) is non empty set
X is set
id X is Relation-like X -defined X -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:X,X:]
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
a is set
(a) is non empty set
bool a is non empty set
{ (b₁) where b₁ is Element of bool a : verum } is set
union { (b₁) where b₁ is Element of bool a : verum } is set
(X) is non empty set
X is set
nabla X is Relation-like X -defined X -valued total quasi_total V27() V29() V34() Element of bool [:X,X:]
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
(X) is non empty set
bool X is non empty set
{ (b₁) where b₁ is Element of bool X : verum } is set
union { (b₁) where b₁ is Element of bool X : verum } is set
X is set
id X is Relation-like X -defined X -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:X,X:]
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
(X) is non empty set
bool X is non empty set
{ (b₁) where b₁ is Element of bool X : verum } is set
union { (b₁) where b₁ is Element of bool X : verum } is set
X is set
(X) is non empty set
bool X is non empty set
{ (b₁) where b₁ is Element of bool X : verum } is set
union { (b₁) where b₁ is Element of bool X : verum } is set
{ [b₁,b₂] where b₁ is Element of (X), b₂ is Element of bool X : b₁ is Relation-like b₂ -defined b₂ -valued total quasi_total V27() V29() Element of bool [:b₂,b₂:] } is set
X is set
(X) is set
(X) is non empty set
bool X is non empty set
{ (b₁) where b₁ is Element of bool X : verum } is set
union { (b₁) where b₁ is Element of bool X : verum } is set
{ [b₁,b₂] where b₁ is Element of (X), b₂ is Element of bool X : b₁ is Relation-like b₂ -defined b₂ -valued total quasi_total V27() V29() Element of bool [:b₂,b₂:] } is set
ii is Element of (X)
aa is Element of bool X
[ii,aa] is V15() set
{ii,aa} is non empty set
{ii} is non empty set
{{ii,aa},{ii}} is non empty set
ii is V15() set
aa is V15() set
[{},{}] is V15() set
{{},{}} is functional non empty set
{{{},{}},{{}}} is non empty set
X is set
(X) is non empty set
(X) is non empty set
bool X is non empty set
{ (b₁) where b₁ is Element of bool X : verum } is set
union { (b₁) where b₁ is Element of bool X : verum } is set
{ [b₁,b₂] where b₁ is Element of (X), b₂ is Element of bool X : b₁ is Relation-like b₂ -defined b₂ -valued total quasi_total V27() V29() Element of bool [:b₂,b₂:] } is set
X is set
id X is Relation-like X -defined X -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:X,X:]
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
[(id X),X] is V15() set
{(id X),X} is non empty set
{(id X)} is functional non empty set
{{(id X),X},{(id X)}} is non empty set
a is set
(a) is non empty set
(a) is non empty set
bool a is non empty set
{ (b₁) where b₁ is Element of bool a : verum } is set
union { (b₁) where b₁ is Element of bool a : verum } is set
{ [b₁,b₂] where b₁ is Element of (a), b₂ is Element of bool a : b₁ is Relation-like b₂ -defined b₂ -valued total quasi_total V27() V29() Element of bool [:b₂,b₂:] } is set
X is set
nabla X is Relation-like X -defined X -valued total quasi_total V27() V29() V34() Element of bool [:X,X:]
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
[(nabla X),X] is V15() set
{(nabla X),X} is non empty set
{(nabla X)} is non empty set
{{(nabla X),X},{(nabla X)}} is non empty set
a is set
(a) is non empty set
(a) is non empty set
bool a is non empty set
{ (b₁) where b₁ is Element of bool a : verum } is set
union { (b₁) where b₁ is Element of bool a : verum } is set
{ [b₁,b₂] where b₁ is Element of (a), b₂ is Element of bool a : b₁ is Relation-like b₂ -defined b₂ -valued total quasi_total V27() V29() Element of bool [:b₂,b₂:] } is set
X is set
id X is Relation-like X -defined X -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:X,X:]
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
[(id X),X] is V15() set
{(id X),X} is non empty set
{(id X)} is functional non empty set
{{(id X),X},{(id X)}} is non empty set
(X) is non empty set
(X) is non empty set
bool X is non empty set
{ (b₁) where b₁ is Element of bool X : verum } is set
union { (b₁) where b₁ is Element of bool X : verum } is set
{ [b₁,b₂] where b₁ is Element of (X), b₂ is Element of bool X : b₁ is Relation-like b₂ -defined b₂ -valued total quasi_total V27() V29() Element of bool [:b₂,b₂:] } is set
X is set
nabla X is Relation-like X -defined X -valued total quasi_total V27() V29() V34() Element of bool [:X,X:]
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
[(nabla X),X] is V15() set
{(nabla X),X} is non empty set
{(nabla X)} is non empty set
{{(nabla X),X},{(nabla X)}} is non empty set
(X) is non empty set
(X) is non empty set
bool X is non empty set
{ (b₁) where b₁ is Element of bool X : verum } is set
union { (b₁) where b₁ is Element of bool X : verum } is set
{ [b₁,b₂] where b₁ is Element of (X), b₂ is Element of bool X : b₁ is Relation-like b₂ -defined b₂ -valued total quasi_total V27() V29() Element of bool [:b₂,b₂:] } is set
X is set
(X) is non empty set
(X) is non empty set
bool X is non empty set
{ (b₁) where b₁ is Element of bool X : verum } is set
union { (b₁) where b₁ is Element of bool X : verum } is set
{ [b₁,b₂] where b₁ is Element of (X), b₂ is Element of bool X : b₁ is Relation-like b₂ -defined b₂ -valued total quasi_total V27() V29() Element of bool [:b₂,b₂:] } is set
a is Element of (X)
a `2 is set
aa is Element of (X)
ii is Element of bool X
[aa,ii] is V15() set
{aa,ii} is non empty set
{aa} is non empty set
{{aa,ii},{aa}} is non empty set
[:ii,ii:] is Relation-like set
bool [:ii,ii:] is non empty set
[aa,ii] `2 is set
a `1 is set
[:(a `2),(a `2):] is Relation-like set
bool [:(a `2),(a `2):] is non empty set
aa is Element of (X)
ii is Element of bool X
[aa,ii] is V15() set
{aa,ii} is non empty set
{aa} is non empty set
{{aa,ii},{aa}} is non empty set
[:ii,ii:] is Relation-like set
bool [:ii,ii:] is non empty set
[aa,ii] `2 is set
[aa,ii] `1 is set
X is set
(X) is non empty set
(X) is non empty set
bool X is non empty set
{ (b<sub>1</sub>) where b<sub>1</sub> is Element of bool X : verum } is set
union { (b<sub>1</sub>) where b<sub>1</sub> is Element of bool X : verum } is set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub> is Element of (X), b<sub>2</sub> is Element of bool X : b<sub>1</sub> is Relation-like b<sub>2</sub> -defined b<sub>2</sub> -valued total quasi_total V27() V29() Element of bool [:b<sub>2</sub>,b<sub>2</sub>:] } is set
{ (Funcs ((X,b<sub>1</sub>),(X,b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : verum } is set
union { (Funcs ((X,b<sub>1</sub>),(X,b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : verum } is set
X is set
(X) is set
(X) is non empty set
(X) is non empty set
bool X is non empty set
{ (b<sub>1</sub>) where b<sub>1</sub> is Element of bool X : verum } is set
union { (b<sub>1</sub>) where b<sub>1</sub> is Element of bool X : verum } is set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub> is Element of (X), b<sub>2</sub> is Element of bool X : b<sub>1</sub> is Relation-like b<sub>2</sub> -defined b<sub>2</sub> -valued total quasi_total V27() V29() Element of bool [:b<sub>2</sub>,b<sub>2</sub>:] } is set
{ (Funcs ((X,b<sub>1</sub>),(X,b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : verum } is set
union { (Funcs ((X,b<sub>1</sub>),(X,b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : verum } is set
{} X is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Element of bool X
nabla ({} X) is Relation-like non-empty empty-yielding {} X -defined {} X -valued Function-like one-to-one constant functional empty total quasi_total onto bijective V27() V29() V34() Element of bool [:({} X),({} X):]
[:({} X),({} X):] is Relation-like set
bool [:({} X),({} X):] is non empty set
[(nabla ({} X)),({} X)] is V15() set
{(nabla ({} X)),({} X)} is functional non empty set
{(nabla ({} X))} is functional non empty set
{{(nabla ({} X)),({} X)},{(nabla ({} X))}} is non empty set
[(nabla ({} X)),({} X)] `2 is set
id ({} X) is Relation-like non-empty empty-yielding {} X -defined {} X -valued Function-like one-to-one constant functional empty total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:({} X),({} X):]
aa is Element of (X)
(X,aa) is Element of bool X
Funcs ((X,aa),(X,aa)) is functional non empty set
ii is set
ii is non empty set
c₆ is set
gg is Element of (X)
(X,gg) is Element of bool X
aa is Element of (X)
(X,aa) is Element of bool X
Funcs ((X,gg),(X,aa)) is functional set
X is set
a is set
(a) is functional non empty set
(a) is non empty set
(a) is non empty set
bool a is non empty set
{ (b₁) where b₁ is Element of bool a : verum } is set
union { (b₁) where b₁ is Element of bool a : verum } is set
{ [b₁,b₂] where b₁ is Element of (a), b₂ is Element of bool a : b₁ is Relation-like b₂ -defined b₂ -valued total quasi_total V27() V29() Element of bool [:b₂,b₂:] } is set
{ (Funcs ((a,b₁),(a,b₂))) where b₁, b₂ is Element of (a) : verum } is set
union { (Funcs ((a,b₁),(a,b₂))) where b₁, b₂ is Element of (a) : verum } is set
ii is set
ii is Element of (a)
(a,ii) is Element of bool a
c₆ is Element of (a)
(a,c₆) is Element of bool a
Funcs ((a,ii),(a,c₆)) is functional set
[:(a,ii),(a,c₆):] is Relation-like set
bool [:(a,ii),(a,c₆):] is non empty set
ii is Element of (a)
(a,ii) is Element of bool a
ii is Element of (a)
(a,ii) is Element of bool a
[:(a,ii),(a,ii):] is Relation-like set
bool [:(a,ii),(a,ii):] is non empty set
Funcs ((a,ii),(a,ii)) is functional set
X is set
(X) is non empty set
(X) is non empty set
bool X is non empty set
{ (b₁) where b₁ is Element of bool X : verum } is set
union { (b₁) where b₁ is Element of bool X : verum } is set
{ [b₁,b₂] where b₁ is Element of (X), b₂ is Element of bool X : b₁ is Relation-like b₂ -defined b₂ -valued total quasi_total V27() V29() Element of bool [:b₂,b₂:] } is set
(X) is functional non empty set
{ (Funcs ((X,b₁),(X,b₂))) where b₁, b₂ is Element of (X) : verum } is set
union { (Funcs ((X,b₁),(X,b₂))) where b₁, b₂ is Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not (X,b₂) = {} or (X,b₁) = {} ) & b₃ is Relation-like (X,b₁) -defined (X,b₂) -valued Function-like quasi_total Element of bool [:(X,b₁),(X,b₂):] & ( for b₄, b₅ being set holds
( not [b₄,b₅] in (X,b₁) or [(b₃ . b₄),(b₃ . b₅)] in (X,b₂) ) ) ) } is set
X is set
(X) is set
(X) is non empty set
(X) is non empty set
bool X is non empty set
{ (b₁) where b₁ is Element of bool X : verum } is set
union { (b₁) where b₁ is Element of bool X : verum } is set
{ [b₁,b₂] where b₁ is Element of (X), b₂ is Element of bool X : b₁ is Relation-like b₂ -defined b₂ -valued total quasi_total V27() V29() Element of bool [:b₂,b₂:] } is set
(X) is functional non empty set
{ (Funcs ((X,b₁),(X,b₂))) where b₁, b₂ is Element of (X) : verum } is set
union { (Funcs ((X,b₁),(X,b₂))) where b₁, b₂ is Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not (X,b₂) = {} or (X,b₁) = {} ) & b₃ is Relation-like (X,b₁) -defined (X,b₂) -valued Function-like quasi_total Element of bool [:(X,b₁),(X,b₂):] & ( for b₄, b₅ being set holds
( not [b₄,b₅] in (X,b₁) or [(b₃ . b₄),(b₃ . b₅)] in (X,b₂) ) ) ) } is set
{} X is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty Element of bool X
nabla ({} X) is Relation-like non-empty empty-yielding {} X -defined {} X -valued Function-like one-to-one constant functional empty total quasi_total onto bijective V27() V29() V34() Element of bool [:({} X),({} X):]
[:({} X),({} X):] is Relation-like set
bool [:({} X),({} X):] is non empty set
[(nabla ({} X)),({} X)] is V15() set
{(nabla ({} X)),({} X)} is functional non empty set
{(nabla ({} X))} is functional non empty set
{{(nabla ({} X)),({} X)},{(nabla ({} X))}} is non empty set
[(nabla ({} X)),({} X)] `2 is set
id ([(nabla ({} X)),({} X)] `2) is Relation-like [(nabla ({} X)),({} X)] `2 -defined [(nabla ({} X)),({} X)] `2 -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:([(nabla ({} X)),({} X)] `2),([(nabla ({} X)),({} X)] `2):]
[:([(nabla ({} X)),({} X)] `2),([(nabla ({} X)),({} X)] `2):] is Relation-like set
bool [:([(nabla ({} X)),({} X)] `2),([(nabla ({} X)),({} X)] `2):] is non empty set
[[(nabla ({} X)),({} X)],[(nabla ({} X)),({} X)]] is V15() set
{[(nabla ({} X)),({} X)],[(nabla ({} X)),({} X)]} is Relation-like non empty set
{[(nabla ({} X)),({} X)]} is Relation-like Function-like non empty set
{{[(nabla ({} X)),({} X)],[(nabla ({} X)),({} X)]},{[(nabla ({} X)),({} X)]}} is non empty set
[[[(nabla ({} X)),({} X)],[(nabla ({} X)),({} X)]],(id ([(nabla ({} X)),({} X)] `2))] is V15() set
{[[(nabla ({} X)),({} X)],[(nabla ({} X)),({} X)]],(id ([(nabla ({} X)),({} X)] `2))} is non empty set
{[[(nabla ({} X)),({} X)],[(nabla ({} X)),({} X)]]} is Relation-like Function-like non empty set
{{[[(nabla ({} X)),({} X)],[(nabla ({} X)),({} X)]],(id ([(nabla ({} X)),({} X)] `2))},{[[(nabla ({} X)),({} X)],[(nabla ({} X)),({} X)]]}} is non empty set
c<sub>6</sub> is Element of (X)
(X,c<sub>6</sub>) is Element of bool X
(X,c<sub>6</sub>) is Relation-like c<sub>6</sub> `2 -defined c₆ `2 -valued total quasi_total V27() V29() Element of bool [:(c<sub>6</sub> `2),(c₆ `2):]
c<sub>6</sub> `2 is set
[:(c₆ `2),(c<sub>6</sub> `2):] is Relation-like set
bool [:(c₆ `2),(c<sub>6</sub> `2):] is non empty set
gg is Relation-like Function-like Element of (X)
aa is set
ii is set
[aa,ii] is V15() set
{aa,ii} is non empty set
{aa} is non empty set
{{aa,ii},{aa}} is non empty set
gg . aa is set
gg . ii is set
[(gg . aa),(gg . ii)] is V15() set
{(gg . aa),(gg . ii)} is non empty set
{(gg . aa)} is non empty set
{{(gg . aa),(gg . ii)},{(gg . aa)}} is non empty set
ii is V15() set
aa is V15() set
X is set
(X) is non empty set
(X) is non empty set
(X) is non empty set
bool X is non empty set
{ (b₁) where b₁ is Element of bool X : verum } is set
union { (b₁) where b₁ is Element of bool X : verum } is set
{ [b₁,b₂] where b₁ is Element of (X), b₂ is Element of bool X : b₁ is Relation-like b₂ -defined b₂ -valued total quasi_total V27() V29() Element of bool [:b₂,b₂:] } is set
(X) is functional non empty set
{ (Funcs ((X,b₁),(X,b₂))) where b₁, b₂ is Element of (X) : verum } is set
union { (Funcs ((X,b₁),(X,b₂))) where b₁, b₂ is Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not (X,b₂) = {} or (X,b₁) = {} ) & b₃ is Relation-like (X,b₁) -defined (X,b₂) -valued Function-like quasi_total Element of bool [:(X,b₁),(X,b₂):] & ( for b₄, b₅ being set holds
( not [b₄,b₅] in (X,b₁) or [(b₃ . b₄),(b₃ . b₅)] in (X,b₂) ) ) ) } is set
a is Element of (X)
aa is Element of (X)
ii is Element of (X)
[aa,ii] is V15() set
{aa,ii} is non empty set
{aa} is non empty set
{{aa,ii},{aa}} is non empty set
ii is Relation-like Function-like Element of (X)
[[aa,ii],ii] is V15() set
{[aa,ii],ii} is non empty set
{[aa,ii]} is Relation-like Function-like non empty set
{{[aa,ii],ii},{[aa,ii]}} is non empty set
(X,ii) is Element of bool X
(X,aa) is Element of bool X
[:(X,aa),(X,ii):] is Relation-like set
bool [:(X,aa),(X,ii):] is non empty set
(X,aa) is Relation-like aa `2 -defined aa `2 -valued total quasi_total V27() V29() Element of bool [:(aa `2),(aa `2):]
aa `2 is set
[:(aa `2),(aa `2):] is Relation-like set
bool [:(aa `2),(aa `2):] is non empty set
(X,ii) is Relation-like ii `2 -defined ii `2 -valued total quasi_total V27() V29() Element of bool [:(ii `2),(ii `2):]
ii `2 is set
[:(ii `2),(ii `2):] is Relation-like set
bool [:(ii `2),(ii `2):] is non empty set
X is set
(X) is non empty set
(X) is non empty set
bool X is non empty set
{ (b₁) where b₁ is Element of bool X : verum } is set
union { (b₁) where b₁ is Element of bool X : verum } is set
{ [b₁,b₂] where b₁ is Element of (X), b₂ is Element of bool X : b₁ is Relation-like b₂ -defined b₂ -valued total quasi_total V27() V29() Element of bool [:b₂,b₂:] } is set
(X) is non empty set
(X) is functional non empty set
{ (Funcs ((X,b₁),(X,b₂))) where b₁, b₂ is Element of (X) : verum } is set
union { (Funcs ((X,b₁),(X,b₂))) where b₁, b₂ is Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not (X,b₂) = {} or (X,b₁) = {} ) & b₃ is Relation-like (X,b₁) -defined (X,b₂) -valued Function-like quasi_total Element of bool [:(X,b₁),(X,b₂):] & ( for b₄, b₅ being set holds
( not [b₄,b₅] in (X,b₁) or [(b₃ . b₄),(b₃ . b₅)] in (X,b₂) ) ) ) } is set
a is Element of (X)
(X,a) is Element of bool X
(X,a) is Relation-like a `2 -defined a `2 -valued total quasi_total V27() V29() Element of bool [:(a `2),(a `2):]
a `2 is set
[:(a `2),(a `2):] is Relation-like set
bool [:(a `2),(a `2):] is non empty set
aa is Element of (X)
(X,aa) is Element of bool X
[:(X,a),(X,aa):] is Relation-like set
bool [:(X,a),(X,aa):] is non empty set
(X,aa) is Relation-like aa `2 -defined aa `2 -valued total quasi_total V27() V29() Element of bool [:(aa `2),(aa `2):]
aa `2 is set
[:(aa `2),(aa `2):] is Relation-like set
bool [:(aa `2),(aa `2):] is non empty set
[a,aa] is V15() set
{a,aa} is non empty set
{a} is non empty set
{{a,aa},{a}} is non empty set
ii is Relation-like (X,a) -defined (X,aa) -valued Function-like quasi_total Element of bool [:(X,a),(X,aa):]
[[a,aa],ii] is V15() set
{[a,aa],ii} is non empty set
{[a,aa]} is Relation-like Function-like non empty set
{{[a,aa],ii},{[a,aa]}} is non empty set
ii is Relation-like Function-like Element of (X)
c₆ is set
gg is set
[c₆,gg] is V15() set
{c₆,gg} is non empty set
{c₆} is non empty set
{{c₆,gg},{c₆}} is non empty set
ii . c₆ is set
ii . gg is set
[(ii . c₆),(ii . gg)] is V15() set
{(ii . c₆),(ii . gg)} is non empty set
{(ii . c₆)} is non empty set
{{(ii . c₆),(ii . gg)},{(ii . c₆)}} is non empty set
X is set
(X) is non empty set
(X) is non empty set
(X) is non empty set
bool X is non empty set
{ (b₁) where b₁ is Element of bool X : verum } is set
union { (b₁) where b₁ is Element of bool X : verum } is set
{ [b₁,b₂] where b₁ is Element of (X), b₂ is Element of bool X : b₁ is Relation-like b₂ -defined b₂ -valued total quasi_total V27() V29() Element of bool [:b₂,b₂:] } is set
(X) is functional non empty set
{ (Funcs ((X,b₁),(X,b₂))) where b₁, b₂ is Element of (X) : verum } is set
union { (Funcs ((X,b₁),(X,b₂))) where b₁, b₂ is Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not (X,b₂) = {} or (X,b₁) = {} ) & b₃ is Relation-like (X,b₁) -defined (X,b₂) -valued Function-like quasi_total Element of bool [:(X,b₁),(X,b₂):] & ( for b₄, b₅ being set holds
( not [b₄,b₅] in (X,b₁) or [(b₃ . b₄),(b₃ . b₅)] in (X,b₂) ) ) ) } is set
a is Element of (X)
a `2 is set
ii is Element of (X)
ii is Element of (X)
[ii,ii] is V15() set
{ii,ii} is non empty set
{ii} is non empty set
{{ii,ii},{ii}} is non empty set
aa is Relation-like Function-like Element of (X)
[[ii,ii],aa] is V15() set
{[ii,ii],aa} is non empty set
{[ii,ii]} is Relation-like Function-like non empty set
{{[ii,ii],aa},{[ii,ii]}} is non empty set
(X,ii) is Element of bool X
(X,ii) is Element of bool X
[:(X,ii),(X,ii):] is Relation-like set
bool [:(X,ii),(X,ii):] is non empty set
(X,ii) is Relation-like ii `2 -defined ii `2 -valued total quasi_total V27() V29() Element of bool [:(ii `2),(ii `2):]
ii `2 is set
[:(ii `2),(ii `2):] is Relation-like set
bool [:(ii `2),(ii `2):] is non empty set
(X,ii) is Relation-like ii `2 -defined ii `2 -valued total quasi_total V27() V29() Element of bool [:(ii `2),(ii `2):]
ii `2 is set
[:(ii `2),(ii `2):] is Relation-like set
bool [:(ii `2),(ii `2):] is non empty set
[[ii,ii],aa] `2 is set
X is set
(X) is non empty set
(X) is non empty set
(X) is non empty set
bool X is non empty set
{ (b₁) where b₁ is Element of bool X : verum } is set
union { (b₁) where b₁ is Element of bool X : verum } is set
{ [b₁,b₂] where b₁ is Element of (X), b₂ is Element of bool X : b₁ is Relation-like b₂ -defined b₂ -valued total quasi_total V27() V29() Element of bool [:b₂,b₂:] } is set
(X) is functional non empty set
{ (Funcs ((X,b₁),(X,b₂))) where b₁, b₂ is Element of (X) : verum } is set
union { (Funcs ((X,b₁),(X,b₂))) where b₁, b₂ is Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not (X,b₂) = {} or (X,b₁) = {} ) & b₃ is Relation-like (X,b₁) -defined (X,b₂) -valued Function-like quasi_total Element of bool [:(X,b₁),(X,b₂):] & ( for b₄, b₅ being set holds
( not [b₄,b₅] in (X,b₁) or [(b₃ . b₄),(b₃ . b₅)] in (X,b₂) ) ) ) } is set
a is Element of (X)
a `1 is set
(a `1) `1 is set
ii is Element of (X)
ii is Element of (X)
[ii,ii] is V15() set
{ii,ii} is non empty set
{ii} is non empty set
{{ii,ii},{ii}} is non empty set
aa is Relation-like Function-like Element of (X)
[[ii,ii],aa] is V15() set
{[ii,ii],aa} is non empty set
{[ii,ii]} is Relation-like Function-like non empty set
{{[ii,ii],aa},{[ii,ii]}} is non empty set
(X,ii) is Element of bool X
(X,ii) is Element of bool X
[:(X,ii),(X,ii):] is Relation-like set
bool [:(X,ii),(X,ii):] is non empty set
(X,ii) is Relation-like ii `2 -defined ii `2 -valued total quasi_total V27() V29() Element of bool [:(ii `2),(ii `2):]
ii `2 is set
[:(ii `2),(ii `2):] is Relation-like set
bool [:(ii `2),(ii `2):] is non empty set
(X,ii) is Relation-like ii `2 -defined ii `2 -valued total quasi_total V27() V29() Element of bool [:(ii `2),(ii `2):]
ii `2 is set
[:(ii `2),(ii `2):] is Relation-like set
bool [:(ii `2),(ii `2):] is non empty set
[[ii,ii],aa] `1 is set
[ii,ii] `1 is set
(a `1) `2 is set
ii is Element of (X)
ii is Element of (X)
[ii,ii] is V15() set
{ii,ii} is non empty set
{ii} is non empty set
{{ii,ii},{ii}} is non empty set
aa is Relation-like Function-like Element of (X)
[[ii,ii],aa] is V15() set
{[ii,ii],aa} is non empty set
{[ii,ii]} is Relation-like Function-like non empty set
{{[ii,ii],aa},{[ii,ii]}} is non empty set
(X,ii) is Element of bool X
(X,ii) is Element of bool X
[:(X,ii),(X,ii):] is Relation-like set
bool [:(X,ii),(X,ii):] is non empty set
(X,ii) is Relation-like ii `2 -defined ii `2 -valued total quasi_total V27() V29() Element of bool [:(ii `2),(ii `2):]
ii `2 is set
[:(ii `2),(ii `2):] is Relation-like set
bool [:(ii `2),(ii `2):] is non empty set
(X,ii) is Relation-like ii `2 -defined ii `2 -valued total quasi_total V27() V29() Element of bool [:(ii `2),(ii `2):]
ii `2 is set
[:(ii `2),(ii `2):] is Relation-like set
bool [:(ii `2),(ii `2):] is non empty set
[[ii,ii],aa] `1 is set
[ii,ii] `2 is set
X is set
(X) is non empty set
(X) is non empty set
(X) is non empty set
bool X is non empty set
{ (b<sub>1</sub>) where b<sub>1</sub> is Element of bool X : verum } is set
union { (b<sub>1</sub>) where b<sub>1</sub> is Element of bool X : verum } is set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub> is Element of (X), b<sub>2</sub> is Element of bool X : b<sub>1</sub> is Relation-like b<sub>2</sub> -defined b<sub>2</sub> -valued total quasi_total V27() V29() Element of bool [:b<sub>2</sub>,b<sub>2</sub>:] } is set
(X) is functional non empty set
{ (Funcs ((X,b<sub>1</sub>),(X,b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : verum } is set
union { (Funcs ((X,b<sub>1</sub>),(X,b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : verum } is set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of (X), b<sub>3</sub> is Relation-like Function-like Element of (X) : ( ( not (X,b<sub>2</sub>) = {} or (X,b<sub>1</sub>) = {} ) & b<sub>3</sub> is Relation-like (X,b<sub>1</sub>) -defined (X,b<sub>2</sub>) -valued Function-like quasi_total Element of bool [:(X,b<sub>1</sub>),(X,b<sub>2</sub>):] & ( for b<sub>4</sub>, b<sub>5</sub> being set holds
( not [b<sub>4</sub>,b<sub>5</sub>] in (X,b<sub>1</sub>) or [(b<sub>3</sub> . b<sub>4</sub>),(b<sub>3</sub> . b<sub>5</sub>)] in (X,b<sub>2</sub>) ) ) ) } is set
a is Element of (X)
(X,a) is Element of (X)
a `1 is set
(a `1) `1 is set
(X,a) is Element of (X)
(a `1) `2 is set
[(X,a),(X,a)] is V15() set
{(X,a),(X,a)} is non empty set
{(X,a)} is non empty set
{{(X,a),(X,a)},{(X,a)}} is non empty set
a `2 is Relation-like Function-like set
[[(X,a),(X,a)],(a `2)] is V15() set
{[(X,a),(X,a)],(a `2)} is non empty set
{[(X,a),(X,a)]} is Relation-like Function-like non empty set
{{[(X,a),(X,a)],(a `2)},{[(X,a),(X,a)]}} is non empty set
ii is Element of (X)
ii is Element of (X)
[ii,ii] is V15() set
{ii,ii} is non empty set
{ii} is non empty set
{{ii,ii},{ii}} is non empty set
aa is Relation-like Function-like Element of (X)
[[ii,ii],aa] is V15() set
{[ii,ii],aa} is non empty set
{[ii,ii]} is Relation-like Function-like non empty set
{{[ii,ii],aa},{[ii,ii]}} is non empty set
(X,ii) is Element of bool X
(X,ii) is Element of bool X
[:(X,ii),(X,ii):] is Relation-like set
bool [:(X,ii),(X,ii):] is non empty set
(X,ii) is Relation-like ii `2 -defined ii `2 -valued total quasi_total V27() V29() Element of bool [:(ii `2),(ii `2):]
ii `2 is set
[:(ii `2),(ii `2):] is Relation-like set
bool [:(ii `2),(ii `2):] is non empty set
(X,ii) is Relation-like ii `2 -defined ii `2 -valued total quasi_total V27() V29() Element of bool [:(ii `2),(ii `2):]
ii `2 is set
[:(ii `2),(ii `2):] is Relation-like set
bool [:(ii `2),(ii `2):] is non empty set
[[ii,ii],aa] `1 is set
X is set
(X) is non empty set
(X) is non empty set
(X) is non empty set
bool X is non empty set
{ (b<sub>1</sub>) where b<sub>1</sub> is Element of bool X : verum } is set
union { (b<sub>1</sub>) where b<sub>1</sub> is Element of bool X : verum } is set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub> is Element of (X), b<sub>2</sub> is Element of bool X : b<sub>1</sub> is Relation-like b<sub>2</sub> -defined b<sub>2</sub> -valued total quasi_total V27() V29() Element of bool [:b<sub>2</sub>,b<sub>2</sub>:] } is set
(X) is functional non empty set
{ (Funcs ((X,b<sub>1</sub>),(X,b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : verum } is set
union { (Funcs ((X,b<sub>1</sub>),(X,b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : verum } is set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of (X), b<sub>3</sub> is Relation-like Function-like Element of (X) : ( ( not (X,b<sub>2</sub>) = {} or (X,b<sub>1</sub>) = {} ) & b<sub>3</sub> is Relation-like (X,b<sub>1</sub>) -defined (X,b<sub>2</sub>) -valued Function-like quasi_total Element of bool [:(X,b<sub>1</sub>),(X,b<sub>2</sub>):] & ( for b<sub>4</sub>, b<sub>5</sub> being set holds
( not [b<sub>4</sub>,b<sub>5</sub>] in (X,b<sub>1</sub>) or [(b<sub>3</sub> . b<sub>4</sub>),(b<sub>3</sub> . b<sub>5</sub>)] in (X,b<sub>2</sub>) ) ) ) } is set
a is Element of (X)
a `2 is Relation-like Function-like set
(X,a) is Element of (X)
a `1 is set
(a `1) `1 is set
(X,a) is Element of (X)
(a `1) `2 is set
aa is Element of (X)
aa `2 is Relation-like Function-like set
(X,aa) is Element of (X)
aa `1 is set
(aa `1) `1 is set
(X,aa) is Element of (X)
(aa `1) `2 is set
[(X,a),(X,a)] is V15() set
{(X,a),(X,a)} is non empty set
{(X,a)} is non empty set
{{(X,a),(X,a)},{(X,a)}} is non empty set
[[(X,a),(X,a)],(a `2)] is V15() set
{[(X,a),(X,a)],(a `2)} is non empty set
{[(X,a),(X,a)]} is Relation-like Function-like non empty set
{{[(X,a),(X,a)],(a `2)},{[(X,a),(X,a)]}} is non empty set
X is set
(X) is non empty set
(X) is non empty set
bool X is non empty set
{ (b₁) where b₁ is Element of bool X : verum } is set
union { (b₁) where b₁ is Element of bool X : verum } is set
{ [b₁,b₂] where b₁ is Element of (X), b₂ is Element of bool X : b₁ is Relation-like b₂ -defined b₂ -valued total quasi_total V27() V29() Element of bool [:b₂,b₂:] } is set
a is Element of (X)
[a,a] is V15() set
{a,a} is non empty set
{a} is non empty set
{{a,a},{a}} is non empty set
(X,a) is Element of bool X
id (X,a) is Relation-like (X,a) -defined (X,a) -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:(X,a),(X,a):]
[:(X,a),(X,a):] is Relation-like set
bool [:(X,a),(X,a):] is non empty set
[[a,a],(id (X,a))] is V15() set
{[a,a],(id (X,a))} is non empty set
{[a,a]} is Relation-like Function-like non empty set
{{[a,a],(id (X,a))},{[a,a]}} is non empty set
(X) is non empty set
(X) is functional non empty set
{ (Funcs ((X,b₁),(X,b₂))) where b₁, b₂ is Element of (X) : verum } is set
union { (Funcs ((X,b₁),(X,b₂))) where b₁, b₂ is Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not (X,b₂) = {} or (X,b₁) = {} ) & b₃ is Relation-like (X,b₁) -defined (X,b₂) -valued Function-like quasi_total Element of bool [:(X,b₁),(X,b₂):] & ( for b₄, b₅ being set holds
( not [b₄,b₅] in (X,b₁) or [(b₃ . b₄),(b₃ . b₅)] in (X,b₂) ) ) ) } is set
ii is set
ii is set
[ii,ii] is V15() set
{ii,ii} is non empty set
{ii} is non empty set
{{ii,ii},{ii}} is non empty set
(X,a) is Relation-like a `2 -defined a `2 -valued total quasi_total V27() V29() Element of bool [:(a `2),(a `2):]
a `2 is set
[:(a `2),(a `2):] is Relation-like set
bool [:(a `2),(a `2):] is non empty set
(id (X,a)) . ii is set
(id (X,a)) . ii is set
[((id (X,a)) . ii),((id (X,a)) . ii)] is V15() set
{((id (X,a)) . ii),((id (X,a)) . ii)} is non empty set
{((id (X,a)) . ii)} is non empty set
{{((id (X,a)) . ii),((id (X,a)) . ii)},{((id (X,a)) . ii)}} is non empty set
X is set
(X) is non empty set
(X) is non empty set
(X) is non empty set
bool X is non empty set
{ (b<sub>1</sub>) where b<sub>1</sub> is Element of bool X : verum } is set
union { (b<sub>1</sub>) where b<sub>1</sub> is Element of bool X : verum } is set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub> is Element of (X), b<sub>2</sub> is Element of bool X : b<sub>1</sub> is Relation-like b<sub>2</sub> -defined b<sub>2</sub> -valued total quasi_total V27() V29() Element of bool [:b<sub>2</sub>,b<sub>2</sub>:] } is set
(X) is functional non empty set
{ (Funcs ((X,b<sub>1</sub>),(X,b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : verum } is set
union { (Funcs ((X,b<sub>1</sub>),(X,b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : verum } is set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of (X), b<sub>3</sub> is Relation-like Function-like Element of (X) : ( ( not (X,b<sub>2</sub>) = {} or (X,b<sub>1</sub>) = {} ) & b<sub>3</sub> is Relation-like (X,b<sub>1</sub>) -defined (X,b<sub>2</sub>) -valued Function-like quasi_total Element of bool [:(X,b<sub>1</sub>),(X,b<sub>2</sub>):] & ( for b<sub>4</sub>, b<sub>5</sub> being set holds
( not [b<sub>4</sub>,b<sub>5</sub>] in (X,b<sub>1</sub>) or [(b<sub>3</sub> . b<sub>4</sub>),(b<sub>3</sub> . b<sub>5</sub>)] in (X,b<sub>2</sub>) ) ) ) } is set
a is Element of (X)
(X,a) is Element of (X)
a `1 is set
(a `1) `2 is set
(X,(X,a)) is Element of bool X
(X,a) is Element of (X)
(a `1) `1 is set
(X,(X,a)) is Element of bool X
a `2 is Relation-like Function-like set
[:(X,(X,a)),(X,(X,a)):] is Relation-like set
bool [:(X,(X,a)),(X,(X,a)):] is non empty set
(X,(X,a)) is Relation-like (X,a) `2 -defined (X,a) `2 -valued total quasi_total V27() V29() Element of bool [:((X,a) `2),((X,a) `2):]
(X,a) `2 is set
[:((X,a) `2),((X,a) `2):] is Relation-like set
bool [:((X,a) `2),((X,a) `2):] is non empty set
(X,(X,a)) is Relation-like (X,a) `2 -defined (X,a) `2 -valued total quasi_total V27() V29() Element of bool [:((X,a) `2),((X,a) `2):]
(X,a) `2 is set
[:((X,a) `2),((X,a) `2):] is Relation-like set
bool [:((X,a) `2),((X,a) `2):] is non empty set
ii is Element of (X)
ii is Element of (X)
[ii,ii] is V15() set
{ii,ii} is non empty set
{ii} is non empty set
{{ii,ii},{ii}} is non empty set
aa is Relation-like Function-like Element of (X)
[[ii,ii],aa] is V15() set
{[ii,ii],aa} is non empty set
{[ii,ii]} is Relation-like Function-like non empty set
{{[ii,ii],aa},{[ii,ii]}} is non empty set
(X,ii) is Element of bool X
(X,ii) is Element of bool X
[:(X,ii),(X,ii):] is Relation-like set
bool [:(X,ii),(X,ii):] is non empty set
(X,ii) is Relation-like ii `2 -defined ii `2 -valued total quasi_total V27() V29() Element of bool [:(ii `2),(ii `2):]
ii `2 is set
[:(ii `2),(ii `2):] is Relation-like set
bool [:(ii `2),(ii `2):] is non empty set
(X,ii) is Relation-like ii `2 -defined ii `2 -valued total quasi_total V27() V29() Element of bool [:(ii `2),(ii `2):]
ii `2 is set
[:(ii `2),(ii `2):] is Relation-like set
bool [:(ii `2),(ii `2):] is non empty set
[(X,a),(X,a)] is V15() set
{(X,a),(X,a)} is non empty set
{(X,a)} is non empty set
{{(X,a),(X,a)},{(X,a)}} is non empty set
[[(X,a),(X,a)],(a `2)] is V15() set
{[(X,a),(X,a)],(a `2)} is non empty set
{[(X,a),(X,a)]} is Relation-like Function-like non empty set
{{[(X,a),(X,a)],(a `2)},{[(X,a),(X,a)]}} is non empty set
c₆ is set
(a `2) . c<sub>6</sub> is set
gg is set
[c<sub>6</sub>,gg] is V15() set
{c<sub>6</sub>,gg} is non empty set
{c<sub>6</sub>} is non empty set
{{c<sub>6</sub>,gg},{c<sub>6</sub>}} is non empty set
(a `2) . gg is set
[((a `2) . c<sub>6</sub>),((a `2) . gg)] is V15() set
{((a `2) . c<sub>6</sub>),((a `2) . gg)} is non empty set
{((a `2) . c<sub>6</sub>)} is non empty set
{{((a `2) . c₆),((a `2) . gg)},{((a `2) . c₆)}} is non empty set
X is set
(X) is non empty set
(X) is non empty set
(X) is non empty set
bool X is non empty set
{ (b₁) where b₁ is Element of bool X : verum } is set
union { (b₁) where b₁ is Element of bool X : verum } is set
{ [b₁,b₂] where b₁ is Element of (X), b₂ is Element of bool X : b₁ is Relation-like b₂ -defined b₂ -valued total quasi_total V27() V29() Element of bool [:b₂,b₂:] } is set
(X) is functional non empty set
{ (Funcs ((X,b₁),(X,b₂))) where b₁, b₂ is Element of (X) : verum } is set
union { (Funcs ((X,b₁),(X,b₂))) where b₁, b₂ is Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not (X,b₂) = {} or (X,b₁) = {} ) & b₃ is Relation-like (X,b₁) -defined (X,b₂) -valued Function-like quasi_total Element of bool [:(X,b₁),(X,b₂):] & ( for b₄, b₅ being set holds
( not [b₄,b₅] in (X,b₁) or [(b₃ . b₄),(b₃ . b₅)] in (X,b₂) ) ) ) } is set
a is Element of (X)
(X,a) is Element of (X)
a `1 is set
(a `1) `2 is set
aa is Element of (X)
(X,aa) is Element of (X)
aa `1 is set
(aa `1) `1 is set
(X,a) is Element of (X)
(a `1) `1 is set
(X,aa) is Element of (X)
(aa `1) `2 is set
[(X,a),(X,aa)] is V15() set
{(X,a),(X,aa)} is non empty set
{(X,a)} is non empty set
{{(X,a),(X,aa)},{(X,a)}} is non empty set
a `2 is Relation-like Function-like set
aa `2 is Relation-like Function-like set
(a `2) * (aa `2) is Relation-like Function-like set
[[(X,a),(X,aa)],((a `2) * (aa `2))] is V15() set
{[(X,a),(X,aa)],((a `2) * (aa `2))} is non empty set
{[(X,a),(X,aa)]} is Relation-like Function-like non empty set
{{[(X,a),(X,aa)],((a `2) * (aa `2))},{[(X,a),(X,aa)]}} is non empty set
(X,(X,aa)) is Element of bool X
(X,(X,aa)) is Element of bool X
(X,(X,a)) is Element of bool X
(X,(X,a)) is Element of bool X
[:(X,(X,a)),(X,(X,a)):] is Relation-like set
bool [:(X,(X,a)),(X,(X,a)):] is non empty set
ii is set
ii is set
[ii,ii] is V15() set
{ii,ii} is non empty set
{ii} is non empty set
{{ii,ii},{ii}} is non empty set
(X,(X,a)) is Relation-like (X,a) `2 -defined (X,a) `2 -valued total quasi_total V27() V29() Element of bool [:((X,a) `2),((X,a) `2):]
(X,a) `2 is set
[:((X,a) `2),((X,a) `2):] is Relation-like set
bool [:((X,a) `2),((X,a) `2):] is non empty set
proj1 (a `2) is set
(a `2) . ii is set
(a `2) . ii is set
[((a `2) . ii),((a `2) . ii)] is V15() set
{((a `2) . ii),((a `2) . ii)} is non empty set
{((a `2) . ii)} is non empty set
{{((a `2) . ii),((a `2) . ii)},{((a `2) . ii)}} is non empty set
(X,(X,a)) is Relation-like (X,a) `2 -defined (X,a) `2 -valued total quasi_total V27() V29() Element of bool [:((X,a) `2),((X,a) `2):]
(X,a) `2 is set
[:((X,a) `2),((X,a) `2):] is Relation-like set
bool [:((X,a) `2),((X,a) `2):] is non empty set
(aa `2) . ((a `2) . ii) is set
(aa `2) . ((a `2) . ii) is set
[((aa `2) . ((a `2) . ii)),((aa `2) . ((a `2) . ii))] is V15() set
{((aa `2) . ((a `2) . ii)),((aa `2) . ((a `2) . ii))} is non empty set
{((aa `2) . ((a `2) . ii))} is non empty set
{{((aa `2) . ((a `2) . ii)),((aa `2) . ((a `2) . ii))},{((aa `2) . ((a `2) . ii))}} is non empty set
(X,(X,aa)) is Relation-like (X,aa) `2 -defined (X,aa) `2 -valued total quasi_total V27() V29() Element of bool [:((X,aa) `2),((X,aa) `2):]
(X,aa) `2 is set
[:((X,aa) `2),((X,aa) `2):] is Relation-like set
bool [:((X,aa) `2),((X,aa) `2):] is non empty set
((a `2) * (aa `2)) . ii is set
[(((a `2) * (aa `2)) . ii),((aa `2) . ((a `2) . ii))] is V15() set
{(((a `2) * (aa `2)) . ii),((aa `2) . ((a `2) . ii))} is non empty set
{(((a `2) * (aa `2)) . ii)} is non empty set
{{(((a `2) * (aa `2)) . ii),((aa `2) . ((a `2) . ii))},{(((a `2) * (aa `2)) . ii)}} is non empty set
((a `2) * (aa `2)) . ii is set
[(((a `2) * (aa `2)) . ii),(((a `2) * (aa `2)) . ii)] is V15() set
{(((a `2) * (aa `2)) . ii),(((a `2) * (aa `2)) . ii)} is non empty set
{{(((a `2) * (aa `2)) . ii),(((a `2) * (aa `2)) . ii)},{(((a `2) * (aa `2)) . ii)}} is non empty set
[:(X,(X,aa)),(X,(X,aa)):] is Relation-like set
bool [:(X,(X,aa)),(X,(X,aa)):] is non empty set
[:(X,(X,a)),(X,(X,aa)):] is Relation-like set
bool [:(X,(X,a)),(X,(X,aa)):] is non empty set
X is set
(X) is non empty set
(X) is non empty set
(X) is non empty set
bool X is non empty set
{ (b₁) where b₁ is Element of bool X : verum } is set
union { (b₁) where b₁ is Element of bool X : verum } is set
{ [b₁,b₂] where b₁ is Element of (X), b₂ is Element of bool X : b₁ is Relation-like b₂ -defined b₂ -valued total quasi_total V27() V29() Element of bool [:b₂,b₂:] } is set
(X) is functional non empty set
{ (Funcs ((X,b₁),(X,b₂))) where b₁, b₂ is Element of (X) : verum } is set
union { (Funcs ((X,b₁),(X,b₂))) where b₁, b₂ is Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not (X,b₂) = {} or (X,b₁) = {} ) & b₃ is Relation-like (X,b₁) -defined (X,b₂) -valued Function-like quasi_total Element of bool [:(X,b₁),(X,b₂):] & ( for b₄, b₅ being set holds
( not [b₄,b₅] in (X,b₁) or [(b₃ . b₄),(b₃ . b₅)] in (X,b₂) ) ) ) } is set
a is Element of (X)
(X,a) is Element of (X)
a `1 is set
(a `1) `1 is set
a `2 is Relation-like Function-like set
(X,a) is Element of (X)
(a `1) `2 is set
aa is Element of (X)
(X,aa) is Element of (X)
aa `1 is set
(aa `1) `2 is set
(X,aa,a) is Element of (X)
(X,aa,a) `2 is Relation-like Function-like set
aa `2 is Relation-like Function-like set
(aa `2) * (a `2) is Relation-like Function-like set
(X,(X,aa,a)) is Element of (X)
(X,aa,a) `1 is set
((X,aa,a) `1) `1 is set
(X,aa) is Element of (X)
(aa `1) `1 is set
(X,(X,aa,a)) is Element of (X)
((X,aa,a) `1) `2 is set
[(X,aa),(X,a)] is V15() set
{(X,aa),(X,a)} is non empty set
{(X,aa)} is non empty set
{{(X,aa),(X,a)},{(X,aa)}} is non empty set
[[(X,aa),(X,a)],((aa `2) * (a `2))] is V15() set
{[(X,aa),(X,a)],((aa `2) * (a `2))} is non empty set
{[(X,aa),(X,a)]} is Relation-like Function-like non empty set
{{[(X,aa),(X,a)],((aa `2) * (a `2))},{[(X,aa),(X,a)]}} is non empty set
[(X,(X,aa,a)),(X,(X,aa,a))] is V15() set
{(X,(X,aa,a)),(X,(X,aa,a))} is non empty set
{(X,(X,aa,a))} is non empty set
{{(X,(X,aa,a)),(X,(X,aa,a))},{(X,(X,aa,a))}} is non empty set
[[(X,(X,aa,a)),(X,(X,aa,a))],((X,aa,a) `2)] is V15() set
{[(X,(X,aa,a)),(X,(X,aa,a))],((X,aa,a) `2)} is non empty set
{[(X,(X,aa,a)),(X,(X,aa,a))]} is Relation-like Function-like non empty set
{{[(X,(X,aa,a)),(X,(X,aa,a))],((X,aa,a) `2)},{[(X,(X,aa,a)),(X,(X,aa,a))]}} is non empty set
X is set
(X) is non empty set
(X) is non empty set
(X) is non empty set
bool X is non empty set
{ (b<sub>1</sub>) where b<sub>1</sub> is Element of bool X : verum } is set
union { (b<sub>1</sub>) where b<sub>1</sub> is Element of bool X : verum } is set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub> is Element of (X), b<sub>2</sub> is Element of bool X : b<sub>1</sub> is Relation-like b<sub>2</sub> -defined b<sub>2</sub> -valued total quasi_total V27() V29() Element of bool [:b<sub>2</sub>,b<sub>2</sub>:] } is set
(X) is functional non empty set
{ (Funcs ((X,b<sub>1</sub>),(X,b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : verum } is set
union { (Funcs ((X,b<sub>1</sub>),(X,b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : verum } is set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of (X), b<sub>3</sub> is Relation-like Function-like Element of (X) : ( ( not (X,b<sub>2</sub>) = {} or (X,b<sub>1</sub>) = {} ) & b<sub>3</sub> is Relation-like (X,b<sub>1</sub>) -defined (X,b<sub>2</sub>) -valued Function-like quasi_total Element of bool [:(X,b<sub>1</sub>),(X,b<sub>2</sub>):] & ( for b<sub>4</sub>, b<sub>5</sub> being set holds
( not [b<sub>4</sub>,b<sub>5</sub>] in (X,b<sub>1</sub>) or [(b<sub>3</sub> . b<sub>4</sub>),(b<sub>3</sub> . b<sub>5</sub>)] in (X,b<sub>2</sub>) ) ) ) } is set
a is Element of (X)
(X,a) is Element of (X)
a `1 is set
(a `1) `1 is set
(X,a) is Element of (X)
(a `1) `2 is set
aa is Element of (X)
(X,aa) is Element of (X)
aa `1 is set
(aa `1) `2 is set
(X,aa,a) is Element of (X)
ii is Element of (X)
(X,ii) is Element of (X)
ii `1 is set
(ii `1) `1 is set
(X,(X,aa,a),ii) is Element of (X)
(X,a,ii) is Element of (X)
(X,aa,(X,a,ii)) is Element of (X)
(X,(X,aa,a)) is Element of (X)
(X,aa,a) `1 is set
((X,aa,a) `1) `2 is set
(X,aa,a) `2 is Relation-like Function-like set
aa `2 is Relation-like Function-like set
a `2 is Relation-like Function-like set
(aa `2) * (a `2) is Relation-like Function-like set
(X,(X,aa,a),ii) `2 is Relation-like Function-like set
ii `2 is Relation-like Function-like set
((aa `2) * (a `2)) * (ii `2) is Relation-like Function-like set
(X,(X,a,ii)) is Element of (X)
(X,a,ii) `1 is set
((X,a,ii) `1) `1 is set
(X,(X,aa,(X,a,ii))) is Element of (X)
(X,aa,(X,a,ii)) `1 is set
((X,aa,(X,a,ii)) `1) `1 is set
(X,aa) is Element of (X)
(aa `1) `1 is set
(X,(X,aa,a)) is Element of (X)
((X,aa,a) `1) `1 is set
(X,(X,(X,aa,a),ii)) is Element of (X)
(X,(X,aa,a),ii) `1 is set
((X,(X,aa,a),ii) `1) `1 is set
(X,(X,a,ii)) is Element of (X)
((X,a,ii) `1) `2 is set
(X,ii) is Element of (X)
(ii `1) `2 is set
(X,(X,aa,(X,a,ii))) is Element of (X)
((X,aa,(X,a,ii)) `1) `2 is set
(X,a,ii) `2 is Relation-like Function-like set
(a `2) * (ii `2) is Relation-like Function-like set
(X,aa,(X,a,ii)) `2 is Relation-like Function-like set
(aa `2) * ((a `2) * (ii `2)) is Relation-like Function-like set
(X,(X,(X,aa,a),ii)) is Element of (X)
((X,(X,aa,a),ii) `1) `2 is set
X is set
(X) is non empty set
(X) is non empty set
bool X is non empty set
{ (b<sub>1</sub>) where b<sub>1</sub> is Element of bool X : verum } is set
union { (b<sub>1</sub>) where b<sub>1</sub> is Element of bool X : verum } is set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub> is Element of (X), b<sub>2</sub> is Element of bool X : b<sub>1</sub> is Relation-like b<sub>2</sub> -defined b<sub>2</sub> -valued total quasi_total V27() V29() Element of bool [:b<sub>2</sub>,b<sub>2</sub>:] } is set
a is Element of (X)
(X,a) is Element of (X)
(X) is non empty set
(X) is functional non empty set
{ (Funcs ((X,b<sub>1</sub>),(X,b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : verum } is set
union { (Funcs ((X,b<sub>1</sub>),(X,b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : verum } is set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of (X), b<sub>3</sub> is Relation-like Function-like Element of (X) : ( ( not (X,b<sub>2</sub>) = {} or (X,b<sub>1</sub>) = {} ) & b<sub>3</sub> is Relation-like (X,b<sub>1</sub>) -defined (X,b<sub>2</sub>) -valued Function-like quasi_total Element of bool [:(X,b<sub>1</sub>),(X,b<sub>2</sub>):] & ( for b<sub>4</sub>, b<sub>5</sub> being set holds
( not [b<sub>4</sub>,b<sub>5</sub>] in (X,b<sub>1</sub>) or [(b<sub>3</sub> . b<sub>4</sub>),(b<sub>3</sub> . b<sub>5</sub>)] in (X,b<sub>2</sub>) ) ) ) } is set
[a,a] is V15() set
{a,a} is non empty set
{a} is non empty set
{{a,a},{a}} is non empty set
(X,a) is Element of bool X
id (X,a) is Relation-like (X,a) -defined (X,a) -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:(X,a),(X,a):]
[:(X,a),(X,a):] is Relation-like set
bool [:(X,a),(X,a):] is non empty set
[[a,a],(id (X,a))] is V15() set
{[a,a],(id (X,a))} is non empty set
{[a,a]} is Relation-like Function-like non empty set
{{[a,a],(id (X,a))},{[a,a]}} is non empty set
(X,a) `2 is Relation-like Function-like set
(X,(X,a)) is Element of (X)
(X,a) `1 is set
((X,a) `1) `1 is set
(X,(X,a)) is Element of (X)
((X,a) `1) `2 is set
[(X,(X,a)),(X,(X,a))] is V15() set
{(X,(X,a)),(X,(X,a))} is non empty set
{(X,(X,a))} is non empty set
{{(X,(X,a)),(X,(X,a))},{(X,(X,a))}} is non empty set
[[(X,(X,a)),(X,(X,a))],((X,a) `2)] is V15() set
{[(X,(X,a)),(X,(X,a))],((X,a) `2)} is non empty set
{[(X,(X,a)),(X,(X,a))]} is Relation-like Function-like non empty set
{{[(X,(X,a)),(X,(X,a))],((X,a) `2)},{[(X,(X,a)),(X,(X,a))]}} is non empty set
X is set
(X) is non empty set
(X) is non empty set
(X) is non empty set
bool X is non empty set
{ (b₁) where b₁ is Element of bool X : verum } is set
union { (b₁) where b₁ is Element of bool X : verum } is set
{ [b₁,b₂] where b₁ is Element of (X), b₂ is Element of bool X : b₁ is Relation-like b₂ -defined b₂ -valued total quasi_total V27() V29() Element of bool [:b₂,b₂:] } is set
(X) is functional non empty set
{ (Funcs ((X,b₁),(X,b₂))) where b₁, b₂ is Element of (X) : verum } is set
union { (Funcs ((X,b₁),(X,b₂))) where b₁, b₂ is Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not (X,b₂) = {} or (X,b₁) = {} ) & b₃ is Relation-like (X,b₁) -defined (X,b₂) -valued Function-like quasi_total Element of bool [:(X,b₁),(X,b₂):] & ( for b₄, b₅ being set holds
( not [b₄,b₅] in (X,b₁) or [(b₃ . b₄),(b₃ . b₅)] in (X,b₂) ) ) ) } is set
a is Element of (X)
(X,a) is Element of (X)
a `1 is set
(a `1) `1 is set
(X,(X,a)) is Element of (X)
[(X,a),(X,a)] is V15() set
{(X,a),(X,a)} is non empty set
{(X,a)} is non empty set
{{(X,a),(X,a)},{(X,a)}} is non empty set
(X,(X,a)) is Element of bool X
id (X,(X,a)) is Relation-like (X,(X,a)) -defined (X,(X,a)) -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:(X,(X,a)),(X,(X,a)):]
[:(X,(X,a)),(X,(X,a)):] is Relation-like set
bool [:(X,(X,a)),(X,(X,a)):] is non empty set
[[(X,a),(X,a)],(id (X,(X,a)))] is V15() set
{[(X,a),(X,a)],(id (X,(X,a)))} is non empty set
{[(X,a),(X,a)]} is Relation-like Function-like non empty set
{{[(X,a),(X,a)],(id (X,(X,a)))},{[(X,a),(X,a)]}} is non empty set
(X,(X,(X,a)),a) is Element of (X)
(X,a) is Element of (X)
(a `1) `2 is set
(X,(X,a)) is Element of (X)
[(X,a),(X,a)] is V15() set
{(X,a),(X,a)} is non empty set
{(X,a)} is non empty set
{{(X,a),(X,a)},{(X,a)}} is non empty set
(X,(X,a)) is Element of bool X
id (X,(X,a)) is Relation-like (X,(X,a)) -defined (X,(X,a)) -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:(X,(X,a)),(X,(X,a)):]
[:(X,(X,a)),(X,(X,a)):] is Relation-like set
bool [:(X,(X,a)),(X,(X,a)):] is non empty set
[[(X,a),(X,a)],(id (X,(X,a)))] is V15() set
{[(X,a),(X,a)],(id (X,(X,a)))} is non empty set
{[(X,a),(X,a)]} is Relation-like Function-like non empty set
{{[(X,a),(X,a)],(id (X,(X,a)))},{[(X,a),(X,a)]}} is non empty set
(X,a,(X,(X,a))) is Element of (X)
(X,(X,a)) `2 is Relation-like Function-like set
(X,(X,(X,a))) is Element of (X)
(X,(X,a)) `1 is set
((X,(X,a)) `1) `1 is set
a `2 is Relation-like Function-like set
[:(X,(X,a)),(X,(X,a)):] is Relation-like set
bool [:(X,(X,a)),(X,(X,a)):] is non empty set
proj2 (a `2) is set
proj1 (a `2) is set
(X,(X,(X,a))) is Element of (X)
((X,(X,a)) `1) `2 is set
(X,(X,(X,(X,a)),a)) is Element of (X)
(X,(X,(X,a)),a) `1 is set
((X,(X,(X,a)),a) `1) `2 is set
(X,(X,(X,a)),a) `2 is Relation-like Function-like set
((X,(X,a)) `2) * (a `2) is Relation-like Function-like set
(X,(X,(X,(X,a)),a)) is Element of (X)
((X,(X,(X,a)),a) `1) `1 is set
(X,(X,a)) `2 is Relation-like Function-like set
(X,(X,(X,a))) is Element of (X)
(X,(X,a)) `1 is set
((X,(X,a)) `1) `2 is set
(X,(X,(X,a))) is Element of (X)
((X,(X,a)) `1) `1 is set
(X,(X,a,(X,(X,a)))) is Element of (X)
(X,a,(X,(X,a))) `1 is set
((X,a,(X,(X,a))) `1) `2 is set
(X,a,(X,(X,a))) `2 is Relation-like Function-like set
(a `2) * ((X,(X,a)) `2) is Relation-like Function-like set
(X,(X,a,(X,(X,a)))) is Element of (X)
((X,a,(X,(X,a))) `1) `1 is set
X is set
(X) is non empty set
(X) is non empty set
(X) is non empty set
bool X is non empty set
{ (b₁) where b₁ is Element of bool X : verum } is set
union { (b₁) where b₁ is Element of bool X : verum } is set
{ [b₁,b₂] where b₁ is Element of (X), b₂ is Element of bool X : b₁ is Relation-like b₂ -defined b₂ -valued total quasi_total V27() V29() Element of bool [:b₂,b₂:] } is set
(X) is functional non empty set
{ (Funcs ((X,b₁),(X,b₂))) where b₁, b₂ is Element of (X) : verum } is set
union { (Funcs ((X,b₁),(X,b₂))) where b₁, b₂ is Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not (X,b₂) = {} or (X,b₁) = {} ) & b₃ is Relation-like (X,b₁) -defined (X,b₂) -valued Function-like quasi_total Element of bool [:(X,b₁),(X,b₂):] & ( for b₄, b₅ being set holds
( not [b₄,b₅] in (X,b₁) or [(b₃ . b₄),(b₃ . b₅)] in (X,b₂) ) ) ) } is set
[:(X),(X):] is Relation-like non empty set
bool [:(X),(X):] is non empty set
a is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]
aa is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]
ii is Element of (X)
a . ii is Element of (X)
(X,ii) is Element of (X)
ii `1 is set
(ii `1) `1 is set
aa . ii is Element of (X)
a is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]
aa is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]
ii is Element of (X)
a . ii is Element of (X)
(X,ii) is Element of (X)
ii `1 is set
(ii `1) `2 is set
aa . ii is Element of (X)
[:(X),(X):] is Relation-like non empty set
[:[:(X),(X):],(X):] is Relation-like non empty set
bool [:[:(X),(X):],(X):] is non empty set
a is set
aa is set
ii is set
ii is set
gg is Element of (X)
c₆ is Element of (X)
(X,gg,c₆) is Element of (X)
a is set
aa is set
ii is set
c₆ is Element of (X)
ii is Element of (X)
(X,c₆,ii) is Element of (X)
a is Relation-like [:(X),(X):] -defined (X) -valued Function-like Element of bool [:[:(X),(X):],(X):]
dom a is Relation-like (X) -defined (X) -valued Element of bool [:(X),(X):]
bool [:(X),(X):] is non empty set
aa is Element of (X)
(X,aa) is Element of (X)
aa `1 is set
(aa `1) `1 is set
ii is Element of (X)
[aa,ii] is V15() set
{aa,ii} is non empty set
{aa} is non empty set
{{aa,ii},{aa}} is non empty set
(X,ii) is Element of (X)
ii `1 is set
(ii `1) `2 is set
ii is set
(X,ii,aa) is Element of (X)
ii is Element of (X)
c₆ is Element of (X)
(X,ii) is Element of (X)
ii `1 is set
(ii `1) `1 is set
(X,c<sub>6</sub>) is Element of (X)
c<sub>6</sub> `1 is set
(c₆ `1) `2 is set
(X,c₆,ii) is Element of (X)
aa is Element of (X)
(X,aa) is Element of (X)
aa `1 is set
(aa `1) `1 is set
ii is Element of (X)
(X,ii) is Element of (X)
ii `1 is set
(ii `1) `2 is set
[aa,ii] is V15() set
{aa,ii} is non empty set
{aa} is non empty set
{{aa,ii},{aa}} is non empty set
a . [aa,ii] is set
(X,ii,aa) is Element of (X)
a . (aa,ii) is set
ii is Element of (X)
c₆ is Element of (X)
(X,ii) is Element of (X)
ii `1 is set
(ii `1) `1 is set
(X,c<sub>6</sub>) is Element of (X)
c<sub>6</sub> `1 is set
(c₆ `1) `2 is set
(X,c₆,ii) is Element of (X)
a is Relation-like [:(X),(X):] -defined (X) -valued Function-like Element of bool [:[:(X),(X):],(X):]
dom a is Relation-like (X) -defined (X) -valued Element of bool [:(X),(X):]
bool [:(X),(X):] is non empty set
aa is Relation-like [:(X),(X):] -defined (X) -valued Function-like Element of bool [:[:(X),(X):],(X):]
dom aa is Relation-like (X) -defined (X) -valued Element of bool [:(X),(X):]
ii is set
ii is set
[ii,ii] is V15() set
{ii,ii} is non empty set
{ii} is non empty set
{{ii,ii},{ii}} is non empty set
c₆ is Element of (X)
(X,c₆) is Element of (X)
c₆ `1 is set
(c<sub>6</sub> `1) `1 is set
gg is Element of (X)
(X,gg) is Element of (X)
gg `1 is set
(gg `1) `2 is set
c₆ is Element of (X)
(X,c₆) is Element of (X)
c₆ `1 is set
(c<sub>6</sub> `1) `1 is set
gg is Element of (X)
(X,gg) is Element of (X)
gg `1 is set
(gg `1) `2 is set
ii is Element of [:(X),(X):]
ii is Element of (X)
c₆ is Element of (X)
[ii,c₆] is V15() set
{ii,c₆} is non empty set
{ii} is non empty set
{{ii,c₆},{ii}} is non empty set
(X,ii) is Element of (X)
ii `1 is set
(ii `1) `1 is set
(X,c<sub>6</sub>) is Element of (X)
c<sub>6</sub> `1 is set
(c₆ `1) `2 is set
a . [ii,c₆] is set
(X,c₆,ii) is Element of (X)
a . ii is set
aa . ii is set
X is set
(X) is non empty set
(X) is non empty set
bool X is non empty set
{ (b₁) where b₁ is Element of bool X : verum } is set
union { (b₁) where b₁ is Element of bool X : verum } is set
{ [b₁,b₂] where b₁ is Element of (X), b₂ is Element of bool X : b₁ is Relation-like b₂ -defined b₂ -valued total quasi_total V27() V29() Element of bool [:b₂,b₂:] } is set
(X) is non empty set
(X) is functional non empty set
{ (Funcs ((X,b₁),(X,b₂))) where b₁, b₂ is Element of (X) : verum } is set
union { (Funcs ((X,b₁),(X,b₂))) where b₁, b₂ is Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not (X,b₂) = {} or (X,b₁) = {} ) & b₃ is Relation-like (X,b₁) -defined (X,b₂) -valued Function-like quasi_total Element of bool [:(X,b₁),(X,b₂):] & ( for b₄, b₅ being set holds
( not [b₄,b₅] in (X,b₁) or [(b₃ . b₄),(b₃ . b₅)] in (X,b₂) ) ) ) } is set
(X) is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]
[:(X),(X):] is Relation-like non empty set
bool [:(X),(X):] is non empty set
(X) is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]
(X) is Relation-like [:(X),(X):] -defined (X) -valued Function-like Element of bool [:[:(X),(X):],(X):]
[:(X),(X):] is Relation-like non empty set
[:[:(X),(X):],(X):] is Relation-like non empty set
bool [:[:(X),(X):],(X):] is non empty set
CatStr(# (X),(X),(X),(X),(X) #) is non empty non void strict CatStr
X is set
(X) is non empty non void strict CatStr
(X) is non empty set
(X) is non empty set
bool X is non empty set
{ (b₁) where b₁ is Element of bool X : verum } is set
union { (b₁) where b₁ is Element of bool X : verum } is set
{ [b₁,b₂] where b₁ is Element of (X), b₂ is Element of bool X : b₁ is Relation-like b₂ -defined b₂ -valued total quasi_total V27() V29() Element of bool [:b₂,b₂:] } is set
(X) is non empty set
(X) is functional non empty set
{ (Funcs ((X,b₁),(X,b₂))) where b₁, b₂ is Element of (X) : verum } is set
union { (Funcs ((X,b₁),(X,b₂))) where b₁, b₂ is Element of (X) : verum } is set
{ [[b₁,b₂],b₃] where b₁, b₂ is Element of (X), b₃ is Relation-like Function-like Element of (X) : ( ( not (X,b₂) = {} or (X,b₁) = {} ) & b₃ is Relation-like (X,b₁) -defined (X,b₂) -valued Function-like quasi_total Element of bool [:(X,b₁),(X,b₂):] & ( for b₄, b₅ being set holds
( not [b₄,b₅] in (X,b₁) or [(b₃ . b₄),(b₃ . b₅)] in (X,b₂) ) ) ) } is set
(X) is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]
[:(X),(X):] is Relation-like non empty set
bool [:(X),(X):] is non empty set
(X) is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]
(X) is Relation-like [:(X),(X):] -defined (X) -valued Function-like Element of bool [:[:(X),(X):],(X):]
[:(X),(X):] is Relation-like non empty set
[:[:(X),(X):],(X):] is Relation-like non empty set
bool [:[:(X),(X):],(X):] is non empty set
CatStr(# (X),(X),(X),(X),(X) #) is non empty non void strict CatStr
the carrier' of (X) is set
aa is Element of the carrier' of (X)
gg is Element of the carrier' of (X)
[aa,gg] is V15() set
{aa,gg} is non empty set
{aa} is non empty set
{{aa,gg},{aa}} is non empty set
the Comp of (X) is Relation-like [: the carrier' of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like Element of bool [:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):]
[: the carrier' of (X), the carrier' of (X):] is Relation-like set
[:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):] is Relation-like set
bool [:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):] is non empty set
proj1 the Comp of (X) is Relation-like set
dom aa is Element of the carrier of (X)
the carrier of (X) is set
the Source of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
[: the carrier' of (X), the carrier of (X):] is Relation-like set
bool [: the carrier' of (X), the carrier of (X):] is non empty set
the Source of (X) . aa is Element of the carrier of (X)
cod gg is Element of the carrier of (X)
the Target of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
the Target of (X) . gg is Element of the carrier of (X)
f is Element of (X)
(X) . f is Element of (X)
(X,f) is Element of (X)
f `1 is set
(f `1) `1 is set
ii is Element of (X)
(X) . ii is Element of (X)
(X,ii) is Element of (X)
ii `1 is set
(ii `1) `2 is set
the carrier' of (X) is set
aa is Element of the carrier' of (X)
dom aa is Element of the carrier of (X)
the carrier of (X) is set
the Source of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
[: the carrier' of (X), the carrier of (X):] is Relation-like set
bool [: the carrier' of (X), the carrier of (X):] is non empty set
the Source of (X) . aa is Element of the carrier of (X)
gg is Element of the carrier' of (X)
cod gg is Element of the carrier of (X)
the Target of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
the Target of (X) . gg is Element of the carrier of (X)
aa (*) gg is Element of the carrier' of (X)
dom (aa (*) gg) is Element of the carrier of (X)
the Source of (X) . (aa (*) gg) is Element of the carrier of (X)
dom gg is Element of the carrier of (X)
the Source of (X) . gg is Element of the carrier of (X)
cod (aa (*) gg) is Element of the carrier of (X)
the Target of (X) . (aa (*) gg) is Element of the carrier of (X)
cod aa is Element of the carrier of (X)
the Target of (X) . aa is Element of the carrier of (X)
[aa,gg] is V15() set
{aa,gg} is non empty set
{aa} is non empty set
{{aa,gg},{aa}} is non empty set
[: the carrier' of (X), the carrier' of (X):] is Relation-like set
the Comp of (X) is Relation-like [: the carrier' of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like Element of bool [:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):]
[:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):] is Relation-like set
bool [:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):] is non empty set
dom the Comp of (X) is Relation-like the carrier' of (X) -defined the carrier' of (X) -valued Element of bool [: the carrier' of (X), the carrier' of (X):]
bool [: the carrier' of (X), the carrier' of (X):] is non empty set
the Comp of (X) . (aa,gg) is set
the Comp of (X) . [aa,gg] is set
f is Element of (X)
(X) . f is Element of (X)
(X,f) is Element of (X)
f `1 is set
(f `1) `1 is set
ii is Element of (X)
(X) . ii is Element of (X)
(X,ii) is Element of (X)
ii `1 is set
(ii `1) `2 is set
[f,ii] is V15() set
{f,ii} is non empty set
{f} is non empty set
{{f,ii},{f}} is non empty set
(X) . [f,ii] is set
(X,ii,f) is Element of (X)
(X) . ii is Element of (X)
(X,ii) is Element of (X)
(ii `1) `1 is set
(X) . f is Element of (X)
(X,f) is Element of (X)
(f `1) `2 is set
(X,(X,ii,f)) is Element of (X)
(X,ii,f) `1 is set
((X,ii,f) `1) `1 is set
(X,(X,ii,f)) is Element of (X)
((X,ii,f) `1) `2 is set
the carrier' of (X) is set
ii is Element of the carrier' of (X)
dom ii is Element of the carrier of (X)
the carrier of (X) is set
the Source of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
[: the carrier' of (X), the carrier of (X):] is Relation-like set
bool [: the carrier' of (X), the carrier of (X):] is non empty set
the Source of (X) . ii is Element of the carrier of (X)
aa is Element of the carrier' of (X)
cod aa is Element of the carrier of (X)
the Target of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
the Target of (X) . aa is Element of the carrier of (X)
dom aa is Element of the carrier of (X)
the Source of (X) . aa is Element of the carrier of (X)
gg is Element of the carrier' of (X)
cod gg is Element of the carrier of (X)
the Target of (X) . gg is Element of the carrier of (X)
aa (*) gg is Element of the carrier' of (X)
ii (*) (aa (*) gg) is Element of the carrier' of (X)
ii (*) aa is Element of the carrier' of (X)
(ii (*) aa) (*) gg is Element of the carrier' of (X)
h is Element of (X)
(X,h) is Element of (X)
h `1 is set
(h `1) `1 is set
(X) . h is Element of (X)
g is Element of (X)
(X,g) is Element of (X)
g `1 is set
(g `1) `2 is set
(X) . g is Element of (X)
(X,g,h) is Element of (X)
(X,(X,g,h)) is Element of (X)
(X,g,h) `1 is set
((X,g,h) `1) `1 is set
(X,g) is Element of (X)
(g `1) `1 is set
(X) . g is Element of (X)
f is Element of (X)
(X,f) is Element of (X)
f `1 is set
(f `1) `2 is set
(X) . f is Element of (X)
(X,f,g) is Element of (X)
(X,(X,f,g)) is Element of (X)
(X,f,g) `1 is set
((X,f,g) `1) `2 is set
[ii,aa] is V15() set
{ii,aa} is non empty set
{ii} is non empty set
{{ii,aa},{ii}} is non empty set
[: the carrier' of (X), the carrier' of (X):] is Relation-like set
the Comp of (X) is Relation-like [: the carrier' of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like Element of bool [:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):]
[:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):] is Relation-like set
bool [:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):] is non empty set
dom the Comp of (X) is Relation-like the carrier' of (X) -defined the carrier' of (X) -valued Element of bool [: the carrier' of (X), the carrier' of (X):]
bool [: the carrier' of (X), the carrier' of (X):] is non empty set
the Comp of (X) . (ii,aa) is set
the Comp of (X) . [ii,aa] is set
[aa,gg] is V15() set
{aa,gg} is non empty set
{aa} is non empty set
{{aa,gg},{aa}} is non empty set
the Comp of (X) . (aa,gg) is set
the Comp of (X) . [aa,gg] is set
dom (ii (*) aa) is Element of the carrier of (X)
the Source of (X) . (ii (*) aa) is Element of the carrier of (X)
[(ii (*) aa),gg] is V15() set
{(ii (*) aa),gg} is non empty set
{(ii (*) aa)} is non empty set
{{(ii (*) aa),gg},{(ii (*) aa)}} is non empty set
cod (aa (*) gg) is Element of the carrier of (X)
the Target of (X) . (aa (*) gg) is Element of the carrier of (X)
[ii,(aa (*) gg)] is V15() set
{ii,(aa (*) gg)} is non empty set
{{ii,(aa (*) gg)},{ii}} is non empty set
the Comp of (X) . (ii,( the Comp of (X) . (aa,gg))) is set
[ii,( the Comp of (X) . (aa,gg))] is V15() set
{ii,( the Comp of (X) . (aa,gg))} is non empty set
{{ii,( the Comp of (X) . (aa,gg))},{ii}} is non empty set
the Comp of (X) . [ii,( the Comp of (X) . (aa,gg))] is set
[h,(X,f,g)] is V15() set
{h,(X,f,g)} is non empty set
{h} is non empty set
{{h,(X,f,g)},{h}} is non empty set
(X) . [h,(X,f,g)] is set
(X,(X,f,g),h) is Element of (X)
(X,f,(X,g,h)) is Element of (X)
[(X,g,h),f] is V15() set
{(X,g,h),f} is non empty set
{(X,g,h)} is non empty set
{{(X,g,h),f},{(X,g,h)}} is non empty set
(X) . [(X,g,h),f] is set
the Comp of (X) . (( the Comp of (X) . (ii,aa)),gg) is set
[( the Comp of (X) . (ii,aa)),gg] is V15() set
{( the Comp of (X) . (ii,aa)),gg} is non empty set
{( the Comp of (X) . (ii,aa))} is non empty set
{{( the Comp of (X) . (ii,aa)),gg},{( the Comp of (X) . (ii,aa))}} is non empty set
the Comp of (X) . [( the Comp of (X) . (ii,aa)),gg] is set
the carrier of (X) is set
gg is Element of the carrier of (X)
Hom (gg,gg) is Element of bool the carrier' of (X)
the carrier' of (X) is set
bool the carrier' of (X) is non empty set
{ b₁ where b₁ is Element of the carrier' of (X) : ( dom b₁ = gg & cod b₁ = gg ) } is set
aa is Element of (X)
(X,aa) is Element of (X)
[aa,aa] is V15() set
{aa,aa} is non empty set
{aa} is non empty set
{{aa,aa},{aa}} is non empty set
(X,aa) is Element of bool X
id (X,aa) is Relation-like (X,aa) -defined (X,aa) -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:(X,aa),(X,aa):]
[:(X,aa),(X,aa):] is Relation-like set
bool [:(X,aa),(X,aa):] is non empty set
[[aa,aa],(id (X,aa))] is V15() set
{[aa,aa],(id (X,aa))} is non empty set
{[aa,aa]} is Relation-like Function-like non empty set
{{[aa,aa],(id (X,aa))},{[aa,aa]}} is non empty set
ii is Element of the carrier' of (X)
cod ii is Element of the carrier of (X)
the Target of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
[: the carrier' of (X), the carrier of (X):] is Relation-like set
bool [: the carrier' of (X), the carrier of (X):] is non empty set
the Target of (X) . ii is Element of the carrier of (X)
(X,(X,aa)) is Element of (X)
(X,aa) `1 is set
((X,aa) `1) `2 is set
dom ii is Element of the carrier of (X)
the Source of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
the Source of (X) . ii is Element of the carrier of (X)
(X,(X,aa)) is Element of (X)
((X,aa) `1) `1 is set
X is set
(X) is non empty non void strict Category-like transitive associative reflexive CatStr
(X) is non empty set
(X) is non empty set
bool X is non empty set
{ (b<sub>1</sub>) where b<sub>1</sub> is Element of bool X : verum } is set
union { (b<sub>1</sub>) where b<sub>1</sub> is Element of bool X : verum } is set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub> is Element of (X), b<sub>2</sub> is Element of bool X : b<sub>1</sub> is Relation-like b<sub>2</sub> -defined b<sub>2</sub> -valued total quasi_total V27() V29() Element of bool [:b<sub>2</sub>,b<sub>2</sub>:] } is set
(X) is non empty set
(X) is functional non empty set
{ (Funcs ((X,b<sub>1</sub>),(X,b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : verum } is set
union { (Funcs ((X,b<sub>1</sub>),(X,b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : verum } is set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of (X), b<sub>3</sub> is Relation-like Function-like Element of (X) : ( ( not (X,b<sub>2</sub>) = {} or (X,b<sub>1</sub>) = {} ) & b<sub>3</sub> is Relation-like (X,b<sub>1</sub>) -defined (X,b<sub>2</sub>) -valued Function-like quasi_total Element of bool [:(X,b<sub>1</sub>),(X,b<sub>2</sub>):] & ( for b<sub>4</sub>, b<sub>5</sub> being set holds
( not [b<sub>4</sub>,b<sub>5</sub>] in (X,b<sub>1</sub>) or [(b<sub>3</sub> . b<sub>4</sub>),(b<sub>3</sub> . b<sub>5</sub>)] in (X,b<sub>2</sub>) ) ) ) } is set
(X) is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]
[:(X),(X):] is Relation-like non empty set
bool [:(X),(X):] is non empty set
(X) is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]
(X) is Relation-like [:(X),(X):] -defined (X) -valued Function-like Element of bool [:[:(X),(X):],(X):]
[:(X),(X):] is Relation-like non empty set
[:[:(X),(X):],(X):] is Relation-like non empty set
bool [:[:(X),(X):],(X):] is non empty set
CatStr(# (X),(X),(X),(X),(X) #) is non empty non void strict CatStr
the carrier of (X) is set
a is Element of the carrier of (X)
aa is Element of (X)
(X,aa) is Element of (X)
[aa,aa] is V15() set
{aa,aa} is non empty set
{aa} is non empty set
{{aa,aa},{aa}} is non empty set
(X,aa) is Element of bool X
id (X,aa) is Relation-like (X,aa) -defined (X,aa) -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:(X,aa),(X,aa):]
[:(X,aa),(X,aa):] is Relation-like set
bool [:(X,aa),(X,aa):] is non empty set
[[aa,aa],(id (X,aa))] is V15() set
{[aa,aa],(id (X,aa))} is non empty set
{[aa,aa]} is Relation-like Function-like non empty set
{{[aa,aa],(id (X,aa))},{[aa,aa]}} is non empty set
ii is Morphism of a,a
ii is Element of the carrier of (X)
Hom (a,ii) is Element of bool the carrier' of (X)
the carrier' of (X) is set
bool the carrier' of (X) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier' of (X) : ( dom b<sub>1</sub> = a & cod b<sub>1</sub> = ii ) } is set
Hom (ii,a) is Element of bool the carrier' of (X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier' of (X) : ( dom b<sub>1</sub> = ii & cod b<sub>1</sub> = a ) } is set
c<sub>6</sub> is Morphism of a,ii
c<sub>6</sub> (*) ii is Element of the carrier' of (X)
Hom (a,a) is non empty Element of bool the carrier' of (X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier' of (X) : ( dom b<sub>1</sub> = a & cod b<sub>1</sub> = a ) } is set
cod ii is Element of the carrier of (X)
the Target of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
[: the carrier' of (X), the carrier of (X):] is Relation-like set
bool [: the carrier' of (X), the carrier of (X):] is non empty set
the Target of (X) . ii is Element of the carrier of (X)
dom c<sub>6</sub> is Element of the carrier of (X)
the Source of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
the Source of (X) . c<sub>6</sub> is Element of the carrier of (X)
gg is Element of (X)
(X,gg) is Element of (X)
gg `1 is set
(gg `1) `1 is set
(X,(X,aa)) is Element of (X)
(X,aa) `1 is set
((X,aa) `1) `2 is set
[c<sub>6</sub>,ii] is V15() set
{c<sub>6</sub>,ii} is non empty set
{c<sub>6</sub>} is non empty set
{{c<sub>6</sub>,ii},{c<sub>6</sub>}} is non empty set
[: the carrier' of (X), the carrier' of (X):] is Relation-like set
the Comp of (X) is Relation-like [: the carrier' of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like Element of bool [:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):]
[:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):] is Relation-like set
bool [:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):] is non empty set
dom the Comp of (X) is Relation-like the carrier' of (X) -defined the carrier' of (X) -valued Element of bool [: the carrier' of (X), the carrier' of (X):]
bool [: the carrier' of (X), the carrier' of (X):] is non empty set
the Comp of (X) . (c<sub>6</sub>,ii) is set
the Comp of (X) . [c<sub>6</sub>,ii] is set
(X,(X,aa),gg) is Element of (X)
c<sub>6</sub> is Morphism of ii,a
ii (*) c<sub>6</sub> is Element of the carrier' of (X)
Hom (a,a) is non empty Element of bool the carrier' of (X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier' of (X) : ( dom b<sub>1</sub> = a & cod b<sub>1</sub> = a ) } is set
dom ii is Element of the carrier of (X)
the Source of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
[: the carrier' of (X), the carrier of (X):] is Relation-like set
bool [: the carrier' of (X), the carrier of (X):] is non empty set
the Source of (X) . ii is Element of the carrier of (X)
cod c<sub>6</sub> is Element of the carrier of (X)
the Target of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
the Target of (X) . c<sub>6</sub> is Element of the carrier of (X)
gg is Element of (X)
(X,gg) is Element of (X)
gg `1 is set
(gg `1) `2 is set
(X,(X,aa)) is Element of (X)
(X,aa) `1 is set
((X,aa) `1) `1 is set
[ii,c<sub>6</sub>] is V15() set
{ii,c<sub>6</sub>} is non empty set
{ii} is non empty set
{{ii,c<sub>6</sub>},{ii}} is non empty set
[: the carrier' of (X), the carrier' of (X):] is Relation-like set
the Comp of (X) is Relation-like [: the carrier' of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like Element of bool [:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):]
[:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):] is Relation-like set
bool [:[: the carrier' of (X), the carrier' of (X):], the carrier' of (X):] is non empty set
dom the Comp of (X) is Relation-like the carrier' of (X) -defined the carrier' of (X) -valued Element of bool [: the carrier' of (X), the carrier' of (X):]
bool [: the carrier' of (X), the carrier' of (X):] is non empty set
the Comp of (X) . (ii,c<sub>6</sub>) is set
the Comp of (X) . [ii,c<sub>6</sub>] is set
(X,gg,(X,aa)) is Element of (X)
X is set
(X) is non empty non void strict Category-like transitive associative reflexive CatStr
(X) is non empty set
(X) is non empty set
bool X is non empty set
{ (b<sub>1</sub>) where b<sub>1</sub> is Element of bool X : verum } is set
union { (b<sub>1</sub>) where b<sub>1</sub> is Element of bool X : verum } is set
{ [b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub> is Element of (X), b<sub>2</sub> is Element of bool X : b<sub>1</sub> is Relation-like b<sub>2</sub> -defined b<sub>2</sub> -valued total quasi_total V27() V29() Element of bool [:b<sub>2</sub>,b<sub>2</sub>:] } is set
(X) is non empty set
(X) is functional non empty set
{ (Funcs ((X,b<sub>1</sub>),(X,b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : verum } is set
union { (Funcs ((X,b<sub>1</sub>),(X,b<sub>2</sub>))) where b<sub>1</sub>, b<sub>2</sub> is Element of (X) : verum } is set
{ [[b<sub>1</sub>,b<sub>2</sub>],b<sub>3</sub>] where b<sub>1</sub>, b<sub>2</sub> is Element of (X), b<sub>3</sub> is Relation-like Function-like Element of (X) : ( ( not (X,b<sub>2</sub>) = {} or (X,b<sub>1</sub>) = {} ) & b<sub>3</sub> is Relation-like (X,b<sub>1</sub>) -defined (X,b<sub>2</sub>) -valued Function-like quasi_total Element of bool [:(X,b<sub>1</sub>),(X,b<sub>2</sub>):] & ( for b<sub>4</sub>, b<sub>5</sub> being set holds
( not [b<sub>4</sub>,b<sub>5</sub>] in (X,b<sub>1</sub>) or [(b<sub>3</sub> . b<sub>4</sub>),(b<sub>3</sub> . b<sub>5</sub>)] in (X,b<sub>2</sub>) ) ) ) } is set
(X) is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]
[:(X),(X):] is Relation-like non empty set
bool [:(X),(X):] is non empty set
(X) is Relation-like (X) -defined (X) -valued Function-like non empty total quasi_total Element of bool [:(X),(X):]
(X) is Relation-like [:(X),(X):] -defined (X) -valued Function-like Element of bool [:[:(X),(X):],(X):]
[:(X),(X):] is Relation-like non empty set
[:[:(X),(X):],(X):] is Relation-like non empty set
bool [:[:(X),(X):],(X):] is non empty set
CatStr(# (X),(X),(X),(X),(X) #) is non empty non void strict CatStr
the carrier of (X) is set
a is Element of the carrier of (X)
the carrier' of (X) is set
aa is Element of (X)
(X,aa) is Element of (X)
[aa,aa] is V15() set
{aa,aa} is non empty set
{aa} is non empty set
{{aa,aa},{aa}} is non empty set
(X,aa) is Element of bool X
id (X,aa) is Relation-like (X,aa) -defined (X,aa) -valued Function-like one-to-one total quasi_total onto bijective V27() V29() V30() V34() Element of bool [:(X,aa),(X,aa):]
[:(X,aa),(X,aa):] is Relation-like set
bool [:(X,aa),(X,aa):] is non empty set
[[aa,aa],(id (X,aa))] is V15() set
{[aa,aa],(id (X,aa))} is non empty set
{[aa,aa]} is Relation-like Function-like non empty set
{{[aa,aa],(id (X,aa))},{[aa,aa]}} is non empty set
ii is Element of the carrier' of (X)
cod ii is Element of the carrier of (X)
the Target of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
[: the carrier' of (X), the carrier of (X):] is Relation-like set
bool [: the carrier' of (X), the carrier of (X):] is non empty set
the Target of (X) . ii is Element of the carrier of (X)
(X,(X,aa)) is Element of (X)
(X,aa) `1 is set
((X,aa) `1) `2 is set
dom ii is Element of the carrier of (X)
the Source of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
the Source of (X) . ii is Element of the carrier of (X)
(X,(X,aa)) is Element of (X)
((X,aa) `1) `1 is set
Hom (a,a) is non empty Element of bool the carrier' of (X)
bool the carrier' of (X) is non empty set
{ b₁ where b₁ is Element of the carrier' of (X) : ( dom b₁ = a & cod b₁ = a ) } is set
ii is Morphism of a,a
c₆ is Element of the carrier of (X)
aa is Element of the carrier of (X)
Hom (a,c₆) is Element of bool the carrier' of (X)
{ b₁ where b₁ is Element of the carrier' of (X) : ( dom b₁ = a & cod b₁ = c₆ ) } is set
gg is Morphism of a,c₆
gg (*) ii is Element of the carrier' of (X)
Hom (aa,a) is Element of bool the carrier' of (X)
{ b₁ where b₁ is Element of the carrier' of (X) : ( dom b₁ = aa & cod b₁ = a ) } is set
ii is Morphism of aa,a
ii (*) ii is Element of the carrier' of (X)