Metamath Proof Explorer

Theorem cfinufil

Description: An ultrafilter is free iff it contains the Fréchet filter cfinfil as a subset. (Contributed by NM, 14-Jul-2008) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion cfinufil ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( ∩ 𝐹 = ∅ ↔ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ∈ Fin } ⊆ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋 )
2 ufilb ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ¬ 𝑥 ∈ 𝐹 ↔ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) )
3 2 adantr ⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ( 𝑋 ∖ 𝑥 ) ∈ Fin ) → ( ¬ 𝑥 ∈ 𝐹 ↔ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) )
4 ufilfil ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
5 4 adantr ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
6 filfinnfr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ∧ ( 𝑋 ∖ 𝑥 ) ∈ Fin ) → ∩ 𝐹 ≠ ∅ )
7 6 3exp ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 → ( ( 𝑋 ∖ 𝑥 ) ∈ Fin → ∩ 𝐹 ≠ ∅ ) ) )
8 7 com23 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ( 𝑋 ∖ 𝑥 ) ∈ Fin → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 → ∩ 𝐹 ≠ ∅ ) ) )
9 5 8 syl ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ( 𝑋 ∖ 𝑥 ) ∈ Fin → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 → ∩ 𝐹 ≠ ∅ ) ) )
10 9 imp ⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ( 𝑋 ∖ 𝑥 ) ∈ Fin ) → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 → ∩ 𝐹 ≠ ∅ ) )
11 3 10 sylbid ⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ( 𝑋 ∖ 𝑥 ) ∈ Fin ) → ( ¬ 𝑥 ∈ 𝐹 → ∩ 𝐹 ≠ ∅ ) )
12 11 necon4bd ⊢ ( ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) ∧ ( 𝑋 ∖ 𝑥 ) ∈ Fin ) → ( ∩ 𝐹 = ∅ → 𝑥 ∈ 𝐹 ) )
13 12 ex ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ( 𝑋 ∖ 𝑥 ) ∈ Fin → ( ∩ 𝐹 = ∅ → 𝑥 ∈ 𝐹 ) ) )
14 13 com23 ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ∩ 𝐹 = ∅ → ( ( 𝑋 ∖ 𝑥 ) ∈ Fin → 𝑥 ∈ 𝐹 ) ) )
15 1 14 sylan2 ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ( ∩ 𝐹 = ∅ → ( ( 𝑋 ∖ 𝑥 ) ∈ Fin → 𝑥 ∈ 𝐹 ) ) )
16 15 ralrimdva ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( ∩ 𝐹 = ∅ → ∀ 𝑥 ∈ 𝒫 𝑋 ( ( 𝑋 ∖ 𝑥 ) ∈ Fin → 𝑥 ∈ 𝐹 ) ) )
17 4 adantr ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑦 ∈ ∩ 𝐹 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
18 uffixsn ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑦 ∈ ∩ 𝐹 ) → { 𝑦 } ∈ 𝐹 )
19 filelss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ { 𝑦 } ∈ 𝐹 ) → { 𝑦 } ⊆ 𝑋 )
20 17 18 19 syl2anc ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑦 ∈ ∩ 𝐹 ) → { 𝑦 } ⊆ 𝑋 )
21 dfss4 ⊢ ( { 𝑦 } ⊆ 𝑋 ↔ ( 𝑋 ∖ ( 𝑋 ∖ { 𝑦 } ) ) = { 𝑦 } )
22 20 21 sylib ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑦 ∈ ∩ 𝐹 ) → ( 𝑋 ∖ ( 𝑋 ∖ { 𝑦 } ) ) = { 𝑦 } )
23 snfi ⊢ { 𝑦 } ∈ Fin
24 22 23 eqeltrdi ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑦 ∈ ∩ 𝐹 ) → ( 𝑋 ∖ ( 𝑋 ∖ { 𝑦 } ) ) ∈ Fin )
25 difss ⊢ ( 𝑋 ∖ { 𝑦 } ) ⊆ 𝑋
26 filtop ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐹 )
27 elpw2g ⊢ ( 𝑋 ∈ 𝐹 → ( ( 𝑋 ∖ { 𝑦 } ) ∈ 𝒫 𝑋 ↔ ( 𝑋 ∖ { 𝑦 } ) ⊆ 𝑋 ) )
28 17 26 27 3syl ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑦 ∈ ∩ 𝐹 ) → ( ( 𝑋 ∖ { 𝑦 } ) ∈ 𝒫 𝑋 ↔ ( 𝑋 ∖ { 𝑦 } ) ⊆ 𝑋 ) )
29 25 28 mpbiri ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑦 ∈ ∩ 𝐹 ) → ( 𝑋 ∖ { 𝑦 } ) ∈ 𝒫 𝑋 )
30 difeq2 ⊢ ( 𝑥 = ( 𝑋 ∖ { 𝑦 } ) → ( 𝑋 ∖ 𝑥 ) = ( 𝑋 ∖ ( 𝑋 ∖ { 𝑦 } ) ) )
31 30 eleq1d ⊢ ( 𝑥 = ( 𝑋 ∖ { 𝑦 } ) → ( ( 𝑋 ∖ 𝑥 ) ∈ Fin ↔ ( 𝑋 ∖ ( 𝑋 ∖ { 𝑦 } ) ) ∈ Fin ) )
32 eleq1 ⊢ ( 𝑥 = ( 𝑋 ∖ { 𝑦 } ) → ( 𝑥 ∈ 𝐹 ↔ ( 𝑋 ∖ { 𝑦 } ) ∈ 𝐹 ) )
33 31 32 imbi12d ⊢ ( 𝑥 = ( 𝑋 ∖ { 𝑦 } ) → ( ( ( 𝑋 ∖ 𝑥 ) ∈ Fin → 𝑥 ∈ 𝐹 ) ↔ ( ( 𝑋 ∖ ( 𝑋 ∖ { 𝑦 } ) ) ∈ Fin → ( 𝑋 ∖ { 𝑦 } ) ∈ 𝐹 ) ) )
34 33 rspcv ⊢ ( ( 𝑋 ∖ { 𝑦 } ) ∈ 𝒫 𝑋 → ( ∀ 𝑥 ∈ 𝒫 𝑋 ( ( 𝑋 ∖ 𝑥 ) ∈ Fin → 𝑥 ∈ 𝐹 ) → ( ( 𝑋 ∖ ( 𝑋 ∖ { 𝑦 } ) ) ∈ Fin → ( 𝑋 ∖ { 𝑦 } ) ∈ 𝐹 ) ) )
35 29 34 syl ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑦 ∈ ∩ 𝐹 ) → ( ∀ 𝑥 ∈ 𝒫 𝑋 ( ( 𝑋 ∖ 𝑥 ) ∈ Fin → 𝑥 ∈ 𝐹 ) → ( ( 𝑋 ∖ ( 𝑋 ∖ { 𝑦 } ) ) ∈ Fin → ( 𝑋 ∖ { 𝑦 } ) ∈ 𝐹 ) ) )
36 24 35 mpid ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑦 ∈ ∩ 𝐹 ) → ( ∀ 𝑥 ∈ 𝒫 𝑋 ( ( 𝑋 ∖ 𝑥 ) ∈ Fin → 𝑥 ∈ 𝐹 ) → ( 𝑋 ∖ { 𝑦 } ) ∈ 𝐹 ) )
37 ufilb ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ { 𝑦 } ⊆ 𝑋 ) → ( ¬ { 𝑦 } ∈ 𝐹 ↔ ( 𝑋 ∖ { 𝑦 } ) ∈ 𝐹 ) )
38 20 37 syldan ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑦 ∈ ∩ 𝐹 ) → ( ¬ { 𝑦 } ∈ 𝐹 ↔ ( 𝑋 ∖ { 𝑦 } ) ∈ 𝐹 ) )
39 18 pm2.24d ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑦 ∈ ∩ 𝐹 ) → ( ¬ { 𝑦 } ∈ 𝐹 → ¬ 𝑦 ∈ ∩ 𝐹 ) )
40 38 39 sylbird ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑦 ∈ ∩ 𝐹 ) → ( ( 𝑋 ∖ { 𝑦 } ) ∈ 𝐹 → ¬ 𝑦 ∈ ∩ 𝐹 ) )
41 36 40 syld ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑦 ∈ ∩ 𝐹 ) → ( ∀ 𝑥 ∈ 𝒫 𝑋 ( ( 𝑋 ∖ 𝑥 ) ∈ Fin → 𝑥 ∈ 𝐹 ) → ¬ 𝑦 ∈ ∩ 𝐹 ) )
42 41 impancom ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( ( 𝑋 ∖ 𝑥 ) ∈ Fin → 𝑥 ∈ 𝐹 ) ) → ( 𝑦 ∈ ∩ 𝐹 → ¬ 𝑦 ∈ ∩ 𝐹 ) )
43 42 pm2.01d ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( ( 𝑋 ∖ 𝑥 ) ∈ Fin → 𝑥 ∈ 𝐹 ) ) → ¬ 𝑦 ∈ ∩ 𝐹 )
44 43 eq0rdv ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( ( 𝑋 ∖ 𝑥 ) ∈ Fin → 𝑥 ∈ 𝐹 ) ) → ∩ 𝐹 = ∅ )
45 44 ex ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( ∀ 𝑥 ∈ 𝒫 𝑋 ( ( 𝑋 ∖ 𝑥 ) ∈ Fin → 𝑥 ∈ 𝐹 ) → ∩ 𝐹 = ∅ ) )
46 16 45 impbid ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( ∩ 𝐹 = ∅ ↔ ∀ 𝑥 ∈ 𝒫 𝑋 ( ( 𝑋 ∖ 𝑥 ) ∈ Fin → 𝑥 ∈ 𝐹 ) ) )
47 rabss ⊢ ( { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ∈ Fin } ⊆ 𝐹 ↔ ∀ 𝑥 ∈ 𝒫 𝑋 ( ( 𝑋 ∖ 𝑥 ) ∈ Fin → 𝑥 ∈ 𝐹 ) )
48 46 47 bitr4di ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( ∩ 𝐹 = ∅ ↔ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ∈ Fin } ⊆ 𝐹 ) )