unielxp

Description: The membership relation for a Cartesian product is inherited by union. (Contributed by NM, 16-Sep-2006)

		Ref	Expression
	Assertion	unielxp	$⊢ A \in (B \times C) \to ⋃ A \in ⋃ (B \times C)$

Proof

Step	Hyp	Ref	Expression
1		elxp7	$⊢ A \in (B \times C) \leftrightarrow (A \in (V \times V) \land (1^{st} (A) \in B \land 2^{nd} (A) \in C))$
2		elvvuni	$⊢ A \in (V \times V) \to ⋃ A \in A$
3	2	adantr	$⊢ (A \in (V \times V) \land (1^{st} (A) \in B \land 2^{nd} (A) \in C)) \to ⋃ A \in A$
4		simprl	$⊢ (⋃ A \in A \land (A \in (V \times V) \land (1^{st} (A) \in B \land 2^{nd} (A) \in C))) \to A \in (V \times V)$
5		eleq2	$⊢ x = A \to (⋃ A \in x \leftrightarrow ⋃ A \in A)$
6		eleq1	$⊢ x = A \to (x \in (V \times V) \leftrightarrow A \in (V \times V))$
7		fveq2	$⊢ x = A \to 1^{st} (x) = 1^{st} (A)$
8	7	eleq1d	$⊢ x = A \to (1^{st} (x) \in B \leftrightarrow 1^{st} (A) \in B)$
9		fveq2	$⊢ x = A \to 2^{nd} (x) = 2^{nd} (A)$
10	9	eleq1d	$⊢ x = A \to (2^{nd} (x) \in C \leftrightarrow 2^{nd} (A) \in C)$
11	8 10	anbi12d	$⊢ x = A \to ((1^{st} (x) \in B \land 2^{nd} (x) \in C) \leftrightarrow (1^{st} (A) \in B \land 2^{nd} (A) \in C))$
12	6 11	anbi12d	$⊢ x = A \to ((x \in (V \times V) \land (1^{st} (x) \in B \land 2^{nd} (x) \in C)) \leftrightarrow (A \in (V \times V) \land (1^{st} (A) \in B \land 2^{nd} (A) \in C)))$
13	5 12	anbi12d	$⊢ x = A \to ((⋃ A \in x \land (x \in (V \times V) \land (1^{st} (x) \in B \land 2^{nd} (x) \in C))) \leftrightarrow (⋃ A \in A \land (A \in (V \times V) \land (1^{st} (A) \in B \land 2^{nd} (A) \in C))))$
14	13	spcegv	$⊢ A \in (V \times V) \to ((⋃ A \in A \land (A \in (V \times V) \land (1^{st} (A) \in B \land 2^{nd} (A) \in C))) \to \exists x (⋃ A \in x \land (x \in (V \times V) \land (1^{st} (x) \in B \land 2^{nd} (x) \in C))))$
15	4 14	mpcom	$⊢ (⋃ A \in A \land (A \in (V \times V) \land (1^{st} (A) \in B \land 2^{nd} (A) \in C))) \to \exists x (⋃ A \in x \land (x \in (V \times V) \land (1^{st} (x) \in B \land 2^{nd} (x) \in C)))$
16		eluniab	$⊢ ⋃ A \in ⋃ \{x \| (x \in (V \times V) \land (1^{st} (x) \in B \land 2^{nd} (x) \in C))\} \leftrightarrow \exists x (⋃ A \in x \land (x \in (V \times V) \land (1^{st} (x) \in B \land 2^{nd} (x) \in C)))$
17	15 16	sylibr	$⊢ (⋃ A \in A \land (A \in (V \times V) \land (1^{st} (A) \in B \land 2^{nd} (A) \in C))) \to ⋃ A \in ⋃ \{x \| (x \in (V \times V) \land (1^{st} (x) \in B \land 2^{nd} (x) \in C))\}$
18		xp2	$⊢ B \times C = \{x \in (V \times V) \| (1^{st} (x) \in B \land 2^{nd} (x) \in C)\}$
19		df-rab	$⊢ \{x \in (V \times V) \| (1^{st} (x) \in B \land 2^{nd} (x) \in C)\} = \{x \| (x \in (V \times V) \land (1^{st} (x) \in B \land 2^{nd} (x) \in C))\}$
20	18 19	eqtri	$⊢ B \times C = \{x \| (x \in (V \times V) \land (1^{st} (x) \in B \land 2^{nd} (x) \in C))\}$
21	20	unieqi	$⊢ ⋃ (B \times C) = ⋃ \{x \| (x \in (V \times V) \land (1^{st} (x) \in B \land 2^{nd} (x) \in C))\}$
22	17 21	eleqtrrdi	$⊢ (⋃ A \in A \land (A \in (V \times V) \land (1^{st} (A) \in B \land 2^{nd} (A) \in C))) \to ⋃ A \in ⋃ (B \times C)$
23	3 22	mpancom	$⊢ (A \in (V \times V) \land (1^{st} (A) \in B \land 2^{nd} (A) \in C)) \to ⋃ A \in ⋃ (B \times C)$
24	1 23	sylbi	$⊢ A \in (B \times C) \to ⋃ A \in ⋃ (B \times C)$

Metamath Proof Explorer

Theorem unielxp

Proof