xpinpreima

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	xpinpreima	$⊢ A \times B = {({1^{st} ↾}_{(V \times V)})}^{-1} [A] \cap {({2^{nd} ↾}_{(V \times V)})}^{-1} [B]$

Proof

Step	Hyp	Ref	Expression
1		inrab	$⊢ \{r \in (V \times V) \| 1^{st} (r) \in A\} \cap \{r \in (V \times V) \| 2^{nd} (r) \in B\} = \{r \in (V \times V) \| (1^{st} (r) \in A \land 2^{nd} (r) \in B)\}$
2		f1stres	$⊢ ({1^{st} ↾}_{(V \times V)}) : V \times V ⟶ V$
3		ffn	$⊢ ({1^{st} ↾}_{(V \times V)}) : V \times V ⟶ V \to ({1^{st} ↾}_{(V \times V)}) Fn (V \times V)$
4		fncnvima2	$⊢ ({1^{st} ↾}_{(V \times V)}) Fn (V \times V) \to {({1^{st} ↾}_{(V \times V)})}^{-1} [A] = \{r \in (V \times V) \| ({1^{st} ↾}_{(V \times V)}) (r) \in A\}$
5	2 3 4	mp2b	$⊢ {({1^{st} ↾}_{(V \times V)})}^{-1} [A] = \{r \in (V \times V) \| ({1^{st} ↾}_{(V \times V)}) (r) \in A\}$
6		fvres	$⊢ r \in (V \times V) \to ({1^{st} ↾}_{(V \times V)}) (r) = 1^{st} (r)$
7	6	eleq1d	$⊢ r \in (V \times V) \to (({1^{st} ↾}_{(V \times V)}) (r) \in A \leftrightarrow 1^{st} (r) \in A)$
8	7	rabbiia	$⊢ \{r \in (V \times V) \| ({1^{st} ↾}_{(V \times V)}) (r) \in A\} = \{r \in (V \times V) \| 1^{st} (r) \in A\}$
9	5 8	eqtri	$⊢ {({1^{st} ↾}_{(V \times V)})}^{-1} [A] = \{r \in (V \times V) \| 1^{st} (r) \in A\}$
10		f2ndres	$⊢ ({2^{nd} ↾}_{(V \times V)}) : V \times V ⟶ V$
11		ffn	$⊢ ({2^{nd} ↾}_{(V \times V)}) : V \times V ⟶ V \to ({2^{nd} ↾}_{(V \times V)}) Fn (V \times V)$
12		fncnvima2	$⊢ ({2^{nd} ↾}_{(V \times V)}) Fn (V \times V) \to {({2^{nd} ↾}_{(V \times V)})}^{-1} [B] = \{r \in (V \times V) \| ({2^{nd} ↾}_{(V \times V)}) (r) \in B\}$
13	10 11 12	mp2b	$⊢ {({2^{nd} ↾}_{(V \times V)})}^{-1} [B] = \{r \in (V \times V) \| ({2^{nd} ↾}_{(V \times V)}) (r) \in B\}$
14		fvres	$⊢ r \in (V \times V) \to ({2^{nd} ↾}_{(V \times V)}) (r) = 2^{nd} (r)$
15	14	eleq1d	$⊢ r \in (V \times V) \to (({2^{nd} ↾}_{(V \times V)}) (r) \in B \leftrightarrow 2^{nd} (r) \in B)$
16	15	rabbiia	$⊢ \{r \in (V \times V) \| ({2^{nd} ↾}_{(V \times V)}) (r) \in B\} = \{r \in (V \times V) \| 2^{nd} (r) \in B\}$
17	13 16	eqtri	$⊢ {({2^{nd} ↾}_{(V \times V)})}^{-1} [B] = \{r \in (V \times V) \| 2^{nd} (r) \in B\}$
18	9 17	ineq12i	$⊢ {({1^{st} ↾}_{(V \times V)})}^{-1} [A] \cap {({2^{nd} ↾}_{(V \times V)})}^{-1} [B] = \{r \in (V \times V) \| 1^{st} (r) \in A\} \cap \{r \in (V \times V) \| 2^{nd} (r) \in B\}$
19		xp2	$⊢ A \times B = \{r \in (V \times V) \| (1^{st} (r) \in A \land 2^{nd} (r) \in B)\}$
20	1 18 19	3eqtr4ri	$⊢ A \times B = {({1^{st} ↾}_{(V \times V)})}^{-1} [A] \cap {({2^{nd} ↾}_{(V \times V)})}^{-1} [B]$

Metamath Proof Explorer

Theorem xpinpreima

Proof