resdmres

Description: Restriction to the domain of a restriction. (Contributed by NM, 8-Apr-2007)

		Ref	Expression
	Assertion	resdmres	$⊢ {A ↾}_{dom ({A ↾}_{B})} = {A ↾}_{B}$

Step	Hyp	Ref	Expression
1		in12	$⊢ A \cap ((B \times V) \cap (dom A \times V)) = (B \times V) \cap (A \cap (dom A \times V))$
2		df-res	$⊢ {A ↾}_{dom A} = A \cap (dom A \times V)$
3		resdm2	$⊢ {A ↾}_{dom A} = {A^{-1}}^{-1}$
4	2 3	eqtr3i	$⊢ A \cap (dom A \times V) = {A^{-1}}^{-1}$
5	4	ineq2i	$⊢ (B \times V) \cap (A \cap (dom A \times V)) = (B \times V) \cap {A^{-1}}^{-1}$
6		incom	$⊢ (B \times V) \cap {A^{-1}}^{-1} = {A^{-1}}^{-1} \cap (B \times V)$
7	1 5 6	3eqtri	$⊢ A \cap ((B \times V) \cap (dom A \times V)) = {A^{-1}}^{-1} \cap (B \times V)$
8		df-res	$⊢ {A ↾}_{dom ({A ↾}_{B})} = A \cap (dom ({A ↾}_{B}) \times V)$
9		dmres	$⊢ dom ({A ↾}_{B}) = B \cap dom A$
10	9	xpeq1i	$⊢ dom ({A ↾}_{B}) \times V = (B \cap dom A) \times V$
11		xpindir	$⊢ (B \cap dom A) \times V = (B \times V) \cap (dom A \times V)$
12	10 11	eqtri	$⊢ dom ({A ↾}_{B}) \times V = (B \times V) \cap (dom A \times V)$
13	12	ineq2i	$⊢ A \cap (dom ({A ↾}_{B}) \times V) = A \cap ((B \times V) \cap (dom A \times V))$
14	8 13	eqtri	$⊢ {A ↾}_{dom ({A ↾}_{B})} = A \cap ((B \times V) \cap (dom A \times V))$
15		df-res	$⊢ {{A^{-1}}^{-1} ↾}_{B} = {A^{-1}}^{-1} \cap (B \times V)$
16	7 14 15	3eqtr4i	$⊢ {A ↾}_{dom ({A ↾}_{B})} = {{A^{-1}}^{-1} ↾}_{B}$
17		rescnvcnv	$⊢ {{A^{-1}}^{-1} ↾}_{B} = {A ↾}_{B}$
18	16 17	eqtri	$⊢ {A ↾}_{dom ({A ↾}_{B})} = {A ↾}_{B}$

Metamath Proof Explorer