Metamath Proof Explorer

Theorem brxrn2

Description: A characterization of the range Cartesian product. (Contributed by Peter Mazsa, 14-Oct-2020)

		Ref	Expression
	Assertion	brxrn2	$⊢ A \in V \to (A R ⋉ S B \leftrightarrow \exists x \exists y (B = ⟨x, y⟩ \land A R x \land A S y))$

Proof

Step	Hyp	Ref	Expression
1		xrnss3v	$⊢ R ⋉ S \subseteq V \times (V \times V)$
2	1	brel	$⊢ A R ⋉ S B \to (A \in V \land B \in (V \times V))$
3	2	simprd	$⊢ A R ⋉ S B \to B \in (V \times V)$
4		elvv	$⊢ B \in (V \times V) \leftrightarrow \exists x \exists y B = ⟨x, y⟩$
5	3 4	sylib	$⊢ A R ⋉ S B \to \exists x \exists y B = ⟨x, y⟩$
6	5	pm4.71ri	$⊢ A R ⋉ S B \leftrightarrow (\exists x \exists y B = ⟨x, y⟩ \land A R ⋉ S B)$
7		19.41vv	$⊢ \exists x \exists y (B = ⟨x, y⟩ \land A R ⋉ S B) \leftrightarrow (\exists x \exists y B = ⟨x, y⟩ \land A R ⋉ S B)$
8		breq2	$⊢ B = ⟨x, y⟩ \to (A R ⋉ S B \leftrightarrow A R ⋉ S ⟨x, y⟩)$
9	8	pm5.32i	$⊢ (B = ⟨x, y⟩ \land A R ⋉ S B) \leftrightarrow (B = ⟨x, y⟩ \land A R ⋉ S ⟨x, y⟩)$
10	9	2exbii	$⊢ \exists x \exists y (B = ⟨x, y⟩ \land A R ⋉ S B) \leftrightarrow \exists x \exists y (B = ⟨x, y⟩ \land A R ⋉ S ⟨x, y⟩)$
11	6 7 10	3bitr2i	$⊢ A R ⋉ S B \leftrightarrow \exists x \exists y (B = ⟨x, y⟩ \land A R ⋉ S ⟨x, y⟩)$
12		brxrn	$⊢ (A \in V \land x \in V \land y \in V) \to (A R ⋉ S ⟨x, y⟩ \leftrightarrow (A R x \land A S y))$
13	12	el3v23	$⊢ A \in V \to (A R ⋉ S ⟨x, y⟩ \leftrightarrow (A R x \land A S y))$
14	13	anbi2d	$⊢ A \in V \to ((B = ⟨x, y⟩ \land A R ⋉ S ⟨x, y⟩) \leftrightarrow (B = ⟨x, y⟩ \land (A R x \land A S y)))$
15		3anass	$⊢ (B = ⟨x, y⟩ \land A R x \land A S y) \leftrightarrow (B = ⟨x, y⟩ \land (A R x \land A S y))$
16	14 15	bitr4di	$⊢ A \in V \to ((B = ⟨x, y⟩ \land A R ⋉ S ⟨x, y⟩) \leftrightarrow (B = ⟨x, y⟩ \land A R x \land A S y))$
17	16	2exbidv	$⊢ A \in V \to (\exists x \exists y (B = ⟨x, y⟩ \land A R ⋉ S ⟨x, y⟩) \leftrightarrow \exists x \exists y (B = ⟨x, y⟩ \land A R x \land A S y))$
18	11 17	bitrid	$⊢ A \in V \to (A R ⋉ S B \leftrightarrow \exists x \exists y (B = ⟨x, y⟩ \land A R x \land A S y))$