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

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

Proof

Step Hyp Ref Expression
1 ufilss ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑆 ) ∈ 𝐹 ) )
2 1 ord ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( ¬ 𝑆 ∈ 𝐹 → ( 𝑋 ∖ 𝑆 ) ∈ 𝐹 ) )
3 ufilfil ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
4 filfbas ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
5 fbncp ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑆 ∈ 𝐹 ) → ¬ ( 𝑋 ∖ 𝑆 ) ∈ 𝐹 )
6 5 ex ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝑆 ∈ 𝐹 → ¬ ( 𝑋 ∖ 𝑆 ) ∈ 𝐹 ) )
7 6 con2d ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( ( 𝑋 ∖ 𝑆 ) ∈ 𝐹 → ¬ 𝑆 ∈ 𝐹 ) )
8 3 4 7 3syl ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( ( 𝑋 ∖ 𝑆 ) ∈ 𝐹 → ¬ 𝑆 ∈ 𝐹 ) )
9 8 adantr ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝑋 ∖ 𝑆 ) ∈ 𝐹 → ¬ 𝑆 ∈ 𝐹 ) )
10 2 9 impbid ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( ¬ 𝑆 ∈ 𝐹 ↔ ( 𝑋 ∖ 𝑆 ) ∈ 𝐹 ) )