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