Metamath Proof Explorer


Theorem yonedalem4c

Description: Lemma for yoneda . (Contributed by Mario Carneiro, 29-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 ( 𝜑𝑋𝐵 )
yonedalem4.n 𝑁 = ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥𝐵 ↦ ( 𝑢 ∈ ( ( 1st𝑓 ) ‘ 𝑥 ) ↦ ( 𝑦𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ↦ ( ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑢 ) ) ) ) )
yonedalem4.p ( 𝜑𝐴 ∈ ( ( 1st𝐹 ) ‘ 𝑋 ) )
Assertion yonedalem4c ( 𝜑 → ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ∈ ( ( ( 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 yonedalem4.n 𝑁 = ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥𝐵 ↦ ( 𝑢 ∈ ( ( 1st𝑓 ) ‘ 𝑥 ) ↦ ( 𝑦𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ↦ ( ( ( 𝑥 ( 2nd𝑓 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑢 ) ) ) ) )
19 yonedalem4.p ( 𝜑𝐴 ∈ ( ( 1st𝐹 ) ‘ 𝑋 ) )
20 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 yonedalem4a ( 𝜑 → ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) = ( 𝑦𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) )
21 oveq1 ( 𝑦 = 𝑧 → ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) = ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) )
22 oveq2 ( 𝑦 = 𝑧 → ( 𝑋 ( 2nd𝐹 ) 𝑦 ) = ( 𝑋 ( 2nd𝐹 ) 𝑧 ) )
23 22 fveq1d ( 𝑦 = 𝑧 → ( ( 𝑋 ( 2nd𝐹 ) 𝑦 ) ‘ 𝑔 ) = ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) )
24 23 fveq1d ( 𝑦 = 𝑧 → ( ( ( 𝑋 ( 2nd𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) = ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) )
25 21 24 mpteq12dv ( 𝑦 = 𝑧 → ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) = ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) )
26 25 cbvmptv ( 𝑦𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) = ( 𝑧𝐵 ↦ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) )
27 20 26 eqtrdi ( 𝜑 → ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) = ( 𝑧𝐵 ↦ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) )
28 4 2 oppcbas 𝐵 = ( Base ‘ 𝑂 )
29 eqid ( Hom ‘ 𝑂 ) = ( Hom ‘ 𝑂 )
30 eqid ( Hom ‘ 𝑆 ) = ( Hom ‘ 𝑆 )
31 relfunc Rel ( 𝑂 Func 𝑆 )
32 1st2ndbr ( ( Rel ( 𝑂 Func 𝑆 ) ∧ 𝐹 ∈ ( 𝑂 Func 𝑆 ) ) → ( 1st𝐹 ) ( 𝑂 Func 𝑆 ) ( 2nd𝐹 ) )
33 31 16 32 sylancr ( 𝜑 → ( 1st𝐹 ) ( 𝑂 Func 𝑆 ) ( 2nd𝐹 ) )
34 33 adantr ( ( 𝜑𝑧𝐵 ) → ( 1st𝐹 ) ( 𝑂 Func 𝑆 ) ( 2nd𝐹 ) )
35 17 adantr ( ( 𝜑𝑧𝐵 ) → 𝑋𝐵 )
36 simpr ( ( 𝜑𝑧𝐵 ) → 𝑧𝐵 )
37 28 29 30 34 35 36 funcf2 ( ( 𝜑𝑧𝐵 ) → ( 𝑋 ( 2nd𝐹 ) 𝑧 ) : ( 𝑋 ( Hom ‘ 𝑂 ) 𝑧 ) ⟶ ( ( ( 1st𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑧 ) ) )
38 37 adantr ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( 𝑋 ( 2nd𝐹 ) 𝑧 ) : ( 𝑋 ( Hom ‘ 𝑂 ) 𝑧 ) ⟶ ( ( ( 1st𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑧 ) ) )
39 simpr ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) )
40 eqid ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
41 40 4 oppchom ( 𝑋 ( Hom ‘ 𝑂 ) 𝑧 ) = ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 )
42 39 41 eleqtrrdi ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑔 ∈ ( 𝑋 ( Hom ‘ 𝑂 ) 𝑧 ) )
43 38 42 ffvelrnd ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ∈ ( ( ( 1st𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑧 ) ) )
44 15 unssbd ( 𝜑𝑈𝑉 )
45 13 44 ssexd ( 𝜑𝑈 ∈ V )
46 45 adantr ( ( 𝜑𝑧𝐵 ) → 𝑈 ∈ V )
47 46 adantr ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑈 ∈ V )
48 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
49 28 48 33 funcf1 ( 𝜑 → ( 1st𝐹 ) : 𝐵 ⟶ ( Base ‘ 𝑆 ) )
50 5 45 setcbas ( 𝜑𝑈 = ( Base ‘ 𝑆 ) )
51 50 feq3d ( 𝜑 → ( ( 1st𝐹 ) : 𝐵𝑈 ↔ ( 1st𝐹 ) : 𝐵 ⟶ ( Base ‘ 𝑆 ) ) )
52 49 51 mpbird ( 𝜑 → ( 1st𝐹 ) : 𝐵𝑈 )
53 52 17 ffvelrnd ( 𝜑 → ( ( 1st𝐹 ) ‘ 𝑋 ) ∈ 𝑈 )
54 53 ad2antrr ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( 1st𝐹 ) ‘ 𝑋 ) ∈ 𝑈 )
55 52 ffvelrnda ( ( 𝜑𝑧𝐵 ) → ( ( 1st𝐹 ) ‘ 𝑧 ) ∈ 𝑈 )
56 55 adantr ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( 1st𝐹 ) ‘ 𝑧 ) ∈ 𝑈 )
57 5 47 30 54 56 elsetchom ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ∈ ( ( ( 1st𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑧 ) ) ↔ ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) : ( ( 1st𝐹 ) ‘ 𝑋 ) ⟶ ( ( 1st𝐹 ) ‘ 𝑧 ) ) )
58 43 57 mpbid ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) : ( ( 1st𝐹 ) ‘ 𝑋 ) ⟶ ( ( 1st𝐹 ) ‘ 𝑧 ) )
59 19 ad2antrr ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝐴 ∈ ( ( 1st𝐹 ) ‘ 𝑋 ) )
60 58 59 ffvelrnd ( ( ( 𝜑𝑧𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ∈ ( ( 1st𝐹 ) ‘ 𝑧 ) )
61 60 fmpttd ( ( 𝜑𝑧𝐵 ) → ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) : ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ⟶ ( ( 1st𝐹 ) ‘ 𝑧 ) )
62 12 adantr ( ( 𝜑𝑧𝐵 ) → 𝐶 ∈ Cat )
63 1 2 62 35 40 36 yon11 ( ( 𝜑𝑧𝐵 ) → ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) = ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) )
64 63 feq2d ( ( 𝜑𝑧𝐵 ) → ( ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) : ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1st𝐹 ) ‘ 𝑧 ) ↔ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) : ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ⟶ ( ( 1st𝐹 ) ‘ 𝑧 ) ) )
65 61 64 mpbird ( ( 𝜑𝑧𝐵 ) → ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) : ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1st𝐹 ) ‘ 𝑧 ) )
66 1 2 12 17 4 5 45 14 yon1cl ( 𝜑 → ( ( 1st𝑌 ) ‘ 𝑋 ) ∈ ( 𝑂 Func 𝑆 ) )
67 1st2ndbr ( ( Rel ( 𝑂 Func 𝑆 ) ∧ ( ( 1st𝑌 ) ‘ 𝑋 ) ∈ ( 𝑂 Func 𝑆 ) ) → ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ( 𝑂 Func 𝑆 ) ( 2nd ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) )
68 31 66 67 sylancr ( 𝜑 → ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ( 𝑂 Func 𝑆 ) ( 2nd ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) )
69 28 48 68 funcf1 ( 𝜑 → ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) : 𝐵 ⟶ ( Base ‘ 𝑆 ) )
70 50 feq3d ( 𝜑 → ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) : 𝐵𝑈 ↔ ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) : 𝐵 ⟶ ( Base ‘ 𝑆 ) ) )
71 69 70 mpbird ( 𝜑 → ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) : 𝐵𝑈 )
72 71 ffvelrnda ( ( 𝜑𝑧𝐵 ) → ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ∈ 𝑈 )
73 5 46 30 72 55 elsetchom ( ( 𝜑𝑧𝐵 ) → ( ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ∈ ( ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑧 ) ) ↔ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) : ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1st𝐹 ) ‘ 𝑧 ) ) )
74 65 73 mpbird ( ( 𝜑𝑧𝐵 ) → ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ∈ ( ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑧 ) ) )
75 74 ralrimiva ( 𝜑 → ∀ 𝑧𝐵 ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ∈ ( ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑧 ) ) )
76 2 fvexi 𝐵 ∈ V
77 mptelixpg ( 𝐵 ∈ V → ( ( 𝑧𝐵 ↦ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) ∈ X 𝑧𝐵 ( ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑧 ) ) ↔ ∀ 𝑧𝐵 ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ∈ ( ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑧 ) ) ) )
78 76 77 ax-mp ( ( 𝑧𝐵 ↦ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) ∈ X 𝑧𝐵 ( ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑧 ) ) ↔ ∀ 𝑧𝐵 ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ∈ ( ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑧 ) ) )
79 75 78 sylibr ( 𝜑 → ( 𝑧𝐵 ↦ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) ∈ X 𝑧𝐵 ( ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑧 ) ) )
80 27 79 eqeltrd ( 𝜑 → ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ∈ X 𝑧𝐵 ( ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑧 ) ) )
81 12 adantr ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → 𝐶 ∈ Cat )
82 17 adantr ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → 𝑋𝐵 )
83 simpr1 ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → 𝑧𝐵 )
84 1 2 81 82 40 83 yon11 ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) = ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) )
85 84 eleq2d ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( 𝑘 ∈ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ↔ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) )
86 85 biimpa ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ) → 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) )
87 eqid ( comp ‘ 𝑂 ) = ( comp ‘ 𝑂 )
88 eqid ( comp ‘ 𝑆 ) = ( comp ‘ 𝑆 )
89 33 adantr ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( 1st𝐹 ) ( 𝑂 Func 𝑆 ) ( 2nd𝐹 ) )
90 89 adantr ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( 1st𝐹 ) ( 𝑂 Func 𝑆 ) ( 2nd𝐹 ) )
91 82 adantr ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑋𝐵 )
92 83 adantr ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑧𝐵 )
93 simpr2 ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → 𝑤𝐵 )
94 93 adantr ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑤𝐵 )
95 simpr ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) )
96 95 41 eleqtrrdi ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝑂 ) 𝑧 ) )
97 simplr3 ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) )
98 28 29 87 88 90 91 92 94 96 97 funcco ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( 𝑋 ( 2nd𝐹 ) 𝑤 ) ‘ ( ( ⟨ 𝑋 , 𝑧 ⟩ ( comp ‘ 𝑂 ) 𝑤 ) 𝑘 ) ) = ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑋 ) , ( ( 1st𝐹 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑤 ) ) ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑘 ) ) )
99 eqid ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
100 2 99 4 91 92 94 oppcco ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ⟨ 𝑋 , 𝑧 ⟩ ( comp ‘ 𝑂 ) 𝑤 ) 𝑘 ) = ( 𝑘 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ) )
101 100 fveq2d ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( 𝑋 ( 2nd𝐹 ) 𝑤 ) ‘ ( ( ⟨ 𝑋 , 𝑧 ⟩ ( comp ‘ 𝑂 ) 𝑤 ) 𝑘 ) ) = ( ( 𝑋 ( 2nd𝐹 ) 𝑤 ) ‘ ( 𝑘 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ) ) )
102 45 adantr ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → 𝑈 ∈ V )
103 102 adantr ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑈 ∈ V )
104 53 ad2antrr ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( 1st𝐹 ) ‘ 𝑋 ) ∈ 𝑈 )
105 55 3ad2antr1 ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( 1st𝐹 ) ‘ 𝑧 ) ∈ 𝑈 )
106 105 adantr ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( 1st𝐹 ) ‘ 𝑧 ) ∈ 𝑈 )
107 52 adantr ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( 1st𝐹 ) : 𝐵𝑈 )
108 107 93 ffvelrnd ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( 1st𝐹 ) ‘ 𝑤 ) ∈ 𝑈 )
109 108 adantr ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( 1st𝐹 ) ‘ 𝑤 ) ∈ 𝑈 )
110 28 29 30 89 82 83 funcf2 ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( 𝑋 ( 2nd𝐹 ) 𝑧 ) : ( 𝑋 ( Hom ‘ 𝑂 ) 𝑧 ) ⟶ ( ( ( 1st𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑧 ) ) )
111 110 adantr ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( 𝑋 ( 2nd𝐹 ) 𝑧 ) : ( 𝑋 ( Hom ‘ 𝑂 ) 𝑧 ) ⟶ ( ( ( 1st𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑧 ) ) )
112 111 96 ffvelrnd ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑘 ) ∈ ( ( ( 1st𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑧 ) ) )
113 5 103 30 104 106 elsetchom ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑘 ) ∈ ( ( ( 1st𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑧 ) ) ↔ ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑘 ) : ( ( 1st𝐹 ) ‘ 𝑋 ) ⟶ ( ( 1st𝐹 ) ‘ 𝑧 ) ) )
114 112 113 mpbid ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑘 ) : ( ( 1st𝐹 ) ‘ 𝑋 ) ⟶ ( ( 1st𝐹 ) ‘ 𝑧 ) )
115 28 29 30 89 83 93 funcf2 ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( 𝑧 ( 2nd𝐹 ) 𝑤 ) : ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ⟶ ( ( ( 1st𝐹 ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑤 ) ) )
116 simpr3 ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) )
117 115 116 ffvelrnd ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ∈ ( ( ( 1st𝐹 ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑤 ) ) )
118 5 102 30 105 108 elsetchom ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ∈ ( ( ( 1st𝐹 ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑤 ) ) ↔ ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) : ( ( 1st𝐹 ) ‘ 𝑧 ) ⟶ ( ( 1st𝐹 ) ‘ 𝑤 ) ) )
119 117 118 mpbid ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) : ( ( 1st𝐹 ) ‘ 𝑧 ) ⟶ ( ( 1st𝐹 ) ‘ 𝑤 ) )
120 119 adantr ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) : ( ( 1st𝐹 ) ‘ 𝑧 ) ⟶ ( ( 1st𝐹 ) ‘ 𝑤 ) )
121 5 103 88 104 106 109 114 120 setcco ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ( ⟨ ( ( 1st𝐹 ) ‘ 𝑋 ) , ( ( 1st𝐹 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑤 ) ) ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑘 ) ) = ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ∘ ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑘 ) ) )
122 98 101 121 3eqtr3d ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( 𝑋 ( 2nd𝐹 ) 𝑤 ) ‘ ( 𝑘 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ) ) = ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ∘ ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑘 ) ) )
123 122 fveq1d ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( 𝑋 ( 2nd𝐹 ) 𝑤 ) ‘ ( 𝑘 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ) ) ‘ 𝐴 ) = ( ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ∘ ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑘 ) ) ‘ 𝐴 ) )
124 19 ad2antrr ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝐴 ∈ ( ( 1st𝐹 ) ‘ 𝑋 ) )
125 fvco3 ( ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑘 ) : ( ( 1st𝐹 ) ‘ 𝑋 ) ⟶ ( ( 1st𝐹 ) ‘ 𝑧 ) ∧ 𝐴 ∈ ( ( 1st𝐹 ) ‘ 𝑋 ) ) → ( ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ∘ ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑘 ) ) ‘ 𝐴 ) = ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ‘ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑘 ) ‘ 𝐴 ) ) )
126 114 124 125 syl2anc ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ∘ ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑘 ) ) ‘ 𝐴 ) = ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ‘ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑘 ) ‘ 𝐴 ) ) )
127 123 126 eqtrd ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( 𝑋 ( 2nd𝐹 ) 𝑤 ) ‘ ( 𝑘 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ) ) ‘ 𝐴 ) = ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ‘ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑘 ) ‘ 𝐴 ) ) )
128 81 adantr ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝐶 ∈ Cat )
129 40 4 oppchom ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) = ( 𝑤 ( Hom ‘ 𝐶 ) 𝑧 )
130 97 129 eleqtrdi ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑧 ) )
131 1 2 128 91 40 92 99 94 130 95 yon12 ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( 𝑧 ( 2nd ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ) ‘ 𝑘 ) = ( 𝑘 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ) )
132 131 fveq2d ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ‘ ( ( ( 𝑧 ( 2nd ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ) ‘ 𝑘 ) ) = ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ‘ ( 𝑘 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ) ) )
133 13 ad2antrr ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑉𝑊 )
134 14 ad2antrr ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ran ( Homf𝐶 ) ⊆ 𝑈 )
135 15 ad2antrr ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ran ( Homf𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 )
136 16 ad2antrr ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝐹 ∈ ( 𝑂 Func 𝑆 ) )
137 2 40 99 128 94 92 91 130 95 catcocl ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( 𝑘 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ) ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑋 ) )
138 1 2 3 4 5 6 7 8 9 10 11 128 133 134 135 136 91 18 124 94 137 yonedalem4b ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ‘ ( 𝑘 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ) ) = ( ( ( 𝑋 ( 2nd𝐹 ) 𝑤 ) ‘ ( 𝑘 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ) ) ‘ 𝐴 ) )
139 132 138 eqtrd ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ‘ ( ( ( 𝑧 ( 2nd ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ) ‘ 𝑘 ) ) = ( ( ( 𝑋 ( 2nd𝐹 ) 𝑤 ) ‘ ( 𝑘 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ) ) ‘ 𝐴 ) )
140 1 2 3 4 5 6 7 8 9 10 11 128 133 134 135 136 91 18 124 92 95 yonedalem4b ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ‘ 𝑘 ) = ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑘 ) ‘ 𝐴 ) )
141 140 fveq2d ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ‘ ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ‘ 𝑘 ) ) = ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ‘ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑘 ) ‘ 𝐴 ) ) )
142 127 139 141 3eqtr4d ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ‘ ( ( ( 𝑧 ( 2nd ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ) ‘ 𝑘 ) ) = ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ‘ ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ‘ 𝑘 ) ) )
143 86 142 syldan ( ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ) → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ‘ ( ( ( 𝑧 ( 2nd ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ) ‘ 𝑘 ) ) = ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ‘ ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ‘ 𝑘 ) ) )
144 143 mpteq2dva ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( 𝑘 ∈ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ↦ ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ‘ ( ( ( 𝑧 ( 2nd ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ) ‘ 𝑘 ) ) ) = ( 𝑘 ∈ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ↦ ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ‘ ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ‘ 𝑘 ) ) ) )
145 fveq2 ( 𝑧 = 𝑤 → ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) = ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) )
146 fveq2 ( 𝑧 = 𝑤 → ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) = ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑤 ) )
147 fveq2 ( 𝑧 = 𝑤 → ( ( 1st𝐹 ) ‘ 𝑧 ) = ( ( 1st𝐹 ) ‘ 𝑤 ) )
148 145 146 147 feq123d ( 𝑧 = 𝑤 → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) : ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1st𝐹 ) ‘ 𝑧 ) ↔ ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) : ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ⟶ ( ( 1st𝐹 ) ‘ 𝑤 ) ) )
149 27 fveq1d ( 𝜑 → ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) = ( ( 𝑧𝐵 ↦ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) ‘ 𝑧 ) )
150 ovex ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∈ V
151 150 mptex ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ∈ V
152 eqid ( 𝑧𝐵 ↦ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) = ( 𝑧𝐵 ↦ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) )
153 152 fvmpt2 ( ( 𝑧𝐵 ∧ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ∈ V ) → ( ( 𝑧𝐵 ↦ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) ‘ 𝑧 ) = ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) )
154 151 153 mpan2 ( 𝑧𝐵 → ( ( 𝑧𝐵 ↦ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) ‘ 𝑧 ) = ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) )
155 149 154 sylan9eq ( ( 𝜑𝑧𝐵 ) → ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) = ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) )
156 155 feq1d ( ( 𝜑𝑧𝐵 ) → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) : ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1st𝐹 ) ‘ 𝑧 ) ↔ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2nd𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) : ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1st𝐹 ) ‘ 𝑧 ) ) )
157 65 156 mpbird ( ( 𝜑𝑧𝐵 ) → ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) : ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1st𝐹 ) ‘ 𝑧 ) )
158 157 ralrimiva ( 𝜑 → ∀ 𝑧𝐵 ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) : ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1st𝐹 ) ‘ 𝑧 ) )
159 158 adantr ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ∀ 𝑧𝐵 ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) : ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1st𝐹 ) ‘ 𝑧 ) )
160 148 159 93 rspcdva ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) : ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ⟶ ( ( 1st𝐹 ) ‘ 𝑤 ) )
161 68 adantr ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ( 𝑂 Func 𝑆 ) ( 2nd ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) )
162 28 29 30 161 83 93 funcf2 ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( 𝑧 ( 2nd ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) 𝑤 ) : ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ⟶ ( ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ) )
163 162 116 ffvelrnd ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( 𝑧 ( 2nd ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ) ∈ ( ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ) )
164 72 3ad2antr1 ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ∈ 𝑈 )
165 71 adantr ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) : 𝐵𝑈 )
166 165 93 ffvelrnd ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ∈ 𝑈 )
167 5 102 30 164 166 elsetchom ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( ( 𝑧 ( 2nd ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ) ∈ ( ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ) ↔ ( ( 𝑧 ( 2nd ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ) : ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ) )
168 163 167 mpbid ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( 𝑧 ( 2nd ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ) : ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑤 ) )
169 fcompt ( ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) : ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ⟶ ( ( 1st𝐹 ) ‘ 𝑤 ) ∧ ( ( 𝑧 ( 2nd ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ) : ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ) → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ∘ ( ( 𝑧 ( 2nd ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ) ) = ( 𝑘 ∈ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ↦ ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ‘ ( ( ( 𝑧 ( 2nd ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ) ‘ 𝑘 ) ) ) )
170 160 168 169 syl2anc ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ∘ ( ( 𝑧 ( 2nd ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ) ) = ( 𝑘 ∈ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ↦ ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ‘ ( ( ( 𝑧 ( 2nd ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ) ‘ 𝑘 ) ) ) )
171 157 3ad2antr1 ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) : ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1st𝐹 ) ‘ 𝑧 ) )
172 fcompt ( ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) : ( ( 1st𝐹 ) ‘ 𝑧 ) ⟶ ( ( 1st𝐹 ) ‘ 𝑤 ) ∧ ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) : ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1st𝐹 ) ‘ 𝑧 ) ) → ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ∘ ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ) = ( 𝑘 ∈ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ↦ ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ‘ ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ‘ 𝑘 ) ) ) )
173 119 171 172 syl2anc ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ∘ ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ) = ( 𝑘 ∈ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ↦ ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ‘ ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ‘ 𝑘 ) ) ) )
174 144 170 173 3eqtr4d ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ∘ ( ( 𝑧 ( 2nd ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ) ) = ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ∘ ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ) )
175 5 102 88 164 166 108 168 160 setcco ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ( ⟨ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑤 ) ) ( ( 𝑧 ( 2nd ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ) ) = ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ∘ ( ( 𝑧 ( 2nd ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ) ) )
176 5 102 88 164 105 108 171 119 setcco ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ( ⟨ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1st𝐹 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑤 ) ) ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ) = ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ∘ ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ) )
177 174 175 176 3eqtr4d ( ( 𝜑 ∧ ( 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ( ⟨ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑤 ) ) ( ( 𝑧 ( 2nd ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ) ) = ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ( ⟨ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1st𝐹 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑤 ) ) ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ) )
178 177 ralrimivvva ( 𝜑 → ∀ 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ( ⟨ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑤 ) ) ( ( 𝑧 ( 2nd ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ) ) = ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ( ⟨ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1st𝐹 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑤 ) ) ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ) )
179 eqid ( 𝑂 Nat 𝑆 ) = ( 𝑂 Nat 𝑆 )
180 179 28 29 30 88 66 16 isnat2 ( 𝜑 → ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ∈ ( ( ( 1st𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↔ ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ∈ X 𝑧𝐵 ( ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑧 ) ) ∧ ∀ 𝑧𝐵𝑤𝐵 ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ( ⟨ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑤 ) ) ( ( 𝑧 ( 2nd ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ) ) = ( ( ( 𝑧 ( 2nd𝐹 ) 𝑤 ) ‘ ) ( ⟨ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1st𝐹 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑆 ) ( ( 1st𝐹 ) ‘ 𝑤 ) ) ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ) ) ) )
181 80 178 180 mpbir2and ( 𝜑 → ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ∈ ( ( ( 1st𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) )