redundss3

Description: Implication of redundancy predicate. (Contributed by Peter Mazsa, 26-Oct-2022)

		Ref	Expression
	Hypothesis	redundss3.1	$⊢ D \subseteq C$
	Assertion	redundss3	$⊢ A Redund ⟨B, C⟩ \to A Redund ⟨B, D⟩$

Step	Hyp	Ref	Expression
1		redundss3.1	$⊢ D \subseteq C$
2		ineq1	$⊢ A \cap C = B \cap C \to (A \cap C) \cap D = (B \cap C) \cap D$
3		dfss	$⊢ D \subseteq C \leftrightarrow D = D \cap C$
4	1 3	mpbi	$⊢ D = D \cap C$
5		incom	$⊢ D \cap C = C \cap D$
6	4 5	eqtri	$⊢ D = C \cap D$
7	6	ineq2i	$⊢ A \cap D = A \cap (C \cap D)$
8		inass	$⊢ (A \cap C) \cap D = A \cap (C \cap D)$
9	7 8	eqtr4i	$⊢ A \cap D = (A \cap C) \cap D$
10	6	ineq2i	$⊢ B \cap D = B \cap (C \cap D)$
11		inass	$⊢ (B \cap C) \cap D = B \cap (C \cap D)$
12	10 11	eqtr4i	$⊢ B \cap D = (B \cap C) \cap D$
13	2 9 12	3eqtr4g	$⊢ A \cap C = B \cap C \to A \cap D = B \cap D$
14	13	anim2i	$⊢ (A \subseteq B \land A \cap C = B \cap C) \to (A \subseteq B \land A \cap D = B \cap D)$
15		df-redund	$⊢ A Redund ⟨B, C⟩ \leftrightarrow (A \subseteq B \land A \cap C = B \cap C)$
16		df-redund	$⊢ A Redund ⟨B, D⟩ \leftrightarrow (A \subseteq B \land A \cap D = B \cap D)$
17	14 15 16	3imtr4i	$⊢ A Redund ⟨B, C⟩ \to A Redund ⟨B, D⟩$

Metamath Proof Explorer