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

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 ( ω ≼ 𝑋 → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ∀ 𝑥 ∈ 𝑓 𝑥 ≈ 𝑋 )

Proof

Step Hyp Ref Expression
1 reldom ⊢ Rel ≼
2 1 brrelex2i ⊢ ( ω ≼ 𝑋 → 𝑋 ∈ V )
3 numth3 ⊢ ( 𝑋 ∈ V → 𝑋 ∈ dom card )
4 2 3 syl ⊢ ( ω ≼ 𝑋 → 𝑋 ∈ dom card )
5 csdfil ⊢ ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) → { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 } ∈ ( Fil ‘ 𝑋 ) )
6 4 5 mpancom ⊢ ( ω ≼ 𝑋 → { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 } ∈ ( Fil ‘ 𝑋 ) )
7 filssufil ⊢ ( { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 } ∈ ( Fil ‘ 𝑋 ) → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 } ⊆ 𝑓 )
8 6 7 syl ⊢ ( ω ≼ 𝑋 → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 } ⊆ 𝑓 )
9 elfvex ⊢ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) → 𝑋 ∈ V )
10 9 ad2antlr ⊢ ( ( ( ω ≼ 𝑋 ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑓 ) → 𝑋 ∈ V )
11 ufilfil ⊢ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) → 𝑓 ∈ ( Fil ‘ 𝑋 ) )
12 filelss ⊢ ( ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑓 ) → 𝑥 ⊆ 𝑋 )
13 11 12 sylan ⊢ ( ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑓 ) → 𝑥 ⊆ 𝑋 )
14 13 adantll ⊢ ( ( ( ω ≼ 𝑋 ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑓 ) → 𝑥 ⊆ 𝑋 )
15 ssdomg ⊢ ( 𝑋 ∈ V → ( 𝑥 ⊆ 𝑋 → 𝑥 ≼ 𝑋 ) )
16 10 14 15 sylc ⊢ ( ( ( ω ≼ 𝑋 ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑓 ) → 𝑥 ≼ 𝑋 )
17 filfbas ⊢ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) → 𝑓 ∈ ( fBas ‘ 𝑋 ) )
18 11 17 syl ⊢ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) → 𝑓 ∈ ( fBas ‘ 𝑋 ) )
19 18 adantl ⊢ ( ( ω ≼ 𝑋 ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) → 𝑓 ∈ ( fBas ‘ 𝑋 ) )
20 fbncp ⊢ ( ( 𝑓 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑓 ) → ¬ ( 𝑋 ∖ 𝑥 ) ∈ 𝑓 )
21 19 20 sylan ⊢ ( ( ( ω ≼ 𝑋 ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑓 ) → ¬ ( 𝑋 ∖ 𝑥 ) ∈ 𝑓 )
22 difeq2 ⊢ ( 𝑦 = ( 𝑋 ∖ 𝑥 ) → ( 𝑋 ∖ 𝑦 ) = ( 𝑋 ∖ ( 𝑋 ∖ 𝑥 ) ) )
23 22 breq1d ⊢ ( 𝑦 = ( 𝑋 ∖ 𝑥 ) → ( ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 ↔ ( 𝑋 ∖ ( 𝑋 ∖ 𝑥 ) ) ≺ 𝑋 ) )
24 difss ⊢ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑋
25 elpw2g ⊢ ( 𝑋 ∈ V → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝒫 𝑋 ↔ ( 𝑋 ∖ 𝑥 ) ⊆ 𝑋 ) )
26 24 25 mpbiri ⊢ ( 𝑋 ∈ V → ( 𝑋 ∖ 𝑥 ) ∈ 𝒫 𝑋 )
27 26 3ad2ant1 ⊢ ( ( 𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋 ) → ( 𝑋 ∖ 𝑥 ) ∈ 𝒫 𝑋 )
28 simp2 ⊢ ( ( 𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋 ) → 𝑥 ⊆ 𝑋 )
29 dfss4 ⊢ ( 𝑥 ⊆ 𝑋 ↔ ( 𝑋 ∖ ( 𝑋 ∖ 𝑥 ) ) = 𝑥 )
30 28 29 sylib ⊢ ( ( 𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋 ) → ( 𝑋 ∖ ( 𝑋 ∖ 𝑥 ) ) = 𝑥 )
31 simp3 ⊢ ( ( 𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋 ) → 𝑥 ≺ 𝑋 )
32 30 31 eqbrtrd ⊢ ( ( 𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋 ) → ( 𝑋 ∖ ( 𝑋 ∖ 𝑥 ) ) ≺ 𝑋 )
33 23 27 32 elrabd ⊢ ( ( 𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋 ) → ( 𝑋 ∖ 𝑥 ) ∈ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 } )
34 ssel ⊢ ( { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 } ⊆ 𝑓 → ( ( 𝑋 ∖ 𝑥 ) ∈ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 } → ( 𝑋 ∖ 𝑥 ) ∈ 𝑓 ) )
35 33 34 syl5com ⊢ ( ( 𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ∧ 𝑥 ≺ 𝑋 ) → ( { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 } ⊆ 𝑓 → ( 𝑋 ∖ 𝑥 ) ∈ 𝑓 ) )
36 35 3expa ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ) ∧ 𝑥 ≺ 𝑋 ) → ( { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 } ⊆ 𝑓 → ( 𝑋 ∖ 𝑥 ) ∈ 𝑓 ) )
37 36 impancom ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ) ∧ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 } ⊆ 𝑓 ) → ( 𝑥 ≺ 𝑋 → ( 𝑋 ∖ 𝑥 ) ∈ 𝑓 ) )
38 37 con3d ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ) ∧ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 } ⊆ 𝑓 ) → ( ¬ ( 𝑋 ∖ 𝑥 ) ∈ 𝑓 → ¬ 𝑥 ≺ 𝑋 ) )
39 38 impancom ⊢ ( ( ( 𝑋 ∈ V ∧ 𝑥 ⊆ 𝑋 ) ∧ ¬ ( 𝑋 ∖ 𝑥 ) ∈ 𝑓 ) → ( { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 } ⊆ 𝑓 → ¬ 𝑥 ≺ 𝑋 ) )
40 10 14 21 39 syl21anc ⊢ ( ( ( ω ≼ 𝑋 ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑓 ) → ( { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 } ⊆ 𝑓 → ¬ 𝑥 ≺ 𝑋 ) )
41 bren2 ⊢ ( 𝑥 ≈ 𝑋 ↔ ( 𝑥 ≼ 𝑋 ∧ ¬ 𝑥 ≺ 𝑋 ) )
42 41 simplbi2 ⊢ ( 𝑥 ≼ 𝑋 → ( ¬ 𝑥 ≺ 𝑋 → 𝑥 ≈ 𝑋 ) )
43 16 40 42 sylsyld ⊢ ( ( ( ω ≼ 𝑋 ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑓 ) → ( { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 } ⊆ 𝑓 → 𝑥 ≈ 𝑋 ) )
44 43 ralrimdva ⊢ ( ( ω ≼ 𝑋 ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) → ( { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 } ⊆ 𝑓 → ∀ 𝑥 ∈ 𝑓 𝑥 ≈ 𝑋 ) )
45 44 reximdva ⊢ ( ω ≼ 𝑋 → ( ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑦 ) ≺ 𝑋 } ⊆ 𝑓 → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ∀ 𝑥 ∈ 𝑓 𝑥 ≈ 𝑋 ) )
46 8 45 mpd ⊢ ( ω ≼ 𝑋 → ∃ 𝑓 ∈ ( UFil ‘ 𝑋 ) ∀ 𝑥 ∈ 𝑓 𝑥 ≈ 𝑋 )