brpprod

Description: Characterize a quaternary relation over a tail Cartesian product. Together with pprodss4v , this completely defines membership in a parallel product. (Contributed by Scott Fenton, 11-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Hypotheses	brpprod.1	$⊢ X \in V$
	brpprod.2	$⊢ Y \in V$
	brpprod.3	$⊢ Z \in V$
	brpprod.4	$⊢ W \in V$
Assertion	brpprod	$⊢ ⟨X, Y⟩ pprod (A, B) ⟨Z, W⟩ \leftrightarrow (X A Z \land Y B W)$

Proof

Step	Hyp	Ref	Expression
1		brpprod.1	$⊢ X \in V$
2		brpprod.2	$⊢ Y \in V$
3		brpprod.3	$⊢ Z \in V$
4		brpprod.4	$⊢ W \in V$
5		df-pprod	$⊢ pprod (A, B) = ((A \circ ({1^{st} ↾}_{(V \times V)})) \otimes (B \circ ({2^{nd} ↾}_{(V \times V)})))$
6	5	breqi	$⊢ ⟨X, Y⟩ pprod (A, B) ⟨Z, W⟩ \leftrightarrow ⟨X, Y⟩ ((A \circ ({1^{st} ↾}_{(V \times V)})) \otimes (B \circ ({2^{nd} ↾}_{(V \times V)}))) ⟨Z, W⟩$
7		opex	$⊢ ⟨X, Y⟩ \in V$
8	7 3 4	brtxp	$⊢ ⟨X, Y⟩ ((A \circ ({1^{st} ↾}_{(V \times V)})) \otimes (B \circ ({2^{nd} ↾}_{(V \times V)}))) ⟨Z, W⟩ \leftrightarrow (⟨X, Y⟩ (A \circ ({1^{st} ↾}_{(V \times V)})) Z \land ⟨X, Y⟩ (B \circ ({2^{nd} ↾}_{(V \times V)})) W)$
9	7 3	brco	$⊢ ⟨X, Y⟩ (A \circ ({1^{st} ↾}_{(V \times V)})) Z \leftrightarrow \exists x (⟨X, Y⟩ ({1^{st} ↾}_{(V \times V)}) x \land x A Z)$
10	1 2	opelvv	$⊢ ⟨X, Y⟩ \in (V \times V)$
11		vex	$⊢ x \in V$
12	11	brresi	$⊢ ⟨X, Y⟩ ({1^{st} ↾}_{(V \times V)}) x \leftrightarrow (⟨X, Y⟩ \in (V \times V) \land ⟨X, Y⟩ 1^{st} x)$
13	10 12	mpbiran	$⊢ ⟨X, Y⟩ ({1^{st} ↾}_{(V \times V)}) x \leftrightarrow ⟨X, Y⟩ 1^{st} x$
14	1 2	br1steq	$⊢ ⟨X, Y⟩ 1^{st} x \leftrightarrow x = X$
15	13 14	bitri	$⊢ ⟨X, Y⟩ ({1^{st} ↾}_{(V \times V)}) x \leftrightarrow x = X$
16	15	anbi1i	$⊢ (⟨X, Y⟩ ({1^{st} ↾}_{(V \times V)}) x \land x A Z) \leftrightarrow (x = X \land x A Z)$
17	16	exbii	$⊢ \exists x (⟨X, Y⟩ ({1^{st} ↾}_{(V \times V)}) x \land x A Z) \leftrightarrow \exists x (x = X \land x A Z)$
18		breq1	$⊢ x = X \to (x A Z \leftrightarrow X A Z)$
19	1 18	ceqsexv	$⊢ \exists x (x = X \land x A Z) \leftrightarrow X A Z$
20	9 17 19	3bitri	$⊢ ⟨X, Y⟩ (A \circ ({1^{st} ↾}_{(V \times V)})) Z \leftrightarrow X A Z$
21	7 4	brco	$⊢ ⟨X, Y⟩ (B \circ ({2^{nd} ↾}_{(V \times V)})) W \leftrightarrow \exists y (⟨X, Y⟩ ({2^{nd} ↾}_{(V \times V)}) y \land y B W)$
22		vex	$⊢ y \in V$
23	22	brresi	$⊢ ⟨X, Y⟩ ({2^{nd} ↾}_{(V \times V)}) y \leftrightarrow (⟨X, Y⟩ \in (V \times V) \land ⟨X, Y⟩ 2^{nd} y)$
24	10 23	mpbiran	$⊢ ⟨X, Y⟩ ({2^{nd} ↾}_{(V \times V)}) y \leftrightarrow ⟨X, Y⟩ 2^{nd} y$
25	1 2	br2ndeq	$⊢ ⟨X, Y⟩ 2^{nd} y \leftrightarrow y = Y$
26	24 25	bitri	$⊢ ⟨X, Y⟩ ({2^{nd} ↾}_{(V \times V)}) y \leftrightarrow y = Y$
27	26	anbi1i	$⊢ (⟨X, Y⟩ ({2^{nd} ↾}_{(V \times V)}) y \land y B W) \leftrightarrow (y = Y \land y B W)$
28	27	exbii	$⊢ \exists y (⟨X, Y⟩ ({2^{nd} ↾}_{(V \times V)}) y \land y B W) \leftrightarrow \exists y (y = Y \land y B W)$
29		breq1	$⊢ y = Y \to (y B W \leftrightarrow Y B W)$
30	2 29	ceqsexv	$⊢ \exists y (y = Y \land y B W) \leftrightarrow Y B W$
31	21 28 30	3bitri	$⊢ ⟨X, Y⟩ (B \circ ({2^{nd} ↾}_{(V \times V)})) W \leftrightarrow Y B W$
32	20 31	anbi12i	$⊢ (⟨X, Y⟩ (A \circ ({1^{st} ↾}_{(V \times V)})) Z \land ⟨X, Y⟩ (B \circ ({2^{nd} ↾}_{(V \times V)})) W) \leftrightarrow (X A Z \land Y B W)$
33	6 8 32	3bitri	$⊢ ⟨X, Y⟩ pprod (A, B) ⟨Z, W⟩ \leftrightarrow (X A Z \land Y B W)$

Metamath Proof Explorer

Theorem brpprod

Proof