Metamath Proof Explorer

Theorem uffix2

Description: A classification of fixed ultrafilters. (Contributed by Mario Carneiro, 24-May-2015) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion uffix2 
|- ( F e. ( UFil ` X ) -> ( |^| F =/= (/) <-> 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 filn0 
 |-  ( F e. ( Fil ` X ) -> F =/= (/) )
3 intssuni 
 |-  ( F =/= (/) -> |^| F C_ U. F )
4 1 2 3 3syl 
 |-  ( F e. ( UFil ` X ) -> |^| F C_ U. F )
5 filunibas 
 |-  ( F e. ( Fil ` X ) -> U. F = X )
6 1 5 syl 
 |-  ( F e. ( UFil ` X ) -> U. F = X )
7 4 6 sseqtrd 
 |-  ( F e. ( UFil ` X ) -> |^| F C_ X )
8 7 sseld 
 |-  ( F e. ( UFil ` X ) -> ( x e. |^| F -> x e. X ) )
9 8 pm4.71rd 
 |-  ( F e. ( UFil ` X ) -> ( x e. |^| F <-> ( x e. X /\ x e. |^| F ) ) )
10 uffixfr 
 |-  ( F e. ( UFil ` X ) -> ( x e. |^| F <-> F = { y e. ~P X | x e. y } ) )
11 10 anbi2d 
 |-  ( F e. ( UFil ` X ) -> ( ( x e. X /\ x e. |^| F ) <-> ( x e. X /\ F = { y e. ~P X | x e. y } ) ) )
12 9 11 bitrd 
 |-  ( F e. ( UFil ` X ) -> ( x e. |^| F <-> ( x e. X /\ F = { y e. ~P X | x e. y } ) ) )
13 12 exbidv 
 |-  ( F e. ( UFil ` X ) -> ( E. x x e. |^| F <-> E. x ( x e. X /\ F = { y e. ~P X | x e. y } ) ) )
14 n0 
 |-  ( |^| F =/= (/) <-> E. x x e. |^| F )
15 df-rex 
 |-  ( E. x e. X F = { y e. ~P X | x e. y } <-> E. x ( x e. X /\ F = { y e. ~P X | x e. y } ) )
16 13 14 15 3bitr4g 
 |-  ( F e. ( UFil ` X ) -> ( |^| F =/= (/) <-> E. x e. X F = { y e. ~P X | x e. y } ) )