MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  yonedainv Structured version   Visualization version   GIF version

Theorem yonedainv 16842
Description: The Yoneda Lemma with explicit inverse. (Contributed by Mario Carneiro, 29-Jan-2017.)
Hypotheses
Ref Expression
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𝑥))))
yonedainv.i 𝐼 = (Inv‘𝑅)
yonedainv.n 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥𝐵 ↦ (𝑢 ∈ ((1st𝑓)‘𝑥) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢)))))
Assertion
Ref Expression
yonedainv (𝜑𝑀(𝑍𝐼𝐸)𝑁)
Distinct variable groups:   𝑓,𝑎,𝑔,𝑥,𝑦, 1   𝑢,𝑎,𝑔,𝑦,𝐶,𝑓,𝑥   𝐸,𝑎,𝑓,𝑔,𝑢,𝑦   𝐵,𝑎,𝑓,𝑔,𝑢,𝑥,𝑦   𝑁,𝑎   𝑂,𝑎,𝑓,𝑔,𝑢,𝑥,𝑦   𝑆,𝑎,𝑓,𝑔,𝑢,𝑥,𝑦   𝑔,𝑀,𝑢,𝑦   𝑄,𝑎,𝑓,𝑔,𝑢,𝑥   𝑇,𝑓,𝑔,𝑢,𝑦   𝜑,𝑎,𝑓,𝑔,𝑢,𝑥,𝑦   𝑢,𝑅   𝑌,𝑎,𝑓,𝑔,𝑢,𝑥,𝑦   𝑍,𝑎,𝑓,𝑔,𝑢,𝑥,𝑦
Allowed substitution hints:   𝑄(𝑦)   𝑅(𝑥,𝑦,𝑓,𝑔,𝑎)   𝑇(𝑥,𝑎)   𝑈(𝑥,𝑦,𝑢,𝑓,𝑔,𝑎)   1 (𝑢)   𝐸(𝑥)   𝐻(𝑥,𝑦,𝑢,𝑓,𝑔,𝑎)   𝐼(𝑥,𝑦,𝑢,𝑓,𝑔,𝑎)   𝑀(𝑥,𝑓,𝑎)   𝑁(𝑥,𝑦,𝑢,𝑓,𝑔)   𝑉(𝑥,𝑦,𝑢,𝑓,𝑔,𝑎)   𝑊(𝑥,𝑦,𝑢,𝑓,𝑔,𝑎)

Proof of Theorem yonedainv
Dummy variables 𝑏 𝑘 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 yoneda.r . . 3 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)
2 eqid 2621 . . . 4 (𝑄 ×c 𝑂) = (𝑄 ×c 𝑂)
3 yoneda.q . . . . 5 𝑄 = (𝑂 FuncCat 𝑆)
43fucbas 16541 . . . 4 (𝑂 Func 𝑆) = (Base‘𝑄)
5 yoneda.o . . . . 5 𝑂 = (oppCat‘𝐶)
6 yoneda.b . . . . 5 𝐵 = (Base‘𝐶)
75, 6oppcbas 16299 . . . 4 𝐵 = (Base‘𝑂)
82, 4, 7xpcbas 16739 . . 3 ((𝑂 Func 𝑆) × 𝐵) = (Base‘(𝑄 ×c 𝑂))
9 eqid 2621 . . 3 ((𝑄 ×c 𝑂) Nat 𝑇) = ((𝑄 ×c 𝑂) Nat 𝑇)
10 yoneda.y . . . . 5 𝑌 = (Yon‘𝐶)
11 yoneda.1 . . . . 5 1 = (Id‘𝐶)
12 yoneda.s . . . . 5 𝑆 = (SetCat‘𝑈)
13 yoneda.t . . . . 5 𝑇 = (SetCat‘𝑉)
14 yoneda.h . . . . 5 𝐻 = (HomF𝑄)
15 yoneda.e . . . . 5 𝐸 = (𝑂 evalF 𝑆)
16 yoneda.z . . . . 5 𝑍 = (𝐻func ((⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))
17 yoneda.c . . . . 5 (𝜑𝐶 ∈ Cat)
18 yoneda.w . . . . 5 (𝜑𝑉𝑊)
19 yoneda.u . . . . 5 (𝜑 → ran (Homf𝐶) ⊆ 𝑈)
20 yoneda.v . . . . 5 (𝜑 → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
2110, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 17, 18, 19, 20yonedalem1 16833 . . . 4 (𝜑 → (𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)))
2221simpld 475 . . 3 (𝜑𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇))
2321simprd 479 . . 3 (𝜑𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇))
24 yonedainv.i . . 3 𝐼 = (Inv‘𝑅)
25 eqid 2621 . . 3 (Inv‘𝑇) = (Inv‘𝑇)
26 yoneda.m . . . 4 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥𝐵 ↦ (𝑎 ∈ (((1st𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎𝑥)‘( 1𝑥))))
2710, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 17, 18, 19, 20, 26yonedalem3 16841 . . 3 (𝜑𝑀 ∈ (𝑍((𝑄 ×c 𝑂) Nat 𝑇)𝐸))
2817adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → 𝐶 ∈ Cat)
2918adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → 𝑉𝑊)
3019adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ran (Homf𝐶) ⊆ 𝑈)
3120adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
32 simprl 793 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ∈ (𝑂 Func 𝑆))
33 simprr 795 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → 𝑤𝐵)
3410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33, 26yonedalem3a 16835 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))) ∧ (𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤)))
3534simprd 479 . . . . . . . . 9 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤))
3628adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → 𝐶 ∈ Cat)
3729adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → 𝑉𝑊)
3830adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → ran (Homf𝐶) ⊆ 𝑈)
3931adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
40 simplrl 799 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → ∈ (𝑂 Func 𝑆))
41 simplrr 800 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → 𝑤𝐵)
42 yonedainv.n . . . . . . . . . . . 12 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥𝐵 ↦ (𝑢 ∈ ((1st𝑓)‘𝑥) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢)))))
43 simpr 477 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → 𝑏 ∈ ((1st)‘𝑤))
4410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 36, 37, 38, 39, 40, 41, 42, 43yonedalem4c 16838 . . . . . . . . . . 11 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → ((𝑁𝑤)‘𝑏) ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
45 eqid 2621 . . . . . . . . . . 11 (𝑏 ∈ ((1st)‘𝑤) ↦ ((𝑁𝑤)‘𝑏)) = (𝑏 ∈ ((1st)‘𝑤) ↦ ((𝑁𝑤)‘𝑏))
4644, 45fmptd 6340 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑏 ∈ ((1st)‘𝑤) ↦ ((𝑁𝑤)‘𝑏)):((1st)‘𝑤)⟶(((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
47 fvex 6158 . . . . . . . . . . . . . . . 16 (Base‘𝐶) ∈ V
486, 47eqeltri 2694 . . . . . . . . . . . . . . 15 𝐵 ∈ V
4948mptex 6440 . . . . . . . . . . . . . 14 (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢))) ∈ V
50 eqid 2621 . . . . . . . . . . . . . 14 (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))) = (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢))))
5149, 50fnmpti 5979 . . . . . . . . . . . . 13 (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))) Fn ((1st)‘𝑤)
52 simpl 473 . . . . . . . . . . . . . . . . . . 19 ((𝑓 = 𝑥 = 𝑤) → 𝑓 = )
5352fveq2d 6152 . . . . . . . . . . . . . . . . . 18 ((𝑓 = 𝑥 = 𝑤) → (1st𝑓) = (1st))
54 simpr 477 . . . . . . . . . . . . . . . . . 18 ((𝑓 = 𝑥 = 𝑤) → 𝑥 = 𝑤)
5553, 54fveq12d 6154 . . . . . . . . . . . . . . . . 17 ((𝑓 = 𝑥 = 𝑤) → ((1st𝑓)‘𝑥) = ((1st)‘𝑤))
56 simplr 791 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → 𝑥 = 𝑤)
5756oveq2d 6620 . . . . . . . . . . . . . . . . . . 19 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → (𝑦(Hom ‘𝐶)𝑥) = (𝑦(Hom ‘𝐶)𝑤))
58 simpll 789 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → 𝑓 = )
5958fveq2d 6152 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → (2nd𝑓) = (2nd))
60 eqidd 2622 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → 𝑦 = 𝑦)
6159, 56, 60oveq123d 6625 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → (𝑥(2nd𝑓)𝑦) = (𝑤(2nd)𝑦))
6261fveq1d 6150 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → ((𝑥(2nd𝑓)𝑦)‘𝑔) = ((𝑤(2nd)𝑦)‘𝑔))
6362fveq1d 6150 . . . . . . . . . . . . . . . . . . 19 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢) = (((𝑤(2nd)𝑦)‘𝑔)‘𝑢))
6457, 63mpteq12dv 4693 . . . . . . . . . . . . . . . . . 18 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢)) = (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))
6564mpteq2dva 4704 . . . . . . . . . . . . . . . . 17 ((𝑓 = 𝑥 = 𝑤) → (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢))) = (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢))))
6655, 65mpteq12dv 4693 . . . . . . . . . . . . . . . 16 ((𝑓 = 𝑥 = 𝑤) → (𝑢 ∈ ((1st𝑓)‘𝑥) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢)))) = (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))))
67 fvex 6158 . . . . . . . . . . . . . . . . 17 ((1st)‘𝑤) ∈ V
6867mptex 6440 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))) ∈ V
6966, 42, 68ovmpt2a 6744 . . . . . . . . . . . . . . 15 (( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵) → (𝑁𝑤) = (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))))
7069adantl 482 . . . . . . . . . . . . . 14 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑁𝑤) = (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))))
7170fneq1d 5939 . . . . . . . . . . . . 13 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑁𝑤) Fn ((1st)‘𝑤) ↔ (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))) Fn ((1st)‘𝑤)))
7251, 71mpbiri 248 . . . . . . . . . . . 12 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑁𝑤) Fn ((1st)‘𝑤))
73 dffn5 6198 . . . . . . . . . . . 12 ((𝑁𝑤) Fn ((1st)‘𝑤) ↔ (𝑁𝑤) = (𝑏 ∈ ((1st)‘𝑤) ↦ ((𝑁𝑤)‘𝑏)))
7472, 73sylib 208 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑁𝑤) = (𝑏 ∈ ((1st)‘𝑤) ↦ ((𝑁𝑤)‘𝑏)))
755oppccat 16303 . . . . . . . . . . . . . 14 (𝐶 ∈ Cat → 𝑂 ∈ Cat)
7617, 75syl 17 . . . . . . . . . . . . 13 (𝜑𝑂 ∈ Cat)
7776adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → 𝑂 ∈ Cat)
7820unssbd 3769 . . . . . . . . . . . . . . 15 (𝜑𝑈𝑉)
7918, 78ssexd 4765 . . . . . . . . . . . . . 14 (𝜑𝑈 ∈ V)
8012setccat 16656 . . . . . . . . . . . . . 14 (𝑈 ∈ V → 𝑆 ∈ Cat)
8179, 80syl 17 . . . . . . . . . . . . 13 (𝜑𝑆 ∈ Cat)
8281adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → 𝑆 ∈ Cat)
8315, 77, 82, 7, 32, 33evlf1 16781 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((1st𝐸)𝑤) = ((1st)‘𝑤))
8410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33yonedalem21 16834 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((1st𝑍)𝑤) = (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
8574, 83, 84feq123d 5991 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑁𝑤):((1st𝐸)𝑤)⟶((1st𝑍)𝑤) ↔ (𝑏 ∈ ((1st)‘𝑤) ↦ ((𝑁𝑤)‘𝑏)):((1st)‘𝑤)⟶(((1st𝑌)‘𝑤)(𝑂 Nat 𝑆))))
8646, 85mpbird 247 . . . . . . . . 9 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑁𝑤):((1st𝐸)𝑤)⟶((1st𝑍)𝑤))
87 fcompt 6354 . . . . . . . . . . 11 (((𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤) ∧ (𝑁𝑤):((1st𝐸)𝑤)⟶((1st𝑍)𝑤)) → ((𝑀𝑤) ∘ (𝑁𝑤)) = (𝑘 ∈ ((1st𝐸)𝑤) ↦ ((𝑀𝑤)‘((𝑁𝑤)‘𝑘))))
8835, 86, 87syl2anc 692 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤) ∘ (𝑁𝑤)) = (𝑘 ∈ ((1st𝐸)𝑤) ↦ ((𝑀𝑤)‘((𝑁𝑤)‘𝑘))))
8983eleq2d 2684 . . . . . . . . . . . . . 14 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑘 ∈ ((1st𝐸)𝑤) ↔ 𝑘 ∈ ((1st)‘𝑤)))
9089biimpa 501 . . . . . . . . . . . . 13 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st𝐸)𝑤)) → 𝑘 ∈ ((1st)‘𝑤))
9128adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝐶 ∈ Cat)
9229adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝑉𝑊)
9330adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ran (Homf𝐶) ⊆ 𝑈)
9431adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
95 simplrl 799 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ∈ (𝑂 Func 𝑆))
96 simplrr 800 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝑤𝐵)
9710, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 91, 92, 93, 94, 95, 96, 26yonedalem3a 16835 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑀𝑤) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))) ∧ (𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤)))
9897simpld 475 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (𝑀𝑤) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))))
9998fveq1d 6150 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑀𝑤)‘((𝑁𝑤)‘𝑘)) = ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘((𝑁𝑤)‘𝑘)))
100 fvex 6158 . . . . . . . . . . . . . . . . . 18 ((𝑁𝑤)‘𝑏) ∈ V
101100a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → ((𝑁𝑤)‘𝑏) ∈ V)
102101, 74, 44fmpt2d 6348 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑁𝑤):((1st)‘𝑤)⟶(((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
103102ffvelrnda 6315 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑁𝑤)‘𝑘) ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
104 fveq1 6147 . . . . . . . . . . . . . . . . 17 (𝑎 = ((𝑁𝑤)‘𝑘) → (𝑎𝑤) = (((𝑁𝑤)‘𝑘)‘𝑤))
105104fveq1d 6150 . . . . . . . . . . . . . . . 16 (𝑎 = ((𝑁𝑤)‘𝑘) → ((𝑎𝑤)‘( 1𝑤)) = ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)))
106 eqid 2621 . . . . . . . . . . . . . . . 16 (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))
107 fvex 6158 . . . . . . . . . . . . . . . 16 ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)) ∈ V
108105, 106, 107fvmpt 6239 . . . . . . . . . . . . . . 15 (((𝑁𝑤)‘𝑘) ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) → ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘((𝑁𝑤)‘𝑘)) = ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)))
109103, 108syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘((𝑁𝑤)‘𝑘)) = ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)))
110 simpr 477 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝑘 ∈ ((1st)‘𝑤))
111 eqid 2621 . . . . . . . . . . . . . . . . 17 (Hom ‘𝐶) = (Hom ‘𝐶)
1126, 111, 11, 91, 96catidcl 16264 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ( 1𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤))
11310, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 91, 92, 93, 94, 95, 96, 42, 110, 96, 112yonedalem4b 16837 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)) = (((𝑤(2nd)𝑤)‘( 1𝑤))‘𝑘))
114 eqid 2621 . . . . . . . . . . . . . . . . . 18 (Id‘𝑂) = (Id‘𝑂)
115 eqid 2621 . . . . . . . . . . . . . . . . . 18 (Id‘𝑆) = (Id‘𝑆)
116 relfunc 16443 . . . . . . . . . . . . . . . . . . 19 Rel (𝑂 Func 𝑆)
117 1st2ndbr 7162 . . . . . . . . . . . . . . . . . . 19 ((Rel (𝑂 Func 𝑆) ∧ ∈ (𝑂 Func 𝑆)) → (1st)(𝑂 Func 𝑆)(2nd))
118116, 95, 117sylancr 694 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (1st)(𝑂 Func 𝑆)(2nd))
1197, 114, 115, 118, 96funcid 16451 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑤(2nd)𝑤)‘((Id‘𝑂)‘𝑤)) = ((Id‘𝑆)‘((1st)‘𝑤)))
1205, 11oppcid 16302 . . . . . . . . . . . . . . . . . . . 20 (𝐶 ∈ Cat → (Id‘𝑂) = 1 )
12191, 120syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (Id‘𝑂) = 1 )
122121fveq1d 6150 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((Id‘𝑂)‘𝑤) = ( 1𝑤))
123122fveq2d 6152 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑤(2nd)𝑤)‘((Id‘𝑂)‘𝑤)) = ((𝑤(2nd)𝑤)‘( 1𝑤)))
12479ad2antrr 761 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝑈 ∈ V)
125 eqid 2621 . . . . . . . . . . . . . . . . . . . . 21 (Base‘𝑆) = (Base‘𝑆)
1267, 125, 118funcf1 16447 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (1st):𝐵⟶(Base‘𝑆))
12712, 124setcbas 16649 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝑈 = (Base‘𝑆))
128127feq3d 5989 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((1st):𝐵𝑈 ↔ (1st):𝐵⟶(Base‘𝑆)))
129126, 128mpbird 247 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (1st):𝐵𝑈)
130129, 96ffvelrnd 6316 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((1st)‘𝑤) ∈ 𝑈)
13112, 115, 124, 130setcid 16657 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((Id‘𝑆)‘((1st)‘𝑤)) = ( I ↾ ((1st)‘𝑤)))
132119, 123, 1313eqtr3d 2663 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑤(2nd)𝑤)‘( 1𝑤)) = ( I ↾ ((1st)‘𝑤)))
133132fveq1d 6150 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (((𝑤(2nd)𝑤)‘( 1𝑤))‘𝑘) = (( I ↾ ((1st)‘𝑤))‘𝑘))
134 fvresi 6393 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ((1st)‘𝑤) → (( I ↾ ((1st)‘𝑤))‘𝑘) = 𝑘)
135134adantl 482 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (( I ↾ ((1st)‘𝑤))‘𝑘) = 𝑘)
136113, 133, 1353eqtrd 2659 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)) = 𝑘)
13799, 109, 1363eqtrd 2659 . . . . . . . . . . . . 13 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑀𝑤)‘((𝑁𝑤)‘𝑘)) = 𝑘)
13890, 137syldan 487 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st𝐸)𝑤)) → ((𝑀𝑤)‘((𝑁𝑤)‘𝑘)) = 𝑘)
139138mpteq2dva 4704 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑘 ∈ ((1st𝐸)𝑤) ↦ ((𝑀𝑤)‘((𝑁𝑤)‘𝑘))) = (𝑘 ∈ ((1st𝐸)𝑤) ↦ 𝑘))
140 mptresid 5415 . . . . . . . . . . 11 (𝑘 ∈ ((1st𝐸)𝑤) ↦ 𝑘) = ( I ↾ ((1st𝐸)𝑤))
141139, 140syl6eq 2671 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑘 ∈ ((1st𝐸)𝑤) ↦ ((𝑀𝑤)‘((𝑁𝑤)‘𝑘))) = ( I ↾ ((1st𝐸)𝑤)))
14288, 141eqtrd 2655 . . . . . . . . 9 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤) ∘ (𝑁𝑤)) = ( I ↾ ((1st𝐸)𝑤)))
143 fcompt 6354 . . . . . . . . . . 11 (((𝑁𝑤):((1st𝐸)𝑤)⟶((1st𝑍)𝑤) ∧ (𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤)) → ((𝑁𝑤) ∘ (𝑀𝑤)) = (𝑏 ∈ ((1st𝑍)𝑤) ↦ ((𝑁𝑤)‘((𝑀𝑤)‘𝑏))))
14486, 35, 143syl2anc 692 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑁𝑤) ∘ (𝑀𝑤)) = (𝑏 ∈ ((1st𝑍)𝑤) ↦ ((𝑁𝑤)‘((𝑀𝑤)‘𝑏))))
145 eqid 2621 . . . . . . . . . . . . . 14 (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆)
14628adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝐶 ∈ Cat)
14729adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑉𝑊)
14830adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ran (Homf𝐶) ⊆ 𝑈)
14931adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
150 simplrl 799 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ∈ (𝑂 Func 𝑆))
151 simplrr 800 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑤𝐵)
15283feq3d 5989 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤) ↔ (𝑀𝑤):((1st𝑍)𝑤)⟶((1st)‘𝑤)))
15335, 152mpbid 222 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑀𝑤):((1st𝑍)𝑤)⟶((1st)‘𝑤))
154153ffvelrnda 6315 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑀𝑤)‘𝑏) ∈ ((1st)‘𝑤))
15510, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 146, 147, 148, 149, 150, 151, 42, 154yonedalem4c 16838 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑁𝑤)‘((𝑀𝑤)‘𝑏)) ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
156145, 155nat1st2nd 16532 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑁𝑤)‘((𝑀𝑤)‘𝑏)) ∈ (⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st), (2nd)⟩))
157145, 156, 7natfn 16535 . . . . . . . . . . . . 13 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑁𝑤)‘((𝑀𝑤)‘𝑏)) Fn 𝐵)
15884eleq2d 2684 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑏 ∈ ((1st𝑍)𝑤) ↔ 𝑏 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆))))
159158biimpa 501 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑏 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
160145, 159nat1st2nd 16532 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑏 ∈ (⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st), (2nd)⟩))
161145, 160, 7natfn 16535 . . . . . . . . . . . . 13 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑏 Fn 𝐵)
162146adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → 𝐶 ∈ Cat)
163151adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → 𝑤𝐵)
164 simpr 477 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → 𝑧𝐵)
16510, 6, 162, 163, 111, 164yon11 16825 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((1st ‘((1st𝑌)‘𝑤))‘𝑧) = (𝑧(Hom ‘𝐶)𝑤))
166165eleq2d 2684 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ↔ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))
167166biimpa 501 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧)) → 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤))
168162adantr 481 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝐶 ∈ Cat)
169147ad2antrr 761 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑉𝑊)
170148ad2antrr 761 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ran (Homf𝐶) ⊆ 𝑈)
171149ad2antrr 761 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
172150ad2antrr 761 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ∈ (𝑂 Func 𝑆))
173163adantr 481 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑤𝐵)
174154ad2antrr 761 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑀𝑤)‘𝑏) ∈ ((1st)‘𝑤))
175 simplr 791 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑧𝐵)
176 simpr 477 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤))
17710, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 168, 169, 170, 171, 172, 173, 42, 174, 175, 176yonedalem4b 16837 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑀𝑤)‘𝑏)))
17810, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 168, 169, 170, 171, 172, 173, 26yonedalem3a 16835 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑀𝑤) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))) ∧ (𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤)))
179178simpld 475 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑀𝑤) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))))
180179fveq1d 6150 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑀𝑤)‘𝑏) = ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘𝑏))
181159ad2antrr 761 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑏 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
182 fveq1 6147 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑏 → (𝑎𝑤) = (𝑏𝑤))
183182fveq1d 6150 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑏 → ((𝑎𝑤)‘( 1𝑤)) = ((𝑏𝑤)‘( 1𝑤)))
184 fvex 6158 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏𝑤)‘( 1𝑤)) ∈ V
185183, 106, 184fvmpt 6239 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) → ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘𝑏) = ((𝑏𝑤)‘( 1𝑤)))
186181, 185syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘𝑏) = ((𝑏𝑤)‘( 1𝑤)))
187180, 186eqtrd 2655 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑀𝑤)‘𝑏) = ((𝑏𝑤)‘( 1𝑤)))
188187fveq2d 6152 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd)𝑧)‘𝑘)‘((𝑀𝑤)‘𝑏)) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))))
189160ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑏 ∈ (⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st), (2nd)⟩))
190 eqid 2621 . . . . . . . . . . . . . . . . . . . . . 22 (Hom ‘𝑂) = (Hom ‘𝑂)
191 eqid 2621 . . . . . . . . . . . . . . . . . . . . . 22 (comp‘𝑆) = (comp‘𝑆)
192111, 5oppchom 16296 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤(Hom ‘𝑂)𝑧) = (𝑧(Hom ‘𝐶)𝑤)
193176, 192syl6eleqr 2709 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑘 ∈ (𝑤(Hom ‘𝑂)𝑧))
194145, 189, 7, 190, 191, 173, 175, 193nati 16536 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏𝑧)(⟨((1st ‘((1st𝑌)‘𝑤))‘𝑤), ((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟩(comp‘𝑆)((1st)‘𝑧))((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)) = (((𝑤(2nd)𝑧)‘𝑘)(⟨((1st ‘((1st𝑌)‘𝑤))‘𝑤), ((1st)‘𝑤)⟩(comp‘𝑆)((1st)‘𝑧))(𝑏𝑤)))
19579ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑈 ∈ V)
196195adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → 𝑈 ∈ V)
197196adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑈 ∈ V)
198 relfunc 16443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Rel (𝐶 Func 𝑄)
19910, 17, 5, 12, 3, 79, 19yoncl 16823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑𝑌 ∈ (𝐶 Func 𝑄))
200 1st2ndbr 7162 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((Rel (𝐶 Func 𝑄) ∧ 𝑌 ∈ (𝐶 Func 𝑄)) → (1st𝑌)(𝐶 Func 𝑄)(2nd𝑌))
201198, 199, 200sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (1st𝑌)(𝐶 Func 𝑄)(2nd𝑌))
2026, 4, 201funcf1 16447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (1st𝑌):𝐵⟶(𝑂 Func 𝑆))
203202ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st𝑌):𝐵⟶(𝑂 Func 𝑆))
204203, 151ffvelrnd 6316 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st𝑌)‘𝑤) ∈ (𝑂 Func 𝑆))
205 1st2ndbr 7162 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Rel (𝑂 Func 𝑆) ∧ ((1st𝑌)‘𝑤) ∈ (𝑂 Func 𝑆)) → (1st ‘((1st𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st𝑌)‘𝑤)))
206116, 204, 205sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st ‘((1st𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st𝑌)‘𝑤)))
2077, 125, 206funcf1 16447 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st ‘((1st𝑌)‘𝑤)):𝐵⟶(Base‘𝑆))
20812, 195setcbas 16649 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑈 = (Base‘𝑆))
209208feq3d 5989 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st ‘((1st𝑌)‘𝑤)):𝐵𝑈 ↔ (1st ‘((1st𝑌)‘𝑤)):𝐵⟶(Base‘𝑆)))
210207, 209mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st ‘((1st𝑌)‘𝑤)):𝐵𝑈)
211210, 151ffvelrnd 6316 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st ‘((1st𝑌)‘𝑤))‘𝑤) ∈ 𝑈)
212211ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘((1st𝑌)‘𝑤))‘𝑤) ∈ 𝑈)
213210ffvelrnda 6315 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ∈ 𝑈)
214213adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ∈ 𝑈)
215116, 150, 117sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st)(𝑂 Func 𝑆)(2nd))
2167, 125, 215funcf1 16447 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st):𝐵⟶(Base‘𝑆))
217208feq3d 5989 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st):𝐵𝑈 ↔ (1st):𝐵⟶(Base‘𝑆)))
218216, 217mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st):𝐵𝑈)
219218ffvelrnda 6315 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((1st)‘𝑧) ∈ 𝑈)
220219adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st)‘𝑧) ∈ 𝑈)
221 eqid 2621 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Hom ‘𝑆) = (Hom ‘𝑆)
222206ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1st ‘((1st𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st𝑌)‘𝑤)))
2237, 190, 221, 222, 173, 175funcf2 16449 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧):(𝑤(Hom ‘𝑂)𝑧)⟶(((1st ‘((1st𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑤))‘𝑧)))
224223, 193ffvelrnd 6316 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑤))‘𝑧)))
22512, 197, 221, 212, 214elsetchom 16652 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑤))‘𝑧)) ↔ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st ‘((1st𝑌)‘𝑤))‘𝑧)))
226224, 225mpbid 222 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st ‘((1st𝑌)‘𝑤))‘𝑧))
227160adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → 𝑏 ∈ (⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st), (2nd)⟩))
228145, 227, 7, 221, 164natcl 16534 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (𝑏𝑧) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st)‘𝑧)))
22912, 196, 221, 213, 219elsetchom 16652 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((𝑏𝑧) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st)‘𝑧)) ↔ (𝑏𝑧):((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟶((1st)‘𝑧)))
230228, 229mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (𝑏𝑧):((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟶((1st)‘𝑧))
231230adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑏𝑧):((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟶((1st)‘𝑧))
23212, 197, 191, 212, 214, 220, 226, 231setcco 16654 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏𝑧)(⟨((1st ‘((1st𝑌)‘𝑤))‘𝑤), ((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟩(comp‘𝑆)((1st)‘𝑧))((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)) = ((𝑏𝑧) ∘ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)))
233218, 151ffvelrnd 6316 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st)‘𝑤) ∈ 𝑈)
234233ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st)‘𝑤) ∈ 𝑈)
235145, 160, 7, 221, 151natcl 16534 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (𝑏𝑤) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st)‘𝑤)))
23612, 195, 221, 211, 233elsetchom 16652 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑏𝑤) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st)‘𝑤)) ↔ (𝑏𝑤):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st)‘𝑤)))
237235, 236mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (𝑏𝑤):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st)‘𝑤))
238237ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑏𝑤):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st)‘𝑤))
239116, 172, 117sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1st)(𝑂 Func 𝑆)(2nd))
2407, 190, 221, 239, 173, 175funcf2 16449 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑤(2nd)𝑧):(𝑤(Hom ‘𝑂)𝑧)⟶(((1st)‘𝑤)(Hom ‘𝑆)((1st)‘𝑧)))
241240, 193ffvelrnd 6316 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd)𝑧)‘𝑘) ∈ (((1st)‘𝑤)(Hom ‘𝑆)((1st)‘𝑧)))
24212, 197, 221, 234, 220elsetchom 16652 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd)𝑧)‘𝑘) ∈ (((1st)‘𝑤)(Hom ‘𝑆)((1st)‘𝑧)) ↔ ((𝑤(2nd)𝑧)‘𝑘):((1st)‘𝑤)⟶((1st)‘𝑧)))
243241, 242mpbid 222 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd)𝑧)‘𝑘):((1st)‘𝑤)⟶((1st)‘𝑧))
24412, 197, 191, 212, 234, 220, 238, 243setcco 16654 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd)𝑧)‘𝑘)(⟨((1st ‘((1st𝑌)‘𝑤))‘𝑤), ((1st)‘𝑤)⟩(comp‘𝑆)((1st)‘𝑧))(𝑏𝑤)) = (((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤)))
245194, 232, 2443eqtr3d 2663 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏𝑧) ∘ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)) = (((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤)))
246245fveq1d 6150 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑏𝑧) ∘ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘))‘( 1𝑤)) = ((((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤))‘( 1𝑤)))
2476, 111, 11, 146, 151catidcl 16264 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ( 1𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤))
24810, 6, 146, 151, 111, 151yon11 16825 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st ‘((1st𝑌)‘𝑤))‘𝑤) = (𝑤(Hom ‘𝐶)𝑤))
249247, 248eleqtrrd 2701 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ( 1𝑤) ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑤))
250249ad2antrr 761 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ( 1𝑤) ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑤))
251 fvco3 6232 . . . . . . . . . . . . . . . . . . . 20 ((((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st ‘((1st𝑌)‘𝑤))‘𝑧) ∧ ( 1𝑤) ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑤)) → (((𝑏𝑧) ∘ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘))‘( 1𝑤)) = ((𝑏𝑧)‘(((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤))))
252226, 250, 251syl2anc 692 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑏𝑧) ∘ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘))‘( 1𝑤)) = ((𝑏𝑧)‘(((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤))))
253 fvco3 6232 . . . . . . . . . . . . . . . . . . . . 21 (((𝑏𝑤):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st)‘𝑤) ∧ ( 1𝑤) ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑤)) → ((((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤))‘( 1𝑤)) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))))
254237, 249, 253syl2anc 692 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤))‘( 1𝑤)) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))))
255254ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤))‘( 1𝑤)) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))))
256246, 252, 2553eqtr3d 2663 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏𝑧)‘(((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤))) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))))
257 eqid 2621 . . . . . . . . . . . . . . . . . . . . 21 (comp‘𝐶) = (comp‘𝐶)
258247ad2antrr 761 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ( 1𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤))
25910, 6, 168, 173, 111, 173, 257, 175, 176, 258yon12 16826 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤)) = (( 1𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐶)𝑤)𝑘))
2606, 111, 11, 168, 175, 257, 173, 176catlid 16265 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (( 1𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐶)𝑤)𝑘) = 𝑘)
261259, 260eqtrd 2655 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤)) = 𝑘)
262261fveq2d 6152 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏𝑧)‘(((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤))) = ((𝑏𝑧)‘𝑘))
263256, 262eqtr3d 2657 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))) = ((𝑏𝑧)‘𝑘))
264177, 188, 2633eqtrd 2659 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = ((𝑏𝑧)‘𝑘))
265167, 264syldan 487 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧)) → ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = ((𝑏𝑧)‘𝑘))
266265mpteq2dva 4704 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ↦ ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧)‘𝑘)) = (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ↦ ((𝑏𝑧)‘𝑘)))
267156adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((𝑁𝑤)‘((𝑀𝑤)‘𝑏)) ∈ (⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st), (2nd)⟩))
268145, 267, 7, 221, 164natcl 16534 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st)‘𝑧)))
26912, 196, 221, 213, 219elsetchom 16652 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st)‘𝑧)) ↔ (((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧):((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟶((1st)‘𝑧)))
270268, 269mpbid 222 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧):((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟶((1st)‘𝑧))
271270feqmptd 6206 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧) = (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ↦ ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧)‘𝑘)))
272230feqmptd 6206 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (𝑏𝑧) = (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ↦ ((𝑏𝑧)‘𝑘)))
273266, 271, 2723eqtr4d 2665 . . . . . . . . . . . . 13 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧) = (𝑏𝑧))
274157, 161, 273eqfnfvd 6270 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑁𝑤)‘((𝑀𝑤)‘𝑏)) = 𝑏)
275274mpteq2dva 4704 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑏 ∈ ((1st𝑍)𝑤) ↦ ((𝑁𝑤)‘((𝑀𝑤)‘𝑏))) = (𝑏 ∈ ((1st𝑍)𝑤) ↦ 𝑏))
276 mptresid 5415 . . . . . . . . . . 11 (𝑏 ∈ ((1st𝑍)𝑤) ↦ 𝑏) = ( I ↾ ((1st𝑍)𝑤))
277275, 276syl6eq 2671 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑏 ∈ ((1st𝑍)𝑤) ↦ ((𝑁𝑤)‘((𝑀𝑤)‘𝑏))) = ( I ↾ ((1st𝑍)𝑤)))
278144, 277eqtrd 2655 . . . . . . . . 9 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑁𝑤) ∘ (𝑀𝑤)) = ( I ↾ ((1st𝑍)𝑤)))
279 fcof1o 6505 . . . . . . . . 9 ((((𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤) ∧ (𝑁𝑤):((1st𝐸)𝑤)⟶((1st𝑍)𝑤)) ∧ (((𝑀𝑤) ∘ (𝑁𝑤)) = ( I ↾ ((1st𝐸)𝑤)) ∧ ((𝑁𝑤) ∘ (𝑀𝑤)) = ( I ↾ ((1st𝑍)𝑤)))) → ((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑀𝑤) = (𝑁𝑤)))
28035, 86, 142, 278, 279syl22anc 1324 . . . . . . . 8 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑀𝑤) = (𝑁𝑤)))
281 eqcom 2628 . . . . . . . . 9 ((𝑀𝑤) = (𝑁𝑤) ↔ (𝑁𝑤) = (𝑀𝑤))
282281anbi2i 729 . . . . . . . 8 (((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑀𝑤) = (𝑁𝑤)) ↔ ((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑁𝑤) = (𝑀𝑤)))
283280, 282sylib 208 . . . . . . 7 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑁𝑤) = (𝑀𝑤)))
284 eqid 2621 . . . . . . . . . . 11 (Base‘𝑇) = (Base‘𝑇)
285 relfunc 16443 . . . . . . . . . . . 12 Rel ((𝑄 ×c 𝑂) Func 𝑇)
286 1st2ndbr 7162 . . . . . . . . . . . 12 ((Rel ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st𝑍)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝑍))
287285, 22, 286sylancr 694 . . . . . . . . . . 11 (𝜑 → (1st𝑍)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝑍))
2888, 284, 287funcf1 16447 . . . . . . . . . 10 (𝜑 → (1st𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
28913, 18setcbas 16649 . . . . . . . . . . 11 (𝜑𝑉 = (Base‘𝑇))
290289feq3d 5989 . . . . . . . . . 10 (𝜑 → ((1st𝑍):((𝑂 Func 𝑆) × 𝐵)⟶𝑉 ↔ (1st𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇)))
291288, 290mpbird 247 . . . . . . . . 9 (𝜑 → (1st𝑍):((𝑂 Func 𝑆) × 𝐵)⟶𝑉)
292291fovrnda 6758 . . . . . . . 8 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((1st𝑍)𝑤) ∈ 𝑉)
293 1st2ndbr 7162 . . . . . . . . . . . 12 ((Rel ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st𝐸)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝐸))
294285, 23, 293sylancr 694 . . . . . . . . . . 11 (𝜑 → (1st𝐸)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝐸))
2958, 284, 294funcf1 16447 . . . . . . . . . 10 (𝜑 → (1st𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
296289feq3d 5989 . . . . . . . . . 10 (𝜑 → ((1st𝐸):((𝑂 Func 𝑆) × 𝐵)⟶𝑉 ↔ (1st𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇)))
297295, 296mpbird 247 . . . . . . . . 9 (𝜑 → (1st𝐸):((𝑂 Func 𝑆) × 𝐵)⟶𝑉)
298297fovrnda 6758 . . . . . . . 8 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((1st𝐸)𝑤) ∈ 𝑉)
29913, 29, 292, 298, 25setcinv 16661 . . . . . . 7 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤)(((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤))(𝑁𝑤) ↔ ((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑁𝑤) = (𝑀𝑤))))
300283, 299mpbird 247 . . . . . 6 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑀𝑤)(((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤))(𝑁𝑤))
301300ralrimivva 2965 . . . . 5 (𝜑 → ∀ ∈ (𝑂 Func 𝑆)∀𝑤𝐵 (𝑀𝑤)(((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤))(𝑁𝑤))
302 fveq2 6148 . . . . . . . 8 (𝑧 = ⟨, 𝑤⟩ → (𝑀𝑧) = (𝑀‘⟨, 𝑤⟩))
303 df-ov 6607 . . . . . . . 8 (𝑀𝑤) = (𝑀‘⟨, 𝑤⟩)
304302, 303syl6eqr 2673 . . . . . . 7 (𝑧 = ⟨, 𝑤⟩ → (𝑀𝑧) = (𝑀𝑤))
305 fveq2 6148 . . . . . . . . 9 (𝑧 = ⟨, 𝑤⟩ → ((1st𝑍)‘𝑧) = ((1st𝑍)‘⟨, 𝑤⟩))
306 df-ov 6607 . . . . . . . . 9 ((1st𝑍)𝑤) = ((1st𝑍)‘⟨, 𝑤⟩)
307305, 306syl6eqr 2673 . . . . . . . 8 (𝑧 = ⟨, 𝑤⟩ → ((1st𝑍)‘𝑧) = ((1st𝑍)𝑤))
308 fveq2 6148 . . . . . . . . 9 (𝑧 = ⟨, 𝑤⟩ → ((1st𝐸)‘𝑧) = ((1st𝐸)‘⟨, 𝑤⟩))
309 df-ov 6607 . . . . . . . . 9 ((1st𝐸)𝑤) = ((1st𝐸)‘⟨, 𝑤⟩)
310308, 309syl6eqr 2673 . . . . . . . 8 (𝑧 = ⟨, 𝑤⟩ → ((1st𝐸)‘𝑧) = ((1st𝐸)𝑤))
311307, 310oveq12d 6622 . . . . . . 7 (𝑧 = ⟨, 𝑤⟩ → (((1st𝑍)‘𝑧)(Inv‘𝑇)((1st𝐸)‘𝑧)) = (((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤)))
312 fveq2 6148 . . . . . . . 8 (𝑧 = ⟨, 𝑤⟩ → (𝑁𝑧) = (𝑁‘⟨, 𝑤⟩))
313 df-ov 6607 . . . . . . . 8 (𝑁𝑤) = (𝑁‘⟨, 𝑤⟩)
314312, 313syl6eqr 2673 . . . . . . 7 (𝑧 = ⟨, 𝑤⟩ → (𝑁𝑧) = (𝑁𝑤))
315304, 311, 314breq123d 4627 . . . . . 6 (𝑧 = ⟨, 𝑤⟩ → ((𝑀𝑧)(((1st𝑍)‘𝑧)(Inv‘𝑇)((1st𝐸)‘𝑧))(𝑁𝑧) ↔ (𝑀𝑤)(((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤))(𝑁𝑤)))
316315ralxp 5223 . . . . 5 (∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑀𝑧)(((1st𝑍)‘𝑧)(Inv‘𝑇)((1st𝐸)‘𝑧))(𝑁𝑧) ↔ ∀ ∈ (𝑂 Func 𝑆)∀𝑤𝐵 (𝑀𝑤)(((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤))(𝑁𝑤))
317301, 316sylibr 224 . . . 4 (𝜑 → ∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑀𝑧)(((1st𝑍)‘𝑧)(Inv‘𝑇)((1st𝐸)‘𝑧))(𝑁𝑧))
318317r19.21bi 2927 . . 3 ((𝜑𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)) → (𝑀𝑧)(((1st𝑍)‘𝑧)(Inv‘𝑇)((1st𝐸)‘𝑧))(𝑁𝑧))
3191, 8, 9, 22, 23, 24, 25, 27, 318invfuc 16555 . 2 (𝜑𝑀(𝑍𝐼𝐸)(𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁𝑧)))
320 fvex 6158 . . . . 5 ((1st𝑓)‘𝑥) ∈ V
321320mptex 6440 . . . 4 (𝑢 ∈ ((1st𝑓)‘𝑥) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢)))) ∈ V
32242, 321fnmpt2i 7184 . . 3 𝑁 Fn ((𝑂 Func 𝑆) × 𝐵)
323 dffn5 6198 . . 3 (𝑁 Fn ((𝑂 Func 𝑆) × 𝐵) ↔ 𝑁 = (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁𝑧)))
324322, 323mpbi 220 . 2 𝑁 = (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁𝑧))
325319, 324syl6breqr 4655 1 (𝜑𝑀(𝑍𝐼𝐸)𝑁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  wcel 1987  wral 2907  Vcvv 3186  cun 3553  wss 3555  cop 4154   class class class wbr 4613  cmpt 4673   I cid 4984   × cxp 5072  ccnv 5073  ran crn 5075  cres 5076  ccom 5078  Rel wrel 5079   Fn wfn 5842  wf 5843  1-1-ontowf1o 5846  cfv 5847  (class class class)co 6604  cmpt2 6606  1st c1st 7111  2nd c2nd 7112  tpos ctpos 7296  Basecbs 15781  Hom chom 15873  compcco 15874  Catccat 16246  Idccid 16247  Homf chomf 16248  oppCatcoppc 16292  Invcinv 16326   Func cfunc 16435  func ccofu 16437   Nat cnat 16522   FuncCat cfuc 16523  SetCatcsetc 16646   ×c cxpc 16729   1stF c1stf 16730   2ndF c2ndf 16731   ⟨,⟩F cprf 16732   evalF cevlf 16770  HomFchof 16809  Yoncyon 16810
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-tpos 7297  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-oadd 7509  df-er 7687  df-map 7804  df-pm 7805  df-ixp 7853  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-nn 10965  df-2 11023  df-3 11024  df-4 11025  df-5 11026  df-6 11027  df-7 11028  df-8 11029  df-9 11030  df-n0 11237  df-z 11322  df-dec 11438  df-uz 11632  df-fz 12269  df-struct 15783  df-ndx 15784  df-slot 15785  df-base 15786  df-sets 15787  df-ress 15788  df-hom 15887  df-cco 15888  df-cat 16250  df-cid 16251  df-homf 16252  df-comf 16253  df-oppc 16293  df-sect 16328  df-inv 16329  df-ssc 16391  df-resc 16392  df-subc 16393  df-func 16439  df-cofu 16441  df-nat 16524  df-fuc 16525  df-setc 16647  df-xpc 16733  df-1stf 16734  df-2ndf 16735  df-prf 16736  df-evlf 16774  df-curf 16775  df-hof 16811  df-yon 16812
This theorem is referenced by:  yonffthlem  16843  yoneda  16844
  Copyright terms: Public domain W3C validator