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
proof
defpred S1[ 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 S1[x,y]
proof
let x be object ; :: thesis: ( x in X implies ex y being object st S1[x,y] )
assume A5: x in X ; :: thesis: ex y being object st S1[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: S1[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;
consider f being Function such that
A6: ( dom f = X & ( for x being object st x in X holds
S1[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} } )
proof
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;
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} }
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 ) )
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 ) )
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 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;
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 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;
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
end;
hence card (FixedUltraFilters X) = card X by CARD_1:5; :: thesis: verum