cnvrescnv

Description: Two ways to express the corestriction of a class. (Contributed by BJ, 28-Dec-2023)

		Ref	Expression
	Assertion	cnvrescnv	$⊢ {({R^{-1} ↾}_{B})}^{-1} = R \cap (V \times B)$

Step	Hyp	Ref	Expression
1		df-res	$⊢ {R^{-1} ↾}_{B} = R^{-1} \cap (B \times V)$
2	1	cnveqi	$⊢ {({R^{-1} ↾}_{B})}^{-1} = {(R^{-1} \cap (B \times V))}^{-1}$
3		cnvin	$⊢ {(R^{-1} \cap (B \times V))}^{-1} = {R^{-1}}^{-1} \cap {(B \times V)}^{-1}$
4		cnvcnv	$⊢ {R^{-1}}^{-1} = R \cap (V \times V)$
5		cnvxp	$⊢ {(B \times V)}^{-1} = V \times B$
6	4 5	ineq12i	$⊢ {R^{-1}}^{-1} \cap {(B \times V)}^{-1} = (R \cap (V \times V)) \cap (V \times B)$
7		inass	$⊢ (R \cap (V \times V)) \cap (V \times B) = R \cap ((V \times V) \cap (V \times B))$
8		inxp	$⊢ (V \times V) \cap (V \times B) = (V \cap V) \times (V \cap B)$
9		inv1	$⊢ V \cap V = V$
10	9	eqcomi	$⊢ V = V \cap V$
11		ssv	$⊢ B \subseteq V$
12		ssid	$⊢ B \subseteq B$
13	11 12	ssini	$⊢ B \subseteq V \cap B$
14		inss2	$⊢ V \cap B \subseteq B$
15	13 14	eqssi	$⊢ B = V \cap B$
16	10 15	xpeq12i	$⊢ V \times B = (V \cap V) \times (V \cap B)$
17	8 16	eqtr4i	$⊢ (V \times V) \cap (V \times B) = V \times B$
18	17	ineq2i	$⊢ R \cap ((V \times V) \cap (V \times B)) = R \cap (V \times B)$
19	6 7 18	3eqtri	$⊢ {R^{-1}}^{-1} \cap {(B \times V)}^{-1} = R \cap (V \times B)$
20	2 3 19	3eqtri	$⊢ {({R^{-1} ↾}_{B})}^{-1} = R \cap (V \times B)$

Metamath Proof Explorer