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	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑆 ) ∈ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		elfvdm	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → 𝑋 ∈ dom UFil )
2		elpw2g	⊢ ( 𝑋 ∈ dom UFil → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
3	1 2	syl	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
4		isufil	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ↔ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) )
5		eleq1	⊢ ( 𝑥 = 𝑆 → ( 𝑥 ∈ 𝐹 ↔ 𝑆 ∈ 𝐹 ) )
6		difeq2	⊢ ( 𝑥 = 𝑆 → ( 𝑋 ∖ 𝑥 ) = ( 𝑋 ∖ 𝑆 ) )
7	6	eleq1d	⊢ ( 𝑥 = 𝑆 → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ↔ ( 𝑋 ∖ 𝑆 ) ∈ 𝐹 ) )
8	5 7	orbi12d	⊢ ( 𝑥 = 𝑆 → ( ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ↔ ( 𝑆 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑆 ) ∈ 𝐹 ) ) )
9	8	rspccv	⊢ ( ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) → ( 𝑆 ∈ 𝒫 𝑋 → ( 𝑆 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑆 ) ∈ 𝐹 ) ) )
10	4 9	simplbiim	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑆 ∈ 𝒫 𝑋 → ( 𝑆 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑆 ) ∈ 𝐹 ) ) )
11	3 10	sylbird	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑆 ⊆ 𝑋 → ( 𝑆 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑆 ) ∈ 𝐹 ) ) )
12	11	imp	⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑆 ) ∈ 𝐹 ) )