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

Theorem yonedainv 18338
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 2735 . . . 4 (𝑄 ×c 𝑂) = (𝑄 ×c 𝑂)
3 yoneda.q . . . . 5 𝑄 = (𝑂 FuncCat 𝑆)
43fucbas 18016 . . . 4 (𝑂 Func 𝑆) = (Base‘𝑄)
5 yoneda.o . . . . 5 𝑂 = (oppCat‘𝐶)
6 yoneda.b . . . . 5 𝐵 = (Base‘𝐶)
75, 6oppcbas 17764 . . . 4 𝐵 = (Base‘𝑂)
82, 4, 7xpcbas 18234 . . 3 ((𝑂 Func 𝑆) × 𝐵) = (Base‘(𝑄 ×c 𝑂))
9 eqid 2735 . . 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 18329 . . . 4 (𝜑 → (𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)))
2221simpld 494 . . 3 (𝜑𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇))
2321simprd 495 . . 3 (𝜑𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇))
24 yonedainv.i . . 3 𝐼 = (Inv‘𝑅)
25 eqid 2735 . . 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 18337 . . 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 771 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ∈ (𝑂 Func 𝑆))
33 simprr 773 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → 𝑤𝐵)
3410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33, 26yonedalem3a 18331 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))) ∧ (𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤)))
3534simprd 495 . . . . . . . . 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 777 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → ∈ (𝑂 Func 𝑆))
41 simplrr 778 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → 𝑤𝐵)
42 yonedainv.n . . . . . . . . . . . 12 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥𝐵 ↦ (𝑢 ∈ ((1st𝑓)‘𝑥) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢)))))
43 simpr 484 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → 𝑏 ∈ ((1st)‘𝑤))
4410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 36, 37, 38, 39, 40, 41, 42, 43yonedalem4c 18334 . . . . . . . . . . 11 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → ((𝑁𝑤)‘𝑏) ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
4544fmpttd 7135 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑏 ∈ ((1st)‘𝑤) ↦ ((𝑁𝑤)‘𝑏)):((1st)‘𝑤)⟶(((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
466fvexi 6921 . . . . . . . . . . . . . . 15 𝐵 ∈ V
4746mptex 7243 . . . . . . . . . . . . . 14 (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢))) ∈ V
48 eqid 2735 . . . . . . . . . . . . . 14 (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))) = (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢))))
4947, 48fnmpti 6712 . . . . . . . . . . . . 13 (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))) Fn ((1st)‘𝑤)
50 simpl 482 . . . . . . . . . . . . . . . . . . 19 ((𝑓 = 𝑥 = 𝑤) → 𝑓 = )
5150fveq2d 6911 . . . . . . . . . . . . . . . . . 18 ((𝑓 = 𝑥 = 𝑤) → (1st𝑓) = (1st))
52 simpr 484 . . . . . . . . . . . . . . . . . 18 ((𝑓 = 𝑥 = 𝑤) → 𝑥 = 𝑤)
5351, 52fveq12d 6914 . . . . . . . . . . . . . . . . 17 ((𝑓 = 𝑥 = 𝑤) → ((1st𝑓)‘𝑥) = ((1st)‘𝑤))
54 simplr 769 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → 𝑥 = 𝑤)
5554oveq2d 7447 . . . . . . . . . . . . . . . . . . 19 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → (𝑦(Hom ‘𝐶)𝑥) = (𝑦(Hom ‘𝐶)𝑤))
56 simpll 767 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → 𝑓 = )
5756fveq2d 6911 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → (2nd𝑓) = (2nd))
58 eqidd 2736 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → 𝑦 = 𝑦)
5957, 54, 58oveq123d 7452 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → (𝑥(2nd𝑓)𝑦) = (𝑤(2nd)𝑦))
6059fveq1d 6909 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → ((𝑥(2nd𝑓)𝑦)‘𝑔) = ((𝑤(2nd)𝑦)‘𝑔))
6160fveq1d 6909 . . . . . . . . . . . . . . . . . . 19 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢) = (((𝑤(2nd)𝑦)‘𝑔)‘𝑢))
6255, 61mpteq12dv 5239 . . . . . . . . . . . . . . . . . 18 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢)) = (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))
6362mpteq2dva 5248 . . . . . . . . . . . . . . . . 17 ((𝑓 = 𝑥 = 𝑤) → (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢))) = (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢))))
6453, 63mpteq12dv 5239 . . . . . . . . . . . . . . . 16 ((𝑓 = 𝑥 = 𝑤) → (𝑢 ∈ ((1st𝑓)‘𝑥) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢)))) = (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))))
65 fvex 6920 . . . . . . . . . . . . . . . . 17 ((1st)‘𝑤) ∈ V
6665mptex 7243 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))) ∈ V
6764, 42, 66ovmpoa 7588 . . . . . . . . . . . . . . 15 (( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵) → (𝑁𝑤) = (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))))
6867adantl 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑁𝑤) = (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))))
6968fneq1d 6662 . . . . . . . . . . . . 13 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑁𝑤) Fn ((1st)‘𝑤) ↔ (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))) Fn ((1st)‘𝑤)))
7049, 69mpbiri 258 . . . . . . . . . . . 12 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑁𝑤) Fn ((1st)‘𝑤))
71 dffn5 6967 . . . . . . . . . . . 12 ((𝑁𝑤) Fn ((1st)‘𝑤) ↔ (𝑁𝑤) = (𝑏 ∈ ((1st)‘𝑤) ↦ ((𝑁𝑤)‘𝑏)))
7270, 71sylib 218 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑁𝑤) = (𝑏 ∈ ((1st)‘𝑤) ↦ ((𝑁𝑤)‘𝑏)))
735oppccat 17769 . . . . . . . . . . . . . 14 (𝐶 ∈ Cat → 𝑂 ∈ Cat)
7417, 73syl 17 . . . . . . . . . . . . 13 (𝜑𝑂 ∈ Cat)
7574adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → 𝑂 ∈ Cat)
7620unssbd 4204 . . . . . . . . . . . . . . 15 (𝜑𝑈𝑉)
7718, 76ssexd 5330 . . . . . . . . . . . . . 14 (𝜑𝑈 ∈ V)
7812setccat 18139 . . . . . . . . . . . . . 14 (𝑈 ∈ V → 𝑆 ∈ Cat)
7977, 78syl 17 . . . . . . . . . . . . 13 (𝜑𝑆 ∈ Cat)
8079adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → 𝑆 ∈ Cat)
8115, 75, 80, 7, 32, 33evlf1 18277 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((1st𝐸)𝑤) = ((1st)‘𝑤))
8210, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33yonedalem21 18330 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((1st𝑍)𝑤) = (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
8372, 81, 82feq123d 6726 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑁𝑤):((1st𝐸)𝑤)⟶((1st𝑍)𝑤) ↔ (𝑏 ∈ ((1st)‘𝑤) ↦ ((𝑁𝑤)‘𝑏)):((1st)‘𝑤)⟶(((1st𝑌)‘𝑤)(𝑂 Nat 𝑆))))
8445, 83mpbird 257 . . . . . . . . 9 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑁𝑤):((1st𝐸)𝑤)⟶((1st𝑍)𝑤))
85 fcompt 7153 . . . . . . . . . . 11 (((𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤) ∧ (𝑁𝑤):((1st𝐸)𝑤)⟶((1st𝑍)𝑤)) → ((𝑀𝑤) ∘ (𝑁𝑤)) = (𝑘 ∈ ((1st𝐸)𝑤) ↦ ((𝑀𝑤)‘((𝑁𝑤)‘𝑘))))
8635, 84, 85syl2anc 584 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤) ∘ (𝑁𝑤)) = (𝑘 ∈ ((1st𝐸)𝑤) ↦ ((𝑀𝑤)‘((𝑁𝑤)‘𝑘))))
8781eleq2d 2825 . . . . . . . . . . . . . 14 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑘 ∈ ((1st𝐸)𝑤) ↔ 𝑘 ∈ ((1st)‘𝑤)))
8887biimpa 476 . . . . . . . . . . . . 13 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st𝐸)𝑤)) → 𝑘 ∈ ((1st)‘𝑤))
8928adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝐶 ∈ Cat)
9029adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝑉𝑊)
9130adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ran (Homf𝐶) ⊆ 𝑈)
9231adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
93 simplrl 777 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ∈ (𝑂 Func 𝑆))
94 simplrr 778 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝑤𝐵)
9510, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 89, 90, 91, 92, 93, 94, 26yonedalem3a 18331 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑀𝑤) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))) ∧ (𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤)))
9695simpld 494 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (𝑀𝑤) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))))
9796fveq1d 6909 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑀𝑤)‘((𝑁𝑤)‘𝑘)) = ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘((𝑁𝑤)‘𝑘)))
9872, 44fmpt3d 7136 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑁𝑤):((1st)‘𝑤)⟶(((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
9998ffvelcdmda 7104 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑁𝑤)‘𝑘) ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
100 fveq1 6906 . . . . . . . . . . . . . . . . 17 (𝑎 = ((𝑁𝑤)‘𝑘) → (𝑎𝑤) = (((𝑁𝑤)‘𝑘)‘𝑤))
101100fveq1d 6909 . . . . . . . . . . . . . . . 16 (𝑎 = ((𝑁𝑤)‘𝑘) → ((𝑎𝑤)‘( 1𝑤)) = ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)))
102 eqid 2735 . . . . . . . . . . . . . . . 16 (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))
103 fvex 6920 . . . . . . . . . . . . . . . 16 ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)) ∈ V
104101, 102, 103fvmpt 7016 . . . . . . . . . . . . . . 15 (((𝑁𝑤)‘𝑘) ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) → ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘((𝑁𝑤)‘𝑘)) = ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)))
10599, 104syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘((𝑁𝑤)‘𝑘)) = ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)))
106 simpr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝑘 ∈ ((1st)‘𝑤))
107 eqid 2735 . . . . . . . . . . . . . . . . 17 (Hom ‘𝐶) = (Hom ‘𝐶)
1086, 107, 11, 89, 94catidcl 17727 . . . . . . . . . . . . . . . 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 18333 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)) = (((𝑤(2nd)𝑤)‘( 1𝑤))‘𝑘))
110 eqid 2735 . . . . . . . . . . . . . . . . . 18 (Id‘𝑂) = (Id‘𝑂)
111 eqid 2735 . . . . . . . . . . . . . . . . . 18 (Id‘𝑆) = (Id‘𝑆)
112 relfunc 17913 . . . . . . . . . . . . . . . . . . 19 Rel (𝑂 Func 𝑆)
113 1st2ndbr 8066 . . . . . . . . . . . . . . . . . . 19 ((Rel (𝑂 Func 𝑆) ∧ ∈ (𝑂 Func 𝑆)) → (1st)(𝑂 Func 𝑆)(2nd))
114112, 93, 113sylancr 587 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (1st)(𝑂 Func 𝑆)(2nd))
1157, 110, 111, 114, 94funcid 17921 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑤(2nd)𝑤)‘((Id‘𝑂)‘𝑤)) = ((Id‘𝑆)‘((1st)‘𝑤)))
1165, 11oppcid 17768 . . . . . . . . . . . . . . . . . . . 20 (𝐶 ∈ Cat → (Id‘𝑂) = 1 )
11789, 116syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (Id‘𝑂) = 1 )
118117fveq1d 6909 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((Id‘𝑂)‘𝑤) = ( 1𝑤))
119118fveq2d 6911 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑤(2nd)𝑤)‘((Id‘𝑂)‘𝑤)) = ((𝑤(2nd)𝑤)‘( 1𝑤)))
12077ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝑈 ∈ V)
121 eqid 2735 . . . . . . . . . . . . . . . . . . . . 21 (Base‘𝑆) = (Base‘𝑆)
1227, 121, 114funcf1 17917 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (1st):𝐵⟶(Base‘𝑆))
12312, 120setcbas 18132 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝑈 = (Base‘𝑆))
124123feq3d 6724 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((1st):𝐵𝑈 ↔ (1st):𝐵⟶(Base‘𝑆)))
125122, 124mpbird 257 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (1st):𝐵𝑈)
126125, 94ffvelcdmd 7105 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((1st)‘𝑤) ∈ 𝑈)
12712, 111, 120, 126setcid 18140 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((Id‘𝑆)‘((1st)‘𝑤)) = ( I ↾ ((1st)‘𝑤)))
128115, 119, 1273eqtr3d 2783 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑤(2nd)𝑤)‘( 1𝑤)) = ( I ↾ ((1st)‘𝑤)))
129128fveq1d 6909 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (((𝑤(2nd)𝑤)‘( 1𝑤))‘𝑘) = (( I ↾ ((1st)‘𝑤))‘𝑘))
130 fvresi 7193 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ((1st)‘𝑤) → (( I ↾ ((1st)‘𝑤))‘𝑘) = 𝑘)
131130adantl 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (( I ↾ ((1st)‘𝑤))‘𝑘) = 𝑘)
132109, 129, 1313eqtrd 2779 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)) = 𝑘)
13397, 105, 1323eqtrd 2779 . . . . . . . . . . . . 13 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑀𝑤)‘((𝑁𝑤)‘𝑘)) = 𝑘)
13488, 133syldan 591 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st𝐸)𝑤)) → ((𝑀𝑤)‘((𝑁𝑤)‘𝑘)) = 𝑘)
135134mpteq2dva 5248 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑘 ∈ ((1st𝐸)𝑤) ↦ ((𝑀𝑤)‘((𝑁𝑤)‘𝑘))) = (𝑘 ∈ ((1st𝐸)𝑤) ↦ 𝑘))
136 mptresid 6071 . . . . . . . . . . 11 ( I ↾ ((1st𝐸)𝑤)) = (𝑘 ∈ ((1st𝐸)𝑤) ↦ 𝑘)
137135, 136eqtr4di 2793 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑘 ∈ ((1st𝐸)𝑤) ↦ ((𝑀𝑤)‘((𝑁𝑤)‘𝑘))) = ( I ↾ ((1st𝐸)𝑤)))
13886, 137eqtrd 2775 . . . . . . . . 9 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤) ∘ (𝑁𝑤)) = ( I ↾ ((1st𝐸)𝑤)))
139 fcompt 7153 . . . . . . . . . . 11 (((𝑁𝑤):((1st𝐸)𝑤)⟶((1st𝑍)𝑤) ∧ (𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤)) → ((𝑁𝑤) ∘ (𝑀𝑤)) = (𝑏 ∈ ((1st𝑍)𝑤) ↦ ((𝑁𝑤)‘((𝑀𝑤)‘𝑏))))
14084, 35, 139syl2anc 584 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑁𝑤) ∘ (𝑀𝑤)) = (𝑏 ∈ ((1st𝑍)𝑤) ↦ ((𝑁𝑤)‘((𝑀𝑤)‘𝑏))))
141 eqid 2735 . . . . . . . . . . . . . 14 (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆)
14228adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝐶 ∈ Cat)
14329adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑉𝑊)
14430adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ran (Homf𝐶) ⊆ 𝑈)
14531adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
146 simplrl 777 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ∈ (𝑂 Func 𝑆))
147 simplrr 778 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑤𝐵)
14881feq3d 6724 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤) ↔ (𝑀𝑤):((1st𝑍)𝑤)⟶((1st)‘𝑤)))
14935, 148mpbid 232 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑀𝑤):((1st𝑍)𝑤)⟶((1st)‘𝑤))
150149ffvelcdmda 7104 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑀𝑤)‘𝑏) ∈ ((1st)‘𝑤))
15110, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 142, 143, 144, 145, 146, 147, 42, 150yonedalem4c 18334 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑁𝑤)‘((𝑀𝑤)‘𝑏)) ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
152141, 151nat1st2nd 18006 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑁𝑤)‘((𝑀𝑤)‘𝑏)) ∈ (⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st), (2nd)⟩))
153141, 152, 7natfn 18009 . . . . . . . . . . . . 13 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑁𝑤)‘((𝑀𝑤)‘𝑏)) Fn 𝐵)
15482eleq2d 2825 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑏 ∈ ((1st𝑍)𝑤) ↔ 𝑏 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆))))
155154biimpa 476 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑏 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
156141, 155nat1st2nd 18006 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑏 ∈ (⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st), (2nd)⟩))
157141, 156, 7natfn 18009 . . . . . . . . . . . . 13 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑏 Fn 𝐵)
158142adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → 𝐶 ∈ Cat)
159147adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → 𝑤𝐵)
160 simpr 484 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → 𝑧𝐵)
16110, 6, 158, 159, 107, 160yon11 18321 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((1st ‘((1st𝑌)‘𝑤))‘𝑧) = (𝑧(Hom ‘𝐶)𝑤))
162161eleq2d 2825 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ↔ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))
163162biimpa 476 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧)) → 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤))
164158adantr 480 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝐶 ∈ Cat)
165143ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑉𝑊)
166144ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ran (Homf𝐶) ⊆ 𝑈)
167145ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
168146ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ∈ (𝑂 Func 𝑆))
169159adantr 480 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑤𝐵)
170150ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑀𝑤)‘𝑏) ∈ ((1st)‘𝑤))
171 simplr 769 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑧𝐵)
172 simpr 484 . . . . . . . . . . . . . . . . . 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 18333 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑀𝑤)‘𝑏)))
17410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 164, 165, 166, 167, 168, 169, 26yonedalem3a 18331 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑀𝑤) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))) ∧ (𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤)))
175174simpld 494 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑀𝑤) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))))
176175fveq1d 6909 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑀𝑤)‘𝑏) = ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘𝑏))
177155ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑏 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
178 fveq1 6906 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑏 → (𝑎𝑤) = (𝑏𝑤))
179178fveq1d 6909 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑏 → ((𝑎𝑤)‘( 1𝑤)) = ((𝑏𝑤)‘( 1𝑤)))
180 fvex 6920 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏𝑤)‘( 1𝑤)) ∈ V
181179, 102, 180fvmpt 7016 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) → ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘𝑏) = ((𝑏𝑤)‘( 1𝑤)))
182177, 181syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘𝑏) = ((𝑏𝑤)‘( 1𝑤)))
183176, 182eqtrd 2775 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑀𝑤)‘𝑏) = ((𝑏𝑤)‘( 1𝑤)))
184183fveq2d 6911 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd)𝑧)‘𝑘)‘((𝑀𝑤)‘𝑏)) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))))
185156ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑏 ∈ (⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st), (2nd)⟩))
186 eqid 2735 . . . . . . . . . . . . . . . . . . . . . 22 (Hom ‘𝑂) = (Hom ‘𝑂)
187 eqid 2735 . . . . . . . . . . . . . . . . . . . . . 22 (comp‘𝑆) = (comp‘𝑆)
188107, 5oppchom 17761 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤(Hom ‘𝑂)𝑧) = (𝑧(Hom ‘𝐶)𝑤)
189172, 188eleqtrrdi 2850 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑘 ∈ (𝑤(Hom ‘𝑂)𝑧))
190141, 185, 7, 186, 187, 169, 171, 189nati 18010 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏𝑧)(⟨((1st ‘((1st𝑌)‘𝑤))‘𝑤), ((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟩(comp‘𝑆)((1st)‘𝑧))((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)) = (((𝑤(2nd)𝑧)‘𝑘)(⟨((1st ‘((1st𝑌)‘𝑤))‘𝑤), ((1st)‘𝑤)⟩(comp‘𝑆)((1st)‘𝑧))(𝑏𝑤)))
19177ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑈 ∈ V)
192191adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → 𝑈 ∈ V)
193192adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑈 ∈ V)
194 relfunc 17913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Rel (𝐶 Func 𝑄)
19510, 17, 5, 12, 3, 77, 19yoncl 18319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑𝑌 ∈ (𝐶 Func 𝑄))
196 1st2ndbr 8066 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((Rel (𝐶 Func 𝑄) ∧ 𝑌 ∈ (𝐶 Func 𝑄)) → (1st𝑌)(𝐶 Func 𝑄)(2nd𝑌))
197194, 195, 196sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (1st𝑌)(𝐶 Func 𝑄)(2nd𝑌))
1986, 4, 197funcf1 17917 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (1st𝑌):𝐵⟶(𝑂 Func 𝑆))
199198ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st𝑌):𝐵⟶(𝑂 Func 𝑆))
200199, 147ffvelcdmd 7105 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st𝑌)‘𝑤) ∈ (𝑂 Func 𝑆))
201 1st2ndbr 8066 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 17917 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st ‘((1st𝑌)‘𝑤)):𝐵⟶(Base‘𝑆))
20412, 191setcbas 18132 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑈 = (Base‘𝑆))
205204feq3d 6724 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st ‘((1st𝑌)‘𝑤)):𝐵𝑈 ↔ (1st ‘((1st𝑌)‘𝑤)):𝐵⟶(Base‘𝑆)))
206203, 205mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st ‘((1st𝑌)‘𝑤)):𝐵𝑈)
207206, 147ffvelcdmd 7105 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st ‘((1st𝑌)‘𝑤))‘𝑤) ∈ 𝑈)
208207ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘((1st𝑌)‘𝑤))‘𝑤) ∈ 𝑈)
209206ffvelcdmda 7104 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ∈ 𝑈)
210209adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ∈ 𝑈)
211112, 146, 113sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st)(𝑂 Func 𝑆)(2nd))
2127, 121, 211funcf1 17917 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st):𝐵⟶(Base‘𝑆))
213204feq3d 6724 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st):𝐵𝑈 ↔ (1st):𝐵⟶(Base‘𝑆)))
214212, 213mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st):𝐵𝑈)
215214ffvelcdmda 7104 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((1st)‘𝑧) ∈ 𝑈)
216215adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st)‘𝑧) ∈ 𝑈)
217 eqid 2735 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Hom ‘𝑆) = (Hom ‘𝑆)
218202ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1st ‘((1st𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st𝑌)‘𝑤)))
2197, 186, 217, 218, 169, 171funcf2 17919 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧):(𝑤(Hom ‘𝑂)𝑧)⟶(((1st ‘((1st𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑤))‘𝑧)))
220219, 189ffvelcdmd 7105 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑤))‘𝑧)))
22112, 193, 217, 208, 210elsetchom 18135 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑤))‘𝑧)) ↔ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st ‘((1st𝑌)‘𝑤))‘𝑧)))
222220, 221mpbid 232 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st ‘((1st𝑌)‘𝑤))‘𝑧))
223156adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → 𝑏 ∈ (⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st), (2nd)⟩))
224141, 223, 7, 217, 160natcl 18008 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (𝑏𝑧) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st)‘𝑧)))
22512, 192, 217, 209, 215elsetchom 18135 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((𝑏𝑧) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st)‘𝑧)) ↔ (𝑏𝑧):((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟶((1st)‘𝑧)))
226224, 225mpbid 232 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (𝑏𝑧):((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟶((1st)‘𝑧))
227226adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑏𝑧):((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟶((1st)‘𝑧))
22812, 193, 187, 208, 210, 216, 222, 227setcco 18137 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏𝑧)(⟨((1st ‘((1st𝑌)‘𝑤))‘𝑤), ((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟩(comp‘𝑆)((1st)‘𝑧))((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)) = ((𝑏𝑧) ∘ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)))
229214, 147ffvelcdmd 7105 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st)‘𝑤) ∈ 𝑈)
230229ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st)‘𝑤) ∈ 𝑈)
231141, 156, 7, 217, 147natcl 18008 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (𝑏𝑤) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st)‘𝑤)))
23212, 191, 217, 207, 229elsetchom 18135 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑏𝑤) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st)‘𝑤)) ↔ (𝑏𝑤):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st)‘𝑤)))
233231, 232mpbid 232 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (𝑏𝑤):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st)‘𝑤))
234233ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑏𝑤):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st)‘𝑤))
235112, 168, 113sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1st)(𝑂 Func 𝑆)(2nd))
2367, 186, 217, 235, 169, 171funcf2 17919 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑤(2nd)𝑧):(𝑤(Hom ‘𝑂)𝑧)⟶(((1st)‘𝑤)(Hom ‘𝑆)((1st)‘𝑧)))
237236, 189ffvelcdmd 7105 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd)𝑧)‘𝑘) ∈ (((1st)‘𝑤)(Hom ‘𝑆)((1st)‘𝑧)))
23812, 193, 217, 230, 216elsetchom 18135 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd)𝑧)‘𝑘) ∈ (((1st)‘𝑤)(Hom ‘𝑆)((1st)‘𝑧)) ↔ ((𝑤(2nd)𝑧)‘𝑘):((1st)‘𝑤)⟶((1st)‘𝑧)))
239237, 238mpbid 232 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd)𝑧)‘𝑘):((1st)‘𝑤)⟶((1st)‘𝑧))
24012, 193, 187, 208, 230, 216, 234, 239setcco 18137 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd)𝑧)‘𝑘)(⟨((1st ‘((1st𝑌)‘𝑤))‘𝑤), ((1st)‘𝑤)⟩(comp‘𝑆)((1st)‘𝑧))(𝑏𝑤)) = (((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤)))
241190, 228, 2403eqtr3d 2783 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏𝑧) ∘ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)) = (((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤)))
242241fveq1d 6909 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑏𝑧) ∘ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘))‘( 1𝑤)) = ((((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤))‘( 1𝑤)))
2436, 107, 11, 142, 147catidcl 17727 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ( 1𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤))
24410, 6, 142, 147, 107, 147yon11 18321 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st ‘((1st𝑌)‘𝑤))‘𝑤) = (𝑤(Hom ‘𝐶)𝑤))
245243, 244eleqtrrd 2842 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ( 1𝑤) ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑤))
246245ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ( 1𝑤) ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑤))
247222, 246fvco3d 7009 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑏𝑧) ∘ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘))‘( 1𝑤)) = ((𝑏𝑧)‘(((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤))))
248233, 245fvco3d 7009 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤))‘( 1𝑤)) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))))
249248ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤))‘( 1𝑤)) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))))
250242, 247, 2493eqtr3d 2783 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏𝑧)‘(((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤))) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))))
251 eqid 2735 . . . . . . . . . . . . . . . . . . . . 21 (comp‘𝐶) = (comp‘𝐶)
252243ad2antrr 726 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ( 1𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤))
25310, 6, 164, 169, 107, 169, 251, 171, 172, 252yon12 18322 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤)) = (( 1𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐶)𝑤)𝑘))
2546, 107, 11, 164, 171, 251, 169, 172catlid 17728 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (( 1𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐶)𝑤)𝑘) = 𝑘)
255253, 254eqtrd 2775 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤)) = 𝑘)
256255fveq2d 6911 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏𝑧)‘(((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤))) = ((𝑏𝑧)‘𝑘))
257250, 256eqtr3d 2777 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))) = ((𝑏𝑧)‘𝑘))
258173, 184, 2573eqtrd 2779 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = ((𝑏𝑧)‘𝑘))
259163, 258syldan 591 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧)) → ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = ((𝑏𝑧)‘𝑘))
260259mpteq2dva 5248 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ↦ ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧)‘𝑘)) = (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ↦ ((𝑏𝑧)‘𝑘)))
261152adantr 480 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((𝑁𝑤)‘((𝑀𝑤)‘𝑏)) ∈ (⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st), (2nd)⟩))
262141, 261, 7, 217, 160natcl 18008 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st)‘𝑧)))
26312, 192, 217, 209, 215elsetchom 18135 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st)‘𝑧)) ↔ (((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧):((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟶((1st)‘𝑧)))
264262, 263mpbid 232 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧):((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟶((1st)‘𝑧))
265264feqmptd 6977 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧) = (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ↦ ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧)‘𝑘)))
266226feqmptd 6977 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (𝑏𝑧) = (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ↦ ((𝑏𝑧)‘𝑘)))
267260, 265, 2663eqtr4d 2785 . . . . . . . . . . . . 13 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧) = (𝑏𝑧))
268153, 157, 267eqfnfvd 7054 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑁𝑤)‘((𝑀𝑤)‘𝑏)) = 𝑏)
269268mpteq2dva 5248 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑏 ∈ ((1st𝑍)𝑤) ↦ ((𝑁𝑤)‘((𝑀𝑤)‘𝑏))) = (𝑏 ∈ ((1st𝑍)𝑤) ↦ 𝑏))
270 mptresid 6071 . . . . . . . . . . 11 ( I ↾ ((1st𝑍)𝑤)) = (𝑏 ∈ ((1st𝑍)𝑤) ↦ 𝑏)
271269, 270eqtr4di 2793 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑏 ∈ ((1st𝑍)𝑤) ↦ ((𝑁𝑤)‘((𝑀𝑤)‘𝑏))) = ( I ↾ ((1st𝑍)𝑤)))
272140, 271eqtrd 2775 . . . . . . . . 9 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑁𝑤) ∘ (𝑀𝑤)) = ( I ↾ ((1st𝑍)𝑤)))
273 fcof1o 7316 . . . . . . . . 9 ((((𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤) ∧ (𝑁𝑤):((1st𝐸)𝑤)⟶((1st𝑍)𝑤)) ∧ (((𝑀𝑤) ∘ (𝑁𝑤)) = ( I ↾ ((1st𝐸)𝑤)) ∧ ((𝑁𝑤) ∘ (𝑀𝑤)) = ( I ↾ ((1st𝑍)𝑤)))) → ((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑀𝑤) = (𝑁𝑤)))
27435, 84, 138, 272, 273syl22anc 839 . . . . . . . 8 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑀𝑤) = (𝑁𝑤)))
275 eqcom 2742 . . . . . . . . 9 ((𝑀𝑤) = (𝑁𝑤) ↔ (𝑁𝑤) = (𝑀𝑤))
276275anbi2i 623 . . . . . . . 8 (((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑀𝑤) = (𝑁𝑤)) ↔ ((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑁𝑤) = (𝑀𝑤)))
277274, 276sylib 218 . . . . . . 7 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑁𝑤) = (𝑀𝑤)))
278 eqid 2735 . . . . . . . . . . 11 (Base‘𝑇) = (Base‘𝑇)
279 relfunc 17913 . . . . . . . . . . . 12 Rel ((𝑄 ×c 𝑂) Func 𝑇)
280 1st2ndbr 8066 . . . . . . . . . . . 12 ((Rel ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st𝑍)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝑍))
281279, 22, 280sylancr 587 . . . . . . . . . . 11 (𝜑 → (1st𝑍)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝑍))
2828, 278, 281funcf1 17917 . . . . . . . . . 10 (𝜑 → (1st𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
28313, 18setcbas 18132 . . . . . . . . . . 11 (𝜑𝑉 = (Base‘𝑇))
284283feq3d 6724 . . . . . . . . . 10 (𝜑 → ((1st𝑍):((𝑂 Func 𝑆) × 𝐵)⟶𝑉 ↔ (1st𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇)))
285282, 284mpbird 257 . . . . . . . . 9 (𝜑 → (1st𝑍):((𝑂 Func 𝑆) × 𝐵)⟶𝑉)
286285fovcdmda 7604 . . . . . . . 8 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((1st𝑍)𝑤) ∈ 𝑉)
287 1st2ndbr 8066 . . . . . . . . . . . 12 ((Rel ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st𝐸)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝐸))
288279, 23, 287sylancr 587 . . . . . . . . . . 11 (𝜑 → (1st𝐸)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝐸))
2898, 278, 288funcf1 17917 . . . . . . . . . 10 (𝜑 → (1st𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
290283feq3d 6724 . . . . . . . . . 10 (𝜑 → ((1st𝐸):((𝑂 Func 𝑆) × 𝐵)⟶𝑉 ↔ (1st𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇)))
291289, 290mpbird 257 . . . . . . . . 9 (𝜑 → (1st𝐸):((𝑂 Func 𝑆) × 𝐵)⟶𝑉)
292291fovcdmda 7604 . . . . . . . 8 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((1st𝐸)𝑤) ∈ 𝑉)
29313, 29, 286, 292, 25setcinv 18144 . . . . . . 7 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤)(((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤))(𝑁𝑤) ↔ ((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑁𝑤) = (𝑀𝑤))))
294277, 293mpbird 257 . . . . . 6 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑀𝑤)(((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤))(𝑁𝑤))
295294ralrimivva 3200 . . . . 5 (𝜑 → ∀ ∈ (𝑂 Func 𝑆)∀𝑤𝐵 (𝑀𝑤)(((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤))(𝑁𝑤))
296 fveq2 6907 . . . . . . . 8 (𝑧 = ⟨, 𝑤⟩ → (𝑀𝑧) = (𝑀‘⟨, 𝑤⟩))
297 df-ov 7434 . . . . . . . 8 (𝑀𝑤) = (𝑀‘⟨, 𝑤⟩)
298296, 297eqtr4di 2793 . . . . . . 7 (𝑧 = ⟨, 𝑤⟩ → (𝑀𝑧) = (𝑀𝑤))
299 fveq2 6907 . . . . . . . . 9 (𝑧 = ⟨, 𝑤⟩ → ((1st𝑍)‘𝑧) = ((1st𝑍)‘⟨, 𝑤⟩))
300 df-ov 7434 . . . . . . . . 9 ((1st𝑍)𝑤) = ((1st𝑍)‘⟨, 𝑤⟩)
301299, 300eqtr4di 2793 . . . . . . . 8 (𝑧 = ⟨, 𝑤⟩ → ((1st𝑍)‘𝑧) = ((1st𝑍)𝑤))
302 fveq2 6907 . . . . . . . . 9 (𝑧 = ⟨, 𝑤⟩ → ((1st𝐸)‘𝑧) = ((1st𝐸)‘⟨, 𝑤⟩))
303 df-ov 7434 . . . . . . . . 9 ((1st𝐸)𝑤) = ((1st𝐸)‘⟨, 𝑤⟩)
304302, 303eqtr4di 2793 . . . . . . . 8 (𝑧 = ⟨, 𝑤⟩ → ((1st𝐸)‘𝑧) = ((1st𝐸)𝑤))
305301, 304oveq12d 7449 . . . . . . 7 (𝑧 = ⟨, 𝑤⟩ → (((1st𝑍)‘𝑧)(Inv‘𝑇)((1st𝐸)‘𝑧)) = (((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤)))
306 fveq2 6907 . . . . . . . 8 (𝑧 = ⟨, 𝑤⟩ → (𝑁𝑧) = (𝑁‘⟨, 𝑤⟩))
307 df-ov 7434 . . . . . . . 8 (𝑁𝑤) = (𝑁‘⟨, 𝑤⟩)
308306, 307eqtr4di 2793 . . . . . . 7 (𝑧 = ⟨, 𝑤⟩ → (𝑁𝑧) = (𝑁𝑤))
309298, 305, 308breq123d 5162 . . . . . 6 (𝑧 = ⟨, 𝑤⟩ → ((𝑀𝑧)(((1st𝑍)‘𝑧)(Inv‘𝑇)((1st𝐸)‘𝑧))(𝑁𝑧) ↔ (𝑀𝑤)(((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤))(𝑁𝑤)))
310309ralxp 5855 . . . . 5 (∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑀𝑧)(((1st𝑍)‘𝑧)(Inv‘𝑇)((1st𝐸)‘𝑧))(𝑁𝑧) ↔ ∀ ∈ (𝑂 Func 𝑆)∀𝑤𝐵 (𝑀𝑤)(((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤))(𝑁𝑤))
311295, 310sylibr 234 . . . 4 (𝜑 → ∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑀𝑧)(((1st𝑍)‘𝑧)(Inv‘𝑇)((1st𝐸)‘𝑧))(𝑁𝑧))
312311r19.21bi 3249 . . 3 ((𝜑𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)) → (𝑀𝑧)(((1st𝑍)‘𝑧)(Inv‘𝑇)((1st𝐸)‘𝑧))(𝑁𝑧))
3131, 8, 9, 22, 23, 24, 25, 27, 312invfuc 18031 . 2 (𝜑𝑀(𝑍𝐼𝐸)(𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁𝑧)))
314 fvex 6920 . . . . 5 ((1st𝑓)‘𝑥) ∈ V
315314mptex 7243 . . . 4 (𝑢 ∈ ((1st𝑓)‘𝑥) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢)))) ∈ V
31642, 315fnmpoi 8094 . . 3 𝑁 Fn ((𝑂 Func 𝑆) × 𝐵)
317 dffn5 6967 . . 3 (𝑁 Fn ((𝑂 Func 𝑆) × 𝐵) ↔ 𝑁 = (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁𝑧)))
318316, 317mpbi 230 . 2 𝑁 = (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁𝑧))
319313, 318breqtrrdi 5190 1 (𝜑𝑀(𝑍𝐼𝐸)𝑁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1537  wcel 2106  wral 3059  Vcvv 3478  cun 3961  wss 3963  cop 4637   class class class wbr 5148  cmpt 5231   I cid 5582   × cxp 5687  ccnv 5688  ran crn 5690  cres 5691  ccom 5693  Rel wrel 5694   Fn wfn 6558  wf 6559  1-1-ontowf1o 6562  cfv 6563  (class class class)co 7431  cmpo 7433  1st c1st 8011  2nd c2nd 8012  tpos ctpos 8249  Basecbs 17245  Hom chom 17309  compcco 17310  Catccat 17709  Idccid 17710  Homf chomf 17711  oppCatcoppc 17756  Invcinv 17793   Func cfunc 17905  func ccofu 17907   Nat cnat 17996   FuncCat cfuc 17997  SetCatcsetc 18129   ×c cxpc 18224   1stF c1stf 18225   2ndF c2ndf 18226   ⟨,⟩F cprf 18227   evalF cevlf 18266  HomFchof 18305  Yoncyon 18306
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-tpos 8250  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-er 8744  df-map 8867  df-pm 8868  df-ixp 8937  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-nn 12265  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334  df-n0 12525  df-z 12612  df-dec 12732  df-uz 12877  df-fz 13545  df-struct 17181  df-sets 17198  df-slot 17216  df-ndx 17228  df-base 17246  df-ress 17275  df-hom 17322  df-cco 17323  df-cat 17713  df-cid 17714  df-homf 17715  df-comf 17716  df-oppc 17757  df-sect 17795  df-inv 17796  df-ssc 17858  df-resc 17859  df-subc 17860  df-func 17909  df-cofu 17911  df-nat 17998  df-fuc 17999  df-setc 18130  df-xpc 18228  df-1stf 18229  df-2ndf 18230  df-prf 18231  df-evlf 18270  df-curf 18271  df-hof 18307  df-yon 18308
This theorem is referenced by:  yonffthlem  18339  yoneda  18340
  Copyright terms: Public domain W3C validator