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