Metamath Proof Explorer


Theorem yonedalem3

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𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 )
yoneda.m 𝑀 = ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥𝐵 ↦ ( 𝑎 ∈ ( ( ( 1st𝑌 ) ‘ 𝑥 ) ( 𝑂 Nat 𝑆 ) 𝑓 ) ↦ ( ( 𝑎𝑥 ) ‘ ( 1𝑥 ) ) ) )
Assertion yonedalem3 ( 𝜑𝑀 ∈ ( 𝑍 ( ( 𝑄 ×c 𝑂 ) 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 yoneda.m 𝑀 = ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥𝐵 ↦ ( 𝑎 ∈ ( ( ( 1st𝑌 ) ‘ 𝑥 ) ( 𝑂 Nat 𝑆 ) 𝑓 ) ↦ ( ( 𝑎𝑥 ) ‘ ( 1𝑥 ) ) ) )
17 ovex ( ( ( 1st𝑌 ) ‘ 𝑥 ) ( 𝑂 Nat 𝑆 ) 𝑓 ) ∈ V
18 17 mptex ( 𝑎 ∈ ( ( ( 1st𝑌 ) ‘ 𝑥 ) ( 𝑂 Nat 𝑆 ) 𝑓 ) ↦ ( ( 𝑎𝑥 ) ‘ ( 1𝑥 ) ) ) ∈ V
19 16 18 fnmpoi 𝑀 Fn ( ( 𝑂 Func 𝑆 ) × 𝐵 )
20 19 a1i ( 𝜑𝑀 Fn ( ( 𝑂 Func 𝑆 ) × 𝐵 ) )
21 12 adantr ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦𝐵 ) ) → 𝐶 ∈ Cat )
22 13 adantr ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦𝐵 ) ) → 𝑉𝑊 )
23 14 adantr ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦𝐵 ) ) → ran ( Homf𝐶 ) ⊆ 𝑈 )
24 15 adantr ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦𝐵 ) ) → ( ran ( Homf𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 )
25 simprl ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦𝐵 ) ) → 𝑔 ∈ ( 𝑂 Func 𝑆 ) )
26 simprr ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦𝐵 ) ) → 𝑦𝐵 )
27 1 2 3 4 5 6 7 8 9 10 11 21 22 23 24 25 26 16 yonedalem3a ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦𝐵 ) ) → ( ( 𝑔 𝑀 𝑦 ) = ( 𝑎 ∈ ( ( ( 1st𝑌 ) ‘ 𝑦 ) ( 𝑂 Nat 𝑆 ) 𝑔 ) ↦ ( ( 𝑎𝑦 ) ‘ ( 1𝑦 ) ) ) ∧ ( 𝑔 𝑀 𝑦 ) : ( 𝑔 ( 1st𝑍 ) 𝑦 ) ⟶ ( 𝑔 ( 1st𝐸 ) 𝑦 ) ) )
28 27 simprd ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦𝐵 ) ) → ( 𝑔 𝑀 𝑦 ) : ( 𝑔 ( 1st𝑍 ) 𝑦 ) ⟶ ( 𝑔 ( 1st𝐸 ) 𝑦 ) )
29 eqid ( Hom ‘ 𝑇 ) = ( Hom ‘ 𝑇 )
30 eqid ( 𝑄 ×c 𝑂 ) = ( 𝑄 ×c 𝑂 )
31 7 fucbas ( 𝑂 Func 𝑆 ) = ( Base ‘ 𝑄 )
32 4 2 oppcbas 𝐵 = ( Base ‘ 𝑂 )
33 30 31 32 xpcbas ( ( 𝑂 Func 𝑆 ) × 𝐵 ) = ( Base ‘ ( 𝑄 ×c 𝑂 ) )
34 eqid ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
35 relfunc Rel ( ( 𝑄 ×c 𝑂 ) Func 𝑇 )
36 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 yonedalem1 ( 𝜑 → ( 𝑍 ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ∧ 𝐸 ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ) )
37 36 simpld ( 𝜑𝑍 ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) )
38 1st2ndbr ( ( Rel ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ∧ 𝑍 ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ) → ( 1st𝑍 ) ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ( 2nd𝑍 ) )
39 35 37 38 sylancr ( 𝜑 → ( 1st𝑍 ) ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ( 2nd𝑍 ) )
40 33 34 39 funcf1 ( 𝜑 → ( 1st𝑍 ) : ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ⟶ ( Base ‘ 𝑇 ) )
41 40 fovrnda ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦𝐵 ) ) → ( 𝑔 ( 1st𝑍 ) 𝑦 ) ∈ ( Base ‘ 𝑇 ) )
42 6 22 setcbas ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦𝐵 ) ) → 𝑉 = ( Base ‘ 𝑇 ) )
43 41 42 eleqtrrd ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦𝐵 ) ) → ( 𝑔 ( 1st𝑍 ) 𝑦 ) ∈ 𝑉 )
44 36 simprd ( 𝜑𝐸 ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) )
45 1st2ndbr ( ( Rel ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ∧ 𝐸 ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ) → ( 1st𝐸 ) ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ( 2nd𝐸 ) )
46 35 44 45 sylancr ( 𝜑 → ( 1st𝐸 ) ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ( 2nd𝐸 ) )
47 33 34 46 funcf1 ( 𝜑 → ( 1st𝐸 ) : ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ⟶ ( Base ‘ 𝑇 ) )
48 47 fovrnda ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦𝐵 ) ) → ( 𝑔 ( 1st𝐸 ) 𝑦 ) ∈ ( Base ‘ 𝑇 ) )
49 48 42 eleqtrrd ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦𝐵 ) ) → ( 𝑔 ( 1st𝐸 ) 𝑦 ) ∈ 𝑉 )
50 6 22 29 43 49 elsetchom ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦𝐵 ) ) → ( ( 𝑔 𝑀 𝑦 ) ∈ ( ( 𝑔 ( 1st𝑍 ) 𝑦 ) ( Hom ‘ 𝑇 ) ( 𝑔 ( 1st𝐸 ) 𝑦 ) ) ↔ ( 𝑔 𝑀 𝑦 ) : ( 𝑔 ( 1st𝑍 ) 𝑦 ) ⟶ ( 𝑔 ( 1st𝐸 ) 𝑦 ) ) )
51 28 50 mpbird ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∧ 𝑦𝐵 ) ) → ( 𝑔 𝑀 𝑦 ) ∈ ( ( 𝑔 ( 1st𝑍 ) 𝑦 ) ( Hom ‘ 𝑇 ) ( 𝑔 ( 1st𝐸 ) 𝑦 ) ) )
52 51 ralrimivva ( 𝜑 → ∀ 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∀ 𝑦𝐵 ( 𝑔 𝑀 𝑦 ) ∈ ( ( 𝑔 ( 1st𝑍 ) 𝑦 ) ( Hom ‘ 𝑇 ) ( 𝑔 ( 1st𝐸 ) 𝑦 ) ) )
53 fveq2 ( 𝑧 = ⟨ 𝑔 , 𝑦 ⟩ → ( 𝑀𝑧 ) = ( 𝑀 ‘ ⟨ 𝑔 , 𝑦 ⟩ ) )
54 df-ov ( 𝑔 𝑀 𝑦 ) = ( 𝑀 ‘ ⟨ 𝑔 , 𝑦 ⟩ )
55 53 54 eqtr4di ( 𝑧 = ⟨ 𝑔 , 𝑦 ⟩ → ( 𝑀𝑧 ) = ( 𝑔 𝑀 𝑦 ) )
56 fveq2 ( 𝑧 = ⟨ 𝑔 , 𝑦 ⟩ → ( ( 1st𝑍 ) ‘ 𝑧 ) = ( ( 1st𝑍 ) ‘ ⟨ 𝑔 , 𝑦 ⟩ ) )
57 df-ov ( 𝑔 ( 1st𝑍 ) 𝑦 ) = ( ( 1st𝑍 ) ‘ ⟨ 𝑔 , 𝑦 ⟩ )
58 56 57 eqtr4di ( 𝑧 = ⟨ 𝑔 , 𝑦 ⟩ → ( ( 1st𝑍 ) ‘ 𝑧 ) = ( 𝑔 ( 1st𝑍 ) 𝑦 ) )
59 fveq2 ( 𝑧 = ⟨ 𝑔 , 𝑦 ⟩ → ( ( 1st𝐸 ) ‘ 𝑧 ) = ( ( 1st𝐸 ) ‘ ⟨ 𝑔 , 𝑦 ⟩ ) )
60 df-ov ( 𝑔 ( 1st𝐸 ) 𝑦 ) = ( ( 1st𝐸 ) ‘ ⟨ 𝑔 , 𝑦 ⟩ )
61 59 60 eqtr4di ( 𝑧 = ⟨ 𝑔 , 𝑦 ⟩ → ( ( 1st𝐸 ) ‘ 𝑧 ) = ( 𝑔 ( 1st𝐸 ) 𝑦 ) )
62 58 61 oveq12d ( 𝑧 = ⟨ 𝑔 , 𝑦 ⟩ → ( ( ( 1st𝑍 ) ‘ 𝑧 ) ( Hom ‘ 𝑇 ) ( ( 1st𝐸 ) ‘ 𝑧 ) ) = ( ( 𝑔 ( 1st𝑍 ) 𝑦 ) ( Hom ‘ 𝑇 ) ( 𝑔 ( 1st𝐸 ) 𝑦 ) ) )
63 55 62 eleq12d ( 𝑧 = ⟨ 𝑔 , 𝑦 ⟩ → ( ( 𝑀𝑧 ) ∈ ( ( ( 1st𝑍 ) ‘ 𝑧 ) ( Hom ‘ 𝑇 ) ( ( 1st𝐸 ) ‘ 𝑧 ) ) ↔ ( 𝑔 𝑀 𝑦 ) ∈ ( ( 𝑔 ( 1st𝑍 ) 𝑦 ) ( Hom ‘ 𝑇 ) ( 𝑔 ( 1st𝐸 ) 𝑦 ) ) ) )
64 63 ralxp ( ∀ 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ( 𝑀𝑧 ) ∈ ( ( ( 1st𝑍 ) ‘ 𝑧 ) ( Hom ‘ 𝑇 ) ( ( 1st𝐸 ) ‘ 𝑧 ) ) ↔ ∀ 𝑔 ∈ ( 𝑂 Func 𝑆 ) ∀ 𝑦𝐵 ( 𝑔 𝑀 𝑦 ) ∈ ( ( 𝑔 ( 1st𝑍 ) 𝑦 ) ( Hom ‘ 𝑇 ) ( 𝑔 ( 1st𝐸 ) 𝑦 ) ) )
65 52 64 sylibr ( 𝜑 → ∀ 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ( 𝑀𝑧 ) ∈ ( ( ( 1st𝑍 ) ‘ 𝑧 ) ( Hom ‘ 𝑇 ) ( ( 1st𝐸 ) ‘ 𝑧 ) ) )
66 ovex ( 𝑂 Func 𝑆 ) ∈ V
67 2 fvexi 𝐵 ∈ V
68 66 67 mpoex ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥𝐵 ↦ ( 𝑎 ∈ ( ( ( 1st𝑌 ) ‘ 𝑥 ) ( 𝑂 Nat 𝑆 ) 𝑓 ) ↦ ( ( 𝑎𝑥 ) ‘ ( 1𝑥 ) ) ) ) ∈ V
69 16 68 eqeltri 𝑀 ∈ V
70 69 elixp ( 𝑀X 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ( ( ( 1st𝑍 ) ‘ 𝑧 ) ( Hom ‘ 𝑇 ) ( ( 1st𝐸 ) ‘ 𝑧 ) ) ↔ ( 𝑀 Fn ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ ∀ 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ( 𝑀𝑧 ) ∈ ( ( ( 1st𝑍 ) ‘ 𝑧 ) ( Hom ‘ 𝑇 ) ( ( 1st𝐸 ) ‘ 𝑧 ) ) ) )
71 20 65 70 sylanbrc ( 𝜑𝑀X 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ( ( ( 1st𝑍 ) ‘ 𝑧 ) ( Hom ‘ 𝑇 ) ( ( 1st𝐸 ) ‘ 𝑧 ) ) )
72 12 adantr ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → 𝐶 ∈ Cat )
73 13 adantr ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → 𝑉𝑊 )
74 14 adantr ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ran ( Homf𝐶 ) ⊆ 𝑈 )
75 15 adantr ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ran ( Homf𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 )
76 simpr1 ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) )
77 xp1st ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) → ( 1st𝑧 ) ∈ ( 𝑂 Func 𝑆 ) )
78 76 77 syl ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 1st𝑧 ) ∈ ( 𝑂 Func 𝑆 ) )
79 xp2nd ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) → ( 2nd𝑧 ) ∈ 𝐵 )
80 76 79 syl ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 2nd𝑧 ) ∈ 𝐵 )
81 simpr2 ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) )
82 xp1st ( 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) → ( 1st𝑤 ) ∈ ( 𝑂 Func 𝑆 ) )
83 81 82 syl ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 1st𝑤 ) ∈ ( 𝑂 Func 𝑆 ) )
84 xp2nd ( 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) → ( 2nd𝑤 ) ∈ 𝐵 )
85 81 84 syl ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 2nd𝑤 ) ∈ 𝐵 )
86 simpr3 ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) )
87 eqid ( 𝑂 Nat 𝑆 ) = ( 𝑂 Nat 𝑆 )
88 7 87 fuchom ( 𝑂 Nat 𝑆 ) = ( Hom ‘ 𝑄 )
89 eqid ( Hom ‘ 𝑂 ) = ( Hom ‘ 𝑂 )
90 eqid ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) = ( Hom ‘ ( 𝑄 ×c 𝑂 ) )
91 30 33 88 89 90 76 81 xpchom ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) = ( ( ( 1st𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1st𝑤 ) ) × ( ( 2nd𝑧 ) ( Hom ‘ 𝑂 ) ( 2nd𝑤 ) ) ) )
92 eqid ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
93 92 4 oppchom ( ( 2nd𝑧 ) ( Hom ‘ 𝑂 ) ( 2nd𝑤 ) ) = ( ( 2nd𝑤 ) ( Hom ‘ 𝐶 ) ( 2nd𝑧 ) )
94 93 xpeq2i ( ( ( 1st𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1st𝑤 ) ) × ( ( 2nd𝑧 ) ( Hom ‘ 𝑂 ) ( 2nd𝑤 ) ) ) = ( ( ( 1st𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1st𝑤 ) ) × ( ( 2nd𝑤 ) ( Hom ‘ 𝐶 ) ( 2nd𝑧 ) ) )
95 91 94 eqtrdi ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) = ( ( ( 1st𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1st𝑤 ) ) × ( ( 2nd𝑤 ) ( Hom ‘ 𝐶 ) ( 2nd𝑧 ) ) ) )
96 86 95 eleqtrd ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → 𝑔 ∈ ( ( ( 1st𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1st𝑤 ) ) × ( ( 2nd𝑤 ) ( Hom ‘ 𝐶 ) ( 2nd𝑧 ) ) ) )
97 xp1st ( 𝑔 ∈ ( ( ( 1st𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1st𝑤 ) ) × ( ( 2nd𝑤 ) ( Hom ‘ 𝐶 ) ( 2nd𝑧 ) ) ) → ( 1st𝑔 ) ∈ ( ( 1st𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1st𝑤 ) ) )
98 96 97 syl ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 1st𝑔 ) ∈ ( ( 1st𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1st𝑤 ) ) )
99 xp2nd ( 𝑔 ∈ ( ( ( 1st𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1st𝑤 ) ) × ( ( 2nd𝑤 ) ( Hom ‘ 𝐶 ) ( 2nd𝑧 ) ) ) → ( 2nd𝑔 ) ∈ ( ( 2nd𝑤 ) ( Hom ‘ 𝐶 ) ( 2nd𝑧 ) ) )
100 96 99 syl ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 2nd𝑔 ) ∈ ( ( 2nd𝑤 ) ( Hom ‘ 𝐶 ) ( 2nd𝑧 ) ) )
101 1 2 3 4 5 6 7 8 9 10 11 72 73 74 75 78 80 83 85 98 100 16 yonedalem3b ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( ( 1st𝑤 ) 𝑀 ( 2nd𝑤 ) ) ( ⟨ ( ( 1st𝑧 ) ( 1st𝑍 ) ( 2nd𝑧 ) ) , ( ( 1st𝑤 ) ( 1st𝑍 ) ( 2nd𝑤 ) ) ⟩ ( comp ‘ 𝑇 ) ( ( 1st𝑤 ) ( 1st𝐸 ) ( 2nd𝑤 ) ) ) ( ( 1st𝑔 ) ( ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ ( 2nd𝑍 ) ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ ) ( 2nd𝑔 ) ) ) = ( ( ( 1st𝑔 ) ( ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ ( 2nd𝐸 ) ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ ) ( 2nd𝑔 ) ) ( ⟨ ( ( 1st𝑧 ) ( 1st𝑍 ) ( 2nd𝑧 ) ) , ( ( 1st𝑧 ) ( 1st𝐸 ) ( 2nd𝑧 ) ) ⟩ ( comp ‘ 𝑇 ) ( ( 1st𝑤 ) ( 1st𝐸 ) ( 2nd𝑤 ) ) ) ( ( 1st𝑧 ) 𝑀 ( 2nd𝑧 ) ) ) )
102 1st2nd2 ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) → 𝑧 = ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ )
103 76 102 syl ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → 𝑧 = ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ )
104 103 fveq2d ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 1st𝑍 ) ‘ 𝑧 ) = ( ( 1st𝑍 ) ‘ ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ ) )
105 df-ov ( ( 1st𝑧 ) ( 1st𝑍 ) ( 2nd𝑧 ) ) = ( ( 1st𝑍 ) ‘ ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ )
106 104 105 eqtr4di ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 1st𝑍 ) ‘ 𝑧 ) = ( ( 1st𝑧 ) ( 1st𝑍 ) ( 2nd𝑧 ) ) )
107 1st2nd2 ( 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) → 𝑤 = ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ )
108 81 107 syl ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → 𝑤 = ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ )
109 108 fveq2d ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 1st𝑍 ) ‘ 𝑤 ) = ( ( 1st𝑍 ) ‘ ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ ) )
110 df-ov ( ( 1st𝑤 ) ( 1st𝑍 ) ( 2nd𝑤 ) ) = ( ( 1st𝑍 ) ‘ ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ )
111 109 110 eqtr4di ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 1st𝑍 ) ‘ 𝑤 ) = ( ( 1st𝑤 ) ( 1st𝑍 ) ( 2nd𝑤 ) ) )
112 106 111 opeq12d ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ⟨ ( ( 1st𝑍 ) ‘ 𝑧 ) , ( ( 1st𝑍 ) ‘ 𝑤 ) ⟩ = ⟨ ( ( 1st𝑧 ) ( 1st𝑍 ) ( 2nd𝑧 ) ) , ( ( 1st𝑤 ) ( 1st𝑍 ) ( 2nd𝑤 ) ) ⟩ )
113 108 fveq2d ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 1st𝐸 ) ‘ 𝑤 ) = ( ( 1st𝐸 ) ‘ ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ ) )
114 df-ov ( ( 1st𝑤 ) ( 1st𝐸 ) ( 2nd𝑤 ) ) = ( ( 1st𝐸 ) ‘ ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ )
115 113 114 eqtr4di ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 1st𝐸 ) ‘ 𝑤 ) = ( ( 1st𝑤 ) ( 1st𝐸 ) ( 2nd𝑤 ) ) )
116 112 115 oveq12d ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ⟨ ( ( 1st𝑍 ) ‘ 𝑧 ) , ( ( 1st𝑍 ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1st𝐸 ) ‘ 𝑤 ) ) = ( ⟨ ( ( 1st𝑧 ) ( 1st𝑍 ) ( 2nd𝑧 ) ) , ( ( 1st𝑤 ) ( 1st𝑍 ) ( 2nd𝑤 ) ) ⟩ ( comp ‘ 𝑇 ) ( ( 1st𝑤 ) ( 1st𝐸 ) ( 2nd𝑤 ) ) ) )
117 108 fveq2d ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 𝑀𝑤 ) = ( 𝑀 ‘ ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ ) )
118 df-ov ( ( 1st𝑤 ) 𝑀 ( 2nd𝑤 ) ) = ( 𝑀 ‘ ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ )
119 117 118 eqtr4di ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 𝑀𝑤 ) = ( ( 1st𝑤 ) 𝑀 ( 2nd𝑤 ) ) )
120 103 108 oveq12d ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 𝑧 ( 2nd𝑍 ) 𝑤 ) = ( ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ ( 2nd𝑍 ) ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ ) )
121 1st2nd2 ( 𝑔 ∈ ( ( ( 1st𝑧 ) ( 𝑂 Nat 𝑆 ) ( 1st𝑤 ) ) × ( ( 2nd𝑤 ) ( Hom ‘ 𝐶 ) ( 2nd𝑧 ) ) ) → 𝑔 = ⟨ ( 1st𝑔 ) , ( 2nd𝑔 ) ⟩ )
122 96 121 syl ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → 𝑔 = ⟨ ( 1st𝑔 ) , ( 2nd𝑔 ) ⟩ )
123 120 122 fveq12d ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 𝑧 ( 2nd𝑍 ) 𝑤 ) ‘ 𝑔 ) = ( ( ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ ( 2nd𝑍 ) ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ ) ‘ ⟨ ( 1st𝑔 ) , ( 2nd𝑔 ) ⟩ ) )
124 df-ov ( ( 1st𝑔 ) ( ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ ( 2nd𝑍 ) ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ ) ( 2nd𝑔 ) ) = ( ( ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ ( 2nd𝑍 ) ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ ) ‘ ⟨ ( 1st𝑔 ) , ( 2nd𝑔 ) ⟩ )
125 123 124 eqtr4di ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 𝑧 ( 2nd𝑍 ) 𝑤 ) ‘ 𝑔 ) = ( ( 1st𝑔 ) ( ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ ( 2nd𝑍 ) ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ ) ( 2nd𝑔 ) ) )
126 116 119 125 oveq123d ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 𝑀𝑤 ) ( ⟨ ( ( 1st𝑍 ) ‘ 𝑧 ) , ( ( 1st𝑍 ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1st𝐸 ) ‘ 𝑤 ) ) ( ( 𝑧 ( 2nd𝑍 ) 𝑤 ) ‘ 𝑔 ) ) = ( ( ( 1st𝑤 ) 𝑀 ( 2nd𝑤 ) ) ( ⟨ ( ( 1st𝑧 ) ( 1st𝑍 ) ( 2nd𝑧 ) ) , ( ( 1st𝑤 ) ( 1st𝑍 ) ( 2nd𝑤 ) ) ⟩ ( comp ‘ 𝑇 ) ( ( 1st𝑤 ) ( 1st𝐸 ) ( 2nd𝑤 ) ) ) ( ( 1st𝑔 ) ( ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ ( 2nd𝑍 ) ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ ) ( 2nd𝑔 ) ) ) )
127 103 fveq2d ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 1st𝐸 ) ‘ 𝑧 ) = ( ( 1st𝐸 ) ‘ ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ ) )
128 df-ov ( ( 1st𝑧 ) ( 1st𝐸 ) ( 2nd𝑧 ) ) = ( ( 1st𝐸 ) ‘ ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ )
129 127 128 eqtr4di ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 1st𝐸 ) ‘ 𝑧 ) = ( ( 1st𝑧 ) ( 1st𝐸 ) ( 2nd𝑧 ) ) )
130 106 129 opeq12d ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ⟨ ( ( 1st𝑍 ) ‘ 𝑧 ) , ( ( 1st𝐸 ) ‘ 𝑧 ) ⟩ = ⟨ ( ( 1st𝑧 ) ( 1st𝑍 ) ( 2nd𝑧 ) ) , ( ( 1st𝑧 ) ( 1st𝐸 ) ( 2nd𝑧 ) ) ⟩ )
131 130 115 oveq12d ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ⟨ ( ( 1st𝑍 ) ‘ 𝑧 ) , ( ( 1st𝐸 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1st𝐸 ) ‘ 𝑤 ) ) = ( ⟨ ( ( 1st𝑧 ) ( 1st𝑍 ) ( 2nd𝑧 ) ) , ( ( 1st𝑧 ) ( 1st𝐸 ) ( 2nd𝑧 ) ) ⟩ ( comp ‘ 𝑇 ) ( ( 1st𝑤 ) ( 1st𝐸 ) ( 2nd𝑤 ) ) ) )
132 103 108 oveq12d ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 𝑧 ( 2nd𝐸 ) 𝑤 ) = ( ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ ( 2nd𝐸 ) ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ ) )
133 132 122 fveq12d ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 𝑧 ( 2nd𝐸 ) 𝑤 ) ‘ 𝑔 ) = ( ( ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ ( 2nd𝐸 ) ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ ) ‘ ⟨ ( 1st𝑔 ) , ( 2nd𝑔 ) ⟩ ) )
134 df-ov ( ( 1st𝑔 ) ( ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ ( 2nd𝐸 ) ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ ) ( 2nd𝑔 ) ) = ( ( ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ ( 2nd𝐸 ) ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ ) ‘ ⟨ ( 1st𝑔 ) , ( 2nd𝑔 ) ⟩ )
135 133 134 eqtr4di ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 𝑧 ( 2nd𝐸 ) 𝑤 ) ‘ 𝑔 ) = ( ( 1st𝑔 ) ( ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ ( 2nd𝐸 ) ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ ) ( 2nd𝑔 ) ) )
136 103 fveq2d ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 𝑀𝑧 ) = ( 𝑀 ‘ ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ ) )
137 df-ov ( ( 1st𝑧 ) 𝑀 ( 2nd𝑧 ) ) = ( 𝑀 ‘ ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ )
138 136 137 eqtr4di ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( 𝑀𝑧 ) = ( ( 1st𝑧 ) 𝑀 ( 2nd𝑧 ) ) )
139 131 135 138 oveq123d ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( ( 𝑧 ( 2nd𝐸 ) 𝑤 ) ‘ 𝑔 ) ( ⟨ ( ( 1st𝑍 ) ‘ 𝑧 ) , ( ( 1st𝐸 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1st𝐸 ) ‘ 𝑤 ) ) ( 𝑀𝑧 ) ) = ( ( ( 1st𝑔 ) ( ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ ( 2nd𝐸 ) ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ ) ( 2nd𝑔 ) ) ( ⟨ ( ( 1st𝑧 ) ( 1st𝑍 ) ( 2nd𝑧 ) ) , ( ( 1st𝑧 ) ( 1st𝐸 ) ( 2nd𝑧 ) ) ⟩ ( comp ‘ 𝑇 ) ( ( 1st𝑤 ) ( 1st𝐸 ) ( 2nd𝑤 ) ) ) ( ( 1st𝑧 ) 𝑀 ( 2nd𝑧 ) ) ) )
140 101 126 139 3eqtr4d ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ) ) → ( ( 𝑀𝑤 ) ( ⟨ ( ( 1st𝑍 ) ‘ 𝑧 ) , ( ( 1st𝑍 ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1st𝐸 ) ‘ 𝑤 ) ) ( ( 𝑧 ( 2nd𝑍 ) 𝑤 ) ‘ 𝑔 ) ) = ( ( ( 𝑧 ( 2nd𝐸 ) 𝑤 ) ‘ 𝑔 ) ( ⟨ ( ( 1st𝑍 ) ‘ 𝑧 ) , ( ( 1st𝐸 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1st𝐸 ) ‘ 𝑤 ) ) ( 𝑀𝑧 ) ) )
141 140 ralrimivvva ( 𝜑 → ∀ 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∀ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∀ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ( ( 𝑀𝑤 ) ( ⟨ ( ( 1st𝑍 ) ‘ 𝑧 ) , ( ( 1st𝑍 ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1st𝐸 ) ‘ 𝑤 ) ) ( ( 𝑧 ( 2nd𝑍 ) 𝑤 ) ‘ 𝑔 ) ) = ( ( ( 𝑧 ( 2nd𝐸 ) 𝑤 ) ‘ 𝑔 ) ( ⟨ ( ( 1st𝑍 ) ‘ 𝑧 ) , ( ( 1st𝐸 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1st𝐸 ) ‘ 𝑤 ) ) ( 𝑀𝑧 ) ) )
142 eqid ( ( 𝑄 ×c 𝑂 ) Nat 𝑇 ) = ( ( 𝑄 ×c 𝑂 ) Nat 𝑇 )
143 eqid ( comp ‘ 𝑇 ) = ( comp ‘ 𝑇 )
144 142 33 90 29 143 37 44 isnat2 ( 𝜑 → ( 𝑀 ∈ ( 𝑍 ( ( 𝑄 ×c 𝑂 ) Nat 𝑇 ) 𝐸 ) ↔ ( 𝑀X 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ( ( ( 1st𝑍 ) ‘ 𝑧 ) ( Hom ‘ 𝑇 ) ( ( 1st𝐸 ) ‘ 𝑧 ) ) ∧ ∀ 𝑧 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∀ 𝑤 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ∀ 𝑔 ∈ ( 𝑧 ( Hom ‘ ( 𝑄 ×c 𝑂 ) ) 𝑤 ) ( ( 𝑀𝑤 ) ( ⟨ ( ( 1st𝑍 ) ‘ 𝑧 ) , ( ( 1st𝑍 ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1st𝐸 ) ‘ 𝑤 ) ) ( ( 𝑧 ( 2nd𝑍 ) 𝑤 ) ‘ 𝑔 ) ) = ( ( ( 𝑧 ( 2nd𝐸 ) 𝑤 ) ‘ 𝑔 ) ( ⟨ ( ( 1st𝑍 ) ‘ 𝑧 ) , ( ( 1st𝐸 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑇 ) ( ( 1st𝐸 ) ‘ 𝑤 ) ) ( 𝑀𝑧 ) ) ) ) )
145 71 141 144 mpbir2and ( 𝜑𝑀 ∈ ( 𝑍 ( ( 𝑄 ×c 𝑂 ) Nat 𝑇 ) 𝐸 ) )