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

Metamath Proof Explorer

Theorem uffixsn

Description: The singleton of the generator of a fixed ultrafilter is in the filter. (Contributed by Mario Carneiro, 24-May-2015) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion uffixsn ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → { 𝐴 } ∈ 𝐹 )

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ ( 𝑥 = { 𝐴 } → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ { 𝐴 } ) )
2 ufilfil ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
3 filn0 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ≠ ∅ )
4 intssuni ⊢ ( 𝐹 ≠ ∅ → ∩ 𝐹 ⊆ ∪ 𝐹 )
5 2 3 4 3syl ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ∩ 𝐹 ⊆ ∪ 𝐹 )
6 filunibas ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∪ 𝐹 = 𝑋 )
7 2 6 syl ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ∪ 𝐹 = 𝑋 )
8 5 7 sseqtrd ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ∩ 𝐹 ⊆ 𝑋 )
9 8 sselda ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → 𝐴 ∈ 𝑋 )
10 9 snssd ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → { 𝐴 } ⊆ 𝑋 )
11 snex ⊢ { 𝐴 } ∈ V
12 11 elpw ⊢ ( { 𝐴 } ∈ 𝒫 𝑋 ↔ { 𝐴 } ⊆ 𝑋 )
13 10 12 sylibr ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → { 𝐴 } ∈ 𝒫 𝑋 )
14 snidg ⊢ ( 𝐴 ∈ ∩ 𝐹 → 𝐴 ∈ { 𝐴 } )
15 14 adantl ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → 𝐴 ∈ { 𝐴 } )
16 1 13 15 elrabd ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → { 𝐴 } ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } )
17 uffixfr ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝐴 ∈ ∩ 𝐹 ↔ 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } ) )
18 17 biimpa ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → 𝐹 = { 𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥 } )
19 16 18 eleqtrrd ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝐴 ∈ ∩ 𝐹 ) → { 𝐴 } ∈ 𝐹 )