Step |
Hyp |
Ref |
Expression |
1 |
|
uncfval.g |
⊢ 𝐹 = ( 〈“ 𝐶 𝐷 𝐸 ”〉 uncurryF 𝐺 ) |
2 |
|
uncfval.c |
⊢ ( 𝜑 → 𝐷 ∈ Cat ) |
3 |
|
uncfval.d |
⊢ ( 𝜑 → 𝐸 ∈ Cat ) |
4 |
|
uncfval.f |
⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) ) |
5 |
|
uncf1.a |
⊢ 𝐴 = ( Base ‘ 𝐶 ) |
6 |
|
uncf1.b |
⊢ 𝐵 = ( Base ‘ 𝐷 ) |
7 |
|
uncf1.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝐴 ) |
8 |
|
uncf1.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝐵 ) |
9 |
1 2 3 4
|
uncfval |
⊢ ( 𝜑 → 𝐹 = ( ( 𝐷 evalF 𝐸 ) ∘func ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) 〈,〉F ( 𝐶 2ndF 𝐷 ) ) ) ) |
10 |
9
|
fveq2d |
⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) = ( 1st ‘ ( ( 𝐷 evalF 𝐸 ) ∘func ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) 〈,〉F ( 𝐶 2ndF 𝐷 ) ) ) ) ) |
11 |
10
|
oveqd |
⊢ ( 𝜑 → ( 𝑋 ( 1st ‘ 𝐹 ) 𝑌 ) = ( 𝑋 ( 1st ‘ ( ( 𝐷 evalF 𝐸 ) ∘func ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) 〈,〉F ( 𝐶 2ndF 𝐷 ) ) ) ) 𝑌 ) ) |
12 |
|
df-ov |
⊢ ( 𝑋 ( 1st ‘ ( ( 𝐷 evalF 𝐸 ) ∘func ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) 〈,〉F ( 𝐶 2ndF 𝐷 ) ) ) ) 𝑌 ) = ( ( 1st ‘ ( ( 𝐷 evalF 𝐸 ) ∘func ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) 〈,〉F ( 𝐶 2ndF 𝐷 ) ) ) ) ‘ 〈 𝑋 , 𝑌 〉 ) |
13 |
|
eqid |
⊢ ( 𝐶 ×c 𝐷 ) = ( 𝐶 ×c 𝐷 ) |
14 |
13 5 6
|
xpcbas |
⊢ ( 𝐴 × 𝐵 ) = ( Base ‘ ( 𝐶 ×c 𝐷 ) ) |
15 |
|
eqid |
⊢ ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) 〈,〉F ( 𝐶 2ndF 𝐷 ) ) = ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) 〈,〉F ( 𝐶 2ndF 𝐷 ) ) |
16 |
|
eqid |
⊢ ( ( 𝐷 FuncCat 𝐸 ) ×c 𝐷 ) = ( ( 𝐷 FuncCat 𝐸 ) ×c 𝐷 ) |
17 |
|
funcrcl |
⊢ ( 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) → ( 𝐶 ∈ Cat ∧ ( 𝐷 FuncCat 𝐸 ) ∈ Cat ) ) |
18 |
4 17
|
syl |
⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ ( 𝐷 FuncCat 𝐸 ) ∈ Cat ) ) |
19 |
18
|
simpld |
⊢ ( 𝜑 → 𝐶 ∈ Cat ) |
20 |
|
eqid |
⊢ ( 𝐶 1stF 𝐷 ) = ( 𝐶 1stF 𝐷 ) |
21 |
13 19 2 20
|
1stfcl |
⊢ ( 𝜑 → ( 𝐶 1stF 𝐷 ) ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐶 ) ) |
22 |
21 4
|
cofucl |
⊢ ( 𝜑 → ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) ∈ ( ( 𝐶 ×c 𝐷 ) Func ( 𝐷 FuncCat 𝐸 ) ) ) |
23 |
|
eqid |
⊢ ( 𝐶 2ndF 𝐷 ) = ( 𝐶 2ndF 𝐷 ) |
24 |
13 19 2 23
|
2ndfcl |
⊢ ( 𝜑 → ( 𝐶 2ndF 𝐷 ) ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐷 ) ) |
25 |
15 16 22 24
|
prfcl |
⊢ ( 𝜑 → ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) 〈,〉F ( 𝐶 2ndF 𝐷 ) ) ∈ ( ( 𝐶 ×c 𝐷 ) Func ( ( 𝐷 FuncCat 𝐸 ) ×c 𝐷 ) ) ) |
26 |
|
eqid |
⊢ ( 𝐷 evalF 𝐸 ) = ( 𝐷 evalF 𝐸 ) |
27 |
|
eqid |
⊢ ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 ) |
28 |
26 27 2 3
|
evlfcl |
⊢ ( 𝜑 → ( 𝐷 evalF 𝐸 ) ∈ ( ( ( 𝐷 FuncCat 𝐸 ) ×c 𝐷 ) Func 𝐸 ) ) |
29 |
7 8
|
opelxpd |
⊢ ( 𝜑 → 〈 𝑋 , 𝑌 〉 ∈ ( 𝐴 × 𝐵 ) ) |
30 |
14 25 28 29
|
cofu1 |
⊢ ( 𝜑 → ( ( 1st ‘ ( ( 𝐷 evalF 𝐸 ) ∘func ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) 〈,〉F ( 𝐶 2ndF 𝐷 ) ) ) ) ‘ 〈 𝑋 , 𝑌 〉 ) = ( ( 1st ‘ ( 𝐷 evalF 𝐸 ) ) ‘ ( ( 1st ‘ ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) 〈,〉F ( 𝐶 2ndF 𝐷 ) ) ) ‘ 〈 𝑋 , 𝑌 〉 ) ) ) |
31 |
12 30
|
syl5eq |
⊢ ( 𝜑 → ( 𝑋 ( 1st ‘ ( ( 𝐷 evalF 𝐸 ) ∘func ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) 〈,〉F ( 𝐶 2ndF 𝐷 ) ) ) ) 𝑌 ) = ( ( 1st ‘ ( 𝐷 evalF 𝐸 ) ) ‘ ( ( 1st ‘ ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) 〈,〉F ( 𝐶 2ndF 𝐷 ) ) ) ‘ 〈 𝑋 , 𝑌 〉 ) ) ) |
32 |
|
eqid |
⊢ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) = ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) |
33 |
15 14 32 22 24 29
|
prf1 |
⊢ ( 𝜑 → ( ( 1st ‘ ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) 〈,〉F ( 𝐶 2ndF 𝐷 ) ) ) ‘ 〈 𝑋 , 𝑌 〉 ) = 〈 ( ( 1st ‘ ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) ) ‘ 〈 𝑋 , 𝑌 〉 ) , ( ( 1st ‘ ( 𝐶 2ndF 𝐷 ) ) ‘ 〈 𝑋 , 𝑌 〉 ) 〉 ) |
34 |
14 21 4 29
|
cofu1 |
⊢ ( 𝜑 → ( ( 1st ‘ ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) ) ‘ 〈 𝑋 , 𝑌 〉 ) = ( ( 1st ‘ 𝐺 ) ‘ ( ( 1st ‘ ( 𝐶 1stF 𝐷 ) ) ‘ 〈 𝑋 , 𝑌 〉 ) ) ) |
35 |
13 14 32 19 2 20 29
|
1stf1 |
⊢ ( 𝜑 → ( ( 1st ‘ ( 𝐶 1stF 𝐷 ) ) ‘ 〈 𝑋 , 𝑌 〉 ) = ( 1st ‘ 〈 𝑋 , 𝑌 〉 ) ) |
36 |
|
op1stg |
⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 1st ‘ 〈 𝑋 , 𝑌 〉 ) = 𝑋 ) |
37 |
7 8 36
|
syl2anc |
⊢ ( 𝜑 → ( 1st ‘ 〈 𝑋 , 𝑌 〉 ) = 𝑋 ) |
38 |
35 37
|
eqtrd |
⊢ ( 𝜑 → ( ( 1st ‘ ( 𝐶 1stF 𝐷 ) ) ‘ 〈 𝑋 , 𝑌 〉 ) = 𝑋 ) |
39 |
38
|
fveq2d |
⊢ ( 𝜑 → ( ( 1st ‘ 𝐺 ) ‘ ( ( 1st ‘ ( 𝐶 1stF 𝐷 ) ) ‘ 〈 𝑋 , 𝑌 〉 ) ) = ( ( 1st ‘ 𝐺 ) ‘ 𝑋 ) ) |
40 |
34 39
|
eqtrd |
⊢ ( 𝜑 → ( ( 1st ‘ ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) ) ‘ 〈 𝑋 , 𝑌 〉 ) = ( ( 1st ‘ 𝐺 ) ‘ 𝑋 ) ) |
41 |
13 14 32 19 2 23 29
|
2ndf1 |
⊢ ( 𝜑 → ( ( 1st ‘ ( 𝐶 2ndF 𝐷 ) ) ‘ 〈 𝑋 , 𝑌 〉 ) = ( 2nd ‘ 〈 𝑋 , 𝑌 〉 ) ) |
42 |
|
op2ndg |
⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 2nd ‘ 〈 𝑋 , 𝑌 〉 ) = 𝑌 ) |
43 |
7 8 42
|
syl2anc |
⊢ ( 𝜑 → ( 2nd ‘ 〈 𝑋 , 𝑌 〉 ) = 𝑌 ) |
44 |
41 43
|
eqtrd |
⊢ ( 𝜑 → ( ( 1st ‘ ( 𝐶 2ndF 𝐷 ) ) ‘ 〈 𝑋 , 𝑌 〉 ) = 𝑌 ) |
45 |
40 44
|
opeq12d |
⊢ ( 𝜑 → 〈 ( ( 1st ‘ ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) ) ‘ 〈 𝑋 , 𝑌 〉 ) , ( ( 1st ‘ ( 𝐶 2ndF 𝐷 ) ) ‘ 〈 𝑋 , 𝑌 〉 ) 〉 = 〈 ( ( 1st ‘ 𝐺 ) ‘ 𝑋 ) , 𝑌 〉 ) |
46 |
33 45
|
eqtrd |
⊢ ( 𝜑 → ( ( 1st ‘ ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) 〈,〉F ( 𝐶 2ndF 𝐷 ) ) ) ‘ 〈 𝑋 , 𝑌 〉 ) = 〈 ( ( 1st ‘ 𝐺 ) ‘ 𝑋 ) , 𝑌 〉 ) |
47 |
46
|
fveq2d |
⊢ ( 𝜑 → ( ( 1st ‘ ( 𝐷 evalF 𝐸 ) ) ‘ ( ( 1st ‘ ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) 〈,〉F ( 𝐶 2ndF 𝐷 ) ) ) ‘ 〈 𝑋 , 𝑌 〉 ) ) = ( ( 1st ‘ ( 𝐷 evalF 𝐸 ) ) ‘ 〈 ( ( 1st ‘ 𝐺 ) ‘ 𝑋 ) , 𝑌 〉 ) ) |
48 |
|
df-ov |
⊢ ( ( ( 1st ‘ 𝐺 ) ‘ 𝑋 ) ( 1st ‘ ( 𝐷 evalF 𝐸 ) ) 𝑌 ) = ( ( 1st ‘ ( 𝐷 evalF 𝐸 ) ) ‘ 〈 ( ( 1st ‘ 𝐺 ) ‘ 𝑋 ) , 𝑌 〉 ) |
49 |
47 48
|
eqtr4di |
⊢ ( 𝜑 → ( ( 1st ‘ ( 𝐷 evalF 𝐸 ) ) ‘ ( ( 1st ‘ ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) 〈,〉F ( 𝐶 2ndF 𝐷 ) ) ) ‘ 〈 𝑋 , 𝑌 〉 ) ) = ( ( ( 1st ‘ 𝐺 ) ‘ 𝑋 ) ( 1st ‘ ( 𝐷 evalF 𝐸 ) ) 𝑌 ) ) |
50 |
27
|
fucbas |
⊢ ( 𝐷 Func 𝐸 ) = ( Base ‘ ( 𝐷 FuncCat 𝐸 ) ) |
51 |
|
relfunc |
⊢ Rel ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) |
52 |
|
1st2ndbr |
⊢ ( ( Rel ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) ∧ 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) ) → ( 1st ‘ 𝐺 ) ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) ( 2nd ‘ 𝐺 ) ) |
53 |
51 4 52
|
sylancr |
⊢ ( 𝜑 → ( 1st ‘ 𝐺 ) ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) ( 2nd ‘ 𝐺 ) ) |
54 |
5 50 53
|
funcf1 |
⊢ ( 𝜑 → ( 1st ‘ 𝐺 ) : 𝐴 ⟶ ( 𝐷 Func 𝐸 ) ) |
55 |
54 7
|
ffvelrnd |
⊢ ( 𝜑 → ( ( 1st ‘ 𝐺 ) ‘ 𝑋 ) ∈ ( 𝐷 Func 𝐸 ) ) |
56 |
26 2 3 6 55 8
|
evlf1 |
⊢ ( 𝜑 → ( ( ( 1st ‘ 𝐺 ) ‘ 𝑋 ) ( 1st ‘ ( 𝐷 evalF 𝐸 ) ) 𝑌 ) = ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑌 ) ) |
57 |
49 56
|
eqtrd |
⊢ ( 𝜑 → ( ( 1st ‘ ( 𝐷 evalF 𝐸 ) ) ‘ ( ( 1st ‘ ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) 〈,〉F ( 𝐶 2ndF 𝐷 ) ) ) ‘ 〈 𝑋 , 𝑌 〉 ) ) = ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑌 ) ) |
58 |
11 31 57
|
3eqtrd |
⊢ ( 𝜑 → ( 𝑋 ( 1st ‘ 𝐹 ) 𝑌 ) = ( ( 1st ‘ ( ( 1st ‘ 𝐺 ) ‘ 𝑋 ) ) ‘ 𝑌 ) ) |