Theorem complss

Description: Complementation reverses inclusion. (Contributed by Andrew Salmon, 15-Jul-2011) (Proof shortened by BJ, 19-Mar-2021)

	Ref	Expression
Assertion	complss	⊢ ( 𝐴 ⊆ 𝐵 ↔ ( V ∖ 𝐵 ) ⊆ ( V ∖ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		sscon	⊢ ( 𝐴 ⊆ 𝐵 → ( V ∖ 𝐵 ) ⊆ ( V ∖ 𝐴 ) )
2		sscon	⊢ ( ( V ∖ 𝐵 ) ⊆ ( V ∖ 𝐴 ) → ( V ∖ ( V ∖ 𝐴 ) ) ⊆ ( V ∖ ( V ∖ 𝐵 ) ) )
3		ddif	⊢ ( V ∖ ( V ∖ 𝐴 ) ) = 𝐴
4		ddif	⊢ ( V ∖ ( V ∖ 𝐵 ) ) = 𝐵
5	2 3 4	3sstr3g	⊢ ( ( V ∖ 𝐵 ) ⊆ ( V ∖ 𝐴 ) → 𝐴 ⊆ 𝐵 )
6	1 5	impbii	⊢ ( 𝐴 ⊆ 𝐵 ↔ ( V ∖ 𝐵 ) ⊆ ( V ∖ 𝐴 ) )