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

Theorem yonedainv 18088
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 2736 . . . 4 (𝑄 ×c 𝑂) = (𝑄 ×c 𝑂)
3 yoneda.q . . . . 5 𝑄 = (𝑂 FuncCat 𝑆)
43fucbas 17766 . . . 4 (𝑂 Func 𝑆) = (Base‘𝑄)
5 yoneda.o . . . . 5 𝑂 = (oppCat‘𝐶)
6 yoneda.b . . . . 5 𝐵 = (Base‘𝐶)
75, 6oppcbas 17517 . . . 4 𝐵 = (Base‘𝑂)
82, 4, 7xpcbas 17984 . . 3 ((𝑂 Func 𝑆) × 𝐵) = (Base‘(𝑄 ×c 𝑂))
9 eqid 2736 . . 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 18079 . . . 4 (𝜑 → (𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)))
2221simpld 495 . . 3 (𝜑𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇))
2321simprd 496 . . 3 (𝜑𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇))
24 yonedainv.i . . 3 𝐼 = (Inv‘𝑅)
25 eqid 2736 . . 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 18087 . . 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 768 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ∈ (𝑂 Func 𝑆))
33 simprr 770 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → 𝑤𝐵)
3410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33, 26yonedalem3a 18081 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))) ∧ (𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤)))
3534simprd 496 . . . . . . . . 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 774 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → ∈ (𝑂 Func 𝑆))
41 simplrr 775 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → 𝑤𝐵)
42 yonedainv.n . . . . . . . . . . . 12 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥𝐵 ↦ (𝑢 ∈ ((1st𝑓)‘𝑥) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢)))))
43 simpr 485 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → 𝑏 ∈ ((1st)‘𝑤))
4410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 36, 37, 38, 39, 40, 41, 42, 43yonedalem4c 18084 . . . . . . . . . . 11 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → ((𝑁𝑤)‘𝑏) ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
4544fmpttd 7039 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑏 ∈ ((1st)‘𝑤) ↦ ((𝑁𝑤)‘𝑏)):((1st)‘𝑤)⟶(((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
466fvexi 6833 . . . . . . . . . . . . . . 15 𝐵 ∈ V
4746mptex 7149 . . . . . . . . . . . . . 14 (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢))) ∈ V
48 eqid 2736 . . . . . . . . . . . . . 14 (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))) = (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢))))
4947, 48fnmpti 6621 . . . . . . . . . . . . 13 (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))) Fn ((1st)‘𝑤)
50 simpl 483 . . . . . . . . . . . . . . . . . . 19 ((𝑓 = 𝑥 = 𝑤) → 𝑓 = )
5150fveq2d 6823 . . . . . . . . . . . . . . . . . 18 ((𝑓 = 𝑥 = 𝑤) → (1st𝑓) = (1st))
52 simpr 485 . . . . . . . . . . . . . . . . . 18 ((𝑓 = 𝑥 = 𝑤) → 𝑥 = 𝑤)
5351, 52fveq12d 6826 . . . . . . . . . . . . . . . . 17 ((𝑓 = 𝑥 = 𝑤) → ((1st𝑓)‘𝑥) = ((1st)‘𝑤))
54 simplr 766 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → 𝑥 = 𝑤)
5554oveq2d 7345 . . . . . . . . . . . . . . . . . . 19 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → (𝑦(Hom ‘𝐶)𝑥) = (𝑦(Hom ‘𝐶)𝑤))
56 simpll 764 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → 𝑓 = )
5756fveq2d 6823 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → (2nd𝑓) = (2nd))
58 eqidd 2737 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → 𝑦 = 𝑦)
5957, 54, 58oveq123d 7350 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → (𝑥(2nd𝑓)𝑦) = (𝑤(2nd)𝑦))
6059fveq1d 6821 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → ((𝑥(2nd𝑓)𝑦)‘𝑔) = ((𝑤(2nd)𝑦)‘𝑔))
6160fveq1d 6821 . . . . . . . . . . . . . . . . . . 19 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢) = (((𝑤(2nd)𝑦)‘𝑔)‘𝑢))
6255, 61mpteq12dv 5180 . . . . . . . . . . . . . . . . . 18 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢)) = (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))
6362mpteq2dva 5189 . . . . . . . . . . . . . . . . 17 ((𝑓 = 𝑥 = 𝑤) → (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢))) = (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢))))
6453, 63mpteq12dv 5180 . . . . . . . . . . . . . . . 16 ((𝑓 = 𝑥 = 𝑤) → (𝑢 ∈ ((1st𝑓)‘𝑥) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢)))) = (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))))
65 fvex 6832 . . . . . . . . . . . . . . . . 17 ((1st)‘𝑤) ∈ V
6665mptex 7149 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))) ∈ V
6764, 42, 66ovmpoa 7482 . . . . . . . . . . . . . . 15 (( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵) → (𝑁𝑤) = (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))))
6867adantl 482 . . . . . . . . . . . . . 14 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑁𝑤) = (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))))
6968fneq1d 6572 . . . . . . . . . . . . 13 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑁𝑤) Fn ((1st)‘𝑤) ↔ (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))) Fn ((1st)‘𝑤)))
7049, 69mpbiri 257 . . . . . . . . . . . 12 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑁𝑤) Fn ((1st)‘𝑤))
71 dffn5 6878 . . . . . . . . . . . 12 ((𝑁𝑤) Fn ((1st)‘𝑤) ↔ (𝑁𝑤) = (𝑏 ∈ ((1st)‘𝑤) ↦ ((𝑁𝑤)‘𝑏)))
7270, 71sylib 217 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑁𝑤) = (𝑏 ∈ ((1st)‘𝑤) ↦ ((𝑁𝑤)‘𝑏)))
735oppccat 17522 . . . . . . . . . . . . . 14 (𝐶 ∈ Cat → 𝑂 ∈ Cat)
7417, 73syl 17 . . . . . . . . . . . . 13 (𝜑𝑂 ∈ Cat)
7574adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → 𝑂 ∈ Cat)
7620unssbd 4134 . . . . . . . . . . . . . . 15 (𝜑𝑈𝑉)
7718, 76ssexd 5265 . . . . . . . . . . . . . 14 (𝜑𝑈 ∈ V)
7812setccat 17889 . . . . . . . . . . . . . 14 (𝑈 ∈ V → 𝑆 ∈ Cat)
7977, 78syl 17 . . . . . . . . . . . . 13 (𝜑𝑆 ∈ Cat)
8079adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → 𝑆 ∈ Cat)
8115, 75, 80, 7, 32, 33evlf1 18027 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((1st𝐸)𝑤) = ((1st)‘𝑤))
8210, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33yonedalem21 18080 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((1st𝑍)𝑤) = (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
8372, 81, 82feq123d 6634 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑁𝑤):((1st𝐸)𝑤)⟶((1st𝑍)𝑤) ↔ (𝑏 ∈ ((1st)‘𝑤) ↦ ((𝑁𝑤)‘𝑏)):((1st)‘𝑤)⟶(((1st𝑌)‘𝑤)(𝑂 Nat 𝑆))))
8445, 83mpbird 256 . . . . . . . . 9 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑁𝑤):((1st𝐸)𝑤)⟶((1st𝑍)𝑤))
85 fcompt 7055 . . . . . . . . . . 11 (((𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤) ∧ (𝑁𝑤):((1st𝐸)𝑤)⟶((1st𝑍)𝑤)) → ((𝑀𝑤) ∘ (𝑁𝑤)) = (𝑘 ∈ ((1st𝐸)𝑤) ↦ ((𝑀𝑤)‘((𝑁𝑤)‘𝑘))))
8635, 84, 85syl2anc 584 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤) ∘ (𝑁𝑤)) = (𝑘 ∈ ((1st𝐸)𝑤) ↦ ((𝑀𝑤)‘((𝑁𝑤)‘𝑘))))
8781eleq2d 2822 . . . . . . . . . . . . . 14 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑘 ∈ ((1st𝐸)𝑤) ↔ 𝑘 ∈ ((1st)‘𝑤)))
8887biimpa 477 . . . . . . . . . . . . 13 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st𝐸)𝑤)) → 𝑘 ∈ ((1st)‘𝑤))
8928adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝐶 ∈ Cat)
9029adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝑉𝑊)
9130adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ran (Homf𝐶) ⊆ 𝑈)
9231adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
93 simplrl 774 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ∈ (𝑂 Func 𝑆))
94 simplrr 775 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝑤𝐵)
9510, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 89, 90, 91, 92, 93, 94, 26yonedalem3a 18081 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑀𝑤) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))) ∧ (𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤)))
9695simpld 495 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (𝑀𝑤) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))))
9796fveq1d 6821 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑀𝑤)‘((𝑁𝑤)‘𝑘)) = ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘((𝑁𝑤)‘𝑘)))
9872, 44fmpt3d 7040 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑁𝑤):((1st)‘𝑤)⟶(((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
9998ffvelcdmda 7011 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑁𝑤)‘𝑘) ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
100 fveq1 6818 . . . . . . . . . . . . . . . . 17 (𝑎 = ((𝑁𝑤)‘𝑘) → (𝑎𝑤) = (((𝑁𝑤)‘𝑘)‘𝑤))
101100fveq1d 6821 . . . . . . . . . . . . . . . 16 (𝑎 = ((𝑁𝑤)‘𝑘) → ((𝑎𝑤)‘( 1𝑤)) = ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)))
102 eqid 2736 . . . . . . . . . . . . . . . 16 (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))
103 fvex 6832 . . . . . . . . . . . . . . . 16 ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)) ∈ V
104101, 102, 103fvmpt 6925 . . . . . . . . . . . . . . 15 (((𝑁𝑤)‘𝑘) ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) → ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘((𝑁𝑤)‘𝑘)) = ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)))
10599, 104syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘((𝑁𝑤)‘𝑘)) = ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)))
106 simpr 485 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝑘 ∈ ((1st)‘𝑤))
107 eqid 2736 . . . . . . . . . . . . . . . . 17 (Hom ‘𝐶) = (Hom ‘𝐶)
1086, 107, 11, 89, 94catidcl 17480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ( 1𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤))
10910, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 89, 90, 91, 92, 93, 94, 42, 106, 94, 108yonedalem4b 18083 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)) = (((𝑤(2nd)𝑤)‘( 1𝑤))‘𝑘))
110 eqid 2736 . . . . . . . . . . . . . . . . . 18 (Id‘𝑂) = (Id‘𝑂)
111 eqid 2736 . . . . . . . . . . . . . . . . . 18 (Id‘𝑆) = (Id‘𝑆)
112 relfunc 17666 . . . . . . . . . . . . . . . . . . 19 Rel (𝑂 Func 𝑆)
113 1st2ndbr 7943 . . . . . . . . . . . . . . . . . . 19 ((Rel (𝑂 Func 𝑆) ∧ ∈ (𝑂 Func 𝑆)) → (1st)(𝑂 Func 𝑆)(2nd))
114112, 93, 113sylancr 587 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (1st)(𝑂 Func 𝑆)(2nd))
1157, 110, 111, 114, 94funcid 17674 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑤(2nd)𝑤)‘((Id‘𝑂)‘𝑤)) = ((Id‘𝑆)‘((1st)‘𝑤)))
1165, 11oppcid 17521 . . . . . . . . . . . . . . . . . . . 20 (𝐶 ∈ Cat → (Id‘𝑂) = 1 )
11789, 116syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (Id‘𝑂) = 1 )
118117fveq1d 6821 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((Id‘𝑂)‘𝑤) = ( 1𝑤))
119118fveq2d 6823 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑤(2nd)𝑤)‘((Id‘𝑂)‘𝑤)) = ((𝑤(2nd)𝑤)‘( 1𝑤)))
12077ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝑈 ∈ V)
121 eqid 2736 . . . . . . . . . . . . . . . . . . . . 21 (Base‘𝑆) = (Base‘𝑆)
1227, 121, 114funcf1 17670 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (1st):𝐵⟶(Base‘𝑆))
12312, 120setcbas 17882 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝑈 = (Base‘𝑆))
124123feq3d 6632 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((1st):𝐵𝑈 ↔ (1st):𝐵⟶(Base‘𝑆)))
125122, 124mpbird 256 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (1st):𝐵𝑈)
126125, 94ffvelcdmd 7012 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((1st)‘𝑤) ∈ 𝑈)
12712, 111, 120, 126setcid 17890 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((Id‘𝑆)‘((1st)‘𝑤)) = ( I ↾ ((1st)‘𝑤)))
128115, 119, 1273eqtr3d 2784 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑤(2nd)𝑤)‘( 1𝑤)) = ( I ↾ ((1st)‘𝑤)))
129128fveq1d 6821 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (((𝑤(2nd)𝑤)‘( 1𝑤))‘𝑘) = (( I ↾ ((1st)‘𝑤))‘𝑘))
130 fvresi 7095 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ((1st)‘𝑤) → (( I ↾ ((1st)‘𝑤))‘𝑘) = 𝑘)
131130adantl 482 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (( I ↾ ((1st)‘𝑤))‘𝑘) = 𝑘)
132109, 129, 1313eqtrd 2780 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)) = 𝑘)
13397, 105, 1323eqtrd 2780 . . . . . . . . . . . . 13 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑀𝑤)‘((𝑁𝑤)‘𝑘)) = 𝑘)
13488, 133syldan 591 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st𝐸)𝑤)) → ((𝑀𝑤)‘((𝑁𝑤)‘𝑘)) = 𝑘)
135134mpteq2dva 5189 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑘 ∈ ((1st𝐸)𝑤) ↦ ((𝑀𝑤)‘((𝑁𝑤)‘𝑘))) = (𝑘 ∈ ((1st𝐸)𝑤) ↦ 𝑘))
136 mptresid 5984 . . . . . . . . . . 11 ( I ↾ ((1st𝐸)𝑤)) = (𝑘 ∈ ((1st𝐸)𝑤) ↦ 𝑘)
137135, 136eqtr4di 2794 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑘 ∈ ((1st𝐸)𝑤) ↦ ((𝑀𝑤)‘((𝑁𝑤)‘𝑘))) = ( I ↾ ((1st𝐸)𝑤)))
13886, 137eqtrd 2776 . . . . . . . . 9 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤) ∘ (𝑁𝑤)) = ( I ↾ ((1st𝐸)𝑤)))
139 fcompt 7055 . . . . . . . . . . 11 (((𝑁𝑤):((1st𝐸)𝑤)⟶((1st𝑍)𝑤) ∧ (𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤)) → ((𝑁𝑤) ∘ (𝑀𝑤)) = (𝑏 ∈ ((1st𝑍)𝑤) ↦ ((𝑁𝑤)‘((𝑀𝑤)‘𝑏))))
14084, 35, 139syl2anc 584 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑁𝑤) ∘ (𝑀𝑤)) = (𝑏 ∈ ((1st𝑍)𝑤) ↦ ((𝑁𝑤)‘((𝑀𝑤)‘𝑏))))
141 eqid 2736 . . . . . . . . . . . . . 14 (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆)
14228adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝐶 ∈ Cat)
14329adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑉𝑊)
14430adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ran (Homf𝐶) ⊆ 𝑈)
14531adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
146 simplrl 774 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ∈ (𝑂 Func 𝑆))
147 simplrr 775 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑤𝐵)
14881feq3d 6632 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤) ↔ (𝑀𝑤):((1st𝑍)𝑤)⟶((1st)‘𝑤)))
14935, 148mpbid 231 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑀𝑤):((1st𝑍)𝑤)⟶((1st)‘𝑤))
150149ffvelcdmda 7011 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑀𝑤)‘𝑏) ∈ ((1st)‘𝑤))
15110, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 142, 143, 144, 145, 146, 147, 42, 150yonedalem4c 18084 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑁𝑤)‘((𝑀𝑤)‘𝑏)) ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
152141, 151nat1st2nd 17756 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑁𝑤)‘((𝑀𝑤)‘𝑏)) ∈ (⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st), (2nd)⟩))
153141, 152, 7natfn 17759 . . . . . . . . . . . . 13 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑁𝑤)‘((𝑀𝑤)‘𝑏)) Fn 𝐵)
15482eleq2d 2822 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑏 ∈ ((1st𝑍)𝑤) ↔ 𝑏 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆))))
155154biimpa 477 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑏 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
156141, 155nat1st2nd 17756 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑏 ∈ (⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st), (2nd)⟩))
157141, 156, 7natfn 17759 . . . . . . . . . . . . 13 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑏 Fn 𝐵)
158142adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → 𝐶 ∈ Cat)
159147adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → 𝑤𝐵)
160 simpr 485 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → 𝑧𝐵)
16110, 6, 158, 159, 107, 160yon11 18071 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((1st ‘((1st𝑌)‘𝑤))‘𝑧) = (𝑧(Hom ‘𝐶)𝑤))
162161eleq2d 2822 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ↔ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))
163162biimpa 477 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧)) → 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤))
164158adantr 481 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝐶 ∈ Cat)
165143ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑉𝑊)
166144ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ran (Homf𝐶) ⊆ 𝑈)
167145ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
168146ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ∈ (𝑂 Func 𝑆))
169159adantr 481 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑤𝐵)
170150ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑀𝑤)‘𝑏) ∈ ((1st)‘𝑤))
171 simplr 766 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑧𝐵)
172 simpr 485 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤))
17310, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 164, 165, 166, 167, 168, 169, 42, 170, 171, 172yonedalem4b 18083 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑀𝑤)‘𝑏)))
17410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 164, 165, 166, 167, 168, 169, 26yonedalem3a 18081 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑀𝑤) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))) ∧ (𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤)))
175174simpld 495 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑀𝑤) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))))
176175fveq1d 6821 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑀𝑤)‘𝑏) = ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘𝑏))
177155ad2antrr 723 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑏 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
178 fveq1 6818 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑏 → (𝑎𝑤) = (𝑏𝑤))
179178fveq1d 6821 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑏 → ((𝑎𝑤)‘( 1𝑤)) = ((𝑏𝑤)‘( 1𝑤)))
180 fvex 6832 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏𝑤)‘( 1𝑤)) ∈ V
181179, 102, 180fvmpt 6925 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) → ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘𝑏) = ((𝑏𝑤)‘( 1𝑤)))
182177, 181syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘𝑏) = ((𝑏𝑤)‘( 1𝑤)))
183176, 182eqtrd 2776 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑀𝑤)‘𝑏) = ((𝑏𝑤)‘( 1𝑤)))
184183fveq2d 6823 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd)𝑧)‘𝑘)‘((𝑀𝑤)‘𝑏)) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))))
185156ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑏 ∈ (⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st), (2nd)⟩))
186 eqid 2736 . . . . . . . . . . . . . . . . . . . . . 22 (Hom ‘𝑂) = (Hom ‘𝑂)
187 eqid 2736 . . . . . . . . . . . . . . . . . . . . . 22 (comp‘𝑆) = (comp‘𝑆)
188107, 5oppchom 17514 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤(Hom ‘𝑂)𝑧) = (𝑧(Hom ‘𝐶)𝑤)
189172, 188eleqtrrdi 2848 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑘 ∈ (𝑤(Hom ‘𝑂)𝑧))
190141, 185, 7, 186, 187, 169, 171, 189nati 17760 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏𝑧)(⟨((1st ‘((1st𝑌)‘𝑤))‘𝑤), ((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟩(comp‘𝑆)((1st)‘𝑧))((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)) = (((𝑤(2nd)𝑧)‘𝑘)(⟨((1st ‘((1st𝑌)‘𝑤))‘𝑤), ((1st)‘𝑤)⟩(comp‘𝑆)((1st)‘𝑧))(𝑏𝑤)))
19177ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑈 ∈ V)
192191adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → 𝑈 ∈ V)
193192adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑈 ∈ V)
194 relfunc 17666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Rel (𝐶 Func 𝑄)
19510, 17, 5, 12, 3, 77, 19yoncl 18069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑𝑌 ∈ (𝐶 Func 𝑄))
196 1st2ndbr 7943 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((Rel (𝐶 Func 𝑄) ∧ 𝑌 ∈ (𝐶 Func 𝑄)) → (1st𝑌)(𝐶 Func 𝑄)(2nd𝑌))
197194, 195, 196sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (1st𝑌)(𝐶 Func 𝑄)(2nd𝑌))
1986, 4, 197funcf1 17670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (1st𝑌):𝐵⟶(𝑂 Func 𝑆))
199198ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st𝑌):𝐵⟶(𝑂 Func 𝑆))
200199, 147ffvelcdmd 7012 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st𝑌)‘𝑤) ∈ (𝑂 Func 𝑆))
201 1st2ndbr 7943 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Rel (𝑂 Func 𝑆) ∧ ((1st𝑌)‘𝑤) ∈ (𝑂 Func 𝑆)) → (1st ‘((1st𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st𝑌)‘𝑤)))
202112, 200, 201sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st ‘((1st𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st𝑌)‘𝑤)))
2037, 121, 202funcf1 17670 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st ‘((1st𝑌)‘𝑤)):𝐵⟶(Base‘𝑆))
20412, 191setcbas 17882 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑈 = (Base‘𝑆))
205204feq3d 6632 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st ‘((1st𝑌)‘𝑤)):𝐵𝑈 ↔ (1st ‘((1st𝑌)‘𝑤)):𝐵⟶(Base‘𝑆)))
206203, 205mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st ‘((1st𝑌)‘𝑤)):𝐵𝑈)
207206, 147ffvelcdmd 7012 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st ‘((1st𝑌)‘𝑤))‘𝑤) ∈ 𝑈)
208207ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘((1st𝑌)‘𝑤))‘𝑤) ∈ 𝑈)
209206ffvelcdmda 7011 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ∈ 𝑈)
210209adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ∈ 𝑈)
211112, 146, 113sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st)(𝑂 Func 𝑆)(2nd))
2127, 121, 211funcf1 17670 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st):𝐵⟶(Base‘𝑆))
213204feq3d 6632 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st):𝐵𝑈 ↔ (1st):𝐵⟶(Base‘𝑆)))
214212, 213mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st):𝐵𝑈)
215214ffvelcdmda 7011 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((1st)‘𝑧) ∈ 𝑈)
216215adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st)‘𝑧) ∈ 𝑈)
217 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Hom ‘𝑆) = (Hom ‘𝑆)
218202ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1st ‘((1st𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st𝑌)‘𝑤)))
2197, 186, 217, 218, 169, 171funcf2 17672 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧):(𝑤(Hom ‘𝑂)𝑧)⟶(((1st ‘((1st𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑤))‘𝑧)))
220219, 189ffvelcdmd 7012 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑤))‘𝑧)))
22112, 193, 217, 208, 210elsetchom 17885 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑤))‘𝑧)) ↔ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st ‘((1st𝑌)‘𝑤))‘𝑧)))
222220, 221mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st ‘((1st𝑌)‘𝑤))‘𝑧))
223156adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → 𝑏 ∈ (⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st), (2nd)⟩))
224141, 223, 7, 217, 160natcl 17758 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (𝑏𝑧) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st)‘𝑧)))
22512, 192, 217, 209, 215elsetchom 17885 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((𝑏𝑧) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st)‘𝑧)) ↔ (𝑏𝑧):((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟶((1st)‘𝑧)))
226224, 225mpbid 231 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (𝑏𝑧):((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟶((1st)‘𝑧))
227226adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑏𝑧):((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟶((1st)‘𝑧))
22812, 193, 187, 208, 210, 216, 222, 227setcco 17887 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏𝑧)(⟨((1st ‘((1st𝑌)‘𝑤))‘𝑤), ((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟩(comp‘𝑆)((1st)‘𝑧))((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)) = ((𝑏𝑧) ∘ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)))
229214, 147ffvelcdmd 7012 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st)‘𝑤) ∈ 𝑈)
230229ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st)‘𝑤) ∈ 𝑈)
231141, 156, 7, 217, 147natcl 17758 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (𝑏𝑤) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st)‘𝑤)))
23212, 191, 217, 207, 229elsetchom 17885 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑏𝑤) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st)‘𝑤)) ↔ (𝑏𝑤):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st)‘𝑤)))
233231, 232mpbid 231 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (𝑏𝑤):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st)‘𝑤))
234233ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑏𝑤):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st)‘𝑤))
235112, 168, 113sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1st)(𝑂 Func 𝑆)(2nd))
2367, 186, 217, 235, 169, 171funcf2 17672 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑤(2nd)𝑧):(𝑤(Hom ‘𝑂)𝑧)⟶(((1st)‘𝑤)(Hom ‘𝑆)((1st)‘𝑧)))
237236, 189ffvelcdmd 7012 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd)𝑧)‘𝑘) ∈ (((1st)‘𝑤)(Hom ‘𝑆)((1st)‘𝑧)))
23812, 193, 217, 230, 216elsetchom 17885 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd)𝑧)‘𝑘) ∈ (((1st)‘𝑤)(Hom ‘𝑆)((1st)‘𝑧)) ↔ ((𝑤(2nd)𝑧)‘𝑘):((1st)‘𝑤)⟶((1st)‘𝑧)))
239237, 238mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd)𝑧)‘𝑘):((1st)‘𝑤)⟶((1st)‘𝑧))
24012, 193, 187, 208, 230, 216, 234, 239setcco 17887 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd)𝑧)‘𝑘)(⟨((1st ‘((1st𝑌)‘𝑤))‘𝑤), ((1st)‘𝑤)⟩(comp‘𝑆)((1st)‘𝑧))(𝑏𝑤)) = (((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤)))
241190, 228, 2403eqtr3d 2784 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏𝑧) ∘ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)) = (((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤)))
242241fveq1d 6821 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑏𝑧) ∘ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘))‘( 1𝑤)) = ((((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤))‘( 1𝑤)))
2436, 107, 11, 142, 147catidcl 17480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ( 1𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤))
24410, 6, 142, 147, 107, 147yon11 18071 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st ‘((1st𝑌)‘𝑤))‘𝑤) = (𝑤(Hom ‘𝐶)𝑤))
245243, 244eleqtrrd 2840 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ( 1𝑤) ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑤))
246245ad2antrr 723 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ( 1𝑤) ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑤))
247222, 246fvco3d 6918 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑏𝑧) ∘ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘))‘( 1𝑤)) = ((𝑏𝑧)‘(((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤))))
248233, 245fvco3d 6918 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤))‘( 1𝑤)) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))))
249248ad2antrr 723 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤))‘( 1𝑤)) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))))
250242, 247, 2493eqtr3d 2784 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏𝑧)‘(((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤))) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))))
251 eqid 2736 . . . . . . . . . . . . . . . . . . . . 21 (comp‘𝐶) = (comp‘𝐶)
252243ad2antrr 723 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ( 1𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤))
25310, 6, 164, 169, 107, 169, 251, 171, 172, 252yon12 18072 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤)) = (( 1𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐶)𝑤)𝑘))
2546, 107, 11, 164, 171, 251, 169, 172catlid 17481 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (( 1𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐶)𝑤)𝑘) = 𝑘)
255253, 254eqtrd 2776 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤)) = 𝑘)
256255fveq2d 6823 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏𝑧)‘(((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤))) = ((𝑏𝑧)‘𝑘))
257250, 256eqtr3d 2778 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))) = ((𝑏𝑧)‘𝑘))
258173, 184, 2573eqtrd 2780 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = ((𝑏𝑧)‘𝑘))
259163, 258syldan 591 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧)) → ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = ((𝑏𝑧)‘𝑘))
260259mpteq2dva 5189 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ↦ ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧)‘𝑘)) = (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ↦ ((𝑏𝑧)‘𝑘)))
261152adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((𝑁𝑤)‘((𝑀𝑤)‘𝑏)) ∈ (⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st), (2nd)⟩))
262141, 261, 7, 217, 160natcl 17758 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st)‘𝑧)))
26312, 192, 217, 209, 215elsetchom 17885 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st)‘𝑧)) ↔ (((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧):((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟶((1st)‘𝑧)))
264262, 263mpbid 231 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧):((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟶((1st)‘𝑧))
265264feqmptd 6887 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧) = (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ↦ ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧)‘𝑘)))
266226feqmptd 6887 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (𝑏𝑧) = (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ↦ ((𝑏𝑧)‘𝑘)))
267260, 265, 2663eqtr4d 2786 . . . . . . . . . . . . 13 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧) = (𝑏𝑧))
268153, 157, 267eqfnfvd 6962 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑁𝑤)‘((𝑀𝑤)‘𝑏)) = 𝑏)
269268mpteq2dva 5189 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑏 ∈ ((1st𝑍)𝑤) ↦ ((𝑁𝑤)‘((𝑀𝑤)‘𝑏))) = (𝑏 ∈ ((1st𝑍)𝑤) ↦ 𝑏))
270 mptresid 5984 . . . . . . . . . . 11 ( I ↾ ((1st𝑍)𝑤)) = (𝑏 ∈ ((1st𝑍)𝑤) ↦ 𝑏)
271269, 270eqtr4di 2794 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑏 ∈ ((1st𝑍)𝑤) ↦ ((𝑁𝑤)‘((𝑀𝑤)‘𝑏))) = ( I ↾ ((1st𝑍)𝑤)))
272140, 271eqtrd 2776 . . . . . . . . 9 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑁𝑤) ∘ (𝑀𝑤)) = ( I ↾ ((1st𝑍)𝑤)))
273 fcof1o 7218 . . . . . . . . 9 ((((𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤) ∧ (𝑁𝑤):((1st𝐸)𝑤)⟶((1st𝑍)𝑤)) ∧ (((𝑀𝑤) ∘ (𝑁𝑤)) = ( I ↾ ((1st𝐸)𝑤)) ∧ ((𝑁𝑤) ∘ (𝑀𝑤)) = ( I ↾ ((1st𝑍)𝑤)))) → ((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑀𝑤) = (𝑁𝑤)))
27435, 84, 138, 272, 273syl22anc 836 . . . . . . . 8 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑀𝑤) = (𝑁𝑤)))
275 eqcom 2743 . . . . . . . . 9 ((𝑀𝑤) = (𝑁𝑤) ↔ (𝑁𝑤) = (𝑀𝑤))
276275anbi2i 623 . . . . . . . 8 (((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑀𝑤) = (𝑁𝑤)) ↔ ((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑁𝑤) = (𝑀𝑤)))
277274, 276sylib 217 . . . . . . 7 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑁𝑤) = (𝑀𝑤)))
278 eqid 2736 . . . . . . . . . . 11 (Base‘𝑇) = (Base‘𝑇)
279 relfunc 17666 . . . . . . . . . . . 12 Rel ((𝑄 ×c 𝑂) Func 𝑇)
280 1st2ndbr 7943 . . . . . . . . . . . 12 ((Rel ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st𝑍)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝑍))
281279, 22, 280sylancr 587 . . . . . . . . . . 11 (𝜑 → (1st𝑍)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝑍))
2828, 278, 281funcf1 17670 . . . . . . . . . 10 (𝜑 → (1st𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
28313, 18setcbas 17882 . . . . . . . . . . 11 (𝜑𝑉 = (Base‘𝑇))
284283feq3d 6632 . . . . . . . . . 10 (𝜑 → ((1st𝑍):((𝑂 Func 𝑆) × 𝐵)⟶𝑉 ↔ (1st𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇)))
285282, 284mpbird 256 . . . . . . . . 9 (𝜑 → (1st𝑍):((𝑂 Func 𝑆) × 𝐵)⟶𝑉)
286285fovcdmda 7497 . . . . . . . 8 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((1st𝑍)𝑤) ∈ 𝑉)
287 1st2ndbr 7943 . . . . . . . . . . . 12 ((Rel ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st𝐸)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝐸))
288279, 23, 287sylancr 587 . . . . . . . . . . 11 (𝜑 → (1st𝐸)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝐸))
2898, 278, 288funcf1 17670 . . . . . . . . . 10 (𝜑 → (1st𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
290283feq3d 6632 . . . . . . . . . 10 (𝜑 → ((1st𝐸):((𝑂 Func 𝑆) × 𝐵)⟶𝑉 ↔ (1st𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇)))
291289, 290mpbird 256 . . . . . . . . 9 (𝜑 → (1st𝐸):((𝑂 Func 𝑆) × 𝐵)⟶𝑉)
292291fovcdmda 7497 . . . . . . . 8 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((1st𝐸)𝑤) ∈ 𝑉)
29313, 29, 286, 292, 25setcinv 17894 . . . . . . 7 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤)(((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤))(𝑁𝑤) ↔ ((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑁𝑤) = (𝑀𝑤))))
294277, 293mpbird 256 . . . . . 6 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑀𝑤)(((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤))(𝑁𝑤))
295294ralrimivva 3193 . . . . 5 (𝜑 → ∀ ∈ (𝑂 Func 𝑆)∀𝑤𝐵 (𝑀𝑤)(((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤))(𝑁𝑤))
296 fveq2 6819 . . . . . . . 8 (𝑧 = ⟨, 𝑤⟩ → (𝑀𝑧) = (𝑀‘⟨, 𝑤⟩))
297 df-ov 7332 . . . . . . . 8 (𝑀𝑤) = (𝑀‘⟨, 𝑤⟩)
298296, 297eqtr4di 2794 . . . . . . 7 (𝑧 = ⟨, 𝑤⟩ → (𝑀𝑧) = (𝑀𝑤))
299 fveq2 6819 . . . . . . . . 9 (𝑧 = ⟨, 𝑤⟩ → ((1st𝑍)‘𝑧) = ((1st𝑍)‘⟨, 𝑤⟩))
300 df-ov 7332 . . . . . . . . 9 ((1st𝑍)𝑤) = ((1st𝑍)‘⟨, 𝑤⟩)
301299, 300eqtr4di 2794 . . . . . . . 8 (𝑧 = ⟨, 𝑤⟩ → ((1st𝑍)‘𝑧) = ((1st𝑍)𝑤))
302 fveq2 6819 . . . . . . . . 9 (𝑧 = ⟨, 𝑤⟩ → ((1st𝐸)‘𝑧) = ((1st𝐸)‘⟨, 𝑤⟩))
303 df-ov 7332 . . . . . . . . 9 ((1st𝐸)𝑤) = ((1st𝐸)‘⟨, 𝑤⟩)
304302, 303eqtr4di 2794 . . . . . . . 8 (𝑧 = ⟨, 𝑤⟩ → ((1st𝐸)‘𝑧) = ((1st𝐸)𝑤))
305301, 304oveq12d 7347 . . . . . . 7 (𝑧 = ⟨, 𝑤⟩ → (((1st𝑍)‘𝑧)(Inv‘𝑇)((1st𝐸)‘𝑧)) = (((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤)))
306 fveq2 6819 . . . . . . . 8 (𝑧 = ⟨, 𝑤⟩ → (𝑁𝑧) = (𝑁‘⟨, 𝑤⟩))
307 df-ov 7332 . . . . . . . 8 (𝑁𝑤) = (𝑁‘⟨, 𝑤⟩)
308306, 307eqtr4di 2794 . . . . . . 7 (𝑧 = ⟨, 𝑤⟩ → (𝑁𝑧) = (𝑁𝑤))
309298, 305, 308breq123d 5103 . . . . . 6 (𝑧 = ⟨, 𝑤⟩ → ((𝑀𝑧)(((1st𝑍)‘𝑧)(Inv‘𝑇)((1st𝐸)‘𝑧))(𝑁𝑧) ↔ (𝑀𝑤)(((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤))(𝑁𝑤)))
310309ralxp 5777 . . . . 5 (∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑀𝑧)(((1st𝑍)‘𝑧)(Inv‘𝑇)((1st𝐸)‘𝑧))(𝑁𝑧) ↔ ∀ ∈ (𝑂 Func 𝑆)∀𝑤𝐵 (𝑀𝑤)(((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤))(𝑁𝑤))
311295, 310sylibr 233 . . . 4 (𝜑 → ∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑀𝑧)(((1st𝑍)‘𝑧)(Inv‘𝑇)((1st𝐸)‘𝑧))(𝑁𝑧))
312311r19.21bi 3230 . . 3 ((𝜑𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)) → (𝑀𝑧)(((1st𝑍)‘𝑧)(Inv‘𝑇)((1st𝐸)‘𝑧))(𝑁𝑧))
3131, 8, 9, 22, 23, 24, 25, 27, 312invfuc 17781 . 2 (𝜑𝑀(𝑍𝐼𝐸)(𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁𝑧)))
314 fvex 6832 . . . . 5 ((1st𝑓)‘𝑥) ∈ V
315314mptex 7149 . . . 4 (𝑢 ∈ ((1st𝑓)‘𝑥) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢)))) ∈ V
31642, 315fnmpoi 7970 . . 3 𝑁 Fn ((𝑂 Func 𝑆) × 𝐵)
317 dffn5 6878 . . 3 (𝑁 Fn ((𝑂 Func 𝑆) × 𝐵) ↔ 𝑁 = (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁𝑧)))
318316, 317mpbi 229 . 2 𝑁 = (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁𝑧))
319313, 318breqtrrdi 5131 1 (𝜑𝑀(𝑍𝐼𝐸)𝑁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1540  wcel 2105  wral 3061  Vcvv 3441  cun 3895  wss 3897  cop 4578   class class class wbr 5089  cmpt 5172   I cid 5511   × cxp 5612  ccnv 5613  ran crn 5615  cres 5616  ccom 5618  Rel wrel 5619   Fn wfn 6468  wf 6469  1-1-ontowf1o 6472  cfv 6473  (class class class)co 7329  cmpo 7331  1st c1st 7889  2nd c2nd 7890  tpos ctpos 8103  Basecbs 17001  Hom chom 17062  compcco 17063  Catccat 17462  Idccid 17463  Homf chomf 17464  oppCatcoppc 17509  Invcinv 17546   Func cfunc 17658  func ccofu 17660   Nat cnat 17746   FuncCat cfuc 17747  SetCatcsetc 17879   ×c cxpc 17974   1stF c1stf 17975   2ndF c2ndf 17976   ⟨,⟩F cprf 17977   evalF cevlf 18016  HomFchof 18055  Yoncyon 18056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5226  ax-sep 5240  ax-nul 5247  ax-pow 5305  ax-pr 5369  ax-un 7642  ax-cnex 11020  ax-resscn 11021  ax-1cn 11022  ax-icn 11023  ax-addcl 11024  ax-addrcl 11025  ax-mulcl 11026  ax-mulrcl 11027  ax-mulcom 11028  ax-addass 11029  ax-mulass 11030  ax-distr 11031  ax-i2m1 11032  ax-1ne0 11033  ax-1rid 11034  ax-rnegex 11035  ax-rrecex 11036  ax-cnre 11037  ax-pre-lttri 11038  ax-pre-lttrn 11039  ax-pre-ltadd 11040  ax-pre-mulgt0 11041
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-tp 4577  df-op 4579  df-uni 4852  df-iun 4940  df-br 5090  df-opab 5152  df-mpt 5173  df-tr 5207  df-id 5512  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5569  df-we 5571  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6232  df-ord 6299  df-on 6300  df-lim 6301  df-suc 6302  df-iota 6425  df-fun 6475  df-fn 6476  df-f 6477  df-f1 6478  df-fo 6479  df-f1o 6480  df-fv 6481  df-riota 7286  df-ov 7332  df-oprab 7333  df-mpo 7334  df-om 7773  df-1st 7891  df-2nd 7892  df-tpos 8104  df-frecs 8159  df-wrecs 8190  df-recs 8264  df-rdg 8303  df-1o 8359  df-er 8561  df-map 8680  df-pm 8681  df-ixp 8749  df-en 8797  df-dom 8798  df-sdom 8799  df-fin 8800  df-pnf 11104  df-mnf 11105  df-xr 11106  df-ltxr 11107  df-le 11108  df-sub 11300  df-neg 11301  df-nn 12067  df-2 12129  df-3 12130  df-4 12131  df-5 12132  df-6 12133  df-7 12134  df-8 12135  df-9 12136  df-n0 12327  df-z 12413  df-dec 12531  df-uz 12676  df-fz 13333  df-struct 16937  df-sets 16954  df-slot 16972  df-ndx 16984  df-base 17002  df-ress 17031  df-hom 17075  df-cco 17076  df-cat 17466  df-cid 17467  df-homf 17468  df-comf 17469  df-oppc 17510  df-sect 17548  df-inv 17549  df-ssc 17611  df-resc 17612  df-subc 17613  df-func 17662  df-cofu 17664  df-nat 17748  df-fuc 17749  df-setc 17880  df-xpc 17978  df-1stf 17979  df-2ndf 17980  df-prf 17981  df-evlf 18020  df-curf 18021  df-hof 18057  df-yon 18058
This theorem is referenced by:  yonffthlem  18089  yoneda  18090
  Copyright terms: Public domain W3C validator