elinxp

Description: Membership in an intersection with a Cartesian product. (Contributed by Peter Mazsa, 9-Sep-2022)

		Ref	Expression
	Assertion	elinxp	$⊢ C \in (R \cap (A \times B)) \leftrightarrow \exists x \in A \exists y \in B (C = ⟨x, y⟩ \land ⟨x, y⟩ \in R)$

Proof

Step	Hyp	Ref	Expression
1		relinxp	$⊢ Rel (R \cap (A \times B))$
2		elrel	$⊢ (Rel (R \cap (A \times B)) \land C \in (R \cap (A \times B))) \to \exists x \exists y C = ⟨x, y⟩$
3	1 2	mpan	$⊢ C \in (R \cap (A \times B)) \to \exists x \exists y C = ⟨x, y⟩$
4		eleq1	$⊢ C = ⟨x, y⟩ \to (C \in (R \cap (A \times B)) \leftrightarrow ⟨x, y⟩ \in (R \cap (A \times B)))$
5	4	biimpd	$⊢ C = ⟨x, y⟩ \to (C \in (R \cap (A \times B)) \to ⟨x, y⟩ \in (R \cap (A \times B)))$
6		opelinxp	$⊢ ⟨x, y⟩ \in (R \cap (A \times B)) \leftrightarrow ((x \in A \land y \in B) \land ⟨x, y⟩ \in R)$
7	6	biimpi	$⊢ ⟨x, y⟩ \in (R \cap (A \times B)) \to ((x \in A \land y \in B) \land ⟨x, y⟩ \in R)$
8	5 7	syl6com	$⊢ C \in (R \cap (A \times B)) \to (C = ⟨x, y⟩ \to ((x \in A \land y \in B) \land ⟨x, y⟩ \in R))$
9	8	ancld	$⊢ C \in (R \cap (A \times B)) \to (C = ⟨x, y⟩ \to (C = ⟨x, y⟩ \land ((x \in A \land y \in B) \land ⟨x, y⟩ \in R)))$
10		an12	$⊢ (C = ⟨x, y⟩ \land ((x \in A \land y \in B) \land ⟨x, y⟩ \in R)) \leftrightarrow ((x \in A \land y \in B) \land (C = ⟨x, y⟩ \land ⟨x, y⟩ \in R))$
11	9 10	syl6ib	$⊢ C \in (R \cap (A \times B)) \to (C = ⟨x, y⟩ \to ((x \in A \land y \in B) \land (C = ⟨x, y⟩ \land ⟨x, y⟩ \in R)))$
12	11	2eximdv	$⊢ C \in (R \cap (A \times B)) \to (\exists x \exists y C = ⟨x, y⟩ \to \exists x \exists y ((x \in A \land y \in B) \land (C = ⟨x, y⟩ \land ⟨x, y⟩ \in R)))$
13	3 12	mpd	$⊢ C \in (R \cap (A \times B)) \to \exists x \exists y ((x \in A \land y \in B) \land (C = ⟨x, y⟩ \land ⟨x, y⟩ \in R))$
14		r2ex	$⊢ \exists x \in A \exists y \in B (C = ⟨x, y⟩ \land ⟨x, y⟩ \in R) \leftrightarrow \exists x \exists y ((x \in A \land y \in B) \land (C = ⟨x, y⟩ \land ⟨x, y⟩ \in R))$
15	13 14	sylibr	$⊢ C \in (R \cap (A \times B)) \to \exists x \in A \exists y \in B (C = ⟨x, y⟩ \land ⟨x, y⟩ \in R)$
16	6	simplbi2	$⊢ (x \in A \land y \in B) \to (⟨x, y⟩ \in R \to ⟨x, y⟩ \in (R \cap (A \times B)))$
17	4	biimprd	$⊢ C = ⟨x, y⟩ \to (⟨x, y⟩ \in (R \cap (A \times B)) \to C \in (R \cap (A \times B)))$
18	16 17	syl9	$⊢ (x \in A \land y \in B) \to (C = ⟨x, y⟩ \to (⟨x, y⟩ \in R \to C \in (R \cap (A \times B))))$
19	18	impd	$⊢ (x \in A \land y \in B) \to ((C = ⟨x, y⟩ \land ⟨x, y⟩ \in R) \to C \in (R \cap (A \times B)))$
20	19	rexlimivv	$⊢ \exists x \in A \exists y \in B (C = ⟨x, y⟩ \land ⟨x, y⟩ \in R) \to C \in (R \cap (A \times B))$
21	15 20	impbii	$⊢ C \in (R \cap (A \times B)) \leftrightarrow \exists x \in A \exists y \in B (C = ⟨x, y⟩ \land ⟨x, y⟩ \in R)$

Metamath Proof Explorer

Theorem elinxp

Proof