sscon34b

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

		Ref	Expression
	Assertion	sscon34b	$⊢ (A \subseteq C \land B \subseteq C) \to (A \subseteq B \leftrightarrow C ∖ B \subseteq C ∖ A)$

Step	Hyp	Ref	Expression
1		sscon	$⊢ A \subseteq B \to C ∖ B \subseteq C ∖ A$
2		sscon	$⊢ C ∖ B \subseteq C ∖ A \to C ∖ (C ∖ A) \subseteq C ∖ (C ∖ B)$
3		dfss4	$⊢ A \subseteq C \leftrightarrow C ∖ (C ∖ A) = A$
4	3	biimpi	$⊢ A \subseteq C \to C ∖ (C ∖ A) = A$
5	4	adantr	$⊢ (A \subseteq C \land B \subseteq C) \to C ∖ (C ∖ A) = A$
6		dfss4	$⊢ B \subseteq C \leftrightarrow C ∖ (C ∖ B) = B$
7	6	biimpi	$⊢ B \subseteq C \to C ∖ (C ∖ B) = B$
8	7	adantl	$⊢ (A \subseteq C \land B \subseteq C) \to C ∖ (C ∖ B) = B$
9	5 8	sseq12d	$⊢ (A \subseteq C \land B \subseteq C) \to (C ∖ (C ∖ A) \subseteq C ∖ (C ∖ B) \leftrightarrow A \subseteq B)$
10	2 9	imbitrid	$⊢ (A \subseteq C \land B \subseteq C) \to (C ∖ B \subseteq C ∖ A \to A \subseteq B)$
11	1 10	impbid2	$⊢ (A \subseteq C \land B \subseteq C) \to (A \subseteq B \leftrightarrow C ∖ B \subseteq C ∖ A)$

Metamath Proof Explorer