Theorem sscon34b

Description: Relative complementation reverses inclusion of subclasses. Relativized version of complss . (Contributed by RP, 3-Jun-2021)

	Ref	Expression
Assertion	sscon34b	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐶 ∖ 𝐵 ) ⊆ ( 𝐶 ∖ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sscon	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐶 ∖ 𝐵 ) ⊆ ( 𝐶 ∖ 𝐴 ) )
2		sscon	⊢ ( ( 𝐶 ∖ 𝐵 ) ⊆ ( 𝐶 ∖ 𝐴 ) → ( 𝐶 ∖ ( 𝐶 ∖ 𝐴 ) ) ⊆ ( 𝐶 ∖ ( 𝐶 ∖ 𝐵 ) ) )
3		dfss4	⊢ ( 𝐴 ⊆ 𝐶 ↔ ( 𝐶 ∖ ( 𝐶 ∖ 𝐴 ) ) = 𝐴 )
4	3	biimpi	⊢ ( 𝐴 ⊆ 𝐶 → ( 𝐶 ∖ ( 𝐶 ∖ 𝐴 ) ) = 𝐴 )
5	4	adantr	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝐶 ∖ ( 𝐶 ∖ 𝐴 ) ) = 𝐴 )
6		dfss4	⊢ ( 𝐵 ⊆ 𝐶 ↔ ( 𝐶 ∖ ( 𝐶 ∖ 𝐵 ) ) = 𝐵 )
7	6	biimpi	⊢ ( 𝐵 ⊆ 𝐶 → ( 𝐶 ∖ ( 𝐶 ∖ 𝐵 ) ) = 𝐵 )
8	7	adantl	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝐶 ∖ ( 𝐶 ∖ 𝐵 ) ) = 𝐵 )
9	5 8	sseq12d	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( ( 𝐶 ∖ ( 𝐶 ∖ 𝐴 ) ) ⊆ ( 𝐶 ∖ ( 𝐶 ∖ 𝐵 ) ) ↔ 𝐴 ⊆ 𝐵 ) )
10	2 9	imbitrid	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( ( 𝐶 ∖ 𝐵 ) ⊆ ( 𝐶 ∖ 𝐴 ) → 𝐴 ⊆ 𝐵 ) )
11	1 10	impbid2	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝐴 ⊆ 𝐵 ↔ ( 𝐶 ∖ 𝐵 ) ⊆ ( 𝐶 ∖ 𝐴 ) ) )