This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mpomptsx

Description: Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 24-Dec-2016)

Ref Expression
Assertion mpomptsx ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↦ ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑢 ∈ V
2 vex ⊢ 𝑣 ∈ V
3 1 2 op1std ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( 1st ‘ 𝑧 ) = 𝑢 )
4 3 csbeq1d ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝑢 / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 )
5 1 2 op2ndd ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( 2nd ‘ 𝑧 ) = 𝑣 )
6 5 csbeq1d ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝑣 / 𝑦 ⦌ 𝐶 )
7 6 csbeq2dv ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ⦋ 𝑢 / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶 )
8 4 7 eqtrd ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 = ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶 )
9 8 mpomptx ⊢ ( 𝑧 ∈ ∪ 𝑢 ∈ 𝐴 ( { 𝑢 } × ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) ↦ ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ) = ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶 )
10 nfcv ⊢ Ⅎ 𝑢 ( { 𝑥 } × 𝐵 )
11 nfcv ⊢ Ⅎ 𝑥 { 𝑢 }
12 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑢 / 𝑥 ⦌ 𝐵
13 11 12 nfxp ⊢ Ⅎ 𝑥 ( { 𝑢 } × ⦋ 𝑢 / 𝑥 ⦌ 𝐵 )
14 sneq ⊢ ( 𝑥 = 𝑢 → { 𝑥 } = { 𝑢 } )
15 csbeq1a ⊢ ( 𝑥 = 𝑢 → 𝐵 = ⦋ 𝑢 / 𝑥 ⦌ 𝐵 )
16 14 15 xpeq12d ⊢ ( 𝑥 = 𝑢 → ( { 𝑥 } × 𝐵 ) = ( { 𝑢 } × ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) )
17 10 13 16 cbviun ⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) = ∪ 𝑢 ∈ 𝐴 ( { 𝑢 } × ⦋ 𝑢 / 𝑥 ⦌ 𝐵 )
18 17 mpteq1i ⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↦ ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ) = ( 𝑧 ∈ ∪ 𝑢 ∈ 𝐴 ( { 𝑢 } × ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) ↦ ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 )
19 nfcv ⊢ Ⅎ 𝑢 𝐵
20 nfcv ⊢ Ⅎ 𝑢 𝐶
21 nfcv ⊢ Ⅎ 𝑣 𝐶
22 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶
23 nfcv ⊢ Ⅎ 𝑦 𝑢
24 nfcsb1v ⊢ Ⅎ 𝑦 ⦋ 𝑣 / 𝑦 ⦌ 𝐶
25 23 24 nfcsbw ⊢ Ⅎ 𝑦 ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶
26 csbeq1a ⊢ ( 𝑦 = 𝑣 → 𝐶 = ⦋ 𝑣 / 𝑦 ⦌ 𝐶 )
27 csbeq1a ⊢ ( 𝑥 = 𝑢 → ⦋ 𝑣 / 𝑦 ⦌ 𝐶 = ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶 )
28 26 27 sylan9eqr ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → 𝐶 = ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶 )
29 19 12 20 21 22 25 15 28 cbvmpox ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑢 ∈ 𝐴 , 𝑣 ∈ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ↦ ⦋ 𝑢 / 𝑥 ⦌ ⦋ 𝑣 / 𝑦 ⦌ 𝐶 )
30 9 18 29 3eqtr4ri ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↦ ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 )