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

Metamath Proof Explorer

Theorem fvmpocurryd

Description: The value of the value of a curried operation given in maps-to notation is the operation value of the original operation. (Contributed by AV, 27-Oct-2019)

Ref Expression
Hypotheses fvmpocurryd.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 )
fvmpocurryd.c ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐶 ∈ 𝑉 )
fvmpocurryd.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑊 )
fvmpocurryd.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
fvmpocurryd.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑌 )
Assertion fvmpocurryd ( 𝜑 → ( ( curry 𝐹 ‘ 𝐴 ) ‘ 𝐵 ) = ( 𝐴 𝐹 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fvmpocurryd.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 )
2 fvmpocurryd.c ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐶 ∈ 𝑉 )
3 fvmpocurryd.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑊 )
4 fvmpocurryd.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
5 fvmpocurryd.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑌 )
6 csbcom ⊢ ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶
7 csbcow ⊢ ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶
8 7 csbeq2i ⊢ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶
9 csbcom ⊢ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶
10 csbcow ⊢ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶
11 10 csbeq2i ⊢ ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝐶
12 9 11 eqtri ⊢ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝐶
13 6 8 12 3eqtri ⊢ ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝐶
14 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝐴 / 𝑥 ⦌ 𝐶
15 14 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∈ 𝑉
16 nfcsb1v ⊢ Ⅎ 𝑦 ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝐶
17 16 nfel1 ⊢ Ⅎ 𝑦 ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∈ 𝑉
18 csbeq1a ⊢ ( 𝑥 = 𝐴 → 𝐶 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
19 18 eleq1d ⊢ ( 𝑥 = 𝐴 → ( 𝐶 ∈ 𝑉 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∈ 𝑉 ) )
20 csbeq1a ⊢ ( 𝑦 = 𝐵 → ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
21 20 eleq1d ⊢ ( 𝑦 = 𝐵 → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∈ 𝑉 ↔ ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∈ 𝑉 ) )
22 15 17 19 21 rspc2 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐶 ∈ 𝑉 → ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∈ 𝑉 ) )
23 22 imp ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐶 ∈ 𝑉 ) → ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∈ 𝑉 )
24 4 5 2 23 syl21anc ⊢ ( 𝜑 → ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∈ 𝑉 )
25 13 24 eqeltrid ⊢ ( 𝜑 → ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝑉 )
26 eqid ⊢ ( 𝑏 ∈ 𝑌 ↦ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ) = ( 𝑏 ∈ 𝑌 ↦ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
27 26 fvmpts ⊢ ( ( 𝐵 ∈ 𝑌 ∧ ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝑉 ) → ( ( 𝑏 ∈ 𝑌 ↦ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ) ‘ 𝐵 ) = ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
28 5 25 27 syl2anc ⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝑌 ↦ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ) ‘ 𝐵 ) = ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
29 nfcv ⊢ Ⅎ 𝑎 𝐶
30 nfcv ⊢ Ⅎ 𝑏 𝐶
31 nfcv ⊢ Ⅎ 𝑥 𝑏
32 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑎 / 𝑥 ⦌ 𝐶
33 31 32 nfcsbw ⊢ Ⅎ 𝑥 ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶
34 nfcsb1v ⊢ Ⅎ 𝑦 ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶
35 csbeq1a ⊢ ( 𝑥 = 𝑎 → 𝐶 = ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
36 csbeq1a ⊢ ( 𝑦 = 𝑏 → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
37 35 36 sylan9eq ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → 𝐶 = ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
38 29 30 33 34 37 cbvmpo ⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 ) = ( 𝑎 ∈ 𝑋 , 𝑏 ∈ 𝑌 ↦ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
39 1 38 eqtri ⊢ 𝐹 = ( 𝑎 ∈ 𝑋 , 𝑏 ∈ 𝑌 ↦ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
40 32 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝑉
41 34 nfel1 ⊢ Ⅎ 𝑦 ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝑉
42 35 eleq1d ⊢ ( 𝑥 = 𝑎 → ( 𝐶 ∈ 𝑉 ↔ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝑉 ) )
43 36 eleq1d ⊢ ( 𝑦 = 𝑏 → ( ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝑉 ↔ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝑉 ) )
44 40 41 42 43 rspc2 ⊢ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐶 ∈ 𝑉 → ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝑉 ) )
45 2 44 mpan9 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) ) → ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝑉 )
46 45 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑌 ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝑉 )
47 5 ne0d ⊢ ( 𝜑 → 𝑌 ≠ ∅ )
48 39 46 47 3 4 mpocurryvald ⊢ ( 𝜑 → ( curry 𝐹 ‘ 𝐴 ) = ( 𝑏 ∈ 𝑌 ↦ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ) )
49 48 fveq1d ⊢ ( 𝜑 → ( ( curry 𝐹 ‘ 𝐴 ) ‘ 𝐵 ) = ( ( 𝑏 ∈ 𝑌 ↦ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ) ‘ 𝐵 ) )
50 1 a1i ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 ) )
51 csbcow ⊢ ⦋ 𝑦 / 𝑏 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑦 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶
52 csbid ⊢ ⦋ 𝑦 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑎 / 𝑥 ⦌ 𝐶
53 51 52 eqtr2i ⊢ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑦 / 𝑏 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶
54 53 a1i ⊢ ( 𝜑 → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑦 / 𝑏 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
55 54 csbeq2dv ⊢ ( 𝜑 → ⦋ 𝑥 / 𝑎 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑥 / 𝑎 ⦌ ⦋ 𝑦 / 𝑏 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
56 csbcow ⊢ ⦋ 𝑥 / 𝑎 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑥 / 𝑥 ⦌ 𝐶
57 csbid ⊢ ⦋ 𝑥 / 𝑥 ⦌ 𝐶 = 𝐶
58 56 57 eqtri ⊢ ⦋ 𝑥 / 𝑎 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = 𝐶
59 csbcom ⊢ ⦋ 𝑥 / 𝑎 ⦌ ⦋ 𝑦 / 𝑏 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑦 / 𝑏 ⦌ ⦋ 𝑥 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶
60 55 58 59 3eqtr3g ⊢ ( 𝜑 → 𝐶 = ⦋ 𝑦 / 𝑏 ⦌ ⦋ 𝑥 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
61 csbeq1 ⊢ ( 𝑥 = 𝐴 → ⦋ 𝑥 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
62 61 adantr ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ⦋ 𝑥 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
63 62 csbeq2dv ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ⦋ 𝑦 / 𝑏 ⦌ ⦋ 𝑥 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑦 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
64 csbeq1 ⊢ ( 𝑦 = 𝐵 → ⦋ 𝑦 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
65 64 adantl ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ⦋ 𝑦 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
66 63 65 eqtrd ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ⦋ 𝑦 / 𝑏 ⦌ ⦋ 𝑥 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
67 60 66 sylan9eq ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝐶 = ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
68 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝑌 = 𝑌 )
69 nfv ⊢ Ⅎ 𝑥 𝜑
70 nfv ⊢ Ⅎ 𝑦 𝜑
71 nfcv ⊢ Ⅎ 𝑦 𝐴
72 nfcv ⊢ Ⅎ 𝑥 𝐵
73 nfcv ⊢ Ⅎ 𝑥 𝐴
74 73 33 nfcsbw ⊢ Ⅎ 𝑥 ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶
75 72 74 nfcsbw ⊢ Ⅎ 𝑥 ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶
76 13 16 nfcxfr ⊢ Ⅎ 𝑦 ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶
77 50 67 68 4 5 25 69 70 71 72 75 76 ovmpodxf ⊢ ( 𝜑 → ( 𝐴 𝐹 𝐵 ) = ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
78 28 49 77 3eqtr4d ⊢ ( 𝜑 → ( ( curry 𝐹 ‘ 𝐴 ) ‘ 𝐵 ) = ( 𝐴 𝐹 𝐵 ) )