Metamath Proof Explorer

Theorem ufilb

Description: The complement is in an ultrafilter iff the set is not. (Contributed by Mario Carneiro, 11-Dec-2013) (Revised by Mario Carneiro, 29-Jul-2015)

Ref Expression
Assertion ufilb 
|- ( ( F e. ( UFil ` X ) /\ S C_ X ) -> ( -. S e. F <-> ( X \ S ) e. F ) )

Proof

Step Hyp Ref Expression
1 ufilss 
 |-  ( ( F e. ( UFil ` X ) /\ S C_ X ) -> ( S e. F \/ ( X \ S ) e. F ) )
2 1 ord 
 |-  ( ( F e. ( UFil ` X ) /\ S C_ X ) -> ( -. S e. F -> ( X \ S ) e. F ) )
3 ufilfil 
 |-  ( F e. ( UFil ` X ) -> F e. ( Fil ` X ) )
4 filfbas 
 |-  ( F e. ( Fil ` X ) -> F e. ( fBas ` X ) )
5 fbncp 
 |-  ( ( F e. ( fBas ` X ) /\ S e. F ) -> -. ( X \ S ) e. F )
6 5 ex 
 |-  ( F e. ( fBas ` X ) -> ( S e. F -> -. ( X \ S ) e. F ) )
7 6 con2d 
 |-  ( F e. ( fBas ` X ) -> ( ( X \ S ) e. F -> -. S e. F ) )
8 3 4 7 3syl 
 |-  ( F e. ( UFil ` X ) -> ( ( X \ S ) e. F -> -. S e. F ) )
9 8 adantr 
 |-  ( ( F e. ( UFil ` X ) /\ S C_ X ) -> ( ( X \ S ) e. F -> -. S e. F ) )
10 2 9 impbid 
 |-  ( ( F e. ( UFil ` X ) /\ S C_ X ) -> ( -. S e. F <-> ( X \ S ) e. F ) )