imainrect

Description: Image by a restricted and corestricted binary relation (intersection of a binary relation with a Cartesian product). (Contributed by Stefan O'Rear, 19-Feb-2015)

		Ref	Expression
	Assertion	imainrect	$⊢ (G \cap (A \times B)) [Y] = G [Y \cap A] \cap B$

Proof

Step	Hyp	Ref	Expression
1		df-res	$⊢ {(G \cap (A \times B)) ↾}_{Y} = (G \cap (A \times B)) \cap (Y \times V)$
2	1	rneqi	$⊢ ran ({(G \cap (A \times B)) ↾}_{Y}) = ran ((G \cap (A \times B)) \cap (Y \times V))$
3		df-ima	$⊢ (G \cap (A \times B)) [Y] = ran ({(G \cap (A \times B)) ↾}_{Y})$
4		df-ima	$⊢ G [Y \cap A] = ran ({G ↾}_{(Y \cap A)})$
5		df-res	$⊢ {G ↾}_{(Y \cap A)} = G \cap ((Y \cap A) \times V)$
6	5	rneqi	$⊢ ran ({G ↾}_{(Y \cap A)}) = ran (G \cap ((Y \cap A) \times V))$
7	4 6	eqtri	$⊢ G [Y \cap A] = ran (G \cap ((Y \cap A) \times V))$
8	7	ineq1i	$⊢ G [Y \cap A] \cap B = ran (G \cap ((Y \cap A) \times V)) \cap B$
9		cnvin	$⊢ {((G \cap ((Y \cap A) \times V)) \cap (V \times B))}^{-1} = {(G \cap ((Y \cap A) \times V))}^{-1} \cap {(V \times B)}^{-1}$
10		inxp	$⊢ (A \times V) \cap (V \times B) = (A \cap V) \times (V \cap B)$
11		inv1	$⊢ A \cap V = A$
12		incom	$⊢ V \cap B = B \cap V$
13		inv1	$⊢ B \cap V = B$
14	12 13	eqtri	$⊢ V \cap B = B$
15	11 14	xpeq12i	$⊢ (A \cap V) \times (V \cap B) = A \times B$
16	10 15	eqtr2i	$⊢ A \times B = (A \times V) \cap (V \times B)$
17	16	ineq2i	$⊢ (G \cap (Y \times V)) \cap (A \times B) = (G \cap (Y \times V)) \cap ((A \times V) \cap (V \times B))$
18		in32	$⊢ (G \cap (A \times B)) \cap (Y \times V) = (G \cap (Y \times V)) \cap (A \times B)$
19		xpindir	$⊢ (Y \cap A) \times V = (Y \times V) \cap (A \times V)$
20	19	ineq2i	$⊢ G \cap ((Y \cap A) \times V) = G \cap ((Y \times V) \cap (A \times V))$
21		inass	$⊢ (G \cap (Y \times V)) \cap (A \times V) = G \cap ((Y \times V) \cap (A \times V))$
22	20 21	eqtr4i	$⊢ G \cap ((Y \cap A) \times V) = (G \cap (Y \times V)) \cap (A \times V)$
23	22	ineq1i	$⊢ (G \cap ((Y \cap A) \times V)) \cap (V \times B) = ((G \cap (Y \times V)) \cap (A \times V)) \cap (V \times B)$
24		inass	$⊢ ((G \cap (Y \times V)) \cap (A \times V)) \cap (V \times B) = (G \cap (Y \times V)) \cap ((A \times V) \cap (V \times B))$
25	23 24	eqtri	$⊢ (G \cap ((Y \cap A) \times V)) \cap (V \times B) = (G \cap (Y \times V)) \cap ((A \times V) \cap (V \times B))$
26	17 18 25	3eqtr4i	$⊢ (G \cap (A \times B)) \cap (Y \times V) = (G \cap ((Y \cap A) \times V)) \cap (V \times B)$
27	26	cnveqi	$⊢ {((G \cap (A \times B)) \cap (Y \times V))}^{-1} = {((G \cap ((Y \cap A) \times V)) \cap (V \times B))}^{-1}$
28		df-res	$⊢ {{(G \cap ((Y \cap A) \times V))}^{-1} ↾}_{B} = {(G \cap ((Y \cap A) \times V))}^{-1} \cap (B \times V)$
29		cnvxp	$⊢ {(V \times B)}^{-1} = B \times V$
30	29	ineq2i	$⊢ {(G \cap ((Y \cap A) \times V))}^{-1} \cap {(V \times B)}^{-1} = {(G \cap ((Y \cap A) \times V))}^{-1} \cap (B \times V)$
31	28 30	eqtr4i	$⊢ {{(G \cap ((Y \cap A) \times V))}^{-1} ↾}_{B} = {(G \cap ((Y \cap A) \times V))}^{-1} \cap {(V \times B)}^{-1}$
32	9 27 31	3eqtr4ri	$⊢ {{(G \cap ((Y \cap A) \times V))}^{-1} ↾}_{B} = {((G \cap (A \times B)) \cap (Y \times V))}^{-1}$
33	32	dmeqi	$⊢ dom ({{(G \cap ((Y \cap A) \times V))}^{-1} ↾}_{B}) = dom {((G \cap (A \times B)) \cap (Y \times V))}^{-1}$
34		incom	$⊢ B \cap dom {(G \cap ((Y \cap A) \times V))}^{-1} = dom {(G \cap ((Y \cap A) \times V))}^{-1} \cap B$
35		dmres	$⊢ dom ({{(G \cap ((Y \cap A) \times V))}^{-1} ↾}_{B}) = B \cap dom {(G \cap ((Y \cap A) \times V))}^{-1}$
36		df-rn	$⊢ ran (G \cap ((Y \cap A) \times V)) = dom {(G \cap ((Y \cap A) \times V))}^{-1}$
37	36	ineq1i	$⊢ ran (G \cap ((Y \cap A) \times V)) \cap B = dom {(G \cap ((Y \cap A) \times V))}^{-1} \cap B$
38	34 35 37	3eqtr4ri	$⊢ ran (G \cap ((Y \cap A) \times V)) \cap B = dom ({{(G \cap ((Y \cap A) \times V))}^{-1} ↾}_{B})$
39		df-rn	$⊢ ran ((G \cap (A \times B)) \cap (Y \times V)) = dom {((G \cap (A \times B)) \cap (Y \times V))}^{-1}$
40	33 38 39	3eqtr4ri	$⊢ ran ((G \cap (A \times B)) \cap (Y \times V)) = ran (G \cap ((Y \cap A) \times V)) \cap B$
41	8 40	eqtr4i	$⊢ G [Y \cap A] \cap B = ran ((G \cap (A \times B)) \cap (Y \times V))$
42	2 3 41	3eqtr4i	$⊢ (G \cap (A \times B)) [Y] = G [Y \cap A] \cap B$

Metamath Proof Explorer

Theorem imainrect

Proof