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

Metamath Proof Explorer

Theorem isufil

Description: The property of being an ultrafilter. (Contributed by Jeff Hankins, 30-Nov-2009) (Revised by Mario Carneiro, 29-Jul-2015)

Ref Expression
Assertion isufil 
|- ( F e. ( UFil ` X ) <-> ( F e. ( Fil ` X ) /\ A. x e. ~P X ( x e. F \/ ( X \ x ) e. F ) ) )

Proof

Step Hyp Ref Expression
1 df-ufil 
 |-  UFil = ( y e. _V |-> { z e. ( Fil ` y ) | A. x e. ~P y ( x e. z \/ ( y \ x ) e. z ) } )
2 pweq 
 |-  ( y = X -> ~P y = ~P X )
3 2 adantr 
 |-  ( ( y = X /\ z = F ) -> ~P y = ~P X )
4 eleq2 
 |-  ( z = F -> ( x e. z <-> x e. F ) )
5 4 adantl 
 |-  ( ( y = X /\ z = F ) -> ( x e. z <-> x e. F ) )
6 difeq1 
 |-  ( y = X -> ( y \ x ) = ( X \ x ) )
7 eleq12 
 |-  ( ( ( y \ x ) = ( X \ x ) /\ z = F ) -> ( ( y \ x ) e. z <-> ( X \ x ) e. F ) )
8 6 7 sylan 
 |-  ( ( y = X /\ z = F ) -> ( ( y \ x ) e. z <-> ( X \ x ) e. F ) )
9 5 8 orbi12d 
 |-  ( ( y = X /\ z = F ) -> ( ( x e. z \/ ( y \ x ) e. z ) <-> ( x e. F \/ ( X \ x ) e. F ) ) )
10 3 9 raleqbidv 
 |-  ( ( y = X /\ z = F ) -> ( A. x e. ~P y ( x e. z \/ ( y \ x ) e. z ) <-> A. x e. ~P X ( x e. F \/ ( X \ x ) e. F ) ) )
11 fveq2 
 |-  ( y = X -> ( Fil ` y ) = ( Fil ` X ) )
12 fvex 
 |-  ( Fil ` y ) e. _V
13 elfvdm 
 |-  ( F e. ( Fil ` X ) -> X e. dom Fil )
14 1 10 11 12 13 elmptrab2 
 |-  ( F e. ( UFil ` X ) <-> ( F e. ( Fil ` X ) /\ A. x e. ~P X ( x e. F \/ ( X \ x ) e. F ) ) )