:: CARD_FIL semantic presentation

K172() is set
K176() is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal limit_cardinal countable denumerable Element of bool K172()
bool K172() is non empty set
1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal countable Element of K176()
[:1,1:] is non empty finite countable set
bool [:1,1:] is non empty finite V43() countable set
[:[:1,1:],1:] is non empty finite countable set
bool [:[:1,1:],1:] is non empty finite V43() countable set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal limit_cardinal countable denumerable set
bool omega is non empty non trivial non finite set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional finite V43() cardinal {} -element countable set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional finite V43() cardinal {} -element countable set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional finite V43() cardinal {} -element countable set
alef {} is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal countable Element of K176()
{{},1} is non empty finite V43() countable set
K177() is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional finite V43() cardinal {} -element countable Element of K176()
union {} is epsilon-transitive epsilon-connected ordinal natural finite cardinal countable set
M is set
{M} is non empty trivial finite 1 -element countable set
card {M} is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal countable Element of omega
F is non empty non trivial non finite set
card F is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
F₂() is set
F₁() is non empty set
{ b₁ where b₁ is Element of F₁() : P₁[b₁] } is set
M is Element of F₁()
M is non empty set
{M} is non empty trivial finite 1 -element countable set
bool M is non empty set
bool (bool M) is non empty set
bool M is non empty Element of bool (bool M)
F is set
F is Element of bool M
N is Element of bool M
F /\ N is Element of bool M
M is non empty set
bool M is non empty set
bool (bool M) is non empty set
{M} is non empty trivial finite 1 -element countable set
F is Element of bool M
N is Element of bool M
F /\ N is Element of bool M
Y is Element of bool M
N1 is Element of bool M
M is non empty set
bool M is non empty set
F is set
bool (bool M) is non empty set
N is Element of bool M
Y is Element of bool M
N /\ Y is Element of bool M
N1 is Element of bool M
f is Element of bool M
f1 is set
g is non empty set
bool g is non empty set
bool (bool g) is non empty set
M is non empty set
{M} is non empty trivial finite 1 -element countable set
bool M is non empty set
F is Element of bool M
N is Element of bool M
F /\ N is Element of bool M
Y is Element of bool M
N1 is Element of bool M
bool (bool M) is non empty set
M is non empty set
F is non empty (M)
bool M is non empty set
the Element of F is Element of F
M is non empty set
bool M is non empty set
F is Element of bool M
M \ F is Element of bool M
N is non empty (M)
F /\ (M \ F) is Element of bool M
M is non empty set
bool M is non empty set
bool (bool M) is non empty set
F is non empty (M)
N is non empty Element of bool (bool M)
{} M is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional finite V43() cardinal {} -element countable Element of bool M
({} M) ` is Element of bool M
M \ ({} M) is set
(({} M) `) ` is Element of bool M
M \ (({} M) `) is set
Y is Element of bool M
N1 is Element of bool M
Y \/ N1 is Element of bool M
Y ` is Element of bool M
M \ Y is set
N1 ` is Element of bool M
M \ N1 is set
(Y `) /\ (N1 `) is Element of bool M
(Y \/ N1) ` is Element of bool M
M \ (Y \/ N1) is set
Y ` is Element of bool M
M \ Y is set
N1 ` is Element of bool M
M \ N1 is set
M is non empty set
bool M is non empty set
bool (bool M) is non empty set
M is non empty set
bool M is non empty set
bool (bool M) is non empty set
F is non empty Element of bool (bool M)
COMPLEMENT F is Element of bool (bool M)
M is non empty set
bool M is non empty set
bool (bool M) is non empty set
F is non empty Element of bool (bool M)
COMPLEMENT F is non empty Element of bool (bool M)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool M : b<sub>1</sub> ` in F } is set
N is set
Y is Element of bool M
Y ` is Element of bool M
M \ Y is set
N is set
Y is Element of bool M
Y ` is Element of bool M
M \ Y is set
M is non empty set
bool M is non empty set
bool (bool M) is non empty set
F is non empty Element of bool (bool M)
COMPLEMENT F is non empty Element of bool (bool M)
{ (b₁ `) where b<sub>1</sub> is Element of bool M : b<sub>1</sub> in F } is set
N is set
Y is Element of bool M
Y ` is Element of bool M
M \ Y is set
(Y `) ` is Element of bool M
M \ (Y `) is set
N is set
Y is Element of bool M
Y ` is Element of bool M
M \ Y is set
(Y `) ` is Element of bool M
M \ (Y `) is set
M is non empty set
bool M is non empty set
bool (bool M) is non empty set
the non empty (M) is non empty (M)
COMPLEMENT the non empty (M) is non empty Element of bool (bool M)
N is Element of bool M
N ` is Element of bool M
M \ N is set
Y is Element of bool M
Y ` is Element of bool M
M \ Y is set
N is Element of bool M
Y is Element of bool M
N \/ Y is Element of bool M
N1 is Element of bool M
f is Element of bool M
M is non empty set
F is non empty (M)
COMPLEMENT F is non empty Element of bool (bool M)
bool M is non empty set
bool (bool M) is non empty set
N is Element of bool M
N ` is Element of bool M
M \ N is set
Y is Element of bool M
Y ` is Element of bool M
M \ Y is set
N is Element of bool M
Y is Element of bool M
N \/ Y is Element of bool M
N1 is Element of bool M
f is Element of bool M
M is non empty set
bool M is non empty set
F is non empty (M)
(M,F) is non empty (M)
N is non empty (M)
COMPLEMENT N is non empty Element of bool (bool M)
bool (bool M) is non empty set
Y is Element of bool M
Y ` is Element of bool M
M \ Y is set
(Y `) /\ Y is Element of bool M
{} M is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional finite V43() cardinal {} -element countable Element of bool M
Y is Element of bool M
Y ` is Element of bool M
M \ Y is set
(Y `) \/ Y is Element of bool M
[#] M is non empty non proper Element of bool M
M is non empty set
F is non empty (M)
bool M is non empty set
the Element of F is Element of F
M is non empty set
bool M is non empty set
bool (bool M) is non empty set
M is non empty set
bool M is non empty set
bool (bool M) is non empty set
M is non empty set
M is non empty set
M is epsilon-transitive epsilon-connected ordinal cardinal set
F is non empty set
bool F is non empty set
bool (bool F) is non empty set
N is non empty Element of bool (bool F)
COMPLEMENT N is non empty Element of bool (bool F)
Y is non empty set
card Y is non empty epsilon-transitive epsilon-connected ordinal cardinal set
union Y is set
N1 is non empty Element of bool (bool F)
COMPLEMENT N1 is non empty Element of bool (bool F)
{ H<sub>1</sub>(b<sub>1</sub>) where b<sub>1</sub> is Element of bool F : b<sub>1</sub> in N1 } is set
card { H<sub>1</sub>(b<sub>1</sub>) where b<sub>1</sub> is Element of bool F : b<sub>1</sub> in N1 } is epsilon-transitive epsilon-connected ordinal cardinal set
card N1 is non empty epsilon-transitive epsilon-connected ordinal cardinal set
{ (b<sub>1</sub> `) where b₁ is Element of bool F : b₁ in N1 } is set
card (COMPLEMENT N1) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
union N1 is Element of bool F
(union N1) ` is Element of bool F
F \ (union N1) is set
[#] F is non empty non proper Element of bool F
([#] F) \ (union N1) is Element of bool F
meet (COMPLEMENT N1) is Element of bool F
(meet (COMPLEMENT N1)) ` is Element of bool F
F \ (meet (COMPLEMENT N1)) is set
((meet (COMPLEMENT N1)) `) ` is Element of bool F
F \ ((meet (COMPLEMENT N1)) `) is set
M is non empty set
M is non empty set
bool M is non empty set
N is Element of bool M
F is non empty (M)
{ (b<sub>1</sub> /\ N) where b<sub>1</sub> is Element of bool M : b<sub>1</sub> in F } is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool M : ex b<sub>2</sub> being Element of bool M st
( b<sub>2</sub> in { (b<sub>1</sub> /\ N) where b<sub>3</sub> is Element of bool M : b<sub>1</sub> in F } & b<sub>2</sub> c= b<sub>1</sub> ) } is set
bool (bool M) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool M : S<sub>1</sub>[b<sub>1</sub>] } is set
M /\ N is Element of bool M
M is non empty set
bool M is non empty set
F is Element of bool M
N is non empty (M)
(M,N,F) is non empty Element of bool (bool M)
bool (bool M) is non empty set
{ (b<sub>1</sub> /\ F) where b<sub>1</sub> is Element of bool M : b<sub>1</sub> in N } is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool M : ex b<sub>2</sub> being Element of bool M st
( b<sub>2</sub> in { (b<sub>1</sub> /\ F) where b<sub>3</sub> is Element of bool M : b<sub>1</sub> in N } & b<sub>2</sub> c= b<sub>1</sub> ) } is set
Y is Element of bool M
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool M : S<sub>1</sub>[b<sub>1</sub>] } is set
N1 is Element of bool M
N1 is Element of bool M
f is Element of bool M
f /\ F is Element of bool M
N1 is Element of bool M
N1 /\ F is Element of bool M
f is Element of bool M
M is non empty set
bool M is non empty set
F is Element of bool M
N is non empty (M)
(M,N,F) is non empty Element of bool (bool M)
bool (bool M) is non empty set
{ (b<sub>1</sub> /\ F) where b<sub>1</sub> is Element of bool M : b<sub>1</sub> in N } is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool M : ex b<sub>2</sub> being Element of bool M st
( b<sub>2</sub> in { (b<sub>1</sub> /\ F) where b<sub>3</sub> is Element of bool M : b<sub>1</sub> in N } & b<sub>2</sub> c= b<sub>1</sub> ) } is set
M /\ F is Element of bool M
Y is Element of bool M
Y /\ F is Element of bool M
Y is Element of bool M
N1 is Element of bool M
Y /\ N1 is Element of bool M
f is Element of bool M
f /\ F is Element of bool M
g is Element of bool M
g /\ F is Element of bool M
(f /\ F) /\ (g /\ F) is Element of bool M
F /\ (g /\ F) is Element of bool M
f /\ (F /\ (g /\ F)) is Element of bool M
F /\ F is Element of bool M
g /\ (F /\ F) is Element of bool M
f /\ (g /\ (F /\ F)) is Element of bool M
f /\ g is Element of bool M
(f /\ g) /\ F is Element of bool M
M \ F is Element of bool M
N1 \/ (M \ F) is Element of bool M
(N1 \/ (M \ F)) /\ F is Element of bool M
N1 /\ F is Element of bool M
(M \ F) /\ F is Element of bool M
(N1 /\ F) \/ ((M \ F) /\ F) is Element of bool M
(N1 /\ F) \/ {} is set
f is Element of bool M
f /\ F is Element of bool M
f \ F is Element of bool M
(f /\ F) \/ (f \ F) is Element of bool M
(f /\ F) \/ (M \ F) is Element of bool M
Y is set
N1 is Element of bool M
N1 /\ F is Element of bool M
M is non empty set
bool M is non empty set
bool (bool M) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (bool M) : b<sub>1</sub> is non empty (M) } is set
bool M is non empty Element of bool (bool M)
bool (bool M) is non empty set
bool (bool (bool M)) is non empty set
{M} is non empty trivial finite 1 -element countable set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (bool M) : S<sub>1</sub>[b<sub>1</sub>] } is set
M is non empty set
(M) is non empty Element of bool (bool (bool M))
bool M is non empty Element of bool (bool M)
bool M is non empty set
bool (bool M) is non empty set
bool (bool M) is non empty set
bool (bool (bool M)) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (bool M) : b<sub>1</sub> is non empty (M) } is set
F is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (bool M) : S<sub>1</sub>[b<sub>1</sub>] } is set
M is non empty set
(M) is non empty Element of bool (bool (bool M))
bool M is non empty Element of bool (bool M)
bool M is non empty set
bool (bool M) is non empty set
bool (bool M) is non empty set
bool (bool (bool M)) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (bool M) : b<sub>1</sub> is non empty (M) } is set
bool (M) is non empty set
F is non empty Element of bool (M)
union F is set
N is set
N is set
Y is Element of bool M
N1 is Element of bool M
Y /\ N1 is Element of bool M
f is set
g is set
f is set
Y is set
M is non empty set
F is non empty (M)
bool M is non empty set
bool (bool M) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (bool M) : ( F c= b<sub>1</sub> & b<sub>1</sub> is non empty (M) ) } is set
(M) is non empty Element of bool (bool (bool M))
bool M is non empty Element of bool (bool M)
bool (bool M) is non empty set
bool (bool (bool M)) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (bool M) : b<sub>1</sub> is non empty (M) } is set
Y is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (bool M) : S<sub>1</sub>[b<sub>1</sub>] } is set
bool (M) is non empty set
Y is non empty Element of bool (M)
N1 is set
f is set
f is non empty Element of bool (M)
union f is set
g is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (bool M) : S<sub>2</sub>[b<sub>1</sub>] } is set
g is Element of Y
f1 is set
N1 is set
f is Element of Y
g is non empty (M)
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool (bool M) : S<sub>1</sub>[b<sub>1</sub>] } is set
f1 is Element of bool M
M \ f1 is Element of bool M
MEET is Element of bool M
MEET \ f1 is Element of bool M
(M,g,f1) is non empty Element of bool (bool M)
{ (b<sub>1</sub> /\ f1) where b<sub>1</sub> is Element of bool M : b<sub>1</sub> in g } is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool M : ex b<sub>2</sub> being Element of bool M st
( b<sub>2</sub> in { (b<sub>1</sub> /\ f1) where b<sub>3</sub> is Element of bool M : b<sub>1</sub> in g } & b<sub>2</sub> c= b<sub>1</sub> ) } is set
M is non empty non trivial non finite set
bool M is non empty non trivial non finite set
card M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool M : card (M \ b<sub>1</sub>) in card M } is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool M : S<sub>1</sub>[b<sub>1</sub>] } is set
bool (bool M) is non empty non trivial non finite set
M \ M is Element of bool M
card (M \ M) is epsilon-transitive epsilon-connected ordinal cardinal set
card {} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional finite V43() cardinal {} -element countable Element of omega
N is non empty Element of bool (bool M)
Y is Element of bool M
M \ Y is Element of bool M
card (M \ Y) is epsilon-transitive epsilon-connected ordinal cardinal set
M \ {} is Element of bool M
card (M \ {}) is epsilon-transitive epsilon-connected ordinal cardinal set
Y is Element of bool M
N1 is Element of bool M
Y /\ N1 is Element of bool M
M \ Y is Element of bool M
card (M \ Y) is epsilon-transitive epsilon-connected ordinal cardinal set
M \ N1 is Element of bool M
card (M \ N1) is epsilon-transitive epsilon-connected ordinal cardinal set
(card (M \ Y)) +` (card (M \ N1)) is epsilon-transitive epsilon-connected ordinal cardinal set
(card M) +` (card M) is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
M \ (Y /\ N1) is Element of bool M
card (M \ (Y /\ N1)) is epsilon-transitive epsilon-connected ordinal cardinal set
(M \ Y) \/ (M \ N1) is Element of bool M
card ((M \ Y) \/ (M \ N1)) is epsilon-transitive epsilon-connected ordinal cardinal set
M \ Y is Element of bool M
card (M \ Y) is epsilon-transitive epsilon-connected ordinal cardinal set
M \ N1 is Element of bool M
card (M \ N1) is epsilon-transitive epsilon-connected ordinal cardinal set
M is non empty non trivial non finite set
(M) is non empty (M)
bool M is non empty non trivial non finite set
card M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool M : card (M \ b<sub>1</sub>) in card M } is set
(M,(M)) is non empty (M)
M is non empty non trivial non finite set
bool M is non empty non trivial non finite set
(M) is non empty (M)
card M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool M : card (M \ b<sub>1</sub>) in card M } is set
F is Element of bool M
M \ F is Element of bool M
card (M \ F) is epsilon-transitive epsilon-connected ordinal cardinal set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool M : S<sub>1</sub>[b<sub>1</sub>] } is set
M is non empty non trivial non finite set
bool M is non empty non trivial non finite set
(M) is non empty (M)
(M) is non empty (M)
card M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool M : card (M \ b<sub>1</sub>) in card M } is set
(M,(M)) is non empty (M)
F is Element of bool M
card F is epsilon-transitive epsilon-connected ordinal cardinal set
F ` is Element of bool M
M \ F is set
(F `) ` is Element of bool M
M \ (F `) is set
card ((F `) `) is epsilon-transitive epsilon-connected ordinal cardinal set
M is non empty non trivial non finite set
(M) is non empty (M)
bool M is non empty non trivial non finite set
card M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool M : card (M \ b<sub>1</sub>) in card M } is set
F is non empty (M)
N is Element of bool M
card N is epsilon-transitive epsilon-connected ordinal cardinal set
M \ N is Element of bool M
M \ (M \ N) is Element of bool M
card (M \ (M \ N)) is epsilon-transitive epsilon-connected ordinal cardinal set
M /\ N is Element of bool M
M is non empty non trivial non finite set
(M) is non empty (M)
bool M is non empty non trivial non finite set
card M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool M : card (M \ b<sub>1</sub>) in card M } is set
F is non empty (M)
N is set
M \ N is Element of bool M
card (M \ N) is epsilon-transitive epsilon-connected ordinal cardinal set
M is non empty non trivial non finite set
(M) is non empty (M)
bool M is non empty non trivial non finite set
card M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool M : card (M \ b<sub>1</sub>) in card M } is set
F is non empty (M)
N is Element of bool M
Y is Element of M
{Y} is non empty trivial finite 1 -element countable set
M \ {Y} is Element of bool M
card {Y} is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal countable Element of omega
Y is Element of M
{Y} is non empty trivial finite 1 -element countable set
M \ {Y} is Element of bool M
Y is set
M is non empty non trivial non finite set
F is non empty (M)
bool M is non empty non trivial non finite set
N is Element of bool M
Y is set
N1 is Element of bool M
{Y} is non empty trivial finite 1 -element countable set
card {Y} is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal countable Element of omega
card M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
M \ {Y} is Element of bool M
M is non empty non trivial non finite set
bool M is non empty non trivial non finite set
F is non empty (M) (M)
(M,F) is non empty (M)
N is Element of bool M
N ` is Element of bool M
M \ N is set
N ` is Element of bool M
M \ N is set
M is non empty non trivial non finite set
card M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
F is non empty (M)
N is set
{N} is non empty trivial finite 1 -element countable set
bool M is non empty non trivial non finite set
M \ {N} is Element of bool M
Y is Element of bool M
N is Relation-like Function-like set
dom N is set
rng N is set
bool M is non empty non trivial non finite set
Y is Element of bool M
card Y is epsilon-transitive epsilon-connected ordinal cardinal set
{ (N . b<sub>1</sub>) where b<sub>1</sub> is Element of M : b<sub>1</sub> in Y } is set
N1 is set
f is Element of M
N . f is set
meet { (N . b<sub>1</sub>) where b<sub>1</sub> is Element of M : b<sub>1</sub> in Y } is set
Y /\ (meet { (N . b<sub>1</sub>) where b<sub>1</sub> is Element of M : b<sub>1</sub> in Y } ) is Element of bool M
N1 is set
N . N1 is set
the Element of Y is Element of Y
N . the Element of Y is set
N .: Y is set
N1 is set
f is Element of M
N . f is set
card { (N . b<sub>1</sub>) where b<sub>1</sub> is Element of M : b<sub>1</sub> in Y } is epsilon-transitive epsilon-connected ordinal cardinal set
M is epsilon-transitive epsilon-connected ordinal cardinal set
nextcard M is epsilon-transitive epsilon-connected ordinal cardinal set
exp (2,M) is epsilon-transitive epsilon-connected ordinal cardinal set
card M is epsilon-transitive epsilon-connected ordinal cardinal set
M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
M is epsilon-transitive epsilon-connected ordinal cardinal set
exp (2,M) is epsilon-transitive epsilon-connected ordinal cardinal set
bool M is non empty Element of bool (bool M)
bool M is non empty set
bool (bool M) is non empty set
card (bool M) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
card M is epsilon-transitive epsilon-connected ordinal cardinal set
exp (2,(card M)) is epsilon-transitive epsilon-connected ordinal cardinal set
M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
nextcard F is epsilon-transitive epsilon-connected ordinal cardinal set
exp (2,F) is epsilon-transitive epsilon-connected ordinal cardinal set
M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
exp (2,F) is epsilon-transitive epsilon-connected ordinal cardinal set
nextcard F is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (F,2) is non empty FUNCTION_DOMAIN of F,2
card (Funcs (F,2)) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
N is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
nextcard N is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
exp (2,N) is epsilon-transitive epsilon-connected ordinal cardinal set
M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal set
F is set
sup F is epsilon-transitive epsilon-connected ordinal set
union F is set
union M is epsilon-transitive epsilon-connected ordinal set
N is set
Y is epsilon-transitive epsilon-connected ordinal set
succ Y is non empty epsilon-transitive epsilon-connected ordinal set
N1 is epsilon-transitive epsilon-connected ordinal set
M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
cf M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
F is non empty (M)
N is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom N is epsilon-transitive epsilon-connected ordinal set
rng N is set
sup N is epsilon-transitive epsilon-connected ordinal set
sup (rng N) is epsilon-transitive epsilon-connected ordinal set
union (rng N) is set
card M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
(M,F) is non empty (M)
Y is set
bool M is non empty non trivial non finite set
card Y is epsilon-transitive epsilon-connected ordinal cardinal set
N1 is Element of bool M
card N1 is epsilon-transitive epsilon-connected ordinal cardinal set
card (rng N) is epsilon-transitive epsilon-connected ordinal cardinal set
card (dom N) is epsilon-transitive epsilon-connected ordinal cardinal set
M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
nextcard M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
succ {} is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal countable Element of omega
alef (succ {}) is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
nextcard omega is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal non limit_cardinal set
M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
cf M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
M is epsilon-transitive epsilon-connected ordinal cardinal non limit_cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
nextcard F is epsilon-transitive epsilon-connected ordinal cardinal set
N is epsilon-transitive epsilon-connected ordinal cardinal set
nextcard N is epsilon-transitive epsilon-connected ordinal cardinal set
M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal non limit_cardinal regular set
(M) is epsilon-transitive epsilon-connected ordinal cardinal set
nextcard (M) is epsilon-transitive epsilon-connected ordinal cardinal set
M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal non limit_cardinal regular set
(M) is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
[:(M),M:] is non empty non trivial non finite set
bool M is non empty non trivial non finite Element of bool (bool M)
bool M is non empty non trivial non finite set
bool (bool M) is non empty non trivial non finite set
[:[:(M),M:],(bool M):] is non empty non trivial non finite set
bool [:[:(M),M:],(bool M):] is non empty non trivial non finite set
M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal non limit_cardinal regular set
(M) is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
[:(M),M:] is non empty non trivial non finite set
bool M is non empty non trivial non finite Element of bool (bool M)
bool M is non empty non trivial non finite set
bool (bool M) is non empty non trivial non finite set
[:[:(M),M:],(bool M):] is non empty non trivial non finite set
bool [:[:(M),M:],(bool M):] is non empty non trivial non finite set
nextcard (M) is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal non limit_cardinal regular set
(nextcard (M)) \ (M) is Element of bool (nextcard (M))
bool (nextcard (M)) is non empty non trivial non finite set
Funcs ((M),(nextcard (M))) is non empty FUNCTION_DOMAIN of (M), nextcard (M)
Y is set
card (M) is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
N1 is epsilon-transitive epsilon-connected ordinal Element of nextcard (M)
card N1 is epsilon-transitive epsilon-connected ordinal cardinal set
f is Relation-like Function-like set
dom f is set
rng f is set
Y is Relation-like Function-like set
dom Y is set
rng Y is set
N1 is set
Y . N1 is set
f is Relation-like Function-like set
dom f is set
rng f is set
N1 is Relation-like Function-like Function-yielding V35() set
f is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of f : H<sub>1</sub>(a<sub>1</sub>,b<sub>1</sub>) = a<sub>2</sub> } is set
bool f is non empty set
g is epsilon-transitive epsilon-connected ordinal Element of (M)
f1 is epsilon-transitive epsilon-connected ordinal Element of M
{ b<sub>1</sub> where b<sub>1</sub> is Element of f : H<sub>1</sub>(g,b<sub>1</sub>) = f1 } is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of f : S<sub>3</sub>[b<sub>1</sub>] } is set
bool f is non empty Element of bool (bool f)
bool (bool f) is non empty set
[:[:(M),M:],(bool f):] is non empty non trivial non finite set
bool [:[:(M),M:],(bool f):] is non empty non trivial non finite set
g is Relation-like [:(M),M:] -defined bool f -valued Function-like quasi_total Element of bool [:[:(M),M:],(bool f):]
f1 is Relation-like [:(M),M:] -defined bool M -valued Function-like quasi_total Element of bool [:[:(M),M:],(bool M):]
MEET is epsilon-transitive epsilon-connected ordinal Element of (M)
B is epsilon-transitive epsilon-connected ordinal Element of (M)
MEET is epsilon-transitive epsilon-connected ordinal Element of M
f1 . (MEET,MEET) is Element of bool M
[MEET,MEET] is non natural set
{MEET,MEET} is non empty finite countable set
{MEET} is non empty trivial finite 1 -element countable set
{{MEET,MEET},{MEET}} is non empty finite V43() countable set
f1 . [MEET,MEET] is set
X1 is epsilon-transitive epsilon-connected ordinal Element of M
f1 . (B,X1) is Element of bool M
[B,X1] is non natural set
{B,X1} is non empty finite countable set
{B} is non empty trivial finite 1 -element countable set
{{B,X1},{B}} is non empty finite V43() countable set
f1 . [B,X1] is set
(f1 . (MEET,MEET)) /\ (f1 . (B,X1)) is Element of bool M
h1 is set
g . (MEET,MEET) is Element of bool f
g . [MEET,MEET] is set
Z is Element of f
N1 . Z is Relation-like Function-like set
(N1 . Z) . MEET is set
(N1 . Z) . B is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of f : S<sub>3</sub>[b<sub>1</sub>] } is set
g . (B,X1) is Element of bool f
g . [B,X1] is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of f : S<sub>4</sub>[b<sub>1</sub>] } is set
MEET is epsilon-transitive epsilon-connected ordinal Element of (M)
B is epsilon-transitive epsilon-connected ordinal Element of M
f1 . (MEET,B) is Element of bool M
[MEET,B] is non natural set
{MEET,B} is non empty finite countable set
{MEET} is non empty trivial finite 1 -element countable set
{{MEET,B},{MEET}} is non empty finite V43() countable set
f1 . [MEET,B] is set
MEET is epsilon-transitive epsilon-connected ordinal Element of M
f1 . (MEET,MEET) is Element of bool M
[MEET,MEET] is non natural set
{MEET,MEET} is non empty finite countable set
{{MEET,MEET},{MEET}} is non empty finite V43() countable set
f1 . [MEET,MEET] is set
(f1 . (MEET,B)) /\ (f1 . (MEET,MEET)) is Element of bool M
X1 is set
h1 is Element of f
N1 . h1 is Relation-like Function-like set
(N1 . h1) . MEET is set
MEET is epsilon-transitive epsilon-connected ordinal Element of M
B is epsilon-transitive epsilon-connected ordinal Element of (M)
f1 . (B,MEET) is Element of bool M
[B,MEET] is non natural set
{B,MEET} is non empty finite countable set
{B} is non empty trivial finite 1 -element countable set
{{B,MEET},{B}} is non empty finite V43() countable set
f1 . [B,MEET] is set
MEET is epsilon-transitive epsilon-connected ordinal Element of (M)
f1 . (MEET,MEET) is Element of bool M
[MEET,MEET] is non natural set
{MEET,MEET} is non empty finite countable set
{MEET} is non empty trivial finite 1 -element countable set
{{MEET,MEET},{MEET}} is non empty finite V43() countable set
f1 . [MEET,MEET] is set
(f1 . (B,MEET)) /\ (f1 . (MEET,MEET)) is Element of bool M
X1 is set
h1 is Element of f
N1 . h1 is Relation-like Function-like set
(N1 . h1) . B is set
(N1 . h1) . MEET is set
Y . h1 is set
Z is Relation-like Function-like set
dom Z is set
rng Z is set
B is Element of f
N1 . B is Relation-like Function-like set
dom (N1 . B) is set
rng (N1 . B) is set
Y . B is set
MEET is Relation-like Function-like set
dom MEET is set
rng MEET is set
MEET is epsilon-transitive epsilon-connected ordinal Element of (M)
{ (f1 . (MEET,b<sub>1</sub>)) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal Element of M : b<sub>1</sub> in M } is set
union { (f1 . (MEET,b<sub>1</sub>)) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal Element of M : b<sub>1</sub> in M } is set
M \ (union { (f1 . (MEET,b<sub>1</sub>)) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal Element of M : b<sub>1</sub> in M } ) is Element of bool M
card (M \ (union { (f1 . (MEET,b<sub>1</sub>)) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal Element of M : b<sub>1</sub> in M } )) is epsilon-transitive epsilon-connected ordinal cardinal set
B is set
MEET is epsilon-transitive epsilon-connected ordinal Element of M
f1 . (MEET,MEET) is Element of bool M
[MEET,MEET] is non natural set
{MEET,MEET} is non empty finite countable set
{MEET} is non empty trivial finite 1 -element countable set
{{MEET,MEET},{MEET}} is non empty finite V43() countable set
f1 . [MEET,MEET] is set
g . (MEET,MEET) is Element of bool f
g . [MEET,MEET] is set
B is set
MEET is Element of f
N1 . MEET is Relation-like Function-like set
dom (N1 . MEET) is set
(N1 . MEET) . MEET is set
rng (N1 . MEET) is set
f1 . (MEET,H<sub>1</sub>(MEET,MEET)) is set
[MEET,((N1 . MEET) . MEET)] is non natural set
{MEET,((N1 . MEET) . MEET)} is non empty finite countable set
{MEET} is non empty trivial finite 1 -element countable set
{{MEET,((N1 . MEET) . MEET)},{MEET}} is non empty finite V43() countable set
f1 . [MEET,((N1 . MEET) . MEET)] is set
{ b<sub>1</sub> where b<sub>1</sub> is Element of f : H<sub>1</sub>(MEET,b<sub>1</sub>) = H<sub>1</sub>(MEET,MEET) } is set
M \ (M) is Element of bool M
M /\ (M) is set
MEET is epsilon-transitive epsilon-connected ordinal Element of M
{ (f1 . (b<sub>1</sub>,MEET)) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal Element of (M) : b<sub>1</sub> in (M) } is set
union { (f1 . (b<sub>1</sub>,MEET)) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal Element of (M) : b<sub>1</sub> in (M) } is set
M \ (union { (f1 . (b<sub>1</sub>,MEET)) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal Element of (M) : b<sub>1</sub> in (M) } ) is Element of bool M
card (M \ (union { (f1 . (b<sub>1</sub>,MEET)) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal Element of (M) : b<sub>1</sub> in (M) } )) is epsilon-transitive epsilon-connected ordinal cardinal set
card MEET is epsilon-transitive epsilon-connected ordinal cardinal set
card (M) is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
{ b<sub>1</sub> where b<sub>1</sub> is Element of f : MEET in b<sub>1</sub> } is set
M \ { b<sub>1</sub> where b<sub>1</sub> is Element of f : MEET in b<sub>1</sub> } is Element of bool M
card (M \ { b<sub>1</sub> where b<sub>1</sub> is Element of f : MEET in b<sub>1</sub> } ) is epsilon-transitive epsilon-connected ordinal cardinal set
{MEET} is non empty trivial finite 1 -element countable set
MEET \/ {MEET} is non empty set
M \ (MEET \/ {MEET}) is Element of bool M
B is set
MEET is epsilon-transitive epsilon-connected ordinal Element of M
X1 is Element of f
M \ (M \ (MEET \/ {MEET})) is Element of bool M
M /\ (MEET \/ {MEET}) is set
card (MEET \/ {MEET}) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
{ b<sub>1</sub> where b<sub>1</sub> is Element of f : S<sub>3</sub>[b<sub>1</sub>] } is set
B is set
MEET is epsilon-transitive epsilon-connected ordinal Element of nextcard (M)
X1 is Element of f
M \ (M) is Element of bool M
M \ (M \ (M)) is Element of bool M
M /\ (M) is set
B is set
MEET is Element of f
N1 . MEET is Relation-like Function-like set
rng (N1 . MEET) is set
dom (N1 . MEET) is set
X1 is set
(N1 . MEET) . X1 is set
h1 is epsilon-transitive epsilon-connected ordinal Element of (M)
{ b<sub>1</sub> where b<sub>1</sub> is Element of f : H<sub>1</sub>(h1,b<sub>1</sub>) = MEET } is set
f1 . (h1,MEET) is Element of bool M
[h1,MEET] is non natural set
{h1,MEET} is non empty finite countable set
{h1} is non empty trivial finite 1 -element countable set
{{h1,MEET},{h1}} is non empty finite V43() countable set
f1 . [h1,MEET] is set
M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal non limit_cardinal regular set
(M) is non empty (M)
(M) is non empty (M)
bool M is non empty non trivial non finite set
card M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool M : card (M \ b<sub>1</sub>) in card M } is set
(M,(M)) is non empty (M)
bool (bool M) is non empty non trivial non finite set
(M) is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
N is non empty (M)
[:(M),M:] is non empty non trivial non finite set
bool M is non empty non trivial non finite Element of bool (bool M)
[:[:(M),M:],(bool M):] is non empty non trivial non finite set
bool [:[:(M),M:],(bool M):] is non empty non trivial non finite set
Y is Relation-like [:(M),M:] -defined bool M -valued Function-like quasi_total Element of bool [:[:(M),M:],(bool M):]
nextcard (M) is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal non limit_cardinal regular set
COMPLEMENT N is non empty Element of bool (bool M)
N1 is epsilon-transitive epsilon-connected ordinal Element of M
{ (Y . (b<sub>1</sub>,N1)) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal Element of (M) : b<sub>1</sub> in (M) } is set
union { (Y . (b<sub>1</sub>,N1)) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal Element of (M) : b<sub>1</sub> in (M) } is set
{ H<sub>1</sub>(b<sub>1</sub>,b<sub>2</sub>) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal Element of (M), b<sub>2</sub> is epsilon-transitive epsilon-connected ordinal Element of M : ( b<sub>2</sub> = N1 & S<sub>2</sub>[b<sub>1</sub>,b<sub>2</sub>] ) } is set
{ H<sub>1</sub>(b<sub>1</sub>,N1) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal Element of (M) : S<sub>2</sub>[b<sub>1</sub>,N1] } is set
{ H<sub>1</sub>(b<sub>1</sub>,b<sub>2</sub>) where b<sub>1</sub> is epsilon-transitive epsilon-connected ordinal Element of (M), b<sub>2</sub> is epsilon-transitive epsilon-connected ordinal Element of M : S<sub>3</sub>[b<sub>1</sub>,b<sub>2</sub>] } is set
f is Element of bool (bool M)
union f is Element of bool M
(union f) ` is Element of bool M
M \ (union f) is set
M \ (union { (Y . (b₁,N1)) where b₁ is epsilon-transitive epsilon-connected ordinal Element of (M) : b₁ in (M) } ) is Element of bool M
card (M \ (union { (Y . (b₁,N1)) where b₁ is epsilon-transitive epsilon-connected ordinal Element of (M) : b₁ in (M) } )) is epsilon-transitive epsilon-connected ordinal cardinal set
N1 is epsilon-transitive epsilon-connected ordinal Element of M
{ (Y . (b₁,N1)) where b₁ is epsilon-transitive epsilon-connected ordinal Element of (M) : b₁ in (M) } is set
the epsilon-transitive epsilon-connected ordinal Element of (M) is epsilon-transitive epsilon-connected ordinal Element of (M)
Y . ( the epsilon-transitive epsilon-connected ordinal Element of (M),N1) is Element of bool M
[ the epsilon-transitive epsilon-connected ordinal Element of (M),N1] is non natural set
{ the epsilon-transitive epsilon-connected ordinal Element of (M),N1} is non empty finite countable set
{ the epsilon-transitive epsilon-connected ordinal Element of (M)} is non empty trivial finite 1 -element countable set
{{ the epsilon-transitive epsilon-connected ordinal Element of (M),N1},{ the epsilon-transitive epsilon-connected ordinal Element of (M)}} is non empty finite V43() countable set
Y . [ the epsilon-transitive epsilon-connected ordinal Element of (M),N1] is set
{N1} is non empty trivial finite 1 -element countable set
[:(M),{N1}:] is non empty non trivial non finite set
{ H₁(b₁) where b₁ is Element of [:(M),M:] : b₁ in [:(M),{N1}:] } is set
card { H₁(b₁) where b₁ is Element of [:(M),M:] : b₁ in [:(M),{N1}:] } is epsilon-transitive epsilon-connected ordinal cardinal set
card [:(M),{N1}:] is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
{ (Y . b₁) where b₁ is Element of [:(M),M:] : b₁ in [:(M),{N1}:] } is set
f is set
g is epsilon-transitive epsilon-connected ordinal Element of (M)
Y . (g,N1) is Element of bool M
[g,N1] is non natural set
{g,N1} is non empty finite countable set
{g} is non empty trivial finite 1 -element countable set
{{g,N1},{g}} is non empty finite V43() countable set
Y . [g,N1] is set
card { (Y . (b₁,N1)) where b₁ is epsilon-transitive epsilon-connected ordinal Element of (M) : b₁ in (M) } is epsilon-transitive epsilon-connected ordinal cardinal set
card { (Y . b₁) where b₁ is Element of [:(M),M:] : b₁ in [:(M),{N1}:] } is epsilon-transitive epsilon-connected ordinal cardinal set
f is set
g is epsilon-transitive epsilon-connected ordinal Element of (M)
Y . (g,N1) is Element of bool M
[g,N1] is non natural set
{g,N1} is non empty finite countable set
{g} is non empty trivial finite 1 -element countable set
{{g,N1},{g}} is non empty finite V43() countable set
Y . [g,N1] is set
card (M) is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
union { (Y . (b₁,N1)) where b₁ is epsilon-transitive epsilon-connected ordinal Element of (M) : b₁ in (M) } is set
[:M,(M):] is non empty non trivial non finite set
bool [:M,(M):] is non empty non trivial non finite set
N1 is Relation-like M -defined (M) -valued Function-like quasi_total Element of bool [:M,(M):]
{ (sup (N1 " {b₁})) where b₁ is epsilon-transitive epsilon-connected ordinal Element of (M) : b₁ in (M) } is set
f is set
g is epsilon-transitive epsilon-connected ordinal Element of (M)
{g} is non empty trivial finite 1 -element countable set
N1 " {g} is Element of bool M
sup (N1 " {g}) is epsilon-transitive epsilon-connected ordinal set
card (N1 " {g}) is epsilon-transitive epsilon-connected ordinal cardinal set
cf M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
{ H₁(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal Element of (M) : b₁ in (M) } is set
card { H₁(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal Element of (M) : b₁ in (M) } is epsilon-transitive epsilon-connected ordinal cardinal set
card (M) is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
card { (sup (N1 " {b₁})) where b₁ is epsilon-transitive epsilon-connected ordinal Element of (M) : b₁ in (M) } is epsilon-transitive epsilon-connected ordinal cardinal set
cf M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
sup { (sup (N1 " {b₁})) where b₁ is epsilon-transitive epsilon-connected ordinal Element of (M) : b₁ in (M) } is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal Element of (M)
{g} is non empty trivial finite 1 -element countable set
N1 " {g} is Element of bool M
sup (N1 " {g}) is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal Element of M
N1 . f is epsilon-transitive epsilon-connected ordinal Element of (M)
{(N1 . f)} is non empty trivial finite 1 -element countable set
N1 " {(N1 . f)} is Element of bool M
sup (N1 " {(N1 . f)}) is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal Element of (M)
{f} is non empty trivial finite 1 -element countable set
N1 " {f} is Element of bool M
card (N1 " {f}) is epsilon-transitive epsilon-connected ordinal cardinal set
f is epsilon-transitive epsilon-connected ordinal Element of (M)
{f} is non empty trivial finite 1 -element countable set
N1 " {f} is Element of bool M
card (N1 " {f}) is epsilon-transitive epsilon-connected ordinal cardinal set
{ (Y . (f,b₁)) where b₁ is epsilon-transitive epsilon-connected ordinal Element of M : N1 . b₁ = f } is set
g is set
f1 is epsilon-transitive epsilon-connected ordinal Element of M
Y . (f,f1) is Element of bool M
[f,f1] is non natural set
{f,f1} is non empty finite countable set
{{f,f1},{f}} is non empty finite V43() countable set
Y . [f,f1] is set
N1 . f1 is epsilon-transitive epsilon-connected ordinal Element of (M)
dom Y is Relation-like (M) -defined M -valued Element of bool [:(M),M:]
bool [:(M),M:] is non empty non trivial non finite set
Funcs (M,(bool M)) is non empty FUNCTION_DOMAIN of M, bool M
curry Y is Relation-like (M) -defined Funcs (M,(bool M)) -valued Function-like quasi_total Element of bool [:(M),(Funcs (M,(bool M))):]
[:(M),(Funcs (M,(bool M))):] is non empty non trivial non finite set
bool [:(M),(Funcs (M,(bool M))):] is non empty non trivial non finite set
(curry Y) . f is Element of Funcs (M,(bool M))
rng Y is Element of bool (bool M)
bool (bool M) is non empty non trivial non finite set
f1 is Relation-like Function-like set
dom f1 is set
rng f1 is set
MEET is Relation-like Function-like set
dom MEET is set
rng MEET is set
MEET * f1 is Relation-like Function-like set
dom (MEET * f1) is set
g is Element of bool (bool M)
rng (MEET * f1) is set
B is set
MEET is epsilon-transitive epsilon-connected ordinal Element of M
Y . (f,MEET) is Element of bool M
[f,MEET] is non natural set
{f,MEET} is non empty finite countable set
{{f,MEET},{f}} is non empty finite V43() countable set
Y . [f,MEET] is set
N1 . MEET is epsilon-transitive epsilon-connected ordinal Element of (M)
dom N1 is Element of bool M
X1 is set
MEET . X1 is set
f1 . (MEET . X1) is set
(MEET * f1) . X1 is set
B is set
MEET . B is set
N1 . (MEET . B) is set
B is set
MEET is set
(MEET * f1) . MEET is set
MEET . MEET is set
f1 . (MEET . MEET) is set
X1 is epsilon-transitive epsilon-connected ordinal Element of M
Y . (f,X1) is Element of bool M
[f,X1] is non natural set
{f,X1} is non empty finite countable set
{{f,X1},{f}} is non empty finite V43() countable set
Y . [f,X1] is set
N1 . X1 is epsilon-transitive epsilon-connected ordinal Element of (M)
B is epsilon-transitive epsilon-connected ordinal Element of M
N1 . B is epsilon-transitive epsilon-connected ordinal Element of (M)
Y . (f,B) is Element of bool M
[f,B] is non natural set
{f,B} is non empty finite countable set
{{f,B},{f}} is non empty finite V43() countable set
Y . [f,B] is set
MEET is epsilon-transitive epsilon-connected ordinal Element of M
Y . (f,MEET) is Element of bool M
[f,MEET] is non natural set
{f,MEET} is non empty finite countable set
{{f,MEET},{f}} is non empty finite V43() countable set
Y . [f,MEET] is set
(Y . (f,B)) /\ (Y . (f,MEET)) is Element of bool M
B is set
MEET is set
(MEET * f1) . B is set
(MEET * f1) . MEET is set
MEET . B is set
MEET . MEET is set
f1 . (MEET . MEET) is set
Y . (f,(MEET . MEET)) is set
[f,(MEET . MEET)] is non natural set
{f,(MEET . MEET)} is non empty finite countable set
{{f,(MEET . MEET)},{f}} is non empty finite V43() countable set
Y . [f,(MEET . MEET)] is set
h1 is epsilon-transitive epsilon-connected ordinal Element of M
N1 . h1 is epsilon-transitive epsilon-connected ordinal Element of (M)
Y . (f,h1) is Element of bool M
[f,h1] is non natural set
{f,h1} is non empty finite countable set
{{f,h1},{f}} is non empty finite V43() countable set
Y . [f,h1] is set
X1 is epsilon-transitive epsilon-connected ordinal Element of M
Y . (f,X1) is Element of bool M
[f,X1] is non natural set
{f,X1} is non empty finite countable set
{{f,X1},{f}} is non empty finite V43() countable set
Y . [f,X1] is set
f1 . (MEET . B) is set
Y . (f,(MEET . B)) is set
[f,(MEET . B)] is non natural set
{f,(MEET . B)} is non empty finite countable set
{{f,(MEET . B)},{f}} is non empty finite V43() countable set
Y . [f,(MEET . B)] is set
card g is epsilon-transitive epsilon-connected ordinal cardinal set
B is set
MEET is epsilon-transitive epsilon-connected ordinal Element of M
Y . (f,MEET) is Element of bool M
[f,MEET] is non natural set
{f,MEET} is non empty finite countable set
{{f,MEET},{f}} is non empty finite V43() countable set
Y . [f,MEET] is set
N1 . MEET is epsilon-transitive epsilon-connected ordinal Element of (M)
B is set
MEET is set
X1 is epsilon-transitive epsilon-connected ordinal Element of M
Y . (f,X1) is Element of bool M
[f,X1] is non natural set
{f,X1} is non empty finite countable set
{{f,X1},{f}} is non empty finite V43() countable set
Y . [f,X1] is set
N1 . X1 is epsilon-transitive epsilon-connected ordinal Element of (M)
h1 is epsilon-transitive epsilon-connected ordinal Element of M
Y . (f,h1) is Element of bool M
[f,h1] is non natural set
{f,h1} is non empty finite countable set
{{f,h1},{f}} is non empty finite V43() countable set
Y . [f,h1] is set
N1 . h1 is epsilon-transitive epsilon-connected ordinal Element of (M)
(Y . (f,h1)) /\ (Y . (f,X1)) is Element of bool M
M is set
card M is epsilon-transitive epsilon-connected ordinal cardinal set
F is Relation-like Function-like set
dom F is set
rng F is set
N is epsilon-transitive epsilon-connected ordinal cardinal set
F | N is Relation-like Function-like set
dom (F | N) is set
F .: N is set
card (F .: N) is epsilon-transitive epsilon-connected ordinal cardinal set
rng (F | N) is set
M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal non limit_cardinal regular set
F is non empty (M)
(M) is non empty (M)
(M) is non empty (M)
bool M is non empty non trivial non finite set
card M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
{ b₁ where b₁ is Element of bool M : card (M \ b₁) in card M } is set
(M,(M)) is non empty (M)
(M,F) is non empty (M)
N is set
Y is Element of bool M
card Y is epsilon-transitive epsilon-connected ordinal cardinal set
bool (bool M) is non empty non trivial non finite set
N is Element of bool (bool M)
card N is epsilon-transitive epsilon-connected ordinal cardinal set
Y is set
{Y} is non empty trivial finite 1 -element countable set
N \ {Y} is Element of bool (bool M)
N1 is set
N \ {Y} is Element of bool N
bool N is non empty set
Y /\ N1 is set
f1 is set
MEET is Element of bool M
f is Element of bool M
g is Element of bool M
M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
F is non empty (M)
card M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
F is non empty (M)
N is epsilon-transitive epsilon-connected ordinal cardinal set
exp (2,N) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (N,2) is non empty FUNCTION_DOMAIN of N,2
card (Funcs (N,2)) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
Y is set
card Y is epsilon-transitive epsilon-connected ordinal cardinal set
card N is epsilon-transitive epsilon-connected ordinal cardinal set
exp (2,(card N)) is epsilon-transitive epsilon-connected ordinal cardinal set
bool N is non empty Element of bool (bool N)
bool N is non empty set
bool (bool N) is non empty set
card (bool N) is non empty epsilon-transitive epsilon-connected ordinal cardinal set
f is Relation-like Function-like set
dom f is set
rng f is set
N1 is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
[:N1,{{},1}:] is non empty non trivial non finite set
bool [:N1,{{},1}:] is non empty non trivial non finite set
{ b₁ where b₁ is Relation-like N1 -defined {{},1} -valued Function-like quasi_total Element of bool [:N1,{{},1}:] : ( b₁ in Y & b₁ . a₁ = a₂ ) } is set
f " { b₁ where b₁ is Relation-like N1 -defined {{},1} -valued Function-like quasi_total Element of bool [:N1,{{},1}:] : ( b₁ in Y & b₁ . a₁ = a₂ ) } is set
g is epsilon-transitive epsilon-connected ordinal Element of N1
{ b₁ where b₁ is Relation-like N1 -defined {{},1} -valued Function-like quasi_total Element of bool [:N1,{{},1}:] : ( b₁ in Y & b₁ . g = 1 ) } is set
bool M is non empty non trivial non finite set
f " { b₁ where b₁ is Relation-like N1 -defined {{},1} -valued Function-like quasi_total Element of bool [:N1,{{},1}:] : ( b₁ in Y & b₁ . g = 1 ) } is set
{ b₁ where b₁ is Relation-like N1 -defined {{},1} -valued Function-like quasi_total Element of bool [:N1,{{},1}:] : ( b₁ in Y & b₁ . g = {} ) } is set
f " { b₁ where b₁ is Relation-like N1 -defined {{},1} -valued Function-like quasi_total Element of bool [:N1,{{},1}:] : ( b₁ in Y & b₁ . g = {} ) } is set
X1 is Relation-like N1 -defined {{},1} -valued Function-like quasi_total Element of bool [:N1,{{},1}:]
X1 . g is finite countable Element of {{},1}
Y \ { b₁ where b₁ is Relation-like N1 -defined {{},1} -valued Function-like quasi_total Element of bool [:N1,{{},1}:] : ( b₁ in Y & b₁ . g = {} ) } is Element of bool Y
bool Y is non empty set
X1 is set
h1 is Relation-like Function-like set
dom h1 is set
rng h1 is set
Z is Relation-like N1 -defined {{},1} -valued Function-like quasi_total Element of bool [:N1,{{},1}:]
X1 is set
h1 is Relation-like N1 -defined {{},1} -valued Function-like quasi_total Element of bool [:N1,{{},1}:]
h1 . g is finite countable Element of {{},1}
Z is Relation-like N1 -defined {{},1} -valued Function-like quasi_total Element of bool [:N1,{{},1}:]
Z . g is finite countable Element of {{},1}
MEET is Element of bool M
f " (rng f) is set
MEET is Element of bool M
(f " (rng f)) \ MEET is Element of bool (f " (rng f))
bool (f " (rng f)) is non empty set
M \ MEET is Element of bool M
X1 is finite countable Element of {{},1}
{ b₁ where b₁ is Relation-like N1 -defined {{},1} -valued Function-like quasi_total Element of bool [:N1,{{},1}:] : ( b₁ in Y & b₁ . g = X1 ) } is set
f " { b₁ where b₁ is Relation-like N1 -defined {{},1} -valued Function-like quasi_total Element of bool [:N1,{{},1}:] : ( b₁ in Y & b₁ . g = X1 ) } is set
X1 is finite countable Element of {{},1}
{ b₁ where b₁ is Relation-like N1 -defined {{},1} -valued Function-like quasi_total Element of bool [:N1,{{},1}:] : ( b₁ in Y & b₁ . g = X1 ) } is set
f " { b₁ where b₁ is Relation-like N1 -defined {{},1} -valued Function-like quasi_total Element of bool [:N1,{{},1}:] : ( b₁ in Y & b₁ . g = X1 ) } is set
g is Relation-like N1 -defined {{},1} -valued Function-like quasi_total Element of bool [:N1,{{},1}:]
{ b₁ where b₁ is Relation-like N1 -defined {{},1} -valued Function-like quasi_total Element of bool [:N1,{{},1}:] : ( b₁ in Y & b₁ . a₁ = g . a₁ ) } is set
f " { b₁ where b₁ is Relation-like N1 -defined {{},1} -valued Function-like quasi_total Element of bool [:N1,{{},1}:] : ( b₁ in Y & b₁ . a₁ = g . a₁ ) } is set
[:M,Y:] is set
bool [:M,Y:] is non empty set
{ H₁(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal Element of N1 : b₁ in N1 } is set
meet { H₁(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal Element of N1 : b₁ in N1 } is set
f | (meet { H₁(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal Element of N1 : b₁ in N1 } ) is Relation-like Function-like set
rng (f | (meet { H₁(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal Element of N1 : b₁ in N1 } )) is set
f .: (meet { H₁(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal Element of N1 : b₁ in N1 } ) is set
card { H₁(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal Element of N1 : b₁ in N1 } is epsilon-transitive epsilon-connected ordinal cardinal set
card N1 is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
the epsilon-transitive epsilon-connected ordinal Element of N1 is epsilon-transitive epsilon-connected ordinal Element of N1
MEET is set
X1 is epsilon-transitive epsilon-connected ordinal Element of N1
g . X1 is finite countable Element of {{},1}
{ b₁ where b₁ is Relation-like N1 -defined {{},1} -valued Function-like quasi_total Element of bool [:N1,{{},1}:] : ( b₁ in Y & b₁ . X1 = g . X1 ) } is set
f " { b₁ where b₁ is Relation-like N1 -defined {{},1} -valued Function-like quasi_total Element of bool [:N1,{{},1}:] : ( b₁ in Y & b₁ . X1 = g . X1 ) } is set
g . the epsilon-transitive epsilon-connected ordinal Element of N1 is finite countable Element of {{},1}
{ b₁ where b₁ is Relation-like N1 -defined {{},1} -valued Function-like quasi_total Element of bool [:N1,{{},1}:] : ( b₁ in Y & b₁ . the epsilon-transitive epsilon-connected ordinal Element of N1 = g . the epsilon-transitive epsilon-connected ordinal Element of N1 ) } is set
f " { b₁ where b₁ is Relation-like N1 -defined {{},1} -valued Function-like quasi_total Element of bool [:N1,{{},1}:] : ( b₁ in Y & b₁ . the epsilon-transitive epsilon-connected ordinal Element of N1 = g . the epsilon-transitive epsilon-connected ordinal Element of N1 ) } is set
MEET is set
f . MEET is set
f1 is Relation-like M -defined Y -valued Function-like quasi_total Element of bool [:M,Y:]
X1 is epsilon-transitive epsilon-connected ordinal Element of M
f1 . X1 is Element of Y
h1 is Relation-like Function-like set
dom h1 is set
rng h1 is set
Z is set
h1 . Z is set
g . Z is set
Z1 is epsilon-transitive epsilon-connected ordinal Element of N1
g . Z1 is finite countable Element of {{},1}
{ b₁ where b₁ is Relation-like N1 -defined {{},1} -valued Function-like quasi_total Element of bool [:N1,{{},1}:] : ( b₁ in Y & b₁ . Z1 = g . Z1 ) } is set
f " { b₁ where b₁ is Relation-like N1 -defined {{},1} -valued Function-like quasi_total Element of bool [:N1,{{},1}:] : ( b₁ in Y & b₁ . Z1 = g . Z1 ) } is set
f . X1 is set
c₁₆ is Relation-like N1 -defined {{},1} -valued Function-like quasi_total Element of bool [:N1,{{},1}:]
c₁₆ . Z1 is finite countable Element of {{},1}
dom g is Element of bool N1
bool N1 is non empty non trivial non finite set
{g} is non empty trivial functional finite 1 -element with_common_domain countable set
MEET is set
X1 is set
f . X1 is set
(dom f) /\ (meet { H₁(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal Element of N1 : b₁ in N1 } ) is set
dom (f | (meet { H₁(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal Element of N1 : b₁ in N1 } )) is set
card (meet { H₁(b₁) where b₁ is epsilon-transitive epsilon-connected ordinal Element of N1 : b₁ in N1 } ) is epsilon-transitive epsilon-connected ordinal cardinal set
card {g} is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal countable Element of omega
bool M is non empty non trivial non finite set
card M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set
MEET is Element of bool M
card MEET is epsilon-transitive epsilon-connected ordinal cardinal set
M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set