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