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 18256

Description: Lemma for yoneda 18260. (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 7422	. . . . . . . 8 ⊢ (𝑏 = 𝑎 → (𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏) = (𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎))
2	1	oveq1d 7429	. . . . . . 7 ⊢ (𝑏 = 𝑎 → ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)) = ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)))
3	2	fveq1d 6893	. . . . . 6 ⊢ (𝑏 = 𝑎 → (((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃) = (((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃))
4	3	fveq1d 6893	. . . . 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 5255	. . . 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 2727	. . . . . . . . 9 ⊢ (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆)
8		yoneda.o	. . . . . . . . . 10 ⊢ 𝑂 = (oppCat‘𝐶)
9		yoneda.b	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝐶)
10	8, 9	oppcbas 17684	. . . . . . . . 9 ⊢ 𝐵 = (Base‘𝑂)
11		eqid 2727	. . . . . . . . 9 ⊢ (comp‘𝑆) = (comp‘𝑆)
12		eqid 2727	. . . . . . . . 9 ⊢ (comp‘𝑄) = (comp‘𝑄)
13		eqid 2727	. . . . . . . . . . . 12 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
14	6, 7	fuchom 17937	. . . . . . . . . . . 12 ⊢ (𝑂 Nat 𝑆) = (Hom ‘𝑄)
15		relfunc 17833	. . . . . . . . . . . . 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 4184	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 ⊆ 𝑉)
22	19, 21	ssexd 5318	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ∈ V)
23		yoneda.u	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran (Hom_f ‘𝐶) ⊆ 𝑈)
24	16, 17, 8, 18, 6, 22, 23	yoncl 18239	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ∈ (𝐶 Func 𝑄))
25		1st2ndbr 8038	. . . . . . . . . . . . 13 ⊢ ((Rel (𝐶 Func 𝑄) ∧ 𝑌 ∈ (𝐶 Func 𝑄)) → (1^st ‘𝑌)(𝐶 Func 𝑄)(2^nd ‘𝑌))
26	15, 24, 25	sylancr 586	. . . . . . . . . . . 12 ⊢ (𝜑 → (1^st ‘𝑌)(𝐶 Func 𝑄)(2^nd ‘𝑌))
27		yonedalem22.p	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ 𝐵)
28		yonedalem21.x	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
29	9, 13, 14, 26, 27, 28	funcf2 17839	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃(2^nd ‘𝑌)𝑋):(𝑃(Hom ‘𝐶)𝑋)⟶(((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑋)))
30		yonedalem22.k	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋))
31	29, 30	ffvelcdmd 7089	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑃(2^nd ‘𝑌)𝑋)‘𝐾) ∈ (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑋)))
32	31	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑃(2^nd ‘𝑌)𝑋)‘𝐾) ∈ (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑋)))
33		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹))
34		yonedalem22.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺))
35	34	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺))
36	6, 7, 12, 33, 35	fuccocl 17941	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎) ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐺))
37	27	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑃 ∈ 𝐵)
38	6, 7, 10, 11, 12, 32, 36, 37	fuccoval 17940	. . . . . . . 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 17940	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)‘𝑃) = ((𝐴‘𝑃)(⟨((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃), ((1^st ‘𝐹)‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))(𝑎‘𝑃)))
40	22	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑈 ∈ V)
41		eqid 2727	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝑆) = (Base‘𝑆)
42		relfunc 17833	. . . . . . . . . . . . . . . 16 ⊢ Rel (𝑂 Func 𝑆)
43	6	fucbas 17936	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑂 Func 𝑆) = (Base‘𝑄)
44	9, 43, 26	funcf1 17837	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1^st ‘𝑌):𝐵⟶(𝑂 Func 𝑆))
45	44, 28	ffvelcdmd 7089	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1^st ‘𝑌)‘𝑋) ∈ (𝑂 Func 𝑆))
46		1st2ndbr 8038	. . . . . . . . . . . . . . . 16 ⊢ ((Rel (𝑂 Func 𝑆) ∧ ((1^st ‘𝑌)‘𝑋) ∈ (𝑂 Func 𝑆)) → (1^st ‘((1^st ‘𝑌)‘𝑋))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑋)))
47	42, 45, 46	sylancr 586	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1^st ‘((1^st ‘𝑌)‘𝑋))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑋)))
48	10, 41, 47	funcf1 17837	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1^st ‘((1^st ‘𝑌)‘𝑋)):𝐵⟶(Base‘𝑆))
49	18, 22	setcbas 18052	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 = (Base‘𝑆))
50	49	feq3d 6703	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑋)):𝐵⟶𝑈 ↔ (1^st ‘((1^st ‘𝑌)‘𝑋)):𝐵⟶(Base‘𝑆)))
51	48, 50	mpbird 257	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1^st ‘((1^st ‘𝑌)‘𝑋)):𝐵⟶𝑈)
52	51, 27	ffvelcdmd 7089	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃) ∈ 𝑈)
53	52	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃) ∈ 𝑈)
54		yonedalem21.f	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑆))
55		1st2ndbr 8038	. . . . . . . . . . . . . . . 16 ⊢ ((Rel (𝑂 Func 𝑆) ∧ 𝐹 ∈ (𝑂 Func 𝑆)) → (1^st ‘𝐹)(𝑂 Func 𝑆)(2^nd ‘𝐹))
56	42, 54, 55	sylancr 586	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1^st ‘𝐹)(𝑂 Func 𝑆)(2^nd ‘𝐹))
57	10, 41, 56	funcf1 17837	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1^st ‘𝐹):𝐵⟶(Base‘𝑆))
58	49	feq3d 6703	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘𝐹):𝐵⟶𝑈 ↔ (1^st ‘𝐹):𝐵⟶(Base‘𝑆)))
59	57, 58	mpbird 257	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1^st ‘𝐹):𝐵⟶𝑈)
60	59, 27	ffvelcdmd 7089	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1^st ‘𝐹)‘𝑃) ∈ 𝑈)
61	60	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘𝐹)‘𝑃) ∈ 𝑈)
62		yonedalem22.g	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐺 ∈ (𝑂 Func 𝑆))
63		1st2ndbr 8038	. . . . . . . . . . . . . . . 16 ⊢ ((Rel (𝑂 Func 𝑆) ∧ 𝐺 ∈ (𝑂 Func 𝑆)) → (1^st ‘𝐺)(𝑂 Func 𝑆)(2^nd ‘𝐺))
64	42, 62, 63	sylancr 586	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1^st ‘𝐺)(𝑂 Func 𝑆)(2^nd ‘𝐺))
65	10, 41, 64	funcf1 17837	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1^st ‘𝐺):𝐵⟶(Base‘𝑆))
66	65, 27	ffvelcdmd 7089	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1^st ‘𝐺)‘𝑃) ∈ (Base‘𝑆))
67	66, 49	eleqtrrd 2831	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1^st ‘𝐺)‘𝑃) ∈ 𝑈)
68	67	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘𝐺)‘𝑃) ∈ 𝑈)
69	7, 33	nat1st2nd 17926	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑎 ∈ (⟨(1^st ‘((1^st ‘𝑌)‘𝑋)), (2^nd ‘((1^st ‘𝑌)‘𝑋))⟩(𝑂 Nat 𝑆)⟨(1^st ‘𝐹), (2^nd ‘𝐹)⟩))
70		eqid 2727	. . . . . . . . . . . . 13 ⊢ (Hom ‘𝑆) = (Hom ‘𝑆)
71	7, 69, 10, 70, 37	natcl 17928	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝑎‘𝑃) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑃)))
72	18, 40, 70, 53, 61	elsetchom 18055	. . . . . . . . . . . 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 17926	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ (⟨(1^st ‘𝐹), (2^nd ‘𝐹)⟩(𝑂 Nat 𝑆)⟨(1^st ‘𝐺), (2^nd ‘𝐺)⟩))
75	7, 74, 10, 70, 27	natcl 17928	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴‘𝑃) ∈ (((1^st ‘𝐹)‘𝑃)(Hom ‘𝑆)((1^st ‘𝐺)‘𝑃)))
76	18, 22, 70, 60, 67	elsetchom 18055	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴‘𝑃) ∈ (((1^st ‘𝐹)‘𝑃)(Hom ‘𝑆)((1^st ‘𝐺)‘𝑃)) ↔ (𝐴‘𝑃):((1^st ‘𝐹)‘𝑃)⟶((1^st ‘𝐺)‘𝑃)))
77	75, 76	mpbid 231	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴‘𝑃):((1^st ‘𝐹)‘𝑃)⟶((1^st ‘𝐺)‘𝑃))
78	77	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝐴‘𝑃):((1^st ‘𝐹)‘𝑃)⟶((1^st ‘𝐺)‘𝑃))
79	18, 40, 11, 53, 61, 68, 73, 78	setcco 18057	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴‘𝑃)(⟨((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃), ((1^st ‘𝐹)‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))(𝑎‘𝑃)) = ((𝐴‘𝑃) ∘ (𝑎‘𝑃)))
80	39, 79	eqtrd 2767	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)‘𝑃) = ((𝐴‘𝑃) ∘ (𝑎‘𝑃)))
81	80	oveq1d 7429	. . . . . . . 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 7089	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘𝑌)‘𝑃) ∈ (𝑂 Func 𝑆))
83		1st2ndbr 8038	. . . . . . . . . . . . . 14 ⊢ ((Rel (𝑂 Func 𝑆) ∧ ((1^st ‘𝑌)‘𝑃) ∈ (𝑂 Func 𝑆)) → (1^st ‘((1^st ‘𝑌)‘𝑃))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑃)))
84	42, 82, 83	sylancr 586	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1^st ‘((1^st ‘𝑌)‘𝑃))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑃)))
85	10, 41, 84	funcf1 17837	. . . . . . . . . . . 12 ⊢ (𝜑 → (1^st ‘((1^st ‘𝑌)‘𝑃)):𝐵⟶(Base‘𝑆))
86	85, 27	ffvelcdmd 7089	. . . . . . . . . . 11 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃) ∈ (Base‘𝑆))
87	86, 49	eleqtrrd 2831	. . . . . . . . . 10 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃) ∈ 𝑈)
88	87	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃) ∈ 𝑈)
89	7, 31	nat1st2nd 17926	. . . . . . . . . . . 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 17928	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃)(Hom ‘𝑆)((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)))
91	18, 22, 70, 87, 52	elsetchom 18055	. . . . . . . . . . 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 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃):((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃)⟶((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃))
94		fco 6741	. . . . . . . . . 10 ⊢ (((𝐴‘𝑃):((1^st ‘𝐹)‘𝑃)⟶((1^st ‘𝐺)‘𝑃) ∧ (𝑎‘𝑃):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟶((1^st ‘𝐹)‘𝑃)) → ((𝐴‘𝑃) ∘ (𝑎‘𝑃)):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟶((1^st ‘𝐺)‘𝑃))
95	78, 73, 94	syl2anc 583	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴‘𝑃) ∘ (𝑎‘𝑃)):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟶((1^st ‘𝐺)‘𝑃))
96	18, 40, 11, 88, 53, 68, 93, 95	setcco 18057	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴‘𝑃) ∘ (𝑎‘𝑃))(⟨((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃), ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))(((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)) = (((𝐴‘𝑃) ∘ (𝑎‘𝑃)) ∘ (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)))
97	38, 81, 96	3eqtrd 2771	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃) = (((𝐴‘𝑃) ∘ (𝑎‘𝑃)) ∘ (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)))
98	97	fveq1d 6893	. . . . . 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 17647	. . . . . . . . 9 ⊢ (𝜑 → ( 1 ‘𝑃) ∈ (𝑃(Hom ‘𝐶)𝑃))
101	16, 9, 17, 27, 13, 27	yon11 18241	. . . . . . . . 9 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃) = (𝑃(Hom ‘𝐶)𝑃))
102	100, 101	eleqtrrd 2831	. . . . . . . 8 ⊢ (𝜑 → ( 1 ‘𝑃) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃))
103	102	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1 ‘𝑃) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃))
104		fvco3 6991	. . . . . . 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 583	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝐴‘𝑃) ∘ (𝑎‘𝑃)) ∘ (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃))‘( 1 ‘𝑃)) = (((𝐴‘𝑃) ∘ (𝑎‘𝑃))‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))))
106	93, 103	ffvelcdmd 7089	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃))
107		fvco3 6991	. . . . . . . 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 583	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴‘𝑃) ∘ (𝑎‘𝑃))‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))) = ((𝐴‘𝑃)‘((𝑎‘𝑃)‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)))))
109	17	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐶 ∈ Cat)
110	28	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑋 ∈ 𝐵)
111		eqid 2727	. . . . . . . . . . . 12 ⊢ (comp‘𝐶) = (comp‘𝐶)
112	30	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋))
113	100	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1 ‘𝑃) ∈ (𝑃(Hom ‘𝐶)𝑃))
114	16, 9, 109, 37, 13, 110, 111, 37, 112, 113	yon2 18243	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)) = (𝐾(⟨𝑃, 𝑃⟩(comp‘𝐶)𝑋)( 1 ‘𝑃)))
115	9, 13, 99, 109, 37, 111, 110, 112	catrid 17649	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝐾(⟨𝑃, 𝑃⟩(comp‘𝐶)𝑋)( 1 ‘𝑃)) = 𝐾)
116	114, 115	eqtrd 2767	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)) = 𝐾)
117	116	fveq2d 6895	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑃)‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))) = ((𝑎‘𝑃)‘𝐾))
118		eqid 2727	. . . . . . . . . . . . . . 15 ⊢ (Hom ‘𝑂) = (Hom ‘𝑂)
119	10, 118, 70, 47, 28, 27	funcf2 17839	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃):(𝑋(Hom ‘𝑂)𝑃)⟶(((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)))
120	13, 8	oppchom 17681	. . . . . . . . . . . . . . 15 ⊢ (𝑋(Hom ‘𝑂)𝑃) = (𝑃(Hom ‘𝐶)𝑋)
121	30, 120	eleqtrrdi 2839	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ (𝑋(Hom ‘𝑂)𝑃))
122	119, 121	ffvelcdmd 7089	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)))
123	51, 28	ffvelcdmd 7089	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋) ∈ 𝑈)
124	18, 22, 70, 123, 52	elsetchom 18055	. . . . . . . . . . . . 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 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)⟶((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃))
127	9, 13, 99, 17, 28	catidcl 17647	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( 1 ‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋))
128	16, 9, 17, 28, 13, 28	yon11 18241	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋) = (𝑋(Hom ‘𝐶)𝑋))
129	127, 128	eleqtrrd 2831	. . . . . . . . . . . 12 ⊢ (𝜑 → ( 1 ‘𝑋) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋))
130	129	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1 ‘𝑋) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋))
131		fvco3 6991	. . . . . . . . . . 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 583	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑎‘𝑃) ∘ ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾))‘( 1 ‘𝑋)) = ((𝑎‘𝑃)‘(((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)‘( 1 ‘𝑋))))
133	121	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐾 ∈ (𝑋(Hom ‘𝑂)𝑃))
134	7, 69, 10, 118, 11, 110, 37, 133	nati 17930	. . . . . . . . . . . 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 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋) ∈ 𝑈)
136	18, 40, 11, 135, 53, 61, 126, 73	setcco 18057	. . . . . . . . . . . 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 7089	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘𝐹)‘𝑋) ∈ 𝑈)
138	137	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘𝐹)‘𝑋) ∈ 𝑈)
139	7, 69, 10, 70, 110	natcl 17928	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝑎‘𝑋) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑋)))
140	18, 40, 70, 135, 138	elsetchom 18055	. . . . . . . . . . . . . 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 17839	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋(2^nd ‘𝐹)𝑃):(𝑋(Hom ‘𝑂)𝑃)⟶(((1^st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑃)))
143	142, 121	ffvelcdmd 7089	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∈ (((1^st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑃)))
144	18, 22, 70, 137, 60	elsetchom 18055	. . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾):((1^st ‘𝐹)‘𝑋)⟶((1^st ‘𝐹)‘𝑃))
147	18, 40, 11, 135, 138, 61, 141, 146	setcco 18057	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)(⟨((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋), ((1^st ‘𝐹)‘𝑋)⟩(comp‘𝑆)((1^st ‘𝐹)‘𝑃))(𝑎‘𝑋)) = (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋)))
148	134, 136, 147	3eqtr3d 2775	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑃) ∘ ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)) = (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋)))
149	148	fveq1d 6893	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑎‘𝑃) ∘ ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾))‘( 1 ‘𝑋)) = ((((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋))‘( 1 ‘𝑋)))
150	127	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1 ‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋))
151	16, 9, 109, 110, 13, 110, 111, 37, 112, 150	yon12 18242	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)‘( 1 ‘𝑋)) = (( 1 ‘𝑋)(⟨𝑃, 𝑋⟩(comp‘𝐶)𝑋)𝐾))
152	9, 13, 99, 109, 37, 111, 110, 112	catlid 17648	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (( 1 ‘𝑋)(⟨𝑃, 𝑋⟩(comp‘𝐶)𝑋)𝐾) = 𝐾)
153	151, 152	eqtrd 2767	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)‘( 1 ‘𝑋)) = 𝐾)
154	153	fveq2d 6895	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑃)‘(((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)‘( 1 ‘𝑋))) = ((𝑎‘𝑃)‘𝐾))
155	132, 149, 154	3eqtr3d 2775	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋))‘( 1 ‘𝑋)) = ((𝑎‘𝑃)‘𝐾))
156		fvco3 6991	. . . . . . . . . 10 ⊢ (((𝑎‘𝑋):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)⟶((1^st ‘𝐹)‘𝑋) ∧ ( 1 ‘𝑋) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)) → ((((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋))‘( 1 ‘𝑋)) = (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))
157	141, 130, 156	syl2anc 583	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋))‘( 1 ‘𝑋)) = (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))
158	117, 155, 157	3eqtr2d 2773	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑃)‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))) = (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))
159	158	fveq2d 6895	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴‘𝑃)‘((𝑎‘𝑃)‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)))) = ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋)))))
160	108, 159	eqtrd 2767	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴‘𝑃) ∘ (𝑎‘𝑃))‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))) = ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋)))))
161	98, 105, 160	3eqtrd 2771	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃)‘( 1 ‘𝑃)) = ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋)))))
162	161	mpteq2dva 5242	. . . 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 2779	. . 3 ⊢ (𝜑 → (𝑏 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃)‘( 1 ‘𝑃))) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))))
164		eqid 2727	. . . . . . . . . . 11 ⊢ (𝑄 ×_c 𝑂) = (𝑄 ×_c 𝑂)
165	164, 43, 10	xpcbas 18154	. . . . . . . . . 10 ⊢ ((𝑂 Func 𝑆) × 𝐵) = (Base‘(𝑄 ×_c 𝑂))
166		eqid 2727	. . . . . . . . . 10 ⊢ (Hom ‘(𝑄 ×_c 𝑂)) = (Hom ‘(𝑄 ×_c 𝑂))
167		eqid 2727	. . . . . . . . . 10 ⊢ (Hom ‘𝑇) = (Hom ‘𝑇)
168		relfunc 17833	. . . . . . . . . . 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 18249	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑍 ∈ ((𝑄 ×_c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×_c 𝑂) Func 𝑇)))
175	174	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑍 ∈ ((𝑄 ×_c 𝑂) Func 𝑇))
176		1st2ndbr 8038	. . . . . . . . . . 11 ⊢ ((Rel ((𝑄 ×_c 𝑂) Func 𝑇) ∧ 𝑍 ∈ ((𝑄 ×_c 𝑂) Func 𝑇)) → (1^st ‘𝑍)((𝑄 ×_c 𝑂) Func 𝑇)(2^nd ‘𝑍))
177	168, 175, 176	sylancr 586	. . . . . . . . . 10 ⊢ (𝜑 → (1^st ‘𝑍)((𝑄 ×_c 𝑂) Func 𝑇)(2^nd ‘𝑍))
178	54, 28	opelxpd 5711	. . . . . . . . . 10 ⊢ (𝜑 → ⟨𝐹, 𝑋⟩ ∈ ((𝑂 Func 𝑆) × 𝐵))
179	62, 27	opelxpd 5711	. . . . . . . . . 10 ⊢ (𝜑 → ⟨𝐺, 𝑃⟩ ∈ ((𝑂 Func 𝑆) × 𝐵))
180	165, 166, 167, 177, 178, 179	funcf2 17839	. . . . . . . . 9 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩):(⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×_c 𝑂))⟨𝐺, 𝑃⟩)⟶(((1^st ‘𝑍)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝑍)‘⟨𝐺, 𝑃⟩)))
181	164, 43, 10, 14, 118, 54, 28, 62, 27, 166	xpchom2 18162	. . . . . . . . . . 11 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×_c 𝑂))⟨𝐺, 𝑃⟩) = ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑋(Hom ‘𝑂)𝑃)))
182	120	xpeq2i 5699	. . . . . . . . . . 11 ⊢ ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑋(Hom ‘𝑂)𝑃)) = ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))
183	181, 182	eqtrdi 2783	. . . . . . . . . 10 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×_c 𝑂))⟨𝐺, 𝑃⟩) = ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋)))
184		df-ov 7417	. . . . . . . . . . . . 13 ⊢ (𝐹(1^st ‘𝑍)𝑋) = ((1^st ‘𝑍)‘⟨𝐹, 𝑋⟩)
185		df-ov 7417	. . . . . . . . . . . . 13 ⊢ (𝐺(1^st ‘𝑍)𝑃) = ((1^st ‘𝑍)‘⟨𝐺, 𝑃⟩)
186	184, 185	oveq12i 7426	. . . . . . . . . . . 12 ⊢ ((𝐹(1^st ‘𝑍)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝑍)𝑃)) = (((1^st ‘𝑍)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝑍)‘⟨𝐺, 𝑃⟩))
187	186	eqcomi 2736	. . . . . . . . . . 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 6711	. . . . . . . . 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 7585	. . . . . . 7 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾) ∈ ((𝐹(1^st ‘𝑍)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝑍)𝑃)))
192		eqid 2727	. . . . . . . . . . 11 ⊢ (Base‘𝑇) = (Base‘𝑇)
193	165, 192, 177	funcf1 17837	. . . . . . . . . 10 ⊢ (𝜑 → (1^st ‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
194	193, 54, 28	fovcdmd 7585	. . . . . . . . 9 ⊢ (𝜑 → (𝐹(1^st ‘𝑍)𝑋) ∈ (Base‘𝑇))
195	169, 19	setcbas 18052	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 = (Base‘𝑇))
196	194, 195	eleqtrrd 2831	. . . . . . . 8 ⊢ (𝜑 → (𝐹(1^st ‘𝑍)𝑋) ∈ 𝑉)
197	193, 62, 27	fovcdmd 7585	. . . . . . . . 9 ⊢ (𝜑 → (𝐺(1^st ‘𝑍)𝑃) ∈ (Base‘𝑇))
198	197, 195	eleqtrrd 2831	. . . . . . . 8 ⊢ (𝜑 → (𝐺(1^st ‘𝑍)𝑃) ∈ 𝑉)
199	169, 19, 167, 196, 198	elsetchom 18055	. . . . . . 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 18255	. . . . . . . 8 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾) = (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(2^nd ‘𝐻)⟨((1^st ‘𝑌)‘𝑃), 𝐺⟩)𝐴))
202	8	oppccat 17689	. . . . . . . . . . 11 ⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat)
203	17, 202	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑂 ∈ Cat)
204	18	setccat 18059	. . . . . . . . . . 11 ⊢ (𝑈 ∈ V → 𝑆 ∈ Cat)
205	22, 204	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ Cat)
206	6, 203, 205	fuccat 17947	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ Cat)
207	170, 206, 43, 14, 45, 54, 82, 62, 12, 31, 34	hof2val 18233	. . . . . . . 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 2767	. . . . . . 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 18250	. . . . . . 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 18250	. . . . . . 7 ⊢ (𝜑 → (𝐺(1^st ‘𝑍)𝑃) = (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺))
211	208, 209, 210	feq123d 6705	. . . . . 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 2727	. . . . . 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 7114	. . . . 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 18251	. . . . 5 ⊢ (𝜑 → ((𝐺𝑀𝑃) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺) ↦ ((𝑎‘𝑃)‘( 1 ‘𝑃))) ∧ (𝐺𝑀𝑃):(𝐺(1^st ‘𝑍)𝑃)⟶(𝐺(1^st ‘𝐸)𝑃)))
218	217	simpld 494	. . . 4 ⊢ (𝜑 → (𝐺𝑀𝑃) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺) ↦ ((𝑎‘𝑃)‘( 1 ‘𝑃))))
219		fveq1 6890	. . . . 5 ⊢ (𝑎 = ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)) → (𝑎‘𝑃) = (((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃))
220	219	fveq1d 6893	. . . 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 7133	. . 3 ⊢ (𝜑 → ((𝐺𝑀𝑃) ∘ (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾)) = (𝑏 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃)‘( 1 ‘𝑃))))
222		eqid 2727	. . . . . . 7 ⊢ (⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩) = (⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)
223	172, 203, 205, 10, 118, 11, 7, 54, 62, 28, 27, 222, 34, 121	evlf2val 18196	. . . . . 6 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) = ((𝐴‘𝑃)(⟨((1^st ‘𝐹)‘𝑋), ((1^st ‘𝐹)‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)))
224	18, 22, 11, 137, 60, 67, 145, 77	setcco 18057	. . . . . 6 ⊢ (𝜑 → ((𝐴‘𝑃)(⟨((1^st ‘𝐹)‘𝑋), ((1^st ‘𝐹)‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)) = ((𝐴‘𝑃) ∘ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)))
225	223, 224	eqtrd 2767	. . . . 5 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) = ((𝐴‘𝑃) ∘ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)))
226	225	coeq1d 5858	. . . 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 18251	. . . . . . . 8 ⊢ (𝜑 → ((𝐹𝑀𝑋) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋))) ∧ (𝐹𝑀𝑋):(𝐹(1^st ‘𝑍)𝑋)⟶(𝐹(1^st ‘𝐸)𝑋)))
228	227	simprd 495	. . . . . . 7 ⊢ (𝜑 → (𝐹𝑀𝑋):(𝐹(1^st ‘𝑍)𝑋)⟶(𝐹(1^st ‘𝐸)𝑋))
229	227	simpld 494	. . . . . . . 8 ⊢ (𝜑 → (𝐹𝑀𝑋) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋))))
230	172, 203, 205, 10, 54, 28	evlf1 18197	. . . . . . . 8 ⊢ (𝜑 → (𝐹(1^st ‘𝐸)𝑋) = ((1^st ‘𝐹)‘𝑋))
231	229, 209, 230	feq123d 6705	. . . . . . 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 2727	. . . . . . 7 ⊢ (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋))) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋)))
234	233	fmpt 7114	. . . . . 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 7136	. . . . . 6 ⊢ (((𝐴‘𝑃):((1^st ‘𝐹)‘𝑃)⟶((1^st ‘𝐺)‘𝑃) ∧ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾):((1^st ‘𝐹)‘𝑋)⟶((1^st ‘𝐹)‘𝑃)) → ((𝐴‘𝑃) ∘ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)) = (𝑦 ∈ ((1^st ‘𝐹)‘𝑋) ↦ ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘𝑦))))
237	77, 145, 236	syl2anc 583	. . . . 5 ⊢ (𝜑 → ((𝐴‘𝑃) ∘ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)) = (𝑦 ∈ ((1^st ‘𝐹)‘𝑋) ↦ ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘𝑦))))
238		2fveq3 6896	. . . . 5 ⊢ (𝑦 = ((𝑎‘𝑋)‘( 1 ‘𝑋)) → ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘𝑦)) = ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋)))))
239	235, 229, 237, 238	fmptcof 7133	. . . 4 ⊢ (𝜑 → (((𝐴‘𝑃) ∘ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)) ∘ (𝐹𝑀𝑋)) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))))
240	226, 239	eqtrd 2767	. . 3 ⊢ (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) ∘ (𝐹𝑀𝑋)) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))))
241	163, 221, 240	3eqtr4d 2777	. 2 ⊢ (𝜑 → ((𝐺𝑀𝑃) ∘ (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾)) = ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) ∘ (𝐹𝑀𝑋)))
242		eqid 2727	. . 3 ⊢ (comp‘𝑇) = (comp‘𝑇)
243	174	simprd 495	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ ((𝑄 ×_c 𝑂) Func 𝑇))
244		1st2ndbr 8038	. . . . . . 7 ⊢ ((Rel ((𝑄 ×_c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×_c 𝑂) Func 𝑇)) → (1^st ‘𝐸)((𝑄 ×_c 𝑂) Func 𝑇)(2^nd ‘𝐸))
245	168, 243, 244	sylancr 586	. . . . . 6 ⊢ (𝜑 → (1^st ‘𝐸)((𝑄 ×_c 𝑂) Func 𝑇)(2^nd ‘𝐸))
246	165, 192, 245	funcf1 17837	. . . . 5 ⊢ (𝜑 → (1^st ‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
247	246, 62, 27	fovcdmd 7585	. . . 4 ⊢ (𝜑 → (𝐺(1^st ‘𝐸)𝑃) ∈ (Base‘𝑇))
248	247, 195	eleqtrrd 2831	. . 3 ⊢ (𝜑 → (𝐺(1^st ‘𝐸)𝑃) ∈ 𝑉)
249	217	simprd 495	. . 3 ⊢ (𝜑 → (𝐺𝑀𝑃):(𝐺(1^st ‘𝑍)𝑃)⟶(𝐺(1^st ‘𝐸)𝑃))
250	169, 19, 242, 196, 198, 248, 200, 249	setcco 18057	. 2 ⊢ (𝜑 → ((𝐺𝑀𝑃)(⟨(𝐹(1^st ‘𝑍)𝑋), (𝐺(1^st ‘𝑍)𝑃)⟩(comp‘𝑇)(𝐺(1^st ‘𝐸)𝑃))(𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾)) = ((𝐺𝑀𝑃) ∘ (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾)))
251	246, 54, 28	fovcdmd 7585	. . . 4 ⊢ (𝜑 → (𝐹(1^st ‘𝐸)𝑋) ∈ (Base‘𝑇))
252	251, 195	eleqtrrd 2831	. . 3 ⊢ (𝜑 → (𝐹(1^st ‘𝐸)𝑋) ∈ 𝑉)
253	165, 166, 167, 245, 178, 179	funcf2 17839	. . . . . 6 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩):(⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×_c 𝑂))⟨𝐺, 𝑃⟩)⟶(((1^st ‘𝐸)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝐸)‘⟨𝐺, 𝑃⟩)))
254		df-ov 7417	. . . . . . . . . 10 ⊢ (𝐹(1^st ‘𝐸)𝑋) = ((1^st ‘𝐸)‘⟨𝐹, 𝑋⟩)
255		df-ov 7417	. . . . . . . . . 10 ⊢ (𝐺(1^st ‘𝐸)𝑃) = ((1^st ‘𝐸)‘⟨𝐺, 𝑃⟩)
256	254, 255	oveq12i 7426	. . . . . . . . 9 ⊢ ((𝐹(1^st ‘𝐸)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝐸)𝑃)) = (((1^st ‘𝐸)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝐸)‘⟨𝐺, 𝑃⟩))
257	256	eqcomi 2736	. . . . . . . 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 6711	. . . . . 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 7585	. . . 4 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) ∈ ((𝐹(1^st ‘𝐸)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝐸)𝑃)))
262	169, 19, 167, 252, 248	elsetchom 18055	. . . 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 18057	. 2 ⊢ (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾)(⟨(𝐹(1^st ‘𝑍)𝑋), (𝐹(1^st ‘𝐸)𝑋)⟩(comp‘𝑇)(𝐺(1^st ‘𝐸)𝑃))(𝐹𝑀𝑋)) = ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) ∘ (𝐹𝑀𝑋)))
265	241, 250, 264	3eqtr4d 2777	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 395 = wceq 1534 ∈ wcel 2099 ∀wral 3056 Vcvv 3469 ∪ cun 3942 ⊆ wss 3944 ⟨cop 4630 class class class wbr 5142 ↦ cmpt 5225 × cxp 5670 ran crn 5673 ∘ ccom 5676 Rel wrel 5677 ⟶wf 6538 ‘cfv 6542 (class class class)co 7414 ∈ cmpo 7416 1^st c1st 7983 2^nd c2nd 7984 tpos ctpos 8222 Basecbs 17165 Hom chom 17229 compcco 17230 Catccat 17629 Idccid 17630 Hom_f chomf 17631 oppCatcoppc 17676 Func cfunc 17825 ∘_func ccofu 17827 Nat cnat 17916 FuncCat cfuc 17917 SetCatcsetc 18049 ×_c cxpc 18144 1^st_F c1stf 18145 2^nd_F c2ndf 18146 ⟨,⟩_F cprf 18147 eval_F cevlf 18186 Hom_Fchof 18225 Yoncyon 18226

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2164 ax-ext 2698 ax-rep 5279 ax-sep 5293 ax-nul 5300 ax-pow 5359 ax-pr 5423 ax-un 7732 ax-cnex 11180 ax-resscn 11181 ax-1cn 11182 ax-icn 11183 ax-addcl 11184 ax-addrcl 11185 ax-mulcl 11186 ax-mulrcl 11187 ax-mulcom 11188 ax-addass 11189 ax-mulass 11190 ax-distr 11191 ax-i2m1 11192 ax-1ne0 11193 ax-1rid 11194 ax-rnegex 11195 ax-rrecex 11196 ax-cnre 11197 ax-pre-lttri 11198 ax-pre-lttrn 11199 ax-pre-ltadd 11200 ax-pre-mulgt0 11201

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2705 df-cleq 2719 df-clel 2805 df-nfc 2880 df-ne 2936 df-nel 3042 df-ral 3057 df-rex 3066 df-rmo 3371 df-reu 3372 df-rab 3428 df-v 3471 df-sbc 3775 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3963 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-tp 4629 df-op 4631 df-uni 4904 df-iun 4993 df-br 5143 df-opab 5205 df-mpt 5226 df-tr 5260 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7370 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7863 df-1st 7985 df-2nd 7986 df-tpos 8223 df-frecs 8278 df-wrecs 8309 df-recs 8383 df-rdg 8422 df-1o 8478 df-er 8716 df-map 8836 df-pm 8837 df-ixp 8906 df-en 8954 df-dom 8955 df-sdom 8956 df-fin 8957 df-pnf 11266 df-mnf 11267 df-xr 11268 df-ltxr 11269 df-le 11270 df-sub 11462 df-neg 11463 df-nn 12229 df-2 12291 df-3 12292 df-4 12293 df-5 12294 df-6 12295 df-7 12296 df-8 12297 df-9 12298 df-n0 12489 df-z 12575 df-dec 12694 df-uz 12839 df-fz 13503 df-struct 17101 df-sets 17118 df-slot 17136 df-ndx 17148 df-base 17166 df-ress 17195 df-hom 17242 df-cco 17243 df-cat 17633 df-cid 17634 df-homf 17635 df-comf 17636 df-oppc 17677 df-ssc 17778 df-resc 17779 df-subc 17780 df-func 17829 df-cofu 17831 df-nat 17918 df-fuc 17919 df-setc 18050 df-xpc 18148 df-1stf 18149 df-2ndf 18150 df-prf 18151 df-evlf 18190 df-curf 18191 df-hof 18227 df-yon 18228

This theorem is referenced by: yonedalem3 18257

W3C validator