Step |
Hyp |
Ref |
Expression |
1 |
|
yoneda.y |
⊢ 𝑌 = ( Yon ‘ 𝐶 ) |
2 |
|
yoneda.b |
⊢ 𝐵 = ( Base ‘ 𝐶 ) |
3 |
|
yoneda.1 |
⊢ 1 = ( Id ‘ 𝐶 ) |
4 |
|
yoneda.o |
⊢ 𝑂 = ( oppCat ‘ 𝐶 ) |
5 |
|
yoneda.s |
⊢ 𝑆 = ( SetCat ‘ 𝑈 ) |
6 |
|
yoneda.t |
⊢ 𝑇 = ( SetCat ‘ 𝑉 ) |
7 |
|
yoneda.q |
⊢ 𝑄 = ( 𝑂 FuncCat 𝑆 ) |
8 |
|
yoneda.h |
⊢ 𝐻 = ( HomF ‘ 𝑄 ) |
9 |
|
yoneda.r |
⊢ 𝑅 = ( ( 𝑄 ×c 𝑂 ) FuncCat 𝑇 ) |
10 |
|
yoneda.e |
⊢ 𝐸 = ( 𝑂 evalF 𝑆 ) |
11 |
|
yoneda.z |
⊢ 𝑍 = ( 𝐻 ∘func ( ( 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ∘func ( 𝑄 2ndF 𝑂 ) ) 〈,〉F ( 𝑄 1stF 𝑂 ) ) ) |
12 |
|
yoneda.c |
⊢ ( 𝜑 → 𝐶 ∈ Cat ) |
13 |
|
yoneda.w |
⊢ ( 𝜑 → 𝑉 ∈ 𝑊 ) |
14 |
|
yoneda.u |
⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ⊆ 𝑈 ) |
15 |
|
yoneda.v |
⊢ ( 𝜑 → ( ran ( Homf ‘ 𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 ) |
16 |
|
yonedalem21.f |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝑂 Func 𝑆 ) ) |
17 |
|
yonedalem21.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) |
18 |
11
|
fveq2i |
⊢ ( 1st ‘ 𝑍 ) = ( 1st ‘ ( 𝐻 ∘func ( ( 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ∘func ( 𝑄 2ndF 𝑂 ) ) 〈,〉F ( 𝑄 1stF 𝑂 ) ) ) ) |
19 |
18
|
oveqi |
⊢ ( 𝐹 ( 1st ‘ 𝑍 ) 𝑋 ) = ( 𝐹 ( 1st ‘ ( 𝐻 ∘func ( ( 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ∘func ( 𝑄 2ndF 𝑂 ) ) 〈,〉F ( 𝑄 1stF 𝑂 ) ) ) ) 𝑋 ) |
20 |
|
df-ov |
⊢ ( 𝐹 ( 1st ‘ ( 𝐻 ∘func ( ( 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ∘func ( 𝑄 2ndF 𝑂 ) ) 〈,〉F ( 𝑄 1stF 𝑂 ) ) ) ) 𝑋 ) = ( ( 1st ‘ ( 𝐻 ∘func ( ( 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ∘func ( 𝑄 2ndF 𝑂 ) ) 〈,〉F ( 𝑄 1stF 𝑂 ) ) ) ) ‘ 〈 𝐹 , 𝑋 〉 ) |
21 |
19 20
|
eqtri |
⊢ ( 𝐹 ( 1st ‘ 𝑍 ) 𝑋 ) = ( ( 1st ‘ ( 𝐻 ∘func ( ( 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ∘func ( 𝑄 2ndF 𝑂 ) ) 〈,〉F ( 𝑄 1stF 𝑂 ) ) ) ) ‘ 〈 𝐹 , 𝑋 〉 ) |
22 |
|
eqid |
⊢ ( 𝑄 ×c 𝑂 ) = ( 𝑄 ×c 𝑂 ) |
23 |
7
|
fucbas |
⊢ ( 𝑂 Func 𝑆 ) = ( Base ‘ 𝑄 ) |
24 |
4 2
|
oppcbas |
⊢ 𝐵 = ( Base ‘ 𝑂 ) |
25 |
22 23 24
|
xpcbas |
⊢ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) = ( Base ‘ ( 𝑄 ×c 𝑂 ) ) |
26 |
|
eqid |
⊢ ( ( 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ∘func ( 𝑄 2ndF 𝑂 ) ) 〈,〉F ( 𝑄 1stF 𝑂 ) ) = ( ( 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ∘func ( 𝑄 2ndF 𝑂 ) ) 〈,〉F ( 𝑄 1stF 𝑂 ) ) |
27 |
|
eqid |
⊢ ( ( oppCat ‘ 𝑄 ) ×c 𝑄 ) = ( ( oppCat ‘ 𝑄 ) ×c 𝑄 ) |
28 |
4
|
oppccat |
⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat ) |
29 |
12 28
|
syl |
⊢ ( 𝜑 → 𝑂 ∈ Cat ) |
30 |
15
|
unssbd |
⊢ ( 𝜑 → 𝑈 ⊆ 𝑉 ) |
31 |
13 30
|
ssexd |
⊢ ( 𝜑 → 𝑈 ∈ V ) |
32 |
5
|
setccat |
⊢ ( 𝑈 ∈ V → 𝑆 ∈ Cat ) |
33 |
31 32
|
syl |
⊢ ( 𝜑 → 𝑆 ∈ Cat ) |
34 |
7 29 33
|
fuccat |
⊢ ( 𝜑 → 𝑄 ∈ Cat ) |
35 |
|
eqid |
⊢ ( 𝑄 2ndF 𝑂 ) = ( 𝑄 2ndF 𝑂 ) |
36 |
22 34 29 35
|
2ndfcl |
⊢ ( 𝜑 → ( 𝑄 2ndF 𝑂 ) ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑂 ) ) |
37 |
|
eqid |
⊢ ( oppCat ‘ 𝑄 ) = ( oppCat ‘ 𝑄 ) |
38 |
|
relfunc |
⊢ Rel ( 𝐶 Func 𝑄 ) |
39 |
1 12 4 5 7 31 14
|
yoncl |
⊢ ( 𝜑 → 𝑌 ∈ ( 𝐶 Func 𝑄 ) ) |
40 |
|
1st2ndbr |
⊢ ( ( Rel ( 𝐶 Func 𝑄 ) ∧ 𝑌 ∈ ( 𝐶 Func 𝑄 ) ) → ( 1st ‘ 𝑌 ) ( 𝐶 Func 𝑄 ) ( 2nd ‘ 𝑌 ) ) |
41 |
38 39 40
|
sylancr |
⊢ ( 𝜑 → ( 1st ‘ 𝑌 ) ( 𝐶 Func 𝑄 ) ( 2nd ‘ 𝑌 ) ) |
42 |
4 37 41
|
funcoppc |
⊢ ( 𝜑 → ( 1st ‘ 𝑌 ) ( 𝑂 Func ( oppCat ‘ 𝑄 ) ) tpos ( 2nd ‘ 𝑌 ) ) |
43 |
|
df-br |
⊢ ( ( 1st ‘ 𝑌 ) ( 𝑂 Func ( oppCat ‘ 𝑄 ) ) tpos ( 2nd ‘ 𝑌 ) ↔ 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ∈ ( 𝑂 Func ( oppCat ‘ 𝑄 ) ) ) |
44 |
42 43
|
sylib |
⊢ ( 𝜑 → 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ∈ ( 𝑂 Func ( oppCat ‘ 𝑄 ) ) ) |
45 |
36 44
|
cofucl |
⊢ ( 𝜑 → ( 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ∘func ( 𝑄 2ndF 𝑂 ) ) ∈ ( ( 𝑄 ×c 𝑂 ) Func ( oppCat ‘ 𝑄 ) ) ) |
46 |
|
eqid |
⊢ ( 𝑄 1stF 𝑂 ) = ( 𝑄 1stF 𝑂 ) |
47 |
22 34 29 46
|
1stfcl |
⊢ ( 𝜑 → ( 𝑄 1stF 𝑂 ) ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑄 ) ) |
48 |
26 27 45 47
|
prfcl |
⊢ ( 𝜑 → ( ( 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ∘func ( 𝑄 2ndF 𝑂 ) ) 〈,〉F ( 𝑄 1stF 𝑂 ) ) ∈ ( ( 𝑄 ×c 𝑂 ) Func ( ( oppCat ‘ 𝑄 ) ×c 𝑄 ) ) ) |
49 |
15
|
unssad |
⊢ ( 𝜑 → ran ( Homf ‘ 𝑄 ) ⊆ 𝑉 ) |
50 |
8 37 6 34 13 49
|
hofcl |
⊢ ( 𝜑 → 𝐻 ∈ ( ( ( oppCat ‘ 𝑄 ) ×c 𝑄 ) Func 𝑇 ) ) |
51 |
16 17
|
opelxpd |
⊢ ( 𝜑 → 〈 𝐹 , 𝑋 〉 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ) |
52 |
25 48 50 51
|
cofu1 |
⊢ ( 𝜑 → ( ( 1st ‘ ( 𝐻 ∘func ( ( 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ∘func ( 𝑄 2ndF 𝑂 ) ) 〈,〉F ( 𝑄 1stF 𝑂 ) ) ) ) ‘ 〈 𝐹 , 𝑋 〉 ) = ( ( 1st ‘ 𝐻 ) ‘ ( ( 1st ‘ ( ( 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ∘func ( 𝑄 2ndF 𝑂 ) ) 〈,〉F ( 𝑄 1stF 𝑂 ) ) ) ‘ 〈 𝐹 , 𝑋 〉 ) ) ) |
53 |
21 52
|
eqtrid |
⊢ ( 𝜑 → ( 𝐹 ( 1st ‘ 𝑍 ) 𝑋 ) = ( ( 1st ‘ 𝐻 ) ‘ ( ( 1st ‘ ( ( 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ∘func ( 𝑄 2ndF 𝑂 ) ) 〈,〉F ( 𝑄 1stF 𝑂 ) ) ) ‘ 〈 𝐹 , 𝑋 〉 ) ) ) |
54 |
|
eqid |
⊢ ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) = ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) |
55 |
26 25 54 45 47 51
|
prf1 |
⊢ ( 𝜑 → ( ( 1st ‘ ( ( 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ∘func ( 𝑄 2ndF 𝑂 ) ) 〈,〉F ( 𝑄 1stF 𝑂 ) ) ) ‘ 〈 𝐹 , 𝑋 〉 ) = 〈 ( ( 1st ‘ ( 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ∘func ( 𝑄 2ndF 𝑂 ) ) ) ‘ 〈 𝐹 , 𝑋 〉 ) , ( ( 1st ‘ ( 𝑄 1stF 𝑂 ) ) ‘ 〈 𝐹 , 𝑋 〉 ) 〉 ) |
56 |
25 36 44 51
|
cofu1 |
⊢ ( 𝜑 → ( ( 1st ‘ ( 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ∘func ( 𝑄 2ndF 𝑂 ) ) ) ‘ 〈 𝐹 , 𝑋 〉 ) = ( ( 1st ‘ 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ) ‘ ( ( 1st ‘ ( 𝑄 2ndF 𝑂 ) ) ‘ 〈 𝐹 , 𝑋 〉 ) ) ) |
57 |
|
fvex |
⊢ ( 1st ‘ 𝑌 ) ∈ V |
58 |
|
fvex |
⊢ ( 2nd ‘ 𝑌 ) ∈ V |
59 |
58
|
tposex |
⊢ tpos ( 2nd ‘ 𝑌 ) ∈ V |
60 |
57 59
|
op1st |
⊢ ( 1st ‘ 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ) = ( 1st ‘ 𝑌 ) |
61 |
60
|
a1i |
⊢ ( 𝜑 → ( 1st ‘ 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ) = ( 1st ‘ 𝑌 ) ) |
62 |
22 25 54 34 29 35 51
|
2ndf1 |
⊢ ( 𝜑 → ( ( 1st ‘ ( 𝑄 2ndF 𝑂 ) ) ‘ 〈 𝐹 , 𝑋 〉 ) = ( 2nd ‘ 〈 𝐹 , 𝑋 〉 ) ) |
63 |
|
op2ndg |
⊢ ( ( 𝐹 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑋 ∈ 𝐵 ) → ( 2nd ‘ 〈 𝐹 , 𝑋 〉 ) = 𝑋 ) |
64 |
16 17 63
|
syl2anc |
⊢ ( 𝜑 → ( 2nd ‘ 〈 𝐹 , 𝑋 〉 ) = 𝑋 ) |
65 |
62 64
|
eqtrd |
⊢ ( 𝜑 → ( ( 1st ‘ ( 𝑄 2ndF 𝑂 ) ) ‘ 〈 𝐹 , 𝑋 〉 ) = 𝑋 ) |
66 |
61 65
|
fveq12d |
⊢ ( 𝜑 → ( ( 1st ‘ 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ) ‘ ( ( 1st ‘ ( 𝑄 2ndF 𝑂 ) ) ‘ 〈 𝐹 , 𝑋 〉 ) ) = ( ( 1st ‘ 𝑌 ) ‘ 𝑋 ) ) |
67 |
56 66
|
eqtrd |
⊢ ( 𝜑 → ( ( 1st ‘ ( 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ∘func ( 𝑄 2ndF 𝑂 ) ) ) ‘ 〈 𝐹 , 𝑋 〉 ) = ( ( 1st ‘ 𝑌 ) ‘ 𝑋 ) ) |
68 |
22 25 54 34 29 46 51
|
1stf1 |
⊢ ( 𝜑 → ( ( 1st ‘ ( 𝑄 1stF 𝑂 ) ) ‘ 〈 𝐹 , 𝑋 〉 ) = ( 1st ‘ 〈 𝐹 , 𝑋 〉 ) ) |
69 |
|
op1stg |
⊢ ( ( 𝐹 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑋 ∈ 𝐵 ) → ( 1st ‘ 〈 𝐹 , 𝑋 〉 ) = 𝐹 ) |
70 |
16 17 69
|
syl2anc |
⊢ ( 𝜑 → ( 1st ‘ 〈 𝐹 , 𝑋 〉 ) = 𝐹 ) |
71 |
68 70
|
eqtrd |
⊢ ( 𝜑 → ( ( 1st ‘ ( 𝑄 1stF 𝑂 ) ) ‘ 〈 𝐹 , 𝑋 〉 ) = 𝐹 ) |
72 |
67 71
|
opeq12d |
⊢ ( 𝜑 → 〈 ( ( 1st ‘ ( 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ∘func ( 𝑄 2ndF 𝑂 ) ) ) ‘ 〈 𝐹 , 𝑋 〉 ) , ( ( 1st ‘ ( 𝑄 1stF 𝑂 ) ) ‘ 〈 𝐹 , 𝑋 〉 ) 〉 = 〈 ( ( 1st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 〉 ) |
73 |
55 72
|
eqtrd |
⊢ ( 𝜑 → ( ( 1st ‘ ( ( 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ∘func ( 𝑄 2ndF 𝑂 ) ) 〈,〉F ( 𝑄 1stF 𝑂 ) ) ) ‘ 〈 𝐹 , 𝑋 〉 ) = 〈 ( ( 1st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 〉 ) |
74 |
73
|
fveq2d |
⊢ ( 𝜑 → ( ( 1st ‘ 𝐻 ) ‘ ( ( 1st ‘ ( ( 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ∘func ( 𝑄 2ndF 𝑂 ) ) 〈,〉F ( 𝑄 1stF 𝑂 ) ) ) ‘ 〈 𝐹 , 𝑋 〉 ) ) = ( ( 1st ‘ 𝐻 ) ‘ 〈 ( ( 1st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 〉 ) ) |
75 |
|
df-ov |
⊢ ( ( ( 1st ‘ 𝑌 ) ‘ 𝑋 ) ( 1st ‘ 𝐻 ) 𝐹 ) = ( ( 1st ‘ 𝐻 ) ‘ 〈 ( ( 1st ‘ 𝑌 ) ‘ 𝑋 ) , 𝐹 〉 ) |
76 |
74 75
|
eqtr4di |
⊢ ( 𝜑 → ( ( 1st ‘ 𝐻 ) ‘ ( ( 1st ‘ ( ( 〈 ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) 〉 ∘func ( 𝑄 2ndF 𝑂 ) ) 〈,〉F ( 𝑄 1stF 𝑂 ) ) ) ‘ 〈 𝐹 , 𝑋 〉 ) ) = ( ( ( 1st ‘ 𝑌 ) ‘ 𝑋 ) ( 1st ‘ 𝐻 ) 𝐹 ) ) |
77 |
|
eqid |
⊢ ( 𝑂 Nat 𝑆 ) = ( 𝑂 Nat 𝑆 ) |
78 |
7 77
|
fuchom |
⊢ ( 𝑂 Nat 𝑆 ) = ( Hom ‘ 𝑄 ) |
79 |
1 2 12 17 4 5 31 14
|
yon1cl |
⊢ ( 𝜑 → ( ( 1st ‘ 𝑌 ) ‘ 𝑋 ) ∈ ( 𝑂 Func 𝑆 ) ) |
80 |
8 34 23 78 79 16
|
hof1 |
⊢ ( 𝜑 → ( ( ( 1st ‘ 𝑌 ) ‘ 𝑋 ) ( 1st ‘ 𝐻 ) 𝐹 ) = ( ( ( 1st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) |
81 |
53 76 80
|
3eqtrd |
⊢ ( 𝜑 → ( 𝐹 ( 1st ‘ 𝑍 ) 𝑋 ) = ( ( ( 1st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ) |