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 X B A X ω A f UFil X A f f =

Proof

Step Hyp Ref Expression
1 ominf ¬ ω Fin
2 domfi A Fin ω A ω Fin
3 2 expcom ω A A Fin ω Fin
4 1 3 mtoi ω A ¬ A Fin
5 cfinfil X B A X ¬ A Fin x 𝒫 X | A x Fin Fil X
6 4 5 syl3an3 X B A X ω A x 𝒫 X | A x Fin Fil X
7 filssufil x 𝒫 X | A x Fin Fil X f UFil X x 𝒫 X | A x Fin f
8 6 7 syl X B A X ω A f UFil X x 𝒫 X | A x Fin f
9 difeq2 x = A A x = A A
10 difid A A =
11 9 10 eqtrdi x = A A x =
12 11 eleq1d x = A A x Fin Fin
13 elpw2g X B A 𝒫 X A X
14 13 biimpar X B A X A 𝒫 X
15 14 3adant3 X B A X ω A A 𝒫 X
16 0fin Fin
17 16 a1i X B A X ω A Fin
18 12 15 17 elrabd X B A X ω A A x 𝒫 X | A x Fin
19 ssel x 𝒫 X | A x Fin f A x 𝒫 X | A x Fin A f
20 18 19 syl5com X B A X ω A x 𝒫 X | A x Fin f A f
21 intss x 𝒫 X | A x Fin f f x 𝒫 X | A x Fin
22 neldifsn ¬ y A y
23 elinti y x 𝒫 X | A x Fin A y x 𝒫 X | A x Fin y A y
24 22 23 mtoi y x 𝒫 X | A x Fin ¬ A y x 𝒫 X | A x Fin
25 difeq2 x = A y A x = A A y
26 25 eleq1d x = A y A x Fin A A y Fin
27 simp2 X B A X ω A A X
28 27 ssdifssd X B A X ω A A y X
29 elpw2g X B A y 𝒫 X A y X
30 29 3ad2ant1 X B A X ω A A y 𝒫 X A y X
31 28 30 mpbird X B A X ω A A y 𝒫 X
32 snfi y Fin
33 eldif x A A y x A ¬ x A y
34 eldif x A y x A ¬ x y
35 34 notbii ¬ x A y ¬ x A ¬ x y
36 iman x A x y ¬ x A ¬ x y
37 35 36 bitr4i ¬ x A y x A x y
38 37 anbi2i x A ¬ x A y x A x A x y
39 33 38 bitri x A A y x A x A x y
40 pm3.35 x A x A x y x y
41 39 40 sylbi x A A y x y
42 41 ssriv A A y y
43 ssfi y Fin A A y y A A y Fin
44 32 42 43 mp2an A A y Fin
45 44 a1i X B A X ω A A A y Fin
46 26 31 45 elrabd X B A X ω A A y x 𝒫 X | A x Fin
47 24 46 nsyl3 X B A X ω A ¬ y x 𝒫 X | A x Fin
48 47 eq0rdv X B A X ω A x 𝒫 X | A x Fin =
49 48 sseq2d X B A X ω A f x 𝒫 X | A x Fin f
50 21 49 syl5ib X B A X ω A x 𝒫 X | A x Fin f f
51 ss0 f f =
52 50 51 syl6 X B A X ω A x 𝒫 X | A x Fin f f =
53 20 52 jcad X B A X ω A x 𝒫 X | A x Fin f A f f =
54 53 reximdv X B A X ω A f UFil X x 𝒫 X | A x Fin f f UFil X A f f =
55 8 54 mpd X B A X ω A f UFil X A f f =