:: 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

F

{ b

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

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

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

card { H

card N1 is non empty epsilon-transitive epsilon-connected ordinal cardinal set

{ (b

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

{ b

( b

bool (bool M) is non empty set

{ b

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

{ b

( b

Y is Element of bool M

{ b

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

{ b

( b

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

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

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

F is set

{ b

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

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

(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

Y is set

{ b

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

g is Element of Y

f1 is set

N1 is set

f is Element of Y

g is non empty (M)

{ b

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

{ b

( b

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

{ b

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

(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

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

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

(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

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

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

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

N1 is set

f is Element of M

N . f is set

meet { (N . b

Y /\ (meet { (N . b

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

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

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

{ b

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

g . (B,X1) is Element of bool f

g . [B,X1] is set

{ b

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

union { (f1 . (MEET,b

M \ (union { (f1 . (MEET,b

card (M \ (union { (f1 . (MEET,b

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

[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

M \ (M) is Element of bool M

M /\ (M) is set

MEET is epsilon-transitive epsilon-connected ordinal Element of M

{ (f1 . (b

union { (f1 . (b

M \ (union { (f1 . (b

card (M \ (union { (f1 . (b

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

M \ { b

card (M \ { b

{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

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

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

(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

union { (Y . (b

{ H

{ H

{ H

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

card (M \ (union { (Y . (b

N1 is epsilon-transitive epsilon-connected ordinal Element of M

{ (Y . (b

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

card { H

card [:(M),{N1}:] is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set

{ (Y . b

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

card { (Y . b

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

[: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

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

card { H

card (M) is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set

card { (sup (N1 " {b

cf M is non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal set

sup { (sup (N1 " {b

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

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

(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

f " { b

g is epsilon-transitive epsilon-connected ordinal Element of N1

{ b

bool M is non empty non trivial non finite set

f " { b

{ b

f " { b

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

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

f " { b

X1 is finite countable Element of {{},1}

{ b

f " { b

g is Relation-like N1 -defined {{},1} -valued Function-like quasi_total Element of bool [:N1,{{},1}:]

{ b

f " { b

[:M,Y:] is set

bool [:M,Y:] is non empty set

{ H

meet { H

f | (meet { H

rng (f | (meet { H

f .: (meet { H

card { H

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

f " { b

g . the epsilon-transitive epsilon-connected ordinal Element of N1 is finite countable Element of {{},1}

{ b

f " { b

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

f " { b

f . X1 is set

c

c

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

dom (f | (meet { H

card (meet { H

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