let X be set ; :: thesis: card (FixedUltraFilters X) = card X

set FUF = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } ;

A1: BoolePoset X = InclPoset (bool X) by YELLOW_1:4;

A2: InclPoset (bool X) = RelStr(# (bool X),(RelIncl (bool X)) #) by YELLOW_1:def 1;

then A3: the carrier of (BoolePoset X) = bool X by YELLOW_1:4;

X, { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } are_equipotent

set FUF = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } ;

A1: BoolePoset X = InclPoset (bool X) by YELLOW_1:4;

A2: InclPoset (bool X) = RelStr(# (bool X),(RelIncl (bool X)) #) by YELLOW_1:def 1;

then A3: the carrier of (BoolePoset X) = bool X by YELLOW_1:4;

X, { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } are_equipotent

proof

hence
card (FixedUltraFilters X) = card X
by CARD_1:5; :: thesis: verum
defpred S_{1}[ object , object ] means ex y being Element of X ex x being Element of (BoolePoset X) st

( x = {y} & $1 = y & $2 = uparrow x );

A4: for x being object st x in X holds

ex y being object st S_{1}[x,y]

A6: ( dom f = X & ( for x being object st x in X holds

S_{1}[x,f . x] ) )
from CLASSES1:sch 1(A4);

take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = X & rng f = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } )

thus f is one-to-one :: thesis: ( dom f = X & rng f = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } )

end;( x = {y} & $1 = y & $2 = uparrow x );

A4: for x being object st x in X holds

ex y being object st S

proof

consider f being Function such that
let x be object ; :: thesis: ( x in X implies ex y being object st S_{1}[x,y] )

assume A5: x in X ; :: thesis: ex y being object st S_{1}[x,y]

then reconsider x9 = x as Element of X ;

reconsider bx = {x} as Element of (BoolePoset X) by A1, A2, A5, ZFMISC_1:31;

take uparrow bx ; :: thesis: S_{1}[x, uparrow bx]

take x9 ; :: thesis: ex x being Element of (BoolePoset X) st

( x = {x9} & x = x9 & uparrow bx = uparrow x )

take bx ; :: thesis: ( bx = {x9} & x = x9 & uparrow bx = uparrow bx )

thus ( bx = {x9} & x = x9 & uparrow bx = uparrow bx ) ; :: thesis: verum

end;assume A5: x in X ; :: thesis: ex y being object st S

then reconsider x9 = x as Element of X ;

reconsider bx = {x} as Element of (BoolePoset X) by A1, A2, A5, ZFMISC_1:31;

take uparrow bx ; :: thesis: S

take x9 ; :: thesis: ex x being Element of (BoolePoset X) st

( x = {x9} & x = x9 & uparrow bx = uparrow x )

take bx ; :: thesis: ( bx = {x9} & x = x9 & uparrow bx = uparrow bx )

thus ( bx = {x9} & x = x9 & uparrow bx = uparrow bx ) ; :: thesis: verum

A6: ( dom f = X & ( for x being object st x in X holds

S

take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = X & rng f = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } )

thus f is one-to-one :: thesis: ( dom f = X & rng f = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } )

proof

thus
dom f = X
by A6; :: thesis: rng f = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} }
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )

assume that

A7: x1 in dom f and

A8: x2 in dom f and

A9: f . x1 = f . x2 ; :: thesis: x1 = x2

consider x29 being Element of X, bx2 being Element of (BoolePoset X) such that

A10: ( bx2 = {x29} & x2 = x29 ) and

A11: f . x2 = uparrow bx2 by A6, A8;

consider x19 being Element of X, bx1 being Element of (BoolePoset X) such that

A12: ( bx1 = {x19} & x1 = x19 ) and

A13: f . x1 = uparrow bx1 by A6, A7;

bx1 = bx2 by A9, A13, A11, WAYBEL_0:20;

hence x1 = x2 by A12, A10, ZFMISC_1:3; :: thesis: verum

end;assume that

A7: x1 in dom f and

A8: x2 in dom f and

A9: f . x1 = f . x2 ; :: thesis: x1 = x2

consider x29 being Element of X, bx2 being Element of (BoolePoset X) such that

A10: ( bx2 = {x29} & x2 = x29 ) and

A11: f . x2 = uparrow bx2 by A6, A8;

consider x19 being Element of X, bx1 being Element of (BoolePoset X) such that

A12: ( bx1 = {x19} & x1 = x19 ) and

A13: f . x1 = uparrow bx1 by A6, A7;

bx1 = bx2 by A9, A13, A11, WAYBEL_0:20;

hence x1 = x2 by A12, A10, ZFMISC_1:3; :: thesis: verum

now :: thesis: for z being object holds

( ( z in rng f implies z in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } ) & ( z in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } implies z in rng f ) )

hence
rng f = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} }
by TARSKI:2; :: thesis: verum( ( z in rng f implies z in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } ) & ( z in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } implies z in rng f ) )

let z be object ; :: thesis: ( ( z in rng f implies z in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } ) & ( z in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } implies z in rng f ) )

then consider bx being Element of (BoolePoset X) such that

A16: z = uparrow bx and

A17: ex y being Element of X st bx = {y} ;

consider y being Element of X such that

A18: bx = {y} by A17;

A19: y in X by A3, A18, ZFMISC_1:31;

then ex x19 being Element of X ex bx1 being Element of (BoolePoset X) st

( bx1 = {x19} & y = x19 & f . y = uparrow bx1 ) by A6;

hence z in rng f by A6, A16, A18, A19, FUNCT_1:def 3; :: thesis: verum

end;hereby :: thesis: ( z in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } implies z in rng f )

assume
z in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} }
; :: thesis: z in rng fassume
z in rng f
; :: thesis: z in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} }

then consider x1 being object such that

A14: x1 in dom f and

A15: z = f . x1 by FUNCT_1:def 3;

ex x19 being Element of X ex bx1 being Element of (BoolePoset X) st

( bx1 = {x19} & x1 = x19 & f . x1 = uparrow bx1 ) by A6, A14;

hence z in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } by A15; :: thesis: verum

end;then consider x1 being object such that

A14: x1 in dom f and

A15: z = f . x1 by FUNCT_1:def 3;

ex x19 being Element of X ex bx1 being Element of (BoolePoset X) st

( bx1 = {x19} & x1 = x19 & f . x1 = uparrow bx1 ) by A6, A14;

hence z in { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } by A15; :: thesis: verum

then consider bx being Element of (BoolePoset X) such that

A16: z = uparrow bx and

A17: ex y being Element of X st bx = {y} ;

consider y being Element of X such that

A18: bx = {y} by A17;

A19: y in X by A3, A18, ZFMISC_1:31;

then ex x19 being Element of X ex bx1 being Element of (BoolePoset X) st

( bx1 = {x19} & y = x19 & f . y = uparrow bx1 ) by A6;

hence z in rng f by A6, A16, A18, A19, FUNCT_1:def 3; :: thesis: verum