This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐴 ∈ 𝑓 ∧ ∩ 𝑓 = ∅ ) )

Proof

Step Hyp Ref Expression
1 ominf ⊢ ¬ ω ∈ Fin
2 domfi ⊢ ( ( 𝐴 ∈ Fin ∧ ω ≼ 𝐴 ) → ω ∈ Fin )
3 2 expcom ⊢ ( ω ≼ 𝐴 → ( 𝐴 ∈ Fin → ω ∈ Fin ) )
4 1 3 mtoi ⊢ ( ω ≼ 𝐴 → ¬ 𝐴 ∈ Fin )
5 cfinfil ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin ) → { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ∈ ( Fil ‘ 𝑋 ) )
6 4 5 syl3an3 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ∈ ( Fil ‘ 𝑋 ) )
7 filssufil ⊢ ( { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ∈ ( Fil ‘ 𝑋 ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ⊆ 𝑓 )
8 6 7 syl ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ⊆ 𝑓 )
9 difeq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ 𝐴 ) )
10 difid ⊢ ( 𝐴 ∖ 𝐴 ) = ∅
11 9 10 eqtrdi ⊢ ( 𝑥 = 𝐴 → ( 𝐴 ∖ 𝑥 ) = ∅ )
12 11 eleq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ↔ ∅ ∈ Fin ) )
13 elpw2g ⊢ ( 𝑋 ∈ 𝐵 → ( 𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋 ) )
14 13 biimpar ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ∈ 𝒫 𝑋 )
15 14 3adant3 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → 𝐴 ∈ 𝒫 𝑋 )
16 0fi ⊢ ∅ ∈ Fin
17 16 a1i ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ∅ ∈ Fin )
18 12 15 17 elrabd ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → 𝐴 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } )
19 ssel ⊢ ( { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ⊆ 𝑓 → ( 𝐴 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } → 𝐴 ∈ 𝑓 ) )
20 18 19 syl5com ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ( { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ⊆ 𝑓 → 𝐴 ∈ 𝑓 ) )
21 intss ⊢ ( { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ⊆ 𝑓 → ∩ 𝑓 ⊆ ∩ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } )
22 neldifsn ⊢ ¬ 𝑦 ∈ ( 𝐴 ∖ { 𝑦 } )
23 elinti ⊢ ( 𝑦 ∈ ∩ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } → ( ( 𝐴 ∖ { 𝑦 } ) ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } → 𝑦 ∈ ( 𝐴 ∖ { 𝑦 } ) ) )
24 22 23 mtoi ⊢ ( 𝑦 ∈ ∩ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } → ¬ ( 𝐴 ∖ { 𝑦 } ) ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } )
25 difeq2 ⊢ ( 𝑥 = ( 𝐴 ∖ { 𝑦 } ) → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) )
26 25 eleq1d ⊢ ( 𝑥 = ( 𝐴 ∖ { 𝑦 } ) → ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ↔ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ∈ Fin ) )
27 simp2 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → 𝐴 ⊆ 𝑋 )
28 27 ssdifssd ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ( 𝐴 ∖ { 𝑦 } ) ⊆ 𝑋 )
29 elpw2g ⊢ ( 𝑋 ∈ 𝐵 → ( ( 𝐴 ∖ { 𝑦 } ) ∈ 𝒫 𝑋 ↔ ( 𝐴 ∖ { 𝑦 } ) ⊆ 𝑋 ) )
30 29 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ( ( 𝐴 ∖ { 𝑦 } ) ∈ 𝒫 𝑋 ↔ ( 𝐴 ∖ { 𝑦 } ) ⊆ 𝑋 ) )
31 28 30 mpbird ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ( 𝐴 ∖ { 𝑦 } ) ∈ 𝒫 𝑋 )
32 snfi ⊢ { 𝑦 } ∈ Fin
33 eldif ⊢ ( 𝑥 ∈ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ( 𝐴 ∖ { 𝑦 } ) ) )
34 eldif ⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 𝑦 } ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ { 𝑦 } ) )
35 34 notbii ⊢ ( ¬ 𝑥 ∈ ( 𝐴 ∖ { 𝑦 } ) ↔ ¬ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ { 𝑦 } ) )
36 iman ⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ { 𝑦 } ) ↔ ¬ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ { 𝑦 } ) )
37 35 36 bitr4i ⊢ ( ¬ 𝑥 ∈ ( 𝐴 ∖ { 𝑦 } ) ↔ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ { 𝑦 } ) )
38 37 anbi2i ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ( 𝐴 ∖ { 𝑦 } ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ { 𝑦 } ) ) )
39 33 38 bitri ⊢ ( 𝑥 ∈ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ { 𝑦 } ) ) )
40 pm3.35 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ { 𝑦 } ) ) → 𝑥 ∈ { 𝑦 } )
41 39 40 sylbi ⊢ ( 𝑥 ∈ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) → 𝑥 ∈ { 𝑦 } )
42 41 ssriv ⊢ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ⊆ { 𝑦 }
43 ssfi ⊢ ( ( { 𝑦 } ∈ Fin ∧ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ⊆ { 𝑦 } ) → ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ∈ Fin )
44 32 42 43 mp2an ⊢ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ∈ Fin
45 44 a1i ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ( 𝐴 ∖ ( 𝐴 ∖ { 𝑦 } ) ) ∈ Fin )
46 26 31 45 elrabd ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ( 𝐴 ∖ { 𝑦 } ) ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } )
47 24 46 nsyl3 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ¬ 𝑦 ∈ ∩ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } )
48 47 eq0rdv ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ∩ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } = ∅ )
49 48 sseq2d ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ( ∩ 𝑓 ⊆ ∩ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ↔ ∩ 𝑓 ⊆ ∅ ) )
50 21 49 imbitrid ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ( { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ⊆ 𝑓 → ∩ 𝑓 ⊆ ∅ ) )
51 ss0 ⊢ ( ∩ 𝑓 ⊆ ∅ → ∩ 𝑓 = ∅ )
52 50 51 syl6 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ( { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ⊆ 𝑓 → ∩ 𝑓 = ∅ ) )
53 20 52 jcad ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ( { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ⊆ 𝑓 → ( 𝐴 ∈ 𝑓 ∧ ∩ 𝑓 = ∅ ) ) )
54 53 reximdv ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ( ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∖ 𝑥 ) ∈ Fin } ⊆ 𝑓 → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐴 ∈ 𝑓 ∧ ∩ 𝑓 = ∅ ) ) )
55 8 54 mpd ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴 ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐴 ∈ 𝑓 ∧ ∩ 𝑓 = ∅ ) )