Step |
Hyp |
Ref |
Expression |
0 |
|
ccurf |
⊢ curryF |
1 |
|
ve |
⊢ 𝑒 |
2 |
|
cvv |
⊢ V |
3 |
|
vf |
⊢ 𝑓 |
4 |
|
c1st |
⊢ 1st |
5 |
1
|
cv |
⊢ 𝑒 |
6 |
5 4
|
cfv |
⊢ ( 1st ‘ 𝑒 ) |
7 |
|
vc |
⊢ 𝑐 |
8 |
|
c2nd |
⊢ 2nd |
9 |
5 8
|
cfv |
⊢ ( 2nd ‘ 𝑒 ) |
10 |
|
vd |
⊢ 𝑑 |
11 |
|
vx |
⊢ 𝑥 |
12 |
|
cbs |
⊢ Base |
13 |
7
|
cv |
⊢ 𝑐 |
14 |
13 12
|
cfv |
⊢ ( Base ‘ 𝑐 ) |
15 |
|
vy |
⊢ 𝑦 |
16 |
10
|
cv |
⊢ 𝑑 |
17 |
16 12
|
cfv |
⊢ ( Base ‘ 𝑑 ) |
18 |
11
|
cv |
⊢ 𝑥 |
19 |
3
|
cv |
⊢ 𝑓 |
20 |
19 4
|
cfv |
⊢ ( 1st ‘ 𝑓 ) |
21 |
15
|
cv |
⊢ 𝑦 |
22 |
18 21 20
|
co |
⊢ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) |
23 |
15 17 22
|
cmpt |
⊢ ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) ) |
24 |
|
vz |
⊢ 𝑧 |
25 |
|
vg |
⊢ 𝑔 |
26 |
|
chom |
⊢ Hom |
27 |
16 26
|
cfv |
⊢ ( Hom ‘ 𝑑 ) |
28 |
24
|
cv |
⊢ 𝑧 |
29 |
21 28 27
|
co |
⊢ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) |
30 |
|
ccid |
⊢ Id |
31 |
13 30
|
cfv |
⊢ ( Id ‘ 𝑐 ) |
32 |
18 31
|
cfv |
⊢ ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) |
33 |
18 21
|
cop |
⊢ 〈 𝑥 , 𝑦 〉 |
34 |
19 8
|
cfv |
⊢ ( 2nd ‘ 𝑓 ) |
35 |
18 28
|
cop |
⊢ 〈 𝑥 , 𝑧 〉 |
36 |
33 35 34
|
co |
⊢ ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝑓 ) 〈 𝑥 , 𝑧 〉 ) |
37 |
25
|
cv |
⊢ 𝑔 |
38 |
32 37 36
|
co |
⊢ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝑓 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) |
39 |
25 29 38
|
cmpt |
⊢ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝑓 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) |
40 |
15 24 17 17 39
|
cmpo |
⊢ ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝑓 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) |
41 |
23 40
|
cop |
⊢ 〈 ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝑓 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 |
42 |
11 14 41
|
cmpt |
⊢ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ 〈 ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝑓 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 ) |
43 |
13 26
|
cfv |
⊢ ( Hom ‘ 𝑐 ) |
44 |
18 21 43
|
co |
⊢ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) |
45 |
21 28
|
cop |
⊢ 〈 𝑦 , 𝑧 〉 |
46 |
35 45 34
|
co |
⊢ ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝑓 ) 〈 𝑦 , 𝑧 〉 ) |
47 |
16 30
|
cfv |
⊢ ( Id ‘ 𝑑 ) |
48 |
28 47
|
cfv |
⊢ ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) |
49 |
37 48 46
|
co |
⊢ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝑓 ) 〈 𝑦 , 𝑧 〉 ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) |
50 |
24 17 49
|
cmpt |
⊢ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝑓 ) 〈 𝑦 , 𝑧 〉 ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) |
51 |
25 44 50
|
cmpt |
⊢ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝑓 ) 〈 𝑦 , 𝑧 〉 ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) |
52 |
11 15 14 14 51
|
cmpo |
⊢ ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝑓 ) 〈 𝑦 , 𝑧 〉 ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) ) |
53 |
42 52
|
cop |
⊢ 〈 ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ 〈 ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝑓 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 ) , ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝑓 ) 〈 𝑦 , 𝑧 〉 ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) ) 〉 |
54 |
10 9 53
|
csb |
⊢ ⦋ ( 2nd ‘ 𝑒 ) / 𝑑 ⦌ 〈 ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ 〈 ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝑓 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 ) , ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝑓 ) 〈 𝑦 , 𝑧 〉 ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) ) 〉 |
55 |
7 6 54
|
csb |
⊢ ⦋ ( 1st ‘ 𝑒 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑒 ) / 𝑑 ⦌ 〈 ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ 〈 ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝑓 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 ) , ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝑓 ) 〈 𝑦 , 𝑧 〉 ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) ) 〉 |
56 |
1 3 2 2 55
|
cmpo |
⊢ ( 𝑒 ∈ V , 𝑓 ∈ V ↦ ⦋ ( 1st ‘ 𝑒 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑒 ) / 𝑑 ⦌ 〈 ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ 〈 ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝑓 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 ) , ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝑓 ) 〈 𝑦 , 𝑧 〉 ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) ) 〉 ) |
57 |
0 56
|
wceq |
⊢ curryF = ( 𝑒 ∈ V , 𝑓 ∈ V ↦ ⦋ ( 1st ‘ 𝑒 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑒 ) / 𝑑 ⦌ 〈 ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ 〈 ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝑓 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 ) , ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝑓 ) 〈 𝑦 , 𝑧 〉 ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) ) 〉 ) |