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

Theorem yonedainv 16744
 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 2610 . . . 4 (𝑄 ×c 𝑂) = (𝑄 ×c 𝑂)
3 yoneda.q . . . . 5 𝑄 = (𝑂 FuncCat 𝑆)
43fucbas 16443 . . . 4 (𝑂 Func 𝑆) = (Base‘𝑄)
5 yoneda.o . . . . 5 𝑂 = (oppCat‘𝐶)
6 yoneda.b . . . . 5 𝐵 = (Base‘𝐶)
75, 6oppcbas 16201 . . . 4 𝐵 = (Base‘𝑂)
82, 4, 7xpcbas 16641 . . 3 ((𝑂 Func 𝑆) × 𝐵) = (Base‘(𝑄 ×c 𝑂))
9 eqid 2610 . . 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 16735 . . . 4 (𝜑 → (𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)))
2221simpld 474 . . 3 (𝜑𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇))
2321simprd 478 . . 3 (𝜑𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇))
24 yonedainv.i . . 3 𝐼 = (Inv‘𝑅)
25 eqid 2610 . . 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 16743 . . 3 (𝜑𝑀 ∈ (𝑍((𝑄 ×c 𝑂) Nat 𝑇)𝐸))
2817adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → 𝐶 ∈ Cat)
2918adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → 𝑉𝑊)
3019adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ran (Homf𝐶) ⊆ 𝑈)
3120adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
32 simprl 790 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ∈ (𝑂 Func 𝑆))
33 simprr 792 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → 𝑤𝐵)
3410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33, 26yonedalem3a 16737 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))) ∧ (𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤)))
3534simprd 478 . . . . . . . . 9 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤))
3628adantr 480 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → 𝐶 ∈ Cat)
3729adantr 480 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → 𝑉𝑊)
3830adantr 480 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → ran (Homf𝐶) ⊆ 𝑈)
3931adantr 480 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
40 simplrl 796 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → ∈ (𝑂 Func 𝑆))
41 simplrr 797 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → 𝑤𝐵)
42 yonedainv.n . . . . . . . . . . . 12 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥𝐵 ↦ (𝑢 ∈ ((1st𝑓)‘𝑥) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢)))))
43 simpr 476 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → 𝑏 ∈ ((1st)‘𝑤))
4410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 36, 37, 38, 39, 40, 41, 42, 43yonedalem4c 16740 . . . . . . . . . . 11 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → ((𝑁𝑤)‘𝑏) ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
45 eqid 2610 . . . . . . . . . . 11 (𝑏 ∈ ((1st)‘𝑤) ↦ ((𝑁𝑤)‘𝑏)) = (𝑏 ∈ ((1st)‘𝑤) ↦ ((𝑁𝑤)‘𝑏))
4644, 45fmptd 6292 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑏 ∈ ((1st)‘𝑤) ↦ ((𝑁𝑤)‘𝑏)):((1st)‘𝑤)⟶(((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
47 fvex 6113 . . . . . . . . . . . . . . . 16 (Base‘𝐶) ∈ V
486, 47eqeltri 2684 . . . . . . . . . . . . . . 15 𝐵 ∈ V
4948mptex 6390 . . . . . . . . . . . . . 14 (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢))) ∈ V
50 eqid 2610 . . . . . . . . . . . . . 14 (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))) = (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢))))
5149, 50fnmpti 5935 . . . . . . . . . . . . 13 (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))) Fn ((1st)‘𝑤)
52 simpl 472 . . . . . . . . . . . . . . . . . . 19 ((𝑓 = 𝑥 = 𝑤) → 𝑓 = )
5352fveq2d 6107 . . . . . . . . . . . . . . . . . 18 ((𝑓 = 𝑥 = 𝑤) → (1st𝑓) = (1st))
54 simpr 476 . . . . . . . . . . . . . . . . . 18 ((𝑓 = 𝑥 = 𝑤) → 𝑥 = 𝑤)
5553, 54fveq12d 6109 . . . . . . . . . . . . . . . . 17 ((𝑓 = 𝑥 = 𝑤) → ((1st𝑓)‘𝑥) = ((1st)‘𝑤))
56 simplr 788 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → 𝑥 = 𝑤)
5756oveq2d 6565 . . . . . . . . . . . . . . . . . . 19 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → (𝑦(Hom ‘𝐶)𝑥) = (𝑦(Hom ‘𝐶)𝑤))
58 simpll 786 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → 𝑓 = )
5958fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → (2nd𝑓) = (2nd))
60 eqidd 2611 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → 𝑦 = 𝑦)
6159, 56, 60oveq123d 6570 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → (𝑥(2nd𝑓)𝑦) = (𝑤(2nd)𝑦))
6261fveq1d 6105 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → ((𝑥(2nd𝑓)𝑦)‘𝑔) = ((𝑤(2nd)𝑦)‘𝑔))
6362fveq1d 6105 . . . . . . . . . . . . . . . . . . 19 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢) = (((𝑤(2nd)𝑦)‘𝑔)‘𝑢))
6457, 63mpteq12dv 4663 . . . . . . . . . . . . . . . . . 18 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢)) = (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))
6564mpteq2dva 4672 . . . . . . . . . . . . . . . . 17 ((𝑓 = 𝑥 = 𝑤) → (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢))) = (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢))))
6655, 65mpteq12dv 4663 . . . . . . . . . . . . . . . 16 ((𝑓 = 𝑥 = 𝑤) → (𝑢 ∈ ((1st𝑓)‘𝑥) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢)))) = (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))))
67 fvex 6113 . . . . . . . . . . . . . . . . 17 ((1st)‘𝑤) ∈ V
6867mptex 6390 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))) ∈ V
6966, 42, 68ovmpt2a 6689 . . . . . . . . . . . . . . 15 (( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵) → (𝑁𝑤) = (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))))
7069adantl 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑁𝑤) = (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))))
7170fneq1d 5895 . . . . . . . . . . . . 13 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑁𝑤) Fn ((1st)‘𝑤) ↔ (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))) Fn ((1st)‘𝑤)))
7251, 71mpbiri 247 . . . . . . . . . . . 12 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑁𝑤) Fn ((1st)‘𝑤))
73 dffn5 6151 . . . . . . . . . . . 12 ((𝑁𝑤) Fn ((1st)‘𝑤) ↔ (𝑁𝑤) = (𝑏 ∈ ((1st)‘𝑤) ↦ ((𝑁𝑤)‘𝑏)))
7472, 73sylib 207 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑁𝑤) = (𝑏 ∈ ((1st)‘𝑤) ↦ ((𝑁𝑤)‘𝑏)))
755oppccat 16205 . . . . . . . . . . . . . 14 (𝐶 ∈ Cat → 𝑂 ∈ Cat)
7617, 75syl 17 . . . . . . . . . . . . 13 (𝜑𝑂 ∈ Cat)
7776adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → 𝑂 ∈ Cat)
7820unssbd 3753 . . . . . . . . . . . . . . 15 (𝜑𝑈𝑉)
7918, 78ssexd 4733 . . . . . . . . . . . . . 14 (𝜑𝑈 ∈ V)
8012setccat 16558 . . . . . . . . . . . . . 14 (𝑈 ∈ V → 𝑆 ∈ Cat)
8179, 80syl 17 . . . . . . . . . . . . 13 (𝜑𝑆 ∈ Cat)
8281adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → 𝑆 ∈ Cat)
8315, 77, 82, 7, 32, 33evlf1 16683 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((1st𝐸)𝑤) = ((1st)‘𝑤))
8410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33yonedalem21 16736 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((1st𝑍)𝑤) = (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
8574, 83, 84feq123d 5947 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑁𝑤):((1st𝐸)𝑤)⟶((1st𝑍)𝑤) ↔ (𝑏 ∈ ((1st)‘𝑤) ↦ ((𝑁𝑤)‘𝑏)):((1st)‘𝑤)⟶(((1st𝑌)‘𝑤)(𝑂 Nat 𝑆))))
8646, 85mpbird 246 . . . . . . . . 9 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑁𝑤):((1st𝐸)𝑤)⟶((1st𝑍)𝑤))
87 fcompt 6306 . . . . . . . . . . 11 (((𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤) ∧ (𝑁𝑤):((1st𝐸)𝑤)⟶((1st𝑍)𝑤)) → ((𝑀𝑤) ∘ (𝑁𝑤)) = (𝑘 ∈ ((1st𝐸)𝑤) ↦ ((𝑀𝑤)‘((𝑁𝑤)‘𝑘))))
8835, 86, 87syl2anc 691 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤) ∘ (𝑁𝑤)) = (𝑘 ∈ ((1st𝐸)𝑤) ↦ ((𝑀𝑤)‘((𝑁𝑤)‘𝑘))))
8983eleq2d 2673 . . . . . . . . . . . . . 14 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑘 ∈ ((1st𝐸)𝑤) ↔ 𝑘 ∈ ((1st)‘𝑤)))
9089biimpa 500 . . . . . . . . . . . . 13 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st𝐸)𝑤)) → 𝑘 ∈ ((1st)‘𝑤))
9128adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝐶 ∈ Cat)
9229adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝑉𝑊)
9330adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ran (Homf𝐶) ⊆ 𝑈)
9431adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
95 simplrl 796 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ∈ (𝑂 Func 𝑆))
96 simplrr 797 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝑤𝐵)
9710, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 91, 92, 93, 94, 95, 96, 26yonedalem3a 16737 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑀𝑤) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))) ∧ (𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤)))
9897simpld 474 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (𝑀𝑤) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))))
9998fveq1d 6105 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑀𝑤)‘((𝑁𝑤)‘𝑘)) = ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘((𝑁𝑤)‘𝑘)))
100 fvex 6113 . . . . . . . . . . . . . . . . . 18 ((𝑁𝑤)‘𝑏) ∈ V
101100a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → ((𝑁𝑤)‘𝑏) ∈ V)
102101, 74, 44fmpt2d 6300 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑁𝑤):((1st)‘𝑤)⟶(((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
103102ffvelrnda 6267 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑁𝑤)‘𝑘) ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
104 fveq1 6102 . . . . . . . . . . . . . . . . 17 (𝑎 = ((𝑁𝑤)‘𝑘) → (𝑎𝑤) = (((𝑁𝑤)‘𝑘)‘𝑤))
105104fveq1d 6105 . . . . . . . . . . . . . . . 16 (𝑎 = ((𝑁𝑤)‘𝑘) → ((𝑎𝑤)‘( 1𝑤)) = ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)))
106 eqid 2610 . . . . . . . . . . . . . . . 16 (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))
107 fvex 6113 . . . . . . . . . . . . . . . 16 ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)) ∈ V
108105, 106, 107fvmpt 6191 . . . . . . . . . . . . . . 15 (((𝑁𝑤)‘𝑘) ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) → ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘((𝑁𝑤)‘𝑘)) = ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)))
109103, 108syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘((𝑁𝑤)‘𝑘)) = ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)))
110 simpr 476 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝑘 ∈ ((1st)‘𝑤))
111 eqid 2610 . . . . . . . . . . . . . . . . 17 (Hom ‘𝐶) = (Hom ‘𝐶)
1126, 111, 11, 91, 96catidcl 16166 . . . . . . . . . . . . . . . 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 16739 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)) = (((𝑤(2nd)𝑤)‘( 1𝑤))‘𝑘))
114 eqid 2610 . . . . . . . . . . . . . . . . . 18 (Id‘𝑂) = (Id‘𝑂)
115 eqid 2610 . . . . . . . . . . . . . . . . . 18 (Id‘𝑆) = (Id‘𝑆)
116 relfunc 16345 . . . . . . . . . . . . . . . . . . 19 Rel (𝑂 Func 𝑆)
117 1st2ndbr 7108 . . . . . . . . . . . . . . . . . . 19 ((Rel (𝑂 Func 𝑆) ∧ ∈ (𝑂 Func 𝑆)) → (1st)(𝑂 Func 𝑆)(2nd))
118116, 95, 117sylancr 694 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (1st)(𝑂 Func 𝑆)(2nd))
1197, 114, 115, 118, 96funcid 16353 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑤(2nd)𝑤)‘((Id‘𝑂)‘𝑤)) = ((Id‘𝑆)‘((1st)‘𝑤)))
1205, 11oppcid 16204 . . . . . . . . . . . . . . . . . . . 20 (𝐶 ∈ Cat → (Id‘𝑂) = 1 )
12191, 120syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (Id‘𝑂) = 1 )
122121fveq1d 6105 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((Id‘𝑂)‘𝑤) = ( 1𝑤))
123122fveq2d 6107 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑤(2nd)𝑤)‘((Id‘𝑂)‘𝑤)) = ((𝑤(2nd)𝑤)‘( 1𝑤)))
12479ad2antrr 758 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝑈 ∈ V)
125 eqid 2610 . . . . . . . . . . . . . . . . . . . . 21 (Base‘𝑆) = (Base‘𝑆)
1267, 125, 118funcf1 16349 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (1st):𝐵⟶(Base‘𝑆))
12712, 124setcbas 16551 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝑈 = (Base‘𝑆))
128127feq3d 5945 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((1st):𝐵𝑈 ↔ (1st):𝐵⟶(Base‘𝑆)))
129126, 128mpbird 246 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (1st):𝐵𝑈)
130129, 96ffvelrnd 6268 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((1st)‘𝑤) ∈ 𝑈)
13112, 115, 124, 130setcid 16559 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((Id‘𝑆)‘((1st)‘𝑤)) = ( I ↾ ((1st)‘𝑤)))
132119, 123, 1313eqtr3d 2652 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑤(2nd)𝑤)‘( 1𝑤)) = ( I ↾ ((1st)‘𝑤)))
133132fveq1d 6105 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (((𝑤(2nd)𝑤)‘( 1𝑤))‘𝑘) = (( I ↾ ((1st)‘𝑤))‘𝑘))
134 fvresi 6344 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ((1st)‘𝑤) → (( I ↾ ((1st)‘𝑤))‘𝑘) = 𝑘)
135134adantl 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (( I ↾ ((1st)‘𝑤))‘𝑘) = 𝑘)
136113, 133, 1353eqtrd 2648 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)) = 𝑘)
13799, 109, 1363eqtrd 2648 . . . . . . . . . . . . 13 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑀𝑤)‘((𝑁𝑤)‘𝑘)) = 𝑘)
13890, 137syldan 486 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st𝐸)𝑤)) → ((𝑀𝑤)‘((𝑁𝑤)‘𝑘)) = 𝑘)
139138mpteq2dva 4672 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑘 ∈ ((1st𝐸)𝑤) ↦ ((𝑀𝑤)‘((𝑁𝑤)‘𝑘))) = (𝑘 ∈ ((1st𝐸)𝑤) ↦ 𝑘))
140 mptresid 5375 . . . . . . . . . . 11 (𝑘 ∈ ((1st𝐸)𝑤) ↦ 𝑘) = ( I ↾ ((1st𝐸)𝑤))
141139, 140syl6eq 2660 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑘 ∈ ((1st𝐸)𝑤) ↦ ((𝑀𝑤)‘((𝑁𝑤)‘𝑘))) = ( I ↾ ((1st𝐸)𝑤)))
14288, 141eqtrd 2644 . . . . . . . . 9 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤) ∘ (𝑁𝑤)) = ( I ↾ ((1st𝐸)𝑤)))
143 fcompt 6306 . . . . . . . . . . 11 (((𝑁𝑤):((1st𝐸)𝑤)⟶((1st𝑍)𝑤) ∧ (𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤)) → ((𝑁𝑤) ∘ (𝑀𝑤)) = (𝑏 ∈ ((1st𝑍)𝑤) ↦ ((𝑁𝑤)‘((𝑀𝑤)‘𝑏))))
14486, 35, 143syl2anc 691 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑁𝑤) ∘ (𝑀𝑤)) = (𝑏 ∈ ((1st𝑍)𝑤) ↦ ((𝑁𝑤)‘((𝑀𝑤)‘𝑏))))
145 eqid 2610 . . . . . . . . . . . . . 14 (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆)
14628adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝐶 ∈ Cat)
14729adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑉𝑊)
14830adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ran (Homf𝐶) ⊆ 𝑈)
14931adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
150 simplrl 796 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ∈ (𝑂 Func 𝑆))
151 simplrr 797 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑤𝐵)
15283feq3d 5945 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤) ↔ (𝑀𝑤):((1st𝑍)𝑤)⟶((1st)‘𝑤)))
15335, 152mpbid 221 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑀𝑤):((1st𝑍)𝑤)⟶((1st)‘𝑤))
154153ffvelrnda 6267 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑀𝑤)‘𝑏) ∈ ((1st)‘𝑤))
15510, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 146, 147, 148, 149, 150, 151, 42, 154yonedalem4c 16740 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑁𝑤)‘((𝑀𝑤)‘𝑏)) ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
156145, 155nat1st2nd 16434 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑁𝑤)‘((𝑀𝑤)‘𝑏)) ∈ (⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st), (2nd)⟩))
157145, 156, 7natfn 16437 . . . . . . . . . . . . 13 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑁𝑤)‘((𝑀𝑤)‘𝑏)) Fn 𝐵)
15884eleq2d 2673 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑏 ∈ ((1st𝑍)𝑤) ↔ 𝑏 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆))))
159158biimpa 500 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑏 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
160145, 159nat1st2nd 16434 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑏 ∈ (⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st), (2nd)⟩))
161145, 160, 7natfn 16437 . . . . . . . . . . . . 13 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑏 Fn 𝐵)
162146adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → 𝐶 ∈ Cat)
163151adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → 𝑤𝐵)
164 simpr 476 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → 𝑧𝐵)
16510, 6, 162, 163, 111, 164yon11 16727 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((1st ‘((1st𝑌)‘𝑤))‘𝑧) = (𝑧(Hom ‘𝐶)𝑤))
166165eleq2d 2673 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ↔ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))
167166biimpa 500 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧)) → 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤))
168162adantr 480 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝐶 ∈ Cat)
169147ad2antrr 758 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑉𝑊)
170148ad2antrr 758 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ran (Homf𝐶) ⊆ 𝑈)
171149ad2antrr 758 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
172150ad2antrr 758 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ∈ (𝑂 Func 𝑆))
173163adantr 480 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑤𝐵)
174154ad2antrr 758 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑀𝑤)‘𝑏) ∈ ((1st)‘𝑤))
175 simplr 788 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑧𝐵)
176 simpr 476 . . . . . . . . . . . . . . . . . 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 16739 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑀𝑤)‘𝑏)))
17810, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 168, 169, 170, 171, 172, 173, 26yonedalem3a 16737 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑀𝑤) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))) ∧ (𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤)))
179178simpld 474 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑀𝑤) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))))
180179fveq1d 6105 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑀𝑤)‘𝑏) = ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘𝑏))
181159ad2antrr 758 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑏 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
182 fveq1 6102 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑏 → (𝑎𝑤) = (𝑏𝑤))
183182fveq1d 6105 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑏 → ((𝑎𝑤)‘( 1𝑤)) = ((𝑏𝑤)‘( 1𝑤)))
184 fvex 6113 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏𝑤)‘( 1𝑤)) ∈ V
185183, 106, 184fvmpt 6191 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) → ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘𝑏) = ((𝑏𝑤)‘( 1𝑤)))
186181, 185syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘𝑏) = ((𝑏𝑤)‘( 1𝑤)))
187180, 186eqtrd 2644 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑀𝑤)‘𝑏) = ((𝑏𝑤)‘( 1𝑤)))
188187fveq2d 6107 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd)𝑧)‘𝑘)‘((𝑀𝑤)‘𝑏)) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))))
189160ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑏 ∈ (⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st), (2nd)⟩))
190 eqid 2610 . . . . . . . . . . . . . . . . . . . . . 22 (Hom ‘𝑂) = (Hom ‘𝑂)
191 eqid 2610 . . . . . . . . . . . . . . . . . . . . . 22 (comp‘𝑆) = (comp‘𝑆)
192111, 5oppchom 16198 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤(Hom ‘𝑂)𝑧) = (𝑧(Hom ‘𝐶)𝑤)
193176, 192syl6eleqr 2699 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑘 ∈ (𝑤(Hom ‘𝑂)𝑧))
194145, 189, 7, 190, 191, 173, 175, 193nati 16438 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏𝑧)(⟨((1st ‘((1st𝑌)‘𝑤))‘𝑤), ((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟩(comp‘𝑆)((1st)‘𝑧))((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)) = (((𝑤(2nd)𝑧)‘𝑘)(⟨((1st ‘((1st𝑌)‘𝑤))‘𝑤), ((1st)‘𝑤)⟩(comp‘𝑆)((1st)‘𝑧))(𝑏𝑤)))
19579ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑈 ∈ V)
196195adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → 𝑈 ∈ V)
197196adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑈 ∈ V)
198 relfunc 16345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Rel (𝐶 Func 𝑄)
19910, 17, 5, 12, 3, 79, 19yoncl 16725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑𝑌 ∈ (𝐶 Func 𝑄))
200 1st2ndbr 7108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((Rel (𝐶 Func 𝑄) ∧ 𝑌 ∈ (𝐶 Func 𝑄)) → (1st𝑌)(𝐶 Func 𝑄)(2nd𝑌))
201198, 199, 200sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (1st𝑌)(𝐶 Func 𝑄)(2nd𝑌))
2026, 4, 201funcf1 16349 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (1st𝑌):𝐵⟶(𝑂 Func 𝑆))
203202ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st𝑌):𝐵⟶(𝑂 Func 𝑆))
204203, 151ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st𝑌)‘𝑤) ∈ (𝑂 Func 𝑆))
205 1st2ndbr 7108 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 16349 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st ‘((1st𝑌)‘𝑤)):𝐵⟶(Base‘𝑆))
20812, 195setcbas 16551 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑈 = (Base‘𝑆))
209208feq3d 5945 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st ‘((1st𝑌)‘𝑤)):𝐵𝑈 ↔ (1st ‘((1st𝑌)‘𝑤)):𝐵⟶(Base‘𝑆)))
210207, 209mpbird 246 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st ‘((1st𝑌)‘𝑤)):𝐵𝑈)
211210, 151ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st ‘((1st𝑌)‘𝑤))‘𝑤) ∈ 𝑈)
212211ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘((1st𝑌)‘𝑤))‘𝑤) ∈ 𝑈)
213210ffvelrnda 6267 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ∈ 𝑈)
214213adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ∈ 𝑈)
215116, 150, 117sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st)(𝑂 Func 𝑆)(2nd))
2167, 125, 215funcf1 16349 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st):𝐵⟶(Base‘𝑆))
217208feq3d 5945 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st):𝐵𝑈 ↔ (1st):𝐵⟶(Base‘𝑆)))
218216, 217mpbird 246 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st):𝐵𝑈)
219218ffvelrnda 6267 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((1st)‘𝑧) ∈ 𝑈)
220219adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st)‘𝑧) ∈ 𝑈)
221 eqid 2610 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Hom ‘𝑆) = (Hom ‘𝑆)
222206ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1st ‘((1st𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st𝑌)‘𝑤)))
2237, 190, 221, 222, 173, 175funcf2 16351 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧):(𝑤(Hom ‘𝑂)𝑧)⟶(((1st ‘((1st𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑤))‘𝑧)))
224223, 193ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑤))‘𝑧)))
22512, 197, 221, 212, 214elsetchom 16554 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑤))‘𝑧)) ↔ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st ‘((1st𝑌)‘𝑤))‘𝑧)))
226224, 225mpbid 221 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st ‘((1st𝑌)‘𝑤))‘𝑧))
227160adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → 𝑏 ∈ (⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st), (2nd)⟩))
228145, 227, 7, 221, 164natcl 16436 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (𝑏𝑧) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st)‘𝑧)))
22912, 196, 221, 213, 219elsetchom 16554 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((𝑏𝑧) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st)‘𝑧)) ↔ (𝑏𝑧):((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟶((1st)‘𝑧)))
230228, 229mpbid 221 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (𝑏𝑧):((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟶((1st)‘𝑧))
231230adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑏𝑧):((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟶((1st)‘𝑧))
23212, 197, 191, 212, 214, 220, 226, 231setcco 16556 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏𝑧)(⟨((1st ‘((1st𝑌)‘𝑤))‘𝑤), ((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟩(comp‘𝑆)((1st)‘𝑧))((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)) = ((𝑏𝑧) ∘ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)))
233218, 151ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st)‘𝑤) ∈ 𝑈)
234233ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st)‘𝑤) ∈ 𝑈)
235145, 160, 7, 221, 151natcl 16436 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (𝑏𝑤) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st)‘𝑤)))
23612, 195, 221, 211, 233elsetchom 16554 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑏𝑤) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st)‘𝑤)) ↔ (𝑏𝑤):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st)‘𝑤)))
237235, 236mpbid 221 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (𝑏𝑤):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st)‘𝑤))
238237ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑏𝑤):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st)‘𝑤))
239116, 172, 117sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1st)(𝑂 Func 𝑆)(2nd))
2407, 190, 221, 239, 173, 175funcf2 16351 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑤(2nd)𝑧):(𝑤(Hom ‘𝑂)𝑧)⟶(((1st)‘𝑤)(Hom ‘𝑆)((1st)‘𝑧)))
241240, 193ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd)𝑧)‘𝑘) ∈ (((1st)‘𝑤)(Hom ‘𝑆)((1st)‘𝑧)))
24212, 197, 221, 234, 220elsetchom 16554 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd)𝑧)‘𝑘) ∈ (((1st)‘𝑤)(Hom ‘𝑆)((1st)‘𝑧)) ↔ ((𝑤(2nd)𝑧)‘𝑘):((1st)‘𝑤)⟶((1st)‘𝑧)))
243241, 242mpbid 221 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd)𝑧)‘𝑘):((1st)‘𝑤)⟶((1st)‘𝑧))
24412, 197, 191, 212, 234, 220, 238, 243setcco 16556 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd)𝑧)‘𝑘)(⟨((1st ‘((1st𝑌)‘𝑤))‘𝑤), ((1st)‘𝑤)⟩(comp‘𝑆)((1st)‘𝑧))(𝑏𝑤)) = (((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤)))
245194, 232, 2443eqtr3d 2652 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏𝑧) ∘ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)) = (((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤)))
246245fveq1d 6105 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑏𝑧) ∘ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘))‘( 1𝑤)) = ((((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤))‘( 1𝑤)))
2476, 111, 11, 146, 151catidcl 16166 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ( 1𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤))
24810, 6, 146, 151, 111, 151yon11 16727 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st ‘((1st𝑌)‘𝑤))‘𝑤) = (𝑤(Hom ‘𝐶)𝑤))
249247, 248eleqtrrd 2691 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ( 1𝑤) ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑤))
250249ad2antrr 758 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ( 1𝑤) ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑤))
251 fvco3 6185 . . . . . . . . . . . . . . . . . . . 20 ((((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st ‘((1st𝑌)‘𝑤))‘𝑧) ∧ ( 1𝑤) ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑤)) → (((𝑏𝑧) ∘ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘))‘( 1𝑤)) = ((𝑏𝑧)‘(((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤))))
252226, 250, 251syl2anc 691 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑏𝑧) ∘ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘))‘( 1𝑤)) = ((𝑏𝑧)‘(((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤))))
253 fvco3 6185 . . . . . . . . . . . . . . . . . . . . 21 (((𝑏𝑤):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st)‘𝑤) ∧ ( 1𝑤) ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑤)) → ((((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤))‘( 1𝑤)) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))))
254237, 249, 253syl2anc 691 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤))‘( 1𝑤)) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))))
255254ad2antrr 758 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤))‘( 1𝑤)) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))))
256246, 252, 2553eqtr3d 2652 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏𝑧)‘(((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤))) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))))
257 eqid 2610 . . . . . . . . . . . . . . . . . . . . 21 (comp‘𝐶) = (comp‘𝐶)
258247ad2antrr 758 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ( 1𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤))
25910, 6, 168, 173, 111, 173, 257, 175, 176, 258yon12 16728 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤)) = (( 1𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐶)𝑤)𝑘))
2606, 111, 11, 168, 175, 257, 173, 176catlid 16167 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (( 1𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐶)𝑤)𝑘) = 𝑘)
261259, 260eqtrd 2644 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤)) = 𝑘)
262261fveq2d 6107 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏𝑧)‘(((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤))) = ((𝑏𝑧)‘𝑘))
263256, 262eqtr3d 2646 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))) = ((𝑏𝑧)‘𝑘))
264177, 188, 2633eqtrd 2648 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = ((𝑏𝑧)‘𝑘))
265167, 264syldan 486 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧)) → ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = ((𝑏𝑧)‘𝑘))
266265mpteq2dva 4672 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ↦ ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧)‘𝑘)) = (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ↦ ((𝑏𝑧)‘𝑘)))
267156adantr 480 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((𝑁𝑤)‘((𝑀𝑤)‘𝑏)) ∈ (⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st), (2nd)⟩))
268145, 267, 7, 221, 164natcl 16436 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st)‘𝑧)))
26912, 196, 221, 213, 219elsetchom 16554 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st)‘𝑧)) ↔ (((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧):((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟶((1st)‘𝑧)))
270268, 269mpbid 221 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧):((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟶((1st)‘𝑧))
271270feqmptd 6159 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧) = (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ↦ ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧)‘𝑘)))
272230feqmptd 6159 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (𝑏𝑧) = (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ↦ ((𝑏𝑧)‘𝑘)))
273266, 271, 2723eqtr4d 2654 . . . . . . . . . . . . 13 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧) = (𝑏𝑧))
274157, 161, 273eqfnfvd 6222 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑁𝑤)‘((𝑀𝑤)‘𝑏)) = 𝑏)
275274mpteq2dva 4672 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑏 ∈ ((1st𝑍)𝑤) ↦ ((𝑁𝑤)‘((𝑀𝑤)‘𝑏))) = (𝑏 ∈ ((1st𝑍)𝑤) ↦ 𝑏))
276 mptresid 5375 . . . . . . . . . . 11 (𝑏 ∈ ((1st𝑍)𝑤) ↦ 𝑏) = ( I ↾ ((1st𝑍)𝑤))
277275, 276syl6eq 2660 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑏 ∈ ((1st𝑍)𝑤) ↦ ((𝑁𝑤)‘((𝑀𝑤)‘𝑏))) = ( I ↾ ((1st𝑍)𝑤)))
278144, 277eqtrd 2644 . . . . . . . . 9 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑁𝑤) ∘ (𝑀𝑤)) = ( I ↾ ((1st𝑍)𝑤)))
279 fcof1o 6451 . . . . . . . . 9 ((((𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤) ∧ (𝑁𝑤):((1st𝐸)𝑤)⟶((1st𝑍)𝑤)) ∧ (((𝑀𝑤) ∘ (𝑁𝑤)) = ( I ↾ ((1st𝐸)𝑤)) ∧ ((𝑁𝑤) ∘ (𝑀𝑤)) = ( I ↾ ((1st𝑍)𝑤)))) → ((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑀𝑤) = (𝑁𝑤)))
28035, 86, 142, 278, 279syl22anc 1319 . . . . . . . 8 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑀𝑤) = (𝑁𝑤)))
281 eqcom 2617 . . . . . . . . 9 ((𝑀𝑤) = (𝑁𝑤) ↔ (𝑁𝑤) = (𝑀𝑤))
282281anbi2i 726 . . . . . . . 8 (((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑀𝑤) = (𝑁𝑤)) ↔ ((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑁𝑤) = (𝑀𝑤)))
283280, 282sylib 207 . . . . . . 7 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑁𝑤) = (𝑀𝑤)))
284 eqid 2610 . . . . . . . . . . 11 (Base‘𝑇) = (Base‘𝑇)
285 relfunc 16345 . . . . . . . . . . . 12 Rel ((𝑄 ×c 𝑂) Func 𝑇)
286 1st2ndbr 7108 . . . . . . . . . . . 12 ((Rel ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st𝑍)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝑍))
287285, 22, 286sylancr 694 . . . . . . . . . . 11 (𝜑 → (1st𝑍)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝑍))
2888, 284, 287funcf1 16349 . . . . . . . . . 10 (𝜑 → (1st𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
28913, 18setcbas 16551 . . . . . . . . . . 11 (𝜑𝑉 = (Base‘𝑇))
290289feq3d 5945 . . . . . . . . . 10 (𝜑 → ((1st𝑍):((𝑂 Func 𝑆) × 𝐵)⟶𝑉 ↔ (1st𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇)))
291288, 290mpbird 246 . . . . . . . . 9 (𝜑 → (1st𝑍):((𝑂 Func 𝑆) × 𝐵)⟶𝑉)
292291fovrnda 6703 . . . . . . . 8 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((1st𝑍)𝑤) ∈ 𝑉)
293 1st2ndbr 7108 . . . . . . . . . . . 12 ((Rel ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st𝐸)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝐸))
294285, 23, 293sylancr 694 . . . . . . . . . . 11 (𝜑 → (1st𝐸)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝐸))
2958, 284, 294funcf1 16349 . . . . . . . . . 10 (𝜑 → (1st𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
296289feq3d 5945 . . . . . . . . . 10 (𝜑 → ((1st𝐸):((𝑂 Func 𝑆) × 𝐵)⟶𝑉 ↔ (1st𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇)))
297295, 296mpbird 246 . . . . . . . . 9 (𝜑 → (1st𝐸):((𝑂 Func 𝑆) × 𝐵)⟶𝑉)
298297fovrnda 6703 . . . . . . . 8 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((1st𝐸)𝑤) ∈ 𝑉)
29913, 29, 292, 298, 25setcinv 16563 . . . . . . 7 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤)(((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤))(𝑁𝑤) ↔ ((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑁𝑤) = (𝑀𝑤))))
300283, 299mpbird 246 . . . . . 6 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑀𝑤)(((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤))(𝑁𝑤))
301300ralrimivva 2954 . . . . 5 (𝜑 → ∀ ∈ (𝑂 Func 𝑆)∀𝑤𝐵 (𝑀𝑤)(((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤))(𝑁𝑤))
302 fveq2 6103 . . . . . . . 8 (𝑧 = ⟨, 𝑤⟩ → (𝑀𝑧) = (𝑀‘⟨, 𝑤⟩))
303 df-ov 6552 . . . . . . . 8 (𝑀𝑤) = (𝑀‘⟨, 𝑤⟩)
304302, 303syl6eqr 2662 . . . . . . 7 (𝑧 = ⟨, 𝑤⟩ → (𝑀𝑧) = (𝑀𝑤))
305 fveq2 6103 . . . . . . . . 9 (𝑧 = ⟨, 𝑤⟩ → ((1st𝑍)‘𝑧) = ((1st𝑍)‘⟨, 𝑤⟩))
306 df-ov 6552 . . . . . . . . 9 ((1st𝑍)𝑤) = ((1st𝑍)‘⟨, 𝑤⟩)
307305, 306syl6eqr 2662 . . . . . . . 8 (𝑧 = ⟨, 𝑤⟩ → ((1st𝑍)‘𝑧) = ((1st𝑍)𝑤))
308 fveq2 6103 . . . . . . . . 9 (𝑧 = ⟨, 𝑤⟩ → ((1st𝐸)‘𝑧) = ((1st𝐸)‘⟨, 𝑤⟩))
309 df-ov 6552 . . . . . . . . 9 ((1st𝐸)𝑤) = ((1st𝐸)‘⟨, 𝑤⟩)
310308, 309syl6eqr 2662 . . . . . . . 8 (𝑧 = ⟨, 𝑤⟩ → ((1st𝐸)‘𝑧) = ((1st𝐸)𝑤))
311307, 310oveq12d 6567 . . . . . . 7 (𝑧 = ⟨, 𝑤⟩ → (((1st𝑍)‘𝑧)(Inv‘𝑇)((1st𝐸)‘𝑧)) = (((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤)))
312 fveq2 6103 . . . . . . . 8 (𝑧 = ⟨, 𝑤⟩ → (𝑁𝑧) = (𝑁‘⟨, 𝑤⟩))
313 df-ov 6552 . . . . . . . 8 (𝑁𝑤) = (𝑁‘⟨, 𝑤⟩)
314312, 313syl6eqr 2662 . . . . . . 7 (𝑧 = ⟨, 𝑤⟩ → (𝑁𝑧) = (𝑁𝑤))
315304, 311, 314breq123d 4597 . . . . . 6 (𝑧 = ⟨, 𝑤⟩ → ((𝑀𝑧)(((1st𝑍)‘𝑧)(Inv‘𝑇)((1st𝐸)‘𝑧))(𝑁𝑧) ↔ (𝑀𝑤)(((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤))(𝑁𝑤)))
316315ralxp 5185 . . . . 5 (∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑀𝑧)(((1st𝑍)‘𝑧)(Inv‘𝑇)((1st𝐸)‘𝑧))(𝑁𝑧) ↔ ∀ ∈ (𝑂 Func 𝑆)∀𝑤𝐵 (𝑀𝑤)(((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤))(𝑁𝑤))
317301, 316sylibr 223 . . . 4 (𝜑 → ∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑀𝑧)(((1st𝑍)‘𝑧)(Inv‘𝑇)((1st𝐸)‘𝑧))(𝑁𝑧))
318317r19.21bi 2916 . . 3 ((𝜑𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)) → (𝑀𝑧)(((1st𝑍)‘𝑧)(Inv‘𝑇)((1st𝐸)‘𝑧))(𝑁𝑧))
3191, 8, 9, 22, 23, 24, 25, 27, 318invfuc 16457 . 2 (𝜑𝑀(𝑍𝐼𝐸)(𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁𝑧)))
320 fvex 6113 . . . . 5 ((1st𝑓)‘𝑥) ∈ V
321320mptex 6390 . . . 4 (𝑢 ∈ ((1st𝑓)‘𝑥) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢)))) ∈ V
32242, 321fnmpt2i 7128 . . 3 𝑁 Fn ((𝑂 Func 𝑆) × 𝐵)
323 dffn5 6151 . . 3 (𝑁 Fn ((𝑂 Func 𝑆) × 𝐵) ↔ 𝑁 = (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁𝑧)))
324322, 323mpbi 219 . 2 𝑁 = (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁𝑧))
325319, 324syl6breqr 4625 1 (𝜑𝑀(𝑍𝐼𝐸)𝑁)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  Vcvv 3173   ∪ cun 3538   ⊆ wss 3540  ⟨cop 4131   class class class wbr 4583   ↦ cmpt 4643   I cid 4948   × cxp 5036  ◡ccnv 5037  ran crn 5039   ↾ cres 5040   ∘ ccom 5042  Rel wrel 5043   Fn wfn 5799  ⟶wf 5800  –1-1-onto→wf1o 5803  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  1st c1st 7057  2nd c2nd 7058  tpos ctpos 7238  Basecbs 15695  Hom chom 15779  compcco 15780  Catccat 16148  Idccid 16149  Homf chomf 16150  oppCatcoppc 16194  Invcinv 16228   Func cfunc 16337   ∘func ccofu 16339   Nat cnat 16424   FuncCat cfuc 16425  SetCatcsetc 16548   ×c cxpc 16631   1stF c1stf 16632   2ndF c2ndf 16633   ⟨,⟩F cprf 16634   evalF cevlf 16672  HomFchof 16711  Yoncyon 16712 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-tpos 7239  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-fz 12198  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-hom 15793  df-cco 15794  df-cat 16152  df-cid 16153  df-homf 16154  df-comf 16155  df-oppc 16195  df-sect 16230  df-inv 16231  df-ssc 16293  df-resc 16294  df-subc 16295  df-func 16341  df-cofu 16343  df-nat 16426  df-fuc 16427  df-setc 16549  df-xpc 16635  df-1stf 16636  df-2ndf 16637  df-prf 16638  df-evlf 16676  df-curf 16677  df-hof 16713  df-yon 16714 This theorem is referenced by:  yonffthlem  16745  yoneda  16746
 Copyright terms: Public domain W3C validator