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
|- ( 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 )