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

Metamath Proof Explorer

Theorem ufilss

Description: For any subset of the base set of an ultrafilter, either the set is in the ultrafilter or the complement is. (Contributed by Jeff Hankins, 1-Dec-2009) (Revised by Mario Carneiro, 29-Jul-2015)

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

Proof

Step Hyp Ref Expression
1 elfvdm 
 |-  ( F e. ( UFil ` X ) -> X e. dom UFil )
2 elpw2g 
 |-  ( X e. dom UFil -> ( S e. ~P X <-> S C_ X ) )
3 1 2 syl 
 |-  ( F e. ( UFil ` X ) -> ( S e. ~P X <-> S C_ X ) )
4 isufil 
 |-  ( F e. ( UFil ` X ) <-> ( F e. ( Fil ` X ) /\ A. x e. ~P X ( x e. F \/ ( X \ x ) e. F ) ) )
5 eleq1 
 |-  ( x = S -> ( x e. F <-> S e. F ) )
6 difeq2 
 |-  ( x = S -> ( X \ x ) = ( X \ S ) )
7 6 eleq1d 
 |-  ( x = S -> ( ( X \ x ) e. F <-> ( X \ S ) e. F ) )
8 5 7 orbi12d 
 |-  ( x = S -> ( ( x e. F \/ ( X \ x ) e. F ) <-> ( S e. F \/ ( X \ S ) e. F ) ) )
9 8 rspccv 
 |-  ( A. x e. ~P X ( x e. F \/ ( X \ x ) e. F ) -> ( S e. ~P X -> ( S e. F \/ ( X \ S ) e. F ) ) )
10 4 9 simplbiim 
 |-  ( F e. ( UFil ` X ) -> ( S e. ~P X -> ( S e. F \/ ( X \ S ) e. F ) ) )
11 3 10 sylbird 
 |-  ( F e. ( UFil ` X ) -> ( S C_ X -> ( S e. F \/ ( X \ S ) e. F ) ) )
12 11 imp 
 |-  ( ( F e. ( UFil ` X ) /\ S C_ X ) -> ( S e. F \/ ( X \ S ) e. F ) )