:: ORDERS_1 semantic presentation

{} is empty Relation-like non-empty empty-yielding reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V45() set
the empty Relation-like non-empty empty-yielding reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V45() set is empty Relation-like non-empty empty-yielding reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V45() set
O is set
union O is set
A is set
the Element of A is Element of A
the Element of union O is Element of union O
g is set
O is non empty set
union O is set
[:O,(union O):] is Relation-like set
bool [:O,(union O):] is non empty set
the Element of O is Element of O
g is Relation-like Function-like set
dom g is set
rng g is set
ff is set
AA is non empty set
Y is set
z is set
g . z is set
{z} is non empty finite set
[:{z},z:] is Relation-like set
ff /\ Y is set
the Element of ff /\ Y is Element of ff /\ Y
AA9 is set
g . AA9 is set
{AA9} is non empty finite set
[:{AA9},AA9:] is Relation-like set
{AA9} /\ {z} is finite set
AA9 /\ z is set
f9 is set
x is set
[f9,x] is V35() set
{f9,x} is non empty finite set
{f9} is non empty finite set
{{f9,x},{f9}} is non empty finite V45() set
ff is set
Y is set
g . Y is set
{Y} is non empty finite set
[:{Y},Y:] is Relation-like set
ff is set
Y is set
Y /\ ff is set
ff /\ Y is set
z is set
{z} is non empty finite set
Y is set
Y /\ ff is set
z is set
y is set
ff /\ Y is set
AA9 is set
{AA9} is non empty finite set
Y is Relation-like Function-like set
dom Y is set
rng Y is set
union AA is set
z is set
y is set
Y . y is set
y /\ ff is set
g . the Element of O is set
z is set
y is set
g . y is set
[:O,AA:] is non empty Relation-like set
bool [:O,AA:] is non empty set
f9 is Relation-like Function-like set
dom f9 is set
rng f9 is set
x is set
y is set
f9 . y is set
z is set
AA9 is non empty Relation-like O -defined AA -valued Function-like total V38(O,AA) Element of bool [:O,AA:]
dom AA9 is non empty Element of bool O
bool O is non empty set
a is set
AA9 . a is set
{a} is non empty finite set
[:{a},a:] is Relation-like set
P2 is set
y9 is set
[P2,y9] is V35() set
{P2,y9} is non empty finite set
{P2} is non empty finite set
{{P2,y9},{P2}} is non empty finite V45() set
[P2,y9] `2 is set
{y} is non empty finite set
[:{y},y:] is Relation-like set
[:AA,(union AA):] is Relation-like set
bool [:AA,(union AA):] is non empty set
[:(union AA),(union O):] is Relation-like set
bool [:(union AA),(union O):] is non empty set
AA9 is non empty Relation-like O -defined AA -valued Function-like total V38(O,AA) Element of bool [:O,AA:]
x is Relation-like AA -defined union AA -valued Function-like V38(AA, union AA) Element of bool [:AA,(union AA):]
x * AA9 is Relation-like O -defined union AA -valued Function-like V38(O, union AA) Element of bool [:O,(union AA):]
[:O,(union AA):] is Relation-like set
bool [:O,(union AA):] is non empty set
dom (x * AA9) is Element of bool O
bool O is non empty set
y is Relation-like union AA -defined union O -valued Function-like V38( union AA, union O) Element of bool [:(union AA),(union O):]
y * (x * AA9) is Relation-like O -defined union O -valued Function-like Element of bool [:O,(union O):]
z is Relation-like O -defined union O -valued Function-like V38(O, union O) Element of bool [:O,(union O):]
a is set
z . a is set
AA9 . a is set
{a} is non empty finite set
[:{a},a:] is Relation-like set
x . (AA9 . a) is set
rng x is Element of bool (union AA)
bool (union AA) is non empty set
y . (x . (AA9 . a)) is set
(x . (AA9 . a)) `2 is set
(AA9 . a) /\ ff is set
y9 is set
z is set
[y9,z] is V35() set
{y9,z} is non empty finite set
{y9} is non empty finite set
{{y9,z},{y9}} is non empty finite V45() set
(x * AA9) . a is set
O is set
bool O is non empty set
bool O is non empty Element of bool (bool O)
bool (bool O) is non empty set
{{}} is non empty functional finite V45() set
(bool O) \ {{}} is Element of bool (bool O)
O is non empty set
(O) is set
bool O is non empty set
bool O is non empty Element of bool (bool O)
bool (bool O) is non empty set
(bool O) \ {{}} is Element of bool (bool O)
O is non empty set
(O) is non empty set
bool O is non empty set
bool O is non empty Element of bool (bool O)
bool (bool O) is non empty set
(bool O) \ {{}} is Element of bool (bool O)
O is set
(O) is set
bool O is non empty set
bool O is non empty Element of bool (bool O)
bool (bool O) is non empty set
(bool O) \ {{}} is Element of bool (bool O)
A is non empty set
O is set
[:O,O:] is Relation-like set
bool [:O,O:] is non empty set
A is Relation-like O -defined O -valued total V38(O,O) Element of bool [:O,O:]
field A is set
dom A is set
rng A is set
(dom A) \/ (rng A) is set
rng A is Element of bool O
bool O is non empty set
O \/ (rng A) is set
O is set
[:O,O:] is Relation-like set
bool [:O,O:] is non empty set
A is set
[A,A] is V35() set
{A,A} is non empty finite set
{A} is non empty finite set
{{A,A},{A}} is non empty finite V45() set
g is Relation-like O -defined O -valued reflexive antisymmetric transitive total V38(O,O) Element of bool [:O,O:]
field g is set
dom g is set
rng g is set
(dom g) \/ (rng g) is set
O is set
[:O,O:] is Relation-like set
bool [:O,O:] is non empty set
A is set
g is set
[A,g] is V35() set
{A,g} is non empty finite set
{A} is non empty finite set
{{A,g},{A}} is non empty finite V45() set
[g,A] is V35() set
{g,A} is non empty finite set
{g} is non empty finite set
{{g,A},{g}} is non empty finite V45() set
AA is Relation-like O -defined O -valued reflexive antisymmetric transitive total V38(O,O) Element of bool [:O,O:]
field AA is set
dom AA is set
rng AA is set
(dom AA) \/ (rng AA) is set
O is set
[:O,O:] is Relation-like set
bool [:O,O:] is non empty set
A is set
g is set
[A,g] is V35() set
{A,g} is non empty finite set
{A} is non empty finite set
{{A,g},{A}} is non empty finite V45() set
AA is set
[g,AA] is V35() set
{g,AA} is non empty finite set
{g} is non empty finite set
{{g,AA},{g}} is non empty finite V45() set
[A,AA] is V35() set
{A,AA} is non empty finite set
{{A,AA},{A}} is non empty finite V45() set
ff is Relation-like O -defined O -valued reflexive antisymmetric transitive total V38(O,O) Element of bool [:O,O:]
field ff is set
dom ff is set
rng ff is set
(dom ff) \/ (rng ff) is set
A is set
O is set
union O is set
g is set
union g is set
O is set
A is Relation-like set
g is set
[g,g] is V35() set
{g,g} is non empty finite set
{g} is non empty finite set
{{g,g},{g}} is non empty finite V45() set
g is set
AA is set
[g,AA] is V35() set
{g,AA} is non empty finite set
{g} is non empty finite set
{{g,AA},{g}} is non empty finite V45() set
[AA,g] is V35() set
{AA,g} is non empty finite set
{AA} is non empty finite set
{{AA,g},{AA}} is non empty finite V45() set
g is set
AA is set
[g,AA] is V35() set
{g,AA} is non empty finite set
{g} is non empty finite set
{{g,AA},{g}} is non empty finite V45() set
[AA,g] is V35() set
{AA,g} is non empty finite set
{AA} is non empty finite set
{{AA,g},{AA}} is non empty finite V45() set
O is set
A is set
g is Relation-like set
AA is set
[AA,AA] is V35() set
{AA,AA} is non empty finite set
{AA} is non empty finite set
{{AA,AA},{AA}} is non empty finite V45() set
O is set
A is set
g is Relation-like set
AA is set
ff is set
[AA,ff] is V35() set
{AA,ff} is non empty finite set
{AA} is non empty finite set
{{AA,ff},{AA}} is non empty finite V45() set
[ff,AA] is V35() set
{ff,AA} is non empty finite set
{ff} is non empty finite set
{{ff,AA},{ff}} is non empty finite V45() set
O is set
A is set
g is Relation-like set
AA is set
ff is set
[AA,ff] is V35() set
{AA,ff} is non empty finite set
{AA} is non empty finite set
{{AA,ff},{AA}} is non empty finite V45() set
Y is set
[ff,Y] is V35() set
{ff,Y} is non empty finite set
{ff} is non empty finite set
{{ff,Y},{ff}} is non empty finite V45() set
[AA,Y] is V35() set
{AA,Y} is non empty finite set
{{AA,Y},{AA}} is non empty finite V45() set
O is set
A is set
g is Relation-like set
AA is set
ff is set
[AA,ff] is V35() set
{AA,ff} is non empty finite set
{AA} is non empty finite set
{{AA,ff},{AA}} is non empty finite V45() set
[ff,AA] is V35() set
{ff,AA} is non empty finite set
{ff} is non empty finite set
{{ff,AA},{ff}} is non empty finite V45() set
O is set
[:O,O:] is Relation-like set
bool [:O,O:] is non empty set
A is Relation-like O -defined O -valued total V38(O,O) Element of bool [:O,O:]
field A is set
dom A is set
rng A is set
(dom A) \/ (rng A) is set
O is set
[:O,O:] is Relation-like set
bool [:O,O:] is non empty set
A is Relation-like O -defined O -valued Element of bool [:O,O:]
dom A is Element of bool O
bool O is non empty set
field A is set
dom A is set
rng A is set
(dom A) \/ (rng A) is set
g is set
[g,g] is V35() set
{g,g} is non empty finite set
{g} is non empty finite set
{{g,g},{g}} is non empty finite V45() set
rng A is Element of bool O
O \/ (rng A) is set
O is set
[:O,O:] is Relation-like set
bool [:O,O:] is non empty set
A is Relation-like O -defined O -valued reflexive antisymmetric transitive total V38(O,O) Element of bool [:O,O:]
dom A is Element of bool O
bool O is non empty set
rng A is Element of bool O
g is set
[g,g] is V35() set
{g,g} is non empty finite set
{g} is non empty finite set
{{g,g},{g}} is non empty finite V45() set
g is set
[g,g] is V35() set
{g,g} is non empty finite set
{g} is non empty finite set
{{g,g},{g}} is non empty finite V45() set
O is set
[:O,O:] is Relation-like set
bool [:O,O:] is non empty set
A is Relation-like O -defined O -valued reflexive antisymmetric transitive total V38(O,O) Element of bool [:O,O:]
field A is set
dom A is set
rng A is set
(dom A) \/ (rng A) is set
O \/ O is set
dom A is Element of bool O
bool O is non empty set
(dom A) \/ O is set
O is Relation-like set
O ~ is Relation-like set
O is Relation-like set
O ~ is Relation-like set
O is Relation-like set
O ~ is Relation-like set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
A is set
field (O ~) is set
dom (O ~) is set
rng (O ~) is set
(dom (O ~)) \/ (rng (O ~)) is set
g is set
[A,g] is V35() set
{A,g} is non empty finite set
{A} is non empty finite set
{{A,g},{A}} is non empty finite V45() set
[g,A] is V35() set
{g,A} is non empty finite set
{g} is non empty finite set
{{g,A},{g}} is non empty finite V45() set
O is Relation-like set
O ~ is Relation-like set
O is Relation-like set
O is Relation-like set
O is Relation-like set
O is set
[:O,O:] is Relation-like set
bool [:O,O:] is non empty set
A is Relation-like O -defined O -valued reflexive antisymmetric transitive total V38(O,O) Element of bool [:O,O:]
O is set
[:O,O:] is Relation-like set
bool [:O,O:] is non empty set
A is Relation-like O -defined O -valued reflexive antisymmetric transitive total V38(O,O) Element of bool [:O,O:]
O is set
[:O,O:] is Relation-like set
bool [:O,O:] is non empty set
A is Relation-like O -defined O -valued reflexive antisymmetric transitive total V38(O,O) Element of bool [:O,O:]
O is Relation-like set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
[:(field O),(field O):] is Relation-like set
A is set
g is set
[A,g] is V35() set
{A,g} is non empty finite set
{A} is non empty finite set
{{A,g},{A}} is non empty finite V45() set
O is Relation-like set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
A is set
O |_2 A is Relation-like set
[:A,A:] is Relation-like set
O /\ [:A,A:] is Relation-like set
field (O |_2 A) is set
dom (O |_2 A) is set
rng (O |_2 A) is set
(dom (O |_2 A)) \/ (rng (O |_2 A)) is set
g is set
g is set
[g,g] is V35() set
{g,g} is non empty finite set
{g} is non empty finite set
{{g,g},{g}} is non empty finite V45() set
O is Relation-like set
A is set
O |_2 A is Relation-like set
[:A,A:] is Relation-like set
O /\ [:A,A:] is Relation-like set
O is Relation-like set
A is set
O |_2 A is Relation-like set
[:A,A:] is Relation-like set
O /\ [:A,A:] is Relation-like set
O is Relation-like set
A is set
O |_2 A is Relation-like set
[:A,A:] is Relation-like set
O /\ [:A,A:] is Relation-like set
O is empty Relation-like non-empty empty-yielding reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V45() set
field O is finite set
dom O is empty Relation-like non-empty empty-yielding reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V45() set
rng O is empty trivial with_non-empty_elements Relation-like non-empty empty-yielding reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V45() set
(dom O) \/ (rng O) is Relation-like reflexive irreflexive symmetric finite V45() set
O is Relation-like set
A is set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
[A,A] is V35() set
{A,A} is non empty finite set
{A} is non empty finite set
{{A,A},{A}} is non empty finite V45() set
A is set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
g is set
[A,g] is V35() set
{A,g} is non empty finite set
{A} is non empty finite set
{{A,g},{A}} is non empty finite V45() set
AA is set
[g,AA] is V35() set
{g,AA} is non empty finite set
{g} is non empty finite set
{{g,AA},{g}} is non empty finite V45() set
[A,AA] is V35() set
{A,AA} is non empty finite set
{{A,AA},{A}} is non empty finite V45() set
A is set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
g is set
[A,g] is V35() set
{A,g} is non empty finite set
{A} is non empty finite set
{{A,g},{A}} is non empty finite V45() set
[g,A] is V35() set
{g,A} is non empty finite set
{g} is non empty finite set
{{g,A},{g}} is non empty finite V45() set
A is set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
g is set
[A,g] is V35() set
{A,g} is non empty finite set
{A} is non empty finite set
{{A,g},{A}} is non empty finite V45() set
[g,A] is V35() set
{g,A} is non empty finite set
{g} is non empty finite set
{{g,A},{g}} is non empty finite V45() set
A is set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
O is set
id O is Relation-like O -defined O -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total V38(O,O) V39(O) V40(O,O) Element of bool [:O,O:]
[:O,O:] is Relation-like set
bool [:O,O:] is non empty set
O is Relation-like set
A is set
O is Relation-like set
A is set
O is Relation-like set
A is set
O is Relation-like set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
O is Relation-like set
A is set
g is set
O is Relation-like set
A is set
O |_2 A is Relation-like set
[:A,A:] is Relation-like set
O /\ [:A,A:] is Relation-like set
g is set
field (O |_2 A) is set
dom (O |_2 A) is set
rng (O |_2 A) is set
(dom (O |_2 A)) \/ (rng (O |_2 A)) is set
[g,g] is V35() set
{g,g} is non empty finite set
{g} is non empty finite set
{{g,g},{g}} is non empty finite V45() set
O is Relation-like set
A is set
O |_2 A is Relation-like set
[:A,A:] is Relation-like set
O /\ [:A,A:] is Relation-like set
g is set
field (O |_2 A) is set
dom (O |_2 A) is set
rng (O |_2 A) is set
(dom (O |_2 A)) \/ (rng (O |_2 A)) is set
AA is set
[g,AA] is V35() set
{g,AA} is non empty finite set
{g} is non empty finite set
{{g,AA},{g}} is non empty finite V45() set
ff is set
[AA,ff] is V35() set
{AA,ff} is non empty finite set
{AA} is non empty finite set
{{AA,ff},{AA}} is non empty finite V45() set
[g,ff] is V35() set
{g,ff} is non empty finite set
{{g,ff},{g}} is non empty finite V45() set
O is Relation-like set
A is set
O |_2 A is Relation-like set
[:A,A:] is Relation-like set
O /\ [:A,A:] is Relation-like set
g is set
field (O |_2 A) is set
dom (O |_2 A) is set
rng (O |_2 A) is set
(dom (O |_2 A)) \/ (rng (O |_2 A)) is set
AA is set
[g,AA] is V35() set
{g,AA} is non empty finite set
{g} is non empty finite set
{{g,AA},{g}} is non empty finite V45() set
[AA,g] is V35() set
{AA,g} is non empty finite set
{AA} is non empty finite set
{{AA,g},{AA}} is non empty finite V45() set
O is Relation-like set
A is set
O |_2 A is Relation-like set
[:A,A:] is Relation-like set
O /\ [:A,A:] is Relation-like set
g is set
field (O |_2 A) is set
dom (O |_2 A) is set
rng (O |_2 A) is set
(dom (O |_2 A)) \/ (rng (O |_2 A)) is set
AA is set
[g,AA] is V35() set
{g,AA} is non empty finite set
{g} is non empty finite set
{{g,AA},{g}} is non empty finite V45() set
[AA,g] is V35() set
{AA,g} is non empty finite set
{AA} is non empty finite set
{{AA,g},{AA}} is non empty finite V45() set
O is Relation-like set
A is set
O |_2 A is Relation-like set
[:A,A:] is Relation-like set
O /\ [:A,A:] is Relation-like set
O is Relation-like set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
O is Relation-like set
A is set
g is set
O is Relation-like set
A is set
O |_2 A is Relation-like set
[:A,A:] is Relation-like set
O /\ [:A,A:] is Relation-like set
O is Relation-like set
A is set
g is set
AA is set
ff is set
[AA,ff] is V35() set
{AA,ff} is non empty finite set
{AA} is non empty finite set
{{AA,ff},{AA}} is non empty finite V45() set
[ff,AA] is V35() set
{ff,AA} is non empty finite set
{ff} is non empty finite set
{{ff,AA},{ff}} is non empty finite V45() set
O is Relation-like set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
O is Relation-like set
A is set
g is set
O is Relation-like set
A is set
O |_2 A is Relation-like set
[:A,A:] is Relation-like set
O /\ [:A,A:] is Relation-like set
O is Relation-like set
O ~ is Relation-like set
A is set
g is set
[g,g] is V35() set
{g,g} is non empty finite set
{g} is non empty finite set
{{g,g},{g}} is non empty finite V45() set
O is Relation-like set
O ~ is Relation-like set
A is set
g is set
AA is set
[g,AA] is V35() set
{g,AA} is non empty finite set
{g} is non empty finite set
{{g,AA},{g}} is non empty finite V45() set
ff is set
[AA,ff] is V35() set
{AA,ff} is non empty finite set
{AA} is non empty finite set
{{AA,ff},{AA}} is non empty finite V45() set
[g,ff] is V35() set
{g,ff} is non empty finite set
{{g,ff},{g}} is non empty finite V45() set
[ff,AA] is V35() set
{ff,AA} is non empty finite set
{ff} is non empty finite set
{{ff,AA},{ff}} is non empty finite V45() set
[AA,g] is V35() set
{AA,g} is non empty finite set
{{AA,g},{AA}} is non empty finite V45() set
[ff,g] is V35() set
{ff,g} is non empty finite set
{{ff,g},{ff}} is non empty finite V45() set
O is Relation-like set
O ~ is Relation-like set
A is set
g is set
AA is set
[g,AA] is V35() set
{g,AA} is non empty finite set
{g} is non empty finite set
{{g,AA},{g}} is non empty finite V45() set
[AA,g] is V35() set
{AA,g} is non empty finite set
{AA} is non empty finite set
{{AA,g},{AA}} is non empty finite V45() set
O is Relation-like set
O ~ is Relation-like set
A is set
g is set
AA is set
[g,AA] is V35() set
{g,AA} is non empty finite set
{g} is non empty finite set
{{g,AA},{g}} is non empty finite V45() set
[AA,g] is V35() set
{AA,g} is non empty finite set
{AA} is non empty finite set
{{AA,g},{AA}} is non empty finite V45() set
O is Relation-like set
O ~ is Relation-like set
A is set
O is Relation-like set
O ~ is Relation-like set
A is set
O is Relation-like set
O ~ is Relation-like set
A is set
O is set
[:O,O:] is Relation-like set
bool [:O,O:] is non empty set
A is Relation-like O -defined O -valued reflexive antisymmetric transitive total V38(O,O) Element of bool [:O,O:]
field A is set
dom A is set
rng A is set
(dom A) \/ (rng A) is set
O is set
[:O,O:] is Relation-like set
bool [:O,O:] is non empty set
A is Relation-like O -defined O -valued reflexive antisymmetric transitive total V38(O,O) Element of bool [:O,O:]
field A is set
dom A is set
rng A is set
(dom A) \/ (rng A) is set
O is Relation-like set
A is set
O |_2 A is Relation-like set
[:A,A:] is Relation-like set
O /\ [:A,A:] is Relation-like set
bool [:A,A:] is non empty set
field (O |_2 A) is set
dom (O |_2 A) is set
rng (O |_2 A) is set
(dom (O |_2 A)) \/ (rng (O |_2 A)) is set
ff is set
Y is set
[ff,Y] is V35() set
{ff,Y} is non empty finite set
{ff} is non empty finite set
{{ff,Y},{ff}} is non empty finite V45() set
[Y,ff] is V35() set
{Y,ff} is non empty finite set
{Y} is non empty finite set
{{Y,ff},{Y}} is non empty finite V45() set
ff is set
Y is set
[ff,Y] is V35() set
{ff,Y} is non empty finite set
{ff} is non empty finite set
{{ff,Y},{ff}} is non empty finite V45() set
z is set
[Y,z] is V35() set
{Y,z} is non empty finite set
{Y} is non empty finite set
{{Y,z},{Y}} is non empty finite V45() set
[ff,z] is V35() set
{ff,z} is non empty finite set
{{ff,z},{ff}} is non empty finite V45() set
ff is set
[ff,ff] is V35() set
{ff,ff} is non empty finite set
{ff} is non empty finite set
{{ff,ff},{ff}} is non empty finite V45() set
AA is Relation-like A -defined A -valued Element of bool [:A,A:]
field AA is set
dom AA is set
rng AA is set
(dom AA) \/ (rng AA) is set
dom AA is Element of bool A
bool A is non empty set
O is Relation-like set
A is set
O |_2 A is Relation-like set
[:A,A:] is Relation-like set
O /\ [:A,A:] is Relation-like set
bool [:A,A:] is non empty set
O is Relation-like set
A is set
O |_2 A is Relation-like set
[:A,A:] is Relation-like set
O /\ [:A,A:] is Relation-like set
bool [:A,A:] is non empty set
O is set
id O is Relation-like O -defined O -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total V38(O,O) V39(O) V40(O,O) () () Element of bool [:O,O:]
[:O,O:] is Relation-like set
bool [:O,O:] is non empty set
field (id O) is set
dom (id O) is set
rng (id O) is set
(dom (id O)) \/ (rng (id O)) is set
rng (id O) is Element of bool O
bool O is non empty set
O \/ (rng (id O)) is set
O \/ O is set
O is Relation-like set
O ~ is Relation-like set
A is set
O |_2 A is Relation-like set
[:A,A:] is Relation-like set
O /\ [:A,A:] is Relation-like set
(O |_2 A) ~ is Relation-like set
(O ~) |_2 A is Relation-like set
(O ~) /\ [:A,A:] is Relation-like set
g is set
AA is set
[g,AA] is V35() set
{g,AA} is non empty finite set
{g} is non empty finite set
{{g,AA},{g}} is non empty finite V45() set
[AA,g] is V35() set
{AA,g} is non empty finite set
{AA} is non empty finite set
{{AA,g},{AA}} is non empty finite V45() set
O is Relation-like set
O |_2 {} is Relation-like set
[:{},{}:] is Relation-like finite set
O /\ [:{},{}:] is Relation-like finite set
{} |` O is empty Relation-like non-empty empty-yielding reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional well_founded well-ordering epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V45() () () () set
({} |` O) | {} is empty Relation-like non-empty empty-yielding rng ({} |` O) -valued reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional well_founded well-ordering epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V45() () () () set
rng ({} |` O) is empty trivial with_non-empty_elements Relation-like non-empty empty-yielding reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional well_founded well-ordering epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V45() () () () set
O is Relation-like set
A is set
O |_2 {} is Relation-like set
O /\ [:{},{}:] is Relation-like finite set
g is set
O is Relation-like set
A is set
O |_2 {} is Relation-like set
O /\ [:{},{}:] is Relation-like finite set
g is set
O is Relation-like set
O ~ is Relation-like set
A is set
g is set
(O ~) |_2 g is Relation-like set
[:g,g:] is Relation-like set
(O ~) /\ [:g,g:] is Relation-like set
O |_2 g is Relation-like set
O /\ [:g,g:] is Relation-like set
(O |_2 g) ~ is Relation-like set
((O |_2 g) ~) ~ is Relation-like set
AA is set
ff is set
[AA,ff] is V35() set
{AA,ff} is non empty finite set
{AA} is non empty finite set
{{AA,ff},{AA}} is non empty finite V45() set
[ff,AA] is V35() set
{ff,AA} is non empty finite set
{ff} is non empty finite set
{{ff,AA},{ff}} is non empty finite V45() set
g is set
O |_2 g is Relation-like set
[:g,g:] is Relation-like set
O /\ [:g,g:] is Relation-like set
(O ~) |_2 g is Relation-like set
(O ~) /\ [:g,g:] is Relation-like set
(O |_2 g) ~ is Relation-like set
AA is set
ff is set
[ff,AA] is V35() set
{ff,AA} is non empty finite set
{ff} is non empty finite set
{{ff,AA},{ff}} is non empty finite V45() set
[AA,ff] is V35() set
{AA,ff} is non empty finite set
{AA} is non empty finite set
{{AA,ff},{AA}} is non empty finite V45() set
O is Relation-like set
O ~ is Relation-like set
A is set
(O ~) ~ is Relation-like set
O is Relation-like set
A is set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
g is set
[g,A] is V35() set
{g,A} is non empty finite set
{g} is non empty finite set
{{g,A},{g}} is non empty finite V45() set
[A,g] is V35() set
{A,g} is non empty finite set
{A} is non empty finite set
{{A,g},{A}} is non empty finite V45() set
O is Relation-like set
A is set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
g is set
[A,g] is V35() set
{A,g} is non empty finite set
{A} is non empty finite set
{{A,g},{A}} is non empty finite V45() set
[g,A] is V35() set
{g,A} is non empty finite set
{g} is non empty finite set
{{g,A},{g}} is non empty finite V45() set
O is Relation-like set
A is set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
g is set
[A,g] is V35() set
{A,g} is non empty finite set
{A} is non empty finite set
{{A,g},{A}} is non empty finite V45() set
[g,A] is V35() set
{g,A} is non empty finite set
{g} is non empty finite set
{{g,A},{g}} is non empty finite V45() set
O is Relation-like set
A is set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
g is set
[g,A] is V35() set
{g,A} is non empty finite set
{g} is non empty finite set
{{g,A},{g}} is non empty finite V45() set
[A,g] is V35() set
{A,g} is non empty finite set
{A} is non empty finite set
{{A,g},{A}} is non empty finite V45() set
O is Relation-like set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
A is set
g is set
AA is set
O |_2 AA is Relation-like set
[:AA,AA:] is Relation-like set
O /\ [:AA,AA:] is Relation-like set
ff is set
[ff,A] is V35() set
{ff,A} is non empty finite set
{ff} is non empty finite set
{{ff,A},{ff}} is non empty finite V45() set
O is Relation-like set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
A is set
g is set
AA is set
O |_2 AA is Relation-like set
[:AA,AA:] is Relation-like set
O /\ [:AA,AA:] is Relation-like set
ff is set
[A,ff] is V35() set
{A,ff} is non empty finite set
{A} is non empty finite set
{{A,ff},{A}} is non empty finite V45() set
O is Relation-like set
O ~ is Relation-like set
A is set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
field (O ~) is set
dom (O ~) is set
rng (O ~) is set
(dom (O ~)) \/ (rng (O ~)) is set
g is set
[A,g] is V35() set
{A,g} is non empty finite set
{A} is non empty finite set
{{A,g},{A}} is non empty finite V45() set
[g,A] is V35() set
{g,A} is non empty finite set
{g} is non empty finite set
{{g,A},{g}} is non empty finite V45() set
g is set
[g,A] is V35() set
{g,A} is non empty finite set
{g} is non empty finite set
{{g,A},{g}} is non empty finite V45() set
[A,g] is V35() set
{A,g} is non empty finite set
{A} is non empty finite set
{{A,g},{A}} is non empty finite V45() set
O is Relation-like set
O ~ is Relation-like set
A is set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
field (O ~) is set
dom (O ~) is set
rng (O ~) is set
(dom (O ~)) \/ (rng (O ~)) is set
g is set
[A,g] is V35() set
{A,g} is non empty finite set
{A} is non empty finite set
{{A,g},{A}} is non empty finite V45() set
[g,A] is V35() set
{g,A} is non empty finite set
{g} is non empty finite set
{{g,A},{g}} is non empty finite V45() set
g is set
[g,A] is V35() set
{g,A} is non empty finite set
{g} is non empty finite set
{{g,A},{g}} is non empty finite V45() set
[A,g] is V35() set
{A,g} is non empty finite set
{A} is non empty finite set
{{A,g},{A}} is non empty finite V45() set
O is Relation-like set
O ~ is Relation-like set
A is set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
field (O ~) is set
dom (O ~) is set
rng (O ~) is set
(dom (O ~)) \/ (rng (O ~)) is set
g is set
[g,A] is V35() set
{g,A} is non empty finite set
{g} is non empty finite set
{{g,A},{g}} is non empty finite V45() set
[A,g] is V35() set
{A,g} is non empty finite set
{A} is non empty finite set
{{A,g},{A}} is non empty finite V45() set
g is set
[A,g] is V35() set
{A,g} is non empty finite set
{A} is non empty finite set
{{A,g},{A}} is non empty finite V45() set
[g,A] is V35() set
{g,A} is non empty finite set
{g} is non empty finite set
{{g,A},{g}} is non empty finite V45() set
O is Relation-like set
O ~ is Relation-like set
A is set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
field (O ~) is set
dom (O ~) is set
rng (O ~) is set
(dom (O ~)) \/ (rng (O ~)) is set
g is set
[g,A] is V35() set
{g,A} is non empty finite set
{g} is non empty finite set
{{g,A},{g}} is non empty finite V45() set
[A,g] is V35() set
{A,g} is non empty finite set
{A} is non empty finite set
{{A,g},{A}} is non empty finite V45() set
g is set
[A,g] is V35() set
{A,g} is non empty finite set
{A} is non empty finite set
{{A,g},{A}} is non empty finite V45() set
[g,A] is V35() set
{g,A} is non empty finite set
{g} is non empty finite set
{{g,A},{g}} is non empty finite V45() set
O is Relation-like set
A is set
g is set
AA is set
O is Relation-like set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
A is set
g is non empty set
AA is non empty set
bool AA is non empty Element of bool (bool AA)
bool AA is non empty set
bool (bool AA) is non empty set
(bool AA) \ {{}} is Element of bool (bool AA)
ff is non empty set
union ff is set
the Relation-like ff -defined union ff -valued Function-like V38(ff, union ff) (ff) is Relation-like ff -defined union ff -valued Function-like V38(ff, union ff) (ff)
z is set
the Relation-like ff -defined union ff -valued Function-like V38(ff, union ff) (ff) . z is set
y is set
AA9 is set
z is set
y is set
the Relation-like ff -defined union ff -valued Function-like V38(ff, union ff) (ff) . z is set
AA9 is set
z is Relation-like Function-like set
dom z is set
y is set
AA9 is set
f9 is epsilon-transitive epsilon-connected ordinal set
x is Relation-like Function-like T-Sequence-like set
rng x is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng x or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng x or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom x is epsilon-transitive epsilon-connected ordinal set
x | f9 is Relation-like rng x -valued Function-like T-Sequence-like set
y is Relation-like Function-like T-Sequence-like set
rng y is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng y or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng y or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom y is epsilon-transitive epsilon-connected ordinal set
z is epsilon-transitive epsilon-connected ordinal set
x | z is Relation-like rng x -valued Function-like T-Sequence-like set
y | z is Relation-like rng y -valued Function-like T-Sequence-like set
dom (y | z) is epsilon-transitive epsilon-connected ordinal set
a is set
x . a is set
(x | z) . a is set
P2 is epsilon-transitive epsilon-connected ordinal set
x | P2 is Relation-like rng x -valued Function-like T-Sequence-like set
y | P2 is Relation-like rng y -valued Function-like T-Sequence-like set
y . P2 is set
rng (y | P2) is Element of bool (rng y)
bool (rng y) is non empty set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng (y | P2) or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng (y | P2) or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
x . P2 is set
rng (x | P2) is Element of bool (rng x)
bool (rng x) is non empty set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng (x | P2) or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng (x | P2) or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
(y | z) . a is set
dom (x | z) is epsilon-transitive epsilon-connected ordinal set
y | f9 is Relation-like rng y -valued Function-like T-Sequence-like set
y is set
z . y is set
the Relation-like ff -defined union ff -valued Function-like V38(ff, union ff) (ff) . y is set
z . {} is set
f9 is Relation-like Function-like T-Sequence-like set
dom f9 is epsilon-transitive epsilon-connected ordinal set
y is epsilon-transitive epsilon-connected ordinal set
x is Relation-like Function-like T-Sequence-like set
dom x is epsilon-transitive epsilon-connected ordinal set
AA9 is epsilon-transitive epsilon-connected ordinal set
y is epsilon-transitive epsilon-connected ordinal set
z is epsilon-transitive epsilon-connected ordinal set
f9 | z is Relation-like rng f9 -valued Function-like T-Sequence-like set
rng f9 is set
x | z is Relation-like rng x -valued Function-like T-Sequence-like set
rng x is set
dom (x | z) is epsilon-transitive epsilon-connected ordinal set
a is set
f9 . a is set
(f9 | z) . a is set
P2 is epsilon-transitive epsilon-connected ordinal set
f9 | P2 is Relation-like rng f9 -valued Function-like T-Sequence-like set
x | P2 is Relation-like rng x -valued Function-like T-Sequence-like set
x . P2 is set
rng (x | P2) is Element of bool (rng x)
bool (rng x) is non empty set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng (x | P2) or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng (x | P2) or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
f9 . P2 is set
rng (f9 | P2) is Element of bool (rng f9)
bool (rng f9) is non empty set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng (f9 | P2) or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng (f9 | P2) or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
(x | z) . a is set
dom (f9 | z) is epsilon-transitive epsilon-connected ordinal set
f9 | y is Relation-like rng f9 -valued Function-like T-Sequence-like set
rng f9 is set
x | y is Relation-like rng x -valued Function-like T-Sequence-like set
rng x is set
y is Element of AA
AA9 is epsilon-transitive epsilon-connected ordinal set
f9 is epsilon-transitive epsilon-connected ordinal set
x is Relation-like Function-like T-Sequence-like set
rng x is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng x or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng x or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom x is epsilon-transitive epsilon-connected ordinal set
y is Relation-like Function-like T-Sequence-like set
rng y is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng y or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng y or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom y is epsilon-transitive epsilon-connected ordinal set
x | f9 is Relation-like rng x -valued Function-like T-Sequence-like set
rng (x | f9) is Element of bool (rng x)
bool (rng x) is non empty set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng (x | f9) or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
P2 is set
y9 is Element of AA
y | f9 is Relation-like rng y -valued Function-like T-Sequence-like set
x . f9 is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng (x | f9) or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
the Relation-like ff -defined union ff -valued Function-like V38(ff, union ff) (ff) . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng x or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
P2 is Element of AA
y | AA9 is Relation-like rng y -valued Function-like T-Sequence-like set
rng (y | AA9) is Element of bool (rng y)
bool (rng y) is non empty set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng (y | AA9) or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
P2 is set
y9 is Element of AA
x | AA9 is Relation-like rng x -valued Function-like T-Sequence-like set
y . AA9 is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng (y | AA9) or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
the Relation-like ff -defined union ff -valued Function-like V38(ff, union ff) (ff) . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng y or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
P2 is Element of AA
y is epsilon-transitive epsilon-connected ordinal set
AA9 is set
f9 is epsilon-transitive epsilon-connected ordinal set
x is Element of AA
y is set
z is Relation-like Function-like T-Sequence-like set
rng z is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng z or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng z or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom z is epsilon-transitive epsilon-connected ordinal set
AA9 is set
y is epsilon-transitive epsilon-connected ordinal set
f9 is set
z is Relation-like Function-like T-Sequence-like set
rng z is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng z or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng z or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom z is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
x is set
P2 is Relation-like Function-like T-Sequence-like set
rng P2 is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng P2 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng P2 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom P2 is epsilon-transitive epsilon-connected ordinal set
AA9 is Relation-like Function-like set
dom AA9 is set
f9 is Relation-like Function-like T-Sequence-like set
rng f9 is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng f9 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
y is set
z is Element of AA
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng f9 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom f9 is epsilon-transitive epsilon-connected ordinal set
y is epsilon-transitive epsilon-connected ordinal set
f9 | y is Relation-like rng f9 -valued Function-like T-Sequence-like set
f9 . y is set
z is Relation-like Function-like T-Sequence-like set
rng z is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng z or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng z or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
a is epsilon-transitive epsilon-connected ordinal set
P2 is Relation-like Function-like T-Sequence-like set
rng P2 is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng P2 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng P2 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom P2 is epsilon-transitive epsilon-connected ordinal set
a is Relation-like Function-like T-Sequence-like set
rng a is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng a or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng a or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom a is epsilon-transitive epsilon-connected ordinal set
P2 is set
a . P2 is set
(f9 | y) . P2 is set
f9 . P2 is set
y9 is epsilon-transitive epsilon-connected ordinal set
a | y9 is Relation-like rng a -valued Function-like T-Sequence-like set
z is Relation-like Function-like T-Sequence-like set
rng z is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng z or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng z or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom z is epsilon-transitive epsilon-connected ordinal set
z9 is epsilon-transitive epsilon-connected ordinal set
z | z9 is Relation-like rng z -valued Function-like T-Sequence-like set
z . z9 is set
L1 is Relation-like Function-like T-Sequence-like set
rng L1 is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng L1 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng L1 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
a | z9 is Relation-like rng a -valued Function-like T-Sequence-like set
a . z9 is set
z is epsilon-transitive epsilon-connected ordinal set
z9 is Relation-like Function-like T-Sequence-like set
rng z9 is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng z9 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng z9 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom z9 is epsilon-transitive epsilon-connected ordinal set
L1 is Relation-like Function-like T-Sequence-like set
rng L1 is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng L1 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng L1 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom L1 is epsilon-transitive epsilon-connected ordinal set
dom (f9 | y) is epsilon-transitive epsilon-connected ordinal set
y is Relation-like Function-like T-Sequence-like set
rng y is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng y or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng y or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom y is epsilon-transitive epsilon-connected ordinal set
y is Element of AA
z is Relation-like Function-like T-Sequence-like set
rng z is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng z or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng z or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom z is epsilon-transitive epsilon-connected ordinal set
y is set
AA9 is set
f9 is set
x is epsilon-transitive epsilon-connected ordinal set
y is Element of AA
z is epsilon-transitive epsilon-connected ordinal set
a is Relation-like Function-like T-Sequence-like set
rng a is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng a or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng a or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom a is epsilon-transitive epsilon-connected ordinal set
P2 is Relation-like Function-like T-Sequence-like set
rng P2 is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng P2 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng P2 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom P2 is epsilon-transitive epsilon-connected ordinal set
a is Relation-like Function-like T-Sequence-like set
rng a is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng a or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng a or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom a is epsilon-transitive epsilon-connected ordinal set
P2 is Relation-like Function-like T-Sequence-like set
rng P2 is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng P2 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng P2 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom P2 is epsilon-transitive epsilon-connected ordinal set
y is set
AA9 is epsilon-transitive epsilon-connected ordinal set
f9 is Element of AA
x is Relation-like Function-like T-Sequence-like set
rng x is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng x or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng x or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom x is epsilon-transitive epsilon-connected ordinal set
y is epsilon-transitive epsilon-connected ordinal set
AA9 is Relation-like Function-like T-Sequence-like set
rng AA9 is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng AA9 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
f9 is set
x is Element of AA
z . AA is set
AA9 is Element of AA
f9 is Relation-like Function-like T-Sequence-like set
dom f9 is epsilon-transitive epsilon-connected ordinal set
rng f9 is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng f9 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng f9 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
x is set
y is Element of AA
z is set
[z,y] is V35() set
{z,y} is non empty finite set
{z} is non empty finite set
{{z,y},{z}} is non empty finite V45() set
x is epsilon-transitive epsilon-connected ordinal set
y is Relation-like Function-like T-Sequence-like set
f9 | x is Relation-like rng f9 -valued Function-like T-Sequence-like set
f9 . x is set
rng y is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng y or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng y or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
f9 is set
x is set
x is Relation-like Function-like T-Sequence-like set
rng x is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng x or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng x or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom x is epsilon-transitive epsilon-connected ordinal set
y is Relation-like Function-like T-Sequence-like set
rng y is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng y or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng y or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom y is epsilon-transitive epsilon-connected ordinal set
y is Relation-like Function-like T-Sequence-like set
rng y is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng y or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng y or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom y is epsilon-transitive epsilon-connected ordinal set
y is Relation-like Function-like T-Sequence-like set
rng y is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng y or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng y or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom y is epsilon-transitive epsilon-connected ordinal set
y is Relation-like Function-like T-Sequence-like set
rng y is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng y or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng y or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom y is epsilon-transitive epsilon-connected ordinal set
x is non empty set
O |_2 x is Relation-like set
[:x,x:] is non empty Relation-like set
O /\ [:x,x:] is Relation-like set
z is set
a is set
y . a is set
P2 is epsilon-transitive epsilon-connected ordinal set
y | P2 is Relation-like rng y -valued Function-like T-Sequence-like set
rng (y | P2) is Element of bool (rng y)
bool (rng y) is non empty set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng (y | P2) or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z is Relation-like Function-like T-Sequence-like set
rng z is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng z or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng z or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom z is epsilon-transitive epsilon-connected ordinal set
z9 is epsilon-transitive epsilon-connected ordinal set
z | z9 is Relation-like rng z -valued Function-like T-Sequence-like set
z . z9 is set
L1 is Relation-like Function-like T-Sequence-like set
rng L1 is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng L1 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng L1 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
y | z9 is Relation-like rng y -valued Function-like T-Sequence-like set
y . z9 is set
z is Relation-like Function-like T-Sequence-like set
rng z is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng z or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng z or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom z is epsilon-transitive epsilon-connected ordinal set
z9 is Relation-like Function-like T-Sequence-like set
rng z9 is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng z9 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng z9 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom z9 is epsilon-transitive epsilon-connected ordinal set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng (y | P2) or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z is Relation-like Function-like T-Sequence-like set
rng z is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng z or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng z or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom z is epsilon-transitive epsilon-connected ordinal set
z is set
field (O |_2 x) is set
dom (O |_2 x) is set
rng (O |_2 x) is set
(dom (O |_2 x)) \/ (rng (O |_2 x)) is set
a is set
[z,a] is V35() set
{z,a} is non empty finite set
{z} is non empty finite set
{{z,a},{z}} is non empty finite V45() set
[a,z] is V35() set
{a,z} is non empty finite set
{a} is non empty finite set
{{a,z},{a}} is non empty finite V45() set
P2 is epsilon-transitive epsilon-connected ordinal set
y9 is epsilon-transitive epsilon-connected ordinal set
z is Element of AA
L1 is Relation-like Function-like T-Sequence-like set
rng L1 is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng L1 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng L1 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom L1 is epsilon-transitive epsilon-connected ordinal set
L1 is Relation-like Function-like T-Sequence-like set
rng L1 is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng L1 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng L1 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom L1 is epsilon-transitive epsilon-connected ordinal set
z9 is Element of AA
L2 is Relation-like Function-like T-Sequence-like set
rng L2 is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng L2 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng L2 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom L2 is epsilon-transitive epsilon-connected ordinal set
L2 is Relation-like Function-like T-Sequence-like set
rng L2 is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng L2 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng L2 or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom L2 is epsilon-transitive epsilon-connected ordinal set
L2 | P2 is Relation-like rng L2 -valued Function-like T-Sequence-like set
rng (L2 | P2) is Element of bool (rng L2)
bool (rng L2) is non empty set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng (L2 | P2) or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
L1 | P2 is Relation-like rng L1 -valued Function-like T-Sequence-like set
L2 . P2 is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng (L2 | P2) or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
c₂₃ is Element of AA
L1 | y9 is Relation-like rng L1 -valued Function-like T-Sequence-like set
rng (L1 | y9) is Element of bool (rng L1)
bool (rng L1) is non empty set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng (L1 | y9) or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
c₂₃ is Element of AA
L2 | y9 is Relation-like rng L2 -valued Function-like T-Sequence-like set
L1 . y9 is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng (L1 | y9) or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
c₂₃ is Element of AA
Y is Relation-like Function-like T-Sequence-like set
rng Y is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng Y or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng Y or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom Y is epsilon-transitive epsilon-connected ordinal set
Z is Relation-like Function-like T-Sequence-like set
rng Z is set
{ b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng Z or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
z . { b₁ where b₁ is Element of AA : for b₂ being set holds
( not b₂ in rng Z or ( not b₂ = b₁ & [b₂,b₁] in O ) ) } is set
dom Z is epsilon-transitive epsilon-connected ordinal set
a is set
a is set
P2 is set
[a,P2] is V35() set
{a,P2} is non empty finite set
{a} is non empty finite set
{{a,P2},{a}} is non empty finite V45() set
[P2,a] is V35() set
{P2,a} is non empty finite set
{P2} is non empty finite set
{{P2,a},{P2}} is non empty finite V45() set
z is set
y9 is Element of AA
z9 is Element of x
[z9,a] is V35() set
{z9,a} is non empty finite set
{z9} is non empty finite set
{{z9,a},{z9}} is non empty finite V45() set
[z,P2] is V35() set
{z,P2} is non empty finite set
{z} is non empty finite set
{{z,P2},{z}} is non empty finite V45() set
O is Relation-like set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
A is set
O ~ is Relation-like set
(O ~) ~ is Relation-like set
field (O ~) is set
dom (O ~) is set
rng (O ~) is set
(dom (O ~)) \/ (rng (O ~)) is set
g is set
O is set
A is non empty set
RelIncl A is non empty Relation-like reflexive antisymmetric transitive set
AA is set
(RelIncl A) |_2 AA is Relation-like set
[:AA,AA:] is Relation-like set
(RelIncl A) /\ [:AA,AA:] is Relation-like antisymmetric set
field ((RelIncl A) |_2 AA) is set
dom ((RelIncl A) |_2 AA) is set
rng ((RelIncl A) |_2 AA) is set
(dom ((RelIncl A) |_2 AA)) \/ (rng ((RelIncl A) |_2 AA)) is set
Y is set
[Y,Y] is V35() set
{Y,Y} is non empty finite set
{Y} is non empty finite set
{{Y,Y},{Y}} is non empty finite V45() set
Y is set
z is set
[Y,z] is V35() set
{Y,z} is non empty finite set
{Y} is non empty finite set
{{Y,z},{Y}} is non empty finite V45() set
[z,Y] is V35() set
{z,Y} is non empty finite set
{z} is non empty finite set
{{z,Y},{z}} is non empty finite V45() set
Y is set
z is set
y is set
[y,z] is V35() set
{y,z} is non empty finite set
{y} is non empty finite set
{{y,z},{y}} is non empty finite V45() set
field (RelIncl A) is set
dom (RelIncl A) is non empty set
rng (RelIncl A) is non empty set
(dom (RelIncl A)) \/ (rng (RelIncl A)) is non empty set
AA is set
ff is set
Y is set
[ff,Y] is V35() set
{ff,Y} is non empty finite set
{ff} is non empty finite set
{{ff,Y},{ff}} is non empty finite V45() set
O is set
A is non empty set
RelIncl A is non empty Relation-like reflexive antisymmetric transitive set
(RelIncl A) ~ is Relation-like reflexive antisymmetric transitive set
AA is set
[AA,AA] is V35() set
{AA,AA} is non empty finite set
{AA} is non empty finite set
{{AA,AA},{AA}} is non empty finite V45() set
AA is set
((RelIncl A) ~) |_2 AA is Relation-like set
[:AA,AA:] is Relation-like set
((RelIncl A) ~) /\ [:AA,AA:] is Relation-like antisymmetric set
field (((RelIncl A) ~) |_2 AA) is set
dom (((RelIncl A) ~) |_2 AA) is set
rng (((RelIncl A) ~) |_2 AA) is set
(dom (((RelIncl A) ~) |_2 AA)) \/ (rng (((RelIncl A) ~) |_2 AA)) is set
Y is set
[Y,Y] is V35() set
{Y,Y} is non empty finite set
{Y} is non empty finite set
{{Y,Y},{Y}} is non empty finite V45() set
Y is set
z is set
[Y,z] is V35() set
{Y,z} is non empty finite set
{Y} is non empty finite set
{{Y,z},{Y}} is non empty finite V45() set
[z,Y] is V35() set
{z,Y} is non empty finite set
{z} is non empty finite set
{{z,Y},{z}} is non empty finite V45() set
Y is set
z is set
y is set
[y,z] is V35() set
{y,z} is non empty finite set
{y} is non empty finite set
{{y,z},{y}} is non empty finite V45() set
[Y,y] is V35() set
{Y,y} is non empty finite set
{Y} is non empty finite set
{{Y,y},{Y}} is non empty finite V45() set
field ((RelIncl A) ~) is set
dom ((RelIncl A) ~) is set
rng ((RelIncl A) ~) is set
(dom ((RelIncl A) ~)) \/ (rng ((RelIncl A) ~)) is set
field (RelIncl A) is set
dom (RelIncl A) is non empty set
rng (RelIncl A) is non empty set
(dom (RelIncl A)) \/ (rng (RelIncl A)) is non empty set
AA is set
ff is set
Y is set
[ff,Y] is V35() set
{ff,Y} is non empty finite set
{ff} is non empty finite set
{{ff,Y},{ff}} is non empty finite V45() set
[Y,ff] is V35() set
{Y,ff} is non empty finite set
{Y} is non empty finite set
{{Y,ff},{Y}} is non empty finite V45() set
O is set
the Element of O is Element of O
g is set
union g is set
AA is set
ff is set
O is set
the Element of O is Element of O
g is set
meet g is set
AA is set
ff is set
F₁() is non empty set
[:F₁(),F₁():] is non empty Relation-like set
bool [:F₁(),F₁():] is non empty set
O is Relation-like F₁() -defined F₁() -valued Element of bool [:F₁(),F₁():]
A is set
g is set
[A,g] is V35() set
{A,g} is non empty finite set
{A} is non empty finite set
{{A,g},{A}} is non empty finite V45() set
AA is set
[g,AA] is V35() set
{g,AA} is non empty finite set
{g} is non empty finite set
{{g,AA},{g}} is non empty finite V45() set
[A,AA] is V35() set
{A,AA} is non empty finite set
{{A,AA},{A}} is non empty finite V45() set
Y is Element of F₁()
z is Element of F₁()
ff is Element of F₁()
dom O is Element of bool F₁()
bool F₁() is non empty set
A is set
g is Element of F₁()
[A,A] is V35() set
{A,A} is non empty finite set
{A} is non empty finite set
{{A,A},{A}} is non empty finite V45() set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
rng O is Element of bool F₁()
(dom O) \/ (rng O) is Element of bool F₁()
A is set
[A,A] is V35() set
{A,A} is non empty finite set
{A} is non empty finite set
{{A,A},{A}} is non empty finite V45() set
g is Element of F₁()
A is set
O |_2 A is Relation-like set
[:A,A:] is Relation-like set
O /\ [:A,A:] is Relation-like F₁() -defined F₁() -valued set
g is Element of F₁()
AA is Element of F₁()
field (O |_2 A) is set
dom (O |_2 A) is set
rng (O |_2 A) is set
(dom (O |_2 A)) \/ (rng (O |_2 A)) is set
ff is set
[ff,ff] is V35() set
{ff,ff} is non empty finite set
{ff} is non empty finite set
{{ff,ff},{ff}} is non empty finite V45() set
(O |_2 A) |_2 A is Relation-like set
(O |_2 A) /\ [:A,A:] is Relation-like set
field ((O |_2 A) |_2 A) is set
dom ((O |_2 A) |_2 A) is set
rng ((O |_2 A) |_2 A) is set
(dom ((O |_2 A) |_2 A)) \/ (rng ((O |_2 A) |_2 A)) is set
[g,AA] is V35() set
{g,AA} is non empty finite set
{g} is non empty finite set
{{g,AA},{g}} is non empty finite V45() set
[AA,g] is V35() set
{AA,g} is non empty finite set
{AA} is non empty finite set
{{AA,g},{AA}} is non empty finite V45() set
g is Element of F₁()
AA is set
[AA,g] is V35() set
{AA,g} is non empty finite set
{AA} is non empty finite set
{{AA,g},{AA}} is non empty finite V45() set
A is set
g is set
[A,g] is V35() set
{A,g} is non empty finite set
{A} is non empty finite set
{{A,g},{A}} is non empty finite V45() set
[g,A] is V35() set
{g,A} is non empty finite set
{g} is non empty finite set
{{g,A},{g}} is non empty finite V45() set
ff is Element of F₁()
AA is Element of F₁()
A is set
g is Element of F₁()
[A,g] is V35() set
{A,g} is non empty finite set
{A} is non empty finite set
{{A,g},{A}} is non empty finite V45() set
F₁() is non empty set
[:F₁(),F₁():] is non empty Relation-like set
bool [:F₁(),F₁():] is non empty set
O is Relation-like F₁() -defined F₁() -valued Element of bool [:F₁(),F₁():]
A is set
g is set
[A,g] is V35() set
{A,g} is non empty finite set
{A} is non empty finite set
{{A,g},{A}} is non empty finite V45() set
AA is set
[g,AA] is V35() set
{g,AA} is non empty finite set
{g} is non empty finite set
{{g,AA},{g}} is non empty finite V45() set
[A,AA] is V35() set
{A,AA} is non empty finite set
{{A,AA},{A}} is non empty finite V45() set
Y is Element of F₁()
z is Element of F₁()
ff is Element of F₁()
dom O is Element of bool F₁()
bool F₁() is non empty set
A is set
g is Element of F₁()
[A,A] is V35() set
{A,A} is non empty finite set
{A} is non empty finite set
{{A,A},{A}} is non empty finite V45() set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
rng O is Element of bool F₁()
(dom O) \/ (rng O) is Element of bool F₁()
A is set
[A,A] is V35() set
{A,A} is non empty finite set
{A} is non empty finite set
{{A,A},{A}} is non empty finite V45() set
g is Element of F₁()
A is set
O |_2 A is Relation-like set
[:A,A:] is Relation-like set
O /\ [:A,A:] is Relation-like F₁() -defined F₁() -valued set
g is Element of F₁()
AA is Element of F₁()
field (O |_2 A) is set
dom (O |_2 A) is set
rng (O |_2 A) is set
(dom (O |_2 A)) \/ (rng (O |_2 A)) is set
ff is set
[ff,ff] is V35() set
{ff,ff} is non empty finite set
{ff} is non empty finite set
{{ff,ff},{ff}} is non empty finite V45() set
(O |_2 A) |_2 A is Relation-like set
(O |_2 A) /\ [:A,A:] is Relation-like set
field ((O |_2 A) |_2 A) is set
dom ((O |_2 A) |_2 A) is set
rng ((O |_2 A) |_2 A) is set
(dom ((O |_2 A) |_2 A)) \/ (rng ((O |_2 A) |_2 A)) is set
[g,AA] is V35() set
{g,AA} is non empty finite set
{g} is non empty finite set
{{g,AA},{g}} is non empty finite V45() set
[AA,g] is V35() set
{AA,g} is non empty finite set
{AA} is non empty finite set
{{AA,g},{AA}} is non empty finite V45() set
g is Element of F₁()
AA is set
[g,AA] is V35() set
{g,AA} is non empty finite set
{g} is non empty finite set
{{g,AA},{g}} is non empty finite V45() set
A is set
g is set
[A,g] is V35() set
{A,g} is non empty finite set
{A} is non empty finite set
{{A,g},{A}} is non empty finite V45() set
[g,A] is V35() set
{g,A} is non empty finite set
{g} is non empty finite set
{{g,A},{g}} is non empty finite V45() set
ff is Element of F₁()
AA is Element of F₁()
A is set
g is Element of F₁()
[g,A] is V35() set
{g,A} is non empty finite set
{g} is non empty finite set
{{g,A},{g}} is non empty finite V45() set
O is Relation-like set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
A is set
[:A,A:] is Relation-like set
bool [:A,A:] is non empty Element of bool (bool [:A,A:])
bool [:A,A:] is non empty set
bool (bool [:A,A:]) is non empty set
g is set
ff is set
union ff is set
union (bool [:A,A:]) is Relation-like A -defined A -valued Element of bool [:A,A:]
AA is Relation-like set
Y is set
the Element of ff is Element of ff
y is Relation-like set
field y is set
dom y is set
rng y is set
(dom y) \/ (rng y) is set
Y is Relation-like set
AA9 is set
f9 is set
[AA9,f9] is V35() set
{AA9,f9} is non empty finite set
{AA9} is non empty finite set
{{AA9,f9},{AA9}} is non empty finite V45() set
[f9,AA9] is V35() set
{f9,AA9} is non empty finite set
{f9} is non empty finite set
{{f9,AA9},{f9}} is non empty finite V45() set
x is set
y is Relation-like set
field y is set
dom y is set
rng y is set
(dom y) \/ (rng y) is set
z is set
a is Relation-like set
field a is set
dom a is set
rng a is set
(dom a) \/ (rng a) is set
AA9 is set
f9 is set
[AA9,f9] is V35() set
{AA9,f9} is non empty finite set
{AA9} is non empty finite set
{{AA9,f9},{AA9}} is non empty finite V45() set
x is set
[f9,x] is V35() set
{f9,x} is non empty finite set
{f9} is non empty finite set
{{f9,x},{f9}} is non empty finite V45() set
[AA9,x] is V35() set
{AA9,x} is non empty finite set
{{AA9,x},{AA9}} is non empty finite V45() set
y is set
z is Relation-like set
field z is set
dom z is set
rng z is set
(dom z) \/ (rng z) is set
a is set
P2 is Relation-like set
field P2 is set
dom P2 is set
rng P2 is set
(dom P2) \/ (rng P2) is set
AA9 is set
[AA9,AA9] is V35() set
{AA9,AA9} is non empty finite set
{AA9} is non empty finite set
{{AA9,AA9},{AA9}} is non empty finite V45() set
field Y is set
dom Y is set
rng Y is set
(dom Y) \/ (rng Y) is set
AA9 is set
f9 is set
[AA9,f9] is V35() set
{AA9,f9} is non empty finite set
{AA9} is non empty finite set
{{AA9,f9},{AA9}} is non empty finite V45() set
x is set
y is Relation-like set
field y is set
dom y is set
rng y is set
(dom y) \/ (rng y) is set
f9 is set
[f9,AA9] is V35() set
{f9,AA9} is non empty finite set
{f9} is non empty finite set
{{f9,AA9},{f9}} is non empty finite V45() set
x is set
y is Relation-like set
field y is set
dom y is set
rng y is set
(dom y) \/ (rng y) is set
AA9 is set
f9 is set
[AA9,f9] is V35() set
{AA9,f9} is non empty finite set
{AA9} is non empty finite set
{{AA9,f9},{AA9}} is non empty finite V45() set
AA is set
ff is Relation-like set
field ff is set
dom ff is set
rng ff is set
(dom ff) \/ (rng ff) is set
Y is set
z is set
[Y,z] is V35() set
{Y,z} is non empty finite set
{Y} is non empty finite set
{{Y,z},{Y}} is non empty finite V45() set
[z,Y] is V35() set
{z,Y} is non empty finite set
{z} is non empty finite set
{{z,Y},{z}} is non empty finite V45() set
y is Relation-like set
field y is set
dom y is set
rng y is set
(dom y) \/ (rng y) is set
AA9 is set
f9 is set
[AA9,f9] is V35() set
{AA9,f9} is non empty finite set
{AA9} is non empty finite set
{{AA9,f9},{AA9}} is non empty finite V45() set
f9 is set
[f9,AA9] is V35() set
{f9,AA9} is non empty finite set
{f9} is non empty finite set
{{f9,AA9},{f9}} is non empty finite V45() set
AA9 is set
f9 is set
[AA9,f9] is V35() set
{AA9,f9} is non empty finite set
{AA9} is non empty finite set
{{AA9,f9},{AA9}} is non empty finite V45() set
AA9 is set
f9 is set
x is set
[AA9,f9] is V35() set
{AA9,f9} is non empty finite set
{AA9} is non empty finite set
{{AA9,f9},{AA9}} is non empty finite V45() set
[f9,x] is V35() set
{f9,x} is non empty finite set
{f9} is non empty finite set
{{f9,x},{f9}} is non empty finite V45() set
[AA9,x] is V35() set
{AA9,x} is non empty finite set
{{AA9,x},{AA9}} is non empty finite V45() set
[f9,Y] is V35() set
{f9,Y} is non empty finite set
{{f9,Y},{f9}} is non empty finite V45() set
[z,x] is V35() set
{z,x} is non empty finite set
{{z,x},{z}} is non empty finite V45() set
[AA9,Y] is V35() set
{AA9,Y} is non empty finite set
{{AA9,Y},{AA9}} is non empty finite V45() set
[z,f9] is V35() set
{z,f9} is non empty finite set
{{z,f9},{z}} is non empty finite V45() set
AA9 is set
f9 is set
[AA9,f9] is V35() set
{AA9,f9} is non empty finite set
{AA9} is non empty finite set
{{AA9,f9},{AA9}} is non empty finite V45() set
[f9,AA9] is V35() set
{f9,AA9} is non empty finite set
{f9} is non empty finite set
{{f9,AA9},{f9}} is non empty finite V45() set
[f9,Y] is V35() set
{f9,Y} is non empty finite set
{{f9,Y},{f9}} is non empty finite V45() set
[z,AA9] is V35() set
{z,AA9} is non empty finite set
{{z,AA9},{z}} is non empty finite V45() set
[AA9,Y] is V35() set
{AA9,Y} is non empty finite set
{{AA9,Y},{AA9}} is non empty finite V45() set
[z,f9] is V35() set
{z,f9} is non empty finite set
{{z,f9},{z}} is non empty finite V45() set
AA9 is set
[AA9,AA9] is V35() set
{AA9,AA9} is non empty finite set
{AA9} is non empty finite set
{{AA9,AA9},{AA9}} is non empty finite V45() set
AA9 is set
f9 is set
[AA9,f9] is V35() set
{AA9,f9} is non empty finite set
{AA9} is non empty finite set
{{AA9,f9},{AA9}} is non empty finite V45() set
[z,z] is V35() set
{z,z} is non empty finite set
{{z,z},{z}} is non empty finite V45() set
[Y,Y] is V35() set
{Y,Y} is non empty finite set
{{Y,Y},{Y}} is non empty finite V45() set
O is Relation-like set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
[:(field O),(field O):] is Relation-like set
O is Relation-like set
A is set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
O |_2 A is Relation-like set
[:A,A:] is Relation-like set
O /\ [:A,A:] is Relation-like set
field (O |_2 A) is set
dom (O |_2 A) is set
rng (O |_2 A) is set
(dom (O |_2 A)) \/ (rng (O |_2 A)) is set
O is Relation-like set
A is set
O |_2 A is Relation-like set
[:A,A:] is Relation-like set
O /\ [:A,A:] is Relation-like set
O is Relation-like set
A is set
O |_2 A is Relation-like set
[:A,A:] is Relation-like set
O /\ [:A,A:] is Relation-like set
O is Relation-like set
A is set
O |_2 A is Relation-like set
[:A,A:] is Relation-like set
O /\ [:A,A:] is Relation-like set
O is Relation-like set
A is set
O |_2 A is Relation-like set
[:A,A:] is Relation-like set
O /\ [:A,A:] is Relation-like set
O is Relation-like set
A is set
g is set
O is Relation-like set
A is set
g is set
O is Relation-like set
O ~ is Relation-like set
O is Relation-like set
A is set
O ~ is Relation-like set
O is Relation-like set
A is set
O ~ is Relation-like set
O is Relation-like set
A is set
O ~ is Relation-like set
O is Relation-like set
A is set
O ~ is Relation-like set
O is Relation-like set
A is set
O |_2 A is Relation-like set
[:A,A:] is Relation-like set
O /\ [:A,A:] is Relation-like set
(O |_2 A) ~ is Relation-like set
O ~ is Relation-like set
(O ~) |_2 A is Relation-like set
(O ~) /\ [:A,A:] is Relation-like set
O is Relation-like set
O |_2 {} is Relation-like set
O /\ [:{},{}:] is Relation-like finite set
O is Relation-like Function-like set
rng O is set
dom O is set
A is set
g is empty Relation-like non-empty empty-yielding reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional well_founded well-ordering epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V45() () () () set
O .: g is empty Relation-like non-empty empty-yielding reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional well_founded well-ordering epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V45() () () () set
g is Relation-like Function-like set
dom g is set
rng g is set
AA is non empty set
union AA is set
the Relation-like AA -defined union AA -valued Function-like V38(AA, union AA) (AA) is Relation-like AA -defined union AA -valued Function-like V38(AA, union AA) (AA)
bool (union AA) is non empty set
the Relation-like AA -defined union AA -valued Function-like V38(AA, union AA) (AA) .: AA is Element of bool (union AA)
Y is Element of bool (union AA)
O .: Y is set
z is set
y is set
g . y is set
{y} is non empty finite set
O " {y} is set
z is set
dom the Relation-like AA -defined union AA -valued Function-like V38(AA, union AA) (AA) is Element of bool AA
bool AA is non empty set
y is set
the Relation-like AA -defined union AA -valued Function-like V38(AA, union AA) (AA) . y is set
g .: A is set
AA9 is set
g . AA9 is set
{AA9} is non empty finite set
O " {AA9} is set
g .: A is set
the Element of AA is Element of AA
the Element of the Element of AA is Element of the Element of AA
AA9 is non empty set
[:AA,AA9:] is non empty Relation-like set
bool [:AA,AA9:] is non empty set
f9 is non empty Relation-like AA -defined AA9 -valued Function-like total V38(AA,AA9) Element of bool [:AA,AA9:]
dom f9 is non empty Element of bool AA
bool AA is non empty set
x is set
y is set
O . y is set
dom the Relation-like AA -defined union AA -valued Function-like V38(AA, union AA) (AA) is Element of bool AA
z is set
the Relation-like AA -defined union AA -valued Function-like V38(AA, union AA) (AA) . z is set
a is set
g . a is set
{a} is non empty finite set
O " {a} is set
g . x is set
the Relation-like AA -defined union AA -valued Function-like V38(AA, union AA) (AA) . (g . x) is set
{x} is non empty finite set
O " {x} is set
O . ( the Relation-like AA -defined union AA -valued Function-like V38(AA, union AA) (AA) . (g . x)) is set
rng the Relation-like AA -defined union AA -valued Function-like V38(AA, union AA) (AA) is Element of bool (union AA)
O is Relation-like set
field O is set
dom O is set
rng O is set
(dom O) \/ (rng O) is set
A is finite set
[:A,A:] is Relation-like finite set
O is Relation-like set
dom O is set
rng O is set
field O is set
(dom O) \/ (rng O) is set
order_type_of {} is epsilon-transitive epsilon-connected ordinal set
RelIncl {} is empty Relation-like non-empty empty-yielding reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Function-like one-to-one constant functional well_founded well-ordering epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V45() () () () set
O is epsilon-transitive epsilon-connected ordinal set
RelIncl O is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
order_type_of (RelIncl O) is epsilon-transitive epsilon-connected ordinal set