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

Metamath Proof Explorer

Theorem uffixfr

Description: An ultrafilter is either fixed or free. A fixed ultrafilter is called principal (generated by a single element A ), and a free ultrafilter is called nonprincipal (having empty intersection). Note that examples of free ultrafilters cannot be defined in ZFC without some form of global choice. (Contributed by Jeff Hankins, 4-Dec-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion uffixfr ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝐴 ∈ ∩ 𝐹 ↔ 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → 𝐹 ∈ ( UFil ‘ 𝑋 ) )
2 ufilfil ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
3 filtop ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐹 )
4 2 3 syl ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → 𝑋 ∈ 𝐹 )
5 filn0 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ≠ ∅ )
6 intssuni ⊢ ( 𝐹 ≠ ∅ → ∩ 𝐹 ⊆ ∪ 𝐹 )
7 2 5 6 3syl ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ∩ 𝐹 ⊆ ∪ 𝐹 )
8 filunibas ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∪ 𝐹 = 𝑋 )
9 2 8 syl ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ∪ 𝐹 = 𝑋 )
10 7 9 sseqtrd ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ∩ 𝐹 ⊆ 𝑋 )
11 10 sselda ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → 𝐴 ∈ 𝑋 )
12 uffix ⊢ ( ( 𝑋 ∈ 𝐹 ∧ 𝐴 ∈ 𝑋 ) → ( { { 𝐴 } } ∈ ( fBas ‘ 𝑋 ) ∧ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } = ( 𝑋 filGen { { 𝐴 } } ) ) )
13 4 11 12 syl2an2r ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → ( { { 𝐴 } } ∈ ( fBas ‘ 𝑋 ) ∧ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } = ( 𝑋 filGen { { 𝐴 } } ) ) )
14 13 simprd ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } = ( 𝑋 filGen { { 𝐴 } } ) )
15 13 simpld ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → { { 𝐴 } } ∈ ( fBas ‘ 𝑋 ) )
16 fgcl ⊢ ( { { 𝐴 } } ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen { { 𝐴 } } ) ∈ ( Fil ‘ 𝑋 ) )
17 15 16 syl ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → ( 𝑋 filGen { { 𝐴 } } ) ∈ ( Fil ‘ 𝑋 ) )
18 14 17 eqeltrd ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ∈ ( Fil ‘ 𝑋 ) )
19 2 adantr ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
20 filsspw ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ⊆ 𝒫 𝑋 )
21 19 20 syl ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → 𝐹 ⊆ 𝒫 𝑋 )
22 elintg ⊢ ( 𝐴 ∈ ∩ 𝐹 → ( 𝐴 ∈ ∩ 𝐹 ↔ ∀ 𝑥 ∈ 𝐹 𝐴 ∈ 𝑥 ) )
23 22 ibi ⊢ ( 𝐴 ∈ ∩ 𝐹 → ∀ 𝑥 ∈ 𝐹 𝐴 ∈ 𝑥 )
24 23 adantl ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → ∀ 𝑥 ∈ 𝐹 𝐴 ∈ 𝑥 )
25 ssrab ⊢ ( 𝐹 ⊆ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ↔ ( 𝐹 ⊆ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ 𝐹 𝐴 ∈ 𝑥 ) )
26 21 24 25 sylanbrc ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → 𝐹 ⊆ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } )
27 ufilmax ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 ⊆ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) → 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } )
28 1 18 26 27 syl3anc ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } )
29 eqimss ⊢ ( 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } → 𝐹 ⊆ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } )
30 29 adantl ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) → 𝐹 ⊆ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } )
31 25 simprbi ⊢ ( 𝐹 ⊆ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } → ∀ 𝑥 ∈ 𝐹 𝐴 ∈ 𝑥 )
32 30 31 syl ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) → ∀ 𝑥 ∈ 𝐹 𝐴 ∈ 𝑥 )
33 eleq2 ⊢ ( 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } → ( 𝑋 ∈ 𝐹 ↔ 𝑋 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) )
34 33 biimpac ⊢ ( ( 𝑋 ∈ 𝐹 ∧ 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) → 𝑋 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } )
35 4 34 sylan ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) → 𝑋 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } )
36 eleq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑋 ) )
37 36 elrab ⊢ ( 𝑋 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ↔ ( 𝑋 ∈ 𝒫 𝑋 ∧ 𝐴 ∈ 𝑋 ) )
38 37 simprbi ⊢ ( 𝑋 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } → 𝐴 ∈ 𝑋 )
39 elintg ⊢ ( 𝐴 ∈ 𝑋 → ( 𝐴 ∈ ∩ 𝐹 ↔ ∀ 𝑥 ∈ 𝐹 𝐴 ∈ 𝑥 ) )
40 35 38 39 3syl ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) → ( 𝐴 ∈ ∩ 𝐹 ↔ ∀ 𝑥 ∈ 𝐹 𝐴 ∈ 𝑥 ) )
41 32 40 mpbird ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) → 𝐴 ∈ ∩ 𝐹 )
42 28 41 impbida ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝐴 ∈ ∩ 𝐹 ↔ 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) )