xpinpreima2

Description: Rewrite the cartesian product of two sets as the intersection of their preimage by 1st and 2nd , the projections on the first and second elements. (Contributed by Thierry Arnoux, 22-Sep-2017)

		Ref	Expression
	Assertion	xpinpreima2	$⊢ (A \subseteq E \land B \subseteq F) \to A \times B = {({1^{st} ↾}_{(E \times F)})}^{-1} [A] \cap {({2^{nd} ↾}_{(E \times F)})}^{-1} [B]$

Proof

Step	Hyp	Ref	Expression
1		xp2	$⊢ A \times B = \{r \in (V \times V) \| (1^{st} (r) \in A \land 2^{nd} (r) \in B)\}$
2		xpss	$⊢ E \times F \subseteq V \times V$
3		rabss2	$⊢ E \times F \subseteq V \times V \to \{r \in (E \times F) \| (1^{st} (r) \in A \land 2^{nd} (r) \in B)\} \subseteq \{r \in (V \times V) \| (1^{st} (r) \in A \land 2^{nd} (r) \in B)\}$
4	2 3	mp1i	$⊢ (A \subseteq E \land B \subseteq F) \to \{r \in (E \times F) \| (1^{st} (r) \in A \land 2^{nd} (r) \in B)\} \subseteq \{r \in (V \times V) \| (1^{st} (r) \in A \land 2^{nd} (r) \in B)\}$
5		simprl	$⊢ ((A \subseteq E \land B \subseteq F) \land (r \in (V \times V) \land (1^{st} (r) \in A \land 2^{nd} (r) \in B))) \to r \in (V \times V)$
6		simpll	$⊢ ((A \subseteq E \land B \subseteq F) \land (r \in (V \times V) \land (1^{st} (r) \in A \land 2^{nd} (r) \in B))) \to A \subseteq E$
7		simprrl	$⊢ ((A \subseteq E \land B \subseteq F) \land (r \in (V \times V) \land (1^{st} (r) \in A \land 2^{nd} (r) \in B))) \to 1^{st} (r) \in A$
8	6 7	sseldd	$⊢ ((A \subseteq E \land B \subseteq F) \land (r \in (V \times V) \land (1^{st} (r) \in A \land 2^{nd} (r) \in B))) \to 1^{st} (r) \in E$
9		simplr	$⊢ ((A \subseteq E \land B \subseteq F) \land (r \in (V \times V) \land (1^{st} (r) \in A \land 2^{nd} (r) \in B))) \to B \subseteq F$
10		simprrr	$⊢ ((A \subseteq E \land B \subseteq F) \land (r \in (V \times V) \land (1^{st} (r) \in A \land 2^{nd} (r) \in B))) \to 2^{nd} (r) \in B$
11	9 10	sseldd	$⊢ ((A \subseteq E \land B \subseteq F) \land (r \in (V \times V) \land (1^{st} (r) \in A \land 2^{nd} (r) \in B))) \to 2^{nd} (r) \in F$
12	8 11	jca	$⊢ ((A \subseteq E \land B \subseteq F) \land (r \in (V \times V) \land (1^{st} (r) \in A \land 2^{nd} (r) \in B))) \to (1^{st} (r) \in E \land 2^{nd} (r) \in F)$
13		elxp7	$⊢ r \in (E \times F) \leftrightarrow (r \in (V \times V) \land (1^{st} (r) \in E \land 2^{nd} (r) \in F))$
14	5 12 13	sylanbrc	$⊢ ((A \subseteq E \land B \subseteq F) \land (r \in (V \times V) \land (1^{st} (r) \in A \land 2^{nd} (r) \in B))) \to r \in (E \times F)$
15	14	rabss3d	$⊢ (A \subseteq E \land B \subseteq F) \to \{r \in (V \times V) \| (1^{st} (r) \in A \land 2^{nd} (r) \in B)\} \subseteq \{r \in (E \times F) \| (1^{st} (r) \in A \land 2^{nd} (r) \in B)\}$
16	4 15	eqssd	$⊢ (A \subseteq E \land B \subseteq F) \to \{r \in (E \times F) \| (1^{st} (r) \in A \land 2^{nd} (r) \in B)\} = \{r \in (V \times V) \| (1^{st} (r) \in A \land 2^{nd} (r) \in B)\}$
17	1 16	eqtr4id	$⊢ (A \subseteq E \land B \subseteq F) \to A \times B = \{r \in (E \times F) \| (1^{st} (r) \in A \land 2^{nd} (r) \in B)\}$
18		inrab	$⊢ \{r \in (E \times F) \| 1^{st} (r) \in A\} \cap \{r \in (E \times F) \| 2^{nd} (r) \in B\} = \{r \in (E \times F) \| (1^{st} (r) \in A \land 2^{nd} (r) \in B)\}$
19	17 18	eqtr4di	$⊢ (A \subseteq E \land B \subseteq F) \to A \times B = \{r \in (E \times F) \| 1^{st} (r) \in A\} \cap \{r \in (E \times F) \| 2^{nd} (r) \in B\}$
20		f1stres	$⊢ ({1^{st} ↾}_{(E \times F)}) : E \times F ⟶ E$
21		ffn	$⊢ ({1^{st} ↾}_{(E \times F)}) : E \times F ⟶ E \to ({1^{st} ↾}_{(E \times F)}) Fn (E \times F)$
22		fncnvima2	$⊢ ({1^{st} ↾}_{(E \times F)}) Fn (E \times F) \to {({1^{st} ↾}_{(E \times F)})}^{-1} [A] = \{r \in (E \times F) \| ({1^{st} ↾}_{(E \times F)}) (r) \in A\}$
23	20 21 22	mp2b	$⊢ {({1^{st} ↾}_{(E \times F)})}^{-1} [A] = \{r \in (E \times F) \| ({1^{st} ↾}_{(E \times F)}) (r) \in A\}$
24		fvres	$⊢ r \in (E \times F) \to ({1^{st} ↾}_{(E \times F)}) (r) = 1^{st} (r)$
25	24	eleq1d	$⊢ r \in (E \times F) \to (({1^{st} ↾}_{(E \times F)}) (r) \in A \leftrightarrow 1^{st} (r) \in A)$
26	25	rabbiia	$⊢ \{r \in (E \times F) \| ({1^{st} ↾}_{(E \times F)}) (r) \in A\} = \{r \in (E \times F) \| 1^{st} (r) \in A\}$
27	23 26	eqtri	$⊢ {({1^{st} ↾}_{(E \times F)})}^{-1} [A] = \{r \in (E \times F) \| 1^{st} (r) \in A\}$
28		f2ndres	$⊢ ({2^{nd} ↾}_{(E \times F)}) : E \times F ⟶ F$
29		ffn	$⊢ ({2^{nd} ↾}_{(E \times F)}) : E \times F ⟶ F \to ({2^{nd} ↾}_{(E \times F)}) Fn (E \times F)$
30		fncnvima2	$⊢ ({2^{nd} ↾}_{(E \times F)}) Fn (E \times F) \to {({2^{nd} ↾}_{(E \times F)})}^{-1} [B] = \{r \in (E \times F) \| ({2^{nd} ↾}_{(E \times F)}) (r) \in B\}$
31	28 29 30	mp2b	$⊢ {({2^{nd} ↾}_{(E \times F)})}^{-1} [B] = \{r \in (E \times F) \| ({2^{nd} ↾}_{(E \times F)}) (r) \in B\}$
32		fvres	$⊢ r \in (E \times F) \to ({2^{nd} ↾}_{(E \times F)}) (r) = 2^{nd} (r)$
33	32	eleq1d	$⊢ r \in (E \times F) \to (({2^{nd} ↾}_{(E \times F)}) (r) \in B \leftrightarrow 2^{nd} (r) \in B)$
34	33	rabbiia	$⊢ \{r \in (E \times F) \| ({2^{nd} ↾}_{(E \times F)}) (r) \in B\} = \{r \in (E \times F) \| 2^{nd} (r) \in B\}$
35	31 34	eqtri	$⊢ {({2^{nd} ↾}_{(E \times F)})}^{-1} [B] = \{r \in (E \times F) \| 2^{nd} (r) \in B\}$
36	27 35	ineq12i	$⊢ {({1^{st} ↾}_{(E \times F)})}^{-1} [A] \cap {({2^{nd} ↾}_{(E \times F)})}^{-1} [B] = \{r \in (E \times F) \| 1^{st} (r) \in A\} \cap \{r \in (E \times F) \| 2^{nd} (r) \in B\}$
37	19 36	eqtr4di	$⊢ (A \subseteq E \land B \subseteq F) \to A \times B = {({1^{st} ↾}_{(E \times F)})}^{-1} [A] \cap {({2^{nd} ↾}_{(E \times F)})}^{-1} [B]$

Metamath Proof Explorer

Theorem xpinpreima2

Proof