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 ⊢ F ∈ UFil ⁡ X ∧ A ∈ ⋂ F → A ∈ F

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ x = A → A ∈ x ↔ A ∈ A
2 ufilfil ⊢ F ∈ UFil ⁡ X → F ∈ Fil ⁡ X
3 filn0 ⊢ F ∈ Fil ⁡ X → F ≠ ∅
4 intssuni ⊢ F ≠ ∅ → ⋂ F ⊆ ⋃ F
5 2 3 4 3syl ⊢ F ∈ UFil ⁡ X → ⋂ F ⊆ ⋃ F
6 filunibas ⊢ F ∈ Fil ⁡ X → ⋃ F = X
7 2 6 syl ⊢ F ∈ UFil ⁡ X → ⋃ F = X
8 5 7 sseqtrd ⊢ F ∈ UFil ⁡ X → ⋂ F ⊆ X
9 8 sselda ⊢ F ∈ UFil ⁡ X ∧ A ∈ ⋂ F → A ∈ X
10 9 snssd ⊢ F ∈ UFil ⁡ X ∧ A ∈ ⋂ F → A ⊆ X
11 snex ⊢ A ∈ V
12 11 elpw ⊢ A ∈ 𝒫 X ↔ A ⊆ X
13 10 12 sylibr ⊢ F ∈ UFil ⁡ X ∧ A ∈ ⋂ F → A ∈ 𝒫 X
14 snidg ⊢ A ∈ ⋂ F → A ∈ A
15 14 adantl ⊢ F ∈ UFil ⁡ X ∧ A ∈ ⋂ F → A ∈ A
16 1 13 15 elrabd ⊢ F ∈ UFil ⁡ X ∧ A ∈ ⋂ F → A ∈ x ∈ 𝒫 X | A ∈ x
17 uffixfr ⊢ F ∈ UFil ⁡ X → A ∈ ⋂ F ↔ F = x ∈ 𝒫 X | A ∈ x
18 17 biimpa ⊢ F ∈ UFil ⁡ X ∧ A ∈ ⋂ F → F = x ∈ 𝒫 X | A ∈ x
19 16 18 eleqtrrd ⊢ F ∈ UFil ⁡ X ∧ A ∈ ⋂ F → A ∈ F