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

Metamath Proof Explorer

Theorem uffixsn

Description: The singleton of the generator of a fixed ultrafilter is in the filter. (Contributed by Mario Carneiro, 24-May-2015) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion uffixsn 
|- ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> { A } e. F )

Proof

Step Hyp Ref Expression
1 eleq2 
 |-  ( x = { A } -> ( A e. x <-> A e. { A } ) )
2 ufilfil 
 |-  ( F e. ( UFil ` X ) -> F e. ( Fil ` X ) )
3 filn0 
 |-  ( F e. ( Fil ` X ) -> F =/= (/) )
4 intssuni 
 |-  ( F =/= (/) -> |^| F C_ U. F )
5 2 3 4 3syl 
 |-  ( F e. ( UFil ` X ) -> |^| F C_ U. F )
6 filunibas 
 |-  ( F e. ( Fil ` X ) -> U. F = X )
7 2 6 syl 
 |-  ( F e. ( UFil ` X ) -> U. F = X )
8 5 7 sseqtrd 
 |-  ( F e. ( UFil ` X ) -> |^| F C_ X )
9 8 sselda 
 |-  ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> A e. X )
10 9 snssd 
 |-  ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> { A } C_ X )
11 snex 
 |-  { A } e. _V
12 11 elpw 
 |-  ( { A } e. ~P X <-> { A } C_ X )
13 10 12 sylibr 
 |-  ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> { A } e. ~P X )
14 snidg 
 |-  ( A e. |^| F -> A e. { A } )
15 14 adantl 
 |-  ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> A e. { A } )
16 1 13 15 elrabd 
 |-  ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> { A } e. { x e. ~P X | A e. x } )
17 uffixfr 
 |-  ( F e. ( UFil ` X ) -> ( A e. |^| F <-> F = { x e. ~P X | A e. x } ) )
18 17 biimpa 
 |-  ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> F = { x e. ~P X | A e. x } )
19 16 18 eleqtrrd 
 |-  ( ( F e. ( UFil ` X ) /\ A e. |^| F ) -> { A } e. F )