brcart

Description: Binary relation form of the cartesian product operator. (Contributed by Scott Fenton, 11-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Hypotheses	brcart.1	$⊢ A \in V$
	brcart.2	$⊢ B \in V$
	brcart.3	$⊢ C \in V$
Assertion	brcart	$⊢ ⟨A, B⟩ 𝖢𝖺𝗋𝗍 C \leftrightarrow C = A \times B$

Proof

Step	Hyp	Ref	Expression
1		brcart.1	$⊢ A \in V$
2		brcart.2	$⊢ B \in V$
3		brcart.3	$⊢ C \in V$
4		opex	$⊢ ⟨A, B⟩ \in V$
5		df-cart	$⊢ 𝖢𝖺𝗋𝗍 = ((V \times V) \times V) ∖ ran ((V \otimes E) ∆ (pprod (E, E) \otimes V))$
6	1 2	opelvv	$⊢ ⟨A, B⟩ \in (V \times V)$
7		brxp	$⊢ ⟨A, B⟩ ((V \times V) \times V) C \leftrightarrow (⟨A, B⟩ \in (V \times V) \land C \in V)$
8	6 3 7	mpbir2an	$⊢ ⟨A, B⟩ ((V \times V) \times V) C$
9		3anass	$⊢ (x = ⟨y, z⟩ \land y E A \land z E B) \leftrightarrow (x = ⟨y, z⟩ \land (y E A \land z E B))$
10	1	epeli	$⊢ y E A \leftrightarrow y \in A$
11	2	epeli	$⊢ z E B \leftrightarrow z \in B$
12	10 11	anbi12i	$⊢ (y E A \land z E B) \leftrightarrow (y \in A \land z \in B)$
13	12	anbi2i	$⊢ (x = ⟨y, z⟩ \land (y E A \land z E B)) \leftrightarrow (x = ⟨y, z⟩ \land (y \in A \land z \in B))$
14	9 13	bitri	$⊢ (x = ⟨y, z⟩ \land y E A \land z E B) \leftrightarrow (x = ⟨y, z⟩ \land (y \in A \land z \in B))$
15	14	2exbii	$⊢ \exists y \exists z (x = ⟨y, z⟩ \land y E A \land z E B) \leftrightarrow \exists y \exists z (x = ⟨y, z⟩ \land (y \in A \land z \in B))$
16		vex	$⊢ x \in V$
17	16 1 2	brpprod3b	$⊢ x pprod (E, E) ⟨A, B⟩ \leftrightarrow \exists y \exists z (x = ⟨y, z⟩ \land y E A \land z E B)$
18		elxp	$⊢ x \in (A \times B) \leftrightarrow \exists y \exists z (x = ⟨y, z⟩ \land (y \in A \land z \in B))$
19	15 17 18	3bitr4ri	$⊢ x \in (A \times B) \leftrightarrow x pprod (E, E) ⟨A, B⟩$
20	4 3 5 8 19	brtxpsd3	$⊢ ⟨A, B⟩ 𝖢𝖺𝗋𝗍 C \leftrightarrow C = A \times B$

Metamath Proof Explorer

Theorem brcart

Proof