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

Theorem yonedalem3b 18324
Description: Lemma for yoneda 18328. (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𝑄) ∪ 𝑈) ⊆ 𝑉)
yonedalem21.f (𝜑𝐹 ∈ (𝑂 Func 𝑆))
yonedalem21.x (𝜑𝑋𝐵)
yonedalem22.g (𝜑𝐺 ∈ (𝑂 Func 𝑆))
yonedalem22.p (𝜑𝑃𝐵)
yonedalem22.a (𝜑𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺))
yonedalem22.k (𝜑𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋))
yonedalem3.m 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥𝐵 ↦ (𝑎 ∈ (((1st𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎𝑥)‘( 1𝑥))))
Assertion
Ref Expression
yonedalem3b (𝜑 → ((𝐺𝑀𝑃)(⟨(𝐹(1st𝑍)𝑋), (𝐺(1st𝑍)𝑃)⟩(comp‘𝑇)(𝐺(1st𝐸)𝑃))(𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾)) = ((𝐴(⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)𝐾)(⟨(𝐹(1st𝑍)𝑋), (𝐹(1st𝐸)𝑋)⟩(comp‘𝑇)(𝐺(1st𝐸)𝑃))(𝐹𝑀𝑋)))
Distinct variable groups:   𝑓,𝑎,𝑥, 1   𝐴,𝑎   𝐶,𝑎,𝑓,𝑥   𝐸,𝑎,𝑓   𝐹,𝑎,𝑓,𝑥   𝐾,𝑎   𝐵,𝑎,𝑓,𝑥   𝐺,𝑎,𝑓,𝑥   𝑂,𝑎,𝑓,𝑥   𝑆,𝑎,𝑓,𝑥   𝑄,𝑎,𝑓,𝑥   𝑇,𝑓   𝑃,𝑎,𝑓,𝑥   𝜑,𝑎,𝑓,𝑥   𝑌,𝑎,𝑓,𝑥   𝑍,𝑎,𝑓,𝑥   𝑋,𝑎,𝑓,𝑥
Allowed substitution hints:   𝐴(𝑥,𝑓)   𝑅(𝑥,𝑓,𝑎)   𝑇(𝑥,𝑎)   𝑈(𝑥,𝑓,𝑎)   𝐸(𝑥)   𝐻(𝑥,𝑓,𝑎)   𝐾(𝑥,𝑓)   𝑀(𝑥,𝑓,𝑎)   𝑉(𝑥,𝑓,𝑎)   𝑊(𝑥,𝑓,𝑎)

Proof of Theorem yonedalem3b
Dummy variables 𝑏 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 7439 . . . . . . . 8 (𝑏 = 𝑎 → (𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏) = (𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎))
21oveq1d 7446 . . . . . . 7 (𝑏 = 𝑎 → ((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾)) = ((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾)))
32fveq1d 6908 . . . . . 6 (𝑏 = 𝑎 → (((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃) = (((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃))
43fveq1d 6908 . . . . 5 (𝑏 = 𝑎 → ((((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃)‘( 1𝑃)) = ((((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃)‘( 1𝑃)))
54cbvmptv 5255 . . . 4 (𝑏 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃)‘( 1𝑃))) = (𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃)‘( 1𝑃)))
6 yoneda.q . . . . . . . . 9 𝑄 = (𝑂 FuncCat 𝑆)
7 eqid 2737 . . . . . . . . 9 (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆)
8 yoneda.o . . . . . . . . . 10 𝑂 = (oppCat‘𝐶)
9 yoneda.b . . . . . . . . . 10 𝐵 = (Base‘𝐶)
108, 9oppcbas 17761 . . . . . . . . 9 𝐵 = (Base‘𝑂)
11 eqid 2737 . . . . . . . . 9 (comp‘𝑆) = (comp‘𝑆)
12 eqid 2737 . . . . . . . . 9 (comp‘𝑄) = (comp‘𝑄)
13 eqid 2737 . . . . . . . . . . . 12 (Hom ‘𝐶) = (Hom ‘𝐶)
146, 7fuchom 18009 . . . . . . . . . . . 12 (𝑂 Nat 𝑆) = (Hom ‘𝑄)
15 relfunc 17907 . . . . . . . . . . . . 13 Rel (𝐶 Func 𝑄)
16 yoneda.y . . . . . . . . . . . . . 14 𝑌 = (Yon‘𝐶)
17 yoneda.c . . . . . . . . . . . . . 14 (𝜑𝐶 ∈ Cat)
18 yoneda.s . . . . . . . . . . . . . 14 𝑆 = (SetCat‘𝑈)
19 yoneda.w . . . . . . . . . . . . . . 15 (𝜑𝑉𝑊)
20 yoneda.v . . . . . . . . . . . . . . . 16 (𝜑 → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
2120unssbd 4194 . . . . . . . . . . . . . . 15 (𝜑𝑈𝑉)
2219, 21ssexd 5324 . . . . . . . . . . . . . 14 (𝜑𝑈 ∈ V)
23 yoneda.u . . . . . . . . . . . . . 14 (𝜑 → ran (Homf𝐶) ⊆ 𝑈)
2416, 17, 8, 18, 6, 22, 23yoncl 18307 . . . . . . . . . . . . 13 (𝜑𝑌 ∈ (𝐶 Func 𝑄))
25 1st2ndbr 8067 . . . . . . . . . . . . 13 ((Rel (𝐶 Func 𝑄) ∧ 𝑌 ∈ (𝐶 Func 𝑄)) → (1st𝑌)(𝐶 Func 𝑄)(2nd𝑌))
2615, 24, 25sylancr 587 . . . . . . . . . . . 12 (𝜑 → (1st𝑌)(𝐶 Func 𝑄)(2nd𝑌))
27 yonedalem22.p . . . . . . . . . . . 12 (𝜑𝑃𝐵)
28 yonedalem21.x . . . . . . . . . . . 12 (𝜑𝑋𝐵)
299, 13, 14, 26, 27, 28funcf2 17913 . . . . . . . . . . 11 (𝜑 → (𝑃(2nd𝑌)𝑋):(𝑃(Hom ‘𝐶)𝑋)⟶(((1st𝑌)‘𝑃)(𝑂 Nat 𝑆)((1st𝑌)‘𝑋)))
30 yonedalem22.k . . . . . . . . . . 11 (𝜑𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋))
3129, 30ffvelcdmd 7105 . . . . . . . . . 10 (𝜑 → ((𝑃(2nd𝑌)𝑋)‘𝐾) ∈ (((1st𝑌)‘𝑃)(𝑂 Nat 𝑆)((1st𝑌)‘𝑋)))
3231adantr 480 . . . . . . . . 9 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑃(2nd𝑌)𝑋)‘𝐾) ∈ (((1st𝑌)‘𝑃)(𝑂 Nat 𝑆)((1st𝑌)‘𝑋)))
33 simpr 484 . . . . . . . . . 10 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹))
34 yonedalem22.a . . . . . . . . . . 11 (𝜑𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺))
3534adantr 480 . . . . . . . . . 10 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺))
366, 7, 12, 33, 35fuccocl 18012 . . . . . . . . 9 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎) ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐺))
3727adantr 480 . . . . . . . . 9 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑃𝐵)
386, 7, 10, 11, 12, 32, 36, 37fuccoval 18011 . . . . . . . 8 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃) = (((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)‘𝑃)(⟨((1st ‘((1st𝑌)‘𝑃))‘𝑃), ((1st ‘((1st𝑌)‘𝑋))‘𝑃)⟩(comp‘𝑆)((1st𝐺)‘𝑃))(((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)))
396, 7, 10, 11, 12, 33, 35, 37fuccoval 18011 . . . . . . . . . 10 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)‘𝑃) = ((𝐴𝑃)(⟨((1st ‘((1st𝑌)‘𝑋))‘𝑃), ((1st𝐹)‘𝑃)⟩(comp‘𝑆)((1st𝐺)‘𝑃))(𝑎𝑃)))
4022adantr 480 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑈 ∈ V)
41 eqid 2737 . . . . . . . . . . . . . . 15 (Base‘𝑆) = (Base‘𝑆)
42 relfunc 17907 . . . . . . . . . . . . . . . 16 Rel (𝑂 Func 𝑆)
436fucbas 18008 . . . . . . . . . . . . . . . . . 18 (𝑂 Func 𝑆) = (Base‘𝑄)
449, 43, 26funcf1 17911 . . . . . . . . . . . . . . . . 17 (𝜑 → (1st𝑌):𝐵⟶(𝑂 Func 𝑆))
4544, 28ffvelcdmd 7105 . . . . . . . . . . . . . . . 16 (𝜑 → ((1st𝑌)‘𝑋) ∈ (𝑂 Func 𝑆))
46 1st2ndbr 8067 . . . . . . . . . . . . . . . 16 ((Rel (𝑂 Func 𝑆) ∧ ((1st𝑌)‘𝑋) ∈ (𝑂 Func 𝑆)) → (1st ‘((1st𝑌)‘𝑋))(𝑂 Func 𝑆)(2nd ‘((1st𝑌)‘𝑋)))
4742, 45, 46sylancr 587 . . . . . . . . . . . . . . 15 (𝜑 → (1st ‘((1st𝑌)‘𝑋))(𝑂 Func 𝑆)(2nd ‘((1st𝑌)‘𝑋)))
4810, 41, 47funcf1 17911 . . . . . . . . . . . . . 14 (𝜑 → (1st ‘((1st𝑌)‘𝑋)):𝐵⟶(Base‘𝑆))
4918, 22setcbas 18123 . . . . . . . . . . . . . . 15 (𝜑𝑈 = (Base‘𝑆))
5049feq3d 6723 . . . . . . . . . . . . . 14 (𝜑 → ((1st ‘((1st𝑌)‘𝑋)):𝐵𝑈 ↔ (1st ‘((1st𝑌)‘𝑋)):𝐵⟶(Base‘𝑆)))
5148, 50mpbird 257 . . . . . . . . . . . . 13 (𝜑 → (1st ‘((1st𝑌)‘𝑋)):𝐵𝑈)
5251, 27ffvelcdmd 7105 . . . . . . . . . . . 12 (𝜑 → ((1st ‘((1st𝑌)‘𝑋))‘𝑃) ∈ 𝑈)
5352adantr 480 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1st ‘((1st𝑌)‘𝑋))‘𝑃) ∈ 𝑈)
54 yonedalem21.f . . . . . . . . . . . . . . . 16 (𝜑𝐹 ∈ (𝑂 Func 𝑆))
55 1st2ndbr 8067 . . . . . . . . . . . . . . . 16 ((Rel (𝑂 Func 𝑆) ∧ 𝐹 ∈ (𝑂 Func 𝑆)) → (1st𝐹)(𝑂 Func 𝑆)(2nd𝐹))
5642, 54, 55sylancr 587 . . . . . . . . . . . . . . 15 (𝜑 → (1st𝐹)(𝑂 Func 𝑆)(2nd𝐹))
5710, 41, 56funcf1 17911 . . . . . . . . . . . . . 14 (𝜑 → (1st𝐹):𝐵⟶(Base‘𝑆))
5849feq3d 6723 . . . . . . . . . . . . . 14 (𝜑 → ((1st𝐹):𝐵𝑈 ↔ (1st𝐹):𝐵⟶(Base‘𝑆)))
5957, 58mpbird 257 . . . . . . . . . . . . 13 (𝜑 → (1st𝐹):𝐵𝑈)
6059, 27ffvelcdmd 7105 . . . . . . . . . . . 12 (𝜑 → ((1st𝐹)‘𝑃) ∈ 𝑈)
6160adantr 480 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1st𝐹)‘𝑃) ∈ 𝑈)
62 yonedalem22.g . . . . . . . . . . . . . . . 16 (𝜑𝐺 ∈ (𝑂 Func 𝑆))
63 1st2ndbr 8067 . . . . . . . . . . . . . . . 16 ((Rel (𝑂 Func 𝑆) ∧ 𝐺 ∈ (𝑂 Func 𝑆)) → (1st𝐺)(𝑂 Func 𝑆)(2nd𝐺))
6442, 62, 63sylancr 587 . . . . . . . . . . . . . . 15 (𝜑 → (1st𝐺)(𝑂 Func 𝑆)(2nd𝐺))
6510, 41, 64funcf1 17911 . . . . . . . . . . . . . 14 (𝜑 → (1st𝐺):𝐵⟶(Base‘𝑆))
6665, 27ffvelcdmd 7105 . . . . . . . . . . . . 13 (𝜑 → ((1st𝐺)‘𝑃) ∈ (Base‘𝑆))
6766, 49eleqtrrd 2844 . . . . . . . . . . . 12 (𝜑 → ((1st𝐺)‘𝑃) ∈ 𝑈)
6867adantr 480 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1st𝐺)‘𝑃) ∈ 𝑈)
697, 33nat1st2nd 17999 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑎 ∈ (⟨(1st ‘((1st𝑌)‘𝑋)), (2nd ‘((1st𝑌)‘𝑋))⟩(𝑂 Nat 𝑆)⟨(1st𝐹), (2nd𝐹)⟩))
70 eqid 2737 . . . . . . . . . . . . 13 (Hom ‘𝑆) = (Hom ‘𝑆)
717, 69, 10, 70, 37natcl 18001 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝑎𝑃) ∈ (((1st ‘((1st𝑌)‘𝑋))‘𝑃)(Hom ‘𝑆)((1st𝐹)‘𝑃)))
7218, 40, 70, 53, 61elsetchom 18126 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎𝑃) ∈ (((1st ‘((1st𝑌)‘𝑋))‘𝑃)(Hom ‘𝑆)((1st𝐹)‘𝑃)) ↔ (𝑎𝑃):((1st ‘((1st𝑌)‘𝑋))‘𝑃)⟶((1st𝐹)‘𝑃)))
7371, 72mpbid 232 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝑎𝑃):((1st ‘((1st𝑌)‘𝑋))‘𝑃)⟶((1st𝐹)‘𝑃))
747, 34nat1st2nd 17999 . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ (⟨(1st𝐹), (2nd𝐹)⟩(𝑂 Nat 𝑆)⟨(1st𝐺), (2nd𝐺)⟩))
757, 74, 10, 70, 27natcl 18001 . . . . . . . . . . . . 13 (𝜑 → (𝐴𝑃) ∈ (((1st𝐹)‘𝑃)(Hom ‘𝑆)((1st𝐺)‘𝑃)))
7618, 22, 70, 60, 67elsetchom 18126 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝑃) ∈ (((1st𝐹)‘𝑃)(Hom ‘𝑆)((1st𝐺)‘𝑃)) ↔ (𝐴𝑃):((1st𝐹)‘𝑃)⟶((1st𝐺)‘𝑃)))
7775, 76mpbid 232 . . . . . . . . . . . 12 (𝜑 → (𝐴𝑃):((1st𝐹)‘𝑃)⟶((1st𝐺)‘𝑃))
7877adantr 480 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝐴𝑃):((1st𝐹)‘𝑃)⟶((1st𝐺)‘𝑃))
7918, 40, 11, 53, 61, 68, 73, 78setcco 18128 . . . . . . . . . 10 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴𝑃)(⟨((1st ‘((1st𝑌)‘𝑋))‘𝑃), ((1st𝐹)‘𝑃)⟩(comp‘𝑆)((1st𝐺)‘𝑃))(𝑎𝑃)) = ((𝐴𝑃) ∘ (𝑎𝑃)))
8039, 79eqtrd 2777 . . . . . . . . 9 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)‘𝑃) = ((𝐴𝑃) ∘ (𝑎𝑃)))
8180oveq1d 7446 . . . . . . . 8 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)‘𝑃)(⟨((1st ‘((1st𝑌)‘𝑃))‘𝑃), ((1st ‘((1st𝑌)‘𝑋))‘𝑃)⟩(comp‘𝑆)((1st𝐺)‘𝑃))(((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)) = (((𝐴𝑃) ∘ (𝑎𝑃))(⟨((1st ‘((1st𝑌)‘𝑃))‘𝑃), ((1st ‘((1st𝑌)‘𝑋))‘𝑃)⟩(comp‘𝑆)((1st𝐺)‘𝑃))(((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)))
8244, 27ffvelcdmd 7105 . . . . . . . . . . . . . 14 (𝜑 → ((1st𝑌)‘𝑃) ∈ (𝑂 Func 𝑆))
83 1st2ndbr 8067 . . . . . . . . . . . . . 14 ((Rel (𝑂 Func 𝑆) ∧ ((1st𝑌)‘𝑃) ∈ (𝑂 Func 𝑆)) → (1st ‘((1st𝑌)‘𝑃))(𝑂 Func 𝑆)(2nd ‘((1st𝑌)‘𝑃)))
8442, 82, 83sylancr 587 . . . . . . . . . . . . 13 (𝜑 → (1st ‘((1st𝑌)‘𝑃))(𝑂 Func 𝑆)(2nd ‘((1st𝑌)‘𝑃)))
8510, 41, 84funcf1 17911 . . . . . . . . . . . 12 (𝜑 → (1st ‘((1st𝑌)‘𝑃)):𝐵⟶(Base‘𝑆))
8685, 27ffvelcdmd 7105 . . . . . . . . . . 11 (𝜑 → ((1st ‘((1st𝑌)‘𝑃))‘𝑃) ∈ (Base‘𝑆))
8786, 49eleqtrrd 2844 . . . . . . . . . 10 (𝜑 → ((1st ‘((1st𝑌)‘𝑃))‘𝑃) ∈ 𝑈)
8887adantr 480 . . . . . . . . 9 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1st ‘((1st𝑌)‘𝑃))‘𝑃) ∈ 𝑈)
897, 31nat1st2nd 17999 . . . . . . . . . . . 12 (𝜑 → ((𝑃(2nd𝑌)𝑋)‘𝐾) ∈ (⟨(1st ‘((1st𝑌)‘𝑃)), (2nd ‘((1st𝑌)‘𝑃))⟩(𝑂 Nat 𝑆)⟨(1st ‘((1st𝑌)‘𝑋)), (2nd ‘((1st𝑌)‘𝑋))⟩))
907, 89, 10, 70, 27natcl 18001 . . . . . . . . . . 11 (𝜑 → (((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃) ∈ (((1st ‘((1st𝑌)‘𝑃))‘𝑃)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑋))‘𝑃)))
9118, 22, 70, 87, 52elsetchom 18126 . . . . . . . . . . 11 (𝜑 → ((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃) ∈ (((1st ‘((1st𝑌)‘𝑃))‘𝑃)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑋))‘𝑃)) ↔ (((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃):((1st ‘((1st𝑌)‘𝑃))‘𝑃)⟶((1st ‘((1st𝑌)‘𝑋))‘𝑃)))
9290, 91mpbid 232 . . . . . . . . . 10 (𝜑 → (((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃):((1st ‘((1st𝑌)‘𝑃))‘𝑃)⟶((1st ‘((1st𝑌)‘𝑋))‘𝑃))
9392adantr 480 . . . . . . . . 9 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃):((1st ‘((1st𝑌)‘𝑃))‘𝑃)⟶((1st ‘((1st𝑌)‘𝑋))‘𝑃))
94 fco 6760 . . . . . . . . . 10 (((𝐴𝑃):((1st𝐹)‘𝑃)⟶((1st𝐺)‘𝑃) ∧ (𝑎𝑃):((1st ‘((1st𝑌)‘𝑋))‘𝑃)⟶((1st𝐹)‘𝑃)) → ((𝐴𝑃) ∘ (𝑎𝑃)):((1st ‘((1st𝑌)‘𝑋))‘𝑃)⟶((1st𝐺)‘𝑃))
9578, 73, 94syl2anc 584 . . . . . . . . 9 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴𝑃) ∘ (𝑎𝑃)):((1st ‘((1st𝑌)‘𝑋))‘𝑃)⟶((1st𝐺)‘𝑃))
9618, 40, 11, 88, 53, 68, 93, 95setcco 18128 . . . . . . . 8 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴𝑃) ∘ (𝑎𝑃))(⟨((1st ‘((1st𝑌)‘𝑃))‘𝑃), ((1st ‘((1st𝑌)‘𝑋))‘𝑃)⟩(comp‘𝑆)((1st𝐺)‘𝑃))(((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)) = (((𝐴𝑃) ∘ (𝑎𝑃)) ∘ (((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)))
9738, 81, 963eqtrd 2781 . . . . . . 7 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃) = (((𝐴𝑃) ∘ (𝑎𝑃)) ∘ (((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)))
9897fveq1d 6908 . . . . . 6 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃)‘( 1𝑃)) = ((((𝐴𝑃) ∘ (𝑎𝑃)) ∘ (((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃))‘( 1𝑃)))
99 yoneda.1 . . . . . . . . . 10 1 = (Id‘𝐶)
1009, 13, 99, 17, 27catidcl 17725 . . . . . . . . 9 (𝜑 → ( 1𝑃) ∈ (𝑃(Hom ‘𝐶)𝑃))
10116, 9, 17, 27, 13, 27yon11 18309 . . . . . . . . 9 (𝜑 → ((1st ‘((1st𝑌)‘𝑃))‘𝑃) = (𝑃(Hom ‘𝐶)𝑃))
102100, 101eleqtrrd 2844 . . . . . . . 8 (𝜑 → ( 1𝑃) ∈ ((1st ‘((1st𝑌)‘𝑃))‘𝑃))
103102adantr 480 . . . . . . 7 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1𝑃) ∈ ((1st ‘((1st𝑌)‘𝑃))‘𝑃))
104 fvco3 7008 . . . . . . 7 (((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃):((1st ‘((1st𝑌)‘𝑃))‘𝑃)⟶((1st ‘((1st𝑌)‘𝑋))‘𝑃) ∧ ( 1𝑃) ∈ ((1st ‘((1st𝑌)‘𝑃))‘𝑃)) → ((((𝐴𝑃) ∘ (𝑎𝑃)) ∘ (((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃))‘( 1𝑃)) = (((𝐴𝑃) ∘ (𝑎𝑃))‘((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃))))
10593, 103, 104syl2anc 584 . . . . . 6 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝐴𝑃) ∘ (𝑎𝑃)) ∘ (((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃))‘( 1𝑃)) = (((𝐴𝑃) ∘ (𝑎𝑃))‘((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃))))
10693, 103ffvelcdmd 7105 . . . . . . . 8 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃)) ∈ ((1st ‘((1st𝑌)‘𝑋))‘𝑃))
107 fvco3 7008 . . . . . . . 8 (((𝑎𝑃):((1st ‘((1st𝑌)‘𝑋))‘𝑃)⟶((1st𝐹)‘𝑃) ∧ ((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃)) ∈ ((1st ‘((1st𝑌)‘𝑋))‘𝑃)) → (((𝐴𝑃) ∘ (𝑎𝑃))‘((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃))) = ((𝐴𝑃)‘((𝑎𝑃)‘((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃)))))
10873, 106, 107syl2anc 584 . . . . . . 7 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴𝑃) ∘ (𝑎𝑃))‘((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃))) = ((𝐴𝑃)‘((𝑎𝑃)‘((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃)))))
10917adantr 480 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐶 ∈ Cat)
11028adantr 480 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑋𝐵)
111 eqid 2737 . . . . . . . . . . . 12 (comp‘𝐶) = (comp‘𝐶)
11230adantr 480 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋))
113100adantr 480 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1𝑃) ∈ (𝑃(Hom ‘𝐶)𝑃))
11416, 9, 109, 37, 13, 110, 111, 37, 112, 113yon2 18311 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃)) = (𝐾(⟨𝑃, 𝑃⟩(comp‘𝐶)𝑋)( 1𝑃)))
1159, 13, 99, 109, 37, 111, 110, 112catrid 17727 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝐾(⟨𝑃, 𝑃⟩(comp‘𝐶)𝑋)( 1𝑃)) = 𝐾)
116114, 115eqtrd 2777 . . . . . . . . . 10 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃)) = 𝐾)
117116fveq2d 6910 . . . . . . . . 9 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎𝑃)‘((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃))) = ((𝑎𝑃)‘𝐾))
118 eqid 2737 . . . . . . . . . . . . . . 15 (Hom ‘𝑂) = (Hom ‘𝑂)
11910, 118, 70, 47, 28, 27funcf2 17913 . . . . . . . . . . . . . 14 (𝜑 → (𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃):(𝑋(Hom ‘𝑂)𝑃)⟶(((1st ‘((1st𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑋))‘𝑃)))
12013, 8oppchom 17758 . . . . . . . . . . . . . . 15 (𝑋(Hom ‘𝑂)𝑃) = (𝑃(Hom ‘𝐶)𝑋)
12130, 120eleqtrrdi 2852 . . . . . . . . . . . . . 14 (𝜑𝐾 ∈ (𝑋(Hom ‘𝑂)𝑃))
122119, 121ffvelcdmd 7105 . . . . . . . . . . . . 13 (𝜑 → ((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾) ∈ (((1st ‘((1st𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑋))‘𝑃)))
12351, 28ffvelcdmd 7105 . . . . . . . . . . . . . 14 (𝜑 → ((1st ‘((1st𝑌)‘𝑋))‘𝑋) ∈ 𝑈)
12418, 22, 70, 123, 52elsetchom 18126 . . . . . . . . . . . . 13 (𝜑 → (((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾) ∈ (((1st ‘((1st𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑋))‘𝑃)) ↔ ((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾):((1st ‘((1st𝑌)‘𝑋))‘𝑋)⟶((1st ‘((1st𝑌)‘𝑋))‘𝑃)))
125122, 124mpbid 232 . . . . . . . . . . . 12 (𝜑 → ((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾):((1st ‘((1st𝑌)‘𝑋))‘𝑋)⟶((1st ‘((1st𝑌)‘𝑋))‘𝑃))
126125adantr 480 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾):((1st ‘((1st𝑌)‘𝑋))‘𝑋)⟶((1st ‘((1st𝑌)‘𝑋))‘𝑃))
1279, 13, 99, 17, 28catidcl 17725 . . . . . . . . . . . . 13 (𝜑 → ( 1𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋))
12816, 9, 17, 28, 13, 28yon11 18309 . . . . . . . . . . . . 13 (𝜑 → ((1st ‘((1st𝑌)‘𝑋))‘𝑋) = (𝑋(Hom ‘𝐶)𝑋))
129127, 128eleqtrrd 2844 . . . . . . . . . . . 12 (𝜑 → ( 1𝑋) ∈ ((1st ‘((1st𝑌)‘𝑋))‘𝑋))
130129adantr 480 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1𝑋) ∈ ((1st ‘((1st𝑌)‘𝑋))‘𝑋))
131 fvco3 7008 . . . . . . . . . . 11 ((((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾):((1st ‘((1st𝑌)‘𝑋))‘𝑋)⟶((1st ‘((1st𝑌)‘𝑋))‘𝑃) ∧ ( 1𝑋) ∈ ((1st ‘((1st𝑌)‘𝑋))‘𝑋)) → (((𝑎𝑃) ∘ ((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾))‘( 1𝑋)) = ((𝑎𝑃)‘(((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾)‘( 1𝑋))))
132126, 130, 131syl2anc 584 . . . . . . . . . 10 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑎𝑃) ∘ ((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾))‘( 1𝑋)) = ((𝑎𝑃)‘(((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾)‘( 1𝑋))))
133121adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐾 ∈ (𝑋(Hom ‘𝑂)𝑃))
1347, 69, 10, 118, 11, 110, 37, 133nati 18003 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎𝑃)(⟨((1st ‘((1st𝑌)‘𝑋))‘𝑋), ((1st ‘((1st𝑌)‘𝑋))‘𝑃)⟩(comp‘𝑆)((1st𝐹)‘𝑃))((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾)) = (((𝑋(2nd𝐹)𝑃)‘𝐾)(⟨((1st ‘((1st𝑌)‘𝑋))‘𝑋), ((1st𝐹)‘𝑋)⟩(comp‘𝑆)((1st𝐹)‘𝑃))(𝑎𝑋)))
135123adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1st ‘((1st𝑌)‘𝑋))‘𝑋) ∈ 𝑈)
13618, 40, 11, 135, 53, 61, 126, 73setcco 18128 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎𝑃)(⟨((1st ‘((1st𝑌)‘𝑋))‘𝑋), ((1st ‘((1st𝑌)‘𝑋))‘𝑃)⟩(comp‘𝑆)((1st𝐹)‘𝑃))((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾)) = ((𝑎𝑃) ∘ ((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾)))
13759, 28ffvelcdmd 7105 . . . . . . . . . . . . . 14 (𝜑 → ((1st𝐹)‘𝑋) ∈ 𝑈)
138137adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1st𝐹)‘𝑋) ∈ 𝑈)
1397, 69, 10, 70, 110natcl 18001 . . . . . . . . . . . . . 14 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝑎𝑋) ∈ (((1st ‘((1st𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1st𝐹)‘𝑋)))
14018, 40, 70, 135, 138elsetchom 18126 . . . . . . . . . . . . . 14 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎𝑋) ∈ (((1st ‘((1st𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1st𝐹)‘𝑋)) ↔ (𝑎𝑋):((1st ‘((1st𝑌)‘𝑋))‘𝑋)⟶((1st𝐹)‘𝑋)))
141139, 140mpbid 232 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝑎𝑋):((1st ‘((1st𝑌)‘𝑋))‘𝑋)⟶((1st𝐹)‘𝑋))
14210, 118, 70, 56, 28, 27funcf2 17913 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋(2nd𝐹)𝑃):(𝑋(Hom ‘𝑂)𝑃)⟶(((1st𝐹)‘𝑋)(Hom ‘𝑆)((1st𝐹)‘𝑃)))
143142, 121ffvelcdmd 7105 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑋(2nd𝐹)𝑃)‘𝐾) ∈ (((1st𝐹)‘𝑋)(Hom ‘𝑆)((1st𝐹)‘𝑃)))
14418, 22, 70, 137, 60elsetchom 18126 . . . . . . . . . . . . . . 15 (𝜑 → (((𝑋(2nd𝐹)𝑃)‘𝐾) ∈ (((1st𝐹)‘𝑋)(Hom ‘𝑆)((1st𝐹)‘𝑃)) ↔ ((𝑋(2nd𝐹)𝑃)‘𝐾):((1st𝐹)‘𝑋)⟶((1st𝐹)‘𝑃)))
145143, 144mpbid 232 . . . . . . . . . . . . . 14 (𝜑 → ((𝑋(2nd𝐹)𝑃)‘𝐾):((1st𝐹)‘𝑋)⟶((1st𝐹)‘𝑃))
146145adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑋(2nd𝐹)𝑃)‘𝐾):((1st𝐹)‘𝑋)⟶((1st𝐹)‘𝑃))
14718, 40, 11, 135, 138, 61, 141, 146setcco 18128 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑋(2nd𝐹)𝑃)‘𝐾)(⟨((1st ‘((1st𝑌)‘𝑋))‘𝑋), ((1st𝐹)‘𝑋)⟩(comp‘𝑆)((1st𝐹)‘𝑃))(𝑎𝑋)) = (((𝑋(2nd𝐹)𝑃)‘𝐾) ∘ (𝑎𝑋)))
148134, 136, 1473eqtr3d 2785 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎𝑃) ∘ ((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾)) = (((𝑋(2nd𝐹)𝑃)‘𝐾) ∘ (𝑎𝑋)))
149148fveq1d 6908 . . . . . . . . . 10 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑎𝑃) ∘ ((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾))‘( 1𝑋)) = ((((𝑋(2nd𝐹)𝑃)‘𝐾) ∘ (𝑎𝑋))‘( 1𝑋)))
150127adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋))
15116, 9, 109, 110, 13, 110, 111, 37, 112, 150yon12 18310 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾)‘( 1𝑋)) = (( 1𝑋)(⟨𝑃, 𝑋⟩(comp‘𝐶)𝑋)𝐾))
1529, 13, 99, 109, 37, 111, 110, 112catlid 17726 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (( 1𝑋)(⟨𝑃, 𝑋⟩(comp‘𝐶)𝑋)𝐾) = 𝐾)
153151, 152eqtrd 2777 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾)‘( 1𝑋)) = 𝐾)
154153fveq2d 6910 . . . . . . . . . 10 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎𝑃)‘(((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾)‘( 1𝑋))) = ((𝑎𝑃)‘𝐾))
155132, 149, 1543eqtr3d 2785 . . . . . . . . 9 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑋(2nd𝐹)𝑃)‘𝐾) ∘ (𝑎𝑋))‘( 1𝑋)) = ((𝑎𝑃)‘𝐾))
156 fvco3 7008 . . . . . . . . . 10 (((𝑎𝑋):((1st ‘((1st𝑌)‘𝑋))‘𝑋)⟶((1st𝐹)‘𝑋) ∧ ( 1𝑋) ∈ ((1st ‘((1st𝑌)‘𝑋))‘𝑋)) → ((((𝑋(2nd𝐹)𝑃)‘𝐾) ∘ (𝑎𝑋))‘( 1𝑋)) = (((𝑋(2nd𝐹)𝑃)‘𝐾)‘((𝑎𝑋)‘( 1𝑋))))
157141, 130, 156syl2anc 584 . . . . . . . . 9 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑋(2nd𝐹)𝑃)‘𝐾) ∘ (𝑎𝑋))‘( 1𝑋)) = (((𝑋(2nd𝐹)𝑃)‘𝐾)‘((𝑎𝑋)‘( 1𝑋))))
158117, 155, 1573eqtr2d 2783 . . . . . . . 8 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎𝑃)‘((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃))) = (((𝑋(2nd𝐹)𝑃)‘𝐾)‘((𝑎𝑋)‘( 1𝑋))))
159158fveq2d 6910 . . . . . . 7 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴𝑃)‘((𝑎𝑃)‘((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃)))) = ((𝐴𝑃)‘(((𝑋(2nd𝐹)𝑃)‘𝐾)‘((𝑎𝑋)‘( 1𝑋)))))
160108, 159eqtrd 2777 . . . . . 6 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴𝑃) ∘ (𝑎𝑃))‘((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃))) = ((𝐴𝑃)‘(((𝑋(2nd𝐹)𝑃)‘𝐾)‘((𝑎𝑋)‘( 1𝑋)))))
16198, 105, 1603eqtrd 2781 . . . . 5 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃)‘( 1𝑃)) = ((𝐴𝑃)‘(((𝑋(2nd𝐹)𝑃)‘𝐾)‘((𝑎𝑋)‘( 1𝑋)))))
162161mpteq2dva 5242 . . . 4 (𝜑 → (𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃)‘( 1𝑃))) = (𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴𝑃)‘(((𝑋(2nd𝐹)𝑃)‘𝐾)‘((𝑎𝑋)‘( 1𝑋))))))
1635, 162eqtrid 2789 . . 3 (𝜑 → (𝑏 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃)‘( 1𝑃))) = (𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴𝑃)‘(((𝑋(2nd𝐹)𝑃)‘𝐾)‘((𝑎𝑋)‘( 1𝑋))))))
164 eqid 2737 . . . . . . . . . . 11 (𝑄 ×c 𝑂) = (𝑄 ×c 𝑂)
165164, 43, 10xpcbas 18223 . . . . . . . . . 10 ((𝑂 Func 𝑆) × 𝐵) = (Base‘(𝑄 ×c 𝑂))
166 eqid 2737 . . . . . . . . . 10 (Hom ‘(𝑄 ×c 𝑂)) = (Hom ‘(𝑄 ×c 𝑂))
167 eqid 2737 . . . . . . . . . 10 (Hom ‘𝑇) = (Hom ‘𝑇)
168 relfunc 17907 . . . . . . . . . . 11 Rel ((𝑄 ×c 𝑂) Func 𝑇)
169 yoneda.t . . . . . . . . . . . . 13 𝑇 = (SetCat‘𝑉)
170 yoneda.h . . . . . . . . . . . . 13 𝐻 = (HomF𝑄)
171 yoneda.r . . . . . . . . . . . . 13 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)
172 yoneda.e . . . . . . . . . . . . 13 𝐸 = (𝑂 evalF 𝑆)
173 yoneda.z . . . . . . . . . . . . 13 𝑍 = (𝐻func ((⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))
17416, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20yonedalem1 18317 . . . . . . . . . . . 12 (𝜑 → (𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)))
175174simpld 494 . . . . . . . . . . 11 (𝜑𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇))
176 1st2ndbr 8067 . . . . . . . . . . 11 ((Rel ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st𝑍)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝑍))
177168, 175, 176sylancr 587 . . . . . . . . . 10 (𝜑 → (1st𝑍)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝑍))
17854, 28opelxpd 5724 . . . . . . . . . 10 (𝜑 → ⟨𝐹, 𝑋⟩ ∈ ((𝑂 Func 𝑆) × 𝐵))
17962, 27opelxpd 5724 . . . . . . . . . 10 (𝜑 → ⟨𝐺, 𝑃⟩ ∈ ((𝑂 Func 𝑆) × 𝐵))
180165, 166, 167, 177, 178, 179funcf2 17913 . . . . . . . . 9 (𝜑 → (⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩):(⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×c 𝑂))⟨𝐺, 𝑃⟩)⟶(((1st𝑍)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1st𝑍)‘⟨𝐺, 𝑃⟩)))
181164, 43, 10, 14, 118, 54, 28, 62, 27, 166xpchom2 18231 . . . . . . . . . . 11 (𝜑 → (⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×c 𝑂))⟨𝐺, 𝑃⟩) = ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑋(Hom ‘𝑂)𝑃)))
182120xpeq2i 5712 . . . . . . . . . . 11 ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑋(Hom ‘𝑂)𝑃)) = ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))
183181, 182eqtrdi 2793 . . . . . . . . . 10 (𝜑 → (⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×c 𝑂))⟨𝐺, 𝑃⟩) = ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋)))
184 df-ov 7434 . . . . . . . . . . . . 13 (𝐹(1st𝑍)𝑋) = ((1st𝑍)‘⟨𝐹, 𝑋⟩)
185 df-ov 7434 . . . . . . . . . . . . 13 (𝐺(1st𝑍)𝑃) = ((1st𝑍)‘⟨𝐺, 𝑃⟩)
186184, 185oveq12i 7443 . . . . . . . . . . . 12 ((𝐹(1st𝑍)𝑋)(Hom ‘𝑇)(𝐺(1st𝑍)𝑃)) = (((1st𝑍)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1st𝑍)‘⟨𝐺, 𝑃⟩))
187186eqcomi 2746 . . . . . . . . . . 11 (((1st𝑍)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1st𝑍)‘⟨𝐺, 𝑃⟩)) = ((𝐹(1st𝑍)𝑋)(Hom ‘𝑇)(𝐺(1st𝑍)𝑃))
188187a1i 11 . . . . . . . . . 10 (𝜑 → (((1st𝑍)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1st𝑍)‘⟨𝐺, 𝑃⟩)) = ((𝐹(1st𝑍)𝑋)(Hom ‘𝑇)(𝐺(1st𝑍)𝑃)))
189183, 188feq23d 6731 . . . . . . . . 9 (𝜑 → ((⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩):(⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×c 𝑂))⟨𝐺, 𝑃⟩)⟶(((1st𝑍)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1st𝑍)‘⟨𝐺, 𝑃⟩)) ↔ (⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩):((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))⟶((𝐹(1st𝑍)𝑋)(Hom ‘𝑇)(𝐺(1st𝑍)𝑃))))
190180, 189mpbid 232 . . . . . . . 8 (𝜑 → (⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩):((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))⟶((𝐹(1st𝑍)𝑋)(Hom ‘𝑇)(𝐺(1st𝑍)𝑃)))
191190, 34, 30fovcdmd 7605 . . . . . . 7 (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾) ∈ ((𝐹(1st𝑍)𝑋)(Hom ‘𝑇)(𝐺(1st𝑍)𝑃)))
192 eqid 2737 . . . . . . . . . . 11 (Base‘𝑇) = (Base‘𝑇)
193165, 192, 177funcf1 17911 . . . . . . . . . 10 (𝜑 → (1st𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
194193, 54, 28fovcdmd 7605 . . . . . . . . 9 (𝜑 → (𝐹(1st𝑍)𝑋) ∈ (Base‘𝑇))
195169, 19setcbas 18123 . . . . . . . . 9 (𝜑𝑉 = (Base‘𝑇))
196194, 195eleqtrrd 2844 . . . . . . . 8 (𝜑 → (𝐹(1st𝑍)𝑋) ∈ 𝑉)
197193, 62, 27fovcdmd 7605 . . . . . . . . 9 (𝜑 → (𝐺(1st𝑍)𝑃) ∈ (Base‘𝑇))
198197, 195eleqtrrd 2844 . . . . . . . 8 (𝜑 → (𝐺(1st𝑍)𝑃) ∈ 𝑉)
199169, 19, 167, 196, 198elsetchom 18126 . . . . . . 7 (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾) ∈ ((𝐹(1st𝑍)𝑋)(Hom ‘𝑇)(𝐺(1st𝑍)𝑃)) ↔ (𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾):(𝐹(1st𝑍)𝑋)⟶(𝐺(1st𝑍)𝑃)))
200191, 199mpbid 232 . . . . . 6 (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾):(𝐹(1st𝑍)𝑋)⟶(𝐺(1st𝑍)𝑃))
20116, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 54, 28, 62, 27, 34, 30yonedalem22 18323 . . . . . . . 8 (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾) = (((𝑃(2nd𝑌)𝑋)‘𝐾)(⟨((1st𝑌)‘𝑋), 𝐹⟩(2nd𝐻)⟨((1st𝑌)‘𝑃), 𝐺⟩)𝐴))
2028oppccat 17765 . . . . . . . . . . 11 (𝐶 ∈ Cat → 𝑂 ∈ Cat)
20317, 202syl 17 . . . . . . . . . 10 (𝜑𝑂 ∈ Cat)
20418setccat 18130 . . . . . . . . . . 11 (𝑈 ∈ V → 𝑆 ∈ Cat)
20522, 204syl 17 . . . . . . . . . 10 (𝜑𝑆 ∈ Cat)
2066, 203, 205fuccat 18018 . . . . . . . . 9 (𝜑𝑄 ∈ Cat)
207170, 206, 43, 14, 45, 54, 82, 62, 12, 31, 34hof2val 18301 . . . . . . . 8 (𝜑 → (((𝑃(2nd𝑌)𝑋)‘𝐾)(⟨((1st𝑌)‘𝑋), 𝐹⟩(2nd𝐻)⟨((1st𝑌)‘𝑃), 𝐺⟩)𝐴) = (𝑏 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))))
208201, 207eqtrd 2777 . . . . . . 7 (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾) = (𝑏 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))))
20916, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 54, 28yonedalem21 18318 . . . . . . 7 (𝜑 → (𝐹(1st𝑍)𝑋) = (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹))
21016, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 62, 27yonedalem21 18318 . . . . . . 7 (𝜑 → (𝐺(1st𝑍)𝑃) = (((1st𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺))
211208, 209, 210feq123d 6725 . . . . . 6 (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾):(𝐹(1st𝑍)𝑋)⟶(𝐺(1st𝑍)𝑃) ↔ (𝑏 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))):(((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)⟶(((1st𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺)))
212200, 211mpbid 232 . . . . 5 (𝜑 → (𝑏 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))):(((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)⟶(((1st𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺))
213 eqid 2737 . . . . . 6 (𝑏 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))) = (𝑏 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾)))
214213fmpt 7130 . . . . 5 (∀𝑏 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾)) ∈ (((1st𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺) ↔ (𝑏 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))):(((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)⟶(((1st𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺))
215212, 214sylibr 234 . . . 4 (𝜑 → ∀𝑏 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾)) ∈ (((1st𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺))
216 yonedalem3.m . . . . . 6 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥𝐵 ↦ (𝑎 ∈ (((1st𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎𝑥)‘( 1𝑥))))
21716, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 62, 27, 216yonedalem3a 18319 . . . . 5 (𝜑 → ((𝐺𝑀𝑃) = (𝑎 ∈ (((1st𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺) ↦ ((𝑎𝑃)‘( 1𝑃))) ∧ (𝐺𝑀𝑃):(𝐺(1st𝑍)𝑃)⟶(𝐺(1st𝐸)𝑃)))
218217simpld 494 . . . 4 (𝜑 → (𝐺𝑀𝑃) = (𝑎 ∈ (((1st𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺) ↦ ((𝑎𝑃)‘( 1𝑃))))
219 fveq1 6905 . . . . 5 (𝑎 = ((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾)) → (𝑎𝑃) = (((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃))
220219fveq1d 6908 . . . 4 (𝑎 = ((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾)) → ((𝑎𝑃)‘( 1𝑃)) = ((((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃)‘( 1𝑃)))
221215, 208, 218, 220fmptcof 7150 . . 3 (𝜑 → ((𝐺𝑀𝑃) ∘ (𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾)) = (𝑏 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃)‘( 1𝑃))))
222 eqid 2737 . . . . . . 7 (⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩) = (⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)
223172, 203, 205, 10, 118, 11, 7, 54, 62, 28, 27, 222, 34, 121evlf2val 18264 . . . . . 6 (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)𝐾) = ((𝐴𝑃)(⟨((1st𝐹)‘𝑋), ((1st𝐹)‘𝑃)⟩(comp‘𝑆)((1st𝐺)‘𝑃))((𝑋(2nd𝐹)𝑃)‘𝐾)))
22418, 22, 11, 137, 60, 67, 145, 77setcco 18128 . . . . . 6 (𝜑 → ((𝐴𝑃)(⟨((1st𝐹)‘𝑋), ((1st𝐹)‘𝑃)⟩(comp‘𝑆)((1st𝐺)‘𝑃))((𝑋(2nd𝐹)𝑃)‘𝐾)) = ((𝐴𝑃) ∘ ((𝑋(2nd𝐹)𝑃)‘𝐾)))
225223, 224eqtrd 2777 . . . . 5 (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)𝐾) = ((𝐴𝑃) ∘ ((𝑋(2nd𝐹)𝑃)‘𝐾)))
226225coeq1d 5872 . . . 4 (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)𝐾) ∘ (𝐹𝑀𝑋)) = (((𝐴𝑃) ∘ ((𝑋(2nd𝐹)𝑃)‘𝐾)) ∘ (𝐹𝑀𝑋)))
22716, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 54, 28, 216yonedalem3a 18319 . . . . . . . 8 (𝜑 → ((𝐹𝑀𝑋) = (𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎𝑋)‘( 1𝑋))) ∧ (𝐹𝑀𝑋):(𝐹(1st𝑍)𝑋)⟶(𝐹(1st𝐸)𝑋)))
228227simprd 495 . . . . . . 7 (𝜑 → (𝐹𝑀𝑋):(𝐹(1st𝑍)𝑋)⟶(𝐹(1st𝐸)𝑋))
229227simpld 494 . . . . . . . 8 (𝜑 → (𝐹𝑀𝑋) = (𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎𝑋)‘( 1𝑋))))
230172, 203, 205, 10, 54, 28evlf1 18265 . . . . . . . 8 (𝜑 → (𝐹(1st𝐸)𝑋) = ((1st𝐹)‘𝑋))
231229, 209, 230feq123d 6725 . . . . . . 7 (𝜑 → ((𝐹𝑀𝑋):(𝐹(1st𝑍)𝑋)⟶(𝐹(1st𝐸)𝑋) ↔ (𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎𝑋)‘( 1𝑋))):(((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)⟶((1st𝐹)‘𝑋)))
232228, 231mpbid 232 . . . . . 6 (𝜑 → (𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎𝑋)‘( 1𝑋))):(((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)⟶((1st𝐹)‘𝑋))
233 eqid 2737 . . . . . . 7 (𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎𝑋)‘( 1𝑋))) = (𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎𝑋)‘( 1𝑋)))
234233fmpt 7130 . . . . . 6 (∀𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)((𝑎𝑋)‘( 1𝑋)) ∈ ((1st𝐹)‘𝑋) ↔ (𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎𝑋)‘( 1𝑋))):(((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)⟶((1st𝐹)‘𝑋))
235232, 234sylibr 234 . . . . 5 (𝜑 → ∀𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)((𝑎𝑋)‘( 1𝑋)) ∈ ((1st𝐹)‘𝑋))
236 fcompt 7153 . . . . . 6 (((𝐴𝑃):((1st𝐹)‘𝑃)⟶((1st𝐺)‘𝑃) ∧ ((𝑋(2nd𝐹)𝑃)‘𝐾):((1st𝐹)‘𝑋)⟶((1st𝐹)‘𝑃)) → ((𝐴𝑃) ∘ ((𝑋(2nd𝐹)𝑃)‘𝐾)) = (𝑦 ∈ ((1st𝐹)‘𝑋) ↦ ((𝐴𝑃)‘(((𝑋(2nd𝐹)𝑃)‘𝐾)‘𝑦))))
23777, 145, 236syl2anc 584 . . . . 5 (𝜑 → ((𝐴𝑃) ∘ ((𝑋(2nd𝐹)𝑃)‘𝐾)) = (𝑦 ∈ ((1st𝐹)‘𝑋) ↦ ((𝐴𝑃)‘(((𝑋(2nd𝐹)𝑃)‘𝐾)‘𝑦))))
238 2fveq3 6911 . . . . 5 (𝑦 = ((𝑎𝑋)‘( 1𝑋)) → ((𝐴𝑃)‘(((𝑋(2nd𝐹)𝑃)‘𝐾)‘𝑦)) = ((𝐴𝑃)‘(((𝑋(2nd𝐹)𝑃)‘𝐾)‘((𝑎𝑋)‘( 1𝑋)))))
239235, 229, 237, 238fmptcof 7150 . . . 4 (𝜑 → (((𝐴𝑃) ∘ ((𝑋(2nd𝐹)𝑃)‘𝐾)) ∘ (𝐹𝑀𝑋)) = (𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴𝑃)‘(((𝑋(2nd𝐹)𝑃)‘𝐾)‘((𝑎𝑋)‘( 1𝑋))))))
240226, 239eqtrd 2777 . . 3 (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)𝐾) ∘ (𝐹𝑀𝑋)) = (𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴𝑃)‘(((𝑋(2nd𝐹)𝑃)‘𝐾)‘((𝑎𝑋)‘( 1𝑋))))))
241163, 221, 2403eqtr4d 2787 . 2 (𝜑 → ((𝐺𝑀𝑃) ∘ (𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾)) = ((𝐴(⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)𝐾) ∘ (𝐹𝑀𝑋)))
242 eqid 2737 . . 3 (comp‘𝑇) = (comp‘𝑇)
243174simprd 495 . . . . . . 7 (𝜑𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇))
244 1st2ndbr 8067 . . . . . . 7 ((Rel ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st𝐸)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝐸))
245168, 243, 244sylancr 587 . . . . . 6 (𝜑 → (1st𝐸)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝐸))
246165, 192, 245funcf1 17911 . . . . 5 (𝜑 → (1st𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
247246, 62, 27fovcdmd 7605 . . . 4 (𝜑 → (𝐺(1st𝐸)𝑃) ∈ (Base‘𝑇))
248247, 195eleqtrrd 2844 . . 3 (𝜑 → (𝐺(1st𝐸)𝑃) ∈ 𝑉)
249217simprd 495 . . 3 (𝜑 → (𝐺𝑀𝑃):(𝐺(1st𝑍)𝑃)⟶(𝐺(1st𝐸)𝑃))
250169, 19, 242, 196, 198, 248, 200, 249setcco 18128 . 2 (𝜑 → ((𝐺𝑀𝑃)(⟨(𝐹(1st𝑍)𝑋), (𝐺(1st𝑍)𝑃)⟩(comp‘𝑇)(𝐺(1st𝐸)𝑃))(𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾)) = ((𝐺𝑀𝑃) ∘ (𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾)))
251246, 54, 28fovcdmd 7605 . . . 4 (𝜑 → (𝐹(1st𝐸)𝑋) ∈ (Base‘𝑇))
252251, 195eleqtrrd 2844 . . 3 (𝜑 → (𝐹(1st𝐸)𝑋) ∈ 𝑉)
253165, 166, 167, 245, 178, 179funcf2 17913 . . . . . 6 (𝜑 → (⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩):(⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×c 𝑂))⟨𝐺, 𝑃⟩)⟶(((1st𝐸)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1st𝐸)‘⟨𝐺, 𝑃⟩)))
254 df-ov 7434 . . . . . . . . . 10 (𝐹(1st𝐸)𝑋) = ((1st𝐸)‘⟨𝐹, 𝑋⟩)
255 df-ov 7434 . . . . . . . . . 10 (𝐺(1st𝐸)𝑃) = ((1st𝐸)‘⟨𝐺, 𝑃⟩)
256254, 255oveq12i 7443 . . . . . . . . 9 ((𝐹(1st𝐸)𝑋)(Hom ‘𝑇)(𝐺(1st𝐸)𝑃)) = (((1st𝐸)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1st𝐸)‘⟨𝐺, 𝑃⟩))
257256eqcomi 2746 . . . . . . . 8 (((1st𝐸)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1st𝐸)‘⟨𝐺, 𝑃⟩)) = ((𝐹(1st𝐸)𝑋)(Hom ‘𝑇)(𝐺(1st𝐸)𝑃))
258257a1i 11 . . . . . . 7 (𝜑 → (((1st𝐸)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1st𝐸)‘⟨𝐺, 𝑃⟩)) = ((𝐹(1st𝐸)𝑋)(Hom ‘𝑇)(𝐺(1st𝐸)𝑃)))
259183, 258feq23d 6731 . . . . . 6 (𝜑 → ((⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩):(⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×c 𝑂))⟨𝐺, 𝑃⟩)⟶(((1st𝐸)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1st𝐸)‘⟨𝐺, 𝑃⟩)) ↔ (⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩):((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))⟶((𝐹(1st𝐸)𝑋)(Hom ‘𝑇)(𝐺(1st𝐸)𝑃))))
260253, 259mpbid 232 . . . . 5 (𝜑 → (⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩):((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))⟶((𝐹(1st𝐸)𝑋)(Hom ‘𝑇)(𝐺(1st𝐸)𝑃)))
261260, 34, 30fovcdmd 7605 . . . 4 (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)𝐾) ∈ ((𝐹(1st𝐸)𝑋)(Hom ‘𝑇)(𝐺(1st𝐸)𝑃)))
262169, 19, 167, 252, 248elsetchom 18126 . . . 4 (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)𝐾) ∈ ((𝐹(1st𝐸)𝑋)(Hom ‘𝑇)(𝐺(1st𝐸)𝑃)) ↔ (𝐴(⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)𝐾):(𝐹(1st𝐸)𝑋)⟶(𝐺(1st𝐸)𝑃)))
263261, 262mpbid 232 . . 3 (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)𝐾):(𝐹(1st𝐸)𝑋)⟶(𝐺(1st𝐸)𝑃))
264169, 19, 242, 196, 252, 248, 228, 263setcco 18128 . 2 (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)𝐾)(⟨(𝐹(1st𝑍)𝑋), (𝐹(1st𝐸)𝑋)⟩(comp‘𝑇)(𝐺(1st𝐸)𝑃))(𝐹𝑀𝑋)) = ((𝐴(⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)𝐾) ∘ (𝐹𝑀𝑋)))
265241, 250, 2643eqtr4d 2787 1 (𝜑 → ((𝐺𝑀𝑃)(⟨(𝐹(1st𝑍)𝑋), (𝐺(1st𝑍)𝑃)⟩(comp‘𝑇)(𝐺(1st𝐸)𝑃))(𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾)) = ((𝐴(⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)𝐾)(⟨(𝐹(1st𝑍)𝑋), (𝐹(1st𝐸)𝑋)⟩(comp‘𝑇)(𝐺(1st𝐸)𝑃))(𝐹𝑀𝑋)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  wcel 2108  wral 3061  Vcvv 3480  cun 3949  wss 3951  cop 4632   class class class wbr 5143  cmpt 5225   × cxp 5683  ran crn 5686  ccom 5689  Rel wrel 5690  wf 6557  cfv 6561  (class class class)co 7431  cmpo 7433  1st c1st 8012  2nd c2nd 8013  tpos ctpos 8250  Basecbs 17247  Hom chom 17308  compcco 17309  Catccat 17707  Idccid 17708  Homf chomf 17709  oppCatcoppc 17754   Func cfunc 17899  func ccofu 17901   Nat cnat 17989   FuncCat cfuc 17990  SetCatcsetc 18120   ×c cxpc 18213   1stF c1stf 18214   2ndF c2ndf 18215   ⟨,⟩F cprf 18216   evalF cevlf 18254  HomFchof 18293  Yoncyon 18294
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-tpos 8251  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-er 8745  df-map 8868  df-pm 8869  df-ixp 8938  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-z 12614  df-dec 12734  df-uz 12879  df-fz 13548  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-hom 17321  df-cco 17322  df-cat 17711  df-cid 17712  df-homf 17713  df-comf 17714  df-oppc 17755  df-ssc 17854  df-resc 17855  df-subc 17856  df-func 17903  df-cofu 17905  df-nat 17991  df-fuc 17992  df-setc 18121  df-xpc 18217  df-1stf 18218  df-2ndf 18219  df-prf 18220  df-evlf 18258  df-curf 18259  df-hof 18295  df-yon 18296
This theorem is referenced by:  yonedalem3  18325
  Copyright terms: Public domain W3C validator