mpomptxf

Description: Express a two-argument function as a one-argument function, or vice-versa. In this version B ( x ) is not assumed to be constant w.r.t x . (Contributed by Mario Carneiro, 29-Dec-2014) (Revised by Thierry Arnoux, 31-Mar-2018)

	Ref	Expression
Hypotheses	mpomptxf.0	$⊢ \underline{Ⅎ} x C$
	mpomptxf.1	$⊢ \underline{Ⅎ} y C$
	mpomptxf.2	$⊢ z = ⟨x, y⟩ \to C = D$
Assertion	mpomptxf	$⊢ (z \in ⋃_{x \in A} (\{x\} \times B) ⟼ C) = (x \in A, y \in B ⟼ D)$

Proof

Step	Hyp	Ref	Expression
1		mpomptxf.0	$⊢ \underline{Ⅎ} x C$
2		mpomptxf.1	$⊢ \underline{Ⅎ} y C$
3		mpomptxf.2	$⊢ z = ⟨x, y⟩ \to C = D$
4		df-mpt	$⊢ (z \in ⋃_{x \in A} (\{x\} \times B) ⟼ C) = \{⟨z, w⟩ \| (z \in ⋃_{x \in A} (\{x\} \times B) \land w = C)\}$
5		df-mpo	$⊢ (x \in A, y \in B ⟼ D) = \{⟨⟨x, y⟩, w⟩ \| ((x \in A \land y \in B) \land w = D)\}$
6		eliunxp	$⊢ z \in ⋃_{x \in A} (\{x\} \times B) \leftrightarrow \exists x \exists y (z = ⟨x, y⟩ \land (x \in A \land y \in B))$
7	6	anbi1i	$⊢ (z \in ⋃_{x \in A} (\{x\} \times B) \land w = C) \leftrightarrow (\exists x \exists y (z = ⟨x, y⟩ \land (x \in A \land y \in B)) \land w = C)$
8	2	nfeq2	$⊢ Ⅎ y w = C$
9	8	19.41	$⊢ \exists y ((z = ⟨x, y⟩ \land (x \in A \land y \in B)) \land w = C) \leftrightarrow (\exists y (z = ⟨x, y⟩ \land (x \in A \land y \in B)) \land w = C)$
10	9	exbii	$⊢ \exists x \exists y ((z = ⟨x, y⟩ \land (x \in A \land y \in B)) \land w = C) \leftrightarrow \exists x (\exists y (z = ⟨x, y⟩ \land (x \in A \land y \in B)) \land w = C)$
11	1	nfeq2	$⊢ Ⅎ x w = C$
12	11	19.41	$⊢ \exists x (\exists y (z = ⟨x, y⟩ \land (x \in A \land y \in B)) \land w = C) \leftrightarrow (\exists x \exists y (z = ⟨x, y⟩ \land (x \in A \land y \in B)) \land w = C)$
13	10 12	bitri	$⊢ \exists x \exists y ((z = ⟨x, y⟩ \land (x \in A \land y \in B)) \land w = C) \leftrightarrow (\exists x \exists y (z = ⟨x, y⟩ \land (x \in A \land y \in B)) \land w = C)$
14		anass	$⊢ ((z = ⟨x, y⟩ \land (x \in A \land y \in B)) \land w = C) \leftrightarrow (z = ⟨x, y⟩ \land ((x \in A \land y \in B) \land w = C))$
15	3	eqeq2d	$⊢ z = ⟨x, y⟩ \to (w = C \leftrightarrow w = D)$
16	15	anbi2d	$⊢ z = ⟨x, y⟩ \to (((x \in A \land y \in B) \land w = C) \leftrightarrow ((x \in A \land y \in B) \land w = D))$
17	16	pm5.32i	$⊢ (z = ⟨x, y⟩ \land ((x \in A \land y \in B) \land w = C)) \leftrightarrow (z = ⟨x, y⟩ \land ((x \in A \land y \in B) \land w = D))$
18	14 17	bitri	$⊢ ((z = ⟨x, y⟩ \land (x \in A \land y \in B)) \land w = C) \leftrightarrow (z = ⟨x, y⟩ \land ((x \in A \land y \in B) \land w = D))$
19	18	2exbii	$⊢ \exists x \exists y ((z = ⟨x, y⟩ \land (x \in A \land y \in B)) \land w = C) \leftrightarrow \exists x \exists y (z = ⟨x, y⟩ \land ((x \in A \land y \in B) \land w = D))$
20	7 13 19	3bitr2i	$⊢ (z \in ⋃_{x \in A} (\{x\} \times B) \land w = C) \leftrightarrow \exists x \exists y (z = ⟨x, y⟩ \land ((x \in A \land y \in B) \land w = D))$
21	20	opabbii	$⊢ \{⟨z, w⟩ \| (z \in ⋃_{x \in A} (\{x\} \times B) \land w = C)\} = \{⟨z, w⟩ \| \exists x \exists y (z = ⟨x, y⟩ \land ((x \in A \land y \in B) \land w = D))\}$
22		dfoprab2	$⊢ \{⟨⟨x, y⟩, w⟩ \| ((x \in A \land y \in B) \land w = D)\} = \{⟨z, w⟩ \| \exists x \exists y (z = ⟨x, y⟩ \land ((x \in A \land y \in B) \land w = D))\}$
23	21 22	eqtr4i	$⊢ \{⟨z, w⟩ \| (z \in ⋃_{x \in A} (\{x\} \times B) \land w = C)\} = \{⟨⟨x, y⟩, w⟩ \| ((x \in A \land y \in B) \land w = D)\}$
24	5 23	eqtr4i	$⊢ (x \in A, y \in B ⟼ D) = \{⟨z, w⟩ \| (z \in ⋃_{x \in A} (\{x\} \times B) \land w = C)\}$
25	4 24	eqtr4i	$⊢ (z \in ⋃_{x \in A} (\{x\} \times B) ⟼ C) = (x \in A, y \in B ⟼ D)$

Metamath Proof Explorer

Theorem mpomptxf

Proof