Step |
Hyp |
Ref |
Expression |
1 |
|
curfval.g |
⊢ 𝐺 = ( 〈 𝐶 , 𝐷 〉 curryF 𝐹 ) |
2 |
|
curfval.a |
⊢ 𝐴 = ( Base ‘ 𝐶 ) |
3 |
|
curfval.c |
⊢ ( 𝜑 → 𝐶 ∈ Cat ) |
4 |
|
curfval.d |
⊢ ( 𝜑 → 𝐷 ∈ Cat ) |
5 |
|
curfval.f |
⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) ) |
6 |
|
curfval.b |
⊢ 𝐵 = ( Base ‘ 𝐷 ) |
7 |
|
curfval.j |
⊢ 𝐽 = ( Hom ‘ 𝐷 ) |
8 |
|
curfval.1 |
⊢ 1 = ( Id ‘ 𝐶 ) |
9 |
|
curfval.h |
⊢ 𝐻 = ( Hom ‘ 𝐶 ) |
10 |
|
curfval.i |
⊢ 𝐼 = ( Id ‘ 𝐷 ) |
11 |
|
df-curf |
⊢ curryF = ( 𝑒 ∈ V , 𝑓 ∈ V ↦ ⦋ ( 1st ‘ 𝑒 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑒 ) / 𝑑 ⦌ 〈 ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ 〈 ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝑓 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 ) , ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝑓 ) 〈 𝑦 , 𝑧 〉 ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) ) 〉 ) |
12 |
11
|
a1i |
⊢ ( 𝜑 → curryF = ( 𝑒 ∈ V , 𝑓 ∈ V ↦ ⦋ ( 1st ‘ 𝑒 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑒 ) / 𝑑 ⦌ 〈 ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ 〈 ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝑓 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 ) , ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝑓 ) 〈 𝑦 , 𝑧 〉 ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) ) 〉 ) ) |
13 |
|
fvexd |
⊢ ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) → ( 1st ‘ 𝑒 ) ∈ V ) |
14 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) → 𝑒 = 〈 𝐶 , 𝐷 〉 ) |
15 |
14
|
fveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) → ( 1st ‘ 𝑒 ) = ( 1st ‘ 〈 𝐶 , 𝐷 〉 ) ) |
16 |
|
op1stg |
⊢ ( ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 1st ‘ 〈 𝐶 , 𝐷 〉 ) = 𝐶 ) |
17 |
3 4 16
|
syl2anc |
⊢ ( 𝜑 → ( 1st ‘ 〈 𝐶 , 𝐷 〉 ) = 𝐶 ) |
18 |
17
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) → ( 1st ‘ 〈 𝐶 , 𝐷 〉 ) = 𝐶 ) |
19 |
15 18
|
eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) → ( 1st ‘ 𝑒 ) = 𝐶 ) |
20 |
|
fvexd |
⊢ ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) → ( 2nd ‘ 𝑒 ) ∈ V ) |
21 |
14
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) → 𝑒 = 〈 𝐶 , 𝐷 〉 ) |
22 |
21
|
fveq2d |
⊢ ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) → ( 2nd ‘ 𝑒 ) = ( 2nd ‘ 〈 𝐶 , 𝐷 〉 ) ) |
23 |
|
op2ndg |
⊢ ( ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 2nd ‘ 〈 𝐶 , 𝐷 〉 ) = 𝐷 ) |
24 |
3 4 23
|
syl2anc |
⊢ ( 𝜑 → ( 2nd ‘ 〈 𝐶 , 𝐷 〉 ) = 𝐷 ) |
25 |
24
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) → ( 2nd ‘ 〈 𝐶 , 𝐷 〉 ) = 𝐷 ) |
26 |
22 25
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) → ( 2nd ‘ 𝑒 ) = 𝐷 ) |
27 |
|
simplr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → 𝑐 = 𝐶 ) |
28 |
27
|
fveq2d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) ) |
29 |
28 2
|
eqtr4di |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( Base ‘ 𝑐 ) = 𝐴 ) |
30 |
|
simpr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → 𝑑 = 𝐷 ) |
31 |
30
|
fveq2d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( Base ‘ 𝑑 ) = ( Base ‘ 𝐷 ) ) |
32 |
31 6
|
eqtr4di |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( Base ‘ 𝑑 ) = 𝐵 ) |
33 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) → 𝑓 = 𝐹 ) |
34 |
33
|
ad2antrr |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → 𝑓 = 𝐹 ) |
35 |
34
|
fveq2d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 1st ‘ 𝑓 ) = ( 1st ‘ 𝐹 ) ) |
36 |
35
|
oveqd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) = ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) |
37 |
32 36
|
mpteq12dv |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) ) |
38 |
30
|
fveq2d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( Hom ‘ 𝑑 ) = ( Hom ‘ 𝐷 ) ) |
39 |
38 7
|
eqtr4di |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( Hom ‘ 𝑑 ) = 𝐽 ) |
40 |
39
|
oveqd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) = ( 𝑦 𝐽 𝑧 ) ) |
41 |
34
|
fveq2d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 2nd ‘ 𝑓 ) = ( 2nd ‘ 𝐹 ) ) |
42 |
41
|
oveqd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝑓 ) 〈 𝑥 , 𝑧 〉 ) = ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝐹 ) 〈 𝑥 , 𝑧 〉 ) ) |
43 |
27
|
fveq2d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( Id ‘ 𝑐 ) = ( Id ‘ 𝐶 ) ) |
44 |
43 8
|
eqtr4di |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( Id ‘ 𝑐 ) = 1 ) |
45 |
44
|
fveq1d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) = ( 1 ‘ 𝑥 ) ) |
46 |
|
eqidd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → 𝑔 = 𝑔 ) |
47 |
42 45 46
|
oveq123d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝑓 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) = ( ( 1 ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝐹 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) |
48 |
40 47
|
mpteq12dv |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝑓 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) = ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝐹 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) |
49 |
32 32 48
|
mpoeq123dv |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝑓 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) = ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝐹 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) ) |
50 |
37 49
|
opeq12d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → 〈 ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝑓 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 = 〈 ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝐹 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 ) |
51 |
29 50
|
mpteq12dv |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ 〈 ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝑓 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 ) = ( 𝑥 ∈ 𝐴 ↦ 〈 ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝐹 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 ) ) |
52 |
27
|
fveq2d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( Hom ‘ 𝑐 ) = ( Hom ‘ 𝐶 ) ) |
53 |
52 9
|
eqtr4di |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( Hom ‘ 𝑐 ) = 𝐻 ) |
54 |
53
|
oveqd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) = ( 𝑥 𝐻 𝑦 ) ) |
55 |
41
|
oveqd |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝑓 ) 〈 𝑦 , 𝑧 〉 ) = ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝐹 ) 〈 𝑦 , 𝑧 〉 ) ) |
56 |
30
|
fveq2d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( Id ‘ 𝑑 ) = ( Id ‘ 𝐷 ) ) |
57 |
56 10
|
eqtr4di |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( Id ‘ 𝑑 ) = 𝐼 ) |
58 |
57
|
fveq1d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) = ( 𝐼 ‘ 𝑧 ) ) |
59 |
55 46 58
|
oveq123d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝑓 ) 〈 𝑦 , 𝑧 〉 ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) = ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝐹 ) 〈 𝑦 , 𝑧 〉 ) ( 𝐼 ‘ 𝑧 ) ) ) |
60 |
32 59
|
mpteq12dv |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝑓 ) 〈 𝑦 , 𝑧 〉 ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) = ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝐹 ) 〈 𝑦 , 𝑧 〉 ) ( 𝐼 ‘ 𝑧 ) ) ) ) |
61 |
54 60
|
mpteq12dv |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝑓 ) 〈 𝑦 , 𝑧 〉 ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) = ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝐹 ) 〈 𝑦 , 𝑧 〉 ) ( 𝐼 ‘ 𝑧 ) ) ) ) ) |
62 |
29 29 61
|
mpoeq123dv |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝑓 ) 〈 𝑦 , 𝑧 〉 ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝐹 ) 〈 𝑦 , 𝑧 〉 ) ( 𝐼 ‘ 𝑧 ) ) ) ) ) ) |
63 |
51 62
|
opeq12d |
⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → 〈 ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ 〈 ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝑓 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 ) , ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝑓 ) 〈 𝑦 , 𝑧 〉 ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) ) 〉 = 〈 ( 𝑥 ∈ 𝐴 ↦ 〈 ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝐹 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 ) , ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝐹 ) 〈 𝑦 , 𝑧 〉 ) ( 𝐼 ‘ 𝑧 ) ) ) ) ) 〉 ) |
64 |
20 26 63
|
csbied2 |
⊢ ( ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑐 = 𝐶 ) → ⦋ ( 2nd ‘ 𝑒 ) / 𝑑 ⦌ 〈 ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ 〈 ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝑓 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 ) , ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝑓 ) 〈 𝑦 , 𝑧 〉 ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) ) 〉 = 〈 ( 𝑥 ∈ 𝐴 ↦ 〈 ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝐹 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 ) , ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝐹 ) 〈 𝑦 , 𝑧 〉 ) ( 𝐼 ‘ 𝑧 ) ) ) ) ) 〉 ) |
65 |
13 19 64
|
csbied2 |
⊢ ( ( 𝜑 ∧ ( 𝑒 = 〈 𝐶 , 𝐷 〉 ∧ 𝑓 = 𝐹 ) ) → ⦋ ( 1st ‘ 𝑒 ) / 𝑐 ⦌ ⦋ ( 2nd ‘ 𝑒 ) / 𝑑 ⦌ 〈 ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ 〈 ( 𝑦 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑥 ( 1st ‘ 𝑓 ) 𝑦 ) ) , ( 𝑦 ∈ ( Base ‘ 𝑑 ) , 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝑑 ) 𝑧 ) ↦ ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝑓 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 ) , ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ↦ ( 𝑧 ∈ ( Base ‘ 𝑑 ) ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝑓 ) 〈 𝑦 , 𝑧 〉 ) ( ( Id ‘ 𝑑 ) ‘ 𝑧 ) ) ) ) ) 〉 = 〈 ( 𝑥 ∈ 𝐴 ↦ 〈 ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝐹 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 ) , ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝐹 ) 〈 𝑦 , 𝑧 〉 ) ( 𝐼 ‘ 𝑧 ) ) ) ) ) 〉 ) |
66 |
|
opex |
⊢ 〈 𝐶 , 𝐷 〉 ∈ V |
67 |
66
|
a1i |
⊢ ( 𝜑 → 〈 𝐶 , 𝐷 〉 ∈ V ) |
68 |
5
|
elexd |
⊢ ( 𝜑 → 𝐹 ∈ V ) |
69 |
|
opex |
⊢ 〈 ( 𝑥 ∈ 𝐴 ↦ 〈 ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝐹 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 ) , ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝐹 ) 〈 𝑦 , 𝑧 〉 ) ( 𝐼 ‘ 𝑧 ) ) ) ) ) 〉 ∈ V |
70 |
69
|
a1i |
⊢ ( 𝜑 → 〈 ( 𝑥 ∈ 𝐴 ↦ 〈 ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝐹 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 ) , ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝐹 ) 〈 𝑦 , 𝑧 〉 ) ( 𝐼 ‘ 𝑧 ) ) ) ) ) 〉 ∈ V ) |
71 |
12 65 67 68 70
|
ovmpod |
⊢ ( 𝜑 → ( 〈 𝐶 , 𝐷 〉 curryF 𝐹 ) = 〈 ( 𝑥 ∈ 𝐴 ↦ 〈 ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝐹 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 ) , ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝐹 ) 〈 𝑦 , 𝑧 〉 ) ( 𝐼 ‘ 𝑧 ) ) ) ) ) 〉 ) |
72 |
1 71
|
syl5eq |
⊢ ( 𝜑 → 𝐺 = 〈 ( 𝑥 ∈ 𝐴 ↦ 〈 ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝐹 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 ) , ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 𝐻 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝐹 ) 〈 𝑦 , 𝑧 〉 ) ( 𝐼 ‘ 𝑧 ) ) ) ) ) 〉 ) |