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

Theorem yonedainv 17527
 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 2801 . . . 4 (𝑄 ×c 𝑂) = (𝑄 ×c 𝑂)
3 yoneda.q . . . . 5 𝑄 = (𝑂 FuncCat 𝑆)
43fucbas 17226 . . . 4 (𝑂 Func 𝑆) = (Base‘𝑄)
5 yoneda.o . . . . 5 𝑂 = (oppCat‘𝐶)
6 yoneda.b . . . . 5 𝐵 = (Base‘𝐶)
75, 6oppcbas 16984 . . . 4 𝐵 = (Base‘𝑂)
82, 4, 7xpcbas 17424 . . 3 ((𝑂 Func 𝑆) × 𝐵) = (Base‘(𝑄 ×c 𝑂))
9 eqid 2801 . . 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 17518 . . . 4 (𝜑 → (𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)))
2221simpld 498 . . 3 (𝜑𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇))
2321simprd 499 . . 3 (𝜑𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇))
24 yonedainv.i . . 3 𝐼 = (Inv‘𝑅)
25 eqid 2801 . . 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 17526 . . 3 (𝜑𝑀 ∈ (𝑍((𝑄 ×c 𝑂) Nat 𝑇)𝐸))
2817adantr 484 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → 𝐶 ∈ Cat)
2918adantr 484 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → 𝑉𝑊)
3019adantr 484 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ran (Homf𝐶) ⊆ 𝑈)
3120adantr 484 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
32 simprl 770 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ∈ (𝑂 Func 𝑆))
33 simprr 772 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → 𝑤𝐵)
3410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33, 26yonedalem3a 17520 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))) ∧ (𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤)))
3534simprd 499 . . . . . . . . 9 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤))
3628adantr 484 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → 𝐶 ∈ Cat)
3729adantr 484 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → 𝑉𝑊)
3830adantr 484 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → ran (Homf𝐶) ⊆ 𝑈)
3931adantr 484 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
40 simplrl 776 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → ∈ (𝑂 Func 𝑆))
41 simplrr 777 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → 𝑤𝐵)
42 yonedainv.n . . . . . . . . . . . 12 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥𝐵 ↦ (𝑢 ∈ ((1st𝑓)‘𝑥) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢)))))
43 simpr 488 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → 𝑏 ∈ ((1st)‘𝑤))
4410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 36, 37, 38, 39, 40, 41, 42, 43yonedalem4c 17523 . . . . . . . . . . 11 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st)‘𝑤)) → ((𝑁𝑤)‘𝑏) ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
4544fmpttd 6860 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑏 ∈ ((1st)‘𝑤) ↦ ((𝑁𝑤)‘𝑏)):((1st)‘𝑤)⟶(((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
466fvexi 6663 . . . . . . . . . . . . . . 15 𝐵 ∈ V
4746mptex 6967 . . . . . . . . . . . . . 14 (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢))) ∈ V
48 eqid 2801 . . . . . . . . . . . . . 14 (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))) = (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢))))
4947, 48fnmpti 6467 . . . . . . . . . . . . 13 (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))) Fn ((1st)‘𝑤)
50 simpl 486 . . . . . . . . . . . . . . . . . . 19 ((𝑓 = 𝑥 = 𝑤) → 𝑓 = )
5150fveq2d 6653 . . . . . . . . . . . . . . . . . 18 ((𝑓 = 𝑥 = 𝑤) → (1st𝑓) = (1st))
52 simpr 488 . . . . . . . . . . . . . . . . . 18 ((𝑓 = 𝑥 = 𝑤) → 𝑥 = 𝑤)
5351, 52fveq12d 6656 . . . . . . . . . . . . . . . . 17 ((𝑓 = 𝑥 = 𝑤) → ((1st𝑓)‘𝑥) = ((1st)‘𝑤))
54 simplr 768 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → 𝑥 = 𝑤)
5554oveq2d 7155 . . . . . . . . . . . . . . . . . . 19 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → (𝑦(Hom ‘𝐶)𝑥) = (𝑦(Hom ‘𝐶)𝑤))
56 simpll 766 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → 𝑓 = )
5756fveq2d 6653 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → (2nd𝑓) = (2nd))
58 eqidd 2802 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → 𝑦 = 𝑦)
5957, 54, 58oveq123d 7160 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → (𝑥(2nd𝑓)𝑦) = (𝑤(2nd)𝑦))
6059fveq1d 6651 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → ((𝑥(2nd𝑓)𝑦)‘𝑔) = ((𝑤(2nd)𝑦)‘𝑔))
6160fveq1d 6651 . . . . . . . . . . . . . . . . . . 19 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢) = (((𝑤(2nd)𝑦)‘𝑔)‘𝑢))
6255, 61mpteq12dv 5118 . . . . . . . . . . . . . . . . . 18 (((𝑓 = 𝑥 = 𝑤) ∧ 𝑦𝐵) → (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢)) = (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))
6362mpteq2dva 5128 . . . . . . . . . . . . . . . . 17 ((𝑓 = 𝑥 = 𝑤) → (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢))) = (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢))))
6453, 63mpteq12dv 5118 . . . . . . . . . . . . . . . 16 ((𝑓 = 𝑥 = 𝑤) → (𝑢 ∈ ((1st𝑓)‘𝑥) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢)))) = (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))))
65 fvex 6662 . . . . . . . . . . . . . . . . 17 ((1st)‘𝑤) ∈ V
6665mptex 6967 . . . . . . . . . . . . . . . 16 (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))) ∈ V
6764, 42, 66ovmpoa 7288 . . . . . . . . . . . . . . 15 (( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵) → (𝑁𝑤) = (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))))
6867adantl 485 . . . . . . . . . . . . . 14 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑁𝑤) = (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))))
6968fneq1d 6420 . . . . . . . . . . . . 13 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑁𝑤) Fn ((1st)‘𝑤) ↔ (𝑢 ∈ ((1st)‘𝑤) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd)𝑦)‘𝑔)‘𝑢)))) Fn ((1st)‘𝑤)))
7049, 69mpbiri 261 . . . . . . . . . . . 12 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑁𝑤) Fn ((1st)‘𝑤))
71 dffn5 6703 . . . . . . . . . . . 12 ((𝑁𝑤) Fn ((1st)‘𝑤) ↔ (𝑁𝑤) = (𝑏 ∈ ((1st)‘𝑤) ↦ ((𝑁𝑤)‘𝑏)))
7270, 71sylib 221 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑁𝑤) = (𝑏 ∈ ((1st)‘𝑤) ↦ ((𝑁𝑤)‘𝑏)))
735oppccat 16988 . . . . . . . . . . . . . 14 (𝐶 ∈ Cat → 𝑂 ∈ Cat)
7417, 73syl 17 . . . . . . . . . . . . 13 (𝜑𝑂 ∈ Cat)
7574adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → 𝑂 ∈ Cat)
7620unssbd 4118 . . . . . . . . . . . . . . 15 (𝜑𝑈𝑉)
7718, 76ssexd 5195 . . . . . . . . . . . . . 14 (𝜑𝑈 ∈ V)
7812setccat 17341 . . . . . . . . . . . . . 14 (𝑈 ∈ V → 𝑆 ∈ Cat)
7977, 78syl 17 . . . . . . . . . . . . 13 (𝜑𝑆 ∈ Cat)
8079adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → 𝑆 ∈ Cat)
8115, 75, 80, 7, 32, 33evlf1 17466 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((1st𝐸)𝑤) = ((1st)‘𝑤))
8210, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33yonedalem21 17519 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((1st𝑍)𝑤) = (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
8372, 81, 82feq123d 6480 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑁𝑤):((1st𝐸)𝑤)⟶((1st𝑍)𝑤) ↔ (𝑏 ∈ ((1st)‘𝑤) ↦ ((𝑁𝑤)‘𝑏)):((1st)‘𝑤)⟶(((1st𝑌)‘𝑤)(𝑂 Nat 𝑆))))
8445, 83mpbird 260 . . . . . . . . 9 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑁𝑤):((1st𝐸)𝑤)⟶((1st𝑍)𝑤))
85 fcompt 6876 . . . . . . . . . . 11 (((𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤) ∧ (𝑁𝑤):((1st𝐸)𝑤)⟶((1st𝑍)𝑤)) → ((𝑀𝑤) ∘ (𝑁𝑤)) = (𝑘 ∈ ((1st𝐸)𝑤) ↦ ((𝑀𝑤)‘((𝑁𝑤)‘𝑘))))
8635, 84, 85syl2anc 587 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤) ∘ (𝑁𝑤)) = (𝑘 ∈ ((1st𝐸)𝑤) ↦ ((𝑀𝑤)‘((𝑁𝑤)‘𝑘))))
8781eleq2d 2878 . . . . . . . . . . . . . 14 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑘 ∈ ((1st𝐸)𝑤) ↔ 𝑘 ∈ ((1st)‘𝑤)))
8887biimpa 480 . . . . . . . . . . . . 13 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st𝐸)𝑤)) → 𝑘 ∈ ((1st)‘𝑤))
8928adantr 484 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝐶 ∈ Cat)
9029adantr 484 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝑉𝑊)
9130adantr 484 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ran (Homf𝐶) ⊆ 𝑈)
9231adantr 484 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
93 simplrl 776 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ∈ (𝑂 Func 𝑆))
94 simplrr 777 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝑤𝐵)
9510, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 89, 90, 91, 92, 93, 94, 26yonedalem3a 17520 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑀𝑤) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))) ∧ (𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤)))
9695simpld 498 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (𝑀𝑤) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))))
9796fveq1d 6651 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑀𝑤)‘((𝑁𝑤)‘𝑘)) = ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘((𝑁𝑤)‘𝑘)))
9872, 44fmpt3d 6861 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑁𝑤):((1st)‘𝑤)⟶(((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
9998ffvelrnda 6832 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑁𝑤)‘𝑘) ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
100 fveq1 6648 . . . . . . . . . . . . . . . . 17 (𝑎 = ((𝑁𝑤)‘𝑘) → (𝑎𝑤) = (((𝑁𝑤)‘𝑘)‘𝑤))
101100fveq1d 6651 . . . . . . . . . . . . . . . 16 (𝑎 = ((𝑁𝑤)‘𝑘) → ((𝑎𝑤)‘( 1𝑤)) = ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)))
102 eqid 2801 . . . . . . . . . . . . . . . 16 (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))
103 fvex 6662 . . . . . . . . . . . . . . . 16 ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)) ∈ V
104101, 102, 103fvmpt 6749 . . . . . . . . . . . . . . 15 (((𝑁𝑤)‘𝑘) ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) → ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘((𝑁𝑤)‘𝑘)) = ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)))
10599, 104syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘((𝑁𝑤)‘𝑘)) = ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)))
106 simpr 488 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝑘 ∈ ((1st)‘𝑤))
107 eqid 2801 . . . . . . . . . . . . . . . . 17 (Hom ‘𝐶) = (Hom ‘𝐶)
1086, 107, 11, 89, 94catidcl 16949 . . . . . . . . . . . . . . . 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 17522 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)) = (((𝑤(2nd)𝑤)‘( 1𝑤))‘𝑘))
110 eqid 2801 . . . . . . . . . . . . . . . . . 18 (Id‘𝑂) = (Id‘𝑂)
111 eqid 2801 . . . . . . . . . . . . . . . . . 18 (Id‘𝑆) = (Id‘𝑆)
112 relfunc 17128 . . . . . . . . . . . . . . . . . . 19 Rel (𝑂 Func 𝑆)
113 1st2ndbr 7727 . . . . . . . . . . . . . . . . . . 19 ((Rel (𝑂 Func 𝑆) ∧ ∈ (𝑂 Func 𝑆)) → (1st)(𝑂 Func 𝑆)(2nd))
114112, 93, 113sylancr 590 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (1st)(𝑂 Func 𝑆)(2nd))
1157, 110, 111, 114, 94funcid 17136 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑤(2nd)𝑤)‘((Id‘𝑂)‘𝑤)) = ((Id‘𝑆)‘((1st)‘𝑤)))
1165, 11oppcid 16987 . . . . . . . . . . . . . . . . . . . 20 (𝐶 ∈ Cat → (Id‘𝑂) = 1 )
11789, 116syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (Id‘𝑂) = 1 )
118117fveq1d 6651 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((Id‘𝑂)‘𝑤) = ( 1𝑤))
119118fveq2d 6653 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑤(2nd)𝑤)‘((Id‘𝑂)‘𝑤)) = ((𝑤(2nd)𝑤)‘( 1𝑤)))
12077ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝑈 ∈ V)
121 eqid 2801 . . . . . . . . . . . . . . . . . . . . 21 (Base‘𝑆) = (Base‘𝑆)
1227, 121, 114funcf1 17132 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (1st):𝐵⟶(Base‘𝑆))
12312, 120setcbas 17334 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → 𝑈 = (Base‘𝑆))
124123feq3d 6478 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((1st):𝐵𝑈 ↔ (1st):𝐵⟶(Base‘𝑆)))
125122, 124mpbird 260 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (1st):𝐵𝑈)
126125, 94ffvelrnd 6833 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((1st)‘𝑤) ∈ 𝑈)
12712, 111, 120, 126setcid 17342 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((Id‘𝑆)‘((1st)‘𝑤)) = ( I ↾ ((1st)‘𝑤)))
128115, 119, 1273eqtr3d 2844 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑤(2nd)𝑤)‘( 1𝑤)) = ( I ↾ ((1st)‘𝑤)))
129128fveq1d 6651 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (((𝑤(2nd)𝑤)‘( 1𝑤))‘𝑘) = (( I ↾ ((1st)‘𝑤))‘𝑘))
130 fvresi 6916 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ((1st)‘𝑤) → (( I ↾ ((1st)‘𝑤))‘𝑘) = 𝑘)
131130adantl 485 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → (( I ↾ ((1st)‘𝑤))‘𝑘) = 𝑘)
132109, 129, 1313eqtrd 2840 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((((𝑁𝑤)‘𝑘)‘𝑤)‘( 1𝑤)) = 𝑘)
13397, 105, 1323eqtrd 2840 . . . . . . . . . . . . 13 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st)‘𝑤)) → ((𝑀𝑤)‘((𝑁𝑤)‘𝑘)) = 𝑘)
13488, 133syldan 594 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑘 ∈ ((1st𝐸)𝑤)) → ((𝑀𝑤)‘((𝑁𝑤)‘𝑘)) = 𝑘)
135134mpteq2dva 5128 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑘 ∈ ((1st𝐸)𝑤) ↦ ((𝑀𝑤)‘((𝑁𝑤)‘𝑘))) = (𝑘 ∈ ((1st𝐸)𝑤) ↦ 𝑘))
136 mptresid 5889 . . . . . . . . . . 11 ( I ↾ ((1st𝐸)𝑤)) = (𝑘 ∈ ((1st𝐸)𝑤) ↦ 𝑘)
137135, 136eqtr4di 2854 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑘 ∈ ((1st𝐸)𝑤) ↦ ((𝑀𝑤)‘((𝑁𝑤)‘𝑘))) = ( I ↾ ((1st𝐸)𝑤)))
13886, 137eqtrd 2836 . . . . . . . . 9 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤) ∘ (𝑁𝑤)) = ( I ↾ ((1st𝐸)𝑤)))
139 fcompt 6876 . . . . . . . . . . 11 (((𝑁𝑤):((1st𝐸)𝑤)⟶((1st𝑍)𝑤) ∧ (𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤)) → ((𝑁𝑤) ∘ (𝑀𝑤)) = (𝑏 ∈ ((1st𝑍)𝑤) ↦ ((𝑁𝑤)‘((𝑀𝑤)‘𝑏))))
14084, 35, 139syl2anc 587 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑁𝑤) ∘ (𝑀𝑤)) = (𝑏 ∈ ((1st𝑍)𝑤) ↦ ((𝑁𝑤)‘((𝑀𝑤)‘𝑏))))
141 eqid 2801 . . . . . . . . . . . . . 14 (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆)
14228adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝐶 ∈ Cat)
14329adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑉𝑊)
14430adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ran (Homf𝐶) ⊆ 𝑈)
14531adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
146 simplrl 776 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ∈ (𝑂 Func 𝑆))
147 simplrr 777 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑤𝐵)
14881feq3d 6478 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤) ↔ (𝑀𝑤):((1st𝑍)𝑤)⟶((1st)‘𝑤)))
14935, 148mpbid 235 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑀𝑤):((1st𝑍)𝑤)⟶((1st)‘𝑤))
150149ffvelrnda 6832 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑀𝑤)‘𝑏) ∈ ((1st)‘𝑤))
15110, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 142, 143, 144, 145, 146, 147, 42, 150yonedalem4c 17523 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑁𝑤)‘((𝑀𝑤)‘𝑏)) ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
152141, 151nat1st2nd 17217 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑁𝑤)‘((𝑀𝑤)‘𝑏)) ∈ (⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st), (2nd)⟩))
153141, 152, 7natfn 17220 . . . . . . . . . . . . 13 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑁𝑤)‘((𝑀𝑤)‘𝑏)) Fn 𝐵)
15482eleq2d 2878 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑏 ∈ ((1st𝑍)𝑤) ↔ 𝑏 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆))))
155154biimpa 480 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑏 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
156141, 155nat1st2nd 17217 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑏 ∈ (⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st), (2nd)⟩))
157141, 156, 7natfn 17220 . . . . . . . . . . . . 13 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑏 Fn 𝐵)
158142adantr 484 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → 𝐶 ∈ Cat)
159147adantr 484 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → 𝑤𝐵)
160 simpr 488 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → 𝑧𝐵)
16110, 6, 158, 159, 107, 160yon11 17510 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((1st ‘((1st𝑌)‘𝑤))‘𝑧) = (𝑧(Hom ‘𝐶)𝑤))
162161eleq2d 2878 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ↔ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))
163162biimpa 480 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧)) → 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤))
164158adantr 484 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝐶 ∈ Cat)
165143ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑉𝑊)
166144ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ran (Homf𝐶) ⊆ 𝑈)
167145ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
168146ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ∈ (𝑂 Func 𝑆))
169159adantr 484 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑤𝐵)
170150ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑀𝑤)‘𝑏) ∈ ((1st)‘𝑤))
171 simplr 768 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑧𝐵)
172 simpr 488 . . . . . . . . . . . . . . . . . 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 17522 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑀𝑤)‘𝑏)))
17410, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 164, 165, 166, 167, 168, 169, 26yonedalem3a 17520 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑀𝑤) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))) ∧ (𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤)))
175174simpld 498 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑀𝑤) = (𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤))))
176175fveq1d 6651 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑀𝑤)‘𝑏) = ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘𝑏))
177155ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑏 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)))
178 fveq1 6648 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 𝑏 → (𝑎𝑤) = (𝑏𝑤))
179178fveq1d 6651 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑏 → ((𝑎𝑤)‘( 1𝑤)) = ((𝑏𝑤)‘( 1𝑤)))
180 fvex 6662 . . . . . . . . . . . . . . . . . . . . 21 ((𝑏𝑤)‘( 1𝑤)) ∈ V
181179, 102, 180fvmpt 6749 . . . . . . . . . . . . . . . . . . . 20 (𝑏 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) → ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘𝑏) = ((𝑏𝑤)‘( 1𝑤)))
182177, 181syl 17 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑎 ∈ (((1st𝑌)‘𝑤)(𝑂 Nat 𝑆)) ↦ ((𝑎𝑤)‘( 1𝑤)))‘𝑏) = ((𝑏𝑤)‘( 1𝑤)))
183176, 182eqtrd 2836 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑀𝑤)‘𝑏) = ((𝑏𝑤)‘( 1𝑤)))
184183fveq2d 6653 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd)𝑧)‘𝑘)‘((𝑀𝑤)‘𝑏)) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))))
185156ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑏 ∈ (⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st), (2nd)⟩))
186 eqid 2801 . . . . . . . . . . . . . . . . . . . . . 22 (Hom ‘𝑂) = (Hom ‘𝑂)
187 eqid 2801 . . . . . . . . . . . . . . . . . . . . . 22 (comp‘𝑆) = (comp‘𝑆)
188107, 5oppchom 16981 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤(Hom ‘𝑂)𝑧) = (𝑧(Hom ‘𝐶)𝑤)
189172, 188eleqtrrdi 2904 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑘 ∈ (𝑤(Hom ‘𝑂)𝑧))
190141, 185, 7, 186, 187, 169, 171, 189nati 17221 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏𝑧)(⟨((1st ‘((1st𝑌)‘𝑤))‘𝑤), ((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟩(comp‘𝑆)((1st)‘𝑧))((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)) = (((𝑤(2nd)𝑧)‘𝑘)(⟨((1st ‘((1st𝑌)‘𝑤))‘𝑤), ((1st)‘𝑤)⟩(comp‘𝑆)((1st)‘𝑧))(𝑏𝑤)))
19177ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑈 ∈ V)
192191adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → 𝑈 ∈ V)
193192adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑈 ∈ V)
194 relfunc 17128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Rel (𝐶 Func 𝑄)
19510, 17, 5, 12, 3, 77, 19yoncl 17508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝜑𝑌 ∈ (𝐶 Func 𝑄))
196 1st2ndbr 7727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((Rel (𝐶 Func 𝑄) ∧ 𝑌 ∈ (𝐶 Func 𝑄)) → (1st𝑌)(𝐶 Func 𝑄)(2nd𝑌))
197194, 195, 196sylancr 590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (1st𝑌)(𝐶 Func 𝑄)(2nd𝑌))
1986, 4, 197funcf1 17132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (1st𝑌):𝐵⟶(𝑂 Func 𝑆))
199198ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st𝑌):𝐵⟶(𝑂 Func 𝑆))
200199, 147ffvelrnd 6833 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st𝑌)‘𝑤) ∈ (𝑂 Func 𝑆))
201 1st2ndbr 7727 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((Rel (𝑂 Func 𝑆) ∧ ((1st𝑌)‘𝑤) ∈ (𝑂 Func 𝑆)) → (1st ‘((1st𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st𝑌)‘𝑤)))
202112, 200, 201sylancr 590 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st ‘((1st𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st𝑌)‘𝑤)))
2037, 121, 202funcf1 17132 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st ‘((1st𝑌)‘𝑤)):𝐵⟶(Base‘𝑆))
20412, 191setcbas 17334 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → 𝑈 = (Base‘𝑆))
205204feq3d 6478 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st ‘((1st𝑌)‘𝑤)):𝐵𝑈 ↔ (1st ‘((1st𝑌)‘𝑤)):𝐵⟶(Base‘𝑆)))
206203, 205mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st ‘((1st𝑌)‘𝑤)):𝐵𝑈)
207206, 147ffvelrnd 6833 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st ‘((1st𝑌)‘𝑤))‘𝑤) ∈ 𝑈)
208207ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘((1st𝑌)‘𝑤))‘𝑤) ∈ 𝑈)
209206ffvelrnda 6832 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ∈ 𝑈)
210209adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ∈ 𝑈)
211112, 146, 113sylancr 590 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st)(𝑂 Func 𝑆)(2nd))
2127, 121, 211funcf1 17132 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st):𝐵⟶(Base‘𝑆))
213204feq3d 6478 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st):𝐵𝑈 ↔ (1st):𝐵⟶(Base‘𝑆)))
214212, 213mpbird 260 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (1st):𝐵𝑈)
215214ffvelrnda 6832 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((1st)‘𝑧) ∈ 𝑈)
216215adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st)‘𝑧) ∈ 𝑈)
217 eqid 2801 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Hom ‘𝑆) = (Hom ‘𝑆)
218202ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1st ‘((1st𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st𝑌)‘𝑤)))
2197, 186, 217, 218, 169, 171funcf2 17134 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧):(𝑤(Hom ‘𝑂)𝑧)⟶(((1st ‘((1st𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑤))‘𝑧)))
220219, 189ffvelrnd 6833 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑤))‘𝑧)))
22112, 193, 217, 208, 210elsetchom 17337 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑤))‘𝑧)) ↔ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st ‘((1st𝑌)‘𝑤))‘𝑧)))
222220, 221mpbid 235 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st ‘((1st𝑌)‘𝑤))‘𝑧))
223156adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → 𝑏 ∈ (⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st), (2nd)⟩))
224141, 223, 7, 217, 160natcl 17219 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (𝑏𝑧) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st)‘𝑧)))
22512, 192, 217, 209, 215elsetchom 17337 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((𝑏𝑧) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st)‘𝑧)) ↔ (𝑏𝑧):((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟶((1st)‘𝑧)))
226224, 225mpbid 235 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (𝑏𝑧):((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟶((1st)‘𝑧))
227226adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑏𝑧):((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟶((1st)‘𝑧))
22812, 193, 187, 208, 210, 216, 222, 227setcco 17339 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏𝑧)(⟨((1st ‘((1st𝑌)‘𝑤))‘𝑤), ((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟩(comp‘𝑆)((1st)‘𝑧))((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)) = ((𝑏𝑧) ∘ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)))
229214, 147ffvelrnd 6833 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st)‘𝑤) ∈ 𝑈)
230229ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st)‘𝑤) ∈ 𝑈)
231141, 156, 7, 217, 147natcl 17219 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (𝑏𝑤) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st)‘𝑤)))
23212, 191, 217, 207, 229elsetchom 17337 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑏𝑤) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st)‘𝑤)) ↔ (𝑏𝑤):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st)‘𝑤)))
233231, 232mpbid 235 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → (𝑏𝑤):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st)‘𝑤))
234233ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑏𝑤):((1st ‘((1st𝑌)‘𝑤))‘𝑤)⟶((1st)‘𝑤))
235112, 168, 113sylancr 590 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1st)(𝑂 Func 𝑆)(2nd))
2367, 186, 217, 235, 169, 171funcf2 17134 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑤(2nd)𝑧):(𝑤(Hom ‘𝑂)𝑧)⟶(((1st)‘𝑤)(Hom ‘𝑆)((1st)‘𝑧)))
237236, 189ffvelrnd 6833 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd)𝑧)‘𝑘) ∈ (((1st)‘𝑤)(Hom ‘𝑆)((1st)‘𝑧)))
23812, 193, 217, 230, 216elsetchom 17337 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd)𝑧)‘𝑘) ∈ (((1st)‘𝑤)(Hom ‘𝑆)((1st)‘𝑧)) ↔ ((𝑤(2nd)𝑧)‘𝑘):((1st)‘𝑤)⟶((1st)‘𝑧)))
239237, 238mpbid 235 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd)𝑧)‘𝑘):((1st)‘𝑤)⟶((1st)‘𝑧))
24012, 193, 187, 208, 230, 216, 234, 239setcco 17339 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd)𝑧)‘𝑘)(⟨((1st ‘((1st𝑌)‘𝑤))‘𝑤), ((1st)‘𝑤)⟩(comp‘𝑆)((1st)‘𝑧))(𝑏𝑤)) = (((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤)))
241190, 228, 2403eqtr3d 2844 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏𝑧) ∘ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)) = (((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤)))
242241fveq1d 6651 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑏𝑧) ∘ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘))‘( 1𝑤)) = ((((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤))‘( 1𝑤)))
2436, 107, 11, 142, 147catidcl 16949 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ( 1𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤))
24410, 6, 142, 147, 107, 147yon11 17510 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((1st ‘((1st𝑌)‘𝑤))‘𝑤) = (𝑤(Hom ‘𝐶)𝑤))
245243, 244eleqtrrd 2896 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ( 1𝑤) ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑤))
246245ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ( 1𝑤) ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑤))
247222, 246fvco3d 6742 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑏𝑧) ∘ ((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘))‘( 1𝑤)) = ((𝑏𝑧)‘(((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤))))
248233, 245fvco3d 6742 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤))‘( 1𝑤)) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))))
249248ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((𝑤(2nd)𝑧)‘𝑘) ∘ (𝑏𝑤))‘( 1𝑤)) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))))
250242, 247, 2493eqtr3d 2844 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏𝑧)‘(((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤))) = (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))))
251 eqid 2801 . . . . . . . . . . . . . . . . . . . . 21 (comp‘𝐶) = (comp‘𝐶)
252243ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ( 1𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤))
25310, 6, 164, 169, 107, 169, 251, 171, 172, 252yon12 17511 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤)) = (( 1𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐶)𝑤)𝑘))
2546, 107, 11, 164, 171, 251, 169, 172catlid 16950 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (( 1𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐶)𝑤)𝑘) = 𝑘)
255253, 254eqtrd 2836 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤)) = 𝑘)
256255fveq2d 6653 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏𝑧)‘(((𝑤(2nd ‘((1st𝑌)‘𝑤))𝑧)‘𝑘)‘( 1𝑤))) = ((𝑏𝑧)‘𝑘))
257250, 256eqtr3d 2838 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd)𝑧)‘𝑘)‘((𝑏𝑤)‘( 1𝑤))) = ((𝑏𝑧)‘𝑘))
258173, 184, 2573eqtrd 2840 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = ((𝑏𝑧)‘𝑘))
259163, 258syldan 594 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) ∧ 𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧)) → ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = ((𝑏𝑧)‘𝑘))
260259mpteq2dva 5128 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ↦ ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧)‘𝑘)) = (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ↦ ((𝑏𝑧)‘𝑘)))
261152adantr 484 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((𝑁𝑤)‘((𝑀𝑤)‘𝑏)) ∈ (⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st), (2nd)⟩))
262141, 261, 7, 217, 160natcl 17219 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st)‘𝑧)))
26312, 192, 217, 209, 215elsetchom 17337 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧) ∈ (((1st ‘((1st𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st)‘𝑧)) ↔ (((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧):((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟶((1st)‘𝑧)))
264262, 263mpbid 235 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧):((1st ‘((1st𝑌)‘𝑤))‘𝑧)⟶((1st)‘𝑧))
265264feqmptd 6712 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧) = (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ↦ ((((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧)‘𝑘)))
266226feqmptd 6712 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (𝑏𝑧) = (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ↦ ((𝑏𝑧)‘𝑘)))
267260, 265, 2663eqtr4d 2846 . . . . . . . . . . . . 13 ((((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) ∧ 𝑧𝐵) → (((𝑁𝑤)‘((𝑀𝑤)‘𝑏))‘𝑧) = (𝑏𝑧))
268153, 157, 267eqfnfvd 6786 . . . . . . . . . . . 12 (((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) ∧ 𝑏 ∈ ((1st𝑍)𝑤)) → ((𝑁𝑤)‘((𝑀𝑤)‘𝑏)) = 𝑏)
269268mpteq2dva 5128 . . . . . . . . . . 11 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑏 ∈ ((1st𝑍)𝑤) ↦ ((𝑁𝑤)‘((𝑀𝑤)‘𝑏))) = (𝑏 ∈ ((1st𝑍)𝑤) ↦ 𝑏))
270 mptresid 5889 . . . . . . . . . . 11 ( I ↾ ((1st𝑍)𝑤)) = (𝑏 ∈ ((1st𝑍)𝑤) ↦ 𝑏)
271269, 270eqtr4di 2854 . . . . . . . . . 10 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑏 ∈ ((1st𝑍)𝑤) ↦ ((𝑁𝑤)‘((𝑀𝑤)‘𝑏))) = ( I ↾ ((1st𝑍)𝑤)))
272140, 271eqtrd 2836 . . . . . . . . 9 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑁𝑤) ∘ (𝑀𝑤)) = ( I ↾ ((1st𝑍)𝑤)))
273 fcof1o 7034 . . . . . . . . 9 ((((𝑀𝑤):((1st𝑍)𝑤)⟶((1st𝐸)𝑤) ∧ (𝑁𝑤):((1st𝐸)𝑤)⟶((1st𝑍)𝑤)) ∧ (((𝑀𝑤) ∘ (𝑁𝑤)) = ( I ↾ ((1st𝐸)𝑤)) ∧ ((𝑁𝑤) ∘ (𝑀𝑤)) = ( I ↾ ((1st𝑍)𝑤)))) → ((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑀𝑤) = (𝑁𝑤)))
27435, 84, 138, 272, 273syl22anc 837 . . . . . . . 8 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑀𝑤) = (𝑁𝑤)))
275 eqcom 2808 . . . . . . . . 9 ((𝑀𝑤) = (𝑁𝑤) ↔ (𝑁𝑤) = (𝑀𝑤))
276275anbi2i 625 . . . . . . . 8 (((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑀𝑤) = (𝑁𝑤)) ↔ ((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑁𝑤) = (𝑀𝑤)))
277274, 276sylib 221 . . . . . . 7 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑁𝑤) = (𝑀𝑤)))
278 eqid 2801 . . . . . . . . . . 11 (Base‘𝑇) = (Base‘𝑇)
279 relfunc 17128 . . . . . . . . . . . 12 Rel ((𝑄 ×c 𝑂) Func 𝑇)
280 1st2ndbr 7727 . . . . . . . . . . . 12 ((Rel ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st𝑍)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝑍))
281279, 22, 280sylancr 590 . . . . . . . . . . 11 (𝜑 → (1st𝑍)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝑍))
2828, 278, 281funcf1 17132 . . . . . . . . . 10 (𝜑 → (1st𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
28313, 18setcbas 17334 . . . . . . . . . . 11 (𝜑𝑉 = (Base‘𝑇))
284283feq3d 6478 . . . . . . . . . 10 (𝜑 → ((1st𝑍):((𝑂 Func 𝑆) × 𝐵)⟶𝑉 ↔ (1st𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇)))
285282, 284mpbird 260 . . . . . . . . 9 (𝜑 → (1st𝑍):((𝑂 Func 𝑆) × 𝐵)⟶𝑉)
286285fovrnda 7303 . . . . . . . 8 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((1st𝑍)𝑤) ∈ 𝑉)
287 1st2ndbr 7727 . . . . . . . . . . . 12 ((Rel ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st𝐸)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝐸))
288279, 23, 287sylancr 590 . . . . . . . . . . 11 (𝜑 → (1st𝐸)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝐸))
2898, 278, 288funcf1 17132 . . . . . . . . . 10 (𝜑 → (1st𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
290283feq3d 6478 . . . . . . . . . 10 (𝜑 → ((1st𝐸):((𝑂 Func 𝑆) × 𝐵)⟶𝑉 ↔ (1st𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇)))
291289, 290mpbird 260 . . . . . . . . 9 (𝜑 → (1st𝐸):((𝑂 Func 𝑆) × 𝐵)⟶𝑉)
292291fovrnda 7303 . . . . . . . 8 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((1st𝐸)𝑤) ∈ 𝑉)
29313, 29, 286, 292, 25setcinv 17346 . . . . . . 7 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → ((𝑀𝑤)(((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤))(𝑁𝑤) ↔ ((𝑀𝑤):((1st𝑍)𝑤)–1-1-onto→((1st𝐸)𝑤) ∧ (𝑁𝑤) = (𝑀𝑤))))
294277, 293mpbird 260 . . . . . 6 ((𝜑 ∧ ( ∈ (𝑂 Func 𝑆) ∧ 𝑤𝐵)) → (𝑀𝑤)(((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤))(𝑁𝑤))
295294ralrimivva 3159 . . . . 5 (𝜑 → ∀ ∈ (𝑂 Func 𝑆)∀𝑤𝐵 (𝑀𝑤)(((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤))(𝑁𝑤))
296 fveq2 6649 . . . . . . . 8 (𝑧 = ⟨, 𝑤⟩ → (𝑀𝑧) = (𝑀‘⟨, 𝑤⟩))
297 df-ov 7142 . . . . . . . 8 (𝑀𝑤) = (𝑀‘⟨, 𝑤⟩)
298296, 297eqtr4di 2854 . . . . . . 7 (𝑧 = ⟨, 𝑤⟩ → (𝑀𝑧) = (𝑀𝑤))
299 fveq2 6649 . . . . . . . . 9 (𝑧 = ⟨, 𝑤⟩ → ((1st𝑍)‘𝑧) = ((1st𝑍)‘⟨, 𝑤⟩))
300 df-ov 7142 . . . . . . . . 9 ((1st𝑍)𝑤) = ((1st𝑍)‘⟨, 𝑤⟩)
301299, 300eqtr4di 2854 . . . . . . . 8 (𝑧 = ⟨, 𝑤⟩ → ((1st𝑍)‘𝑧) = ((1st𝑍)𝑤))
302 fveq2 6649 . . . . . . . . 9 (𝑧 = ⟨, 𝑤⟩ → ((1st𝐸)‘𝑧) = ((1st𝐸)‘⟨, 𝑤⟩))
303 df-ov 7142 . . . . . . . . 9 ((1st𝐸)𝑤) = ((1st𝐸)‘⟨, 𝑤⟩)
304302, 303eqtr4di 2854 . . . . . . . 8 (𝑧 = ⟨, 𝑤⟩ → ((1st𝐸)‘𝑧) = ((1st𝐸)𝑤))
305301, 304oveq12d 7157 . . . . . . 7 (𝑧 = ⟨, 𝑤⟩ → (((1st𝑍)‘𝑧)(Inv‘𝑇)((1st𝐸)‘𝑧)) = (((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤)))
306 fveq2 6649 . . . . . . . 8 (𝑧 = ⟨, 𝑤⟩ → (𝑁𝑧) = (𝑁‘⟨, 𝑤⟩))
307 df-ov 7142 . . . . . . . 8 (𝑁𝑤) = (𝑁‘⟨, 𝑤⟩)
308306, 307eqtr4di 2854 . . . . . . 7 (𝑧 = ⟨, 𝑤⟩ → (𝑁𝑧) = (𝑁𝑤))
309298, 305, 308breq123d 5047 . . . . . 6 (𝑧 = ⟨, 𝑤⟩ → ((𝑀𝑧)(((1st𝑍)‘𝑧)(Inv‘𝑇)((1st𝐸)‘𝑧))(𝑁𝑧) ↔ (𝑀𝑤)(((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤))(𝑁𝑤)))
310309ralxp 5680 . . . . 5 (∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑀𝑧)(((1st𝑍)‘𝑧)(Inv‘𝑇)((1st𝐸)‘𝑧))(𝑁𝑧) ↔ ∀ ∈ (𝑂 Func 𝑆)∀𝑤𝐵 (𝑀𝑤)(((1st𝑍)𝑤)(Inv‘𝑇)((1st𝐸)𝑤))(𝑁𝑤))
311295, 310sylibr 237 . . . 4 (𝜑 → ∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑀𝑧)(((1st𝑍)‘𝑧)(Inv‘𝑇)((1st𝐸)‘𝑧))(𝑁𝑧))
312311r19.21bi 3176 . . 3 ((𝜑𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)) → (𝑀𝑧)(((1st𝑍)‘𝑧)(Inv‘𝑇)((1st𝐸)‘𝑧))(𝑁𝑧))
3131, 8, 9, 22, 23, 24, 25, 27, 312invfuc 17240 . 2 (𝜑𝑀(𝑍𝐼𝐸)(𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁𝑧)))
314 fvex 6662 . . . . 5 ((1st𝑓)‘𝑥) ∈ V
315314mptex 6967 . . . 4 (𝑢 ∈ ((1st𝑓)‘𝑥) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢)))) ∈ V
31642, 315fnmpoi 7754 . . 3 𝑁 Fn ((𝑂 Func 𝑆) × 𝐵)
317 dffn5 6703 . . 3 (𝑁 Fn ((𝑂 Func 𝑆) × 𝐵) ↔ 𝑁 = (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁𝑧)))
318316, 317mpbi 233 . 2 𝑁 = (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁𝑧))
319313, 318breqtrrdi 5075 1 (𝜑𝑀(𝑍𝐼𝐸)𝑁)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2112  ∀wral 3109  Vcvv 3444   ∪ cun 3882   ⊆ wss 3884  ⟨cop 4534   class class class wbr 5033   ↦ cmpt 5113   I cid 5427   × cxp 5521  ◡ccnv 5522  ran crn 5524   ↾ cres 5525   ∘ ccom 5527  Rel wrel 5528   Fn wfn 6323  ⟶wf 6324  –1-1-onto→wf1o 6327  ‘cfv 6328  (class class class)co 7139   ∈ cmpo 7141  1st c1st 7673  2nd c2nd 7674  tpos ctpos 7878  Basecbs 16479  Hom chom 16572  compcco 16573  Catccat 16931  Idccid 16932  Homf chomf 16933  oppCatcoppc 16977  Invcinv 17011   Func cfunc 17120   ∘func ccofu 17122   Nat cnat 17207   FuncCat cfuc 17208  SetCatcsetc 17331   ×c cxpc 17414   1stF c1stf 17415   2ndF c2ndf 17416   ⟨,⟩F cprf 17417   evalF cevlf 17455  HomFchof 17494  Yoncyon 17495 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-1st 7675  df-2nd 7676  df-tpos 7879  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-oadd 8093  df-er 8276  df-map 8395  df-pm 8396  df-ixp 8449  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-nn 11630  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-fz 12890  df-struct 16481  df-ndx 16482  df-slot 16483  df-base 16485  df-sets 16486  df-ress 16487  df-hom 16585  df-cco 16586  df-cat 16935  df-cid 16936  df-homf 16937  df-comf 16938  df-oppc 16978  df-sect 17013  df-inv 17014  df-ssc 17076  df-resc 17077  df-subc 17078  df-func 17124  df-cofu 17126  df-nat 17209  df-fuc 17210  df-setc 17332  df-xpc 17418  df-1stf 17419  df-2ndf 17420  df-prf 17421  df-evlf 17459  df-curf 17460  df-hof 17496  df-yon 17497 This theorem is referenced by:  yonffthlem  17528  yoneda  17529
 Copyright terms: Public domain W3C validator