brtxp2

Description: The binary relation over a tail cross when the second argument is not an ordered pair. (Contributed by Scott Fenton, 14-Apr-2014) (Revised by Mario Carneiro, 3-May-2015)

		Ref	Expression
	Hypothesis	brtxp2.1	$⊢ A \in V$
	Assertion	brtxp2	$⊢ A (R \otimes S) B \leftrightarrow \exists x \exists y (B = ⟨x, y⟩ \land A R x \land A S y)$

Proof

Step	Hyp	Ref	Expression
1		brtxp2.1	$⊢ A \in V$
2		txpss3v	$⊢ (R \otimes S) \subseteq V \times (V \times V)$
3	2	brel	$⊢ A (R \otimes S) B \to (A \in V \land B \in (V \times V))$
4	3	simprd	$⊢ A (R \otimes S) B \to B \in (V \times V)$
5		elvv	$⊢ B \in (V \times V) \leftrightarrow \exists x \exists y B = ⟨x, y⟩$
6	4 5	sylib	$⊢ A (R \otimes S) B \to \exists x \exists y B = ⟨x, y⟩$
7	6	pm4.71ri	$⊢ A (R \otimes S) B \leftrightarrow (\exists x \exists y B = ⟨x, y⟩ \land A (R \otimes S) B)$
8		19.41vv	$⊢ \exists x \exists y (B = ⟨x, y⟩ \land A (R \otimes S) B) \leftrightarrow (\exists x \exists y B = ⟨x, y⟩ \land A (R \otimes S) B)$
9	7 8	bitr4i	$⊢ A (R \otimes S) B \leftrightarrow \exists x \exists y (B = ⟨x, y⟩ \land A (R \otimes S) B)$
10		breq2	$⊢ B = ⟨x, y⟩ \to (A (R \otimes S) B \leftrightarrow A (R \otimes S) ⟨x, y⟩)$
11	10	pm5.32i	$⊢ (B = ⟨x, y⟩ \land A (R \otimes S) B) \leftrightarrow (B = ⟨x, y⟩ \land A (R \otimes S) ⟨x, y⟩)$
12	11	2exbii	$⊢ \exists x \exists y (B = ⟨x, y⟩ \land A (R \otimes S) B) \leftrightarrow \exists x \exists y (B = ⟨x, y⟩ \land A (R \otimes S) ⟨x, y⟩)$
13		vex	$⊢ x \in V$
14		vex	$⊢ y \in V$
15	1 13 14	brtxp	$⊢ A (R \otimes S) ⟨x, y⟩ \leftrightarrow (A R x \land A S y)$
16	15	anbi2i	$⊢ (B = ⟨x, y⟩ \land A (R \otimes S) ⟨x, y⟩) \leftrightarrow (B = ⟨x, y⟩ \land (A R x \land A S y))$
17		3anass	$⊢ (B = ⟨x, y⟩ \land A R x \land A S y) \leftrightarrow (B = ⟨x, y⟩ \land (A R x \land A S y))$
18	16 17	bitr4i	$⊢ (B = ⟨x, y⟩ \land A (R \otimes S) ⟨x, y⟩) \leftrightarrow (B = ⟨x, y⟩ \land A R x \land A S y)$
19	18	2exbii	$⊢ \exists x \exists y (B = ⟨x, y⟩ \land A (R \otimes S) ⟨x, y⟩) \leftrightarrow \exists x \exists y (B = ⟨x, y⟩ \land A R x \land A S y)$
20	9 12 19	3bitri	$⊢ A (R \otimes S) B \leftrightarrow \exists x \exists y (B = ⟨x, y⟩ \land A R x \land A S y)$

Metamath Proof Explorer

Theorem brtxp2

Proof