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 18371

Description: Lemma for yoneda 18375. (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 7424	. . . . . . . 8 ⊢ (𝑏 = 𝑎 → (𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏) = (𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎))
2	1	oveq1d 7431	. . . . . . 7 ⊢ (𝑏 = 𝑎 → ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)) = ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)))
3	2	fveq1d 6884	. . . . . 6 ⊢ (𝑏 = 𝑎 → (((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃) = (((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃))
4	3	fveq1d 6884	. . . . 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 5213	. . . 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 2762	. . . . . . . . 9 ⊢ (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆)
8		yoneda.o	. . . . . . . . . 10 ⊢ 𝑂 = (oppCat‘𝐶)
9		yoneda.b	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝐶)
10	8, 9	oppcbas 17810	. . . . . . . . 9 ⊢ 𝐵 = (Base‘𝑂)
11		eqid 2762	. . . . . . . . 9 ⊢ (comp‘𝑆) = (comp‘𝑆)
12		eqid 2762	. . . . . . . . 9 ⊢ (comp‘𝑄) = (comp‘𝑄)
13		eqid 2762	. . . . . . . . . . . 12 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
14	6, 7	fuchom 18057	. . . . . . . . . . . 12 ⊢ (𝑂 Nat 𝑆) = (Hom ‘𝑄)
15		relfunc 17955	. . . . . . . . . . . . 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 4143	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 ⊆ 𝑉)
22	19, 21	ssexd 5293	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ∈ V)
23		yoneda.u	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran (Hom_f ‘𝐶) ⊆ 𝑈)
24	16, 17, 8, 18, 6, 22, 23	yoncl 18354	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ∈ (𝐶 Func 𝑄))
25		1st2ndbr 8042	. . . . . . . . . . . . 13 ⊢ ((Rel (𝐶 Func 𝑄) ∧ 𝑌 ∈ (𝐶 Func 𝑄)) → (1^st ‘𝑌)(𝐶 Func 𝑄)(2^nd ‘𝑌))
26	15, 24, 25	sylancr 599	. . . . . . . . . . . 12 ⊢ (𝜑 → (1^st ‘𝑌)(𝐶 Func 𝑄)(2^nd ‘𝑌))
27		yonedalem22.p	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ 𝐵)
28		yonedalem21.x	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
29	9, 13, 14, 26, 27, 28	funcf2 17961	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃(2^nd ‘𝑌)𝑋):(𝑃(Hom ‘𝐶)𝑋)⟶(((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑋)))
30		yonedalem22.k	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋))
31	29, 30	ffvelcdmd 7081	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑃(2^nd ‘𝑌)𝑋)‘𝐾) ∈ (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑋)))
32	31	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑃(2^nd ‘𝑌)𝑋)‘𝐾) ∈ (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑋)))
33		simpr 490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹))
34		yonedalem22.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺))
35	34	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺))
36	6, 7, 12, 33, 35	fuccocl 18060	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎) ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐺))
37	27	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑃 ∈ 𝐵)
38	6, 7, 10, 11, 12, 32, 36, 37	fuccoval 18059	. . . . . . . 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 18059	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)‘𝑃) = ((𝐴‘𝑃)(⟨((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃), ((1^st ‘𝐹)‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))(𝑎‘𝑃)))
40	22	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑈 ∈ V)
41		eqid 2762	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝑆) = (Base‘𝑆)
42		relfunc 17955	. . . . . . . . . . . . . . . 16 ⊢ Rel (𝑂 Func 𝑆)
43	6	fucbas 18056	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑂 Func 𝑆) = (Base‘𝑄)
44	9, 43, 26	funcf1 17959	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1^st ‘𝑌):𝐵⟶(𝑂 Func 𝑆))
45	44, 28	ffvelcdmd 7081	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1^st ‘𝑌)‘𝑋) ∈ (𝑂 Func 𝑆))
46		1st2ndbr 8042	. . . . . . . . . . . . . . . 16 ⊢ ((Rel (𝑂 Func 𝑆) ∧ ((1^st ‘𝑌)‘𝑋) ∈ (𝑂 Func 𝑆)) → (1^st ‘((1^st ‘𝑌)‘𝑋))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑋)))
47	42, 45, 46	sylancr 599	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1^st ‘((1^st ‘𝑌)‘𝑋))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑋)))
48	10, 41, 47	funcf1 17959	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1^st ‘((1^st ‘𝑌)‘𝑋)):𝐵⟶(Base‘𝑆))
49	18, 22	setcbas 18171	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 = (Base‘𝑆))
50	49	feq3d 6691	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑋)):𝐵⟶𝑈 ↔ (1^st ‘((1^st ‘𝑌)‘𝑋)):𝐵⟶(Base‘𝑆)))
51	48, 50	mpbird 260	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1^st ‘((1^st ‘𝑌)‘𝑋)):𝐵⟶𝑈)
52	51, 27	ffvelcdmd 7081	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃) ∈ 𝑈)
53	52	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃) ∈ 𝑈)
54		yonedalem21.f	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑆))
55		1st2ndbr 8042	. . . . . . . . . . . . . . . 16 ⊢ ((Rel (𝑂 Func 𝑆) ∧ 𝐹 ∈ (𝑂 Func 𝑆)) → (1^st ‘𝐹)(𝑂 Func 𝑆)(2^nd ‘𝐹))
56	42, 54, 55	sylancr 599	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1^st ‘𝐹)(𝑂 Func 𝑆)(2^nd ‘𝐹))
57	10, 41, 56	funcf1 17959	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1^st ‘𝐹):𝐵⟶(Base‘𝑆))
58	49	feq3d 6691	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘𝐹):𝐵⟶𝑈 ↔ (1^st ‘𝐹):𝐵⟶(Base‘𝑆)))
59	57, 58	mpbird 260	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1^st ‘𝐹):𝐵⟶𝑈)
60	59, 27	ffvelcdmd 7081	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1^st ‘𝐹)‘𝑃) ∈ 𝑈)
61	60	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘𝐹)‘𝑃) ∈ 𝑈)
62		yonedalem22.g	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐺 ∈ (𝑂 Func 𝑆))
63		1st2ndbr 8042	. . . . . . . . . . . . . . . 16 ⊢ ((Rel (𝑂 Func 𝑆) ∧ 𝐺 ∈ (𝑂 Func 𝑆)) → (1^st ‘𝐺)(𝑂 Func 𝑆)(2^nd ‘𝐺))
64	42, 62, 63	sylancr 599	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1^st ‘𝐺)(𝑂 Func 𝑆)(2^nd ‘𝐺))
65	10, 41, 64	funcf1 17959	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1^st ‘𝐺):𝐵⟶(Base‘𝑆))
66	65, 27	ffvelcdmd 7081	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1^st ‘𝐺)‘𝑃) ∈ (Base‘𝑆))
67	66, 49	eleqtrrd 2865	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1^st ‘𝐺)‘𝑃) ∈ 𝑈)
68	67	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘𝐺)‘𝑃) ∈ 𝑈)
69	7, 33	nat1st2nd 18047	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑎 ∈ (⟨(1^st ‘((1^st ‘𝑌)‘𝑋)), (2^nd ‘((1^st ‘𝑌)‘𝑋))⟩(𝑂 Nat 𝑆)⟨(1^st ‘𝐹), (2^nd ‘𝐹)⟩))
70		eqid 2762	. . . . . . . . . . . . 13 ⊢ (Hom ‘𝑆) = (Hom ‘𝑆)
71	7, 69, 10, 70, 37	natcl 18049	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝑎‘𝑃) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑃)))
72	18, 40, 70, 53, 61	elsetchom 18174	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑃) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑃)) ↔ (𝑎‘𝑃):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟶((1^st ‘𝐹)‘𝑃)))
73	71, 72	mpbid 235	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝑎‘𝑃):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟶((1^st ‘𝐹)‘𝑃))
74	7, 34	nat1st2nd 18047	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ (⟨(1^st ‘𝐹), (2^nd ‘𝐹)⟩(𝑂 Nat 𝑆)⟨(1^st ‘𝐺), (2^nd ‘𝐺)⟩))
75	7, 74, 10, 70, 27	natcl 18049	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴‘𝑃) ∈ (((1^st ‘𝐹)‘𝑃)(Hom ‘𝑆)((1^st ‘𝐺)‘𝑃)))
76	18, 22, 70, 60, 67	elsetchom 18174	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴‘𝑃) ∈ (((1^st ‘𝐹)‘𝑃)(Hom ‘𝑆)((1^st ‘𝐺)‘𝑃)) ↔ (𝐴‘𝑃):((1^st ‘𝐹)‘𝑃)⟶((1^st ‘𝐺)‘𝑃)))
77	75, 76	mpbid 235	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴‘𝑃):((1^st ‘𝐹)‘𝑃)⟶((1^st ‘𝐺)‘𝑃))
78	77	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝐴‘𝑃):((1^st ‘𝐹)‘𝑃)⟶((1^st ‘𝐺)‘𝑃))
79	18, 40, 11, 53, 61, 68, 73, 78	setcco 18176	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴‘𝑃)(⟨((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃), ((1^st ‘𝐹)‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))(𝑎‘𝑃)) = ((𝐴‘𝑃) ∘ (𝑎‘𝑃)))
80	39, 79	eqtrd 2797	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)‘𝑃) = ((𝐴‘𝑃) ∘ (𝑎‘𝑃)))
81	80	oveq1d 7431	. . . . . . . 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 7081	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘𝑌)‘𝑃) ∈ (𝑂 Func 𝑆))
83		1st2ndbr 8042	. . . . . . . . . . . . . 14 ⊢ ((Rel (𝑂 Func 𝑆) ∧ ((1^st ‘𝑌)‘𝑃) ∈ (𝑂 Func 𝑆)) → (1^st ‘((1^st ‘𝑌)‘𝑃))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑃)))
84	42, 82, 83	sylancr 599	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1^st ‘((1^st ‘𝑌)‘𝑃))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑃)))
85	10, 41, 84	funcf1 17959	. . . . . . . . . . . 12 ⊢ (𝜑 → (1^st ‘((1^st ‘𝑌)‘𝑃)):𝐵⟶(Base‘𝑆))
86	85, 27	ffvelcdmd 7081	. . . . . . . . . . 11 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃) ∈ (Base‘𝑆))
87	86, 49	eleqtrrd 2865	. . . . . . . . . 10 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃) ∈ 𝑈)
88	87	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃) ∈ 𝑈)
89	7, 31	nat1st2nd 18047	. . . . . . . . . . . 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 18049	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃)(Hom ‘𝑆)((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)))
91	18, 22, 70, 87, 52	elsetchom 18174	. . . . . . . . . . 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 235	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃):((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃)⟶((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃))
93	92	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃):((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃)⟶((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃))
94		fco 6731	. . . . . . . . . 10 ⊢ (((𝐴‘𝑃):((1^st ‘𝐹)‘𝑃)⟶((1^st ‘𝐺)‘𝑃) ∧ (𝑎‘𝑃):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟶((1^st ‘𝐹)‘𝑃)) → ((𝐴‘𝑃) ∘ (𝑎‘𝑃)):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟶((1^st ‘𝐺)‘𝑃))
95	78, 73, 94	syl2anc 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴‘𝑃) ∘ (𝑎‘𝑃)):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟶((1^st ‘𝐺)‘𝑃))
96	18, 40, 11, 88, 53, 68, 93, 95	setcco 18176	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴‘𝑃) ∘ (𝑎‘𝑃))(⟨((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃), ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))(((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)) = (((𝐴‘𝑃) ∘ (𝑎‘𝑃)) ∘ (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)))
97	38, 81, 96	3eqtrd 2801	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃) = (((𝐴‘𝑃) ∘ (𝑎‘𝑃)) ∘ (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)))
98	97	fveq1d 6884	. . . . . 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 17774	. . . . . . . . 9 ⊢ (𝜑 → ( 1 ‘𝑃) ∈ (𝑃(Hom ‘𝐶)𝑃))
101	16, 9, 17, 27, 13, 27	yon11 18356	. . . . . . . . 9 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃) = (𝑃(Hom ‘𝐶)𝑃))
102	100, 101	eleqtrrd 2865	. . . . . . . 8 ⊢ (𝜑 → ( 1 ‘𝑃) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃))
103	102	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1 ‘𝑃) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃))
104		fvco3 6982	. . . . . . 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 596	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝐴‘𝑃) ∘ (𝑎‘𝑃)) ∘ (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃))‘( 1 ‘𝑃)) = (((𝐴‘𝑃) ∘ (𝑎‘𝑃))‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))))
106	93, 103	ffvelcdmd 7081	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃))
107		fvco3 6982	. . . . . . . 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 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴‘𝑃) ∘ (𝑎‘𝑃))‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))) = ((𝐴‘𝑃)‘((𝑎‘𝑃)‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)))))
109	17	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐶 ∈ Cat)
110	28	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑋 ∈ 𝐵)
111		eqid 2762	. . . . . . . . . . . 12 ⊢ (comp‘𝐶) = (comp‘𝐶)
112	30	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋))
113	100	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1 ‘𝑃) ∈ (𝑃(Hom ‘𝐶)𝑃))
114	16, 9, 109, 37, 13, 110, 111, 37, 112, 113	yon2 18358	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)) = (𝐾(⟨𝑃, 𝑃⟩(comp‘𝐶)𝑋)( 1 ‘𝑃)))
115	9, 13, 99, 109, 37, 111, 110, 112	catrid 17776	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝐾(⟨𝑃, 𝑃⟩(comp‘𝐶)𝑋)( 1 ‘𝑃)) = 𝐾)
116	114, 115	eqtrd 2797	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)) = 𝐾)
117	116	fveq2d 6886	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑃)‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))) = ((𝑎‘𝑃)‘𝐾))
118		eqid 2762	. . . . . . . . . . . . . . 15 ⊢ (Hom ‘𝑂) = (Hom ‘𝑂)
119	10, 118, 70, 47, 28, 27	funcf2 17961	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃):(𝑋(Hom ‘𝑂)𝑃)⟶(((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)))
120	13, 8	oppchom 17807	. . . . . . . . . . . . . . 15 ⊢ (𝑋(Hom ‘𝑂)𝑃) = (𝑃(Hom ‘𝐶)𝑋)
121	30, 120	eleqtrrdi 2873	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ (𝑋(Hom ‘𝑂)𝑃))
122	119, 121	ffvelcdmd 7081	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)))
123	51, 28	ffvelcdmd 7081	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋) ∈ 𝑈)
124	18, 22, 70, 123, 52	elsetchom 18174	. . . . . . . . . . . . 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 235	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)⟶((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃))
126	125	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)⟶((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃))
127	9, 13, 99, 17, 28	catidcl 17774	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( 1 ‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋))
128	16, 9, 17, 28, 13, 28	yon11 18356	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋) = (𝑋(Hom ‘𝐶)𝑋))
129	127, 128	eleqtrrd 2865	. . . . . . . . . . . 12 ⊢ (𝜑 → ( 1 ‘𝑋) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋))
130	129	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1 ‘𝑋) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋))
131		fvco3 6982	. . . . . . . . . . 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 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑎‘𝑃) ∘ ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾))‘( 1 ‘𝑋)) = ((𝑎‘𝑃)‘(((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)‘( 1 ‘𝑋))))
133	121	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐾 ∈ (𝑋(Hom ‘𝑂)𝑃))
134	7, 69, 10, 118, 11, 110, 37, 133	nati 18051	. . . . . . . . . . . 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 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋) ∈ 𝑈)
136	18, 40, 11, 135, 53, 61, 126, 73	setcco 18176	. . . . . . . . . . . 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 7081	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘𝐹)‘𝑋) ∈ 𝑈)
138	137	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘𝐹)‘𝑋) ∈ 𝑈)
139	7, 69, 10, 70, 110	natcl 18049	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝑎‘𝑋) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑋)))
140	18, 40, 70, 135, 138	elsetchom 18174	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑋) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑋)) ↔ (𝑎‘𝑋):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)⟶((1^st ‘𝐹)‘𝑋)))
141	139, 140	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝑎‘𝑋):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)⟶((1^st ‘𝐹)‘𝑋))
142	10, 118, 70, 56, 28, 27	funcf2 17961	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋(2^nd ‘𝐹)𝑃):(𝑋(Hom ‘𝑂)𝑃)⟶(((1^st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑃)))
143	142, 121	ffvelcdmd 7081	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∈ (((1^st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑃)))
144	18, 22, 70, 137, 60	elsetchom 18174	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∈ (((1^st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑃)) ↔ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾):((1^st ‘𝐹)‘𝑋)⟶((1^st ‘𝐹)‘𝑃)))
145	143, 144	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾):((1^st ‘𝐹)‘𝑋)⟶((1^st ‘𝐹)‘𝑃))
146	145	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾):((1^st ‘𝐹)‘𝑋)⟶((1^st ‘𝐹)‘𝑃))
147	18, 40, 11, 135, 138, 61, 141, 146	setcco 18176	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)(⟨((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋), ((1^st ‘𝐹)‘𝑋)⟩(comp‘𝑆)((1^st ‘𝐹)‘𝑃))(𝑎‘𝑋)) = (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋)))
148	134, 136, 147	3eqtr3d 2805	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑃) ∘ ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)) = (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋)))
149	148	fveq1d 6884	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑎‘𝑃) ∘ ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾))‘( 1 ‘𝑋)) = ((((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋))‘( 1 ‘𝑋)))
150	127	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1 ‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋))
151	16, 9, 109, 110, 13, 110, 111, 37, 112, 150	yon12 18357	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)‘( 1 ‘𝑋)) = (( 1 ‘𝑋)(⟨𝑃, 𝑋⟩(comp‘𝐶)𝑋)𝐾))
152	9, 13, 99, 109, 37, 111, 110, 112	catlid 17775	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (( 1 ‘𝑋)(⟨𝑃, 𝑋⟩(comp‘𝐶)𝑋)𝐾) = 𝐾)
153	151, 152	eqtrd 2797	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)‘( 1 ‘𝑋)) = 𝐾)
154	153	fveq2d 6886	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑃)‘(((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)‘( 1 ‘𝑋))) = ((𝑎‘𝑃)‘𝐾))
155	132, 149, 154	3eqtr3d 2805	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋))‘( 1 ‘𝑋)) = ((𝑎‘𝑃)‘𝐾))
156		fvco3 6982	. . . . . . . . . 10 ⊢ (((𝑎‘𝑋):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)⟶((1^st ‘𝐹)‘𝑋) ∧ ( 1 ‘𝑋) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)) → ((((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋))‘( 1 ‘𝑋)) = (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))
157	141, 130, 156	syl2anc 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋))‘( 1 ‘𝑋)) = (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))
158	117, 155, 157	3eqtr2d 2803	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑃)‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))) = (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))
159	158	fveq2d 6886	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴‘𝑃)‘((𝑎‘𝑃)‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)))) = ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋)))))
160	108, 159	eqtrd 2797	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴‘𝑃) ∘ (𝑎‘𝑃))‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))) = ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋)))))
161	98, 105, 160	3eqtrd 2801	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃)‘( 1 ‘𝑃)) = ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋)))))
162	161	mpteq2dva 5202	. . . 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 2809	. . 3 ⊢ (𝜑 → (𝑏 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃)‘( 1 ‘𝑃))) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))))
164		eqid 2762	. . . . . . . . . . 11 ⊢ (𝑄 ×_c 𝑂) = (𝑄 ×_c 𝑂)
165	164, 43, 10	xpcbas 18270	. . . . . . . . . 10 ⊢ ((𝑂 Func 𝑆) × 𝐵) = (Base‘(𝑄 ×_c 𝑂))
166		eqid 2762	. . . . . . . . . 10 ⊢ (Hom ‘(𝑄 ×_c 𝑂)) = (Hom ‘(𝑄 ×_c 𝑂))
167		eqid 2762	. . . . . . . . . 10 ⊢ (Hom ‘𝑇) = (Hom ‘𝑇)
168		relfunc 17955	. . . . . . . . . . 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 18364	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑍 ∈ ((𝑄 ×_c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×_c 𝑂) Func 𝑇)))
175	174	simpld 500	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑍 ∈ ((𝑄 ×_c 𝑂) Func 𝑇))
176		1st2ndbr 8042	. . . . . . . . . . 11 ⊢ ((Rel ((𝑄 ×_c 𝑂) Func 𝑇) ∧ 𝑍 ∈ ((𝑄 ×_c 𝑂) Func 𝑇)) → (1^st ‘𝑍)((𝑄 ×_c 𝑂) Func 𝑇)(2^nd ‘𝑍))
177	168, 175, 176	sylancr 599	. . . . . . . . . 10 ⊢ (𝜑 → (1^st ‘𝑍)((𝑄 ×_c 𝑂) Func 𝑇)(2^nd ‘𝑍))
178	54, 28	opelxpd 5698	. . . . . . . . . 10 ⊢ (𝜑 → ⟨𝐹, 𝑋⟩ ∈ ((𝑂 Func 𝑆) × 𝐵))
179	62, 27	opelxpd 5698	. . . . . . . . . 10 ⊢ (𝜑 → ⟨𝐺, 𝑃⟩ ∈ ((𝑂 Func 𝑆) × 𝐵))
180	165, 166, 167, 177, 178, 179	funcf2 17961	. . . . . . . . 9 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩):(⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×_c 𝑂))⟨𝐺, 𝑃⟩)⟶(((1^st ‘𝑍)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝑍)‘⟨𝐺, 𝑃⟩)))
181	164, 43, 10, 14, 118, 54, 28, 62, 27, 166	xpchom2 18278	. . . . . . . . . . 11 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×_c 𝑂))⟨𝐺, 𝑃⟩) = ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑋(Hom ‘𝑂)𝑃)))
182	120	xpeq2i 5686	. . . . . . . . . . 11 ⊢ ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑋(Hom ‘𝑂)𝑃)) = ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))
183	181, 182	eqtrdi 2813	. . . . . . . . . 10 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×_c 𝑂))⟨𝐺, 𝑃⟩) = ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋)))
184		df-ov 7419	. . . . . . . . . . . . 13 ⊢ (𝐹(1^st ‘𝑍)𝑋) = ((1^st ‘𝑍)‘⟨𝐹, 𝑋⟩)
185		df-ov 7419	. . . . . . . . . . . . 13 ⊢ (𝐺(1^st ‘𝑍)𝑃) = ((1^st ‘𝑍)‘⟨𝐺, 𝑃⟩)
186	184, 185	oveq12i 7428	. . . . . . . . . . . 12 ⊢ ((𝐹(1^st ‘𝑍)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝑍)𝑃)) = (((1^st ‘𝑍)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝑍)‘⟨𝐺, 𝑃⟩))
187	186	eqcomi 2771	. . . . . . . . . . 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 6701	. . . . . . . . 9 ⊢ (𝜑 → ((⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩):(⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×_c 𝑂))⟨𝐺, 𝑃⟩)⟶(((1^st ‘𝑍)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝑍)‘⟨𝐺, 𝑃⟩)) ↔ (⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩):((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))⟶((𝐹(1^st ‘𝑍)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝑍)𝑃))))
190	180, 189	mpbid 235	. . . . . . . 8 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩):((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))⟶((𝐹(1^st ‘𝑍)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝑍)𝑃)))
191	190, 34, 30	fovcdmd 7589	. . . . . . 7 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾) ∈ ((𝐹(1^st ‘𝑍)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝑍)𝑃)))
192		eqid 2762	. . . . . . . . . . 11 ⊢ (Base‘𝑇) = (Base‘𝑇)
193	165, 192, 177	funcf1 17959	. . . . . . . . . 10 ⊢ (𝜑 → (1^st ‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
194	193, 54, 28	fovcdmd 7589	. . . . . . . . 9 ⊢ (𝜑 → (𝐹(1^st ‘𝑍)𝑋) ∈ (Base‘𝑇))
195	169, 19	setcbas 18171	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 = (Base‘𝑇))
196	194, 195	eleqtrrd 2865	. . . . . . . 8 ⊢ (𝜑 → (𝐹(1^st ‘𝑍)𝑋) ∈ 𝑉)
197	193, 62, 27	fovcdmd 7589	. . . . . . . . 9 ⊢ (𝜑 → (𝐺(1^st ‘𝑍)𝑃) ∈ (Base‘𝑇))
198	197, 195	eleqtrrd 2865	. . . . . . . 8 ⊢ (𝜑 → (𝐺(1^st ‘𝑍)𝑃) ∈ 𝑉)
199	169, 19, 167, 196, 198	elsetchom 18174	. . . . . . 7 ⊢ (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾) ∈ ((𝐹(1^st ‘𝑍)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝑍)𝑃)) ↔ (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾):(𝐹(1^st ‘𝑍)𝑋)⟶(𝐺(1^st ‘𝑍)𝑃)))
200	191, 199	mpbid 235	. . . . . 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 18370	. . . . . . . 8 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾) = (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(2^nd ‘𝐻)⟨((1^st ‘𝑌)‘𝑃), 𝐺⟩)𝐴))
202	8	oppccat 17814	. . . . . . . . . . 11 ⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat)
203	17, 202	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑂 ∈ Cat)
204	18	setccat 18178	. . . . . . . . . . 11 ⊢ (𝑈 ∈ V → 𝑆 ∈ Cat)
205	22, 204	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ Cat)
206	6, 203, 205	fuccat 18066	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ Cat)
207	170, 206, 43, 14, 45, 54, 82, 62, 12, 31, 34	hof2val 18348	. . . . . . . 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 2797	. . . . . . 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 18365	. . . . . . 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 18365	. . . . . . 7 ⊢ (𝜑 → (𝐺(1^st ‘𝑍)𝑃) = (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺))
211	208, 209, 210	feq123d 6695	. . . . . 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 235	. . . . 5 ⊢ (𝜑 → (𝑏 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))):(((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)⟶(((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺))
213		eqid 2762	. . . . . 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 237	. . . 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 18366	. . . . 5 ⊢ (𝜑 → ((𝐺𝑀𝑃) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺) ↦ ((𝑎‘𝑃)‘( 1 ‘𝑃))) ∧ (𝐺𝑀𝑃):(𝐺(1^st ‘𝑍)𝑃)⟶(𝐺(1^st ‘𝐸)𝑃)))
218	217	simpld 500	. . . 4 ⊢ (𝜑 → (𝐺𝑀𝑃) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺) ↦ ((𝑎‘𝑃)‘( 1 ‘𝑃))))
219		fveq1 6881	. . . . 5 ⊢ (𝑎 = ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)) → (𝑎‘𝑃) = (((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃))
220	219	fveq1d 6884	. . . 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 7127	. . 3 ⊢ (𝜑 → ((𝐺𝑀𝑃) ∘ (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾)) = (𝑏 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃)‘( 1 ‘𝑃))))
222		eqid 2762	. . . . . . 7 ⊢ (⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩) = (⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)
223	172, 203, 205, 10, 118, 11, 7, 54, 62, 28, 27, 222, 34, 121	evlf2val 18311	. . . . . 6 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) = ((𝐴‘𝑃)(⟨((1^st ‘𝐹)‘𝑋), ((1^st ‘𝐹)‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)))
224	18, 22, 11, 137, 60, 67, 145, 77	setcco 18176	. . . . . 6 ⊢ (𝜑 → ((𝐴‘𝑃)(⟨((1^st ‘𝐹)‘𝑋), ((1^st ‘𝐹)‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)) = ((𝐴‘𝑃) ∘ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)))
225	223, 224	eqtrd 2797	. . . . 5 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) = ((𝐴‘𝑃) ∘ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)))
226	225	coeq1d 5845	. . . 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 18366	. . . . . . . 8 ⊢ (𝜑 → ((𝐹𝑀𝑋) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋))) ∧ (𝐹𝑀𝑋):(𝐹(1^st ‘𝑍)𝑋)⟶(𝐹(1^st ‘𝐸)𝑋)))
228	227	simprd 501	. . . . . . 7 ⊢ (𝜑 → (𝐹𝑀𝑋):(𝐹(1^st ‘𝑍)𝑋)⟶(𝐹(1^st ‘𝐸)𝑋))
229	227	simpld 500	. . . . . . . 8 ⊢ (𝜑 → (𝐹𝑀𝑋) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋))))
230	172, 203, 205, 10, 54, 28	evlf1 18312	. . . . . . . 8 ⊢ (𝜑 → (𝐹(1^st ‘𝐸)𝑋) = ((1^st ‘𝐹)‘𝑋))
231	229, 209, 230	feq123d 6695	. . . . . . 7 ⊢ (𝜑 → ((𝐹𝑀𝑋):(𝐹(1^st ‘𝑍)𝑋)⟶(𝐹(1^st ‘𝐸)𝑋) ↔ (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋))):(((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)⟶((1^st ‘𝐹)‘𝑋)))
232	228, 231	mpbid 235	. . . . . 6 ⊢ (𝜑 → (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋))):(((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)⟶((1^st ‘𝐹)‘𝑋))
233		eqid 2762	. . . . . . 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 237	. . . . 5 ⊢ (𝜑 → ∀𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)((𝑎‘𝑋)‘( 1 ‘𝑋)) ∈ ((1^st ‘𝐹)‘𝑋))
236		fcompt 7130	. . . . . 6 ⊢ (((𝐴‘𝑃):((1^st ‘𝐹)‘𝑃)⟶((1^st ‘𝐺)‘𝑃) ∧ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾):((1^st ‘𝐹)‘𝑋)⟶((1^st ‘𝐹)‘𝑃)) → ((𝐴‘𝑃) ∘ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)) = (𝑦 ∈ ((1^st ‘𝐹)‘𝑋) ↦ ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘𝑦))))
237	77, 145, 236	syl2anc 596	. . . . 5 ⊢ (𝜑 → ((𝐴‘𝑃) ∘ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)) = (𝑦 ∈ ((1^st ‘𝐹)‘𝑋) ↦ ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘𝑦))))
238		2fveq3 6887	. . . . 5 ⊢ (𝑦 = ((𝑎‘𝑋)‘( 1 ‘𝑋)) → ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘𝑦)) = ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋)))))
239	235, 229, 237, 238	fmptcof 7127	. . . 4 ⊢ (𝜑 → (((𝐴‘𝑃) ∘ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)) ∘ (𝐹𝑀𝑋)) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))))
240	226, 239	eqtrd 2797	. . 3 ⊢ (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) ∘ (𝐹𝑀𝑋)) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))))
241	163, 221, 240	3eqtr4d 2807	. 2 ⊢ (𝜑 → ((𝐺𝑀𝑃) ∘ (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾)) = ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) ∘ (𝐹𝑀𝑋)))
242		eqid 2762	. . 3 ⊢ (comp‘𝑇) = (comp‘𝑇)
243	174	simprd 501	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ ((𝑄 ×_c 𝑂) Func 𝑇))
244		1st2ndbr 8042	. . . . . . 7 ⊢ ((Rel ((𝑄 ×_c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×_c 𝑂) Func 𝑇)) → (1^st ‘𝐸)((𝑄 ×_c 𝑂) Func 𝑇)(2^nd ‘𝐸))
245	168, 243, 244	sylancr 599	. . . . . 6 ⊢ (𝜑 → (1^st ‘𝐸)((𝑄 ×_c 𝑂) Func 𝑇)(2^nd ‘𝐸))
246	165, 192, 245	funcf1 17959	. . . . 5 ⊢ (𝜑 → (1^st ‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
247	246, 62, 27	fovcdmd 7589	. . . 4 ⊢ (𝜑 → (𝐺(1^st ‘𝐸)𝑃) ∈ (Base‘𝑇))
248	247, 195	eleqtrrd 2865	. . 3 ⊢ (𝜑 → (𝐺(1^st ‘𝐸)𝑃) ∈ 𝑉)
249	217	simprd 501	. . 3 ⊢ (𝜑 → (𝐺𝑀𝑃):(𝐺(1^st ‘𝑍)𝑃)⟶(𝐺(1^st ‘𝐸)𝑃))
250	169, 19, 242, 196, 198, 248, 200, 249	setcco 18176	. 2 ⊢ (𝜑 → ((𝐺𝑀𝑃)(⟨(𝐹(1^st ‘𝑍)𝑋), (𝐺(1^st ‘𝑍)𝑃)⟩(comp‘𝑇)(𝐺(1^st ‘𝐸)𝑃))(𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾)) = ((𝐺𝑀𝑃) ∘ (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾)))
251	246, 54, 28	fovcdmd 7589	. . . 4 ⊢ (𝜑 → (𝐹(1^st ‘𝐸)𝑋) ∈ (Base‘𝑇))
252	251, 195	eleqtrrd 2865	. . 3 ⊢ (𝜑 → (𝐹(1^st ‘𝐸)𝑋) ∈ 𝑉)
253	165, 166, 167, 245, 178, 179	funcf2 17961	. . . . . 6 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩):(⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×_c 𝑂))⟨𝐺, 𝑃⟩)⟶(((1^st ‘𝐸)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝐸)‘⟨𝐺, 𝑃⟩)))
254		df-ov 7419	. . . . . . . . . 10 ⊢ (𝐹(1^st ‘𝐸)𝑋) = ((1^st ‘𝐸)‘⟨𝐹, 𝑋⟩)
255		df-ov 7419	. . . . . . . . . 10 ⊢ (𝐺(1^st ‘𝐸)𝑃) = ((1^st ‘𝐸)‘⟨𝐺, 𝑃⟩)
256	254, 255	oveq12i 7428	. . . . . . . . 9 ⊢ ((𝐹(1^st ‘𝐸)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝐸)𝑃)) = (((1^st ‘𝐸)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝐸)‘⟨𝐺, 𝑃⟩))
257	256	eqcomi 2771	. . . . . . . 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 6701	. . . . . 6 ⊢ (𝜑 → ((⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩):(⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×_c 𝑂))⟨𝐺, 𝑃⟩)⟶(((1^st ‘𝐸)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝐸)‘⟨𝐺, 𝑃⟩)) ↔ (⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩):((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))⟶((𝐹(1^st ‘𝐸)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝐸)𝑃))))
260	253, 259	mpbid 235	. . . . 5 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩):((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))⟶((𝐹(1^st ‘𝐸)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝐸)𝑃)))
261	260, 34, 30	fovcdmd 7589	. . . 4 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) ∈ ((𝐹(1^st ‘𝐸)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝐸)𝑃)))
262	169, 19, 167, 252, 248	elsetchom 18174	. . . 4 ⊢ (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) ∈ ((𝐹(1^st ‘𝐸)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝐸)𝑃)) ↔ (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾):(𝐹(1^st ‘𝐸)𝑋)⟶(𝐺(1^st ‘𝐸)𝑃)))
263	261, 262	mpbid 235	. . 3 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾):(𝐹(1^st ‘𝐸)𝑋)⟶(𝐺(1^st ‘𝐸)𝑃))
264	169, 19, 242, 196, 252, 248, 228, 263	setcco 18176	. 2 ⊢ (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾)(⟨(𝐹(1^st ‘𝑍)𝑋), (𝐹(1^st ‘𝐸)𝑋)⟩(comp‘𝑇)(𝐺(1^st ‘𝐸)𝑃))(𝐹𝑀𝑋)) = ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) ∘ (𝐹𝑀𝑋)))
265	241, 250, 264	3eqtr4d 2807	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

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ∀wral 3078 Vcvv 3453 ∪ cun 3900 ⊆ wss 3902 ⟨cop 4593 class class class wbr 5107 ↦ cmpt 5190 × cxp 5657 ran crn 5660 ∘ ccom 5663 Rel wrel 5664 ⟶wf 6533 ‘cfv 6537 (class class class)co 7416 ∈ cmpo 7418 1^st c1st 7987 2^nd c2nd 7988 tpos ctpos 8226 Basecbs 17305 Hom chom 17357 compcco 17358 Catccat 17756 Idccid 17757 Hom_f chomf 17758 oppCatcoppc 17803 Func cfunc 17947 ∘_func ccofu 17949 Nat cnat 18037 FuncCat cfuc 18038 SetCatcsetc 18168 ×_c cxpc 18260 1^st_F c1stf 18261 2^nd_F c2ndf 18262 ⟨,⟩_F cprf 18263 eval_F cevlf 18301 Hom_Fchof 18340 Yoncyon 18341

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7866 df-1st 7989 df-2nd 7990 df-tpos 8227 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8458 df-er 8699 df-map 8831 df-pm 8832 df-ixp 8908 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-nn 12261 df-2 12330 df-3 12331 df-4 12332 df-5 12333 df-6 12334 df-7 12335 df-8 12336 df-9 12337 df-n0 12532 df-z 12619 df-dec 12740 df-uz 12891 df-fz 13564 df-struct 17243 df-sets 17260 df-slot 17278 df-ndx 17290 df-base 17306 df-ress 17327 df-hom 17370 df-cco 17371 df-cat 17760 df-cid 17761 df-homf 17762 df-comf 17763 df-oppc 17804 df-ssc 17903 df-resc 17904 df-subc 17905 df-func 17951 df-cofu 17953 df-nat 18039 df-fuc 18040 df-setc 18169 df-xpc 18264 df-1stf 18265 df-2ndf 18266 df-prf 18267 df-evlf 18305 df-curf 18306 df-hof 18342 df-yon 18343

This theorem is used by: yonedalem3 18372

W3C validator