yonedalem3b - Metamath Proof Explorer

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

Theorem yonedalem3b 18228

Description: Lemma for yoneda 18232. (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	⊢ 𝐻 = (Hom_F‘𝑄)
yoneda.r	⊢ 𝑅 = ((𝑄 ×_c 𝑂) FuncCat 𝑇)
yoneda.e	⊢ 𝐸 = (𝑂 eval_F 𝑆)
yoneda.z	⊢ 𝑍 = (𝐻 ∘_func ((⟨(1^st ‘𝑌), tpos (2^nd ‘𝑌)⟩ ∘_func (𝑄 2^nd_F 𝑂)) ⟨,⟩_F (𝑄 1^st_F 𝑂)))
yoneda.c	⊢ (𝜑 → 𝐶 ∈ Cat)
yoneda.w	⊢ (𝜑 → 𝑉 ∈ 𝑊)
yoneda.u	⊢ (𝜑 → ran (Hom_f ‘𝐶) ⊆ 𝑈)
yoneda.v	⊢ (𝜑 → (ran (Hom_f ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
yonedalem21.f	⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑆))
yonedalem21.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
yonedalem22.g	⊢ (𝜑 → 𝐺 ∈ (𝑂 Func 𝑆))
yonedalem22.p	⊢ (𝜑 → 𝑃 ∈ 𝐵)
yonedalem22.a	⊢ (𝜑 → 𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺))
yonedalem22.k	⊢ (𝜑 → 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋))
yonedalem3.m	⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1^st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥))))

**Assertion**
Ref	Expression
yonedalem3b	⊢ (𝜑 → ((𝐺𝑀𝑃)(⟨(𝐹(1^st ‘𝑍)𝑋), (𝐺(1^st ‘𝑍)𝑃)⟩(comp‘𝑇)(𝐺(1^st ‘𝐸)𝑃))(𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾)) = ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾)(⟨(𝐹(1^st ‘𝑍)𝑋), (𝐹(1^st ‘𝐸)𝑋)⟩(comp‘𝑇)(𝐺(1^st ‘𝐸)𝑃))(𝐹𝑀𝑋)))

Distinct variable groups: 𝑓,𝑎,𝑥, 1 𝐴,𝑎 𝐶,𝑎,𝑓,𝑥 𝐸,𝑎,𝑓 𝐹,𝑎,𝑓,𝑥 𝐾,𝑎 𝐵,𝑎,𝑓,𝑥 𝐺,𝑎,𝑓,𝑥 𝑂,𝑎,𝑓,𝑥 𝑆,𝑎,𝑓,𝑥 𝑄,𝑎,𝑓,𝑥 𝑇,𝑓 𝑃,𝑎,𝑓,𝑥 𝜑,𝑎,𝑓,𝑥 𝑌,𝑎,𝑓,𝑥 𝑍,𝑎,𝑓,𝑥 𝑋,𝑎,𝑓,𝑥 Allowed substitution hints: 𝐴(𝑥,𝑓) 𝑅(𝑥,𝑓,𝑎) 𝑇(𝑥,𝑎) 𝑈(𝑥,𝑓,𝑎) 𝐸(𝑥) 𝐻(𝑥,𝑓,𝑎) 𝐾(𝑥,𝑓) 𝑀(𝑥,𝑓,𝑎) 𝑉(𝑥,𝑓,𝑎) 𝑊(𝑥,𝑓,𝑎)

Proof of Theorem yonedalem3b Dummy variables 𝑏 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 7413	. . . . . . . 8 ⊢ (𝑏 = 𝑎 → (𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏) = (𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎))
2	1	oveq1d 7420	. . . . . . 7 ⊢ (𝑏 = 𝑎 → ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)) = ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)))
3	2	fveq1d 6890	. . . . . 6 ⊢ (𝑏 = 𝑎 → (((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃) = (((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃))
4	3	fveq1d 6890	. . . . 5 ⊢ (𝑏 = 𝑎 → ((((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃)‘( 1 ‘𝑃)) = ((((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃)‘( 1 ‘𝑃)))
5	4	cbvmptv 5260	. . . 4 ⊢ (𝑏 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃)‘( 1 ‘𝑃))) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃)‘( 1 ‘𝑃)))
6		yoneda.q	. . . . . . . . 9 ⊢ 𝑄 = (𝑂 FuncCat 𝑆)
7		eqid 2732	. . . . . . . . 9 ⊢ (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆)
8		yoneda.o	. . . . . . . . . 10 ⊢ 𝑂 = (oppCat‘𝐶)
9		yoneda.b	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝐶)
10	8, 9	oppcbas 17659	. . . . . . . . 9 ⊢ 𝐵 = (Base‘𝑂)
11		eqid 2732	. . . . . . . . 9 ⊢ (comp‘𝑆) = (comp‘𝑆)
12		eqid 2732	. . . . . . . . 9 ⊢ (comp‘𝑄) = (comp‘𝑄)
13		eqid 2732	. . . . . . . . . . . 12 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
14	6, 7	fuchom 17909	. . . . . . . . . . . 12 ⊢ (𝑂 Nat 𝑆) = (Hom ‘𝑄)
15		relfunc 17808	. . . . . . . . . . . . 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 (Hom_f ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
21	20	unssbd 4187	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 ⊆ 𝑉)
22	19, 21	ssexd 5323	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ∈ V)
23		yoneda.u	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran (Hom_f ‘𝐶) ⊆ 𝑈)
24	16, 17, 8, 18, 6, 22, 23	yoncl 18211	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ∈ (𝐶 Func 𝑄))
25		1st2ndbr 8024	. . . . . . . . . . . . 13 ⊢ ((Rel (𝐶 Func 𝑄) ∧ 𝑌 ∈ (𝐶 Func 𝑄)) → (1^st ‘𝑌)(𝐶 Func 𝑄)(2^nd ‘𝑌))
26	15, 24, 25	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝜑 → (1^st ‘𝑌)(𝐶 Func 𝑄)(2^nd ‘𝑌))
27		yonedalem22.p	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ 𝐵)
28		yonedalem21.x	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
29	9, 13, 14, 26, 27, 28	funcf2 17814	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃(2^nd ‘𝑌)𝑋):(𝑃(Hom ‘𝐶)𝑋)⟶(((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑋)))
30		yonedalem22.k	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋))
31	29, 30	ffvelcdmd 7084	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑃(2^nd ‘𝑌)𝑋)‘𝐾) ∈ (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑋)))
32	31	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑃(2^nd ‘𝑌)𝑋)‘𝐾) ∈ (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑋)))
33		simpr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹))
34		yonedalem22.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺))
35	34	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺))
36	6, 7, 12, 33, 35	fuccocl 17913	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎) ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐺))
37	27	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑃 ∈ 𝐵)
38	6, 7, 10, 11, 12, 32, 36, 37	fuccoval 17912	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃) = (((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)‘𝑃)(⟨((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃), ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))(((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)))
39	6, 7, 10, 11, 12, 33, 35, 37	fuccoval 17912	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)‘𝑃) = ((𝐴‘𝑃)(⟨((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃), ((1^st ‘𝐹)‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))(𝑎‘𝑃)))
40	22	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑈 ∈ V)
41		eqid 2732	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝑆) = (Base‘𝑆)
42		relfunc 17808	. . . . . . . . . . . . . . . 16 ⊢ Rel (𝑂 Func 𝑆)
43	6	fucbas 17908	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑂 Func 𝑆) = (Base‘𝑄)
44	9, 43, 26	funcf1 17812	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1^st ‘𝑌):𝐵⟶(𝑂 Func 𝑆))
45	44, 28	ffvelcdmd 7084	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1^st ‘𝑌)‘𝑋) ∈ (𝑂 Func 𝑆))
46		1st2ndbr 8024	. . . . . . . . . . . . . . . 16 ⊢ ((Rel (𝑂 Func 𝑆) ∧ ((1^st ‘𝑌)‘𝑋) ∈ (𝑂 Func 𝑆)) → (1^st ‘((1^st ‘𝑌)‘𝑋))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑋)))
47	42, 45, 46	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1^st ‘((1^st ‘𝑌)‘𝑋))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑋)))
48	10, 41, 47	funcf1 17812	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1^st ‘((1^st ‘𝑌)‘𝑋)):𝐵⟶(Base‘𝑆))
49	18, 22	setcbas 18024	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 = (Base‘𝑆))
50	49	feq3d 6701	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑋)):𝐵⟶𝑈 ↔ (1^st ‘((1^st ‘𝑌)‘𝑋)):𝐵⟶(Base‘𝑆)))
51	48, 50	mpbird 256	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1^st ‘((1^st ‘𝑌)‘𝑋)):𝐵⟶𝑈)
52	51, 27	ffvelcdmd 7084	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃) ∈ 𝑈)
53	52	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃) ∈ 𝑈)
54		yonedalem21.f	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑆))
55		1st2ndbr 8024	. . . . . . . . . . . . . . . 16 ⊢ ((Rel (𝑂 Func 𝑆) ∧ 𝐹 ∈ (𝑂 Func 𝑆)) → (1^st ‘𝐹)(𝑂 Func 𝑆)(2^nd ‘𝐹))
56	42, 54, 55	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1^st ‘𝐹)(𝑂 Func 𝑆)(2^nd ‘𝐹))
57	10, 41, 56	funcf1 17812	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1^st ‘𝐹):𝐵⟶(Base‘𝑆))
58	49	feq3d 6701	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘𝐹):𝐵⟶𝑈 ↔ (1^st ‘𝐹):𝐵⟶(Base‘𝑆)))
59	57, 58	mpbird 256	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1^st ‘𝐹):𝐵⟶𝑈)
60	59, 27	ffvelcdmd 7084	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1^st ‘𝐹)‘𝑃) ∈ 𝑈)
61	60	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘𝐹)‘𝑃) ∈ 𝑈)
62		yonedalem22.g	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐺 ∈ (𝑂 Func 𝑆))
63		1st2ndbr 8024	. . . . . . . . . . . . . . . 16 ⊢ ((Rel (𝑂 Func 𝑆) ∧ 𝐺 ∈ (𝑂 Func 𝑆)) → (1^st ‘𝐺)(𝑂 Func 𝑆)(2^nd ‘𝐺))
64	42, 62, 63	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1^st ‘𝐺)(𝑂 Func 𝑆)(2^nd ‘𝐺))
65	10, 41, 64	funcf1 17812	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1^st ‘𝐺):𝐵⟶(Base‘𝑆))
66	65, 27	ffvelcdmd 7084	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1^st ‘𝐺)‘𝑃) ∈ (Base‘𝑆))
67	66, 49	eleqtrrd 2836	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1^st ‘𝐺)‘𝑃) ∈ 𝑈)
68	67	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘𝐺)‘𝑃) ∈ 𝑈)
69	7, 33	nat1st2nd 17898	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑎 ∈ (⟨(1^st ‘((1^st ‘𝑌)‘𝑋)), (2^nd ‘((1^st ‘𝑌)‘𝑋))⟩(𝑂 Nat 𝑆)⟨(1^st ‘𝐹), (2^nd ‘𝐹)⟩))
70		eqid 2732	. . . . . . . . . . . . 13 ⊢ (Hom ‘𝑆) = (Hom ‘𝑆)
71	7, 69, 10, 70, 37	natcl 17900	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝑎‘𝑃) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑃)))
72	18, 40, 70, 53, 61	elsetchom 18027	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑃) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑃)) ↔ (𝑎‘𝑃):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟶((1^st ‘𝐹)‘𝑃)))
73	71, 72	mpbid 231	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝑎‘𝑃):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟶((1^st ‘𝐹)‘𝑃))
74	7, 34	nat1st2nd 17898	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ (⟨(1^st ‘𝐹), (2^nd ‘𝐹)⟩(𝑂 Nat 𝑆)⟨(1^st ‘𝐺), (2^nd ‘𝐺)⟩))
75	7, 74, 10, 70, 27	natcl 17900	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴‘𝑃) ∈ (((1^st ‘𝐹)‘𝑃)(Hom ‘𝑆)((1^st ‘𝐺)‘𝑃)))
76	18, 22, 70, 60, 67	elsetchom 18027	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴‘𝑃) ∈ (((1^st ‘𝐹)‘𝑃)(Hom ‘𝑆)((1^st ‘𝐺)‘𝑃)) ↔ (𝐴‘𝑃):((1^st ‘𝐹)‘𝑃)⟶((1^st ‘𝐺)‘𝑃)))
77	75, 76	mpbid 231	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴‘𝑃):((1^st ‘𝐹)‘𝑃)⟶((1^st ‘𝐺)‘𝑃))
78	77	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝐴‘𝑃):((1^st ‘𝐹)‘𝑃)⟶((1^st ‘𝐺)‘𝑃))
79	18, 40, 11, 53, 61, 68, 73, 78	setcco 18029	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴‘𝑃)(⟨((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃), ((1^st ‘𝐹)‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))(𝑎‘𝑃)) = ((𝐴‘𝑃) ∘ (𝑎‘𝑃)))
80	39, 79	eqtrd 2772	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)‘𝑃) = ((𝐴‘𝑃) ∘ (𝑎‘𝑃)))
81	80	oveq1d 7420	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)‘𝑃)(⟨((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃), ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))(((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)) = (((𝐴‘𝑃) ∘ (𝑎‘𝑃))(⟨((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃), ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))(((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)))
82	44, 27	ffvelcdmd 7084	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘𝑌)‘𝑃) ∈ (𝑂 Func 𝑆))
83		1st2ndbr 8024	. . . . . . . . . . . . . 14 ⊢ ((Rel (𝑂 Func 𝑆) ∧ ((1^st ‘𝑌)‘𝑃) ∈ (𝑂 Func 𝑆)) → (1^st ‘((1^st ‘𝑌)‘𝑃))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑃)))
84	42, 82, 83	sylancr 587	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1^st ‘((1^st ‘𝑌)‘𝑃))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑃)))
85	10, 41, 84	funcf1 17812	. . . . . . . . . . . 12 ⊢ (𝜑 → (1^st ‘((1^st ‘𝑌)‘𝑃)):𝐵⟶(Base‘𝑆))
86	85, 27	ffvelcdmd 7084	. . . . . . . . . . 11 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃) ∈ (Base‘𝑆))
87	86, 49	eleqtrrd 2836	. . . . . . . . . 10 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃) ∈ 𝑈)
88	87	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃) ∈ 𝑈)
89	7, 31	nat1st2nd 17898	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑃(2^nd ‘𝑌)𝑋)‘𝐾) ∈ (⟨(1^st ‘((1^st ‘𝑌)‘𝑃)), (2^nd ‘((1^st ‘𝑌)‘𝑃))⟩(𝑂 Nat 𝑆)⟨(1^st ‘((1^st ‘𝑌)‘𝑋)), (2^nd ‘((1^st ‘𝑌)‘𝑋))⟩))
90	7, 89, 10, 70, 27	natcl 17900	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃)(Hom ‘𝑆)((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)))
91	18, 22, 70, 87, 52	elsetchom 18027	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃)(Hom ‘𝑆)((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)) ↔ (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃):((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃)⟶((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)))
92	90, 91	mpbid 231	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃):((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃)⟶((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃))
93	92	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃):((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃)⟶((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃))
94		fco 6738	. . . . . . . . . 10 ⊢ (((𝐴‘𝑃):((1^st ‘𝐹)‘𝑃)⟶((1^st ‘𝐺)‘𝑃) ∧ (𝑎‘𝑃):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟶((1^st ‘𝐹)‘𝑃)) → ((𝐴‘𝑃) ∘ (𝑎‘𝑃)):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟶((1^st ‘𝐺)‘𝑃))
95	78, 73, 94	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴‘𝑃) ∘ (𝑎‘𝑃)):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟶((1^st ‘𝐺)‘𝑃))
96	18, 40, 11, 88, 53, 68, 93, 95	setcco 18029	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴‘𝑃) ∘ (𝑎‘𝑃))(⟨((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃), ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))(((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)) = (((𝐴‘𝑃) ∘ (𝑎‘𝑃)) ∘ (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)))
97	38, 81, 96	3eqtrd 2776	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃) = (((𝐴‘𝑃) ∘ (𝑎‘𝑃)) ∘ (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)))
98	97	fveq1d 6890	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃)‘( 1 ‘𝑃)) = ((((𝐴‘𝑃) ∘ (𝑎‘𝑃)) ∘ (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃))‘( 1 ‘𝑃)))
99		yoneda.1	. . . . . . . . . 10 ⊢ 1 = (Id‘𝐶)
100	9, 13, 99, 17, 27	catidcl 17622	. . . . . . . . 9 ⊢ (𝜑 → ( 1 ‘𝑃) ∈ (𝑃(Hom ‘𝐶)𝑃))
101	16, 9, 17, 27, 13, 27	yon11 18213	. . . . . . . . 9 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃) = (𝑃(Hom ‘𝐶)𝑃))
102	100, 101	eleqtrrd 2836	. . . . . . . 8 ⊢ (𝜑 → ( 1 ‘𝑃) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃))
103	102	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1 ‘𝑃) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃))
104		fvco3 6987	. . . . . . 7 ⊢ (((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃):((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃)⟶((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃) ∧ ( 1 ‘𝑃) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃)) → ((((𝐴‘𝑃) ∘ (𝑎‘𝑃)) ∘ (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃))‘( 1 ‘𝑃)) = (((𝐴‘𝑃) ∘ (𝑎‘𝑃))‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))))
105	93, 103, 104	syl2anc 584	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝐴‘𝑃) ∘ (𝑎‘𝑃)) ∘ (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃))‘( 1 ‘𝑃)) = (((𝐴‘𝑃) ∘ (𝑎‘𝑃))‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))))
106	93, 103	ffvelcdmd 7084	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃))
107		fvco3 6987	. . . . . . . 8 ⊢ (((𝑎‘𝑃):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟶((1^st ‘𝐹)‘𝑃) ∧ ((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)) → (((𝐴‘𝑃) ∘ (𝑎‘𝑃))‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))) = ((𝐴‘𝑃)‘((𝑎‘𝑃)‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)))))
108	73, 106, 107	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴‘𝑃) ∘ (𝑎‘𝑃))‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))) = ((𝐴‘𝑃)‘((𝑎‘𝑃)‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)))))
109	17	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐶 ∈ Cat)
110	28	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑋 ∈ 𝐵)
111		eqid 2732	. . . . . . . . . . . 12 ⊢ (comp‘𝐶) = (comp‘𝐶)
112	30	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋))
113	100	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1 ‘𝑃) ∈ (𝑃(Hom ‘𝐶)𝑃))
114	16, 9, 109, 37, 13, 110, 111, 37, 112, 113	yon2 18215	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)) = (𝐾(⟨𝑃, 𝑃⟩(comp‘𝐶)𝑋)( 1 ‘𝑃)))
115	9, 13, 99, 109, 37, 111, 110, 112	catrid 17624	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝐾(⟨𝑃, 𝑃⟩(comp‘𝐶)𝑋)( 1 ‘𝑃)) = 𝐾)
116	114, 115	eqtrd 2772	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)) = 𝐾)
117	116	fveq2d 6892	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑃)‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))) = ((𝑎‘𝑃)‘𝐾))
118		eqid 2732	. . . . . . . . . . . . . . 15 ⊢ (Hom ‘𝑂) = (Hom ‘𝑂)
119	10, 118, 70, 47, 28, 27	funcf2 17814	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃):(𝑋(Hom ‘𝑂)𝑃)⟶(((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)))
120	13, 8	oppchom 17656	. . . . . . . . . . . . . . 15 ⊢ (𝑋(Hom ‘𝑂)𝑃) = (𝑃(Hom ‘𝐶)𝑋)
121	30, 120	eleqtrrdi 2844	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ (𝑋(Hom ‘𝑂)𝑃))
122	119, 121	ffvelcdmd 7084	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)))
123	51, 28	ffvelcdmd 7084	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋) ∈ 𝑈)
124	18, 22, 70, 123, 52	elsetchom 18027	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)) ↔ ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)⟶((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)))
125	122, 124	mpbid 231	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)⟶((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃))
126	125	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)⟶((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃))
127	9, 13, 99, 17, 28	catidcl 17622	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( 1 ‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋))
128	16, 9, 17, 28, 13, 28	yon11 18213	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋) = (𝑋(Hom ‘𝐶)𝑋))
129	127, 128	eleqtrrd 2836	. . . . . . . . . . . 12 ⊢ (𝜑 → ( 1 ‘𝑋) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋))
130	129	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1 ‘𝑋) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋))
131		fvco3 6987	. . . . . . . . . . 11 ⊢ ((((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)⟶((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃) ∧ ( 1 ‘𝑋) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)) → (((𝑎‘𝑃) ∘ ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾))‘( 1 ‘𝑋)) = ((𝑎‘𝑃)‘(((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)‘( 1 ‘𝑋))))
132	126, 130, 131	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑎‘𝑃) ∘ ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾))‘( 1 ‘𝑋)) = ((𝑎‘𝑃)‘(((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)‘( 1 ‘𝑋))))
133	121	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐾 ∈ (𝑋(Hom ‘𝑂)𝑃))
134	7, 69, 10, 118, 11, 110, 37, 133	nati 17902	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑃)(⟨((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋), ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐹)‘𝑃))((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)) = (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)(⟨((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋), ((1^st ‘𝐹)‘𝑋)⟩(comp‘𝑆)((1^st ‘𝐹)‘𝑃))(𝑎‘𝑋)))
135	123	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋) ∈ 𝑈)
136	18, 40, 11, 135, 53, 61, 126, 73	setcco 18029	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑃)(⟨((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋), ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐹)‘𝑃))((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)) = ((𝑎‘𝑃) ∘ ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)))
137	59, 28	ffvelcdmd 7084	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘𝐹)‘𝑋) ∈ 𝑈)
138	137	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘𝐹)‘𝑋) ∈ 𝑈)
139	7, 69, 10, 70, 110	natcl 17900	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝑎‘𝑋) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑋)))
140	18, 40, 70, 135, 138	elsetchom 18027	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑋) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑋)) ↔ (𝑎‘𝑋):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)⟶((1^st ‘𝐹)‘𝑋)))
141	139, 140	mpbid 231	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝑎‘𝑋):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)⟶((1^st ‘𝐹)‘𝑋))
142	10, 118, 70, 56, 28, 27	funcf2 17814	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋(2^nd ‘𝐹)𝑃):(𝑋(Hom ‘𝑂)𝑃)⟶(((1^st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑃)))
143	142, 121	ffvelcdmd 7084	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∈ (((1^st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑃)))
144	18, 22, 70, 137, 60	elsetchom 18027	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∈ (((1^st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑃)) ↔ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾):((1^st ‘𝐹)‘𝑋)⟶((1^st ‘𝐹)‘𝑃)))
145	143, 144	mpbid 231	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾):((1^st ‘𝐹)‘𝑋)⟶((1^st ‘𝐹)‘𝑃))
146	145	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾):((1^st ‘𝐹)‘𝑋)⟶((1^st ‘𝐹)‘𝑃))
147	18, 40, 11, 135, 138, 61, 141, 146	setcco 18029	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)(⟨((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋), ((1^st ‘𝐹)‘𝑋)⟩(comp‘𝑆)((1^st ‘𝐹)‘𝑃))(𝑎‘𝑋)) = (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋)))
148	134, 136, 147	3eqtr3d 2780	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑃) ∘ ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)) = (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋)))
149	148	fveq1d 6890	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑎‘𝑃) ∘ ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾))‘( 1 ‘𝑋)) = ((((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋))‘( 1 ‘𝑋)))
150	127	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1 ‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋))
151	16, 9, 109, 110, 13, 110, 111, 37, 112, 150	yon12 18214	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)‘( 1 ‘𝑋)) = (( 1 ‘𝑋)(⟨𝑃, 𝑋⟩(comp‘𝐶)𝑋)𝐾))
152	9, 13, 99, 109, 37, 111, 110, 112	catlid 17623	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (( 1 ‘𝑋)(⟨𝑃, 𝑋⟩(comp‘𝐶)𝑋)𝐾) = 𝐾)
153	151, 152	eqtrd 2772	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)‘( 1 ‘𝑋)) = 𝐾)
154	153	fveq2d 6892	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑃)‘(((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)‘( 1 ‘𝑋))) = ((𝑎‘𝑃)‘𝐾))
155	132, 149, 154	3eqtr3d 2780	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋))‘( 1 ‘𝑋)) = ((𝑎‘𝑃)‘𝐾))
156		fvco3 6987	. . . . . . . . . 10 ⊢ (((𝑎‘𝑋):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)⟶((1^st ‘𝐹)‘𝑋) ∧ ( 1 ‘𝑋) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)) → ((((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋))‘( 1 ‘𝑋)) = (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))
157	141, 130, 156	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋))‘( 1 ‘𝑋)) = (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))
158	117, 155, 157	3eqtr2d 2778	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑃)‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))) = (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))
159	158	fveq2d 6892	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴‘𝑃)‘((𝑎‘𝑃)‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)))) = ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋)))))
160	108, 159	eqtrd 2772	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴‘𝑃) ∘ (𝑎‘𝑃))‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))) = ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋)))))
161	98, 105, 160	3eqtrd 2776	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃)‘( 1 ‘𝑃)) = ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋)))))
162	161	mpteq2dva 5247	. . . 4 ⊢ (𝜑 → (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃)‘( 1 ‘𝑃))) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))))
163	5, 162	eqtrid 2784	. . 3 ⊢ (𝜑 → (𝑏 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃)‘( 1 ‘𝑃))) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))))
164		eqid 2732	. . . . . . . . . . 11 ⊢ (𝑄 ×_c 𝑂) = (𝑄 ×_c 𝑂)
165	164, 43, 10	xpcbas 18126	. . . . . . . . . 10 ⊢ ((𝑂 Func 𝑆) × 𝐵) = (Base‘(𝑄 ×_c 𝑂))
166		eqid 2732	. . . . . . . . . 10 ⊢ (Hom ‘(𝑄 ×_c 𝑂)) = (Hom ‘(𝑄 ×_c 𝑂))
167		eqid 2732	. . . . . . . . . 10 ⊢ (Hom ‘𝑇) = (Hom ‘𝑇)
168		relfunc 17808	. . . . . . . . . . 11 ⊢ Rel ((𝑄 ×_c 𝑂) Func 𝑇)
169		yoneda.t	. . . . . . . . . . . . 13 ⊢ 𝑇 = (SetCat‘𝑉)
170		yoneda.h	. . . . . . . . . . . . 13 ⊢ 𝐻 = (Hom_F‘𝑄)
171		yoneda.r	. . . . . . . . . . . . 13 ⊢ 𝑅 = ((𝑄 ×_c 𝑂) FuncCat 𝑇)
172		yoneda.e	. . . . . . . . . . . . 13 ⊢ 𝐸 = (𝑂 eval_F 𝑆)
173		yoneda.z	. . . . . . . . . . . . 13 ⊢ 𝑍 = (𝐻 ∘_func ((⟨(1^st ‘𝑌), tpos (2^nd ‘𝑌)⟩ ∘_func (𝑄 2^nd_F 𝑂)) ⟨,⟩_F (𝑄 1^st_F 𝑂)))
174	16, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20	yonedalem1 18221	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑍 ∈ ((𝑄 ×_c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×_c 𝑂) Func 𝑇)))
175	174	simpld 495	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑍 ∈ ((𝑄 ×_c 𝑂) Func 𝑇))
176		1st2ndbr 8024	. . . . . . . . . . 11 ⊢ ((Rel ((𝑄 ×_c 𝑂) Func 𝑇) ∧ 𝑍 ∈ ((𝑄 ×_c 𝑂) Func 𝑇)) → (1^st ‘𝑍)((𝑄 ×_c 𝑂) Func 𝑇)(2^nd ‘𝑍))
177	168, 175, 176	sylancr 587	. . . . . . . . . 10 ⊢ (𝜑 → (1^st ‘𝑍)((𝑄 ×_c 𝑂) Func 𝑇)(2^nd ‘𝑍))
178	54, 28	opelxpd 5713	. . . . . . . . . 10 ⊢ (𝜑 → ⟨𝐹, 𝑋⟩ ∈ ((𝑂 Func 𝑆) × 𝐵))
179	62, 27	opelxpd 5713	. . . . . . . . . 10 ⊢ (𝜑 → ⟨𝐺, 𝑃⟩ ∈ ((𝑂 Func 𝑆) × 𝐵))
180	165, 166, 167, 177, 178, 179	funcf2 17814	. . . . . . . . 9 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩):(⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×_c 𝑂))⟨𝐺, 𝑃⟩)⟶(((1^st ‘𝑍)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝑍)‘⟨𝐺, 𝑃⟩)))
181	164, 43, 10, 14, 118, 54, 28, 62, 27, 166	xpchom2 18134	. . . . . . . . . . 11 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×_c 𝑂))⟨𝐺, 𝑃⟩) = ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑋(Hom ‘𝑂)𝑃)))
182	120	xpeq2i 5702	. . . . . . . . . . 11 ⊢ ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑋(Hom ‘𝑂)𝑃)) = ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))
183	181, 182	eqtrdi 2788	. . . . . . . . . 10 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×_c 𝑂))⟨𝐺, 𝑃⟩) = ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋)))
184		df-ov 7408	. . . . . . . . . . . . 13 ⊢ (𝐹(1^st ‘𝑍)𝑋) = ((1^st ‘𝑍)‘⟨𝐹, 𝑋⟩)
185		df-ov 7408	. . . . . . . . . . . . 13 ⊢ (𝐺(1^st ‘𝑍)𝑃) = ((1^st ‘𝑍)‘⟨𝐺, 𝑃⟩)
186	184, 185	oveq12i 7417	. . . . . . . . . . . 12 ⊢ ((𝐹(1^st ‘𝑍)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝑍)𝑃)) = (((1^st ‘𝑍)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝑍)‘⟨𝐺, 𝑃⟩))
187	186	eqcomi 2741	. . . . . . . . . . 11 ⊢ (((1^st ‘𝑍)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝑍)‘⟨𝐺, 𝑃⟩)) = ((𝐹(1^st ‘𝑍)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝑍)𝑃))
188	187	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → (((1^st ‘𝑍)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝑍)‘⟨𝐺, 𝑃⟩)) = ((𝐹(1^st ‘𝑍)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝑍)𝑃)))
189	183, 188	feq23d 6709	. . . . . . . . 9 ⊢ (𝜑 → ((⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩):(⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×_c 𝑂))⟨𝐺, 𝑃⟩)⟶(((1^st ‘𝑍)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝑍)‘⟨𝐺, 𝑃⟩)) ↔ (⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩):((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))⟶((𝐹(1^st ‘𝑍)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝑍)𝑃))))
190	180, 189	mpbid 231	. . . . . . . 8 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩):((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))⟶((𝐹(1^st ‘𝑍)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝑍)𝑃)))
191	190, 34, 30	fovcdmd 7575	. . . . . . 7 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾) ∈ ((𝐹(1^st ‘𝑍)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝑍)𝑃)))
192		eqid 2732	. . . . . . . . . . 11 ⊢ (Base‘𝑇) = (Base‘𝑇)
193	165, 192, 177	funcf1 17812	. . . . . . . . . 10 ⊢ (𝜑 → (1^st ‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
194	193, 54, 28	fovcdmd 7575	. . . . . . . . 9 ⊢ (𝜑 → (𝐹(1^st ‘𝑍)𝑋) ∈ (Base‘𝑇))
195	169, 19	setcbas 18024	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 = (Base‘𝑇))
196	194, 195	eleqtrrd 2836	. . . . . . . 8 ⊢ (𝜑 → (𝐹(1^st ‘𝑍)𝑋) ∈ 𝑉)
197	193, 62, 27	fovcdmd 7575	. . . . . . . . 9 ⊢ (𝜑 → (𝐺(1^st ‘𝑍)𝑃) ∈ (Base‘𝑇))
198	197, 195	eleqtrrd 2836	. . . . . . . 8 ⊢ (𝜑 → (𝐺(1^st ‘𝑍)𝑃) ∈ 𝑉)
199	169, 19, 167, 196, 198	elsetchom 18027	. . . . . . 7 ⊢ (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾) ∈ ((𝐹(1^st ‘𝑍)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝑍)𝑃)) ↔ (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾):(𝐹(1^st ‘𝑍)𝑋)⟶(𝐺(1^st ‘𝑍)𝑃)))
200	191, 199	mpbid 231	. . . . . 6 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾):(𝐹(1^st ‘𝑍)𝑋)⟶(𝐺(1^st ‘𝑍)𝑃))
201	16, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 54, 28, 62, 27, 34, 30	yonedalem22 18227	. . . . . . . 8 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾) = (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(2^nd ‘𝐻)⟨((1^st ‘𝑌)‘𝑃), 𝐺⟩)𝐴))
202	8	oppccat 17664	. . . . . . . . . . 11 ⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat)
203	17, 202	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑂 ∈ Cat)
204	18	setccat 18031	. . . . . . . . . . 11 ⊢ (𝑈 ∈ V → 𝑆 ∈ Cat)
205	22, 204	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ Cat)
206	6, 203, 205	fuccat 17919	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ Cat)
207	170, 206, 43, 14, 45, 54, 82, 62, 12, 31, 34	hof2val 18205	. . . . . . . 8 ⊢ (𝜑 → (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(2^nd ‘𝐻)⟨((1^st ‘𝑌)‘𝑃), 𝐺⟩)𝐴) = (𝑏 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))))
208	201, 207	eqtrd 2772	. . . . . . 7 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾) = (𝑏 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))))
209	16, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 54, 28	yonedalem21 18222	. . . . . . 7 ⊢ (𝜑 → (𝐹(1^st ‘𝑍)𝑋) = (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹))
210	16, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 62, 27	yonedalem21 18222	. . . . . . 7 ⊢ (𝜑 → (𝐺(1^st ‘𝑍)𝑃) = (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺))
211	208, 209, 210	feq123d 6703	. . . . . 6 ⊢ (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾):(𝐹(1^st ‘𝑍)𝑋)⟶(𝐺(1^st ‘𝑍)𝑃) ↔ (𝑏 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))):(((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)⟶(((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺)))
212	200, 211	mpbid 231	. . . . 5 ⊢ (𝜑 → (𝑏 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))):(((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)⟶(((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺))
213		eqid 2732	. . . . . 6 ⊢ (𝑏 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))) = (𝑏 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)))
214	213	fmpt 7106	. . . . 5 ⊢ (∀𝑏 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)) ∈ (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺) ↔ (𝑏 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))):(((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)⟶(((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺))
215	212, 214	sylibr 233	. . . 4 ⊢ (𝜑 → ∀𝑏 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)) ∈ (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺))
216		yonedalem3.m	. . . . . 6 ⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1^st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥))))
217	16, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 62, 27, 216	yonedalem3a 18223	. . . . 5 ⊢ (𝜑 → ((𝐺𝑀𝑃) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺) ↦ ((𝑎‘𝑃)‘( 1 ‘𝑃))) ∧ (𝐺𝑀𝑃):(𝐺(1^st ‘𝑍)𝑃)⟶(𝐺(1^st ‘𝐸)𝑃)))
218	217	simpld 495	. . . 4 ⊢ (𝜑 → (𝐺𝑀𝑃) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺) ↦ ((𝑎‘𝑃)‘( 1 ‘𝑃))))
219		fveq1 6887	. . . . 5 ⊢ (𝑎 = ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)) → (𝑎‘𝑃) = (((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃))
220	219	fveq1d 6890	. . . 4 ⊢ (𝑎 = ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)) → ((𝑎‘𝑃)‘( 1 ‘𝑃)) = ((((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃)‘( 1 ‘𝑃)))
221	215, 208, 218, 220	fmptcof 7124	. . 3 ⊢ (𝜑 → ((𝐺𝑀𝑃) ∘ (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾)) = (𝑏 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃)‘( 1 ‘𝑃))))
222		eqid 2732	. . . . . . 7 ⊢ (⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩) = (⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)
223	172, 203, 205, 10, 118, 11, 7, 54, 62, 28, 27, 222, 34, 121	evlf2val 18168	. . . . . 6 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) = ((𝐴‘𝑃)(⟨((1^st ‘𝐹)‘𝑋), ((1^st ‘𝐹)‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)))
224	18, 22, 11, 137, 60, 67, 145, 77	setcco 18029	. . . . . 6 ⊢ (𝜑 → ((𝐴‘𝑃)(⟨((1^st ‘𝐹)‘𝑋), ((1^st ‘𝐹)‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)) = ((𝐴‘𝑃) ∘ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)))
225	223, 224	eqtrd 2772	. . . . 5 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) = ((𝐴‘𝑃) ∘ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)))
226	225	coeq1d 5859	. . . 4 ⊢ (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) ∘ (𝐹𝑀𝑋)) = (((𝐴‘𝑃) ∘ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)) ∘ (𝐹𝑀𝑋)))
227	16, 9, 99, 8, 18, 169, 6, 170, 171, 172, 173, 17, 19, 23, 20, 54, 28, 216	yonedalem3a 18223	. . . . . . . 8 ⊢ (𝜑 → ((𝐹𝑀𝑋) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋))) ∧ (𝐹𝑀𝑋):(𝐹(1^st ‘𝑍)𝑋)⟶(𝐹(1^st ‘𝐸)𝑋)))
228	227	simprd 496	. . . . . . 7 ⊢ (𝜑 → (𝐹𝑀𝑋):(𝐹(1^st ‘𝑍)𝑋)⟶(𝐹(1^st ‘𝐸)𝑋))
229	227	simpld 495	. . . . . . . 8 ⊢ (𝜑 → (𝐹𝑀𝑋) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋))))
230	172, 203, 205, 10, 54, 28	evlf1 18169	. . . . . . . 8 ⊢ (𝜑 → (𝐹(1^st ‘𝐸)𝑋) = ((1^st ‘𝐹)‘𝑋))
231	229, 209, 230	feq123d 6703	. . . . . . 7 ⊢ (𝜑 → ((𝐹𝑀𝑋):(𝐹(1^st ‘𝑍)𝑋)⟶(𝐹(1^st ‘𝐸)𝑋) ↔ (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋))):(((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)⟶((1^st ‘𝐹)‘𝑋)))
232	228, 231	mpbid 231	. . . . . 6 ⊢ (𝜑 → (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋))):(((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)⟶((1^st ‘𝐹)‘𝑋))
233		eqid 2732	. . . . . . 7 ⊢ (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋))) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋)))
234	233	fmpt 7106	. . . . . 6 ⊢ (∀𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)((𝑎‘𝑋)‘( 1 ‘𝑋)) ∈ ((1^st ‘𝐹)‘𝑋) ↔ (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋))):(((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)⟶((1^st ‘𝐹)‘𝑋))
235	232, 234	sylibr 233	. . . . 5 ⊢ (𝜑 → ∀𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)((𝑎‘𝑋)‘( 1 ‘𝑋)) ∈ ((1^st ‘𝐹)‘𝑋))
236		fcompt 7127	. . . . . 6 ⊢ (((𝐴‘𝑃):((1^st ‘𝐹)‘𝑃)⟶((1^st ‘𝐺)‘𝑃) ∧ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾):((1^st ‘𝐹)‘𝑋)⟶((1^st ‘𝐹)‘𝑃)) → ((𝐴‘𝑃) ∘ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)) = (𝑦 ∈ ((1^st ‘𝐹)‘𝑋) ↦ ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘𝑦))))
237	77, 145, 236	syl2anc 584	. . . . 5 ⊢ (𝜑 → ((𝐴‘𝑃) ∘ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)) = (𝑦 ∈ ((1^st ‘𝐹)‘𝑋) ↦ ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘𝑦))))
238		2fveq3 6893	. . . . 5 ⊢ (𝑦 = ((𝑎‘𝑋)‘( 1 ‘𝑋)) → ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘𝑦)) = ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋)))))
239	235, 229, 237, 238	fmptcof 7124	. . . 4 ⊢ (𝜑 → (((𝐴‘𝑃) ∘ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)) ∘ (𝐹𝑀𝑋)) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))))
240	226, 239	eqtrd 2772	. . 3 ⊢ (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) ∘ (𝐹𝑀𝑋)) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))))
241	163, 221, 240	3eqtr4d 2782	. 2 ⊢ (𝜑 → ((𝐺𝑀𝑃) ∘ (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾)) = ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) ∘ (𝐹𝑀𝑋)))
242		eqid 2732	. . 3 ⊢ (comp‘𝑇) = (comp‘𝑇)
243	174	simprd 496	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ ((𝑄 ×_c 𝑂) Func 𝑇))
244		1st2ndbr 8024	. . . . . . 7 ⊢ ((Rel ((𝑄 ×_c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×_c 𝑂) Func 𝑇)) → (1^st ‘𝐸)((𝑄 ×_c 𝑂) Func 𝑇)(2^nd ‘𝐸))
245	168, 243, 244	sylancr 587	. . . . . 6 ⊢ (𝜑 → (1^st ‘𝐸)((𝑄 ×_c 𝑂) Func 𝑇)(2^nd ‘𝐸))
246	165, 192, 245	funcf1 17812	. . . . 5 ⊢ (𝜑 → (1^st ‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
247	246, 62, 27	fovcdmd 7575	. . . 4 ⊢ (𝜑 → (𝐺(1^st ‘𝐸)𝑃) ∈ (Base‘𝑇))
248	247, 195	eleqtrrd 2836	. . 3 ⊢ (𝜑 → (𝐺(1^st ‘𝐸)𝑃) ∈ 𝑉)
249	217	simprd 496	. . 3 ⊢ (𝜑 → (𝐺𝑀𝑃):(𝐺(1^st ‘𝑍)𝑃)⟶(𝐺(1^st ‘𝐸)𝑃))
250	169, 19, 242, 196, 198, 248, 200, 249	setcco 18029	. 2 ⊢ (𝜑 → ((𝐺𝑀𝑃)(⟨(𝐹(1^st ‘𝑍)𝑋), (𝐺(1^st ‘𝑍)𝑃)⟩(comp‘𝑇)(𝐺(1^st ‘𝐸)𝑃))(𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾)) = ((𝐺𝑀𝑃) ∘ (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾)))
251	246, 54, 28	fovcdmd 7575	. . . 4 ⊢ (𝜑 → (𝐹(1^st ‘𝐸)𝑋) ∈ (Base‘𝑇))
252	251, 195	eleqtrrd 2836	. . 3 ⊢ (𝜑 → (𝐹(1^st ‘𝐸)𝑋) ∈ 𝑉)
253	165, 166, 167, 245, 178, 179	funcf2 17814	. . . . . 6 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩):(⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×_c 𝑂))⟨𝐺, 𝑃⟩)⟶(((1^st ‘𝐸)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝐸)‘⟨𝐺, 𝑃⟩)))
254		df-ov 7408	. . . . . . . . . 10 ⊢ (𝐹(1^st ‘𝐸)𝑋) = ((1^st ‘𝐸)‘⟨𝐹, 𝑋⟩)
255		df-ov 7408	. . . . . . . . . 10 ⊢ (𝐺(1^st ‘𝐸)𝑃) = ((1^st ‘𝐸)‘⟨𝐺, 𝑃⟩)
256	254, 255	oveq12i 7417	. . . . . . . . 9 ⊢ ((𝐹(1^st ‘𝐸)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝐸)𝑃)) = (((1^st ‘𝐸)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝐸)‘⟨𝐺, 𝑃⟩))
257	256	eqcomi 2741	. . . . . . . 8 ⊢ (((1^st ‘𝐸)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝐸)‘⟨𝐺, 𝑃⟩)) = ((𝐹(1^st ‘𝐸)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝐸)𝑃))
258	257	a1i 11	. . . . . . 7 ⊢ (𝜑 → (((1^st ‘𝐸)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝐸)‘⟨𝐺, 𝑃⟩)) = ((𝐹(1^st ‘𝐸)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝐸)𝑃)))
259	183, 258	feq23d 6709	. . . . . 6 ⊢ (𝜑 → ((⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩):(⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×_c 𝑂))⟨𝐺, 𝑃⟩)⟶(((1^st ‘𝐸)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝐸)‘⟨𝐺, 𝑃⟩)) ↔ (⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩):((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))⟶((𝐹(1^st ‘𝐸)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝐸)𝑃))))
260	253, 259	mpbid 231	. . . . 5 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩):((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))⟶((𝐹(1^st ‘𝐸)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝐸)𝑃)))
261	260, 34, 30	fovcdmd 7575	. . . 4 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) ∈ ((𝐹(1^st ‘𝐸)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝐸)𝑃)))
262	169, 19, 167, 252, 248	elsetchom 18027	. . . 4 ⊢ (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) ∈ ((𝐹(1^st ‘𝐸)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝐸)𝑃)) ↔ (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾):(𝐹(1^st ‘𝐸)𝑋)⟶(𝐺(1^st ‘𝐸)𝑃)))
263	261, 262	mpbid 231	. . 3 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾):(𝐹(1^st ‘𝐸)𝑋)⟶(𝐺(1^st ‘𝐸)𝑃))
264	169, 19, 242, 196, 252, 248, 228, 263	setcco 18029	. 2 ⊢ (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾)(⟨(𝐹(1^st ‘𝑍)𝑋), (𝐹(1^st ‘𝐸)𝑋)⟩(comp‘𝑇)(𝐺(1^st ‘𝐸)𝑃))(𝐹𝑀𝑋)) = ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) ∘ (𝐹𝑀𝑋)))
265	241, 250, 264	3eqtr4d 2782	1 ⊢ (𝜑 → ((𝐺𝑀𝑃)(⟨(𝐹(1^st ‘𝑍)𝑋), (𝐺(1^st ‘𝑍)𝑃)⟩(comp‘𝑇)(𝐺(1^st ‘𝐸)𝑃))(𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾)) = ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾)(⟨(𝐹(1^st ‘𝑍)𝑋), (𝐹(1^st ‘𝐸)𝑋)⟩(comp‘𝑇)(𝐺(1^st ‘𝐸)𝑃))(𝐹𝑀𝑋)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∀wral 3061 Vcvv 3474 ∪ cun 3945 ⊆ wss 3947 ⟨cop 4633 class class class wbr 5147 ↦ cmpt 5230 × cxp 5673 ran crn 5676 ∘ ccom 5679 Rel wrel 5680 ⟶wf 6536 ‘cfv 6540 (class class class)co 7405 ∈ cmpo 7407 1^st c1st 7969 2^nd c2nd 7970 tpos ctpos 8206 Basecbs 17140 Hom chom 17204 compcco 17205 Catccat 17604 Idccid 17605 Hom_f chomf 17606 oppCatcoppc 17651 Func cfunc 17800 ∘_func ccofu 17802 Nat cnat 17888 FuncCat cfuc 17889 SetCatcsetc 18021 ×_c cxpc 18116 1^st_F c1stf 18117 2^nd_F c2ndf 18118 ⟨,⟩_F cprf 18119 eval_F cevlf 18158 Hom_Fchof 18197 Yoncyon 18198

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-tp 4632 df-op 4634 df-uni 4908 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6297 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7852 df-1st 7971 df-2nd 7972 df-tpos 8207 df-frecs 8262 df-wrecs 8293 df-recs 8367 df-rdg 8406 df-1o 8462 df-er 8699 df-map 8818 df-pm 8819 df-ixp 8888 df-en 8936 df-dom 8937 df-sdom 8938 df-fin 8939 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11442 df-neg 11443 df-nn 12209 df-2 12271 df-3 12272 df-4 12273 df-5 12274 df-6 12275 df-7 12276 df-8 12277 df-9 12278 df-n0 12469 df-z 12555 df-dec 12674 df-uz 12819 df-fz 13481 df-struct 17076 df-sets 17093 df-slot 17111 df-ndx 17123 df-base 17141 df-ress 17170 df-hom 17217 df-cco 17218 df-cat 17608 df-cid 17609 df-homf 17610 df-comf 17611 df-oppc 17652 df-ssc 17753 df-resc 17754 df-subc 17755 df-func 17804 df-cofu 17806 df-nat 17890 df-fuc 17891 df-setc 18022 df-xpc 18120 df-1stf 18121 df-2ndf 18122 df-prf 18123 df-evlf 18162 df-curf 18163 df-hof 18199 df-yon 18200

This theorem is referenced by: yonedalem3 18229

W3C validator