elxp4

Description: Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp5 , elxp6 , and elxp7 . (Contributed by NM, 17-Feb-2004)

		Ref	Expression
	Assertion	elxp4	$⊢ A \in (B \times C) \leftrightarrow (A = ⟨⋃ dom \{A\}, ⋃ ran \{A\}⟩ \land (⋃ dom \{A\} \in B \land ⋃ ran \{A\} \in C))$

Proof

Step	Hyp	Ref	Expression
1		elxp	$⊢ A \in (B \times C) \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land (x \in B \land y \in C))$
2		sneq	$⊢ A = ⟨x, y⟩ \to \{A\} = \{⟨x, y⟩\}$
3	2	rneqd	$⊢ A = ⟨x, y⟩ \to ran \{A\} = ran \{⟨x, y⟩\}$
4	3	unieqd	$⊢ A = ⟨x, y⟩ \to ⋃ ran \{A\} = ⋃ ran \{⟨x, y⟩\}$
5		vex	$⊢ x \in V$
6		vex	$⊢ y \in V$
7	5 6	op2nda	$⊢ ⋃ ran \{⟨x, y⟩\} = y$
8	4 7	eqtr2di	$⊢ A = ⟨x, y⟩ \to y = ⋃ ran \{A\}$
9	8	pm4.71ri	$⊢ A = ⟨x, y⟩ \leftrightarrow (y = ⋃ ran \{A\} \land A = ⟨x, y⟩)$
10	9	anbi1i	$⊢ (A = ⟨x, y⟩ \land (x \in B \land y \in C)) \leftrightarrow ((y = ⋃ ran \{A\} \land A = ⟨x, y⟩) \land (x \in B \land y \in C))$
11		anass	$⊢ ((y = ⋃ ran \{A\} \land A = ⟨x, y⟩) \land (x \in B \land y \in C)) \leftrightarrow (y = ⋃ ran \{A\} \land (A = ⟨x, y⟩ \land (x \in B \land y \in C)))$
12	10 11	bitri	$⊢ (A = ⟨x, y⟩ \land (x \in B \land y \in C)) \leftrightarrow (y = ⋃ ran \{A\} \land (A = ⟨x, y⟩ \land (x \in B \land y \in C)))$
13	12	exbii	$⊢ \exists y (A = ⟨x, y⟩ \land (x \in B \land y \in C)) \leftrightarrow \exists y (y = ⋃ ran \{A\} \land (A = ⟨x, y⟩ \land (x \in B \land y \in C)))$
14		snex	$⊢ \{A\} \in V$
15	14	rnex	$⊢ ran \{A\} \in V$
16	15	uniex	$⊢ ⋃ ran \{A\} \in V$
17		opeq2	$⊢ y = ⋃ ran \{A\} \to ⟨x, y⟩ = ⟨x, ⋃ ran \{A\}⟩$
18	17	eqeq2d	$⊢ y = ⋃ ran \{A\} \to (A = ⟨x, y⟩ \leftrightarrow A = ⟨x, ⋃ ran \{A\}⟩)$
19		eleq1	$⊢ y = ⋃ ran \{A\} \to (y \in C \leftrightarrow ⋃ ran \{A\} \in C)$
20	19	anbi2d	$⊢ y = ⋃ ran \{A\} \to ((x \in B \land y \in C) \leftrightarrow (x \in B \land ⋃ ran \{A\} \in C))$
21	18 20	anbi12d	$⊢ y = ⋃ ran \{A\} \to ((A = ⟨x, y⟩ \land (x \in B \land y \in C)) \leftrightarrow (A = ⟨x, ⋃ ran \{A\}⟩ \land (x \in B \land ⋃ ran \{A\} \in C)))$
22	16 21	ceqsexv	$⊢ \exists y (y = ⋃ ran \{A\} \land (A = ⟨x, y⟩ \land (x \in B \land y \in C))) \leftrightarrow (A = ⟨x, ⋃ ran \{A\}⟩ \land (x \in B \land ⋃ ran \{A\} \in C))$
23	13 22	bitri	$⊢ \exists y (A = ⟨x, y⟩ \land (x \in B \land y \in C)) \leftrightarrow (A = ⟨x, ⋃ ran \{A\}⟩ \land (x \in B \land ⋃ ran \{A\} \in C))$
24		sneq	$⊢ A = ⟨x, ⋃ ran \{A\}⟩ \to \{A\} = \{⟨x, ⋃ ran \{A\}⟩\}$
25	24	dmeqd	$⊢ A = ⟨x, ⋃ ran \{A\}⟩ \to dom \{A\} = dom \{⟨x, ⋃ ran \{A\}⟩\}$
26	25	unieqd	$⊢ A = ⟨x, ⋃ ran \{A\}⟩ \to ⋃ dom \{A\} = ⋃ dom \{⟨x, ⋃ ran \{A\}⟩\}$
27	5 16	op1sta	$⊢ ⋃ dom \{⟨x, ⋃ ran \{A\}⟩\} = x$
28	26 27	eqtr2di	$⊢ A = ⟨x, ⋃ ran \{A\}⟩ \to x = ⋃ dom \{A\}$
29	28	pm4.71ri	$⊢ A = ⟨x, ⋃ ran \{A\}⟩ \leftrightarrow (x = ⋃ dom \{A\} \land A = ⟨x, ⋃ ran \{A\}⟩)$
30	29	anbi1i	$⊢ (A = ⟨x, ⋃ ran \{A\}⟩ \land (x \in B \land ⋃ ran \{A\} \in C)) \leftrightarrow ((x = ⋃ dom \{A\} \land A = ⟨x, ⋃ ran \{A\}⟩) \land (x \in B \land ⋃ ran \{A\} \in C))$
31		anass	$⊢ ((x = ⋃ dom \{A\} \land A = ⟨x, ⋃ ran \{A\}⟩) \land (x \in B \land ⋃ ran \{A\} \in C)) \leftrightarrow (x = ⋃ dom \{A\} \land (A = ⟨x, ⋃ ran \{A\}⟩ \land (x \in B \land ⋃ ran \{A\} \in C)))$
32	23 30 31	3bitri	$⊢ \exists y (A = ⟨x, y⟩ \land (x \in B \land y \in C)) \leftrightarrow (x = ⋃ dom \{A\} \land (A = ⟨x, ⋃ ran \{A\}⟩ \land (x \in B \land ⋃ ran \{A\} \in C)))$
33	32	exbii	$⊢ \exists x \exists y (A = ⟨x, y⟩ \land (x \in B \land y \in C)) \leftrightarrow \exists x (x = ⋃ dom \{A\} \land (A = ⟨x, ⋃ ran \{A\}⟩ \land (x \in B \land ⋃ ran \{A\} \in C)))$
34	14	dmex	$⊢ dom \{A\} \in V$
35	34	uniex	$⊢ ⋃ dom \{A\} \in V$
36		opeq1	$⊢ x = ⋃ dom \{A\} \to ⟨x, ⋃ ran \{A\}⟩ = ⟨⋃ dom \{A\}, ⋃ ran \{A\}⟩$
37	36	eqeq2d	$⊢ x = ⋃ dom \{A\} \to (A = ⟨x, ⋃ ran \{A\}⟩ \leftrightarrow A = ⟨⋃ dom \{A\}, ⋃ ran \{A\}⟩)$
38		eleq1	$⊢ x = ⋃ dom \{A\} \to (x \in B \leftrightarrow ⋃ dom \{A\} \in B)$
39	38	anbi1d	$⊢ x = ⋃ dom \{A\} \to ((x \in B \land ⋃ ran \{A\} \in C) \leftrightarrow (⋃ dom \{A\} \in B \land ⋃ ran \{A\} \in C))$
40	37 39	anbi12d	$⊢ x = ⋃ dom \{A\} \to ((A = ⟨x, ⋃ ran \{A\}⟩ \land (x \in B \land ⋃ ran \{A\} \in C)) \leftrightarrow (A = ⟨⋃ dom \{A\}, ⋃ ran \{A\}⟩ \land (⋃ dom \{A\} \in B \land ⋃ ran \{A\} \in C)))$
41	35 40	ceqsexv	$⊢ \exists x (x = ⋃ dom \{A\} \land (A = ⟨x, ⋃ ran \{A\}⟩ \land (x \in B \land ⋃ ran \{A\} \in C))) \leftrightarrow (A = ⟨⋃ dom \{A\}, ⋃ ran \{A\}⟩ \land (⋃ dom \{A\} \in B \land ⋃ ran \{A\} \in C))$
42	1 33 41	3bitri	$⊢ A \in (B \times C) \leftrightarrow (A = ⟨⋃ dom \{A\}, ⋃ ran \{A\}⟩ \land (⋃ dom \{A\} \in B \land ⋃ ran \{A\} \in C))$

Metamath Proof Explorer

Theorem elxp4

Proof