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