:: MMLQUERY semantic presentation

REAL is set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set
bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
[:NAT,REAL:] is set
bool [:NAT,REAL:] is non empty set
bool (bool REAL) is non empty set
{} is set
the empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V37() cardinal {} -element FinSequence-membered ext-real non positive non negative V67() set is empty functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V37() cardinal {} -element FinSequence-membered ext-real non positive non negative V67() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
dom {} is set
rng {} is set
0 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
X is Relation-like set
A is Relation-like set
c1 is set
Im (X,c1) is set
{c1} is non empty trivial finite 1 -element set
X .: {c1} is set
Im (A,c1) is set
A .: {c1} is set
c2 is set
z is set
[z,c2] is set
{z,c2} is finite set
{z} is non empty trivial finite 1 -element set
{{z,c2},{z}} is finite V37() set
c1 is set
c2 is set
[c1,c2] is set
{c1,c2} is finite set
{c1} is non empty trivial finite 1 -element set
{{c1,c2},{c1}} is finite V37() set
Im (X,c1) is set
X .: {c1} is set
Im (A,c1) is set
A .: {c1} is set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
c1 is Element of X
Im (A,c1) is set
{c1} is non empty trivial finite 1 -element set
A .: {c1} is set
bool X is non empty set
A .: {c1} is Element of bool X
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,A) is Element of bool X
bool X is non empty set
{A} is non empty trivial finite 1 -element set
c1 .: {A} is set
c2 is Element of X
[A,c2] is set
{A,c2} is finite set
{{A,c2},{A}} is finite V37() set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
bool X is non empty set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
bool X is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
c1 is Element of bool X
A .: c1 is set
A .: c1 is Element of bool X
{ (X,A,b₁) where b₁ is Element of X : b₁ in c1 } is set
union { (X,A,b₁) where b₁ is Element of X : b₁ in c1 } is set
c2 is set
z is set
x is Element of X
(X,A,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
A .: {x} is set
[x,c2] is set
{x,c2} is finite set
{{x,c2},{x}} is finite V37() set
c2 is set
z is set
[z,c2] is set
{z,c2} is finite set
{z} is non empty trivial finite 1 -element set
{{z,c2},{z}} is finite V37() set
x is Element of X
(X,A,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
A .: {x} is set
c2 is Element of bool X
z is Element of bool X
meet { (X,A,b₁) where b₁ is Element of X : b₁ in c1 } is set
c2 is set
z is set
x is Element of X
(X,A,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
A .: {x} is set
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,A) & b₁ in c1 ) } is set
c2 is set
z is Element of X
x is Element of X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
{ b₁ where b₁ is Element of X : ( card (X,A,b₁) = card (X,c2,b₁) & b₁ in c1 ) } is set
z is set
x is Element of X
(X,A,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
A .: {x} is set
card (X,A,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,c2,x) is Element of bool X
c2 .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of X : ( card (X,A,b₁) c= card (X,c2,b₁) & b₁ in c1 ) } is set
z is set
x is Element of X
(X,A,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
A .: {x} is set
card (X,A,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,c2,x) is Element of bool X
c2 .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of X : ( card (X,c2,b₁) c= card (X,A,b₁) & b₁ in c1 ) } is set
z is set
x is Element of X
(X,c2,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c2 .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,A,x) is Element of bool X
A .: {x} is set
card (X,A,x) is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of X : ( card (X,A,b₁) in card (X,c2,b₁) & b₁ in c1 ) } is set
z is set
x is Element of X
(X,A,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
A .: {x} is set
card (X,A,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,c2,x) is Element of bool X
c2 .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of X : ( card (X,c2,b₁) in card (X,A,b₁) & b₁ in c1 ) } is set
z is set
x is Element of X
(X,c2,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c2 .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,A,x) is Element of bool X
A .: {x} is set
card (X,A,x) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
A is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,c1,b₁) = c2 & b₁ in A ) } is set
z is set
x is Element of X
(X,c1,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c1 .: {x} is set
card (X,c1,x) is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of X : ( card (X,c1,b₁) c= c2 & b₁ in A ) } is set
z is set
x is Element of X
(X,c1,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c1 .: {x} is set
card (X,c1,x) is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of X : ( c2 c= card (X,c1,b₁) & b₁ in A ) } is set
z is set
x is Element of X
(X,c1,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c1 .: {x} is set
card (X,c1,x) is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of X : ( card (X,c1,b₁) in c2 & b₁ in A ) } is set
z is set
x is Element of X
(X,c1,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c1 .: {x} is set
card (X,c1,x) is epsilon-transitive epsilon-connected ordinal cardinal set
{ b₁ where b₁ is Element of X : ( c2 in card (X,c1,b₁) & b₁ in A ) } is set
z is set
x is Element of X
(X,c1,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c1 .: {x} is set
card (X,c1,x) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c2,A) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,c2) & b₁ in A ) } is set
(X,c2,c1) is Element of bool X
{c1} is non empty trivial finite 1 -element set
c2 .: {c1} is set
z is Element of X
x is Element of X
the Element of (X,c2,c1) is Element of (X,c2,c1)
x is Element of X
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,A) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,c1) & b₁ in A ) } is set
c2 is set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
dom c1 is Element of bool X
(X,c1,A) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,c1) & b₁ in A ) } is set
c2 is set
z is Element of X
(X,c1,z) is Element of bool X
{z} is non empty trivial finite 1 -element set
c1 .: {z} is set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c2,c1) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,c2) & b₁ in c1 ) } is set
z is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,A,c2,z) is Element of bool X
{ b₁ where b₁ is Element of X : ( z c= card (X,c2,b₁) & b₁ in A ) } is set
x is set
s is Element of X
(X,c2,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
c2 .: {s} is set
card (X,c2,s) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A,c1,1) is Element of bool X
{ b₁ where b₁ is Element of X : ( 1 c= card (X,c1,b₁) & b₁ in A ) } is set
(X,c1,A) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,c1) & b₁ in A ) } is set
c2 is set
z is Element of X
(X,c1,z) is Element of bool X
{z} is non empty trivial finite 1 -element set
c1 .: {z} is set
succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
card (X,c1,z) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c2,c1) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,c2) & b₁ in c1 ) } is set
z is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,A,c2,z) is Element of bool X
{ b₁ where b₁ is Element of X : ( z in card (X,c2,b₁) & b₁ in A ) } is set
x is set
s is Element of X
(X,c2,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
c2 .: {s} is set
card (X,c2,s) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A,c1,0) is Element of bool X
{ b₁ where b₁ is Element of X : ( 0 in card (X,c1,b₁) & b₁ in A ) } is set
(X,c1,A) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,c1) & b₁ in A ) } is set
c2 is set
z is Element of X
(X,c1,z) is Element of bool X
{z} is non empty trivial finite 1 -element set
c1 .: {z} is set
card (X,c1,z) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c2,c1) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,c2) & b₁ in c1 ) } is set
z is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,A,c2,z) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,c2,b₁) = z & b₁ in A ) } is set
x is set
s is Element of X
(X,c2,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
c2 .: {s} is set
card (X,c2,s) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
c2 + 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
(X,A,c1,(c2 + 1)) is Element of bool X
{ b₁ where b₁ is Element of X : ( c2 + 1 c= card (X,c1,b₁) & b₁ in A ) } is set
(X,A,c1,c2) is Element of bool X
{ b₁ where b₁ is Element of X : ( c2 in card (X,c1,b₁) & b₁ in A ) } is set
z is set
x is Element of X
(X,c1,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c1 .: {x} is set
card (X,c1,x) is epsilon-transitive epsilon-connected ordinal cardinal set
succ c2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
z is set
x is Element of X
(X,c1,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c1 .: {x} is set
card (X,c1,x) is epsilon-transitive epsilon-connected ordinal cardinal set
succ c2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,A,c1,c2) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,c1,b₁) c= c2 & b₁ in A ) } is set
c2 + 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() Element of NAT
(X,A,c1,(c2 + 1)) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,c1,b₁) in c2 + 1 & b₁ in A ) } is set
z is set
x is Element of X
(X,c1,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c1 .: {x} is set
card (X,c1,x) is epsilon-transitive epsilon-connected ordinal cardinal set
succ c2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
z is set
x is Element of X
(X,c1,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c1 .: {x} is set
card (X,c1,x) is epsilon-transitive epsilon-connected ordinal cardinal set
succ c2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Relation-like X -defined X -valued Element of bool [:X,X:]
x is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,c1,z,x) is Element of bool X
{ b₁ where b₁ is Element of X : ( x c= card (X,z,b₁) & b₁ in c1 ) } is set
s is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,A,c2,s) is Element of bool X
{ b₁ where b₁ is Element of X : ( s c= card (X,c2,b₁) & b₁ in A ) } is set
s is set
x is Element of X
(X,c2,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c2 .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,z,x) is Element of bool X
z .: {x} is set
card (X,z,x) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Relation-like X -defined X -valued Element of bool [:X,X:]
x is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,c1,z,x) is Element of bool X
{ b₁ where b₁ is Element of X : ( x in card (X,z,b₁) & b₁ in c1 ) } is set
s is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,A,c2,s) is Element of bool X
{ b₁ where b₁ is Element of X : ( s in card (X,c2,b₁) & b₁ in A ) } is set
s is set
x is Element of X
(X,c2,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c2 .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,z,x) is Element of bool X
z .: {x} is set
card (X,z,x) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Relation-like X -defined X -valued Element of bool [:X,X:]
x is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,A,z,x) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,z,b₁) c= x & b₁ in A ) } is set
s is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,c1,c2,s) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,c2,b₁) c= s & b₁ in c1 ) } is set
s is set
x is Element of X
(X,z,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
z .: {x} is set
card (X,z,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,c2,x) is Element of bool X
c2 .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Relation-like X -defined X -valued Element of bool [:X,X:]
x is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,A,z,x) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,z,b₁) in x & b₁ in A ) } is set
s is epsilon-transitive epsilon-connected ordinal natural finite cardinal ext-real V67() set
(X,c1,c2,s) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,c2,b₁) in s & b₁ in c1 ) } is set
s is set
x is Element of X
(X,z,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
z .: {x} is set
card (X,z,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,c2,x) is Element of bool X
c2 .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Relation-like X -defined X -valued Element of bool [:X,X:]
x is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,x,A,z) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,z,b₁) c= card (X,x,b₁) & b₁ in A ) } is set
s is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,s,c1,c2) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,c2,b₁) c= card (X,s,b₁) & b₁ in c1 ) } is set
s is set
x is Element of X
(X,z,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
z .: {x} is set
card (X,z,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,x,x) is Element of bool X
x .: {x} is set
card (X,x,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,c2,x) is Element of bool X
c2 .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,s,x) is Element of bool X
s .: {x} is set
card (X,s,x) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Relation-like X -defined X -valued Element of bool [:X,X:]
x is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,x,A,z) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,z,b₁) in card (X,x,b₁) & b₁ in A ) } is set
s is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,s,c1,c2) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,c2,b₁) in card (X,s,b₁) & b₁ in c1 ) } is set
s is set
x is Element of X
(X,z,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
z .: {x} is set
card (X,z,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,x,x) is Element of bool X
x .: {x} is set
card (X,x,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,c2,x) is Element of bool X
c2 .: {x} is set
(X,s,x) is Element of bool X
s .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
card (X,s,x) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Relation-like X -defined X -valued Element of bool [:X,X:]
x is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,x,c1,z) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,x,b₁) c= card (X,z,b₁) & b₁ in c1 ) } is set
s is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,s,A,c2) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,s,b₁) c= card (X,c2,b₁) & b₁ in A ) } is set
s is set
x is Element of X
(X,s,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
s .: {x} is set
card (X,s,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,c2,x) is Element of bool X
c2 .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,z,x) is Element of bool X
z .: {x} is set
card (X,z,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,x,x) is Element of bool X
x .: {x} is set
card (X,x,x) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Relation-like X -defined X -valued Element of bool [:X,X:]
x is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,x,c1,z) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,x,b₁) in card (X,z,b₁) & b₁ in c1 ) } is set
s is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,s,A,c2) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,s,b₁) in card (X,c2,b₁) & b₁ in A ) } is set
s is set
x is Element of X
(X,s,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
s .: {x} is set
card (X,s,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,c2,x) is Element of bool X
c2 .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,z,x) is Element of bool X
z .: {x} is set
card (X,z,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,x,x) is Element of bool X
x .: {x} is set
card (X,x,x) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,A) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,c1) & b₁ in A ) } is set
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,A,c2) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,c2,b₁) in card (X,c1,b₁) & b₁ in A ) } is set
z is set
x is Element of X
(X,c2,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c2 .: {x} is set
card (X,c2,x) is epsilon-transitive epsilon-connected ordinal cardinal set
(X,c1,x) is Element of bool X
c1 .: {x} is set
card (X,c1,x) is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c2,A) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,c2) & b₁ in A ) } is set
z is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,z,c1) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,z) & b₁ in c1 ) } is set
x is set
s is Element of X
(X,c2,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
c2 .: {s} is set
(X,z,s) is Element of bool X
z .: {s} is set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,A) is Element of bool X
{ (X,c1,b₁) where b₁ is Element of X : b₁ in A } is set
union { (X,c1,b₁) where b₁ is Element of X : b₁ in A } is set
c2 is Element of X
z is set
[z,c2] is set
{z,c2} is finite set
{z} is non empty trivial finite 1 -element set
{{z,c2},{z}} is finite V37() set
x is Element of X
s is Element of X
(X,c1,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
c1 .: {s} is set
z is Element of X
(X,c1,z) is Element of bool X
{z} is non empty trivial finite 1 -element set
c1 .: {z} is set
[z,c2] is set
{z,c2} is finite set
{{z,c2},{z}} is finite V37() set
X is set
bool X is non empty set
X is set
bool X is non empty set
A is Element of bool X
c1 is Element of bool X
A /\ c1 is set
A /\ c1 is Element of bool X
A \/ c1 is set
A \/ c1 is Element of bool X
A \ c1 is set
A \ c1 is Element of bool X
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
(X,A,c1) is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c2,(X,A,c1)) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in (X,A,c1) } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in (X,A,c1) } is set
(X,c2,A) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in A } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in A } is set
(X,c2,c1) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in c1 } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in c1 } is set
(X,(X,c2,A),(X,c2,c1)) is Element of bool X
z is set
the Element of A is Element of A
s is Element of X
(X,c2,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
c2 .: {s} is set
s is set
x is Element of X
(X,c2,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c2 .: {x} is set
the Element of c1 is Element of c1
s is Element of X
(X,c2,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
c2 .: {s} is set
s is set
x is Element of X
(X,c2,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c2 .: {x} is set
z is set
the Element of c1 is Element of c1
s is Element of X
(X,c2,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
c2 .: {s} is set
s is set
x is Element of X
(X,c2,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c2 .: {x} is set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c2,A) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in A } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in A } is set
z is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,z,c1) is Element of bool X
{ (X,z,b₁) where b₁ is Element of X : b₁ in c1 } is set
union { (X,z,b₁) where b₁ is Element of X : b₁ in c1 } is set
(X,c2,c1) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in c1 } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in c1 } is set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,A) is Element of bool X
{ (X,c1,b₁) where b₁ is Element of X : b₁ in A } is set
meet { (X,c1,b₁) where b₁ is Element of X : b₁ in A } is set
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c2,A) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in A } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in A } is set
z is set
x is set
s is Element of X
(X,c1,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
c1 .: {s} is set
(X,c2,s) is Element of bool X
c2 .: {s} is set
s is set
x is Element of X
(X,c2,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c2 .: {x} is set
(X,c1,x) is Element of bool X
c1 .: {x} is set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,A) is Element of bool X
{ (X,c1,b₁) where b₁ is Element of X : b₁ in A } is set
meet { (X,c1,b₁) where b₁ is Element of X : b₁ in A } is set
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
([:X,X:],c1,c2) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,([:X,X:],c1,c2),A) is Element of bool X
{ (X,([:X,X:],c1,c2),b₁) where b₁ is Element of X : b₁ in A } is set
meet { (X,([:X,X:],c1,c2),b₁) where b₁ is Element of X : b₁ in A } is set
(X,c2,A) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in A } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in A } is set
(X,(X,c1,A),(X,c2,A)) is Element of bool X
z is set
the Element of A is Element of A
s is set
x is Element of X
(X,c1,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c1 .: {x} is set
(X,([:X,X:],c1,c2),x) is Element of bool X
([:X,X:],c1,c2) .: {x} is set
Y is set
x is Element of X
(X,([:X,X:],c1,c2),x) is Element of bool X
{x} is non empty trivial finite 1 -element set
([:X,X:],c1,c2) .: {x} is set
(X,c1,x) is Element of bool X
c1 .: {x} is set
(X,c2,x) is Element of bool X
c2 .: {x} is set
(X,(X,c1,x),(X,c2,x)) is Element of bool X
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Element of bool X
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c2,c1) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in c1 } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in c1 } is set
(X,c2,A) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in A } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in A } is set
z is set
the Element of A is Element of A
s is Element of X
(X,c2,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
c2 .: {s} is set
s is set
x is Element of X
(X,c2,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
c2 .: {x} is set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is set
z is set
[c2,z] is set
{c2,z} is finite set
{c2} is non empty trivial finite 1 -element set
{{c2,z},{c2}} is finite V37() set
s is Element of X
x is Element of X
(X,A,x) is Element of bool X
bool X is non empty set
{x} is non empty trivial finite 1 -element set
A .: {x} is set
(X,c1,x) is Element of bool X
c1 .: {x} is set
bool X is non empty set
x is Element of X
{x} is non empty trivial finite 1 -element set
s is Element of X
(X,c1,x) is Element of bool X
c1 .: {x} is set
(X,A,x) is Element of bool X
A .: {x} is set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
bool X is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is Element of X
{c2} is non empty trivial finite 1 -element set
(X,A,c2) is Element of bool X
A .: {c2} is set
z is Element of bool X
(X,A,z) is Element of bool X
{ (X,A,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,A,b₁) where b₁ is Element of X : b₁ in z } is set
(X,c1,c2) is Element of bool X
c1 .: {c2} is set
c2 is Element of X
(X,A,c2) is Element of bool X
{c2} is non empty trivial finite 1 -element set
A .: {c2} is set
(X,c1,c2) is Element of bool X
c1 .: {c2} is set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
bool X is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
c1 is Relation-like set
c2 is set
z is set
[c2,z] is set
{c2,z} is finite set
{c2} is non empty trivial finite 1 -element set
{{c2,z},{c2}} is finite V37() set
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
{ (IFEQ ((X,A,b₁),{},{b₁},{})) where b₁ is Element of X : b₁ in z } is set
union { (IFEQ ((X,A,b₁),{},{b₁},{})) where b₁ is Element of X : b₁ in z } is set
x is set
s is Element of X
(X,c2,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
c2 .: {s} is set
[s,x] is set
{s,x} is finite set
{{s,x},{s}} is finite V37() set
(X,A,s) is Element of bool X
A .: {s} is set
IFEQ ((X,A,s),{},{s},{}) is set
x is set
s is set
s is Element of X
(X,A,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
A .: {s} is set
IFEQ ((X,A,s),{},{s},{}) is set
[s,x] is set
{s,x} is finite set
{{s,x},{s}} is finite V37() set
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Element of bool X
(X,c1,z) is Element of bool X
{ (X,c1,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c1,b₁) where b₁ is Element of X : b₁ in z } is set
{ (IFEQ ((X,A,b₁),{},{b₁},{})) where b₁ is Element of X : b₁ in z } is set
union { (IFEQ ((X,A,b₁),{},{b₁},{})) where b₁ is Element of X : b₁ in z } is set
(X,c2,z) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
A /\ c1 is X -defined X -valued set
A /\ c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
bool X is non empty set
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
A /\ c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
{ (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
union { (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
x is set
s is set
[s,x] is set
{s,x} is finite set
{s} is non empty trivial finite 1 -element set
{{s,x},{s}} is finite V37() set
s is Element of X
x is Element of X
[s,x] is set
{s,x} is finite set
{s} is non empty trivial finite 1 -element set
{{s,x},{s}} is finite V37() set
(X,A,s) is Element of bool X
A .: {s} is set
(X,c1,s) is Element of bool X
c1 .: {s} is set
(X,(X,A,s),(X,c1,s)) is Element of bool X
x is set
s is set
s is Element of X
(X,A,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
A .: {s} is set
(X,c1,s) is Element of bool X
c1 .: {s} is set
(X,(X,A,s),(X,c1,s)) is Element of bool X
x is Element of X
[s,x] is set
{s,x} is finite set
{{s,x},{s}} is finite V37() set
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
{ (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
union { (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
{ (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
union { (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
A /\ c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(A /\ c1),z) is Element of bool X
{ (X,(A /\ c1),b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,(A /\ c1),b₁) where b₁ is Element of X : b₁ in z } is set
A \/ c1 is X -defined X -valued set
A \/ c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
A \/ c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
{ (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
union { (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
x is set
s is set
[s,x] is set
{s,x} is finite set
{s} is non empty trivial finite 1 -element set
{{s,x},{s}} is finite V37() set
s is Element of X
x is Element of X
[s,x] is set
{s,x} is finite set
{s} is non empty trivial finite 1 -element set
{{s,x},{s}} is finite V37() set
(X,A,s) is Element of bool X
A .: {s} is set
(X,c1,s) is Element of bool X
c1 .: {s} is set
(X,(X,A,s),(X,c1,s)) is Element of bool X
x is set
s is set
s is Element of X
(X,A,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
A .: {s} is set
(X,c1,s) is Element of bool X
c1 .: {s} is set
(X,(X,A,s),(X,c1,s)) is Element of bool X
x is Element of X
[s,x] is set
{s,x} is finite set
{{s,x},{s}} is finite V37() set
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
{ (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
union { (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
{ (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
union { (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
A \/ c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(A \/ c1),z) is Element of bool X
{ (X,(A \/ c1),b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,(A \/ c1),b₁) where b₁ is Element of X : b₁ in z } is set
A \ c1 is X -defined X -valued set
A \ c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
A \ c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
{ (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
union { (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
x is set
s is set
[s,x] is set
{s,x} is finite set
{s} is non empty trivial finite 1 -element set
{{s,x},{s}} is finite V37() set
s is Element of X
x is Element of X
[s,x] is set
{s,x} is finite set
{s} is non empty trivial finite 1 -element set
{{s,x},{s}} is finite V37() set
(X,A,s) is Element of bool X
A .: {s} is set
(X,c1,s) is Element of bool X
c1 .: {s} is set
(X,(X,A,s),(X,c1,s)) is Element of bool X
x is set
s is set
s is Element of X
(X,A,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
A .: {s} is set
(X,c1,s) is Element of bool X
c1 .: {s} is set
(X,(X,A,s),(X,c1,s)) is Element of bool X
x is Element of X
[s,x] is set
{s,x} is finite set
{{s,x},{s}} is finite V37() set
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
{ (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
union { (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
{ (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
union { (X,(X,A,b₁),(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
A \ c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(A \ c1),z) is Element of bool X
{ (X,(A \ c1),b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,(A \ c1),b₁) where b₁ is Element of X : b₁ in z } is set
A * c1 is Relation-like set
A * c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
(X,A,z) is Element of bool X
{ (X,A,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,A,b₁) where b₁ is Element of X : b₁ in z } is set
(X,c1,(X,A,z)) is Element of bool X
{ (X,c1,b₁) where b₁ is Element of X : b₁ in (X,A,z) } is set
union { (X,c1,b₁) where b₁ is Element of X : b₁ in (X,A,z) } is set
z is Element of bool X
(X,c2,z) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in z } is set
(X,A,z) is Element of bool X
{ (X,A,b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,A,b₁) where b₁ is Element of X : b₁ in z } is set
(X,c1,(X,A,z)) is Element of bool X
{ (X,c1,b₁) where b₁ is Element of X : b₁ in (X,A,z) } is set
union { (X,c1,b₁) where b₁ is Element of X : b₁ in (X,A,z) } is set
A * c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(A * c1),z) is Element of bool X
{ (X,(A * c1),b₁) where b₁ is Element of X : b₁ in z } is set
union { (X,(A * c1),b₁) where b₁ is Element of X : b₁ in z } is set
c2 is Relation-like set
z is set
x is set
[z,x] is set
{z,x} is finite set
{z} is non empty trivial finite 1 -element set
{{z,x},{z}} is finite V37() set
z is Relation-like X -defined X -valued Element of bool [:X,X:]
x is Element of bool X
(X,z,x) is Element of bool X
{ (X,z,b₁) where b₁ is Element of X : b₁ in x } is set
union { (X,z,b₁) where b₁ is Element of X : b₁ in x } is set
{ (X,c1,(X,A,b₁)) where b₁ is Element of X : b₁ in x } is set
union { (X,c1,(X,A,b₁)) where b₁ is Element of X : b₁ in x } is set
s is set
s is Element of X
(X,z,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
z .: {s} is set
[s,s] is set
{s,s} is finite set
{{s,s},{s}} is finite V37() set
(X,A,s) is Element of bool X
A .: {s} is set
(X,c1,(X,A,s)) is Element of bool X
{ (X,c1,b₁) where b₁ is Element of X : b₁ in (X,A,s) } is set
meet { (X,c1,b₁) where b₁ is Element of X : b₁ in (X,A,s) } is set
x is Element of X
(X,A,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
A .: {x} is set
(X,c1,(X,A,x)) is Element of bool X
{ (X,c1,b₁) where b₁ is Element of X : b₁ in (X,A,x) } is set
meet { (X,c1,b₁) where b₁ is Element of X : b₁ in (X,A,x) } is set
s is set
s is set
x is Element of X
(X,A,x) is Element of bool X
{x} is non empty trivial finite 1 -element set
A .: {x} is set
(X,c1,(X,A,x)) is Element of bool X
{ (X,c1,b₁) where b₁ is Element of X : b₁ in (X,A,x) } is set
meet { (X,c1,b₁) where b₁ is Element of X : b₁ in (X,A,x) } is set
[x,s] is set
{x,s} is finite set
{{x,s},{x}} is finite V37() set
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Relation-like X -defined X -valued Element of bool [:X,X:]
x is Element of bool X
(X,c2,x) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in x } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in x } is set
{ (X,c1,(X,A,b₁)) where b₁ is Element of X : b₁ in x } is set
union { (X,c1,(X,A,b₁)) where b₁ is Element of X : b₁ in x } is set
(X,z,x) is Element of bool X
{ (X,z,b₁) where b₁ is Element of X : b₁ in x } is set
union { (X,z,b₁) where b₁ is Element of X : b₁ in x } is set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,c2) is Relation-like X -defined X -valued Element of bool [:X,X:]
A is Element of X
(X,(X,c1,c2),A) is Element of bool X
bool X is non empty set
{A} is non empty trivial finite 1 -element set
(X,c1,c2) .: {A} is set
(X,c1,A) is Element of bool X
c1 .: {A} is set
(X,c2,A) is Element of bool X
c2 .: {A} is set
(X,(X,c1,A),(X,c2,A)) is Element of bool X
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,c2) is Relation-like X -defined X -valued Element of bool [:X,X:]
A is Element of X
(X,(X,c1,c2),A) is Element of bool X
bool X is non empty set
{A} is non empty trivial finite 1 -element set
(X,c1,c2) .: {A} is set
(X,c1,A) is Element of bool X
c1 .: {A} is set
(X,c2,A) is Element of bool X
c2 .: {A} is set
(X,(X,c1,A),(X,c2,A)) is Element of bool X
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,c2) is Relation-like X -defined X -valued Element of bool [:X,X:]
A is Element of X
(X,(X,c1,c2),A) is Element of bool X
bool X is non empty set
{A} is non empty trivial finite 1 -element set
(X,c1,c2) .: {A} is set
(X,c1,A) is Element of bool X
c1 .: {A} is set
(X,c2,A) is Element of bool X
c2 .: {A} is set
(X,(X,c1,A),(X,c2,A)) is Element of bool X
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,c2) is Relation-like X -defined X -valued Element of bool [:X,X:]
A is Element of X
(X,(X,c1,c2),A) is Element of bool X
bool X is non empty set
{A} is non empty trivial finite 1 -element set
(X,c1,c2) .: {A} is set
(X,c1,A) is Element of bool X
c1 .: {A} is set
(X,c2,(X,c1,A)) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in (X,c1,A) } is set
union { (X,c2,b₁) where b₁ is Element of X : b₁ in (X,c1,A) } is set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,A) is Element of bool X
bool X is non empty set
{A} is non empty trivial finite 1 -element set
c1 .: {A} is set
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,c2) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,c1,c2),A) is Element of bool X
(X,c1,c2) .: {A} is set
(X,c2,(X,c1,A)) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in (X,c1,A) } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in (X,c1,A) } is set
z is Element of bool X
{ (X,c2,(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
{(X,c2,(X,c1,A))} is non empty trivial finite 1 -element set
x is set
s is Element of X
(X,c1,s) is Element of bool X
{s} is non empty trivial finite 1 -element set
c1 .: {s} is set
(X,c2,(X,c1,s)) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in (X,c1,s) } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in (X,c1,s) } is set
x is set
union { (X,c2,(X,c1,b₁)) where b₁ is Element of X : b₁ in z } is set
X is set
A is set
[X,A] is set
{X,A} is finite set
{X} is non empty trivial finite 1 -element set
{{X,A},{X}} is finite V37() set
c1 is set
[:c1,c1:] is set
bool [:c1,c1:] is non empty set
c2 is Relation-like c1 -defined c1 -valued Element of bool [:c1,c1:]
(c1,c2) is Relation-like c1 -defined c1 -valued Element of bool [:c1,c1:]
dom c2 is Element of bool c1
bool c1 is non empty set
Im ((c1,c2),X) is set
(c1,c2) .: {X} is set
(c1,c2) .: {X} is Element of bool c1
{ (IFEQ ((c1,c2,b₁),{},{b₁},{})) where b₁ is Element of c1 : b₁ in {X} } is set
union { (IFEQ ((c1,c2,b₁),{},{b₁},{})) where b₁ is Element of c1 : b₁ in {X} } is set
z is set
x is Element of c1
(c1,c2,x) is Element of bool c1
{x} is non empty trivial finite 1 -element set
c2 .: {x} is set
IFEQ ((c1,c2,x),{},{x},{}) is set
s is set
[x,s] is set
{x,s} is finite set
{{x,s},{x}} is finite V37() set
z is Element of c1
(c1,c2,z) is Element of bool c1
{z} is non empty trivial finite 1 -element set
c2 .: {z} is set
x is set
[z,x] is set
{z,x} is finite set
{{z,x},{z}} is finite V37() set
IFEQ ((c1,c2,z),{},{z},{}) is set
{ (IFEQ ((c1,c2,b₁),{},{b₁},{})) where b₁ is Element of c1 : b₁ in {z} } is set
union { (IFEQ ((c1,c2,b₁),{},{b₁},{})) where b₁ is Element of c1 : b₁ in {z} } is set
x is Element of bool c1
(c1,(c1,c2),x) is Element of bool c1
{ (c1,(c1,c2),b₁) where b₁ is Element of c1 : b₁ in x } is set
union { (c1,(c1,c2),b₁) where b₁ is Element of c1 : b₁ in x } is set
(c1,(c1,c2),z) is Element of bool c1
(c1,c2) .: {z} is set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A) is Relation-like X -defined X -valued Element of bool [:X,X:]
dom A is Element of bool X
bool X is non empty set
X \ (dom A) is Element of bool X
id (X \ (dom A)) is Relation-like set
c1 is set
c2 is set
[c1,c2] is set
{c1,c2} is finite set
{c1} is non empty trivial finite 1 -element set
{{c1,c2},{c1}} is finite V37() set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,A)) is Relation-like X -defined X -valued Element of bool [:X,X:]
dom (X,(X,A)) is Element of bool X
bool X is non empty set
dom A is Element of bool X
dom (X,A) is Element of bool X
X \ (dom (X,A)) is Element of bool X
id (X \ (dom (X,A))) is Relation-like set
dom (id (X \ (dom (X,A)))) is set
X \ (dom A) is Element of bool X
id (X \ (dom A)) is Relation-like set
dom (id (X \ (dom A))) is set
X \ (dom (id (X \ (dom A)))) is Element of bool X
X \ (X \ (dom A)) is Element of bool X
X /\ (dom A) is Element of bool X
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,c1)) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,(X,c1)),A) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,(X,(X,c1))) & b₁ in A ) } is set
(X,c1,A) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,c1) & b₁ in A ) } is set
c2 is set
z is Element of X
(X,(X,(X,c1)),z) is Element of bool X
{z} is non empty trivial finite 1 -element set
(X,(X,c1)) .: {z} is set
dom (X,(X,c1)) is Element of bool X
dom c1 is Element of bool X
(X,c1,z) is Element of bool X
c1 .: {z} is set
c2 is set
z is Element of X
(X,c1,z) is Element of bool X
{z} is non empty trivial finite 1 -element set
c1 .: {z} is set
dom c1 is Element of bool X
dom (X,(X,c1)) is Element of bool X
(X,(X,(X,c1)),z) is Element of bool X
(X,(X,c1)) .: {z} is set
X is set
bool X is non empty set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Element of bool X
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A,c1,0) is Element of bool X
{ b₁ where b₁ is Element of X : ( card (X,c1,b₁) = 0 & b₁ in A ) } is set
(X,c1) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,c1),A) is Element of bool X
{ b₁ where b₁ is Element of X : ex b₂ being Element of X st
( (b₁,b₂,(X,c1)) & b₁ in A ) } is set
c2 is set
z is Element of X
(X,c1,z) is Element of bool X
{z} is non empty trivial finite 1 -element set
c1 .: {z} is set
card (X,c1,z) is epsilon-transitive epsilon-connected ordinal cardinal set
dom c1 is Element of bool X
[z,z] is set
{z,z} is finite set
{{z,z},{z}} is finite V37() set
c2 is set
z is Element of X
x is Element of X
x is Element of X
[z,x] is set
{z,x} is finite set
{z} is non empty trivial finite 1 -element set
{{z,x},{z}} is finite V37() set
dom c1 is Element of bool X
(X,c1,z) is Element of bool X
c1 .: {z} is set
card (X,c1,z) is epsilon-transitive epsilon-connected ordinal cardinal set
s is Element of X
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,A)) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,(X,A))) is Relation-like X -defined X -valued Element of bool [:X,X:]
dom (X,(X,A)) is Element of bool X
bool X is non empty set
X \ (dom (X,(X,A))) is Element of bool X
id (X \ (dom (X,(X,A)))) is Relation-like set
dom A is Element of bool X
X \ (dom A) is Element of bool X
id (X \ (dom A)) is Relation-like set
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A) is Relation-like X -defined X -valued Element of bool [:X,X:]
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,A),(X,c1)) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A,c1) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,A,c1)) is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is set
z is set
[c2,z] is set
{c2,z} is finite set
{c2} is non empty trivial finite 1 -element set
{{c2,z},{c2}} is finite V37() set
dom A is Element of bool X
bool X is non empty set
dom c1 is Element of bool X
(dom A) /\ (dom c1) is Element of bool X
dom (X,A,c1) is Element of bool X
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A) is Relation-like X -defined X -valued Element of bool [:X,X:]
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A,c1) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,A,c1)) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,A),(X,c1)) is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is set
z is set
[c2,z] is set
{c2,z} is finite set
{c2} is non empty trivial finite 1 -element set
{{c2,z},{c2}} is finite V37() set
dom (X,A,c1) is Element of bool X
bool X is non empty set
dom A is Element of bool X
dom c1 is Element of bool X
(dom A) \/ (dom c1) is Element of bool X
dom A is Element of bool X
bool X is non empty set
dom c1 is Element of bool X
(dom A) \/ (dom c1) is Element of bool X
dom (X,A,c1) is Element of bool X
X is set
[:X,X:] is set
bool [:X,X:] is non empty set
A is Relation-like X -defined X -valued Element of bool [:X,X:]
dom A is Element of bool X
bool X is non empty set
c1 is Relation-like X -defined X -valued Element of bool [:X,X:]
dom c1 is Element of bool X
(X,A,c1) is Relation-like X -defined X -valued Element of bool [:X,X:]
c2 is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,A,c1),c2) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,A,c2) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,c1,c2) is Relation-like X -defined X -valued Element of bool [:X,X:]
(X,(X,A,c2),(X,c1,c2)) is Relation-like X -defined X -valued Element of bool [:X,X:]
z is set
x is set
[z,x] is set
{z,x} is finite set
{z} is non empty trivial finite 1 -element set
{{z,x},{z}} is finite V37() set
s is Element of X
s is Element of X
(X,(X,(X,A,c1),c2),s) is Element of bool X
{s} is non empty trivial finite 1 -element set
(X,(X,A,c1),c2) .: {s} is set
(X,(X,A,c1),s) is Element of bool X
(X,A,c1) .: {s} is set
(X,c2,(X,(X,A,c1),s)) is Element of bool X
{ (X,c2,b₁) where b₁ is Element of X : b₁ in (X,(X,A,c1),s) } is set
meet { (X,c2,b₁) where b₁ is Element of X : b₁ in (X,(X,A,c1),s) } is set
(X,A,s) is Element of bool X
A .: {s} is set
(X,c1,s) is Element of