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 )