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

Metamath Proof Explorer

Theorem ufildom1

Description: An ultrafilter is generated by at most one element (because free ultrafilters have no generators and fixed ultrafilters have exactly one). (Contributed by Mario Carneiro, 24-May-2015) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion ufildom1 ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ∩ 𝐹 ≼ 1o )

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( ∩ 𝐹 = ∅ → ( ∩ 𝐹 ≼ 1o ↔ ∅ ≼ 1o ) )
2 uffixsn ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ∈ ∩ 𝐹 ) → { 𝑥 } ∈ 𝐹 )
3 intss1 ⊢ ( { 𝑥 } ∈ 𝐹 → ∩ 𝐹 ⊆ { 𝑥 } )
4 2 3 syl ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ∈ ∩ 𝐹 ) → ∩ 𝐹 ⊆ { 𝑥 } )
5 simpr ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ∈ ∩ 𝐹 ) → 𝑥 ∈ ∩ 𝐹 )
6 5 snssd ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ∈ ∩ 𝐹 ) → { 𝑥 } ⊆ ∩ 𝐹 )
7 4 6 eqssd ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ∈ ∩ 𝐹 ) → ∩ 𝐹 = { 𝑥 } )
8 7 ex ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑥 ∈ ∩ 𝐹 → ∩ 𝐹 = { 𝑥 } ) )
9 8 eximdv ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( ∃ 𝑥 𝑥 ∈ ∩ 𝐹 → ∃ 𝑥 ∩ 𝐹 = { 𝑥 } ) )
10 n0 ⊢ ( ∩ 𝐹 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ∩ 𝐹 )
11 en1 ⊢ ( ∩ 𝐹 ≈ 1o ↔ ∃ 𝑥 ∩ 𝐹 = { 𝑥 } )
12 9 10 11 3imtr4g ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( ∩ 𝐹 ≠ ∅ → ∩ 𝐹 ≈ 1o ) )
13 12 imp ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ ∩ 𝐹 ≠ ∅ ) → ∩ 𝐹 ≈ 1o )
14 endom ⊢ ( ∩ 𝐹 ≈ 1o → ∩ 𝐹 ≼ 1o )
15 13 14 syl ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ ∩ 𝐹 ≠ ∅ ) → ∩ 𝐹 ≼ 1o )
16 1on ⊢ 1o ∈ On
17 0domg ⊢ ( 1o ∈ On → ∅ ≼ 1o )
18 16 17 mp1i ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ∅ ≼ 1o )
19 1 15 18 pm2.61ne ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ∩ 𝐹 ≼ 1o )