Metamath Proof Explorer


Theorem ufilen

Description: Any infinite set has an ultrafilter on it whose elements are of the same cardinality as the set. Any such ultrafilter is necessarily free. (Contributed by Jeff Hankins, 7-Dec-2009) (Revised by Stefan O'Rear, 3-Aug-2015)

Ref Expression
Assertion ufilen ωXfUFilXxfxX

Proof

Step Hyp Ref Expression
1 reldom Rel
2 1 brrelex2i ωXXV
3 numth3 XVXdomcard
4 2 3 syl ωXXdomcard
5 csdfil XdomcardωXy𝒫X|XyXFilX
6 4 5 mpancom ωXy𝒫X|XyXFilX
7 filssufil y𝒫X|XyXFilXfUFilXy𝒫X|XyXf
8 6 7 syl ωXfUFilXy𝒫X|XyXf
9 elfvex fUFilXXV
10 9 ad2antlr ωXfUFilXxfXV
11 ufilfil fUFilXfFilX
12 filelss fFilXxfxX
13 11 12 sylan fUFilXxfxX
14 13 adantll ωXfUFilXxfxX
15 ssdomg XVxXxX
16 10 14 15 sylc ωXfUFilXxfxX
17 filfbas fFilXffBasX
18 11 17 syl fUFilXffBasX
19 18 adantl ωXfUFilXffBasX
20 fbncp ffBasXxf¬Xxf
21 19 20 sylan ωXfUFilXxf¬Xxf
22 difeq2 y=XxXy=XXx
23 22 breq1d y=XxXyXXXxX
24 difss XxX
25 elpw2g XVXx𝒫XXxX
26 24 25 mpbiri XVXx𝒫X
27 26 3ad2ant1 XVxXxXXx𝒫X
28 simp2 XVxXxXxX
29 dfss4 xXXXx=x
30 28 29 sylib XVxXxXXXx=x
31 simp3 XVxXxXxX
32 30 31 eqbrtrd XVxXxXXXxX
33 23 27 32 elrabd XVxXxXXxy𝒫X|XyX
34 ssel y𝒫X|XyXfXxy𝒫X|XyXXxf
35 33 34 syl5com XVxXxXy𝒫X|XyXfXxf
36 35 3expa XVxXxXy𝒫X|XyXfXxf
37 36 impancom XVxXy𝒫X|XyXfxXXxf
38 37 con3d XVxXy𝒫X|XyXf¬Xxf¬xX
39 38 impancom XVxX¬Xxfy𝒫X|XyXf¬xX
40 10 14 21 39 syl21anc ωXfUFilXxfy𝒫X|XyXf¬xX
41 bren2 xXxX¬xX
42 41 simplbi2 xX¬xXxX
43 16 40 42 sylsyld ωXfUFilXxfy𝒫X|XyXfxX
44 43 ralrimdva ωXfUFilXy𝒫X|XyXfxfxX
45 44 reximdva ωXfUFilXy𝒫X|XyXffUFilXxfxX
46 8 45 mpd ωXfUFilXxfxX