REAL is complex-membered ext-real-membered real-membered V7() set
NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal limit_cardinal ordinal-membered Element of bool REAL
bool REAL is non empty set
NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal limit_cardinal ordinal-membered set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
0 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() V8() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() real V70() V71() decreasing non-decreasing non-increasing V79() ordinal-membered Element of NAT
RAT is complex-membered ext-real-membered real-membered rational-membered V7() set
{} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered set
the complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered set is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered set
1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT
K158(NAT,0,1) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty finite V53() Element of bool NAT
K158(NAT,0,1) ^omega is non empty functional set
bool (K158(NAT,0,1) ^omega) is non empty set
[:NAT,REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:NAT,REAL:] is non empty set
K326() is set
{{},1} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty finite V53() set
INT is complex-membered ext-real-membered real-membered rational-membered integer-membered V7() set
K412() is set
bool K412() is non empty set
K413() is Element of bool K412()
K453() is non empty V136() L10()
the carrier of K453() is non empty set
K416( the carrier of K453()) is non empty M30( the carrier of K453())
K452(K453()) is Element of bool K416( the carrier of K453())
bool K416( the carrier of K453()) is non empty set
[:K452(K453()),NAT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:K452(K453()),NAT:] is non empty set
[:NAT,K452(K453()):] is Relation-like set
bool [:NAT,K452(K453()):] is non empty set
2 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT
K317(2,K326()) is M14(K326())
[:K317(2,K326()),K326():] is Relation-like set
bool [:K317(2,K326()),K326():] is non empty set
3 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT
K317(3,K326()) is M14(K326())
[:K317(3,K326()),K326():] is Relation-like set
bool [:K317(3,K326()),K326():] is non empty set
K509() is Relation-like K317(2,K326()) -defined K326() -valued Function-like quasi_total Element of bool [:K317(2,K326()),K326():]
{{}} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial functional finite V53() 1 -element V90() set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O +^ A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(O +^ A) \ O is ordinal-membered Element of bool (O +^ A)
bool (O +^ A) is non empty set
C is set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B -^ O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O +^ c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O +^ B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is set
A is set
{O} is non empty trivial finite 1 -element set
A \/ {O} is non empty set
(A \/ {O}) \ A is Element of bool (A \/ {O})
bool (A \/ {O}) is non empty set
O is set
succ O is non empty set
{O} is non empty trivial finite 1 -element set
O \/ {O} is non empty set
(succ O) \ O is Element of bool (succ O)
bool (succ O) is non empty set
O is Relation-like Function-like set
proj1 O is set
A is Relation-like set
O .: A is set
C is set
B is set
O . B is set
c5 is set
f is set
[c5,f] is V30() set
{c5,f} is non empty finite set
{c5} is non empty trivial finite 1 -element set
{{c5,f},{c5}} is non empty finite V53() set
O . (c5,f) is set
O . [c5,f] is set
B is set
c5 is set
[B,c5] is V30() set
{B,c5} is non empty finite set
{B} is non empty trivial finite 1 -element set
{{B,c5},{B}} is non empty finite V53() set
O . (B,c5) is set
O . [B,c5] is set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
union O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O \ A is ordinal-membered Element of bool O
bool O is non empty set
inf (O \ A) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
On (O \ A) is ordinal-membered set
K181((On (O \ A))) is set
sup (O \ A) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
union (O \ A) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
the epsilon-transitive epsilon-connected ordinal ordinal-membered Element of O \ A is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of O \ A
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B is set
c5 is set
f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O \ A is ordinal-membered Element of bool O
bool O is non empty set
the epsilon-transitive epsilon-connected ordinal ordinal-membered Element of O \ A is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of O \ A
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A +^ B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 is T-Sequence-like Relation-like Function-like set
proj1 c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f is set
c5 . f is set
k is set
c5 . k is set
f is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
c5 . f is set
A +^ f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c9 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
c5 . c9 is set
A +^ c9 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
proj2 c5 is set
A +^ NAT is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f is set
k is set
c5 . k is set
f is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
A +^ f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is Relation-like Function-like set
proj1 O is set
A is Relation-like Function-like set
proj1 A is set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C \ B is ordinal-membered Element of bool C
bool C is non empty set
O is Relation-like Function-like set
proj1 O is set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A \ C is ordinal-membered Element of bool A
bool A is non empty set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is Relation-like Function-like set
A is T-Sequence-like Relation-like Function-like set
proj1 A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
proj1 O is set
(proj1 A) \ {} is ordinal-membered Element of bool (proj1 A)
bool (proj1 A) is non empty set
O is Relation-like Function-like set
A is Relation-like Function-like FinSequence-like set
len A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
succ (len A) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
{(len A)} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set
(len A) \/ {(len A)} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty finite set
proj1 O is set
C is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
B is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT
C \ B is finite ordinal-membered Element of bool C
bool C is non empty finite V53() set
f is set
dom A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
c5 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
succ {} is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
{} \/ {{}} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty finite V53() set
k is set
f is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
c5 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is Relation-like Function-like set
proj1 A is set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C \ B is ordinal-membered Element of bool C
bool C is non empty set
the epsilon-transitive epsilon-connected ordinal ordinal-membered Element of C \ B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of C \ B
O \ O is ordinal-membered Element of bool O
bool O is non empty set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C \ O is ordinal-membered Element of bool C
bool C is non empty set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is Relation-like Function-like set
proj1 A is set
sup (proj1 A) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C \ B is ordinal-membered Element of bool C
bool C is non empty set
the epsilon-transitive epsilon-connected ordinal ordinal-membered Element of C \ B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of C \ B
f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O \ f is ordinal-membered Element of bool O
bool O is non empty set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O \ C is ordinal-membered Element of bool O
bool O is non empty set
sup (proj1 A) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is Relation-like Function-like set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
proj1 O is set
A is T-Sequence-like Relation-like Function-like () set
proj1 A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is Relation-like Function-like set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
proj1 O is set
A is Relation-like Function-like FinSequence-like () set
dom A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
len A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
O is Relation-like Function-like set
proj1 O is set
inf (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
On (proj1 O) is ordinal-membered set
K181((On (proj1 O))) is set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is Relation-like Function-like set
proj1 O is set
sup (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is Relation-like Function-like set
proj1 C is set
sup (proj1 C) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is Relation-like Function-like set
proj1 O is set
inf (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
On (proj1 O) is ordinal-membered set
K181((On (proj1 O))) is set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
sup (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
sup (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is Relation-like Function-like set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(O) -^ (O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
({}) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
({}) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
({}) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
({}) -^ ({}) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
dom {} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) Element of bool NAT
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is Relation-like Function-like set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
proj1 O is set
sup (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
On (proj1 O) is ordinal-membered set
A is set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is Relation-like Function-like set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
proj1 O is set
sup (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
proj1 A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) set
C is set
A is set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
[:C,A:] is Relation-like set
bool [:C,A:] is non empty set
{} [:C,A:] is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) Element of bool [:C,A:]
B is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) Element of bool [:C,A:]
O is Relation-like Function-like () set
proj1 O is set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A \ C is ordinal-membered Element of bool A
bool A is non empty set
O is Relation-like Function-like () set
proj1 O is ordinal-membered set
sup (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
proj1 O is ordinal-membered set
sup (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is Relation-like Function-like () set
proj1 O is ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A \ C is ordinal-membered Element of bool A
bool A is non empty set
the epsilon-transitive epsilon-connected ordinal ordinal-membered Element of A \ C is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of A \ C
O is Relation-like Function-like set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
proj1 O is set
inf (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
On (proj1 O) is ordinal-membered set
K181((On (proj1 O))) is set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
the epsilon-transitive epsilon-connected ordinal ordinal-membered Element of On (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of On (proj1 O)
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is Relation-like Function-like set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
proj1 O is set
inf (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
On (proj1 O) is ordinal-membered set
K181((On (proj1 O))) is set
O is Relation-like Function-like () set
proj1 O is ordinal-membered set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(O) \ (O) is ordinal-membered Element of bool (O)
bool (O) is non empty set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A \ C is ordinal-membered Element of bool A
bool A is non empty set
sup (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
inf (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
On (proj1 O) is ordinal-membered set
K181((On (proj1 O))) is set
B is set
B is set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O \ A is ordinal-membered Element of bool O
bool O is non empty set
C is Relation-like Function-like () set
proj1 C is ordinal-membered set
(C) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(C) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
the epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 C is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 C
sup (proj1 C) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
sup O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is T-Sequence-like Relation-like Function-like () ( {} ) set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
proj1 O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(O) -^ (O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(proj1 O) \ {} is ordinal-membered Element of bool (proj1 O)
bool (proj1 O) is non empty set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
the complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding O -defined C -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) set is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding O -defined C -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is set
[O,A] is V30() set
{O,A} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,A},{O}} is non empty finite V53() set
{[O,A]} is non empty trivial Relation-like Function-like constant finite 1 -element set
succ O is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
O \/ {O} is non empty set
proj1 {[O,A]} is non empty trivial finite 1 -element set
(succ O) \ O is ordinal-membered Element of bool (succ O)
bool (succ O) is non empty set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
[O,A] is V30() set
{O,A} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,A},{O}} is non empty finite V53() set
{[O,A]} is non empty trivial Relation-like Function-like constant finite 1 -element () set
C is Relation-like Function-like () set
proj2 C is set
{A} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is real set
[O,A] is V30() set
{O,A} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,A},{O}} is non empty finite V53() set
{[O,A]} is non empty trivial Relation-like Function-like constant finite 1 -element () set
C is Relation-like Function-like () set
proj2 C is set
{A} is complex-membered ext-real-membered real-membered non empty trivial finite 1 -element set
A is non empty set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is Element of A
[O,C] is V30() set
{O,C} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,C},{O}} is non empty finite V53() set
{[O,C]} is non empty trivial Relation-like Function-like constant finite 1 -element () set
B is Relation-like Function-like () set
proj2 B is set
{C} is non empty trivial finite 1 -element set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is set
[O,A] is V30() set
{O,A} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,A},{O}} is non empty finite V53() set
{[O,A]} is non empty trivial Relation-like Function-like constant finite 1 -element () set
succ O is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
O \/ {O} is non empty set
C is Relation-like Function-like () set
proj1 C is ordinal-membered set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
sup (proj1 C) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
the epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
[O, the epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set ] is V30() set
{O, the epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set } is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O, the epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set },{O}} is non empty finite V53() set
{[O, the epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set ]} is non empty trivial Relation-like RAT -valued Function-like constant complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing finite 1 -element () (O) ( succ O) set
succ O is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
O \/ {O} is non empty set
C is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued () set
A is non empty set
the Element of A is Element of A
[O, the Element of A] is V30() set
{O, the Element of A} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O, the Element of A},{O}} is non empty finite V53() set
{[O, the Element of A]} is non empty trivial Relation-like A -valued Function-like constant finite 1 -element () (O) ( succ O) set
succ O is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
O \/ {O} is non empty set
B is Relation-like A -valued Function-like () set
O is Relation-like Function-like () set
proj1 O is ordinal-membered set
union (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . (union (proj1 O)) is set
O is T-Sequence-like Relation-like Function-like () ( {} ) set
last O is set
proj1 O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
union (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . (union (proj1 O)) is set
(O) is set
O is Relation-like Function-like finite () set
proj1 O is finite ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . A is set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . C is set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B \ c5 is ordinal-membered Element of bool B
bool B is non empty set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
c5 +^ f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
k is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 +^ k is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 +^ f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
succ c9 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
{c9} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set
c9 \/ {c9} is non empty finite set
succ A is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{A} is non empty trivial finite 1 -element set
A \/ {A} is non empty set
c5 +^ (succ c9) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
q is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
q + y is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
(succ A) +^ {} is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . H1( {} ) is set
b is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
(succ A) +^ b is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . H1(b) is set
b + 1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT
(succ A) +^ (b + 1) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . H1(b + 1) is set
succ b is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
{b} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set
b \/ {b} is non empty finite set
succ H1(b) is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{((succ A) +^ b)} is non empty trivial finite 1 -element set
((succ A) +^ b) \/ {((succ A) +^ b)} is non empty set
y is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
q +^ y is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 +^ (q +^ y) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(succ A) +^ y is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is Relation-like Function-like () set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(O) -^ (O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
proj1 O is ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . A is set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . C is set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B \ c5 is ordinal-membered Element of bool B
bool B is non empty set
c5 +^ NAT is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 +^ f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
k is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 +^ k is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
succ f is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
{f} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set
f \/ {f} is non empty finite set
succ A is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{A} is non empty trivial finite 1 -element set
A \/ {A} is non empty set
c5 +^ (succ f) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
p is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
p + q is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
(succ A) +^ {} is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . H1( {} ) is set
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
(succ A) +^ y is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . H1(y) is set
y + 1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT
(succ A) +^ (y + 1) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . H1(y + 1) is set
succ y is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
{y} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set
y \/ {y} is non empty finite set
succ H1(y) is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{((succ A) +^ y)} is non empty trivial finite 1 -element set
((succ A) +^ y) \/ {((succ A) +^ y)} is non empty set
y is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
p +^ y is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 +^ (p +^ y) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(succ A) +^ y is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is T-Sequence-like Relation-like Function-like () ( {} ) set
O . {} is set
proj1 O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is T-Sequence-like Relation-like Function-like () ( {} ) set
proj1 A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . C is set
succ C is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{C} is non empty trivial finite 1 -element set
C \/ {C} is non empty set
O . (succ C) is set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . C is set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A . C is set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A . B is set
O . C is set
len (O . C) is epsilon-transitive epsilon-connected ordinal cardinal ordinal-membered set
O . B is set
len (O . B) is epsilon-transitive epsilon-connected ordinal cardinal ordinal-membered set
O is T-Sequence-like Relation-like Function-like () ( {} ) set
O . {} is set
proj1 O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(O) is set
union (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . (union (proj1 O)) is set
A is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
union A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
B + 1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT
succ B is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
{B} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set
B \/ {B} is non empty finite set
O . (union A) is set
F1() is T-Sequence-like Relation-like Function-like () ( {} ) set
F1() . {} is set
F2((F1() . {})) is set
proj1 F1() is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is T-Sequence-like Relation-like Function-like () ( {} ) set
proj1 O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O | NAT is T-Sequence-like Relation-like proj2 O -valued Function-like () ( {} ) set
proj2 O is set
proj1 (O | NAT) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
((O | NAT)) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
((O | NAT)) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
((O | NAT)) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
((O | NAT)) -^ ((O | NAT)) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(O | NAT) . {} is set
O . {} is set
C is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
(O | NAT) . C is set
C + 1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT
(O | NAT) . (C + 1) is set
succ C is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
{C} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set
C \/ {C} is non empty finite set
O . C is set
(O | NAT) . (succ C) is set
O . (succ C) is set
F1() . C is set
F2((F1() . C)) is set
F1() . (succ C) is set
F2((F1() . (succ C))) is set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
succ C is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{C} is non empty trivial finite 1 -element set
C \/ {C} is non empty set
(O | NAT) . (succ C) is set
(O | NAT) . C is set
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
(O | NAT) . B is set
O . C is set
O . (succ C) is set
F1() . C is set
F2((F1() . C)) is set
F1() . (succ C) is set
F2((F1() . (succ C))) is set
O is set
A is Relation-like O -defined Function-like set
C is set
B is set
Swap (A,C,B) is Relation-like Function-like set
proj1 (Swap (A,C,B)) is set
dom A is Element of bool O
bool O is non empty set
O is set
A is Relation-like O -valued Function-like set
C is set
B is set
Swap (A,C,B) is Relation-like Function-like set
proj2 (Swap (A,C,B)) is set
proj2 A is set
O is set
A is set
C is Relation-like Function-like set
proj1 C is set
Swap (C,O,A) is Relation-like Function-like set
(Swap (C,O,A)) . O is set
C . A is set
C +* (O,(C . A)) is Relation-like Function-like set
C . O is set
(C +* (O,(C . A))) +* (A,(C . O)) is Relation-like Function-like set
proj1 (C +* (O,(C . A))) is set
(C +* (O,(C . A))) . O is set
O is set
A is set
C is set
B is Relation-like O -valued Function-like () set
proj1 B is ordinal-membered set
Swap (B,A,C) is Relation-like O -valued Function-like set
(Swap (B,A,C)) /. A is Element of O
B /. C is Element of O
proj1 (Swap (B,A,C)) is set
(Swap (B,A,C)) . A is set
B . C is set
O is set
A is set
C is Relation-like Function-like set
proj1 C is set
Swap (C,O,A) is Relation-like Function-like set
(Swap (C,O,A)) . A is set
C . O is set
C . A is set
C +* (O,(C . A)) is Relation-like Function-like set
(C +* (O,(C . A))) +* (A,(C . O)) is Relation-like Function-like set
proj1 (C +* (O,(C . A))) is set
O is set
A is set
C is set
B is Relation-like O -valued Function-like () set
proj1 B is ordinal-membered set
Swap (B,A,C) is Relation-like O -valued Function-like set
(Swap (B,A,C)) /. C is Element of O
B /. A is Element of O
proj1 (Swap (B,A,C)) is set
(Swap (B,A,C)) . C is set
B . A is set
O is set
A is set
C is set
B is Relation-like Function-like set
Swap (B,A,C) is Relation-like Function-like set
(Swap (B,A,C)) . O is set
B . O is set
proj1 B is set
B . C is set
B +* (A,(B . C)) is Relation-like Function-like set
B . A is set
(B +* (A,(B . C))) +* (C,(B . A)) is Relation-like Function-like set
(B +* (A,(B . C))) . O is set
proj1 B is set
proj1 B is set
O is set
A is set
C is set
B is set
c5 is Relation-like O -valued Function-like () set
proj1 c5 is ordinal-membered set
Swap (c5,C,B) is Relation-like O -valued Function-like set
(Swap (c5,C,B)) /. A is Element of O
c5 /. A is Element of O
proj1 (Swap (c5,C,B)) is set
(Swap (c5,C,B)) . A is set
c5 . A is set
O is set
A is set
C is Relation-like Function-like set
proj1 C is set
Swap (C,O,A) is Relation-like Function-like set
Swap (C,A,O) is Relation-like Function-like set
proj1 (Swap (C,O,A)) is set
proj1 (Swap (C,A,O)) is set
B is set
(Swap (C,O,A)) . B is set
(Swap (C,A,O)) . B is set
(Swap (C,O,A)) . B is set
C . A is set
(Swap (C,A,O)) . B is set
(Swap (C,O,A)) . B is set
C . O is set
(Swap (C,A,O)) . B is set
(Swap (C,O,A)) . B is set
C . B is set
(Swap (C,A,O)) . B is set
O is non empty set
id O is non empty Relation-like O -defined O -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:O,O:]
[:O,O:] is non empty Relation-like set
bool [:O,O:] is non empty set
O is non empty set
A is non empty Relation-like O -valued Function-like onto set
proj1 A is non empty set
C is Element of proj1 A
B is Element of proj1 A
Swap (A,C,B) is Relation-like O -valued Function-like set
proj2 (Swap (A,C,B)) is set
proj2 A is non empty set
O is Relation-like Function-like () set
A is set
C is set
Swap (O,A,C) is Relation-like Function-like set
proj1 O is ordinal-membered set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B \ c5 is ordinal-membered Element of bool B
bool B is non empty set
proj1 (Swap (O,A,C)) is set
O is set
A is set
C is Relation-like Function-like () set
proj1 C is ordinal-membered set
Swap (C,O,A) is Relation-like Function-like () set
Swap ((Swap (C,O,A)),O,A) is Relation-like Function-like () set
proj1 (Swap ((Swap (C,O,A)),O,A)) is ordinal-membered set
proj1 (Swap (C,O,A)) is ordinal-membered set
f is set
(Swap ((Swap (C,O,A)),O,A)) . f is set
(Swap (C,O,A)) . f is set
C . f is set
(Swap ((Swap (C,O,A)),O,A)) . f is set
(Swap (C,O,A)) . A is set
C . f is set
(Swap ((Swap (C,O,A)),O,A)) . f is set
(Swap (C,O,A)) . O is set
C . f is set
O is Relation-like Function-like complex-valued ext-real-valued real-valued () set
A is set
C is set
Swap (O,A,C) is Relation-like Function-like () set
B is Relation-like Function-like () set
c5 is set
proj1 B is ordinal-membered set
B . c5 is set
proj1 O is ordinal-membered set
O . C is V8() ext-real real set
O . A is V8() ext-real real set
O . c5 is V8() ext-real real set
O is Relation-like Function-like () set
proj1 O is ordinal-membered set
[:(proj1 O),(proj1 O):] is Relation-like set
bool [:(proj1 O),(proj1 O):] is non empty set
id (proj1 O) is Relation-like proj1 O -defined proj1 O -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 O),(proj1 O):]
(id (proj1 O)) * O is Relation-like proj1 O -defined Function-like set
O is Relation-like Function-like () set
proj1 O is ordinal-membered set
proj2 O is set
A is Relation-like Function-like () (O)
proj1 A is ordinal-membered set
proj2 A is set
[:(proj1 O),(proj1 O):] is Relation-like set
bool [:(proj1 O),(proj1 O):] is non empty set
C is Relation-like proj1 O -defined proj1 O -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 O),(proj1 O):]
C * O is Relation-like proj1 O -defined Function-like set
proj2 C is set
dom C is Element of bool (proj1 O)
bool (proj1 O) is non empty set
O is Relation-like Function-like () set
proj1 O is ordinal-membered set
id (proj1 O) is Relation-like proj1 O -defined proj1 O -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 O),(proj1 O):]
[:(proj1 O),(proj1 O):] is Relation-like set
bool [:(proj1 O),(proj1 O):] is non empty set
(id (proj1 O)) * O is Relation-like proj1 O -defined Function-like set
O is Relation-like Function-like () set
A is Relation-like Function-like () set
proj1 O is ordinal-membered set
proj1 A is ordinal-membered set
[:(proj1 A),(proj1 A):] is Relation-like set
bool [:(proj1 A),(proj1 A):] is non empty set
C is Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]
C * A is Relation-like proj1 A -defined Function-like set
[:(proj1 O),(proj1 O):] is Relation-like set
bool [:(proj1 O),(proj1 O):] is non empty set
C " is Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]
B is Relation-like proj1 O -defined proj1 O -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 O),(proj1 O):]
B * O is Relation-like proj1 O -defined Function-like set
id (proj1 A) is Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]
(id (proj1 A)) * A is Relation-like proj1 A -defined Function-like set
C * B is Relation-like proj1 O -defined proj1 A -valued Function-like one-to-one Element of bool [:(proj1 O),(proj1 A):]
[:(proj1 O),(proj1 A):] is Relation-like set
bool [:(proj1 O),(proj1 A):] is non empty set
(C * B) * A is Relation-like proj1 O -defined Function-like set
O is Relation-like Function-like () set
A is Relation-like Function-like () set
C is Relation-like Function-like () set
proj1 C is ordinal-membered set
proj1 A is ordinal-membered set
[:(proj1 A),(proj1 A):] is Relation-like set
bool [:(proj1 A),(proj1 A):] is non empty set
B is Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]
B * A is Relation-like proj1 A -defined Function-like set
[:(proj1 C),(proj1 C):] is Relation-like set
bool [:(proj1 C),(proj1 C):] is non empty set
c5 is Relation-like proj1 C -defined proj1 C -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 C),(proj1 C):]
c5 * C is Relation-like proj1 C -defined Function-like set
c5 * B is Relation-like proj1 A -defined proj1 C -valued Function-like one-to-one Element of bool [:(proj1 A),(proj1 C):]
[:(proj1 A),(proj1 C):] is Relation-like set
bool [:(proj1 A),(proj1 C):] is non empty set
f is Relation-like proj1 C -defined proj1 C -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 C),(proj1 C):]
f * C is Relation-like proj1 C -defined Function-like set
O is set
id O is Relation-like O -defined O -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:O,O:]
[:O,O:] is Relation-like set
bool [:O,O:] is non empty set
A is set
C is set
Swap ((id O),A,C) is Relation-like O -defined O -valued Function-like set
dom (id O) is Element of bool O
bool O is non empty set
f is set
proj1 (Swap ((id O),A,C)) is set
(Swap ((id O),A,C)) . f is set
k is set
(Swap ((id O),A,C)) . k is set
dom (Swap ((id O),A,C)) is Element of bool O
(id O) . f is set
(id O) . k is set
(id O) . A is set
(id O) . C is set
O is non empty set
id O is non empty Relation-like O -defined O -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:O,O:]
[:O,O:] is non empty Relation-like set
bool [:O,O:] is non empty set
A is Element of O
C is Element of O
Swap ((id O),A,C) is Relation-like O -defined O -valued Function-like set
O is non empty set
id O is non empty Relation-like O -defined O -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:O,O:]
[:O,O:] is non empty Relation-like set
bool [:O,O:] is non empty set
A is Element of O
C is Element of O
Swap ((id O),A,C) is Relation-like O -defined O -valued Function-like one-to-one set
dom (id O) is non empty Element of bool O
bool O is non empty set
B is Element of dom (id O)
c5 is Element of dom (id O)
Swap ((id O),B,c5) is Relation-like O -defined O -valued Function-like one-to-one onto set
dom (Swap ((id O),A,C)) is Element of bool O
O is non empty set
A is non empty set
[:O,A:] is non empty Relation-like set
bool [:O,A:] is non empty set
C is non empty Relation-like O -defined A -valued Function-like total quasi_total Element of bool [:O,A:]
B is Element of O
c5 is Element of O
Swap (C,B,c5) is Relation-like O -defined A -valued Function-like set
dom C is non empty Element of bool O
bool O is non empty set
dom (Swap (C,B,c5)) is Element of bool O
proj2 (Swap (C,B,c5)) is set
proj2 C is non empty set
O is set
A is set
id A is Relation-like A -defined A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:A,A:]
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
C is set
Swap ((id A),O,C) is Relation-like A -defined A -valued Function-like set
B is Relation-like Function-like set
c5 is Relation-like Function-like () set
proj1 c5 is ordinal-membered set
Swap (c5,O,C) is Relation-like Function-like () set
B * c5 is Relation-like Function-like set
dom (id A) is Element of bool A
bool A is non empty set
proj2 (id A) is set
proj1 B is set
proj2 B is set
proj1 (Swap (c5,O,C)) is ordinal-membered set
proj1 (B * c5) is set
f is set
(id A) . O is set
(id A) . C is set
(id A) . f is set
(Swap (c5,O,C)) . f is set
c5 . C is set
B . f is set
c5 . O is set
c5 . f is set
(B * c5) . f is set
O is set
A is set
C is Relation-like Function-like () set
proj1 C is ordinal-membered set
Swap (C,O,A) is Relation-like Function-like () set
c5 is non empty set
[:(proj1 C),(proj1 C):] is Relation-like set
bool [:(proj1 C),(proj1 C):] is non empty set
id c5 is non empty Relation-like c5 -defined c5 -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:c5,c5:]
[:c5,c5:] is non empty Relation-like set
bool [:c5,c5:] is non empty set
f is Element of c5
k is Element of c5
(c5,c5,(id c5),f,k) is non empty Relation-like c5 -defined c5 -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:c5,c5:]
f is Relation-like proj1 C -defined proj1 C -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 C),(proj1 C):]
f * C is Relation-like proj1 C -defined Function-like set
O is set
A is set
C is Relation-like Function-like () set
proj1 C is ordinal-membered set
Swap (C,O,A) is Relation-like Function-like () set
B is Relation-like Function-like () set
Swap (B,O,A) is Relation-like Function-like () set
proj1 B is ordinal-membered set
O is RelStr
the carrier of O is set
A is Relation-like the carrier of O -valued Function-like () set
proj1 A is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & not A /. b1 <= A /. b2 ) } is set
O is RelStr
the carrier of O is set
A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined the carrier of O -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
proj1 A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) set
A /. C is Element of the carrier of O
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A /. B is Element of the carrier of O
A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined the carrier of O -valued the carrier of O -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) (O) set
(O,A) is set
proj1 A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & not A /. b1 <= A /. b2 ) } is set
the Element of (O,A) is Element of (O,A)
dom A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) Element of bool NAT
B is V8() epsilon-transitive epsilon-connected ordinal natural Relation-like Function-like ext-real non negative finite cardinal real V70() ordinal-membered Element of dom A
c5 is V8() epsilon-transitive epsilon-connected ordinal natural Relation-like Function-like ext-real non negative finite cardinal real V70() ordinal-membered Element of dom A
[B,c5] is V30() set
{B,c5} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty functional finite V53() set
{B} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial functional finite V53() 1 -element V90() set
{{B,c5},{B}} is non empty finite V53() set
A /. B is Element of the carrier of O
A /. c5 is Element of the carrier of O
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
C is Element of the carrier of O
A is Element of the carrier of O
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like () set
(O,A) is set
proj1 A is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & not A /. b1 <= A /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & A /. b2 < A /. b1 ) } is set
B is set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
f is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
[c5,f] is V30() set
{c5,f} is non empty finite set
{c5} is non empty trivial finite 1 -element set
{{c5,f},{c5}} is non empty finite V53() set
A /. c5 is Element of the carrier of O
A /. f is Element of the carrier of O
B is set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
f is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
[c5,f] is V30() set
{c5,f} is non empty finite set
{c5} is non empty trivial finite 1 -element set
{{c5,f},{c5}} is non empty finite V53() set
A /. f is Element of the carrier of O
A /. c5 is Element of the carrier of O
B is set
c5 is set
O is set
A is set
[O,A] is V30() set
{O,A} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,A},{O}} is non empty finite V53() set
C is non empty reflexive transitive antisymmetric connected RelStr
the carrier of C is non empty set
B is Relation-like the carrier of C -valued Function-like () set
(C,B) is set
proj1 B is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 B : ( b1 in b2 & not B /. b1 <= B /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 B : ( b1 in b2 & B /. b2 < B /. b1 ) } is set
B /. A is Element of the carrier of C
B /. O is Element of the carrier of C
c5 is non empty Relation-like Function-like set
proj1 c5 is non empty set
f is Element of proj1 c5
k is Element of proj1 c5
[f,k] is V30() set
{f,k} is non empty finite set
{f} is non empty trivial finite 1 -element set
{{f,k},{f}} is non empty finite V53() set
B /. f is Element of the carrier of C
B /. k is Element of the carrier of C
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like () set
(O,A) is set
proj1 A is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & not A /. b1 <= A /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & A /. b2 < A /. b1 ) } is set
[:(proj1 A),(proj1 A):] is Relation-like set
C is set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
[B,c5] is V30() set
{B,c5} is non empty finite set
{B} is non empty trivial finite 1 -element set
{{B,c5},{B}} is non empty finite V53() set
A /. c5 is Element of the carrier of O
A /. B is Element of the carrier of O
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like finite () set
(O,A) is set
proj1 A is finite ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & not A /. b1 <= A /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & A /. b2 < A /. b1 ) } is set
[:(proj1 A),(proj1 A):] is Relation-like finite set
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like () set
(O,A) is set
proj1 A is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & not A /. b1 <= A /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & A /. b2 < A /. b1 ) } is set
the Element of (O,A) is Element of (O,A)
B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
[B,c5] is V30() set
{B,c5} is non empty finite set
{B} is non empty trivial finite 1 -element set
{{B,c5},{B}} is non empty finite V53() set
A /. c5 is Element of the carrier of O
A /. B is Element of the carrier of O
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A /. C is Element of the carrier of O
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A /. B is Element of the carrier of O
[C,B] is V30() set
{C,B} is non empty finite set
{C} is non empty trivial finite 1 -element set
{{C,B},{C}} is non empty finite V53() set
O is set
A is set
[O,A] is V30() set
{O,A} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,A},{O}} is non empty finite V53() set
[A,O] is V30() set
{A,O} is non empty finite set
{A} is non empty trivial finite 1 -element set
{{A,O},{A}} is non empty finite V53() set
C is non empty reflexive transitive antisymmetric connected RelStr
the carrier of C is non empty set
B is Relation-like the carrier of C -valued Function-like () set
(C,B) is set
proj1 B is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 B : ( b1 in b2 & not B /. b1 <= B /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 B : ( b1 in b2 & B /. b2 < B /. b1 ) } is set
O is set
A is set
[O,A] is V30() set
{O,A} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,A},{O}} is non empty finite V53() set
C is set
[A,C] is V30() set
{A,C} is non empty finite set
{A} is non empty trivial finite 1 -element set
{{A,C},{A}} is non empty finite V53() set
[O,C] is V30() set
{O,C} is non empty finite set
{{O,C},{O}} is non empty finite V53() set
B is non empty reflexive transitive antisymmetric connected RelStr
the carrier of B is non empty set
c5 is Relation-like the carrier of B -valued Function-like () set
(B,c5) is set
proj1 c5 is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5 : ( b1 in b2 & not c5 /. b1 <= c5 /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5 : ( b1 in b2 & c5 /. b2 < c5 /. b1 ) } is set
f is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
k is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
c5 /. k is Element of the carrier of B
c5 /. f is Element of the carrier of B
f is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
c5 /. f is Element of the carrier of B
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like () set
(O,A) is set
proj1 A is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & not A /. b1 <= A /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & A /. b2 < A /. b1 ) } is set
[:(proj1 A),(proj1 A):] is Relation-like set
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like () set
(O,A) is Relation-like set
proj1 A is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & not A /. b1 <= A /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & A /. b2 < A /. b1 ) } is set
C is Relation-like set
B is set
field C is set
proj1 C is set
proj2 C is set
(proj1 C) \/ (proj2 C) is set
c5 is set
[B,c5] is V30() set
{B,c5} is non empty finite set
{B} is non empty trivial finite 1 -element set
{{B,c5},{B}} is non empty finite V53() set
[c5,B] is V30() set
{c5,B} is non empty finite set
{c5} is non empty trivial finite 1 -element set
{{c5,B},{c5}} is non empty finite V53() set
B is set
field C is set
proj1 C is set
proj2 C is set
(proj1 C) \/ (proj2 C) is set
c5 is set
[B,c5] is V30() set
{B,c5} is non empty finite set
{B} is non empty trivial finite 1 -element set
{{B,c5},{B}} is non empty finite V53() set
f is set
[c5,f] is V30() set
{c5,f} is non empty finite set
{c5} is non empty trivial finite 1 -element set
{{c5,f},{c5}} is non empty finite V53() set
[B,f] is V30() set
{B,f} is non empty finite set
{{B,f},{B}} is non empty finite V53() set
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
B is Element of the carrier of O
c5 is Element of the carrier of O
O is set
A is set
[O,A] is V30() set
{O,A} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,A},{O}} is non empty finite V53() set
C is non empty reflexive transitive antisymmetric connected RelStr
the carrier of C is non empty set
B is Relation-like the carrier of C -valued Function-like () set
(C,B) is Relation-like asymmetric transitive set
proj1 B is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 B : ( b1 in b2 & not B /. b1 <= B /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 B : ( b1 in b2 & B /. b2 < B /. b1 ) } is set
Swap (B,O,A) is Relation-like the carrier of C -valued Function-like () set
(C,(Swap (B,O,A))) is Relation-like asymmetric transitive set
proj1 (Swap (B,O,A)) is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (Swap (B,O,A)) : ( b1 in b2 & not (Swap (B,O,A)) /. b1 <= (Swap (B,O,A)) /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (Swap (B,O,A)) : ( b1 in b2 & (Swap (B,O,A)) /. b2 < (Swap (B,O,A)) /. b1 ) } is set
B /. A is Element of the carrier of C
B /. O is Element of the carrier of C
(Swap (B,O,A)) /. O is Element of the carrier of C
(Swap (B,O,A)) /. A is Element of the carrier of C
O is set
A is set
C is set
B is set
[C,B] is V30() set
{C,B} is non empty finite set
{C} is non empty trivial finite 1 -element set
{{C,B},{C}} is non empty finite V53() set
c5 is non empty reflexive transitive antisymmetric connected RelStr
the carrier of c5 is non empty set
f is Relation-like the carrier of c5 -valued Function-like () set
proj1 f is ordinal-membered set
(c5,f) is Relation-like asymmetric transitive set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 f : ( b1 in b2 & not f /. b1 <= f /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 f : ( b1 in b2 & f /. b2 < f /. b1 ) } is set
Swap (f,O,A) is Relation-like the carrier of c5 -valued Function-like () set
(c5,(Swap (f,O,A))) is Relation-like asymmetric transitive set
proj1 (Swap (f,O,A)) is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (Swap (f,O,A)) : ( b1 in b2 & not (Swap (f,O,A)) /. b1 <= (Swap (f,O,A)) /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (Swap (f,O,A)) : ( b1 in b2 & (Swap (f,O,A)) /. b2 < (Swap (f,O,A)) /. b1 ) } is set
(Swap (f,O,A)) /. C is Element of the carrier of c5
f /. C is Element of the carrier of c5
(Swap (f,O,A)) /. B is Element of the carrier of c5
f /. B is Element of the carrier of c5
O is set
A is set
[O,A] is V30() set
{O,A} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,A},{O}} is non empty finite V53() set
C is set
[C,A] is V30() set
{C,A} is non empty finite set
{C} is non empty trivial finite 1 -element set
{{C,A},{C}} is non empty finite V53() set
[C,O] is V30() set
{C,O} is non empty finite set
{{C,O},{C}} is non empty finite V53() set
B is non empty reflexive transitive antisymmetric connected RelStr
the carrier of B is non empty set
c5 is Relation-like the carrier of B -valued Function-like () set
(B,c5) is Relation-like asymmetric transitive set
proj1 c5 is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5 : ( b1 in b2 & not c5 /. b1 <= c5 /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5 : ( b1 in b2 & c5 /. b2 < c5 /. b1 ) } is set
Swap (c5,O,A) is Relation-like the carrier of B -valued Function-like () set
(B,(Swap (c5,O,A))) is Relation-like asymmetric transitive set
proj1 (Swap (c5,O,A)) is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (Swap (c5,O,A)) : ( b1 in b2 & not (Swap (c5,O,A)) /. b1 <= (Swap (c5,O,A)) /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (Swap (c5,O,A)) : ( b1 in b2 & (Swap (c5,O,A)) /. b2 < (Swap (c5,O,A)) /. b1 ) } is set
c5 /. A is Element of the carrier of B
c5 /. O is Element of the carrier of B
(Swap (c5,O,A)) /. O is Element of the carrier of B
(Swap (c5,O,A)) /. A is Element of the carrier of B
c5 /. C is Element of the carrier of B
(Swap (c5,O,A)) /. C is Element of the carrier of B
O is set
A is set
[O,A] is V30() set
{O,A} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,A},{O}} is non empty finite V53() set
C is set
[C,O] is V30() set
{C,O} is non empty finite set
{C} is non empty trivial finite 1 -element set
{{C,O},{C}} is non empty finite V53() set
[C,A] is V30() set
{C,A} is non empty finite set
{{C,A},{C}} is non empty finite V53() set
B is non empty reflexive transitive antisymmetric connected RelStr
the carrier of B is non empty set
c5 is Relation-like the carrier of B -valued Function-like () set
(B,c5) is Relation-like asymmetric transitive set
proj1 c5 is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5 : ( b1 in b2 & not c5 /. b1 <= c5 /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5 : ( b1 in b2 & c5 /. b2 < c5 /. b1 ) } is set
Swap (c5,O,A) is Relation-like the carrier of B -valued Function-like () set
(B,(Swap (c5,O,A))) is Relation-like asymmetric transitive set
proj1 (Swap (c5,O,A)) is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (Swap (c5,O,A)) : ( b1 in b2 & not (Swap (c5,O,A)) /. b1 <= (Swap (c5,O,A)) /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (Swap (c5,O,A)) : ( b1 in b2 & (Swap (c5,O,A)) /. b2 < (Swap (c5,O,A)) /. b1 ) } is set
c5 /. A is Element of the carrier of B
c5 /. O is Element of the carrier of B
c5 /. C is Element of the carrier of B
(Swap (c5,O,A)) /. A is Element of the carrier of B
(Swap (c5,O,A)) /. C is Element of the carrier of B
O is set
A is set
[O,A] is V30() set
{O,A} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,A},{O}} is non empty finite V53() set
C is set
[O,C] is V30() set
{O,C} is non empty finite set
{{O,C},{O}} is non empty finite V53() set
B is non empty reflexive transitive antisymmetric connected RelStr
the carrier of B is non empty set
c5 is Relation-like the carrier of B -valued Function-like () set
(B,c5) is Relation-like asymmetric transitive set
proj1 c5 is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5 : ( b1 in b2 & not c5 /. b1 <= c5 /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5 : ( b1 in b2 & c5 /. b2 < c5 /. b1 ) } is set
Swap (c5,O,A) is Relation-like the carrier of B -valued Function-like () set
(B,(Swap (c5,O,A))) is Relation-like asymmetric transitive set
proj1 (Swap (c5,O,A)) is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (Swap (c5,O,A)) : ( b1 in b2 & not (Swap (c5,O,A)) /. b1 <= (Swap (c5,O,A)) /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (Swap (c5,O,A)) : ( b1 in b2 & (Swap (c5,O,A)) /. b2 < (Swap (c5,O,A)) /. b1 ) } is set
c5 /. A is Element of the carrier of B
c5 /. O is Element of the carrier of B
(Swap (c5,O,A)) /. C is Element of the carrier of B
(Swap (c5,O,A)) /. O is Element of the carrier of B
c5 /. C is Element of the carrier of B
O is set
A is set
[O,A] is V30() set
{O,A} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,A},{O}} is non empty finite V53() set
C is set
[C,A] is V30() set
{C,A} is non empty finite set
{C} is non empty trivial finite 1 -element set
{{C,A},{C}} is non empty finite V53() set
B is non empty reflexive transitive antisymmetric connected RelStr
the carrier of B is non empty set
c5 is Relation-like the carrier of B -valued Function-like () set
(B,c5) is Relation-like asymmetric transitive set
proj1 c5 is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5 : ( b1 in b2 & not c5 /. b1 <= c5 /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5 : ( b1 in b2 & c5 /. b2 < c5 /. b1 ) } is set
Swap (c5,O,A) is Relation-like the carrier of B -valued Function-like () set
(B,(Swap (c5,O,A))) is Relation-like asymmetric transitive set
proj1 (Swap (c5,O,A)) is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (Swap (c5,O,A)) : ( b1 in b2 & not (Swap (c5,O,A)) /. b1 <= (Swap (c5,O,A)) /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (Swap (c5,O,A)) : ( b1 in b2 & (Swap (c5,O,A)) /. b2 < (Swap (c5,O,A)) /. b1 ) } is set
c5 /. A is Element of the carrier of B
c5 /. O is Element of the carrier of B
(Swap (c5,O,A)) /. A is Element of the carrier of B
(Swap (c5,O,A)) /. C is Element of the carrier of B
c5 /. C is Element of the carrier of B
O is set
A is set
[O,A] is V30() set
{O,A} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,A},{O}} is non empty finite V53() set
C is set
[O,C] is V30() set
{O,C} is non empty finite set
{{O,C},{O}} is non empty finite V53() set
[A,C] is V30() set
{A,C} is non empty finite set
{A} is non empty trivial finite 1 -element set
{{A,C},{A}} is non empty finite V53() set
B is non empty reflexive transitive antisymmetric connected RelStr
the carrier of B is non empty set
c5 is Relation-like the carrier of B -valued Function-like () set
(B,c5) is Relation-like asymmetric transitive set
proj1 c5 is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5 : ( b1 in b2 & not c5 /. b1 <= c5 /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5 : ( b1 in b2 & c5 /. b2 < c5 /. b1 ) } is set
Swap (c5,O,A) is Relation-like the carrier of B -valued Function-like () set
(B,(Swap (c5,O,A))) is Relation-like asymmetric transitive set
proj1 (Swap (c5,O,A)) is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (Swap (c5,O,A)) : ( b1 in b2 & not (Swap (c5,O,A)) /. b1 <= (Swap (c5,O,A)) /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (Swap (c5,O,A)) : ( b1 in b2 & (Swap (c5,O,A)) /. b2 < (Swap (c5,O,A)) /. b1 ) } is set
c5 /. A is Element of the carrier of B
c5 /. O is Element of the carrier of B
(Swap (c5,O,A)) /. C is Element of the carrier of B
(Swap (c5,O,A)) /. O is Element of the carrier of B
c5 /. C is Element of the carrier of B
O is set
A is set
[O,A] is V30() set
{O,A} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,A},{O}} is non empty finite V53() set
C is set
[O,C] is V30() set
{O,C} is non empty finite set
{{O,C},{O}} is non empty finite V53() set
[A,C] is V30() set
{A,C} is non empty finite set
{A} is non empty trivial finite 1 -element set
{{A,C},{A}} is non empty finite V53() set
B is non empty reflexive transitive antisymmetric connected RelStr
the carrier of B is non empty set
c5 is Relation-like the carrier of B -valued Function-like () set
(B,c5) is Relation-like asymmetric transitive set
proj1 c5 is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5 : ( b1 in b2 & not c5 /. b1 <= c5 /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5 : ( b1 in b2 & c5 /. b2 < c5 /. b1 ) } is set
Swap (c5,O,A) is Relation-like the carrier of B -valued Function-like () set
(B,(Swap (c5,O,A))) is Relation-like asymmetric transitive set
proj1 (Swap (c5,O,A)) is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (Swap (c5,O,A)) : ( b1 in b2 & not (Swap (c5,O,A)) /. b1 <= (Swap (c5,O,A)) /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (Swap (c5,O,A)) : ( b1 in b2 & (Swap (c5,O,A)) /. b2 < (Swap (c5,O,A)) /. b1 ) } is set
c5 /. A is Element of the carrier of B
c5 /. O is Element of the carrier of B
c5 /. C is Element of the carrier of B
(Swap (c5,O,A)) /. A is Element of the carrier of B
(Swap (c5,O,A)) /. C is Element of the carrier of B
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like () set
proj1 A is ordinal-membered set
id (proj1 A) is Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]
[:(proj1 A),(proj1 A):] is Relation-like set
bool [:(proj1 A),(proj1 A):] is non empty set
C is set
B is set
Swap ((id (proj1 A)),C,B) is Relation-like proj1 A -defined proj1 A -valued Function-like set
[:(Swap ((id (proj1 A)),C,B)),(Swap ((id (proj1 A)),C,B)):] is Relation-like Function-like set
{C} is non empty trivial finite 1 -element set
succ B is non empty set
{B} is non empty trivial finite 1 -element set
B \/ {B} is non empty set
(succ B) \ C is Element of bool (succ B)
bool (succ B) is non empty set
[:{C},((succ B) \ C):] is Relation-like set
[:((succ B) \ C),{B}:] is Relation-like set
[:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:] is Relation-like set
id ([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]) is Relation-like [:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:] -defined [:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]),([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]):]
[:([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]),([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]):] is Relation-like set
bool [:([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]),([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]):] is non empty set
[:(Swap ((id (proj1 A)),C,B)),(Swap ((id (proj1 A)),C,B)):] +* (id ([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:])) is Relation-like Function-like set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
succ A is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{A} is non empty trivial finite 1 -element set
A \/ {A} is non empty set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(succ A) \ C is ordinal-membered Element of bool (succ A)
bool (succ A) is non empty set
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is non empty Relation-like the carrier of O -valued Function-like () set
proj1 A is non empty ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
succ C is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{C} is non empty trivial finite 1 -element set
C \/ {C} is non empty set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
(succ C) \ B is ordinal-membered Element of bool (succ C)
bool (succ C) is non empty set
c5 is set
f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
k is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f \ k is ordinal-membered Element of bool f
bool f is non empty set
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is non empty Relation-like the carrier of O -valued Function-like () set
proj1 A is non empty ordinal-membered set
[:(proj1 A),(proj1 A):] is non empty Relation-like set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
(O,A,C,B) is Relation-like Function-like set
id (proj1 A) is non empty Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]
bool [:(proj1 A),(proj1 A):] is non empty set
Swap ((id (proj1 A)),C,B) is Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total onto set
[:(Swap ((id (proj1 A)),C,B)),(Swap ((id (proj1 A)),C,B)):] is Relation-like Function-like set
{C} is non empty trivial finite 1 -element set
succ B is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{B} is non empty trivial finite 1 -element set
B \/ {B} is non empty set
(succ B) \ C is ordinal-membered Element of bool (succ B)
bool (succ B) is non empty set
[:{C},((succ B) \ C):] is Relation-like set
[:((succ B) \ C),{B}:] is Relation-like set
[:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:] is Relation-like set
id ([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]) is Relation-like [:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:] -defined [:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]),([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]):]
[:([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]),([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]):] is Relation-like set
bool [:([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]),([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]):] is non empty set
[:(Swap ((id (proj1 A)),C,B)),(Swap ((id (proj1 A)),C,B)):] +* (id ([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:])) is Relation-like Function-like set
proj1 (O,A,C,B) is set
proj2 (O,A,C,B) is set
((proj1 A),(proj1 A),(id (proj1 A)),C,B) is non empty Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]
[:((proj1 A),(proj1 A),(id (proj1 A)),C,B),((proj1 A),(proj1 A),(id (proj1 A)),C,B):] is non empty Relation-like [:(proj1 A),(proj1 A):] -defined [:(proj1 A),(proj1 A):] -valued Function-like total quasi_total Element of bool [:[:(proj1 A),(proj1 A):],[:(proj1 A),(proj1 A):]:]
[:[:(proj1 A),(proj1 A):],[:(proj1 A),(proj1 A):]:] is non empty Relation-like set
bool [:[:(proj1 A),(proj1 A):],[:(proj1 A),(proj1 A):]:] is non empty set
dom (id (proj1 A)) is non empty Element of bool (proj1 A)
bool (proj1 A) is non empty set
dom ((proj1 A),(proj1 A),(id (proj1 A)),C,B) is non empty Element of bool (proj1 A)
[:(proj1 A),(proj1 A):] \/ ([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]) is non empty Relation-like set
[:(proj1 A),(proj1 A):] \/ [:{C},((succ B) \ C):] is non empty Relation-like set
([:(proj1 A),(proj1 A):] \/ [:{C},((succ B) \ C):]) \/ [:((succ B) \ C),{B}:] is non empty Relation-like set
[:(proj1 A),(proj1 A):] \/ [:((succ B) \ C),{B}:] is non empty Relation-like set
dom [:((proj1 A),(proj1 A),(id (proj1 A)),C,B),((proj1 A),(proj1 A),(id (proj1 A)),C,B):] is non empty Relation-like proj1 A -defined proj1 A -valued Element of bool [:(proj1 A),(proj1 A):]
dom (id ([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:])) is Relation-like Element of bool ([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:])
bool ([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]) is non empty set
(dom [:((proj1 A),(proj1 A),(id (proj1 A)),C,B),((proj1 A),(proj1 A),(id (proj1 A)),C,B):]) \/ (dom (id ([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]))) is non empty Relation-like set
(dom [:((proj1 A),(proj1 A),(id (proj1 A)),C,B),((proj1 A),(proj1 A),(id (proj1 A)),C,B):]) \/ ([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]) is non empty Relation-like set
proj2 (id ([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:])) is set
proj2 (id (proj1 A)) is non empty set
proj2 ((proj1 A),(proj1 A),(id (proj1 A)),C,B) is non empty set
proj2 [:((proj1 A),(proj1 A),(id (proj1 A)),C,B),((proj1 A),(proj1 A),(id (proj1 A)),C,B):] is non empty Relation-like set
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is non empty Relation-like the carrier of O -valued Function-like () set
proj1 A is non empty ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
[C,B] is V30() set
{C,B} is non empty finite set
{C} is non empty trivial finite 1 -element set
{{C,B},{C}} is non empty finite V53() set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
(O,A,C,c5) is Relation-like Function-like set
id (proj1 A) is non empty Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]
[:(proj1 A),(proj1 A):] is non empty Relation-like set
bool [:(proj1 A),(proj1 A):] is non empty set
Swap ((id (proj1 A)),C,c5) is Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total onto set
[:(Swap ((id (proj1 A)),C,c5)),(Swap ((id (proj1 A)),C,c5)):] is Relation-like Function-like set
succ c5 is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{c5} is non empty trivial finite 1 -element set
c5 \/ {c5} is non empty set
(succ c5) \ C is ordinal-membered Element of bool (succ c5)
bool (succ c5) is non empty set
[:{C},((succ c5) \ C):] is Relation-like set
[:((succ c5) \ C),{c5}:] is Relation-like set
[:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:] is Relation-like set
id ([:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:]) is Relation-like [:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:] -defined [:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:([:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:]),([:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:]):]
[:([:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:]),([:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:]):] is Relation-like set
bool [:([:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:]),([:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:]):] is non empty set
[:(Swap ((id (proj1 A)),C,c5)),(Swap ((id (proj1 A)),C,c5)):] +* (id ([:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:])) is Relation-like Function-like set
(O,A,C,c5) . (C,B) is set
(O,A,C,c5) . [C,B] is set
(O,A,C,c5) . (B,c5) is set
[B,c5] is V30() set
{B,c5} is non empty finite set
{B} is non empty trivial finite 1 -element set
{{B,c5},{B}} is non empty finite V53() set
(O,A,C,c5) . [B,c5] is set
dom (id ([:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:])) is Relation-like Element of bool ([:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:])
bool ([:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:]) is non empty set
(id ([:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:])) . (C,B) is set
(id ([:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:])) . [C,B] is set
(id ([:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:])) . (B,c5) is set
(id ([:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:])) . [B,c5] is set
O is Relation-like Function-like set
A is non empty reflexive transitive antisymmetric connected RelStr
the carrier of A is non empty set
C is non empty Relation-like the carrier of A -valued Function-like () set
proj1 C is non empty ordinal-membered set
id (proj1 C) is non empty Relation-like proj1 C -defined proj1 C -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 C),(proj1 C):]
[:(proj1 C),(proj1 C):] is non empty Relation-like set
bool [:(proj1 C),(proj1 C):] is non empty set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 C
O . B is set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 C
f is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 C
O . f is set
[(O . B),(O . f)] is V30() set
{(O . B),(O . f)} is non empty finite set
{(O . B)} is non empty trivial finite 1 -element set
{{(O . B),(O . f)},{(O . B)}} is non empty finite V53() set
k is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 C
((proj1 C),(proj1 C),(id (proj1 C)),c5,k) is non empty Relation-like proj1 C -defined proj1 C -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 C),(proj1 C):]
(A,C,c5,k) is Relation-like Function-like set
Swap ((id (proj1 C)),c5,k) is Relation-like proj1 C -defined proj1 C -valued Function-like one-to-one total onto set
[:(Swap ((id (proj1 C)),c5,k)),(Swap ((id (proj1 C)),c5,k)):] is Relation-like Function-like set
{c5} is non empty trivial finite 1 -element set
succ k is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{k} is non empty trivial finite 1 -element set
k \/ {k} is non empty set
(succ k) \ c5 is ordinal-membered Element of bool (succ k)
bool (succ k) is non empty set
[:{c5},((succ k) \ c5):] is Relation-like set
[:((succ k) \ c5),{k}:] is Relation-like set
[:{c5},((succ k) \ c5):] \/ [:((succ k) \ c5),{k}:] is Relation-like set
id ([:{c5},((succ k) \ c5):] \/ [:((succ k) \ c5),{k}:]) is Relation-like [:{c5},((succ k) \ c5):] \/ [:((succ k) \ c5),{k}:] -defined [:{c5},((succ k) \ c5):] \/ [:((succ k) \ c5),{k}:] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:([:{c5},((succ k) \ c5):] \/ [:((succ k) \ c5),{k}:]),([:{c5},((succ k) \ c5):] \/ [:((succ k) \ c5),{k}:]):]
[:([:{c5},((succ k) \ c5):] \/ [:((succ k) \ c5),{k}:]),([:{c5},((succ k) \ c5):] \/ [:((succ k) \ c5),{k}:]):] is Relation-like set
bool [:([:{c5},((succ k) \ c5):] \/ [:((succ k) \ c5),{k}:]),([:{c5},((succ k) \ c5):] \/ [:((succ k) \ c5),{k}:]):] is non empty set
[:(Swap ((id (proj1 C)),c5,k)),(Swap ((id (proj1 C)),c5,k)):] +* (id ([:{c5},((succ k) \ c5):] \/ [:((succ k) \ c5),{k}:])) is Relation-like Function-like set
(A,C,c5,k) . (B,f) is set
[B,f] is V30() set
{B,f} is non empty finite set
{B} is non empty trivial finite 1 -element set
{{B,f},{B}} is non empty finite V53() set
(A,C,c5,k) . [B,f] is set
proj1 O is set
dom (id (proj1 C)) is non empty Element of bool (proj1 C)
bool (proj1 C) is non empty set
dom (id ([:{c5},((succ k) \ c5):] \/ [:((succ k) \ c5),{k}:])) is Relation-like Element of bool ([:{c5},((succ k) \ c5):] \/ [:((succ k) \ c5),{k}:])
bool ([:{c5},((succ k) \ c5):] \/ [:((succ k) \ c5),{k}:]) is non empty set
[:O,O:] is Relation-like Function-like set
[:O,O:] . (B,f) is set
[:O,O:] . [B,f] is set
O is Relation-like Function-like set
A is non empty reflexive transitive antisymmetric connected RelStr
the carrier of A is non empty set
C is non empty Relation-like the carrier of A -valued Function-like () set
proj1 C is non empty ordinal-membered set
id (proj1 C) is non empty Relation-like proj1 C -defined proj1 C -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 C),(proj1 C):]
[:(proj1 C),(proj1 C):] is non empty Relation-like set
bool [:(proj1 C),(proj1 C):] is non empty set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 C
O . B is set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 C
O . c5 is set
[(O . B),(O . c5)] is V30() set
{(O . B),(O . c5)} is non empty finite set
{(O . B)} is non empty trivial finite 1 -element set
{{(O . B),(O . c5)},{(O . B)}} is non empty finite V53() set
f is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 C
((proj1 C),(proj1 C),(id (proj1 C)),c5,f) is non empty Relation-like proj1 C -defined proj1 C -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 C),(proj1 C):]
(A,C,c5,f) is Relation-like Function-like set
Swap ((id (proj1 C)),c5,f) is Relation-like proj1 C -defined proj1 C -valued Function-like one-to-one total onto set
[:(Swap ((id (proj1 C)),c5,f)),(Swap ((id (proj1 C)),c5,f)):] is Relation-like Function-like set
{c5} is non empty trivial finite 1 -element set
succ f is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{f} is non empty trivial finite 1 -element set
f \/ {f} is non empty set
(succ f) \ c5 is ordinal-membered Element of bool (succ f)
bool (succ f) is non empty set
[:{c5},((succ f) \ c5):] is Relation-like set
[:((succ f) \ c5),{f}:] is Relation-like set
[:{c5},((succ f) \ c5):] \/ [:((succ f) \ c5),{f}:] is Relation-like set
id ([:{c5},((succ f) \ c5):] \/ [:((succ f) \ c5),{f}:]) is Relation-like [:{c5},((succ f) \ c5):] \/ [:((succ f) \ c5),{f}:] -defined [:{c5},((succ f) \ c5):] \/ [:((succ f) \ c5),{f}:] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:([:{c5},((succ f) \ c5):] \/ [:((succ f) \ c5),{f}:]),([:{c5},((succ f) \ c5):] \/ [:((succ f) \ c5),{f}:]):]
[:([:{c5},((succ f) \ c5):] \/ [:((succ f) \ c5),{f}:]),([:{c5},((succ f) \ c5):] \/ [:((succ f) \ c5),{f}:]):] is Relation-like set
bool [:([:{c5},((succ f) \ c5):] \/ [:((succ f) \ c5),{f}:]),([:{c5},((succ f) \ c5):] \/ [:((succ f) \ c5),{f}:]):] is non empty set
[:(Swap ((id (proj1 C)),c5,f)),(Swap ((id (proj1 C)),c5,f)):] +* (id ([:{c5},((succ f) \ c5):] \/ [:((succ f) \ c5),{f}:])) is Relation-like Function-like set
(A,C,c5,f) . (B,f) is set
[B,f] is V30() set
{B,f} is non empty finite set
{B} is non empty trivial finite 1 -element set
{{B,f},{B}} is non empty finite V53() set
(A,C,c5,f) . [B,f] is set
O . f is set
[(O . B),(O . f)] is V30() set
{(O . B),(O . f)} is non empty finite set
{{(O . B),(O . f)},{(O . B)}} is non empty finite V53() set
(A,C,c5,f) . (B,c5) is set
[B,c5] is V30() set
{B,c5} is non empty finite set
{{B,c5},{B}} is non empty finite V53() set
(A,C,c5,f) . [B,c5] is set
[:((proj1 C),(proj1 C),(id (proj1 C)),c5,f),((proj1 C),(proj1 C),(id (proj1 C)),c5,f):] is non empty Relation-like [:(proj1 C),(proj1 C):] -defined [:(proj1 C),(proj1 C):] -valued Function-like total quasi_total Element of bool [:[:(proj1 C),(proj1 C):],[:(proj1 C),(proj1 C):]:]
[:[:(proj1 C),(proj1 C):],[:(proj1 C),(proj1 C):]:] is non empty Relation-like set
bool [:[:(proj1 C),(proj1 C):],[:(proj1 C),(proj1 C):]:] is non empty set
dom (id (proj1 C)) is non empty Element of bool (proj1 C)
bool (proj1 C) is non empty set
dom ((proj1 C),(proj1 C),(id (proj1 C)),c5,f) is non empty Element of bool (proj1 C)
dom (id ([:{c5},((succ f) \ c5):] \/ [:((succ f) \ c5),{f}:])) is Relation-like Element of bool ([:{c5},((succ f) \ c5):] \/ [:((succ f) \ c5),{f}:])
bool ([:{c5},((succ f) \ c5):] \/ [:((succ f) \ c5),{f}:]) is non empty set
[:((proj1 C),(proj1 C),(id (proj1 C)),c5,f),((proj1 C),(proj1 C),(id (proj1 C)),c5,f):] . (B,f) is Element of [:(proj1 C),(proj1 C):]
[:((proj1 C),(proj1 C),(id (proj1 C)),c5,f),((proj1 C),(proj1 C),(id (proj1 C)),c5,f):] . [B,f] is set
[:((proj1 C),(proj1 C),(id (proj1 C)),c5,f),((proj1 C),(proj1 C),(id (proj1 C)),c5,f):] . (B,c5) is Element of [:(proj1 C),(proj1 C):]
[:((proj1 C),(proj1 C),(id (proj1 C)),c5,f),((proj1 C),(proj1 C),(id (proj1 C)),c5,f):] . [B,c5] is set
O is Relation-like Function-like set
A is non empty reflexive transitive antisymmetric connected RelStr
the carrier of A is non empty set
C is non empty Relation-like the carrier of A -valued Function-like () set
proj1 C is non empty ordinal-membered set
id (proj1 C) is non empty Relation-like proj1 C -defined proj1 C -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 C),(proj1 C):]
[:(proj1 C),(proj1 C):] is non empty Relation-like set
bool [:(proj1 C),(proj1 C):] is non empty set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 C
O . B is set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 C
O . c5 is set
[(O . B),(O . c5)] is V30() set
{(O . B),(O . c5)} is non empty finite set
{(O . B)} is non empty trivial finite 1 -element set
{{(O . B),(O . c5)},{(O . B)}} is non empty finite V53() set
f is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 C
((proj1 C),(proj1 C),(id (proj1 C)),f,B) is non empty Relation-like proj1 C -defined proj1 C -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 C),(proj1 C):]
(A,C,f,B) is Relation-like Function-like set
Swap ((id (proj1 C)),f,B) is Relation-like proj1 C -defined proj1 C -valued Function-like one-to-one total onto set
[:(Swap ((id (proj1 C)),f,B)),(Swap ((id (proj1 C)),f,B)):] is Relation-like Function-like set
{f} is non empty trivial finite 1 -element set
succ B is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{B} is non empty trivial finite 1 -element set
B \/ {B} is non empty set
(succ B) \ f is ordinal-membered Element of bool (succ B)
bool (succ B) is non empty set
[:{f},((succ B) \ f):] is Relation-like set
[:((succ B) \ f),{B}:] is Relation-like set
[:{f},((succ B) \ f):] \/ [:((succ B) \ f),{B}:] is Relation-like set
id ([:{f},((succ B) \ f):] \/ [:((succ B) \ f),{B}:]) is Relation-like [:{f},((succ B) \ f):] \/ [:((succ B) \ f),{B}:] -defined [:{f},((succ B) \ f):] \/ [:((succ B) \ f),{B}:] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:([:{f},((succ B) \ f):] \/ [:((succ B) \ f),{B}:]),([:{f},((succ B) \ f):] \/ [:((succ B) \ f),{B}:]):]
[:([:{f},((succ B) \ f):] \/ [:((succ B) \ f),{B}:]),([:{f},((succ B) \ f):] \/ [:((succ B) \ f),{B}:]):] is Relation-like set
bool [:([:{f},((succ B) \ f):] \/ [:((succ B) \ f),{B}:]),([:{f},((succ B) \ f):] \/ [:((succ B) \ f),{B}:]):] is non empty set
[:(Swap ((id (proj1 C)),f,B)),(Swap ((id (proj1 C)),f,B)):] +* (id ([:{f},((succ B) \ f):] \/ [:((succ B) \ f),{B}:])) is Relation-like Function-like set
(A,C,f,B) . (f,c5) is set
[f,c5] is V30() set
{f,c5} is non empty finite set
{{f,c5},{f}} is non empty finite V53() set
(A,C,f,B) . [f,c5] is set
O . f is set
[(O . f),(O . c5)] is V30() set
{(O . f),(O . c5)} is non empty finite set
{(O . f)} is non empty trivial finite 1 -element set
{{(O . f),(O . c5)},{(O . f)}} is non empty finite V53() set
(A,C,f,B) . (B,c5) is set
[B,c5] is V30() set
{B,c5} is non empty finite set
{{B,c5},{B}} is non empty finite V53() set
(A,C,f,B) . [B,c5] is set
[:((proj1 C),(proj1 C),(id (proj1 C)),f,B),((proj1 C),(proj1 C),(id (proj1 C)),f,B):] is non empty Relation-like [:(proj1 C),(proj1 C):] -defined [:(proj1 C),(proj1 C):] -valued Function-like total quasi_total Element of bool [:[:(proj1 C),(proj1 C):],[:(proj1 C),(proj1 C):]:]
[:[:(proj1 C),(proj1 C):],[:(proj1 C),(proj1 C):]:] is non empty Relation-like set
bool [:[:(proj1 C),(proj1 C):],[:(proj1 C),(proj1 C):]:] is non empty set
dom (id (proj1 C)) is non empty Element of bool (proj1 C)
bool (proj1 C) is non empty set
dom ((proj1 C),(proj1 C),(id (proj1 C)),f,B) is non empty Element of bool (proj1 C)
dom (id ([:{f},((succ B) \ f):] \/ [:((succ B) \ f),{B}:])) is Relation-like Element of bool ([:{f},((succ B) \ f):] \/ [:((succ B) \ f),{B}:])
bool ([:{f},((succ B) \ f):] \/ [:((succ B) \ f),{B}:]) is non empty set
[:((proj1 C),(proj1 C),(id (proj1 C)),f,B),((proj1 C),(proj1 C),(id (proj1 C)),f,B):] . (f,c5) is Element of [:(proj1 C),(proj1 C):]
[:((proj1 C),(proj1 C),(id (proj1 C)),f,B),((proj1 C),(proj1 C),(id (proj1 C)),f,B):] . [f,c5] is set
[:((proj1 C),(proj1 C),(id (proj1 C)),f,B),((proj1 C),(proj1 C),(id (proj1 C)),f,B):] . (B,c5) is Element of [:(proj1 C),(proj1 C):]
[:((proj1 C),(proj1 C),(id (proj1 C)),f,B),((proj1 C),(proj1 C),(id (proj1 C)),f,B):] . [B,c5] is set
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is non empty Relation-like the carrier of O -valued Function-like () set
proj1 A is non empty ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
(O,A,C,B) is Relation-like Function-like set
id (proj1 A) is non empty Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]
[:(proj1 A),(proj1 A):] is non empty Relation-like set
bool [:(proj1 A),(proj1 A):] is non empty set
Swap ((id (proj1 A)),C,B) is Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total onto set
[:(Swap ((id (proj1 A)),C,B)),(Swap ((id (proj1 A)),C,B)):] is Relation-like Function-like set
{C} is non empty trivial finite 1 -element set
succ B is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{B} is non empty trivial finite 1 -element set
B \/ {B} is non empty set
(succ B) \ C is ordinal-membered Element of bool (succ B)
bool (succ B) is non empty set
[:{C},((succ B) \ C):] is Relation-like set
[:((succ B) \ C),{B}:] is Relation-like set
[:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:] is Relation-like set
id ([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]) is Relation-like [:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:] -defined [:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]),([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]):]
[:([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]),([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]):] is Relation-like set
bool [:([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]),([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]):] is non empty set
[:(Swap ((id (proj1 A)),C,B)),(Swap ((id (proj1 A)),C,B)):] +* (id ([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:])) is Relation-like Function-like set
(O,A,C,B) . (C,B) is set
[C,B] is V30() set
{C,B} is non empty finite set
{{C,B},{C}} is non empty finite V53() set
(O,A,C,B) . [C,B] is set
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is non empty Relation-like the carrier of O -valued Function-like () set
proj1 A is non empty ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
(O,A,C,B) is Relation-like Function-like set
id (proj1 A) is non empty Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]
[:(proj1 A),(proj1 A):] is non empty Relation-like set
bool [:(proj1 A),(proj1 A):] is non empty set
Swap ((id (proj1 A)),C,B) is Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total onto set
[:(Swap ((id (proj1 A)),C,B)),(Swap ((id (proj1 A)),C,B)):] is Relation-like Function-like set
{C} is non empty trivial finite 1 -element set
succ B is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{B} is non empty trivial finite 1 -element set
B \/ {B} is non empty set
(succ B) \ C is ordinal-membered Element of bool (succ B)
bool (succ B) is non empty set
[:{C},((succ B) \ C):] is Relation-like set
[:((succ B) \ C),{B}:] is Relation-like set
[:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:] is Relation-like set
id ([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]) is Relation-like [:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:] -defined [:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]),([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]):]
[:([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]),([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]):] is Relation-like set
bool [:([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]),([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]):] is non empty set
[:(Swap ((id (proj1 A)),C,B)),(Swap ((id (proj1 A)),C,B)):] +* (id ([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:])) is Relation-like Function-like set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
f is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
(O,A,C,B) . (c5,f) is set
[c5,f] is V30() set
{c5,f} is non empty finite set
{c5} is non empty trivial finite 1 -element set
{{c5,f},{c5}} is non empty finite V53() set
(O,A,C,B) . [c5,f] is set
((proj1 A),(proj1 A),(id (proj1 A)),C,B) is non empty Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]
[:((proj1 A),(proj1 A),(id (proj1 A)),C,B),((proj1 A),(proj1 A),(id (proj1 A)),C,B):] is non empty Relation-like [:(proj1 A),(proj1 A):] -defined [:(proj1 A),(proj1 A):] -valued Function-like total quasi_total Element of bool [:[:(proj1 A),(proj1 A):],[:(proj1 A),(proj1 A):]:]
[:[:(proj1 A),(proj1 A):],[:(proj1 A),(proj1 A):]:] is non empty Relation-like set
bool [:[:(proj1 A),(proj1 A):],[:(proj1 A),(proj1 A):]:] is non empty set
((proj1 A),(proj1 A),(id (proj1 A)),C,B) . c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
((proj1 A),(proj1 A),(id (proj1 A)),C,B) . f is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
[(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . c5),(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . f)] is V30() set
{(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . c5),(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . f)} is non empty finite set
{(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . c5)} is non empty trivial finite 1 -element set
{{(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . c5),(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . f)},{(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . c5)}} is non empty finite V53() set
(id (proj1 A)) . c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
[((id (proj1 A)) . c5),(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . f)] is V30() set
{((id (proj1 A)) . c5),(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . f)} is non empty finite set
{((id (proj1 A)) . c5)} is non empty trivial finite 1 -element set
{{((id (proj1 A)) . c5),(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . f)},{((id (proj1 A)) . c5)}} is non empty finite V53() set
(id (proj1 A)) . f is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
[((id (proj1 A)) . c5),((id (proj1 A)) . f)] is V30() set
{((id (proj1 A)) . c5),((id (proj1 A)) . f)} is non empty finite set
{{((id (proj1 A)) . c5),((id (proj1 A)) . f)},{((id (proj1 A)) . c5)}} is non empty finite V53() set
[c5,((id (proj1 A)) . f)] is V30() set
{c5,((id (proj1 A)) . f)} is non empty finite set
{{c5,((id (proj1 A)) . f)},{c5}} is non empty finite V53() set
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is non empty Relation-like the carrier of O -valued Function-like () set
proj1 A is non empty ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
[C,B] is V30() set
{C,B} is non empty finite set
{C} is non empty trivial finite 1 -element set
{{C,B},{C}} is non empty finite V53() set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
(O,A,B,c5) is Relation-like Function-like set
id (proj1 A) is non empty Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]
[:(proj1 A),(proj1 A):] is non empty Relation-like set
bool [:(proj1 A),(proj1 A):] is non empty set
Swap ((id (proj1 A)),B,c5) is Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total onto set
[:(Swap ((id (proj1 A)),B,c5)),(Swap ((id (proj1 A)),B,c5)):] is Relation-like Function-like set
{B} is non empty trivial finite 1 -element set
succ c5 is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{c5} is non empty trivial finite 1 -element set
c5 \/ {c5} is non empty set
(succ c5) \ B is ordinal-membered Element of bool (succ c5)
bool (succ c5) is non empty set
[:{B},((succ c5) \ B):] is Relation-like set
[:((succ c5) \ B),{c5}:] is Relation-like set
[:{B},((succ c5) \ B):] \/ [:((succ c5) \ B),{c5}:] is Relation-like set
id ([:{B},((succ c5) \ B):] \/ [:((succ c5) \ B),{c5}:]) is Relation-like [:{B},((succ c5) \ B):] \/ [:((succ c5) \ B),{c5}:] -defined [:{B},((succ c5) \ B):] \/ [:((succ c5) \ B),{c5}:] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:([:{B},((succ c5) \ B):] \/ [:((succ c5) \ B),{c5}:]),([:{B},((succ c5) \ B):] \/ [:((succ c5) \ B),{c5}:]):]
[:([:{B},((succ c5) \ B):] \/ [:((succ c5) \ B),{c5}:]),([:{B},((succ c5) \ B):] \/ [:((succ c5) \ B),{c5}:]):] is Relation-like set
bool [:([:{B},((succ c5) \ B):] \/ [:((succ c5) \ B),{c5}:]),([:{B},((succ c5) \ B):] \/ [:((succ c5) \ B),{c5}:]):] is non empty set
[:(Swap ((id (proj1 A)),B,c5)),(Swap ((id (proj1 A)),B,c5)):] +* (id ([:{B},((succ c5) \ B):] \/ [:((succ c5) \ B),{c5}:])) is Relation-like Function-like set
(O,A,B,c5) . (C,B) is set
(O,A,B,c5) . [C,B] is set
[C,c5] is V30() set
{C,c5} is non empty finite set
{{C,c5},{C}} is non empty finite V53() set
(O,A,B,c5) . (C,c5) is set
(O,A,B,c5) . [C,c5] is set
((proj1 A),(proj1 A),(id (proj1 A)),B,c5) is non empty Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]
[:((proj1 A),(proj1 A),(id (proj1 A)),B,c5),((proj1 A),(proj1 A),(id (proj1 A)),B,c5):] is non empty Relation-like [:(proj1 A),(proj1 A):] -defined [:(proj1 A),(proj1 A):] -valued Function-like total quasi_total Element of bool [:[:(proj1 A),(proj1 A):],[:(proj1 A),(proj1 A):]:]
[:[:(proj1 A),(proj1 A):],[:(proj1 A),(proj1 A):]:] is non empty Relation-like set
bool [:[:(proj1 A),(proj1 A):],[:(proj1 A),(proj1 A):]:] is non empty set
dom (id (proj1 A)) is non empty Element of bool (proj1 A)
bool (proj1 A) is non empty set
((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . C is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
[(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . C),(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . B)] is V30() set
{(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . C),(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . B)} is non empty finite set
{(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . C)} is non empty trivial finite 1 -element set
{{(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . C),(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . B)},{(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . C)}} is non empty finite V53() set
(id (proj1 A)) . C is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
[((id (proj1 A)) . C),(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . B)] is V30() set
{((id (proj1 A)) . C),(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . B)} is non empty finite set
{((id (proj1 A)) . C)} is non empty trivial finite 1 -element set
{{((id (proj1 A)) . C),(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . B)},{((id (proj1 A)) . C)}} is non empty finite V53() set
[C,(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . B)] is V30() set
{C,(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . B)} is non empty finite set
{{C,(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . B)},{C}} is non empty finite V53() set
(id (proj1 A)) . c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
[C,((id (proj1 A)) . c5)] is V30() set
{C,((id (proj1 A)) . c5)} is non empty finite set
{{C,((id (proj1 A)) . c5)},{C}} is non empty finite V53() set
((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
[(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . C),(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . c5)] is V30() set
{(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . C),(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . c5)} is non empty finite set
{{(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . C),(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . c5)},{(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . C)}} is non empty finite V53() set
[((id (proj1 A)) . C),(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . c5)] is V30() set
{((id (proj1 A)) . C),(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . c5)} is non empty finite set
{{((id (proj1 A)) . C),(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . c5)},{((id (proj1 A)) . C)}} is non empty finite V53() set
[C,(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . c5)] is V30() set
{C,(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . c5)} is non empty finite set
{{C,(((proj1 A),(proj1 A),(id (proj1 A)),B,c5) . c5)},{C}} is non empty finite V53() set
(id (proj1 A)) . B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
[C,((id (proj1 A)) . B)] is V30() set
{C,((id (proj1 A)) . B)} is non empty finite set
{{C,((id (proj1 A)) . B)},{C}} is non empty finite V53() set
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is non empty Relation-like the carrier of O -valued Function-like () set
proj1 A is non empty ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
[C,B] is V30() set
{C,B} is non empty finite set
{C} is non empty trivial finite 1 -element set
{{C,B},{C}} is non empty finite V53() set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
(O,A,C,c5) is Relation-like Function-like set
id (proj1 A) is non empty Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]
[:(proj1 A),(proj1 A):] is non empty Relation-like set
bool [:(proj1 A),(proj1 A):] is non empty set
Swap ((id (proj1 A)),C,c5) is Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total onto set
[:(Swap ((id (proj1 A)),C,c5)),(Swap ((id (proj1 A)),C,c5)):] is Relation-like Function-like set
succ c5 is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{c5} is non empty trivial finite 1 -element set
c5 \/ {c5} is non empty set
(succ c5) \ C is ordinal-membered Element of bool (succ c5)
bool (succ c5) is non empty set
[:{C},((succ c5) \ C):] is Relation-like set
[:((succ c5) \ C),{c5}:] is Relation-like set
[:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:] is Relation-like set
id ([:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:]) is Relation-like [:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:] -defined [:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:([:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:]),([:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:]):]
[:([:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:]),([:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:]):] is Relation-like set
bool [:([:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:]),([:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:]):] is non empty set
[:(Swap ((id (proj1 A)),C,c5)),(Swap ((id (proj1 A)),C,c5)):] +* (id ([:{C},((succ c5) \ C):] \/ [:((succ c5) \ C),{c5}:])) is Relation-like Function-like set
(O,A,C,c5) . (C,B) is set
(O,A,C,c5) . [C,B] is set
(O,A,C,c5) . (B,c5) is set
[B,c5] is V30() set
{B,c5} is non empty finite set
{B} is non empty trivial finite 1 -element set
{{B,c5},{B}} is non empty finite V53() set
(O,A,C,c5) . [B,c5] is set
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is non empty Relation-like the carrier of O -valued Function-like () set
proj1 A is non empty ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
(O,A,C,B) is Relation-like Function-like set
id (proj1 A) is non empty Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]
[:(proj1 A),(proj1 A):] is non empty Relation-like set
bool [:(proj1 A),(proj1 A):] is non empty set
Swap ((id (proj1 A)),C,B) is Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total onto set
[:(Swap ((id (proj1 A)),C,B)),(Swap ((id (proj1 A)),C,B)):] is Relation-like Function-like set
{C} is non empty trivial finite 1 -element set
succ B is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{B} is non empty trivial finite 1 -element set
B \/ {B} is non empty set
(succ B) \ C is ordinal-membered Element of bool (succ B)
bool (succ B) is non empty set
[:{C},((succ B) \ C):] is Relation-like set
[:((succ B) \ C),{B}:] is Relation-like set
[:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:] is Relation-like set
id ([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]) is Relation-like [:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:] -defined [:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]),([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]):]
[:([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]),([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]):] is Relation-like set
bool [:([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]),([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]):] is non empty set
[:(Swap ((id (proj1 A)),C,B)),(Swap ((id (proj1 A)),C,B)):] +* (id ([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:])) is Relation-like Function-like set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
(O,A,C,B) . (C,c5) is set
[C,c5] is V30() set
{C,c5} is non empty finite set
{{C,c5},{C}} is non empty finite V53() set
(O,A,C,B) . [C,c5] is set
[B,c5] is V30() set
{B,c5} is non empty finite set
{{B,c5},{B}} is non empty finite V53() set
(O,A,C,B) . (B,c5) is set
(O,A,C,B) . [B,c5] is set
((proj1 A),(proj1 A),(id (proj1 A)),C,B) is non empty Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]
[:((proj1 A),(proj1 A),(id (proj1 A)),C,B),((proj1 A),(proj1 A),(id (proj1 A)),C,B):] is non empty Relation-like [:(proj1 A),(proj1 A):] -defined [:(proj1 A),(proj1 A):] -valued Function-like total quasi_total Element of bool [:[:(proj1 A),(proj1 A):],[:(proj1 A),(proj1 A):]:]
[:[:(proj1 A),(proj1 A):],[:(proj1 A),(proj1 A):]:] is non empty Relation-like set
bool [:[:(proj1 A),(proj1 A):],[:(proj1 A),(proj1 A):]:] is non empty set
dom (id (proj1 A)) is non empty Element of bool (proj1 A)
bool (proj1 A) is non empty set
((proj1 A),(proj1 A),(id (proj1 A)),C,B) . C is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
((proj1 A),(proj1 A),(id (proj1 A)),C,B) . c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
[(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . C),(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . c5)] is V30() set
{(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . C),(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . c5)} is non empty finite set
{(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . C)} is non empty trivial finite 1 -element set
{{(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . C),(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . c5)},{(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . C)}} is non empty finite V53() set
(id (proj1 A)) . c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
[(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . C),((id (proj1 A)) . c5)] is V30() set
{(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . C),((id (proj1 A)) . c5)} is non empty finite set
{{(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . C),((id (proj1 A)) . c5)},{(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . C)}} is non empty finite V53() set
[(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . C),c5] is V30() set
{(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . C),c5} is non empty finite set
{{(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . C),c5},{(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . C)}} is non empty finite V53() set
(id (proj1 A)) . B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
[((id (proj1 A)) . B),c5] is V30() set
{((id (proj1 A)) . B),c5} is non empty finite set
{((id (proj1 A)) . B)} is non empty trivial finite 1 -element set
{{((id (proj1 A)) . B),c5},{((id (proj1 A)) . B)}} is non empty finite V53() set
((proj1 A),(proj1 A),(id (proj1 A)),C,B) . B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
[(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . B),(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . c5)] is V30() set
{(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . B),(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . c5)} is non empty finite set
{(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . B)} is non empty trivial finite 1 -element set
{{(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . B),(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . c5)},{(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . B)}} is non empty finite V53() set
[(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . B),((id (proj1 A)) . c5)] is V30() set
{(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . B),((id (proj1 A)) . c5)} is non empty finite set
{{(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . B),((id (proj1 A)) . c5)},{(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . B)}} is non empty finite V53() set
[(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . B),c5] is V30() set
{(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . B),c5} is non empty finite set
{{(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . B),c5},{(((proj1 A),(proj1 A),(id (proj1 A)),C,B) . B)}} is non empty finite V53() set
(id (proj1 A)) . C is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
[((id (proj1 A)) . C),c5] is V30() set
{((id (proj1 A)) . C),c5} is non empty finite set
{((id (proj1 A)) . C)} is non empty trivial finite 1 -element set
{{((id (proj1 A)) . C),c5},{((id (proj1 A)) . C)}} is non empty finite V53() set
O is Relation-like Function-like set
A is non empty reflexive transitive antisymmetric connected RelStr
the carrier of A is non empty set
C is non empty Relation-like the carrier of A -valued Function-like () set
proj1 C is non empty ordinal-membered set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 C
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 C
(A,C,B,c5) is Relation-like Function-like set
id (proj1 C) is non empty Relation-like proj1 C -defined proj1 C -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 C),(proj1 C):]
[:(proj1 C),(proj1 C):] is non empty Relation-like set
bool [:(proj1 C),(proj1 C):] is non empty set
Swap ((id (proj1 C)),B,c5) is Relation-like proj1 C -defined proj1 C -valued Function-like one-to-one total onto set
[:(Swap ((id (proj1 C)),B,c5)),(Swap ((id (proj1 C)),B,c5)):] is Relation-like Function-like set
{B} is non empty trivial finite 1 -element set
succ c5 is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{c5} is non empty trivial finite 1 -element set
c5 \/ {c5} is non empty set
(succ c5) \ B is ordinal-membered Element of bool (succ c5)
bool (succ c5) is non empty set
[:{B},((succ c5) \ B):] is Relation-like set
[:((succ c5) \ B),{c5}:] is Relation-like set
[:{B},((succ c5) \ B):] \/ [:((succ c5) \ B),{c5}:] is Relation-like set
id ([:{B},((succ c5) \ B):] \/ [:((succ c5) \ B),{c5}:]) is Relation-like [:{B},((succ c5) \ B):] \/ [:((succ c5) \ B),{c5}:] -defined [:{B},((succ c5) \ B):] \/ [:((succ c5) \ B),{c5}:] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:([:{B},((succ c5) \ B):] \/ [:((succ c5) \ B),{c5}:]),([:{B},((succ c5) \ B):] \/ [:((succ c5) \ B),{c5}:]):]
[:([:{B},((succ c5) \ B):] \/ [:((succ c5) \ B),{c5}:]),([:{B},((succ c5) \ B):] \/ [:((succ c5) \ B),{c5}:]):] is Relation-like set
bool [:([:{B},((succ c5) \ B):] \/ [:((succ c5) \ B),{c5}:]),([:{B},((succ c5) \ B):] \/ [:((succ c5) \ B),{c5}:]):] is non empty set
[:(Swap ((id (proj1 C)),B,c5)),(Swap ((id (proj1 C)),B,c5)):] +* (id ([:{B},((succ c5) \ B):] \/ [:((succ c5) \ B),{c5}:])) is Relation-like Function-like set
f is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 C
f is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 C
k is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 C
c9 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 C
O . (f,f) is set
[f,f] is V30() set
{f,f} is non empty finite set
{f} is non empty trivial finite 1 -element set
{{f,f},{f}} is non empty finite V53() set
O . [f,f] is set
O . (k,c9) is set
[k,c9] is V30() set
{k,c9} is non empty finite set
{k} is non empty trivial finite 1 -element set
{{k,c9},{k}} is non empty finite V53() set
O . [k,c9] is set
((proj1 C),(proj1 C),(id (proj1 C)),B,c5) is non empty Relation-like proj1 C -defined proj1 C -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 C),(proj1 C):]
[:((proj1 C),(proj1 C),(id (proj1 C)),B,c5),((proj1 C),(proj1 C),(id (proj1 C)),B,c5):] is non empty Relation-like [:(proj1 C),(proj1 C):] -defined [:(proj1 C),(proj1 C):] -valued Function-like total quasi_total Element of bool [:[:(proj1 C),(proj1 C):],[:(proj1 C),(proj1 C):]:]
[:[:(proj1 C),(proj1 C):],[:(proj1 C),(proj1 C):]:] is non empty Relation-like set
bool [:[:(proj1 C),(proj1 C):],[:(proj1 C),(proj1 C):]:] is non empty set
[k,c5] is V30() set
{k,c5} is non empty finite set
{{k,c5},{k}} is non empty finite V53() set
[k,B] is V30() set
{k,B} is non empty finite set
{{k,B},{k}} is non empty finite V53() set
[c5,c9] is V30() set
{c5,c9} is non empty finite set
{{c5,c9},{c5}} is non empty finite V53() set
[B,c9] is V30() set
{B,c9} is non empty finite set
{{B,c9},{B}} is non empty finite V53() set
[k,c5] is V30() set
{k,c5} is non empty finite set
{{k,c5},{k}} is non empty finite V53() set
[k,B] is V30() set
{k,B} is non empty finite set
{{k,B},{k}} is non empty finite V53() set
[c5,c9] is V30() set
{c5,c9} is non empty finite set
{{c5,c9},{c5}} is non empty finite V53() set
[B,c9] is V30() set
{B,c9} is non empty finite set
{{B,c9},{B}} is non empty finite V53() set
[k,c5] is V30() set
{k,c5} is non empty finite set
{{k,c5},{k}} is non empty finite V53() set
[k,B] is V30() set
{k,B} is non empty finite set
{{k,B},{k}} is non empty finite V53() set
[c5,c9] is V30() set
{c5,c9} is non empty finite set
{{c5,c9},{c5}} is non empty finite V53() set
[B,c9] is V30() set
{B,c9} is non empty finite set
{{B,c9},{B}} is non empty finite V53() set
[k,c5] is V30() set
{k,c5} is non empty finite set
{{k,c5},{k}} is non empty finite V53() set
[k,B] is V30() set
{k,B} is non empty finite set
{{k,B},{k}} is non empty finite V53() set
[c5,c9] is V30() set
{c5,c9} is non empty finite set
{{c5,c9},{c5}} is non empty finite V53() set
[B,c9] is V30() set
{B,c9} is non empty finite set
{{B,c9},{B}} is non empty finite V53() set
[f,c5] is V30() set
{f,c5} is non empty finite set
{{f,c5},{f}} is non empty finite V53() set
[k,c5] is V30() set
{k,c5} is non empty finite set
{{k,c5},{k}} is non empty finite V53() set
[k,B] is V30() set
{k,B} is non empty finite set
{{k,B},{k}} is non empty finite V53() set
[c5,c9] is V30() set
{c5,c9} is non empty finite set
{{c5,c9},{c5}} is non empty finite V53() set
[B,c9] is V30() set
{B,c9} is non empty finite set
{{B,c9},{B}} is non empty finite V53() set
[f,B] is V30() set
{f,B} is non empty finite set
{{f,B},{f}} is non empty finite V53() set
[k,c5] is V30() set
{k,c5} is non empty finite set
{{k,c5},{k}} is non empty finite V53() set
[k,B] is V30() set
{k,B} is non empty finite set
{{k,B},{k}} is non empty finite V53() set
[c5,c9] is V30() set
{c5,c9} is non empty finite set
{{c5,c9},{c5}} is non empty finite V53() set
[B,c9] is V30() set
{B,c9} is non empty finite set
{{B,c9},{B}} is non empty finite V53() set
[c5,f] is V30() set
{c5,f} is non empty finite set
{{c5,f},{c5}} is non empty finite V53() set
[k,c5] is V30() set
{k,c5} is non empty finite set
{{k,c5},{k}} is non empty finite V53() set
[k,B] is V30() set
{k,B} is non empty finite set
{{k,B},{k}} is non empty finite V53() set
[c5,c9] is V30() set
{c5,c9} is non empty finite set
{{c5,c9},{c5}} is non empty finite V53() set
[B,c9] is V30() set
{B,c9} is non empty finite set
{{B,c9},{B}} is non empty finite V53() set
[B,f] is V30() set
{B,f} is non empty finite set
{{B,f},{B}} is non empty finite V53() set
[k,c5] is V30() set
{k,c5} is non empty finite set
{{k,c5},{k}} is non empty finite V53() set
[k,B] is V30() set
{k,B} is non empty finite set
{{k,B},{k}} is non empty finite V53() set
[c5,c9] is V30() set
{c5,c9} is non empty finite set
{{c5,c9},{c5}} is non empty finite V53() set
[B,c9] is V30() set
{B,c9} is non empty finite set
{{B,c9},{B}} is non empty finite V53() set
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is non empty Relation-like the carrier of O -valued Function-like () set
proj1 A is non empty ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
(O,A,C,B) is Relation-like Function-like set
id (proj1 A) is non empty Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]
[:(proj1 A),(proj1 A):] is non empty Relation-like set
bool [:(proj1 A),(proj1 A):] is non empty set
Swap ((id (proj1 A)),C,B) is Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total onto set
[:(Swap ((id (proj1 A)),C,B)),(Swap ((id (proj1 A)),C,B)):] is Relation-like Function-like set
{C} is non empty trivial finite 1 -element set
succ B is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{B} is non empty trivial finite 1 -element set
B \/ {B} is non empty set
(succ B) \ C is ordinal-membered Element of bool (succ B)
bool (succ B) is non empty set
[:{C},((succ B) \ C):] is Relation-like set
[:((succ B) \ C),{B}:] is Relation-like set
[:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:] is Relation-like set
id ([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]) is Relation-like [:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:] -defined [:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]),([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]):]
[:([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]),([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]):] is Relation-like set
bool [:([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]),([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]):] is non empty set
[:(Swap ((id (proj1 A)),C,B)),(Swap ((id (proj1 A)),C,B)):] +* (id ([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:])) is Relation-like Function-like set
Swap (A,C,B) is Relation-like the carrier of O -valued Function-like () set
(O,(Swap (A,C,B))) is Relation-like asymmetric transitive set
proj1 (Swap (A,C,B)) is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (Swap (A,C,B)) : ( b1 in b2 & not (Swap (A,C,B)) /. b1 <= (Swap (A,C,B)) /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (Swap (A,C,B)) : ( b1 in b2 & (Swap (A,C,B)) /. b2 < (Swap (A,C,B)) /. b1 ) } is set
(O,A,C,B) | (O,(Swap (A,C,B))) is Relation-like Function-like set
c9 is set
proj1 ((O,A,C,B) | (O,(Swap (A,C,B)))) is set
((O,A,C,B) | (O,(Swap (A,C,B)))) . c9 is set
p is set
((O,A,C,B) | (O,(Swap (A,C,B)))) . p is set
q is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
y is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
[q,y] is V30() set
{q,y} is non empty finite set
{q} is non empty trivial finite 1 -element set
{{q,y},{q}} is non empty finite V53() set
(Swap (A,C,B)) /. y is Element of the carrier of O
(Swap (A,C,B)) /. q is Element of the carrier of O
y is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
b is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
[y,b] is V30() set
{y,b} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,b},{y}} is non empty finite V53() set
(Swap (A,C,B)) /. b is Element of the carrier of O
(Swap (A,C,B)) /. y is Element of the carrier of O
(O,A,C,B) . (q,y) is set
(O,A,C,B) . [q,y] is set
(O,A,C,B) . (y,b) is set
(O,A,C,B) . [y,b] is set
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like () set
C is set
B is set
(O,A,C,B) is Relation-like Function-like set
proj1 A is ordinal-membered set
id (proj1 A) is Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]
[:(proj1 A),(proj1 A):] is Relation-like set
bool [:(proj1 A),(proj1 A):] is non empty set
Swap ((id (proj1 A)),C,B) is Relation-like proj1 A -defined proj1 A -valued Function-like set
[:(Swap ((id (proj1 A)),C,B)),(Swap ((id (proj1 A)),C,B)):] is Relation-like Function-like set
{C} is non empty trivial finite 1 -element set
succ B is non empty set
{B} is non empty trivial finite 1 -element set
B \/ {B} is non empty set
(succ B) \ C is Element of bool (succ B)
bool (succ B) is non empty set
[:{C},((succ B) \ C):] is Relation-like set
[:((succ B) \ C),{B}:] is Relation-like set
[:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:] is Relation-like set
id ([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]) is Relation-like [:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:] -defined [:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]),([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]):]
[:([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]),([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]):] is Relation-like set
bool [:([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]),([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]):] is non empty set
[:(Swap ((id (proj1 A)),C,B)),(Swap ((id (proj1 A)),C,B)):] +* (id ([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:])) is Relation-like Function-like set
c5 is set
(O,A,C,B) .: c5 is set
proj2 (O,A,C,B) is set
proj2 [:(Swap ((id (proj1 A)),C,B)),(Swap ((id (proj1 A)),C,B)):] is set
proj2 (Swap ((id (proj1 A)),C,B)) is set
[:(proj2 (Swap ((id (proj1 A)),C,B))),(proj2 (Swap ((id (proj1 A)),C,B))):] is Relation-like set
proj2 (id ([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:])) is set
(proj2 [:(Swap ((id (proj1 A)),C,B)),(Swap ((id (proj1 A)),C,B)):]) \/ (proj2 (id ([:{C},((succ B) \ C):] \/ [:((succ B) \ C),{B}:]))) is set
O is set
A is set
[O,A] is V30() set
{O,A} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,A},{O}} is non empty finite V53() set
C is non empty reflexive transitive antisymmetric connected RelStr
the carrier of C is non empty set
B is Relation-like the carrier of C -valued Function-like () set
(C,B) is Relation-like asymmetric transitive set
proj1 B is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 B : ( b1 in b2 & not B /. b1 <= B /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 B : ( b1 in b2 & B /. b2 < B /. b1 ) } is set
(C,B,O,A) is Relation-like Function-like set
id (proj1 B) is Relation-like proj1 B -defined proj1 B -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 B),(proj1 B):]
[:(proj1 B),(proj1 B):] is Relation-like set
bool [:(proj1 B),(proj1 B):] is non empty set
Swap ((id (proj1 B)),O,A) is Relation-like proj1 B -defined proj1 B -valued Function-like set
[:(Swap ((id (proj1 B)),O,A)),(Swap ((id (proj1 B)),O,A)):] is Relation-like Function-like set
succ A is non empty set
{A} is non empty trivial finite 1 -element set
A \/ {A} is non empty set
(succ A) \ O is Element of bool (succ A)
bool (succ A) is non empty set
[:{O},((succ A) \ O):] is Relation-like set
[:((succ A) \ O),{A}:] is Relation-like set
[:{O},((succ A) \ O):] \/ [:((succ A) \ O),{A}:] is Relation-like set
id ([:{O},((succ A) \ O):] \/ [:((succ A) \ O),{A}:]) is Relation-like [:{O},((succ A) \ O):] \/ [:((succ A) \ O),{A}:] -defined [:{O},((succ A) \ O):] \/ [:((succ A) \ O),{A}:] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:([:{O},((succ A) \ O):] \/ [:((succ A) \ O),{A}:]),([:{O},((succ A) \ O):] \/ [:((succ A) \ O),{A}:]):]
[:([:{O},((succ A) \ O):] \/ [:((succ A) \ O),{A}:]),([:{O},((succ A) \ O):] \/ [:((succ A) \ O),{A}:]):] is Relation-like set
bool [:([:{O},((succ A) \ O):] \/ [:((succ A) \ O),{A}:]),([:{O},((succ A) \ O):] \/ [:((succ A) \ O),{A}:]):] is non empty set
[:(Swap ((id (proj1 B)),O,A)),(Swap ((id (proj1 B)),O,A)):] +* (id ([:{O},((succ A) \ O):] \/ [:((succ A) \ O),{A}:])) is Relation-like Function-like set
Swap (B,O,A) is Relation-like the carrier of C -valued Function-like () set
(C,(Swap (B,O,A))) is Relation-like asymmetric transitive set
proj1 (Swap (B,O,A)) is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (Swap (B,O,A)) : ( b1 in b2 & not (Swap (B,O,A)) /. b1 <= (Swap (B,O,A)) /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (Swap (B,O,A)) : ( b1 in b2 & (Swap (B,O,A)) /. b2 < (Swap (B,O,A)) /. b1 ) } is set
(C,B,O,A) .: (C,(Swap (B,O,A))) is Relation-like set
B /. A is Element of the carrier of C
B /. O is Element of the carrier of C
c5 is non empty Relation-like the carrier of C -valued Function-like () set
proj1 c5 is non empty ordinal-membered set
f is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
k is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
(C,c5,f,k) is Relation-like Function-like set
id (proj1 c5) is non empty Relation-like proj1 c5 -defined proj1 c5 -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 c5),(proj1 c5):]
[:(proj1 c5),(proj1 c5):] is non empty Relation-like set
bool [:(proj1 c5),(proj1 c5):] is non empty set
Swap ((id (proj1 c5)),f,k) is Relation-like proj1 c5 -defined proj1 c5 -valued Function-like one-to-one total onto set
[:(Swap ((id (proj1 c5)),f,k)),(Swap ((id (proj1 c5)),f,k)):] is Relation-like Function-like set
{f} is non empty trivial finite 1 -element set
succ k is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{k} is non empty trivial finite 1 -element set
k \/ {k} is non empty set
(succ k) \ f is ordinal-membered Element of bool (succ k)
bool (succ k) is non empty set
[:{f},((succ k) \ f):] is Relation-like set
[:((succ k) \ f),{k}:] is Relation-like set
[:{f},((succ k) \ f):] \/ [:((succ k) \ f),{k}:] is Relation-like set
id ([:{f},((succ k) \ f):] \/ [:((succ k) \ f),{k}:]) is Relation-like [:{f},((succ k) \ f):] \/ [:((succ k) \ f),{k}:] -defined [:{f},((succ k) \ f):] \/ [:((succ k) \ f),{k}:] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:([:{f},((succ k) \ f):] \/ [:((succ k) \ f),{k}:]),([:{f},((succ k) \ f):] \/ [:((succ k) \ f),{k}:]):]
[:([:{f},((succ k) \ f):] \/ [:((succ k) \ f),{k}:]),([:{f},((succ k) \ f):] \/ [:((succ k) \ f),{k}:]):] is Relation-like set
bool [:([:{f},((succ k) \ f):] \/ [:((succ k) \ f),{k}:]),([:{f},((succ k) \ f):] \/ [:((succ k) \ f),{k}:]):] is non empty set
[:(Swap ((id (proj1 c5)),f,k)),(Swap ((id (proj1 c5)),f,k)):] +* (id ([:{f},((succ k) \ f):] \/ [:((succ k) \ f),{k}:])) is Relation-like Function-like set
Swap (c5,f,k) is Relation-like the carrier of C -valued Function-like () set
proj1 (Swap (c5,f,k)) is ordinal-membered set
b is set
Fy is set
[b,Fy] is V30() set
{b,Fy} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,Fy},{b}} is non empty finite V53() set
proj1 (C,B,O,A) is set
c16 is set
b is set
[c16,b] is V30() set
{c16,b} is non empty finite set
{c16} is non empty trivial finite 1 -element set
{{c16,b},{c16}} is non empty finite V53() set
(C,B,O,A) . (c16,b) is set
(C,B,O,A) . [c16,b] is set
a is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
b is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
[a,b] is V30() set
{a,b} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,b},{a}} is non empty finite V53() set
a is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
b is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
[a,k] is V30() set
{a,k} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,k},{a}} is non empty finite V53() set
a is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
b is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
[a,f] is V30() set
{a,f} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,f},{a}} is non empty finite V53() set
a is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
b is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
[a,b] is V30() set
{a,b} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,b},{a}} is non empty finite V53() set
a is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
b is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
a is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
b is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
[k,b] is V30() set
{k,b} is non empty finite set
{{k,b},{k}} is non empty finite V53() set
a is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
b is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
[f,b] is V30() set
{f,b} is non empty finite set
{{f,b},{f}} is non empty finite V53() set
a is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
b is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
[a,b] is V30() set
{a,b} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,b},{a}} is non empty finite V53() set
a is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
b is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
proj1 (C,B,O,A) is set
b is set
Fy is set
[b,Fy] is V30() set
{b,Fy} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,Fy},{b}} is non empty finite V53() set
(C,B,O,A) . (b,Fy) is set
(C,B,O,A) . [b,Fy] is set
(C,B,O,A) . (f,k) is set
[f,k] is V30() set
{f,k} is non empty finite set
{{f,k},{f}} is non empty finite V53() set
(C,B,O,A) . [f,k] is set
c16 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
b is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
O is Relation-like Function-like finite set
A is set
C is set
Swap (O,A,C) is Relation-like Function-like set
proj1 (Swap (O,A,C)) is set
proj1 O is finite set
O is set
A is set
[O,A] is V30() set
{O,A} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,A},{O}} is non empty finite V53() set
C is non empty reflexive transitive antisymmetric connected RelStr
the carrier of C is non empty set
B is Relation-like the carrier of C -valued Function-like () set
(C,B) is Relation-like asymmetric transitive set
proj1 B is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 B : ( b1 in b2 & not B /. b1 <= B /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 B : ( b1 in b2 & B /. b2 < B /. b1 ) } is set
Swap (B,O,A) is Relation-like the carrier of C -valued Function-like () set
(C,(Swap (B,O,A))) is Relation-like asymmetric transitive set
proj1 (Swap (B,O,A)) is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (Swap (B,O,A)) : ( b1 in b2 & not (Swap (B,O,A)) /. b1 <= (Swap (B,O,A)) /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (Swap (B,O,A)) : ( b1 in b2 & (Swap (B,O,A)) /. b2 < (Swap (B,O,A)) /. b1 ) } is set
len (C,(Swap (B,O,A))) is epsilon-transitive epsilon-connected ordinal cardinal ordinal-membered set
len (C,B) is epsilon-transitive epsilon-connected ordinal cardinal ordinal-membered set
(C,B,O,A) is Relation-like Function-like set
id (proj1 B) is Relation-like proj1 B -defined proj1 B -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 B),(proj1 B):]
[:(proj1 B),(proj1 B):] is Relation-like set
bool [:(proj1 B),(proj1 B):] is non empty set
Swap ((id (proj1 B)),O,A) is Relation-like proj1 B -defined proj1 B -valued Function-like set
[:(Swap ((id (proj1 B)),O,A)),(Swap ((id (proj1 B)),O,A)):] is Relation-like Function-like set
succ A is non empty set
{A} is non empty trivial finite 1 -element set
A \/ {A} is non empty set
(succ A) \ O is Element of bool (succ A)
bool (succ A) is non empty set
[:{O},((succ A) \ O):] is Relation-like set
[:((succ A) \ O),{A}:] is Relation-like set
[:{O},((succ A) \ O):] \/ [:((succ A) \ O),{A}:] is Relation-like set
id ([:{O},((succ A) \ O):] \/ [:((succ A) \ O),{A}:]) is Relation-like [:{O},((succ A) \ O):] \/ [:((succ A) \ O),{A}:] -defined [:{O},((succ A) \ O):] \/ [:((succ A) \ O),{A}:] -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:([:{O},((succ A) \ O):] \/ [:((succ A) \ O),{A}:]),([:{O},((succ A) \ O):] \/ [:((succ A) \ O),{A}:]):]
[:([:{O},((succ A) \ O):] \/ [:((succ A) \ O),{A}:]),([:{O},((succ A) \ O):] \/ [:((succ A) \ O),{A}:]):] is Relation-like set
bool [:([:{O},((succ A) \ O):] \/ [:((succ A) \ O),{A}:]),([:{O},((succ A) \ O):] \/ [:((succ A) \ O),{A}:]):] is non empty set
[:(Swap ((id (proj1 B)),O,A)),(Swap ((id (proj1 B)),O,A)):] +* (id ([:{O},((succ A) \ O):] \/ [:((succ A) \ O),{A}:])) is Relation-like Function-like set
(C,B,O,A) .: (C,(Swap (B,O,A))) is Relation-like set
f is finite set
card f is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
c9 is finite set
card c9 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
(C,B,O,A) | (C,(Swap (B,O,A))) is Relation-like Function-like set
p is Relation-like Function-like set
proj1 p is set
proj2 p is set
proj1 (C,B,O,A) is set
O is set
A is set
[O,A] is V30() set
{O,A} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,A},{O}} is non empty finite V53() set
C is non empty reflexive transitive antisymmetric connected RelStr
the carrier of C is non empty set
B is Relation-like the carrier of C -valued Function-like finite () set
(C,B) is Relation-like finite asymmetric transitive set
proj1 B is finite ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 B : ( b1 in b2 & not B /. b1 <= B /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 B : ( b1 in b2 & B /. b2 < B /. b1 ) } is set
card (C,B) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
Swap (B,O,A) is Relation-like the carrier of C -valued Function-like finite () set
(C,(Swap (B,O,A))) is Relation-like finite asymmetric transitive set
proj1 (Swap (B,O,A)) is finite ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (Swap (B,O,A)) : ( b1 in b2 & not (Swap (B,O,A)) /. b1 <= (Swap (B,O,A)) /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (Swap (B,O,A)) : ( b1 in b2 & (Swap (B,O,A)) /. b2 < (Swap (B,O,A)) /. b1 ) } is set
card (C,(Swap (B,O,A))) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like () set
<%A%> is non empty trivial T-Sequence-like Relation-like NAT -defined Function-like constant finite 1 -element V67() V206() () ( {} ) set
C is non empty T-Sequence-like Relation-like Function-like () ( {} ) set
(C) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C . (C) is set
proj1 C is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C . B is set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
succ B is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{B} is non empty trivial finite 1 -element set
B \/ {B} is non empty set
C . B is set
C . (succ B) is set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is non empty reflexive transitive antisymmetric connected RelStr
the carrier of A is non empty set
C is Relation-like the carrier of A -valued Function-like () set
[O,C] is V30() set
{O,C} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,C},{O}} is non empty finite V53() set
{[O,C]} is non empty trivial Relation-like Function-like constant finite 1 -element () (O) ( succ O) set
succ O is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
O \/ {O} is non empty set
B is non empty Relation-like Function-like () (O) set
proj1 B is non empty ordinal-membered set
(B) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B . (B) is set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B . c5 is set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
succ c5 is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{c5} is non empty trivial finite 1 -element set
c5 \/ {c5} is non empty set
B . c5 is set
B . (succ c5) is set
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like () set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
[C,A] is V30() set
{C,A} is non empty finite set
{C} is non empty trivial finite 1 -element set
{{C,A},{C}} is non empty finite V53() set
{[C,A]} is non empty trivial Relation-like Function-like constant finite 1 -element () (C) ( succ C) set
succ C is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
C \/ {C} is non empty set
B is non empty Relation-like Function-like finite () (C) set
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like () set
C is non empty Relation-like Function-like () (O,A)
B is set
C . B is set
proj1 C is non empty ordinal-membered set
proj1 C is non empty ordinal-membered set
proj1 C is non empty ordinal-membered set
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like () set
C is non empty Relation-like Function-like () (O,A)
B is set
C . B is Relation-like Function-like () set
proj1 C is non empty ordinal-membered set
proj2 (C . B) is set
proj1 C is non empty ordinal-membered set
proj1 C is non empty ordinal-membered set
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like () set
C is non empty Relation-like Function-like () (O,A)
(C) is set
proj1 C is non empty ordinal-membered set
union (proj1 C) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C . (union (proj1 C)) is Relation-like the carrier of O -valued Function-like () set
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like () set
C is non empty Relation-like Function-like () (O,A)
(C) is Relation-like Function-like () set
proj1 C is non empty ordinal-membered set
union (proj1 C) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C . (union (proj1 C)) is Relation-like the carrier of O -valued Function-like () set
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like () set
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like () set
C is non empty T-Sequence-like Relation-like Function-like () ( {} ) (O,A)
(C) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C . (C) is Relation-like the carrier of O -valued Function-like () set
B is Relation-like the carrier of O -valued Function-like finite () set
C . {} is Relation-like the carrier of O -valued Function-like () set
(O,(C . {})) is Relation-like asymmetric transitive set
proj1 (C . {}) is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (C . {}) : ( b1 in b2 & not (C . {}) /. b1 <= (C . {}) /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (C . {}) : ( b1 in b2 & (C . {}) /. b2 < (C . {}) /. b1 ) } is set
len (O,(C . {})) is epsilon-transitive epsilon-connected ordinal cardinal ordinal-membered set
proj1 C is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
succ c5 is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{c5} is non empty trivial finite 1 -element set
c5 \/ {c5} is non empty set
C . c5 is Relation-like the carrier of O -valued Function-like () set
(O,(C . c5)) is Relation-like asymmetric transitive set
proj1 (C . c5) is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (C . c5) : ( b1 in b2 & not (C . c5) /. b1 <= (C . c5) /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (C . c5) : ( b1 in b2 & (C . c5) /. b2 < (C . c5) /. b1 ) } is set
len (O,(C . c5)) is epsilon-transitive epsilon-connected ordinal cardinal ordinal-membered set
C . (succ c5) is Relation-like the carrier of O -valued Function-like () set
(O,(C . (succ c5))) is Relation-like asymmetric transitive set
proj1 (C . (succ c5)) is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (C . (succ c5)) : ( b1 in b2 & not (C . (succ c5)) /. b1 <= (C . (succ c5)) /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (C . (succ c5)) : ( b1 in b2 & (C . (succ c5)) /. b2 < (C . (succ c5)) /. b1 ) } is set
len (O,(C . (succ c5))) is epsilon-transitive epsilon-connected ordinal cardinal ordinal-membered set
k is set
f is set
[k,f] is V30() set
{k,f} is non empty finite set
{k} is non empty trivial finite 1 -element set
{{k,f},{k}} is non empty finite V53() set
f is Relation-like the carrier of O -valued Function-like () set
(O,f) is Relation-like asymmetric transitive set
proj1 f is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 f : ( b1 in b2 & not f /. b1 <= f /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 f : ( b1 in b2 & f /. b2 < f /. b1 ) } is set
Swap (f,k,f) is Relation-like the carrier of O -valued Function-like () set
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like () set
C is non empty T-Sequence-like Relation-like Function-like () ( {} ) (O,A)
proj1 C is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
B is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
union B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
f + 1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT
succ f is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
{f} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set
f \/ {f} is non empty finite set
C . (union B) is Relation-like the carrier of O -valued Function-like () set
(O,(C . (union B))) is Relation-like asymmetric transitive set
proj1 (C . (union B)) is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (C . (union B)) : ( b1 in b2 & not (C . (union B)) /. b1 <= (C . (union B)) /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (C . (union B)) : ( b1 in b2 & (C . (union B)) /. b2 < (C . (union B)) /. b1 ) } is set
(C) is Relation-like the carrier of O -valued Function-like () set
union (proj1 C) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C . (union (proj1 C)) is Relation-like the carrier of O -valued Function-like () set
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like () set
C is non empty Relation-like Function-like finite () (O,A)
(C) is Relation-like the carrier of O -valued Function-like () set
proj1 C is non empty finite ordinal-membered set
union (proj1 C) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C . (union (proj1 C)) is Relation-like the carrier of O -valued Function-like () set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B \ c5 is ordinal-membered Element of bool B
bool B is non empty set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
c5 +^ f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 +^ {} is epsilon-transitive epsilon-connected ordinal ordinal-membered set
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
k + 1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT
succ k is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
{k} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set
k \/ {k} is non empty finite set
c5 +^ (succ k) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 +^ k is epsilon-transitive epsilon-connected ordinal ordinal-membered set
succ (c5 +^ k) is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{(c5 +^ k)} is non empty trivial finite 1 -element set
(c5 +^ k) \/ {(c5 +^ k)} is non empty set
union B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
union (B \ c5) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(C) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C . (C) is Relation-like the carrier of O -valued Function-like () set
C . c5 is Relation-like the carrier of O -valued Function-like () set
C . (c5 +^ {}) is Relation-like the carrier of O -valued Function-like () set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
c5 +^ f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C . (c5 +^ f) is Relation-like the carrier of O -valued Function-like () set
f + 1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT
c5 +^ (f + 1) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C . (c5 +^ (f + 1)) is Relation-like the carrier of O -valued Function-like () set
succ f is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
{f} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set
f \/ {f} is non empty finite set
succ (c5 +^ f) is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{(c5 +^ f)} is non empty trivial finite 1 -element set
(c5 +^ f) \/ {(c5 +^ f)} is non empty set
p is set
q is set
[p,q] is V30() set
{p,q} is non empty finite set
{p} is non empty trivial finite 1 -element set
{{p,q},{p}} is non empty finite V53() set
c9 is Relation-like the carrier of O -valued Function-like () set
(O,c9) is Relation-like asymmetric transitive set
proj1 c9 is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c9 : ( b1 in b2 & not c9 /. b1 <= c9 /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c9 : ( b1 in b2 & c9 /. b2 < c9 /. b1 ) } is set
Swap (c9,p,q) is Relation-like the carrier of O -valued Function-like () set
C . (c5 +^ k) is Relation-like the carrier of O -valued Function-like () set
f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C . f is Relation-like the carrier of O -valued Function-like () set
f -^ c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 +^ (f -^ c5) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
c5 +^ c9 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C . (c5 +^ c9) is Relation-like the carrier of O -valued Function-like () set
O is set
A is T-Sequence-like Relation-like NAT -defined O -valued Function-like finite V67() () ( {} ) set
(A) is set
proj1 A is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
union (proj1 A) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A . (union (proj1 A)) is set
dom A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered Element of bool NAT
C is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
C + 1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT
succ C is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
{C} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set
C \/ {C} is non empty finite set
union (dom A) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is set
<%O%> is non empty trivial T-Sequence-like Relation-like NAT -defined Function-like constant finite 1 -element V67() () ( {} ) set
(<%O%>) is set
proj1 <%O%> is non empty trivial epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal 1 -element ordinal-membered set
union (proj1 <%O%>) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
<%O%> . (union (proj1 <%O%>)) is set
dom <%O%> is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal 1 -element ordinal-membered Element of bool NAT
succ {} is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
{} \/ {{}} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty finite V53() set
union (dom <%O%>) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is set
<%O%> is non empty trivial T-Sequence-like Relation-like NAT -defined Function-like constant finite 1 -element V67() () ( {} ) set
A is T-Sequence-like Relation-like NAT -defined Function-like finite V67() () ( {} ) set
A ^ <%O%> is non empty T-Sequence-like Relation-like NAT -defined Function-like finite V67() () ( {} ) set
((A ^ <%O%>)) is set
proj1 (A ^ <%O%>) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
union (proj1 (A ^ <%O%>)) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(A ^ <%O%>) . (union (proj1 (A ^ <%O%>))) is set
dom <%O%> is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal 1 -element ordinal-membered Element of bool NAT
dom (A ^ <%O%>) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered Element of bool NAT
dom A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered Element of bool NAT
(dom A) +^ 1 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
succ (dom A) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
{(dom A)} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set
(dom A) \/ {(dom A)} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty finite set
union (dom (A ^ <%O%>)) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
len A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
proj1 A is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
O is set
O ^omega is non empty functional set
A is T-Sequence-like Relation-like NAT -defined Function-like finite V67() () ( {} ) Element of O ^omega
F3() is set
F2() is non empty set
F1(F3()) is set
F2() ^omega is non empty functional set
A is Element of F2()
<%A%> is non empty trivial T-Sequence-like Relation-like NAT -defined F2() -valued Function-like constant finite 1 -element V67() () ( {} ) set
B is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
c5 is T-Sequence-like Relation-like NAT -defined F2() -valued Function-like finite V67() () ( {} ) Element of F2() ^omega
(c5) is set
proj1 c5 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
union (proj1 c5) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 . (union (proj1 c5)) is set
F1((c5)) is set
f is T-Sequence-like Relation-like NAT -defined F2() -valued Function-like finite V67() () ( {} ) Element of F2() ^omega
f is Element of F2()
F1(f) is set
<%f%> is non empty trivial T-Sequence-like Relation-like NAT -defined F2() -valued Function-like constant finite 1 -element V67() () ( {} ) set
c5 ^ <%f%> is non empty T-Sequence-like Relation-like NAT -defined F2() -valued Function-like finite V67() () ( {} ) set
k is T-Sequence-like Relation-like NAT -defined F2() -valued Function-like finite V67() () ( {} ) Element of F2() ^omega
[:NAT,(F2() ^omega):] is non empty non trivial Relation-like non finite set
bool [:NAT,(F2() ^omega):] is non empty non trivial non finite set
C is T-Sequence-like Relation-like NAT -defined F2() -valued Function-like finite V67() () ( {} ) Element of F2() ^omega
B is non empty Relation-like NAT -defined F2() ^omega -valued Function-like total quasi_total Element of bool [:NAT,(F2() ^omega):]
B . {} is T-Sequence-like Relation-like NAT -defined F2() -valued Function-like finite V67() () ( {} ) Element of F2() ^omega
c5 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
B . c5 is T-Sequence-like Relation-like NAT -defined F2() -valued Function-like finite V67() () ( {} ) Element of F2() ^omega
c5 + 1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT
B . (c5 + 1) is T-Sequence-like Relation-like NAT -defined F2() -valued Function-like finite V67() () ( {} ) Element of F2() ^omega
((B . c5)) is set
proj1 (B . c5) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
union (proj1 (B . c5)) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(B . c5) . (union (proj1 (B . c5))) is set
F1(((B . c5))) is set
f is non empty T-Sequence-like Relation-like Function-like () ( {} ) set
k is Element of F2()
F1(k) is set
<%k%> is non empty trivial T-Sequence-like Relation-like NAT -defined F2() -valued Function-like constant finite 1 -element V67() () ( {} ) set
(B . c5) ^ <%k%> is non empty T-Sequence-like Relation-like NAT -defined F2() -valued Function-like finite V67() () ( {} ) set
k is set
<%k%> is non empty trivial T-Sequence-like Relation-like NAT -defined Function-like constant finite 1 -element V67() () ( {} ) set
f ^ <%k%> is non empty T-Sequence-like Relation-like Function-like () ( {} ) set
(B . {}) . {} is set
proj1 (B . {}) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
succ c5 is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{c5} is non empty trivial finite 1 -element set
c5 \/ {c5} is non empty set
(B . {}) . c5 is set
(B . {}) . (succ c5) is set
dom (B . {}) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered Element of bool NAT
c5 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
B . c5 is T-Sequence-like Relation-like NAT -defined F2() -valued Function-like finite V67() () ( {} ) Element of F2() ^omega
(B . c5) . {} is set
proj1 (B . c5) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
c5 + 1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT
B . (c5 + 1) is T-Sequence-like Relation-like NAT -defined F2() -valued Function-like finite V67() () ( {} ) Element of F2() ^omega
(B . (c5 + 1)) . {} is set
proj1 (B . (c5 + 1)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
((B . c5)) is set
union (proj1 (B . c5)) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(B . c5) . (union (proj1 (B . c5))) is set
F1(((B . c5))) is set
f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
succ f is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{f} is non empty trivial finite 1 -element set
f \/ {f} is non empty set
(B . (c5 + 1)) . f is set
(B . (c5 + 1)) . (succ f) is set
k is Element of F2()
F1(k) is set
<%k%> is non empty trivial T-Sequence-like Relation-like NAT -defined F2() -valued Function-like constant finite 1 -element V67() () ( {} ) set
(B . c5) ^ <%k%> is non empty T-Sequence-like Relation-like NAT -defined F2() -valued Function-like finite V67() () ( {} ) set
f is non empty T-Sequence-like Relation-like NAT -defined F2() -valued Function-like finite V67() () ( {} ) set
(f) is set
proj1 f is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
union (proj1 f) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f . (union (proj1 f)) is set
F1((f)) is set
f is Element of F2()
F1(f) is set
<%f%> is non empty trivial T-Sequence-like Relation-like NAT -defined F2() -valued Function-like constant finite 1 -element V67() () ( {} ) set
f ^ <%f%> is non empty T-Sequence-like Relation-like NAT -defined F2() -valued Function-like finite V67() () ( {} ) set
dom f is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered Element of bool NAT
c9 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
succ c9 is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{c9} is non empty trivial finite 1 -element set
c9 \/ {c9} is non empty set
(B . (c5 + 1)) . c9 is set
(B . (c5 + 1)) . (succ c9) is set
dom (B . (c5 + 1)) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered Element of bool NAT
k is T-Sequence-like Relation-like NAT -defined F2() -valued Function-like finite V67() () ( {} ) set
dom k is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered Element of bool NAT
k . c9 is set
k . (succ c9) is set
dom <%f%> is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal 1 -element ordinal-membered Element of bool NAT
(dom f) +^ 1 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
succ (dom f) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
{(dom f)} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set
(dom f) \/ {(dom f)} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty finite set
q is Element of F2()
y is Element of F2()
f . c9 is set
f . (succ c9) is set
y is Element of F2()
b is Element of F2()
union (dom f) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(succ c9) +^ {} is epsilon-transitive epsilon-connected ordinal ordinal-membered set
<%f%> . {} is set
(C) is set
proj1 C is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
union (proj1 C) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C . (union (proj1 C)) is set
((B . {})) is set
union (proj1 (B . {})) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(B . {}) . (union (proj1 (B . {}))) is set
F1(((B . {}))) is set
len F1(((B . {}))) is epsilon-transitive epsilon-connected ordinal cardinal ordinal-membered set
c5 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
c5 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
B . f is T-Sequence-like Relation-like NAT -defined F2() -valued Function-like finite V67() () ( {} ) Element of F2() ^omega
((B . f)) is set
proj1 (B . f) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
union (proj1 (B . f)) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(B . f) . (union (proj1 (B . f))) is set
F1(((B . f))) is set
len F1(((B . f))) is epsilon-transitive epsilon-connected ordinal cardinal ordinal-membered set
f + 1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT
B . (f + 1) is T-Sequence-like Relation-like NAT -defined F2() -valued Function-like finite V67() () ( {} ) Element of F2() ^omega
k is T-Sequence-like Relation-like NAT -defined F2() -valued Function-like finite V67() () ( {} ) Element of F2() ^omega
f is T-Sequence-like Relation-like NAT -defined F2() -valued Function-like finite V67() () ( {} ) Element of F2() ^omega
(k) is set
proj1 k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
union (proj1 k) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
k . (union (proj1 k)) is set
F1((k)) is set
c9 is Element of F2()
F1(c9) is set
<%c9%> is non empty trivial T-Sequence-like Relation-like NAT -defined F2() -valued Function-like constant finite 1 -element V67() () ( {} ) set
k ^ <%c9%> is non empty T-Sequence-like Relation-like NAT -defined F2() -valued Function-like finite V67() () ( {} ) set
c9 is Element of F2()
F1(c9) is set
<%c9%> is non empty trivial T-Sequence-like Relation-like NAT -defined F2() -valued Function-like constant finite 1 -element V67() () ( {} ) set
k ^ <%c9%> is non empty T-Sequence-like Relation-like NAT -defined F2() -valued Function-like finite V67() () ( {} ) set
(f) is set
proj1 f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
union (proj1 f) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f . (union (proj1 f)) is set
F1((f)) is set
len F1((f)) is epsilon-transitive epsilon-connected ordinal cardinal ordinal-membered set
p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
c5 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
B . c5 is T-Sequence-like Relation-like NAT -defined F2() -valued Function-like finite V67() () ( {} ) Element of F2() ^omega
((B . c5)) is set
proj1 (B . c5) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
union (proj1 (B . c5)) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(B . c5) . (union (proj1 (B . c5))) is set
F1(((B . c5))) is set
len F1(((B . c5))) is epsilon-transitive epsilon-connected ordinal cardinal ordinal-membered set
c5 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
B . c5 is T-Sequence-like Relation-like NAT -defined F2() -valued Function-like finite V67() () ( {} ) Element of F2() ^omega
((B . c5)) is set
proj1 (B . c5) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
union (proj1 (B . c5)) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(B . c5) . (union (proj1 (B . c5))) is set
F1(((B . c5))) is set
len F1(((B . c5))) is epsilon-transitive epsilon-connected ordinal cardinal ordinal-membered set
f is non empty T-Sequence-like Relation-like NAT -defined F2() -valued Function-like finite V67() () ( {} ) set
(f) is set
proj1 f is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
union (proj1 f) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f . (union (proj1 f)) is set
f . {} is set
dom f is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered Element of bool NAT
k is Element of F2()
F1(k) is set
f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
succ f is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{f} is non empty trivial finite 1 -element set
f \/ {f} is non empty set
f . f is set
f . (succ f) is set
O is Relation-like Function-like () set
proj1 O is ordinal-membered set
proj2 O is set
Funcs ((proj1 O),(proj2 O)) is functional set
A is Relation-like Function-like () (O)
proj1 A is ordinal-membered set
proj2 A is set
O is Relation-like Function-like complex-valued ext-real-valued real-valued () set
A is Relation-like Function-like () (O)
proj1 O is ordinal-membered set
[:(proj1 O),(proj1 O):] is Relation-like set
bool [:(proj1 O),(proj1 O):] is non empty set
C is Relation-like proj1 O -defined proj1 O -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 O),(proj1 O):]
C * O is Relation-like proj1 O -defined Function-like complex-valued ext-real-valued real-valued set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is non empty set
Funcs (O,A) is non empty functional FUNCTION_DOMAIN of O,A
C is Relation-like O -defined A -valued Function-like total quasi_total Element of Funcs (O,A)
dom C is Element of bool O
bool O is non empty set
O is set
A is complex-membered ext-real-membered real-membered non empty set
Funcs (O,A) is non empty functional FUNCTION_DOMAIN of O,A
C is Relation-like O -defined A -valued Function-like total quasi_total Element of Funcs (O,A)
O is set
A is Relation-like O -valued Function-like () set
C is Relation-like Function-like () (A)
proj1 A is ordinal-membered set
[:(proj1 A),(proj1 A):] is Relation-like set
bool [:(proj1 A),(proj1 A):] is non empty set
B is Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]
B * A is Relation-like proj1 A -defined O -valued Function-like set
A is set
bool A is non empty set
O is set
C is Element of bool A
Funcs (O,C) is functional set
B is Relation-like Function-like Element of Funcs (O,C)
proj2 B is set
proj2 B is set
O is set
A is set
[:O,A:] is Relation-like set
bool [:O,A:] is non empty set
C is Relation-like O -defined A -valued set
dom C is Element of bool O
bool O is non empty set
rng C is Element of bool A
bool A is non empty set
[:(dom C),(rng C):] is Relation-like set
O is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
A is set
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is non empty T-Sequence-like Relation-like NAT -defined the carrier of O -valued Function-like finite V67() () ( {} ) set
bool the carrier of O is non empty set
proj2 A is non empty finite set
dom A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered Element of bool NAT
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is non empty Element of bool the carrier of O
Funcs (B,C) is non empty functional FUNCTION_DOMAIN of B,C
(O,A) is Relation-like finite asymmetric transitive set
proj1 A is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & not A /. b1 <= A /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & A /. b2 < A /. b1 ) } is set
len (O,A) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
f is T-Sequence-like Relation-like B -defined C -valued Function-like total quasi_total () ( {} ) Element of Funcs (B,C)
(O,f) is set
len (O,f) is epsilon-transitive epsilon-connected ordinal cardinal ordinal-membered set
k is Relation-like the carrier of O -valued Function-like () set
(O,k) is Relation-like asymmetric transitive set
proj1 k is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 k : ( b1 in b2 & not k /. b1 <= k /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 k : ( b1 in b2 & k /. b2 < k /. b1 ) } is set
the Element of (O,k) is Element of (O,k)
dom f is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of bool B
bool B is non empty set
[:(dom f),(dom f):] is Relation-like set
bool [:(dom f),(dom f):] is non empty set
p is set
q is set
[p,q] is V30() set
{p,q} is non empty finite set
{p} is non empty trivial finite 1 -element set
{{p,q},{p}} is non empty finite V53() set
Swap (f,p,q) is Relation-like B -defined C -valued Function-like () set
dom (Swap (f,p,q)) is ordinal-membered Element of bool B
proj2 (Swap (f,p,q)) is set
proj2 f is set
y is T-Sequence-like Relation-like B -defined C -valued Function-like total quasi_total () ( {} ) Element of Funcs (B,C)
(O,y) is set
len (O,y) is epsilon-transitive epsilon-connected ordinal cardinal ordinal-membered set
b is Relation-like the carrier of O -valued Function-like () set
(O,b) is Relation-like asymmetric transitive set
proj1 b is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 b : ( b1 in b2 & not b /. b1 <= b /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 b : ( b1 in b2 & b /. b2 < b /. b1 ) } is set
len (O,b) is epsilon-transitive epsilon-connected ordinal cardinal ordinal-membered set
len (O,k) is epsilon-transitive epsilon-connected ordinal cardinal ordinal-membered set
k is T-Sequence-like Relation-like B -defined C -valued Function-like total quasi_total () ( {} ) Element of Funcs (B,C)
f is non empty T-Sequence-like Relation-like NAT -defined Function-like finite V67() () ( {} ) set
(f) is set
proj1 f is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
union (proj1 f) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f . (union (proj1 f)) is set
(O,k) is set
len (O,k) is epsilon-transitive epsilon-connected ordinal cardinal ordinal-membered set
f . {} is set
dom f is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered Element of bool NAT
(f) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f . (f) is set
f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f . f is set
c9 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
succ c9 is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{c9} is non empty trivial finite 1 -element set
c9 \/ {c9} is non empty set
c9 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
succ c9 is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{c9} is non empty trivial finite 1 -element set
c9 \/ {c9} is non empty set
f . c9 is set
p is T-Sequence-like Relation-like B -defined C -valued Function-like total quasi_total () ( {} ) Element of Funcs (B,C)
q is T-Sequence-like Relation-like B -defined C -valued Function-like total quasi_total () ( {} ) Element of Funcs (B,C)
y is V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of dom A
y is V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of dom A
[y,y] is V30() set
{y,y} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty finite V53() set
{y} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set
{{y,y},{y}} is non empty finite V53() set
(O,p) is set
Swap (p,y,y) is Relation-like B -defined C -valued Function-like () set
f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
succ f is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{f} is non empty trivial finite 1 -element set
f \/ {f} is non empty set
f . f is set
f . (succ f) is set
c9 is T-Sequence-like Relation-like B -defined C -valued Function-like total quasi_total () ( {} ) Element of Funcs (B,C)
p is T-Sequence-like Relation-like B -defined C -valued Function-like total quasi_total () ( {} ) Element of Funcs (B,C)
q is V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of dom A
y is V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of dom A
[q,y] is V30() set
{q,y} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty finite V53() set
{q} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set
{{q,y},{q}} is non empty finite V53() set
(O,c9) is set
Swap (c9,q,y) is Relation-like B -defined C -valued Function-like () set
f is non empty T-Sequence-like Relation-like Function-like () ( {} ) (O,A)
(f) is Relation-like the carrier of O -valued Function-like () set
proj1 f is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
union (proj1 f) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f . (union (proj1 f)) is Relation-like the carrier of O -valued Function-like () set
(O,(f)) is Relation-like asymmetric transitive set
proj1 (f) is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (f) : ( b1 in b2 & not (f) /. b1 <= (f) /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 (f) : ( b1 in b2 & (f) /. b2 < (f) /. b1 ) } is set
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is non empty T-Sequence-like Relation-like NAT -defined the carrier of O -valued Function-like finite V67() () ( {} ) set
C is non empty T-Sequence-like Relation-like Function-like () ( {} ) (O,A)
(C) is Relation-like the carrier of O -valued Function-like () set
proj1 C is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
union (proj1 C) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C . (union (proj1 C)) is Relation-like the carrier of O -valued Function-like () set
B is Relation-like the carrier of O -valued Function-like () (A)
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is T-Sequence-like Relation-like NAT -defined the carrier of O -valued Function-like finite V67() () ( {} ) set