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 |
|
eqid |
⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 ) |
10 |
|
eqid |
⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 ) |
11 |
1 2 3 4 5 6 7 8 9 10
|
curfval |
⊢ ( 𝜑 → 𝐺 = 〈 ( 𝑥 ∈ 𝐴 ↦ 〈 ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝐹 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 ) , ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝐹 ) 〈 𝑦 , 𝑧 〉 ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) 〉 ) |
12 |
2
|
fvexi |
⊢ 𝐴 ∈ V |
13 |
12
|
mptex |
⊢ ( 𝑥 ∈ 𝐴 ↦ 〈 ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝐹 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 ) ∈ V |
14 |
12 12
|
mpoex |
⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝐹 ) 〈 𝑦 , 𝑧 〉 ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) ∈ V |
15 |
13 14
|
op1std |
⊢ ( 𝐺 = 〈 ( 𝑥 ∈ 𝐴 ↦ 〈 ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝐹 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 ) , ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐴 ↦ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ( 〈 𝑥 , 𝑧 〉 ( 2nd ‘ 𝐹 ) 〈 𝑦 , 𝑧 〉 ) ( ( Id ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) ) 〉 → ( 1st ‘ 𝐺 ) = ( 𝑥 ∈ 𝐴 ↦ 〈 ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝐹 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 ) ) |
16 |
11 15
|
syl |
⊢ ( 𝜑 → ( 1st ‘ 𝐺 ) = ( 𝑥 ∈ 𝐴 ↦ 〈 ( 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( 1st ‘ 𝐹 ) 𝑦 ) ) , ( 𝑦 ∈ 𝐵 , 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ↦ ( ( 1 ‘ 𝑥 ) ( 〈 𝑥 , 𝑦 〉 ( 2nd ‘ 𝐹 ) 〈 𝑥 , 𝑧 〉 ) 𝑔 ) ) ) 〉 ) ) |