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

Theorem yonedalem3b 17538
 Description: Lemma for yoneda 17542. (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 7150 . . . . . . . 8 (𝑏 = 𝑎 → (𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏) = (𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎))
21oveq1d 7157 . . . . . . 7 (𝑏 = 𝑎 → ((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾)) = ((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾)))
32fveq1d 6654 . . . . . 6 (𝑏 = 𝑎 → (((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃) = (((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃))
43fveq1d 6654 . . . . 5 (𝑏 = 𝑎 → ((((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃)‘( 1𝑃)) = ((((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃)‘( 1𝑃)))
54cbvmptv 5136 . . . 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 2798 . . . . . . . . 9 (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆)
8 yoneda.o . . . . . . . . . 10 𝑂 = (oppCat‘𝐶)
9 yoneda.b . . . . . . . . . 10 𝐵 = (Base‘𝐶)
108, 9oppcbas 16997 . . . . . . . . 9 𝐵 = (Base‘𝑂)
11 eqid 2798 . . . . . . . . 9 (comp‘𝑆) = (comp‘𝑆)
12 eqid 2798 . . . . . . . . 9 (comp‘𝑄) = (comp‘𝑄)
13 eqid 2798 . . . . . . . . . . . 12 (Hom ‘𝐶) = (Hom ‘𝐶)
146, 7fuchom 17240 . . . . . . . . . . . 12 (𝑂 Nat 𝑆) = (Hom ‘𝑄)
15 relfunc 17141 . . . . . . . . . . . . 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 4117 . . . . . . . . . . . . . . 15 (𝜑𝑈𝑉)
2219, 21ssexd 5195 . . . . . . . . . . . . . 14 (𝜑𝑈 ∈ V)
23 yoneda.u . . . . . . . . . . . . . 14 (𝜑 → ran (Homf𝐶) ⊆ 𝑈)
2416, 17, 8, 18, 6, 22, 23yoncl 17521 . . . . . . . . . . . . 13 (𝜑𝑌 ∈ (𝐶 Func 𝑄))
25 1st2ndbr 7733 . . . . . . . . . . . . 13 ((Rel (𝐶 Func 𝑄) ∧ 𝑌 ∈ (𝐶 Func 𝑄)) → (1st𝑌)(𝐶 Func 𝑄)(2nd𝑌))
2615, 24, 25sylancr 590 . . . . . . . . . . . 12 (𝜑 → (1st𝑌)(𝐶 Func 𝑄)(2nd𝑌))
27 yonedalem22.p . . . . . . . . . . . 12 (𝜑𝑃𝐵)
28 yonedalem21.x . . . . . . . . . . . 12 (𝜑𝑋𝐵)
299, 13, 14, 26, 27, 28funcf2 17147 . . . . . . . . . . 11 (𝜑 → (𝑃(2nd𝑌)𝑋):(𝑃(Hom ‘𝐶)𝑋)⟶(((1st𝑌)‘𝑃)(𝑂 Nat 𝑆)((1st𝑌)‘𝑋)))
30 yonedalem22.k . . . . . . . . . . 11 (𝜑𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋))
3129, 30ffvelrnd 6836 . . . . . . . . . 10 (𝜑 → ((𝑃(2nd𝑌)𝑋)‘𝐾) ∈ (((1st𝑌)‘𝑃)(𝑂 Nat 𝑆)((1st𝑌)‘𝑋)))
3231adantr 484 . . . . . . . . 9 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑃(2nd𝑌)𝑋)‘𝐾) ∈ (((1st𝑌)‘𝑃)(𝑂 Nat 𝑆)((1st𝑌)‘𝑋)))
33 simpr 488 . . . . . . . . . 10 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹))
34 yonedalem22.a . . . . . . . . . . 11 (𝜑𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺))
3534adantr 484 . . . . . . . . . 10 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺))
366, 7, 12, 33, 35fuccocl 17243 . . . . . . . . 9 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎) ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐺))
3727adantr 484 . . . . . . . . 9 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑃𝐵)
386, 7, 10, 11, 12, 32, 36, 37fuccoval 17242 . . . . . . . 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 17242 . . . . . . . . . 10 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)‘𝑃) = ((𝐴𝑃)(⟨((1st ‘((1st𝑌)‘𝑋))‘𝑃), ((1st𝐹)‘𝑃)⟩(comp‘𝑆)((1st𝐺)‘𝑃))(𝑎𝑃)))
4022adantr 484 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑈 ∈ V)
41 eqid 2798 . . . . . . . . . . . . . . 15 (Base‘𝑆) = (Base‘𝑆)
42 relfunc 17141 . . . . . . . . . . . . . . . 16 Rel (𝑂 Func 𝑆)
436fucbas 17239 . . . . . . . . . . . . . . . . . 18 (𝑂 Func 𝑆) = (Base‘𝑄)
449, 43, 26funcf1 17145 . . . . . . . . . . . . . . . . 17 (𝜑 → (1st𝑌):𝐵⟶(𝑂 Func 𝑆))
4544, 28ffvelrnd 6836 . . . . . . . . . . . . . . . 16 (𝜑 → ((1st𝑌)‘𝑋) ∈ (𝑂 Func 𝑆))
46 1st2ndbr 7733 . . . . . . . . . . . . . . . 16 ((Rel (𝑂 Func 𝑆) ∧ ((1st𝑌)‘𝑋) ∈ (𝑂 Func 𝑆)) → (1st ‘((1st𝑌)‘𝑋))(𝑂 Func 𝑆)(2nd ‘((1st𝑌)‘𝑋)))
4742, 45, 46sylancr 590 . . . . . . . . . . . . . . 15 (𝜑 → (1st ‘((1st𝑌)‘𝑋))(𝑂 Func 𝑆)(2nd ‘((1st𝑌)‘𝑋)))
4810, 41, 47funcf1 17145 . . . . . . . . . . . . . 14 (𝜑 → (1st ‘((1st𝑌)‘𝑋)):𝐵⟶(Base‘𝑆))
4918, 22setcbas 17347 . . . . . . . . . . . . . . 15 (𝜑𝑈 = (Base‘𝑆))
5049feq3d 6479 . . . . . . . . . . . . . 14 (𝜑 → ((1st ‘((1st𝑌)‘𝑋)):𝐵𝑈 ↔ (1st ‘((1st𝑌)‘𝑋)):𝐵⟶(Base‘𝑆)))
5148, 50mpbird 260 . . . . . . . . . . . . 13 (𝜑 → (1st ‘((1st𝑌)‘𝑋)):𝐵𝑈)
5251, 27ffvelrnd 6836 . . . . . . . . . . . 12 (𝜑 → ((1st ‘((1st𝑌)‘𝑋))‘𝑃) ∈ 𝑈)
5352adantr 484 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1st ‘((1st𝑌)‘𝑋))‘𝑃) ∈ 𝑈)
54 yonedalem21.f . . . . . . . . . . . . . . . 16 (𝜑𝐹 ∈ (𝑂 Func 𝑆))
55 1st2ndbr 7733 . . . . . . . . . . . . . . . 16 ((Rel (𝑂 Func 𝑆) ∧ 𝐹 ∈ (𝑂 Func 𝑆)) → (1st𝐹)(𝑂 Func 𝑆)(2nd𝐹))
5642, 54, 55sylancr 590 . . . . . . . . . . . . . . 15 (𝜑 → (1st𝐹)(𝑂 Func 𝑆)(2nd𝐹))
5710, 41, 56funcf1 17145 . . . . . . . . . . . . . 14 (𝜑 → (1st𝐹):𝐵⟶(Base‘𝑆))
5849feq3d 6479 . . . . . . . . . . . . . 14 (𝜑 → ((1st𝐹):𝐵𝑈 ↔ (1st𝐹):𝐵⟶(Base‘𝑆)))
5957, 58mpbird 260 . . . . . . . . . . . . 13 (𝜑 → (1st𝐹):𝐵𝑈)
6059, 27ffvelrnd 6836 . . . . . . . . . . . 12 (𝜑 → ((1st𝐹)‘𝑃) ∈ 𝑈)
6160adantr 484 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1st𝐹)‘𝑃) ∈ 𝑈)
62 yonedalem22.g . . . . . . . . . . . . . . . 16 (𝜑𝐺 ∈ (𝑂 Func 𝑆))
63 1st2ndbr 7733 . . . . . . . . . . . . . . . 16 ((Rel (𝑂 Func 𝑆) ∧ 𝐺 ∈ (𝑂 Func 𝑆)) → (1st𝐺)(𝑂 Func 𝑆)(2nd𝐺))
6442, 62, 63sylancr 590 . . . . . . . . . . . . . . 15 (𝜑 → (1st𝐺)(𝑂 Func 𝑆)(2nd𝐺))
6510, 41, 64funcf1 17145 . . . . . . . . . . . . . 14 (𝜑 → (1st𝐺):𝐵⟶(Base‘𝑆))
6665, 27ffvelrnd 6836 . . . . . . . . . . . . 13 (𝜑 → ((1st𝐺)‘𝑃) ∈ (Base‘𝑆))
6766, 49eleqtrrd 2893 . . . . . . . . . . . 12 (𝜑 → ((1st𝐺)‘𝑃) ∈ 𝑈)
6867adantr 484 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1st𝐺)‘𝑃) ∈ 𝑈)
697, 33nat1st2nd 17230 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑎 ∈ (⟨(1st ‘((1st𝑌)‘𝑋)), (2nd ‘((1st𝑌)‘𝑋))⟩(𝑂 Nat 𝑆)⟨(1st𝐹), (2nd𝐹)⟩))
70 eqid 2798 . . . . . . . . . . . . 13 (Hom ‘𝑆) = (Hom ‘𝑆)
717, 69, 10, 70, 37natcl 17232 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝑎𝑃) ∈ (((1st ‘((1st𝑌)‘𝑋))‘𝑃)(Hom ‘𝑆)((1st𝐹)‘𝑃)))
7218, 40, 70, 53, 61elsetchom 17350 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎𝑃) ∈ (((1st ‘((1st𝑌)‘𝑋))‘𝑃)(Hom ‘𝑆)((1st𝐹)‘𝑃)) ↔ (𝑎𝑃):((1st ‘((1st𝑌)‘𝑋))‘𝑃)⟶((1st𝐹)‘𝑃)))
7371, 72mpbid 235 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝑎𝑃):((1st ‘((1st𝑌)‘𝑋))‘𝑃)⟶((1st𝐹)‘𝑃))
747, 34nat1st2nd 17230 . . . . . . . . . . . . . 14 (𝜑𝐴 ∈ (⟨(1st𝐹), (2nd𝐹)⟩(𝑂 Nat 𝑆)⟨(1st𝐺), (2nd𝐺)⟩))
757, 74, 10, 70, 27natcl 17232 . . . . . . . . . . . . 13 (𝜑 → (𝐴𝑃) ∈ (((1st𝐹)‘𝑃)(Hom ‘𝑆)((1st𝐺)‘𝑃)))
7618, 22, 70, 60, 67elsetchom 17350 . . . . . . . . . . . . 13 (𝜑 → ((𝐴𝑃) ∈ (((1st𝐹)‘𝑃)(Hom ‘𝑆)((1st𝐺)‘𝑃)) ↔ (𝐴𝑃):((1st𝐹)‘𝑃)⟶((1st𝐺)‘𝑃)))
7775, 76mpbid 235 . . . . . . . . . . . 12 (𝜑 → (𝐴𝑃):((1st𝐹)‘𝑃)⟶((1st𝐺)‘𝑃))
7877adantr 484 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝐴𝑃):((1st𝐹)‘𝑃)⟶((1st𝐺)‘𝑃))
7918, 40, 11, 53, 61, 68, 73, 78setcco 17352 . . . . . . . . . 10 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴𝑃)(⟨((1st ‘((1st𝑌)‘𝑋))‘𝑃), ((1st𝐹)‘𝑃)⟩(comp‘𝑆)((1st𝐺)‘𝑃))(𝑎𝑃)) = ((𝐴𝑃) ∘ (𝑎𝑃)))
8039, 79eqtrd 2833 . . . . . . . . 9 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)‘𝑃) = ((𝐴𝑃) ∘ (𝑎𝑃)))
8180oveq1d 7157 . . . . . . . 8 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)‘𝑃)(⟨((1st ‘((1st𝑌)‘𝑃))‘𝑃), ((1st ‘((1st𝑌)‘𝑋))‘𝑃)⟩(comp‘𝑆)((1st𝐺)‘𝑃))(((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)) = (((𝐴𝑃) ∘ (𝑎𝑃))(⟨((1st ‘((1st𝑌)‘𝑃))‘𝑃), ((1st ‘((1st𝑌)‘𝑋))‘𝑃)⟩(comp‘𝑆)((1st𝐺)‘𝑃))(((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)))
8244, 27ffvelrnd 6836 . . . . . . . . . . . . . 14 (𝜑 → ((1st𝑌)‘𝑃) ∈ (𝑂 Func 𝑆))
83 1st2ndbr 7733 . . . . . . . . . . . . . 14 ((Rel (𝑂 Func 𝑆) ∧ ((1st𝑌)‘𝑃) ∈ (𝑂 Func 𝑆)) → (1st ‘((1st𝑌)‘𝑃))(𝑂 Func 𝑆)(2nd ‘((1st𝑌)‘𝑃)))
8442, 82, 83sylancr 590 . . . . . . . . . . . . 13 (𝜑 → (1st ‘((1st𝑌)‘𝑃))(𝑂 Func 𝑆)(2nd ‘((1st𝑌)‘𝑃)))
8510, 41, 84funcf1 17145 . . . . . . . . . . . 12 (𝜑 → (1st ‘((1st𝑌)‘𝑃)):𝐵⟶(Base‘𝑆))
8685, 27ffvelrnd 6836 . . . . . . . . . . 11 (𝜑 → ((1st ‘((1st𝑌)‘𝑃))‘𝑃) ∈ (Base‘𝑆))
8786, 49eleqtrrd 2893 . . . . . . . . . 10 (𝜑 → ((1st ‘((1st𝑌)‘𝑃))‘𝑃) ∈ 𝑈)
8887adantr 484 . . . . . . . . 9 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1st ‘((1st𝑌)‘𝑃))‘𝑃) ∈ 𝑈)
897, 31nat1st2nd 17230 . . . . . . . . . . . 12 (𝜑 → ((𝑃(2nd𝑌)𝑋)‘𝐾) ∈ (⟨(1st ‘((1st𝑌)‘𝑃)), (2nd ‘((1st𝑌)‘𝑃))⟩(𝑂 Nat 𝑆)⟨(1st ‘((1st𝑌)‘𝑋)), (2nd ‘((1st𝑌)‘𝑋))⟩))
907, 89, 10, 70, 27natcl 17232 . . . . . . . . . . 11 (𝜑 → (((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃) ∈ (((1st ‘((1st𝑌)‘𝑃))‘𝑃)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑋))‘𝑃)))
9118, 22, 70, 87, 52elsetchom 17350 . . . . . . . . . . 11 (𝜑 → ((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃) ∈ (((1st ‘((1st𝑌)‘𝑃))‘𝑃)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑋))‘𝑃)) ↔ (((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃):((1st ‘((1st𝑌)‘𝑃))‘𝑃)⟶((1st ‘((1st𝑌)‘𝑋))‘𝑃)))
9290, 91mpbid 235 . . . . . . . . . 10 (𝜑 → (((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃):((1st ‘((1st𝑌)‘𝑃))‘𝑃)⟶((1st ‘((1st𝑌)‘𝑋))‘𝑃))
9392adantr 484 . . . . . . . . 9 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃):((1st ‘((1st𝑌)‘𝑃))‘𝑃)⟶((1st ‘((1st𝑌)‘𝑋))‘𝑃))
94 fco 6510 . . . . . . . . . 10 (((𝐴𝑃):((1st𝐹)‘𝑃)⟶((1st𝐺)‘𝑃) ∧ (𝑎𝑃):((1st ‘((1st𝑌)‘𝑋))‘𝑃)⟶((1st𝐹)‘𝑃)) → ((𝐴𝑃) ∘ (𝑎𝑃)):((1st ‘((1st𝑌)‘𝑋))‘𝑃)⟶((1st𝐺)‘𝑃))
9578, 73, 94syl2anc 587 . . . . . . . . 9 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴𝑃) ∘ (𝑎𝑃)):((1st ‘((1st𝑌)‘𝑋))‘𝑃)⟶((1st𝐺)‘𝑃))
9618, 40, 11, 88, 53, 68, 93, 95setcco 17352 . . . . . . . 8 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴𝑃) ∘ (𝑎𝑃))(⟨((1st ‘((1st𝑌)‘𝑃))‘𝑃), ((1st ‘((1st𝑌)‘𝑋))‘𝑃)⟩(comp‘𝑆)((1st𝐺)‘𝑃))(((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)) = (((𝐴𝑃) ∘ (𝑎𝑃)) ∘ (((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)))
9738, 81, 963eqtrd 2837 . . . . . . 7 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃) = (((𝐴𝑃) ∘ (𝑎𝑃)) ∘ (((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)))
9897fveq1d 6654 . . . . . 6 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃)‘( 1𝑃)) = ((((𝐴𝑃) ∘ (𝑎𝑃)) ∘ (((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃))‘( 1𝑃)))
99 yoneda.1 . . . . . . . . . 10 1 = (Id‘𝐶)
1009, 13, 99, 17, 27catidcl 16962 . . . . . . . . 9 (𝜑 → ( 1𝑃) ∈ (𝑃(Hom ‘𝐶)𝑃))
10116, 9, 17, 27, 13, 27yon11 17523 . . . . . . . . 9 (𝜑 → ((1st ‘((1st𝑌)‘𝑃))‘𝑃) = (𝑃(Hom ‘𝐶)𝑃))
102100, 101eleqtrrd 2893 . . . . . . . 8 (𝜑 → ( 1𝑃) ∈ ((1st ‘((1st𝑌)‘𝑃))‘𝑃))
103102adantr 484 . . . . . . 7 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1𝑃) ∈ ((1st ‘((1st𝑌)‘𝑃))‘𝑃))
104 fvco3 6744 . . . . . . 7 (((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃):((1st ‘((1st𝑌)‘𝑃))‘𝑃)⟶((1st ‘((1st𝑌)‘𝑋))‘𝑃) ∧ ( 1𝑃) ∈ ((1st ‘((1st𝑌)‘𝑃))‘𝑃)) → ((((𝐴𝑃) ∘ (𝑎𝑃)) ∘ (((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃))‘( 1𝑃)) = (((𝐴𝑃) ∘ (𝑎𝑃))‘((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃))))
10593, 103, 104syl2anc 587 . . . . . 6 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝐴𝑃) ∘ (𝑎𝑃)) ∘ (((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃))‘( 1𝑃)) = (((𝐴𝑃) ∘ (𝑎𝑃))‘((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃))))
10693, 103ffvelrnd 6836 . . . . . . . 8 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃)) ∈ ((1st ‘((1st𝑌)‘𝑋))‘𝑃))
107 fvco3 6744 . . . . . . . 8 (((𝑎𝑃):((1st ‘((1st𝑌)‘𝑋))‘𝑃)⟶((1st𝐹)‘𝑃) ∧ ((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃)) ∈ ((1st ‘((1st𝑌)‘𝑋))‘𝑃)) → (((𝐴𝑃) ∘ (𝑎𝑃))‘((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃))) = ((𝐴𝑃)‘((𝑎𝑃)‘((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃)))))
10873, 106, 107syl2anc 587 . . . . . . 7 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴𝑃) ∘ (𝑎𝑃))‘((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃))) = ((𝐴𝑃)‘((𝑎𝑃)‘((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃)))))
10917adantr 484 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐶 ∈ Cat)
11028adantr 484 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑋𝐵)
111 eqid 2798 . . . . . . . . . . . 12 (comp‘𝐶) = (comp‘𝐶)
11230adantr 484 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋))
113100adantr 484 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1𝑃) ∈ (𝑃(Hom ‘𝐶)𝑃))
11416, 9, 109, 37, 13, 110, 111, 37, 112, 113yon2 17525 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃)) = (𝐾(⟨𝑃, 𝑃⟩(comp‘𝐶)𝑋)( 1𝑃)))
1159, 13, 99, 109, 37, 111, 110, 112catrid 16964 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝐾(⟨𝑃, 𝑃⟩(comp‘𝐶)𝑋)( 1𝑃)) = 𝐾)
116114, 115eqtrd 2833 . . . . . . . . . 10 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃)) = 𝐾)
117116fveq2d 6656 . . . . . . . . 9 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎𝑃)‘((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃))) = ((𝑎𝑃)‘𝐾))
118 eqid 2798 . . . . . . . . . . . . . . 15 (Hom ‘𝑂) = (Hom ‘𝑂)
11910, 118, 70, 47, 28, 27funcf2 17147 . . . . . . . . . . . . . 14 (𝜑 → (𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃):(𝑋(Hom ‘𝑂)𝑃)⟶(((1st ‘((1st𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑋))‘𝑃)))
12013, 8oppchom 16994 . . . . . . . . . . . . . . 15 (𝑋(Hom ‘𝑂)𝑃) = (𝑃(Hom ‘𝐶)𝑋)
12130, 120eleqtrrdi 2901 . . . . . . . . . . . . . 14 (𝜑𝐾 ∈ (𝑋(Hom ‘𝑂)𝑃))
122119, 121ffvelrnd 6836 . . . . . . . . . . . . 13 (𝜑 → ((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾) ∈ (((1st ‘((1st𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑋))‘𝑃)))
12351, 28ffvelrnd 6836 . . . . . . . . . . . . . 14 (𝜑 → ((1st ‘((1st𝑌)‘𝑋))‘𝑋) ∈ 𝑈)
12418, 22, 70, 123, 52elsetchom 17350 . . . . . . . . . . . . 13 (𝜑 → (((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾) ∈ (((1st ‘((1st𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑋))‘𝑃)) ↔ ((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾):((1st ‘((1st𝑌)‘𝑋))‘𝑋)⟶((1st ‘((1st𝑌)‘𝑋))‘𝑃)))
125122, 124mpbid 235 . . . . . . . . . . . 12 (𝜑 → ((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾):((1st ‘((1st𝑌)‘𝑋))‘𝑋)⟶((1st ‘((1st𝑌)‘𝑋))‘𝑃))
126125adantr 484 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾):((1st ‘((1st𝑌)‘𝑋))‘𝑋)⟶((1st ‘((1st𝑌)‘𝑋))‘𝑃))
1279, 13, 99, 17, 28catidcl 16962 . . . . . . . . . . . . 13 (𝜑 → ( 1𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋))
12816, 9, 17, 28, 13, 28yon11 17523 . . . . . . . . . . . . 13 (𝜑 → ((1st ‘((1st𝑌)‘𝑋))‘𝑋) = (𝑋(Hom ‘𝐶)𝑋))
129127, 128eleqtrrd 2893 . . . . . . . . . . . 12 (𝜑 → ( 1𝑋) ∈ ((1st ‘((1st𝑌)‘𝑋))‘𝑋))
130129adantr 484 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1𝑋) ∈ ((1st ‘((1st𝑌)‘𝑋))‘𝑋))
131 fvco3 6744 . . . . . . . . . . 11 ((((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾):((1st ‘((1st𝑌)‘𝑋))‘𝑋)⟶((1st ‘((1st𝑌)‘𝑋))‘𝑃) ∧ ( 1𝑋) ∈ ((1st ‘((1st𝑌)‘𝑋))‘𝑋)) → (((𝑎𝑃) ∘ ((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾))‘( 1𝑋)) = ((𝑎𝑃)‘(((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾)‘( 1𝑋))))
132126, 130, 131syl2anc 587 . . . . . . . . . 10 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑎𝑃) ∘ ((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾))‘( 1𝑋)) = ((𝑎𝑃)‘(((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾)‘( 1𝑋))))
133121adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐾 ∈ (𝑋(Hom ‘𝑂)𝑃))
1347, 69, 10, 118, 11, 110, 37, 133nati 17234 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎𝑃)(⟨((1st ‘((1st𝑌)‘𝑋))‘𝑋), ((1st ‘((1st𝑌)‘𝑋))‘𝑃)⟩(comp‘𝑆)((1st𝐹)‘𝑃))((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾)) = (((𝑋(2nd𝐹)𝑃)‘𝐾)(⟨((1st ‘((1st𝑌)‘𝑋))‘𝑋), ((1st𝐹)‘𝑋)⟩(comp‘𝑆)((1st𝐹)‘𝑃))(𝑎𝑋)))
135123adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1st ‘((1st𝑌)‘𝑋))‘𝑋) ∈ 𝑈)
13618, 40, 11, 135, 53, 61, 126, 73setcco 17352 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎𝑃)(⟨((1st ‘((1st𝑌)‘𝑋))‘𝑋), ((1st ‘((1st𝑌)‘𝑋))‘𝑃)⟩(comp‘𝑆)((1st𝐹)‘𝑃))((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾)) = ((𝑎𝑃) ∘ ((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾)))
13759, 28ffvelrnd 6836 . . . . . . . . . . . . . 14 (𝜑 → ((1st𝐹)‘𝑋) ∈ 𝑈)
138137adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1st𝐹)‘𝑋) ∈ 𝑈)
1397, 69, 10, 70, 110natcl 17232 . . . . . . . . . . . . . 14 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝑎𝑋) ∈ (((1st ‘((1st𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1st𝐹)‘𝑋)))
14018, 40, 70, 135, 138elsetchom 17350 . . . . . . . . . . . . . 14 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎𝑋) ∈ (((1st ‘((1st𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1st𝐹)‘𝑋)) ↔ (𝑎𝑋):((1st ‘((1st𝑌)‘𝑋))‘𝑋)⟶((1st𝐹)‘𝑋)))
141139, 140mpbid 235 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝑎𝑋):((1st ‘((1st𝑌)‘𝑋))‘𝑋)⟶((1st𝐹)‘𝑋))
14210, 118, 70, 56, 28, 27funcf2 17147 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑋(2nd𝐹)𝑃):(𝑋(Hom ‘𝑂)𝑃)⟶(((1st𝐹)‘𝑋)(Hom ‘𝑆)((1st𝐹)‘𝑃)))
143142, 121ffvelrnd 6836 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑋(2nd𝐹)𝑃)‘𝐾) ∈ (((1st𝐹)‘𝑋)(Hom ‘𝑆)((1st𝐹)‘𝑃)))
14418, 22, 70, 137, 60elsetchom 17350 . . . . . . . . . . . . . . 15 (𝜑 → (((𝑋(2nd𝐹)𝑃)‘𝐾) ∈ (((1st𝐹)‘𝑋)(Hom ‘𝑆)((1st𝐹)‘𝑃)) ↔ ((𝑋(2nd𝐹)𝑃)‘𝐾):((1st𝐹)‘𝑋)⟶((1st𝐹)‘𝑃)))
145143, 144mpbid 235 . . . . . . . . . . . . . 14 (𝜑 → ((𝑋(2nd𝐹)𝑃)‘𝐾):((1st𝐹)‘𝑋)⟶((1st𝐹)‘𝑃))
146145adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑋(2nd𝐹)𝑃)‘𝐾):((1st𝐹)‘𝑋)⟶((1st𝐹)‘𝑃))
14718, 40, 11, 135, 138, 61, 141, 146setcco 17352 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑋(2nd𝐹)𝑃)‘𝐾)(⟨((1st ‘((1st𝑌)‘𝑋))‘𝑋), ((1st𝐹)‘𝑋)⟩(comp‘𝑆)((1st𝐹)‘𝑃))(𝑎𝑋)) = (((𝑋(2nd𝐹)𝑃)‘𝐾) ∘ (𝑎𝑋)))
148134, 136, 1473eqtr3d 2841 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎𝑃) ∘ ((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾)) = (((𝑋(2nd𝐹)𝑃)‘𝐾) ∘ (𝑎𝑋)))
149148fveq1d 6654 . . . . . . . . . 10 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑎𝑃) ∘ ((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾))‘( 1𝑋)) = ((((𝑋(2nd𝐹)𝑃)‘𝐾) ∘ (𝑎𝑋))‘( 1𝑋)))
150127adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋))
15116, 9, 109, 110, 13, 110, 111, 37, 112, 150yon12 17524 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾)‘( 1𝑋)) = (( 1𝑋)(⟨𝑃, 𝑋⟩(comp‘𝐶)𝑋)𝐾))
1529, 13, 99, 109, 37, 111, 110, 112catlid 16963 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (( 1𝑋)(⟨𝑃, 𝑋⟩(comp‘𝐶)𝑋)𝐾) = 𝐾)
153151, 152eqtrd 2833 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾)‘( 1𝑋)) = 𝐾)
154153fveq2d 6656 . . . . . . . . . 10 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎𝑃)‘(((𝑋(2nd ‘((1st𝑌)‘𝑋))𝑃)‘𝐾)‘( 1𝑋))) = ((𝑎𝑃)‘𝐾))
155132, 149, 1543eqtr3d 2841 . . . . . . . . 9 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑋(2nd𝐹)𝑃)‘𝐾) ∘ (𝑎𝑋))‘( 1𝑋)) = ((𝑎𝑃)‘𝐾))
156 fvco3 6744 . . . . . . . . . 10 (((𝑎𝑋):((1st ‘((1st𝑌)‘𝑋))‘𝑋)⟶((1st𝐹)‘𝑋) ∧ ( 1𝑋) ∈ ((1st ‘((1st𝑌)‘𝑋))‘𝑋)) → ((((𝑋(2nd𝐹)𝑃)‘𝐾) ∘ (𝑎𝑋))‘( 1𝑋)) = (((𝑋(2nd𝐹)𝑃)‘𝐾)‘((𝑎𝑋)‘( 1𝑋))))
157141, 130, 156syl2anc 587 . . . . . . . . 9 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑋(2nd𝐹)𝑃)‘𝐾) ∘ (𝑎𝑋))‘( 1𝑋)) = (((𝑋(2nd𝐹)𝑃)‘𝐾)‘((𝑎𝑋)‘( 1𝑋))))
158117, 155, 1573eqtr2d 2839 . . . . . . . 8 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎𝑃)‘((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃))) = (((𝑋(2nd𝐹)𝑃)‘𝐾)‘((𝑎𝑋)‘( 1𝑋))))
159158fveq2d 6656 . . . . . . 7 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴𝑃)‘((𝑎𝑃)‘((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃)))) = ((𝐴𝑃)‘(((𝑋(2nd𝐹)𝑃)‘𝐾)‘((𝑎𝑋)‘( 1𝑋)))))
160108, 159eqtrd 2833 . . . . . 6 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴𝑃) ∘ (𝑎𝑃))‘((((𝑃(2nd𝑌)𝑋)‘𝐾)‘𝑃)‘( 1𝑃))) = ((𝐴𝑃)‘(((𝑋(2nd𝐹)𝑃)‘𝐾)‘((𝑎𝑋)‘( 1𝑋)))))
16198, 105, 1603eqtrd 2837 . . . . 5 ((𝜑𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃)‘( 1𝑃)) = ((𝐴𝑃)‘(((𝑋(2nd𝐹)𝑃)‘𝐾)‘((𝑎𝑋)‘( 1𝑋)))))
162161mpteq2dva 5128 . . . 4 (𝜑 → (𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃)‘( 1𝑃))) = (𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴𝑃)‘(((𝑋(2nd𝐹)𝑃)‘𝐾)‘((𝑎𝑋)‘( 1𝑋))))))
1635, 162syl5eq 2845 . . 3 (𝜑 → (𝑏 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃)‘( 1𝑃))) = (𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴𝑃)‘(((𝑋(2nd𝐹)𝑃)‘𝐾)‘((𝑎𝑋)‘( 1𝑋))))))
164 eqid 2798 . . . . . . . . . . 11 (𝑄 ×c 𝑂) = (𝑄 ×c 𝑂)
165164, 43, 10xpcbas 17437 . . . . . . . . . 10 ((𝑂 Func 𝑆) × 𝐵) = (Base‘(𝑄 ×c 𝑂))
166 eqid 2798 . . . . . . . . . 10 (Hom ‘(𝑄 ×c 𝑂)) = (Hom ‘(𝑄 ×c 𝑂))
167 eqid 2798 . . . . . . . . . 10 (Hom ‘𝑇) = (Hom ‘𝑇)
168 relfunc 17141 . . . . . . . . . . 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 17531 . . . . . . . . . . . 12 (𝜑 → (𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)))
175174simpld 498 . . . . . . . . . . 11 (𝜑𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇))
176 1st2ndbr 7733 . . . . . . . . . . 11 ((Rel ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st𝑍)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝑍))
177168, 175, 176sylancr 590 . . . . . . . . . 10 (𝜑 → (1st𝑍)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝑍))
17854, 28opelxpd 5560 . . . . . . . . . 10 (𝜑 → ⟨𝐹, 𝑋⟩ ∈ ((𝑂 Func 𝑆) × 𝐵))
17962, 27opelxpd 5560 . . . . . . . . . 10 (𝜑 → ⟨𝐺, 𝑃⟩ ∈ ((𝑂 Func 𝑆) × 𝐵))
180165, 166, 167, 177, 178, 179funcf2 17147 . . . . . . . . 9 (𝜑 → (⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩):(⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×c 𝑂))⟨𝐺, 𝑃⟩)⟶(((1st𝑍)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1st𝑍)‘⟨𝐺, 𝑃⟩)))
181164, 43, 10, 14, 118, 54, 28, 62, 27, 166xpchom2 17445 . . . . . . . . . . 11 (𝜑 → (⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×c 𝑂))⟨𝐺, 𝑃⟩) = ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑋(Hom ‘𝑂)𝑃)))
182120xpeq2i 5549 . . . . . . . . . . 11 ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑋(Hom ‘𝑂)𝑃)) = ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))
183181, 182eqtrdi 2849 . . . . . . . . . 10 (𝜑 → (⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×c 𝑂))⟨𝐺, 𝑃⟩) = ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋)))
184 df-ov 7145 . . . . . . . . . . . . 13 (𝐹(1st𝑍)𝑋) = ((1st𝑍)‘⟨𝐹, 𝑋⟩)
185 df-ov 7145 . . . . . . . . . . . . 13 (𝐺(1st𝑍)𝑃) = ((1st𝑍)‘⟨𝐺, 𝑃⟩)
186184, 185oveq12i 7154 . . . . . . . . . . . 12 ((𝐹(1st𝑍)𝑋)(Hom ‘𝑇)(𝐺(1st𝑍)𝑃)) = (((1st𝑍)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1st𝑍)‘⟨𝐺, 𝑃⟩))
187186eqcomi 2807 . . . . . . . . . . 11 (((1st𝑍)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1st𝑍)‘⟨𝐺, 𝑃⟩)) = ((𝐹(1st𝑍)𝑋)(Hom ‘𝑇)(𝐺(1st𝑍)𝑃))
188187a1i 11 . . . . . . . . . 10 (𝜑 → (((1st𝑍)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1st𝑍)‘⟨𝐺, 𝑃⟩)) = ((𝐹(1st𝑍)𝑋)(Hom ‘𝑇)(𝐺(1st𝑍)𝑃)))
189183, 188feq23d 6487 . . . . . . . . 9 (𝜑 → ((⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩):(⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×c 𝑂))⟨𝐺, 𝑃⟩)⟶(((1st𝑍)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1st𝑍)‘⟨𝐺, 𝑃⟩)) ↔ (⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩):((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))⟶((𝐹(1st𝑍)𝑋)(Hom ‘𝑇)(𝐺(1st𝑍)𝑃))))
190180, 189mpbid 235 . . . . . . . 8 (𝜑 → (⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩):((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))⟶((𝐹(1st𝑍)𝑋)(Hom ‘𝑇)(𝐺(1st𝑍)𝑃)))
191190, 34, 30fovrnd 7308 . . . . . . 7 (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾) ∈ ((𝐹(1st𝑍)𝑋)(Hom ‘𝑇)(𝐺(1st𝑍)𝑃)))
192 eqid 2798 . . . . . . . . . . 11 (Base‘𝑇) = (Base‘𝑇)
193165, 192, 177funcf1 17145 . . . . . . . . . 10 (𝜑 → (1st𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
194193, 54, 28fovrnd 7308 . . . . . . . . 9 (𝜑 → (𝐹(1st𝑍)𝑋) ∈ (Base‘𝑇))
195169, 19setcbas 17347 . . . . . . . . 9 (𝜑𝑉 = (Base‘𝑇))
196194, 195eleqtrrd 2893 . . . . . . . 8 (𝜑 → (𝐹(1st𝑍)𝑋) ∈ 𝑉)
197193, 62, 27fovrnd 7308 . . . . . . . . 9 (𝜑 → (𝐺(1st𝑍)𝑃) ∈ (Base‘𝑇))
198197, 195eleqtrrd 2893 . . . . . . . 8 (𝜑 → (𝐺(1st𝑍)𝑃) ∈ 𝑉)
199169, 19, 167, 196, 198elsetchom 17350 . . . . . . 7 (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾) ∈ ((𝐹(1st𝑍)𝑋)(Hom ‘𝑇)(𝐺(1st𝑍)𝑃)) ↔ (𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾):(𝐹(1st𝑍)𝑋)⟶(𝐺(1st𝑍)𝑃)))
200191, 199mpbid 235 . . . . . 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 17537 . . . . . . . 8 (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾) = (((𝑃(2nd𝑌)𝑋)‘𝐾)(⟨((1st𝑌)‘𝑋), 𝐹⟩(2nd𝐻)⟨((1st𝑌)‘𝑃), 𝐺⟩)𝐴))
2028oppccat 17001 . . . . . . . . . . 11 (𝐶 ∈ Cat → 𝑂 ∈ Cat)
20317, 202syl 17 . . . . . . . . . 10 (𝜑𝑂 ∈ Cat)
20418setccat 17354 . . . . . . . . . . 11 (𝑈 ∈ V → 𝑆 ∈ Cat)
20522, 204syl 17 . . . . . . . . . 10 (𝜑𝑆 ∈ Cat)
2066, 203, 205fuccat 17249 . . . . . . . . 9 (𝜑𝑄 ∈ Cat)
207170, 206, 43, 14, 45, 54, 82, 62, 12, 31, 34hof2val 17515 . . . . . . . 8 (𝜑 → (((𝑃(2nd𝑌)𝑋)‘𝐾)(⟨((1st𝑌)‘𝑋), 𝐹⟩(2nd𝐻)⟨((1st𝑌)‘𝑃), 𝐺⟩)𝐴) = (𝑏 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))))
208201, 207eqtrd 2833 . . . . . . 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 17532 . . . . . . 7 (𝜑 → (𝐹(1st𝑍)𝑋) = (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹))
21016, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 62, 27yonedalem21 17532 . . . . . . 7 (𝜑 → (𝐺(1st𝑍)𝑃) = (((1st𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺))
211208, 209, 210feq123d 6481 . . . . . 6 (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾):(𝐹(1st𝑍)𝑋)⟶(𝐺(1st𝑍)𝑃) ↔ (𝑏 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))):(((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)⟶(((1st𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺)))
212200, 211mpbid 235 . . . . 5 (𝜑 → (𝑏 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))):(((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)⟶(((1st𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺))
213 eqid 2798 . . . . . 6 (𝑏 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))) = (𝑏 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾)))
214213fmpt 6858 . . . . 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 237 . . . 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 17533 . . . . 5 (𝜑 → ((𝐺𝑀𝑃) = (𝑎 ∈ (((1st𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺) ↦ ((𝑎𝑃)‘( 1𝑃))) ∧ (𝐺𝑀𝑃):(𝐺(1st𝑍)𝑃)⟶(𝐺(1st𝐸)𝑃)))
218217simpld 498 . . . 4 (𝜑 → (𝐺𝑀𝑃) = (𝑎 ∈ (((1st𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺) ↦ ((𝑎𝑃)‘( 1𝑃))))
219 fveq1 6651 . . . . 5 (𝑎 = ((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾)) → (𝑎𝑃) = (((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃))
220219fveq1d 6654 . . . 4 (𝑎 = ((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾)) → ((𝑎𝑃)‘( 1𝑃)) = ((((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃)‘( 1𝑃)))
221215, 208, 218, 220fmptcof 6876 . . 3 (𝜑 → ((𝐺𝑀𝑃) ∘ (𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾)) = (𝑏 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((((𝐴(⟨((1st𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1st𝑌)‘𝑃), ((1st𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2nd𝑌)𝑋)‘𝐾))‘𝑃)‘( 1𝑃))))
222 eqid 2798 . . . . . . 7 (⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩) = (⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)
223172, 203, 205, 10, 118, 11, 7, 54, 62, 28, 27, 222, 34, 121evlf2val 17478 . . . . . 6 (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)𝐾) = ((𝐴𝑃)(⟨((1st𝐹)‘𝑋), ((1st𝐹)‘𝑃)⟩(comp‘𝑆)((1st𝐺)‘𝑃))((𝑋(2nd𝐹)𝑃)‘𝐾)))
22418, 22, 11, 137, 60, 67, 145, 77setcco 17352 . . . . . 6 (𝜑 → ((𝐴𝑃)(⟨((1st𝐹)‘𝑋), ((1st𝐹)‘𝑃)⟩(comp‘𝑆)((1st𝐺)‘𝑃))((𝑋(2nd𝐹)𝑃)‘𝐾)) = ((𝐴𝑃) ∘ ((𝑋(2nd𝐹)𝑃)‘𝐾)))
225223, 224eqtrd 2833 . . . . 5 (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)𝐾) = ((𝐴𝑃) ∘ ((𝑋(2nd𝐹)𝑃)‘𝐾)))
226225coeq1d 5699 . . . 4 (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)𝐾) ∘ (𝐹𝑀𝑋)) = (((𝐴𝑃) ∘ ((𝑋(2nd𝐹)𝑃)‘𝐾)) ∘ (𝐹𝑀𝑋)))
22716, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 54, 28, 216yonedalem3a 17533 . . . . . . . 8 (𝜑 → ((𝐹𝑀𝑋) = (𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎𝑋)‘( 1𝑋))) ∧ (𝐹𝑀𝑋):(𝐹(1st𝑍)𝑋)⟶(𝐹(1st𝐸)𝑋)))
228227simprd 499 . . . . . . 7 (𝜑 → (𝐹𝑀𝑋):(𝐹(1st𝑍)𝑋)⟶(𝐹(1st𝐸)𝑋))
229227simpld 498 . . . . . . . 8 (𝜑 → (𝐹𝑀𝑋) = (𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎𝑋)‘( 1𝑋))))
230172, 203, 205, 10, 54, 28evlf1 17479 . . . . . . . 8 (𝜑 → (𝐹(1st𝐸)𝑋) = ((1st𝐹)‘𝑋))
231229, 209, 230feq123d 6481 . . . . . . 7 (𝜑 → ((𝐹𝑀𝑋):(𝐹(1st𝑍)𝑋)⟶(𝐹(1st𝐸)𝑋) ↔ (𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎𝑋)‘( 1𝑋))):(((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)⟶((1st𝐹)‘𝑋)))
232228, 231mpbid 235 . . . . . 6 (𝜑 → (𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎𝑋)‘( 1𝑋))):(((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)⟶((1st𝐹)‘𝑋))
233 eqid 2798 . . . . . . 7 (𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎𝑋)‘( 1𝑋))) = (𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎𝑋)‘( 1𝑋)))
234233fmpt 6858 . . . . . 6 (∀𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)((𝑎𝑋)‘( 1𝑋)) ∈ ((1st𝐹)‘𝑋) ↔ (𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎𝑋)‘( 1𝑋))):(((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)⟶((1st𝐹)‘𝑋))
235232, 234sylibr 237 . . . . 5 (𝜑 → ∀𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)((𝑎𝑋)‘( 1𝑋)) ∈ ((1st𝐹)‘𝑋))
236 fcompt 6879 . . . . . 6 (((𝐴𝑃):((1st𝐹)‘𝑃)⟶((1st𝐺)‘𝑃) ∧ ((𝑋(2nd𝐹)𝑃)‘𝐾):((1st𝐹)‘𝑋)⟶((1st𝐹)‘𝑃)) → ((𝐴𝑃) ∘ ((𝑋(2nd𝐹)𝑃)‘𝐾)) = (𝑦 ∈ ((1st𝐹)‘𝑋) ↦ ((𝐴𝑃)‘(((𝑋(2nd𝐹)𝑃)‘𝐾)‘𝑦))))
23777, 145, 236syl2anc 587 . . . . 5 (𝜑 → ((𝐴𝑃) ∘ ((𝑋(2nd𝐹)𝑃)‘𝐾)) = (𝑦 ∈ ((1st𝐹)‘𝑋) ↦ ((𝐴𝑃)‘(((𝑋(2nd𝐹)𝑃)‘𝐾)‘𝑦))))
238 2fveq3 6657 . . . . 5 (𝑦 = ((𝑎𝑋)‘( 1𝑋)) → ((𝐴𝑃)‘(((𝑋(2nd𝐹)𝑃)‘𝐾)‘𝑦)) = ((𝐴𝑃)‘(((𝑋(2nd𝐹)𝑃)‘𝐾)‘((𝑎𝑋)‘( 1𝑋)))))
239235, 229, 237, 238fmptcof 6876 . . . 4 (𝜑 → (((𝐴𝑃) ∘ ((𝑋(2nd𝐹)𝑃)‘𝐾)) ∘ (𝐹𝑀𝑋)) = (𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴𝑃)‘(((𝑋(2nd𝐹)𝑃)‘𝐾)‘((𝑎𝑋)‘( 1𝑋))))))
240226, 239eqtrd 2833 . . 3 (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)𝐾) ∘ (𝐹𝑀𝑋)) = (𝑎 ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴𝑃)‘(((𝑋(2nd𝐹)𝑃)‘𝐾)‘((𝑎𝑋)‘( 1𝑋))))))
241163, 221, 2403eqtr4d 2843 . 2 (𝜑 → ((𝐺𝑀𝑃) ∘ (𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾)) = ((𝐴(⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)𝐾) ∘ (𝐹𝑀𝑋)))
242 eqid 2798 . . 3 (comp‘𝑇) = (comp‘𝑇)
243174simprd 499 . . . . . . 7 (𝜑𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇))
244 1st2ndbr 7733 . . . . . . 7 ((Rel ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st𝐸)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝐸))
245168, 243, 244sylancr 590 . . . . . 6 (𝜑 → (1st𝐸)((𝑄 ×c 𝑂) Func 𝑇)(2nd𝐸))
246165, 192, 245funcf1 17145 . . . . 5 (𝜑 → (1st𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
247246, 62, 27fovrnd 7308 . . . 4 (𝜑 → (𝐺(1st𝐸)𝑃) ∈ (Base‘𝑇))
248247, 195eleqtrrd 2893 . . 3 (𝜑 → (𝐺(1st𝐸)𝑃) ∈ 𝑉)
249217simprd 499 . . 3 (𝜑 → (𝐺𝑀𝑃):(𝐺(1st𝑍)𝑃)⟶(𝐺(1st𝐸)𝑃))
250169, 19, 242, 196, 198, 248, 200, 249setcco 17352 . 2 (𝜑 → ((𝐺𝑀𝑃)(⟨(𝐹(1st𝑍)𝑋), (𝐺(1st𝑍)𝑃)⟩(comp‘𝑇)(𝐺(1st𝐸)𝑃))(𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾)) = ((𝐺𝑀𝑃) ∘ (𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾)))
251246, 54, 28fovrnd 7308 . . . 4 (𝜑 → (𝐹(1st𝐸)𝑋) ∈ (Base‘𝑇))
252251, 195eleqtrrd 2893 . . 3 (𝜑 → (𝐹(1st𝐸)𝑋) ∈ 𝑉)
253165, 166, 167, 245, 178, 179funcf2 17147 . . . . . 6 (𝜑 → (⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩):(⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×c 𝑂))⟨𝐺, 𝑃⟩)⟶(((1st𝐸)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1st𝐸)‘⟨𝐺, 𝑃⟩)))
254 df-ov 7145 . . . . . . . . . 10 (𝐹(1st𝐸)𝑋) = ((1st𝐸)‘⟨𝐹, 𝑋⟩)
255 df-ov 7145 . . . . . . . . . 10 (𝐺(1st𝐸)𝑃) = ((1st𝐸)‘⟨𝐺, 𝑃⟩)
256254, 255oveq12i 7154 . . . . . . . . 9 ((𝐹(1st𝐸)𝑋)(Hom ‘𝑇)(𝐺(1st𝐸)𝑃)) = (((1st𝐸)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1st𝐸)‘⟨𝐺, 𝑃⟩))
257256eqcomi 2807 . . . . . . . 8 (((1st𝐸)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1st𝐸)‘⟨𝐺, 𝑃⟩)) = ((𝐹(1st𝐸)𝑋)(Hom ‘𝑇)(𝐺(1st𝐸)𝑃))
258257a1i 11 . . . . . . 7 (𝜑 → (((1st𝐸)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1st𝐸)‘⟨𝐺, 𝑃⟩)) = ((𝐹(1st𝐸)𝑋)(Hom ‘𝑇)(𝐺(1st𝐸)𝑃)))
259183, 258feq23d 6487 . . . . . 6 (𝜑 → ((⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩):(⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×c 𝑂))⟨𝐺, 𝑃⟩)⟶(((1st𝐸)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1st𝐸)‘⟨𝐺, 𝑃⟩)) ↔ (⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩):((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))⟶((𝐹(1st𝐸)𝑋)(Hom ‘𝑇)(𝐺(1st𝐸)𝑃))))
260253, 259mpbid 235 . . . . 5 (𝜑 → (⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩):((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))⟶((𝐹(1st𝐸)𝑋)(Hom ‘𝑇)(𝐺(1st𝐸)𝑃)))
261260, 34, 30fovrnd 7308 . . . 4 (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)𝐾) ∈ ((𝐹(1st𝐸)𝑋)(Hom ‘𝑇)(𝐺(1st𝐸)𝑃)))
262169, 19, 167, 252, 248elsetchom 17350 . . . 4 (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)𝐾) ∈ ((𝐹(1st𝐸)𝑋)(Hom ‘𝑇)(𝐺(1st𝐸)𝑃)) ↔ (𝐴(⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)𝐾):(𝐹(1st𝐸)𝑋)⟶(𝐺(1st𝐸)𝑃)))
263261, 262mpbid 235 . . 3 (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)𝐾):(𝐹(1st𝐸)𝑋)⟶(𝐺(1st𝐸)𝑃))
264169, 19, 242, 196, 252, 248, 228, 263setcco 17352 . 2 (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)𝐾)(⟨(𝐹(1st𝑍)𝑋), (𝐹(1st𝐸)𝑋)⟩(comp‘𝑇)(𝐺(1st𝐸)𝑃))(𝐹𝑀𝑋)) = ((𝐴(⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)𝐾) ∘ (𝐹𝑀𝑋)))
265241, 250, 2643eqtr4d 2843 1 (𝜑 → ((𝐺𝑀𝑃)(⟨(𝐹(1st𝑍)𝑋), (𝐺(1st𝑍)𝑃)⟩(comp‘𝑇)(𝐺(1st𝐸)𝑃))(𝐴(⟨𝐹, 𝑋⟩(2nd𝑍)⟨𝐺, 𝑃⟩)𝐾)) = ((𝐴(⟨𝐹, 𝑋⟩(2nd𝐸)⟨𝐺, 𝑃⟩)𝐾)(⟨(𝐹(1st𝑍)𝑋), (𝐹(1st𝐸)𝑋)⟩(comp‘𝑇)(𝐺(1st𝐸)𝑃))(𝐹𝑀𝑋)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106  Vcvv 3441   ∪ cun 3880   ⊆ wss 3882  ⟨cop 4533   class class class wbr 5033   ↦ cmpt 5113   × cxp 5520  ran crn 5523   ∘ ccom 5526  Rel wrel 5527  ⟶wf 6325  ‘cfv 6329  (class class class)co 7142   ∈ cmpo 7144  1st c1st 7679  2nd c2nd 7680  tpos ctpos 7889  Basecbs 16492  Hom chom 16585  compcco 16586  Catccat 16944  Idccid 16945  Homf chomf 16946  oppCatcoppc 16990   Func cfunc 17133   ∘func ccofu 17135   Nat cnat 17220   FuncCat cfuc 17221  SetCatcsetc 17344   ×c cxpc 17427   1stF c1stf 17428   2ndF c2ndf 17429   ⟨,⟩F cprf 17430   evalF cevlf 17468  HomFchof 17507  Yoncyon 17508 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 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7451  ax-cnex 10597  ax-resscn 10598  ax-1cn 10599  ax-icn 10600  ax-addcl 10601  ax-addrcl 10602  ax-mulcl 10603  ax-mulrcl 10604  ax-mulcom 10605  ax-addass 10606  ax-mulass 10607  ax-distr 10608  ax-i2m1 10609  ax-1ne0 10610  ax-1rid 10611  ax-rnegex 10612  ax-rrecex 10613  ax-cnre 10614  ax-pre-lttri 10615  ax-pre-lttrn 10616  ax-pre-ltadd 10617  ax-pre-mulgt0 10618 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 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3722  df-csb 3830  df-dif 3885  df-un 3887  df-in 3889  df-ss 3899  df-pss 3901  df-nul 4246  df-if 4428  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  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 5441  df-so 5442  df-fr 5481  df-we 5483  df-xp 5528  df-rel 5529  df-cnv 5530  df-co 5531  df-dm 5532  df-rn 5533  df-res 5534  df-ima 5535  df-pred 6121  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-iota 6288  df-fun 6331  df-fn 6332  df-f 6333  df-f1 6334  df-fo 6335  df-f1o 6336  df-fv 6337  df-riota 7100  df-ov 7145  df-oprab 7146  df-mpo 7147  df-om 7571  df-1st 7681  df-2nd 7682  df-tpos 7890  df-wrecs 7945  df-recs 8006  df-rdg 8044  df-1o 8100  df-oadd 8104  df-er 8287  df-map 8406  df-pm 8407  df-ixp 8460  df-en 8508  df-dom 8509  df-sdom 8510  df-fin 8511  df-pnf 10681  df-mnf 10682  df-xr 10683  df-ltxr 10684  df-le 10685  df-sub 10876  df-neg 10877  df-nn 11641  df-2 11703  df-3 11704  df-4 11705  df-5 11706  df-6 11707  df-7 11708  df-8 11709  df-9 11710  df-n0 11901  df-z 11987  df-dec 12104  df-uz 12249  df-fz 12903  df-struct 16494  df-ndx 16495  df-slot 16496  df-base 16498  df-sets 16499  df-ress 16500  df-hom 16598  df-cco 16599  df-cat 16948  df-cid 16949  df-homf 16950  df-comf 16951  df-oppc 16991  df-ssc 17089  df-resc 17090  df-subc 17091  df-func 17137  df-cofu 17139  df-nat 17222  df-fuc 17223  df-setc 17345  df-xpc 17431  df-1stf 17432  df-2ndf 17433  df-prf 17434  df-evlf 17472  df-curf 17473  df-hof 17509  df-yon 17510 This theorem is referenced by:  yonedalem3  17539
 Copyright terms: Public domain W3C validator