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	⊢ 𝐶 ∈ V
	Assertion	dfmpo	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝐶 ⟩ }

Proof

Step	Hyp	Ref	Expression
1		dfmpo.1	⊢ 𝐶 ∈ V
2		mpompts	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 1^st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 )
3	1	csbex	⊢ ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ∈ V
4	3	csbex	⊢ ⦋ ( 1^st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ∈ V
5	4	dfmpt	⊢ ( 𝑤 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 1^st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ) = ∪ 𝑤 ∈ ( 𝐴 × 𝐵 ) { ⟨ 𝑤 , ⦋ ( 1^st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ⟩ }
6		nfcv	⊢ Ⅎ 𝑥 𝑤
7		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ ( 1^st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶
8	6 7	nfop	⊢ Ⅎ 𝑥 ⟨ 𝑤 , ⦋ ( 1^st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ⟩
9	8	nfsn	⊢ Ⅎ 𝑥 { ⟨ 𝑤 , ⦋ ( 1^st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ⟩ }
10		nfcv	⊢ Ⅎ 𝑦 𝑤
11		nfcv	⊢ Ⅎ 𝑦 ( 1^st ‘ 𝑤 )
12		nfcsb1v	⊢ Ⅎ 𝑦 ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶
13	11 12	nfcsbw	⊢ Ⅎ 𝑦 ⦋ ( 1^st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶
14	10 13	nfop	⊢ Ⅎ 𝑦 ⟨ 𝑤 , ⦋ ( 1^st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ⟩
15	14	nfsn	⊢ Ⅎ 𝑦 { ⟨ 𝑤 , ⦋ ( 1^st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ⟩ }
16		nfcv	⊢ Ⅎ 𝑤 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝐶 ⟩ }
17		id	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ )
18		csbopeq1a	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ⦋ ( 1^st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 = 𝐶 )
19	17 18	opeq12d	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ⟨ 𝑤 , ⦋ ( 1^st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝐶 ⟩ )
20	19	sneqd	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → { ⟨ 𝑤 , ⦋ ( 1^st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ⟩ } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝐶 ⟩ } )
21	9 15 16 20	iunxpf	⊢ ∪ 𝑤 ∈ ( 𝐴 × 𝐵 ) { ⟨ 𝑤 , ⦋ ( 1^st ‘ 𝑤 ) / 𝑥 ⦌ ⦋ ( 2^nd ‘ 𝑤 ) / 𝑦 ⦌ 𝐶 ⟩ } = ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝐶 ⟩ }
22	2 5 21	3eqtri	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝐶 ⟩ }

Metamath Proof Explorer

Theorem dfmpo

Proof