elxp5

Description: Membership in a Cartesian product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 when the double intersection does not create class existence problems (caused by int0 ). (Contributed by NM, 1-Aug-2004)

		Ref	Expression
	Assertion	elxp5	$⊢ A \in (B \times C) \leftrightarrow (A = ⟨⋂ ⋂ A, ⋃ ran \{A\}⟩ \land (⋂ ⋂ 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		inteq	$⊢ A = ⟨x, ⋃ ran \{A\}⟩ \to ⋂ A = ⋂ ⟨x, ⋃ ran \{A\}⟩$
25	24	inteqd	$⊢ A = ⟨x, ⋃ ran \{A\}⟩ \to ⋂ ⋂ A = ⋂ ⋂ ⟨x, ⋃ ran \{A\}⟩$
26	5 16	op1stb	$⊢ ⋂ ⋂ ⟨x, ⋃ ran \{A\}⟩ = x$
27	25 26	eqtr2di	$⊢ A = ⟨x, ⋃ ran \{A\}⟩ \to x = ⋂ ⋂ A$
28	27	pm4.71ri	$⊢ A = ⟨x, ⋃ ran \{A\}⟩ \leftrightarrow (x = ⋂ ⋂ A \land A = ⟨x, ⋃ ran \{A\}⟩)$
29	28	anbi1i	$⊢ (A = ⟨x, ⋃ ran \{A\}⟩ \land (x \in B \land ⋃ ran \{A\} \in C)) \leftrightarrow ((x = ⋂ ⋂ A \land A = ⟨x, ⋃ ran \{A\}⟩) \land (x \in B \land ⋃ ran \{A\} \in C))$
30		anass	$⊢ ((x = ⋂ ⋂ A \land A = ⟨x, ⋃ ran \{A\}⟩) \land (x \in B \land ⋃ ran \{A\} \in C)) \leftrightarrow (x = ⋂ ⋂ A \land (A = ⟨x, ⋃ ran \{A\}⟩ \land (x \in B \land ⋃ ran \{A\} \in C)))$
31	23 29 30	3bitri	$⊢ \exists y (A = ⟨x, y⟩ \land (x \in B \land y \in C)) \leftrightarrow (x = ⋂ ⋂ A \land (A = ⟨x, ⋃ ran \{A\}⟩ \land (x \in B \land ⋃ ran \{A\} \in C)))$
32	31	exbii	$⊢ \exists x \exists y (A = ⟨x, y⟩ \land (x \in B \land y \in C)) \leftrightarrow \exists x (x = ⋂ ⋂ A \land (A = ⟨x, ⋃ ran \{A\}⟩ \land (x \in B \land ⋃ ran \{A\} \in C)))$
33		eqvisset	$⊢ x = ⋂ ⋂ A \to ⋂ ⋂ A \in V$
34	33	adantr	$⊢ (x = ⋂ ⋂ A \land (A = ⟨x, ⋃ ran \{A\}⟩ \land (x \in B \land ⋃ ran \{A\} \in C))) \to ⋂ ⋂ A \in V$
35	34	exlimiv	$⊢ \exists x (x = ⋂ ⋂ A \land (A = ⟨x, ⋃ ran \{A\}⟩ \land (x \in B \land ⋃ ran \{A\} \in C))) \to ⋂ ⋂ A \in V$
36		elex	$⊢ ⋂ ⋂ A \in B \to ⋂ ⋂ A \in V$
37	36	ad2antrl	$⊢ (A = ⟨⋂ ⋂ A, ⋃ ran \{A\}⟩ \land (⋂ ⋂ A \in B \land ⋃ ran \{A\} \in C)) \to ⋂ ⋂ A \in V$
38		opeq1	$⊢ x = ⋂ ⋂ A \to ⟨x, ⋃ ran \{A\}⟩ = ⟨⋂ ⋂ A, ⋃ ran \{A\}⟩$
39	38	eqeq2d	$⊢ x = ⋂ ⋂ A \to (A = ⟨x, ⋃ ran \{A\}⟩ \leftrightarrow A = ⟨⋂ ⋂ A, ⋃ ran \{A\}⟩)$
40		eleq1	$⊢ x = ⋂ ⋂ A \to (x \in B \leftrightarrow ⋂ ⋂ A \in B)$
41	40	anbi1d	$⊢ x = ⋂ ⋂ A \to ((x \in B \land ⋃ ran \{A\} \in C) \leftrightarrow (⋂ ⋂ A \in B \land ⋃ ran \{A\} \in C))$
42	39 41	anbi12d	$⊢ x = ⋂ ⋂ A \to ((A = ⟨x, ⋃ ran \{A\}⟩ \land (x \in B \land ⋃ ran \{A\} \in C)) \leftrightarrow (A = ⟨⋂ ⋂ A, ⋃ ran \{A\}⟩ \land (⋂ ⋂ A \in B \land ⋃ ran \{A\} \in C)))$
43	42	ceqsexgv	$⊢ ⋂ ⋂ A \in V \to (\exists x (x = ⋂ ⋂ A \land (A = ⟨x, ⋃ ran \{A\}⟩ \land (x \in B \land ⋃ ran \{A\} \in C))) \leftrightarrow (A = ⟨⋂ ⋂ A, ⋃ ran \{A\}⟩ \land (⋂ ⋂ A \in B \land ⋃ ran \{A\} \in C)))$
44	35 37 43	pm5.21nii	$⊢ \exists x (x = ⋂ ⋂ A \land (A = ⟨x, ⋃ ran \{A\}⟩ \land (x \in B \land ⋃ ran \{A\} \in C))) \leftrightarrow (A = ⟨⋂ ⋂ A, ⋃ ran \{A\}⟩ \land (⋂ ⋂ A \in B \land ⋃ ran \{A\} \in C))$
45	1 32 44	3bitri	$⊢ A \in (B \times C) \leftrightarrow (A = ⟨⋂ ⋂ A, ⋃ ran \{A\}⟩ \land (⋂ ⋂ A \in B \land ⋃ ran \{A\} \in C))$

Metamath Proof Explorer

Theorem elxp5

Proof