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	|- ( F e. ( UFil ` X ) -> |^| F ~<_ 1o )

Proof

Step	Hyp	Ref	Expression
1		breq1	|- ( |^| F = (/) -> ( |^| F ~<_ 1o <-> (/) ~<_ 1o ) )
2		uffixsn	|- ( ( F e. ( UFil ` X ) /\ x e. |^| F ) -> { x } e. F )
3		intss1	|- ( { x } e. F -> |^| F C_ { x } )
4	2 3	syl	|- ( ( F e. ( UFil ` X ) /\ x e. |^| F ) -> |^| F C_ { x } )
5		simpr	|- ( ( F e. ( UFil ` X ) /\ x e. |^| F ) -> x e. |^| F )
6	5	snssd	|- ( ( F e. ( UFil ` X ) /\ x e. |^| F ) -> { x } C_ |^| F )
7	4 6	eqssd	|- ( ( F e. ( UFil ` X ) /\ x e. |^| F ) -> |^| F = { x } )
8	7	ex	|- ( F e. ( UFil ` X ) -> ( x e. |^| F -> |^| F = { x } ) )
9	8	eximdv	|- ( F e. ( UFil ` X ) -> ( E. x x e. |^| F -> E. x |^| F = { x } ) )
10		n0	|- ( |^| F =/= (/) <-> E. x x e. |^| F )
11		en1	|- ( |^| F ~~ 1o <-> E. x |^| F = { x } )
12	9 10 11	3imtr4g	|- ( F e. ( UFil ` X ) -> ( |^| F =/= (/) -> |^| F ~~ 1o ) )
13	12	imp	|- ( ( F e. ( UFil ` X ) /\ |^| F =/= (/) ) -> |^| F ~~ 1o )
14		endom	|- ( |^| F ~~ 1o -> |^| F ~<_ 1o )
15	13 14	syl	|- ( ( F e. ( UFil ` X ) /\ |^| F =/= (/) ) -> |^| F ~<_ 1o )
16		1on	|- 1o e. On
17		0domg	|- ( 1o e. On -> (/) ~<_ 1o )
18	16 17	mp1i	|- ( F e. ( UFil ` X ) -> (/) ~<_ 1o )
19	1 15 18	pm2.61ne	|- ( F e. ( UFil ` X ) -> |^| F ~<_ 1o )