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

Metamath Proof Explorer

Theorem uffinfix

Description: An ultrafilter containing a finite element is fixed. (Contributed by Jeff Hankins, 5-Dec-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion uffinfix 
|- ( ( F e. ( UFil ` X ) /\ S e. F /\ S e. Fin ) -> E. x e. X F = { y e. ~P X | x e. y } )

Proof

Step Hyp Ref Expression
1 ufilfil 
 |-  ( F e. ( UFil ` X ) -> F e. ( Fil ` X ) )
2 filfinnfr 
 |-  ( ( F e. ( Fil ` X ) /\ S e. F /\ S e. Fin ) -> |^| F =/= (/) )
3 1 2 syl3an1 
 |-  ( ( F e. ( UFil ` X ) /\ S e. F /\ S e. Fin ) -> |^| F =/= (/) )
4 uffix2 
 |-  ( F e. ( UFil ` X ) -> ( |^| F =/= (/) <-> E. x e. X F = { y e. ~P X | x e. y } ) )
5 4 3ad2ant1 
 |-  ( ( F e. ( UFil ` X ) /\ S e. F /\ S e. Fin ) -> ( |^| F =/= (/) <-> E. x e. X F = { y e. ~P X | x e. y } ) )
6 3 5 mpbid 
 |-  ( ( F e. ( UFil ` X ) /\ S e. F /\ S e. Fin ) -> E. x e. X F = { y e. ~P X | x e. y } )