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