opeliunxp

Description: Membership in a union of Cartesian products. (Contributed by Mario Carneiro, 29-Dec-2014) (Revised by Mario Carneiro, 1-Jan-2017)

		Ref	Expression
	Assertion	opeliunxp	$⊢ ⟨x, C⟩ \in ⋃_{x \in A} (\{x\} \times B) \leftrightarrow (x \in A \land C \in B)$

Proof

Step	Hyp	Ref	Expression
1		df-iun	$⊢ ⋃_{x \in A} (\{x\} \times B) = \{y \| \exists x \in A y \in (\{x\} \times B)\}$
2	1	eleq2i	$⊢ ⟨x, C⟩ \in ⋃_{x \in A} (\{x\} \times B) \leftrightarrow ⟨x, C⟩ \in \{y \| \exists x \in A y \in (\{x\} \times B)\}$
3		opex	$⊢ ⟨x, C⟩ \in V$
4		df-rex	$⊢ \exists x \in A y \in (\{x\} \times B) \leftrightarrow \exists x (x \in A \land y \in (\{x\} \times B))$
5		nfv	$⊢ Ⅎ z (x \in A \land y \in (\{x\} \times B))$
6		nfs1v	$⊢ Ⅎ x [z/ x] x \in A$
7		nfcv	$⊢ \underline{Ⅎ} x \{z\}$
8		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ z / x ⦌ B$
9	7 8	nfxp	$⊢ \underline{Ⅎ} x (\{z\} \times ⦋ z / x ⦌ B)$
10	9	nfcri	$⊢ Ⅎ x y \in (\{z\} \times ⦋ z / x ⦌ B)$
11	6 10	nfan	$⊢ Ⅎ x ([z/ x] x \in A \land y \in (\{z\} \times ⦋ z / x ⦌ B))$
12		sbequ12	$⊢ x = z \to (x \in A \leftrightarrow [z/ x] x \in A)$
13		sneq	$⊢ x = z \to \{x\} = \{z\}$
14		csbeq1a	$⊢ x = z \to B = ⦋ z / x ⦌ B$
15	13 14	xpeq12d	$⊢ x = z \to \{x\} \times B = \{z\} \times ⦋ z / x ⦌ B$
16	15	eleq2d	$⊢ x = z \to (y \in (\{x\} \times B) \leftrightarrow y \in (\{z\} \times ⦋ z / x ⦌ B))$
17	12 16	anbi12d	$⊢ x = z \to ((x \in A \land y \in (\{x\} \times B)) \leftrightarrow ([z/ x] x \in A \land y \in (\{z\} \times ⦋ z / x ⦌ B)))$
18	5 11 17	cbvexv1	$⊢ \exists x (x \in A \land y \in (\{x\} \times B)) \leftrightarrow \exists z ([z/ x] x \in A \land y \in (\{z\} \times ⦋ z / x ⦌ B))$
19	4 18	bitri	$⊢ \exists x \in A y \in (\{x\} \times B) \leftrightarrow \exists z ([z/ x] x \in A \land y \in (\{z\} \times ⦋ z / x ⦌ B))$
20		eleq1	$⊢ y = ⟨x, C⟩ \to (y \in (\{z\} \times ⦋ z / x ⦌ B) \leftrightarrow ⟨x, C⟩ \in (\{z\} \times ⦋ z / x ⦌ B))$
21	20	anbi2d	$⊢ y = ⟨x, C⟩ \to (([z/ x] x \in A \land y \in (\{z\} \times ⦋ z / x ⦌ B)) \leftrightarrow ([z/ x] x \in A \land ⟨x, C⟩ \in (\{z\} \times ⦋ z / x ⦌ B)))$
22	21	exbidv	$⊢ y = ⟨x, C⟩ \to (\exists z ([z/ x] x \in A \land y \in (\{z\} \times ⦋ z / x ⦌ B)) \leftrightarrow \exists z ([z/ x] x \in A \land ⟨x, C⟩ \in (\{z\} \times ⦋ z / x ⦌ B)))$
23	19 22	syl5bb	$⊢ y = ⟨x, C⟩ \to (\exists x \in A y \in (\{x\} \times B) \leftrightarrow \exists z ([z/ x] x \in A \land ⟨x, C⟩ \in (\{z\} \times ⦋ z / x ⦌ B)))$
24	3 23	elab	$⊢ ⟨x, C⟩ \in \{y \| \exists x \in A y \in (\{x\} \times B)\} \leftrightarrow \exists z ([z/ x] x \in A \land ⟨x, C⟩ \in (\{z\} \times ⦋ z / x ⦌ B))$
25		opelxp	$⊢ ⟨x, C⟩ \in (\{z\} \times ⦋ z / x ⦌ B) \leftrightarrow (x \in \{z\} \land C \in ⦋ z / x ⦌ B)$
26	25	anbi2i	$⊢ ([z/ x] x \in A \land ⟨x, C⟩ \in (\{z\} \times ⦋ z / x ⦌ B)) \leftrightarrow ([z/ x] x \in A \land (x \in \{z\} \land C \in ⦋ z / x ⦌ B))$
27		an12	$⊢ ([z/ x] x \in A \land (x \in \{z\} \land C \in ⦋ z / x ⦌ B)) \leftrightarrow (x \in \{z\} \land ([z/ x] x \in A \land C \in ⦋ z / x ⦌ B))$
28		velsn	$⊢ x \in \{z\} \leftrightarrow x = z$
29		equcom	$⊢ x = z \leftrightarrow z = x$
30	28 29	bitri	$⊢ x \in \{z\} \leftrightarrow z = x$
31	30	anbi1i	$⊢ (x \in \{z\} \land ([z/ x] x \in A \land C \in ⦋ z / x ⦌ B)) \leftrightarrow (z = x \land ([z/ x] x \in A \land C \in ⦋ z / x ⦌ B))$
32	26 27 31	3bitri	$⊢ ([z/ x] x \in A \land ⟨x, C⟩ \in (\{z\} \times ⦋ z / x ⦌ B)) \leftrightarrow (z = x \land ([z/ x] x \in A \land C \in ⦋ z / x ⦌ B))$
33	32	exbii	$⊢ \exists z ([z/ x] x \in A \land ⟨x, C⟩ \in (\{z\} \times ⦋ z / x ⦌ B)) \leftrightarrow \exists z (z = x \land ([z/ x] x \in A \land C \in ⦋ z / x ⦌ B))$
34		sbequ12r	$⊢ z = x \to ([z/ x] x \in A \leftrightarrow x \in A)$
35	14	equcoms	$⊢ z = x \to B = ⦋ z / x ⦌ B$
36	35	eqcomd	$⊢ z = x \to ⦋ z / x ⦌ B = B$
37	36	eleq2d	$⊢ z = x \to (C \in ⦋ z / x ⦌ B \leftrightarrow C \in B)$
38	34 37	anbi12d	$⊢ z = x \to (([z/ x] x \in A \land C \in ⦋ z / x ⦌ B) \leftrightarrow (x \in A \land C \in B))$
39	38	equsexvw	$⊢ \exists z (z = x \land ([z/ x] x \in A \land C \in ⦋ z / x ⦌ B)) \leftrightarrow (x \in A \land C \in B)$
40	33 39	bitri	$⊢ \exists z ([z/ x] x \in A \land ⟨x, C⟩ \in (\{z\} \times ⦋ z / x ⦌ B)) \leftrightarrow (x \in A \land C \in B)$
41	2 24 40	3bitri	$⊢ ⟨x, C⟩ \in ⋃_{x \in A} (\{x\} \times B) \leftrightarrow (x \in A \land C \in B)$

Metamath Proof Explorer

Theorem opeliunxp

Proof