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

Metamath Proof Explorer

Theorem uffix2

Description: A classification of fixed ultrafilters. (Contributed by Mario Carneiro, 24-May-2015) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion uffix2 ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( ∩ 𝐹 ≠ ∅ ↔ ∃ 𝑥 ∈ 𝑋 𝐹 = { 𝑦 ∈ 𝒫 𝑋 ∣ 𝑥 ∈ 𝑦 } ) )

Proof

Step Hyp Ref Expression
1 ufilfil ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
2 filn0 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ≠ ∅ )
3 intssuni ⊢ ( 𝐹 ≠ ∅ → ∩ 𝐹 ⊆ ∪ 𝐹 )
4 1 2 3 3syl ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ∩ 𝐹 ⊆ ∪ 𝐹 )
5 filunibas ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∪ 𝐹 = 𝑋 )
6 1 5 syl ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ∪ 𝐹 = 𝑋 )
7 4 6 sseqtrd ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ∩ 𝐹 ⊆ 𝑋 )
8 7 sseld ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑥 ∈ ∩ 𝐹 → 𝑥 ∈ 𝑋 ) )
9 8 pm4.71rd ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑥 ∈ ∩ 𝐹 ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ ∩ 𝐹 ) ) )
10 uffixfr ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑥 ∈ ∩ 𝐹 ↔ 𝐹 = { 𝑦 ∈ 𝒫 𝑋 ∣ 𝑥 ∈ 𝑦 } ) )
11 10 anbi2d ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ ∩ 𝐹 ) ↔ ( 𝑥 ∈ 𝑋 ∧ 𝐹 = { 𝑦 ∈ 𝒫 𝑋 ∣ 𝑥 ∈ 𝑦 } ) ) )
12 9 11 bitrd ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑥 ∈ ∩ 𝐹 ↔ ( 𝑥 ∈ 𝑋 ∧ 𝐹 = { 𝑦 ∈ 𝒫 𝑋 ∣ 𝑥 ∈ 𝑦 } ) ) )
13 12 exbidv ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( ∃ 𝑥 𝑥 ∈ ∩ 𝐹 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑋 ∧ 𝐹 = { 𝑦 ∈ 𝒫 𝑋 ∣ 𝑥 ∈ 𝑦 } ) ) )
14 n0 ⊢ ( ∩ 𝐹 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ∩ 𝐹 )
15 df-rex ⊢ ( ∃ 𝑥 ∈ 𝑋 𝐹 = { 𝑦 ∈ 𝒫 𝑋 ∣ 𝑥 ∈ 𝑦 } ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑋 ∧ 𝐹 = { 𝑦 ∈ 𝒫 𝑋 ∣ 𝑥 ∈ 𝑦 } ) )
16 13 14 15 3bitr4g ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( ∩ 𝐹 ≠ ∅ ↔ ∃ 𝑥 ∈ 𝑋 𝐹 = { 𝑦 ∈ 𝒫 𝑋 ∣ 𝑥 ∈ 𝑦 } ) )