dfmpo

Description: Alternate definition for the maps-to notation df-mpo (although it requires that C be a set). (Contributed by NM, 19-Dec-2008) (Revised by Mario Carneiro, 31-Aug-2015)

		Ref	Expression
	Hypothesis	dfmpo.1	$⊢ C \in V$
	Assertion	dfmpo	$⊢ (x \in A, y \in B ⟼ C) = ⋃_{x \in A} ⋃_{y \in B} \{⟨⟨x, y⟩, C⟩\}$

Proof

Step	Hyp	Ref	Expression
1		dfmpo.1	$⊢ C \in V$
2		mpompts	$⊢ (x \in A, y \in B ⟼ C) = (w \in (A \times B) ⟼ ⦋ 1^{st} (w) / x ⦌ ⦋ 2^{nd} (w) / y ⦌ C)$
3	1	csbex	$⊢ ⦋ 2^{nd} (w) / y ⦌ C \in V$
4	3	csbex	$⊢ ⦋ 1^{st} (w) / x ⦌ ⦋ 2^{nd} (w) / y ⦌ C \in V$
5	4	dfmpt	$⊢ (w \in (A \times B) ⟼ ⦋ 1^{st} (w) / x ⦌ ⦋ 2^{nd} (w) / y ⦌ C) = ⋃_{w \in A \times B} \{⟨w, ⦋ 1^{st} (w) / x ⦌ ⦋ 2^{nd} (w) / y ⦌ C⟩\}$
6		nfcv	$⊢ \underline{Ⅎ} x w$
7		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ 1^{st} (w) / x ⦌ ⦋ 2^{nd} (w) / y ⦌ C$
8	6 7	nfop	$⊢ \underline{Ⅎ} x ⟨w, ⦋ 1^{st} (w) / x ⦌ ⦋ 2^{nd} (w) / y ⦌ C⟩$
9	8	nfsn	$⊢ \underline{Ⅎ} x \{⟨w, ⦋ 1^{st} (w) / x ⦌ ⦋ 2^{nd} (w) / y ⦌ C⟩\}$
10		nfcv	$⊢ \underline{Ⅎ} y w$
11		nfcv	$⊢ \underline{Ⅎ} y 1^{st} (w)$
12		nfcsb1v	$⊢ \underline{Ⅎ} y ⦋ 2^{nd} (w) / y ⦌ C$
13	11 12	nfcsbw	$⊢ \underline{Ⅎ} y ⦋ 1^{st} (w) / x ⦌ ⦋ 2^{nd} (w) / y ⦌ C$
14	10 13	nfop	$⊢ \underline{Ⅎ} y ⟨w, ⦋ 1^{st} (w) / x ⦌ ⦋ 2^{nd} (w) / y ⦌ C⟩$
15	14	nfsn	$⊢ \underline{Ⅎ} y \{⟨w, ⦋ 1^{st} (w) / x ⦌ ⦋ 2^{nd} (w) / y ⦌ C⟩\}$
16		nfcv	$⊢ \underline{Ⅎ} w \{⟨⟨x, y⟩, C⟩\}$
17		id	$⊢ w = ⟨x, y⟩ \to w = ⟨x, y⟩$
18		csbopeq1a	$⊢ w = ⟨x, y⟩ \to ⦋ 1^{st} (w) / x ⦌ ⦋ 2^{nd} (w) / y ⦌ C = C$
19	17 18	opeq12d	$⊢ w = ⟨x, y⟩ \to ⟨w, ⦋ 1^{st} (w) / x ⦌ ⦋ 2^{nd} (w) / y ⦌ C⟩ = ⟨⟨x, y⟩, C⟩$
20	19	sneqd	$⊢ w = ⟨x, y⟩ \to \{⟨w, ⦋ 1^{st} (w) / x ⦌ ⦋ 2^{nd} (w) / y ⦌ C⟩\} = \{⟨⟨x, y⟩, C⟩\}$
21	9 15 16 20	iunxpf	$⊢ ⋃_{w \in A \times B} \{⟨w, ⦋ 1^{st} (w) / x ⦌ ⦋ 2^{nd} (w) / y ⦌ C⟩\} = ⋃_{x \in A} ⋃_{y \in B} \{⟨⟨x, y⟩, C⟩\}$
22	2 5 21	3eqtri	$⊢ (x \in A, y \in B ⟼ C) = ⋃_{x \in A} ⋃_{y \in B} \{⟨⟨x, y⟩, C⟩\}$

Metamath Proof Explorer

Theorem dfmpo

Proof