eliunxp2

Description: Membership in a union of Cartesian products over its second component, analogous to eliunxp . (Contributed by AV, 30-Mar-2019)

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

Proof

Step	Hyp	Ref	Expression
1		relxp	$⊢ Rel (A \times \{y\})$
2	1	rgenw	$⊢ \forall y \in B Rel (A \times \{y\})$
3		reliun	$⊢ Rel ⋃_{y \in B} (A \times \{y\}) \leftrightarrow \forall y \in B Rel (A \times \{y\})$
4	2 3	mpbir	$⊢ Rel ⋃_{y \in B} (A \times \{y\})$
5		elrel	$⊢ (Rel ⋃_{y \in B} (A \times \{y\}) \land C \in ⋃_{y \in B} (A \times \{y\})) \to \exists x \exists y C = ⟨x, y⟩$
6	4 5	mpan	$⊢ C \in ⋃_{y \in B} (A \times \{y\}) \to \exists x \exists y C = ⟨x, y⟩$
7		excom	$⊢ \exists y \exists x C = ⟨x, y⟩ \leftrightarrow \exists x \exists y C = ⟨x, y⟩$
8	6 7	sylibr	$⊢ C \in ⋃_{y \in B} (A \times \{y\}) \to \exists y \exists x C = ⟨x, y⟩$
9	8	pm4.71ri	$⊢ C \in ⋃_{y \in B} (A \times \{y\}) \leftrightarrow (\exists y \exists x C = ⟨x, y⟩ \land C \in ⋃_{y \in B} (A \times \{y\}))$
10		nfiu1	$⊢ \underline{Ⅎ} y ⋃_{y \in B} (A \times \{y\})$
11	10	nfel2	$⊢ Ⅎ y C \in ⋃_{y \in B} (A \times \{y\})$
12	11	19.41	$⊢ \exists y (\exists x C = ⟨x, y⟩ \land C \in ⋃_{y \in B} (A \times \{y\})) \leftrightarrow (\exists y \exists x C = ⟨x, y⟩ \land C \in ⋃_{y \in B} (A \times \{y\}))$
13		19.41v	$⊢ \exists x (C = ⟨x, y⟩ \land C \in ⋃_{y \in B} (A \times \{y\})) \leftrightarrow (\exists x C = ⟨x, y⟩ \land C \in ⋃_{y \in B} (A \times \{y\}))$
14		eleq1	$⊢ C = ⟨x, y⟩ \to (C \in ⋃_{y \in B} (A \times \{y\}) \leftrightarrow ⟨x, y⟩ \in ⋃_{y \in B} (A \times \{y\}))$
15		opeliun2xp	$⊢ ⟨x, y⟩ \in ⋃_{y \in B} (A \times \{y\}) \leftrightarrow (y \in B \land x \in A)$
16	15	biancomi	$⊢ ⟨x, y⟩ \in ⋃_{y \in B} (A \times \{y\}) \leftrightarrow (x \in A \land y \in B)$
17	14 16	bitrdi	$⊢ C = ⟨x, y⟩ \to (C \in ⋃_{y \in B} (A \times \{y\}) \leftrightarrow (x \in A \land y \in B))$
18	17	pm5.32i	$⊢ (C = ⟨x, y⟩ \land C \in ⋃_{y \in B} (A \times \{y\})) \leftrightarrow (C = ⟨x, y⟩ \land (x \in A \land y \in B))$
19	18	exbii	$⊢ \exists x (C = ⟨x, y⟩ \land C \in ⋃_{y \in B} (A \times \{y\})) \leftrightarrow \exists x (C = ⟨x, y⟩ \land (x \in A \land y \in B))$
20	13 19	bitr3i	$⊢ (\exists x C = ⟨x, y⟩ \land C \in ⋃_{y \in B} (A \times \{y\})) \leftrightarrow \exists x (C = ⟨x, y⟩ \land (x \in A \land y \in B))$
21	20	exbii	$⊢ \exists y (\exists x C = ⟨x, y⟩ \land C \in ⋃_{y \in B} (A \times \{y\})) \leftrightarrow \exists y \exists x (C = ⟨x, y⟩ \land (x \in A \land y \in B))$
22	9 12 21	3bitr2i	$⊢ C \in ⋃_{y \in B} (A \times \{y\}) \leftrightarrow \exists y \exists x (C = ⟨x, y⟩ \land (x \in A \land y \in B))$
23		excom	$⊢ \exists y \exists x (C = ⟨x, y⟩ \land (x \in A \land y \in B)) \leftrightarrow \exists x \exists y (C = ⟨x, y⟩ \land (x \in A \land y \in B))$
24	22 23	bitri	$⊢ C \in ⋃_{y \in B} (A \times \{y\}) \leftrightarrow \exists x \exists y (C = ⟨x, y⟩ \land (x \in A \land y \in B))$

Metamath Proof Explorer

Theorem eliunxp2

Proof