Metamath Proof Explorer


Theorem ufinffr

Description: An infinite subset is contained in a free ultrafilter. (Contributed by Jeff Hankins, 6-Dec-2009) (Revised by Mario Carneiro, 4-Dec-2013)

Ref Expression
Assertion ufinffr XBAXωAfUFilXAff=

Proof

Step Hyp Ref Expression
1 ominf ¬ωFin
2 domfi AFinωAωFin
3 2 expcom ωAAFinωFin
4 1 3 mtoi ωA¬AFin
5 cfinfil XBAX¬AFinx𝒫X|AxFinFilX
6 4 5 syl3an3 XBAXωAx𝒫X|AxFinFilX
7 filssufil x𝒫X|AxFinFilXfUFilXx𝒫X|AxFinf
8 6 7 syl XBAXωAfUFilXx𝒫X|AxFinf
9 difeq2 x=AAx=AA
10 difid AA=
11 9 10 eqtrdi x=AAx=
12 11 eleq1d x=AAxFinFin
13 elpw2g XBA𝒫XAX
14 13 biimpar XBAXA𝒫X
15 14 3adant3 XBAXωAA𝒫X
16 0fin Fin
17 16 a1i XBAXωAFin
18 12 15 17 elrabd XBAXωAAx𝒫X|AxFin
19 ssel x𝒫X|AxFinfAx𝒫X|AxFinAf
20 18 19 syl5com XBAXωAx𝒫X|AxFinfAf
21 intss x𝒫X|AxFinffx𝒫X|AxFin
22 neldifsn ¬yAy
23 elinti yx𝒫X|AxFinAyx𝒫X|AxFinyAy
24 22 23 mtoi yx𝒫X|AxFin¬Ayx𝒫X|AxFin
25 difeq2 x=AyAx=AAy
26 25 eleq1d x=AyAxFinAAyFin
27 simp2 XBAXωAAX
28 27 ssdifssd XBAXωAAyX
29 elpw2g XBAy𝒫XAyX
30 29 3ad2ant1 XBAXωAAy𝒫XAyX
31 28 30 mpbird XBAXωAAy𝒫X
32 snfi yFin
33 eldif xAAyxA¬xAy
34 eldif xAyxA¬xy
35 34 notbii ¬xAy¬xA¬xy
36 iman xAxy¬xA¬xy
37 35 36 bitr4i ¬xAyxAxy
38 37 anbi2i xA¬xAyxAxAxy
39 33 38 bitri xAAyxAxAxy
40 pm3.35 xAxAxyxy
41 39 40 sylbi xAAyxy
42 41 ssriv AAyy
43 ssfi yFinAAyyAAyFin
44 32 42 43 mp2an AAyFin
45 44 a1i XBAXωAAAyFin
46 26 31 45 elrabd XBAXωAAyx𝒫X|AxFin
47 24 46 nsyl3 XBAXωA¬yx𝒫X|AxFin
48 47 eq0rdv XBAXωAx𝒫X|AxFin=
49 48 sseq2d XBAXωAfx𝒫X|AxFinf
50 21 49 syl5ib XBAXωAx𝒫X|AxFinff
51 ss0 ff=
52 50 51 syl6 XBAXωAx𝒫X|AxFinff=
53 20 52 jcad XBAXωAx𝒫X|AxFinfAff=
54 53 reximdv XBAXωAfUFilXx𝒫X|AxFinffUFilXAff=
55 8 54 mpd XBAXωAfUFilXAff=