ressabs

Description: Restriction absorption law. (Contributed by Mario Carneiro, 12-Jun-2015)

		Ref	Expression
	Assertion	ressabs	$⊢ (A \in X \land B \subseteq A) \to (W ↾_{𝑠} A) ↾_{𝑠} B = W ↾_{𝑠} B$

Step	Hyp	Ref	Expression
1		ssexg	$⊢ (B \subseteq A \land A \in X) \to B \in V$
2	1	ancoms	$⊢ (A \in X \land B \subseteq A) \to B \in V$
3		ressress	$⊢ (A \in X \land B \in V) \to (W ↾_{𝑠} A) ↾_{𝑠} B = W ↾_{𝑠} (A \cap B)$
4	2 3	syldan	$⊢ (A \in X \land B \subseteq A) \to (W ↾_{𝑠} A) ↾_{𝑠} B = W ↾_{𝑠} (A \cap B)$
5		simpr	$⊢ (A \in X \land B \subseteq A) \to B \subseteq A$
6		sseqin2	$⊢ B \subseteq A \leftrightarrow A \cap B = B$
7	5 6	sylib	$⊢ (A \in X \land B \subseteq A) \to A \cap B = B$
8	7	oveq2d	$⊢ (A \in X \land B \subseteq A) \to W ↾_{𝑠} (A \cap B) = W ↾_{𝑠} B$
9	4 8	eqtrd	$⊢ (A \in X \land B \subseteq A) \to (W ↾_{𝑠} A) ↾_{𝑠} B = W ↾_{𝑠} B$

Metamath Proof Explorer