Metamath Proof Explorer


Theorem yonedalem21

Description: Lemma for yoneda . (Contributed by Mario Carneiro, 28-Jan-2017)

Ref Expression
Hypotheses yoneda.y 𝑌 = ( Yon ‘ 𝐶 )
yoneda.b 𝐵 = ( Base ‘ 𝐶 )
yoneda.1 1 = ( Id ‘ 𝐶 )
yoneda.o 𝑂 = ( oppCat ‘ 𝐶 )
yoneda.s 𝑆 = ( SetCat ‘ 𝑈 )
yoneda.t 𝑇 = ( SetCat ‘ 𝑉 )
yoneda.q 𝑄 = ( 𝑂 FuncCat 𝑆 )
yoneda.h 𝐻 = ( HomF𝑄 )
yoneda.r 𝑅 = ( ( 𝑄 ×c 𝑂 ) FuncCat 𝑇 )
yoneda.e 𝐸 = ( 𝑂 evalF 𝑆 )
yoneda.z 𝑍 = ( 𝐻func ( ( ⟨ ( 1st𝑌 ) , tpos ( 2nd𝑌 ) ⟩ ∘func ( 𝑄 2ndF 𝑂 ) ) ⟨,⟩F ( 𝑄 1stF 𝑂 ) ) )
yoneda.c ( 𝜑𝐶 ∈ Cat )
yoneda.w ( 𝜑𝑉𝑊 )
yoneda.u ( 𝜑 → ran ( Homf𝐶 ) ⊆ 𝑈 )
yoneda.v ( 𝜑 → ( ran ( Homf𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 )
yonedalem21.f ( 𝜑𝐹 ∈ ( 𝑂 Func 𝑆 ) )
yonedalem21.x ( 𝜑𝑋𝐵 )
Assertion yonedalem21 ( 𝜑 → ( 𝐹 ( 1st𝑍 ) 𝑋 ) = ( ( ( 1st𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) )

Proof

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 𝑆 ) 𝐹 ) )