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 18265

Description: Lemma for yoneda 18269. (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 7421	. . . . . . . 8 ⊢ (𝑏 = 𝑎 → (𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏) = (𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎))
2	1	oveq1d 7428	. . . . . . 7 ⊢ (𝑏 = 𝑎 → ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)) = ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)))
3	2	fveq1d 6892	. . . . . 6 ⊢ (𝑏 = 𝑎 → (((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃) = (((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃))
4	3	fveq1d 6892	. . . . 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 5257	. . . 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 2725	. . . . . . . . 9 ⊢ (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆)
8		yoneda.o	. . . . . . . . . 10 ⊢ 𝑂 = (oppCat‘𝐶)
9		yoneda.b	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝐶)
10	8, 9	oppcbas 17693	. . . . . . . . 9 ⊢ 𝐵 = (Base‘𝑂)
11		eqid 2725	. . . . . . . . 9 ⊢ (comp‘𝑆) = (comp‘𝑆)
12		eqid 2725	. . . . . . . . 9 ⊢ (comp‘𝑄) = (comp‘𝑄)
13		eqid 2725	. . . . . . . . . . . 12 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
14	6, 7	fuchom 17946	. . . . . . . . . . . 12 ⊢ (𝑂 Nat 𝑆) = (Hom ‘𝑄)
15		relfunc 17842	. . . . . . . . . . . . 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 4183	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 ⊆ 𝑉)
22	19, 21	ssexd 5320	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ∈ V)
23		yoneda.u	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran (Hom_f ‘𝐶) ⊆ 𝑈)
24	16, 17, 8, 18, 6, 22, 23	yoncl 18248	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ∈ (𝐶 Func 𝑄))
25		1st2ndbr 8040	. . . . . . . . . . . . 13 ⊢ ((Rel (𝐶 Func 𝑄) ∧ 𝑌 ∈ (𝐶 Func 𝑄)) → (1^st ‘𝑌)(𝐶 Func 𝑄)(2^nd ‘𝑌))
26	15, 24, 25	sylancr 585	. . . . . . . . . . . 12 ⊢ (𝜑 → (1^st ‘𝑌)(𝐶 Func 𝑄)(2^nd ‘𝑌))
27		yonedalem22.p	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ 𝐵)
28		yonedalem21.x	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
29	9, 13, 14, 26, 27, 28	funcf2 17848	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃(2^nd ‘𝑌)𝑋):(𝑃(Hom ‘𝐶)𝑋)⟶(((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑋)))
30		yonedalem22.k	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋))
31	29, 30	ffvelcdmd 7088	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑃(2^nd ‘𝑌)𝑋)‘𝐾) ∈ (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑋)))
32	31	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑃(2^nd ‘𝑌)𝑋)‘𝐾) ∈ (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑋)))
33		simpr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹))
34		yonedalem22.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺))
35	34	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺))
36	6, 7, 12, 33, 35	fuccocl 17950	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎) ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐺))
37	27	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑃 ∈ 𝐵)
38	6, 7, 10, 11, 12, 32, 36, 37	fuccoval 17949	. . . . . . . 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 17949	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)‘𝑃) = ((𝐴‘𝑃)(⟨((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃), ((1^st ‘𝐹)‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))(𝑎‘𝑃)))
40	22	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑈 ∈ V)
41		eqid 2725	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝑆) = (Base‘𝑆)
42		relfunc 17842	. . . . . . . . . . . . . . . 16 ⊢ Rel (𝑂 Func 𝑆)
43	6	fucbas 17945	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑂 Func 𝑆) = (Base‘𝑄)
44	9, 43, 26	funcf1 17846	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1^st ‘𝑌):𝐵⟶(𝑂 Func 𝑆))
45	44, 28	ffvelcdmd 7088	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1^st ‘𝑌)‘𝑋) ∈ (𝑂 Func 𝑆))
46		1st2ndbr 8040	. . . . . . . . . . . . . . . 16 ⊢ ((Rel (𝑂 Func 𝑆) ∧ ((1^st ‘𝑌)‘𝑋) ∈ (𝑂 Func 𝑆)) → (1^st ‘((1^st ‘𝑌)‘𝑋))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑋)))
47	42, 45, 46	sylancr 585	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1^st ‘((1^st ‘𝑌)‘𝑋))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑋)))
48	10, 41, 47	funcf1 17846	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1^st ‘((1^st ‘𝑌)‘𝑋)):𝐵⟶(Base‘𝑆))
49	18, 22	setcbas 18061	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 = (Base‘𝑆))
50	49	feq3d 6704	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑋)):𝐵⟶𝑈 ↔ (1^st ‘((1^st ‘𝑌)‘𝑋)):𝐵⟶(Base‘𝑆)))
51	48, 50	mpbird 256	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1^st ‘((1^st ‘𝑌)‘𝑋)):𝐵⟶𝑈)
52	51, 27	ffvelcdmd 7088	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃) ∈ 𝑈)
53	52	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃) ∈ 𝑈)
54		yonedalem21.f	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑆))
55		1st2ndbr 8040	. . . . . . . . . . . . . . . 16 ⊢ ((Rel (𝑂 Func 𝑆) ∧ 𝐹 ∈ (𝑂 Func 𝑆)) → (1^st ‘𝐹)(𝑂 Func 𝑆)(2^nd ‘𝐹))
56	42, 54, 55	sylancr 585	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1^st ‘𝐹)(𝑂 Func 𝑆)(2^nd ‘𝐹))
57	10, 41, 56	funcf1 17846	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1^st ‘𝐹):𝐵⟶(Base‘𝑆))
58	49	feq3d 6704	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘𝐹):𝐵⟶𝑈 ↔ (1^st ‘𝐹):𝐵⟶(Base‘𝑆)))
59	57, 58	mpbird 256	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1^st ‘𝐹):𝐵⟶𝑈)
60	59, 27	ffvelcdmd 7088	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1^st ‘𝐹)‘𝑃) ∈ 𝑈)
61	60	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘𝐹)‘𝑃) ∈ 𝑈)
62		yonedalem22.g	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐺 ∈ (𝑂 Func 𝑆))
63		1st2ndbr 8040	. . . . . . . . . . . . . . . 16 ⊢ ((Rel (𝑂 Func 𝑆) ∧ 𝐺 ∈ (𝑂 Func 𝑆)) → (1^st ‘𝐺)(𝑂 Func 𝑆)(2^nd ‘𝐺))
64	42, 62, 63	sylancr 585	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1^st ‘𝐺)(𝑂 Func 𝑆)(2^nd ‘𝐺))
65	10, 41, 64	funcf1 17846	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1^st ‘𝐺):𝐵⟶(Base‘𝑆))
66	65, 27	ffvelcdmd 7088	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1^st ‘𝐺)‘𝑃) ∈ (Base‘𝑆))
67	66, 49	eleqtrrd 2828	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1^st ‘𝐺)‘𝑃) ∈ 𝑈)
68	67	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘𝐺)‘𝑃) ∈ 𝑈)
69	7, 33	nat1st2nd 17935	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑎 ∈ (⟨(1^st ‘((1^st ‘𝑌)‘𝑋)), (2^nd ‘((1^st ‘𝑌)‘𝑋))⟩(𝑂 Nat 𝑆)⟨(1^st ‘𝐹), (2^nd ‘𝐹)⟩))
70		eqid 2725	. . . . . . . . . . . . 13 ⊢ (Hom ‘𝑆) = (Hom ‘𝑆)
71	7, 69, 10, 70, 37	natcl 17937	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝑎‘𝑃) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑃)))
72	18, 40, 70, 53, 61	elsetchom 18064	. . . . . . . . . . . 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 17935	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ (⟨(1^st ‘𝐹), (2^nd ‘𝐹)⟩(𝑂 Nat 𝑆)⟨(1^st ‘𝐺), (2^nd ‘𝐺)⟩))
75	7, 74, 10, 70, 27	natcl 17937	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴‘𝑃) ∈ (((1^st ‘𝐹)‘𝑃)(Hom ‘𝑆)((1^st ‘𝐺)‘𝑃)))
76	18, 22, 70, 60, 67	elsetchom 18064	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴‘𝑃) ∈ (((1^st ‘𝐹)‘𝑃)(Hom ‘𝑆)((1^st ‘𝐺)‘𝑃)) ↔ (𝐴‘𝑃):((1^st ‘𝐹)‘𝑃)⟶((1^st ‘𝐺)‘𝑃)))
77	75, 76	mpbid 231	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴‘𝑃):((1^st ‘𝐹)‘𝑃)⟶((1^st ‘𝐺)‘𝑃))
78	77	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝐴‘𝑃):((1^st ‘𝐹)‘𝑃)⟶((1^st ‘𝐺)‘𝑃))
79	18, 40, 11, 53, 61, 68, 73, 78	setcco 18066	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴‘𝑃)(⟨((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃), ((1^st ‘𝐹)‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))(𝑎‘𝑃)) = ((𝐴‘𝑃) ∘ (𝑎‘𝑃)))
80	39, 79	eqtrd 2765	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)‘𝑃) = ((𝐴‘𝑃) ∘ (𝑎‘𝑃)))
81	80	oveq1d 7428	. . . . . . . 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 7088	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘𝑌)‘𝑃) ∈ (𝑂 Func 𝑆))
83		1st2ndbr 8040	. . . . . . . . . . . . . 14 ⊢ ((Rel (𝑂 Func 𝑆) ∧ ((1^st ‘𝑌)‘𝑃) ∈ (𝑂 Func 𝑆)) → (1^st ‘((1^st ‘𝑌)‘𝑃))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑃)))
84	42, 82, 83	sylancr 585	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1^st ‘((1^st ‘𝑌)‘𝑃))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑃)))
85	10, 41, 84	funcf1 17846	. . . . . . . . . . . 12 ⊢ (𝜑 → (1^st ‘((1^st ‘𝑌)‘𝑃)):𝐵⟶(Base‘𝑆))
86	85, 27	ffvelcdmd 7088	. . . . . . . . . . 11 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃) ∈ (Base‘𝑆))
87	86, 49	eleqtrrd 2828	. . . . . . . . . 10 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃) ∈ 𝑈)
88	87	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃) ∈ 𝑈)
89	7, 31	nat1st2nd 17935	. . . . . . . . . . . 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 17937	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃)(Hom ‘𝑆)((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)))
91	18, 22, 70, 87, 52	elsetchom 18064	. . . . . . . . . . 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 479	. . . . . . . . 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 582	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴‘𝑃) ∘ (𝑎‘𝑃)):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟶((1^st ‘𝐺)‘𝑃))
96	18, 40, 11, 88, 53, 68, 93, 95	setcco 18066	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴‘𝑃) ∘ (𝑎‘𝑃))(⟨((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃), ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))(((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)) = (((𝐴‘𝑃) ∘ (𝑎‘𝑃)) ∘ (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)))
97	38, 81, 96	3eqtrd 2769	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃) = (((𝐴‘𝑃) ∘ (𝑎‘𝑃)) ∘ (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)))
98	97	fveq1d 6892	. . . . . 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 17656	. . . . . . . . 9 ⊢ (𝜑 → ( 1 ‘𝑃) ∈ (𝑃(Hom ‘𝐶)𝑃))
101	16, 9, 17, 27, 13, 27	yon11 18250	. . . . . . . . 9 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃) = (𝑃(Hom ‘𝐶)𝑃))
102	100, 101	eleqtrrd 2828	. . . . . . . 8 ⊢ (𝜑 → ( 1 ‘𝑃) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃))
103	102	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1 ‘𝑃) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃))
104		fvco3 6990	. . . . . . 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 582	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝐴‘𝑃) ∘ (𝑎‘𝑃)) ∘ (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃))‘( 1 ‘𝑃)) = (((𝐴‘𝑃) ∘ (𝑎‘𝑃))‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))))
106	93, 103	ffvelcdmd 7088	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃))
107		fvco3 6990	. . . . . . . 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 582	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴‘𝑃) ∘ (𝑎‘𝑃))‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))) = ((𝐴‘𝑃)‘((𝑎‘𝑃)‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)))))
109	17	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐶 ∈ Cat)
110	28	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑋 ∈ 𝐵)
111		eqid 2725	. . . . . . . . . . . 12 ⊢ (comp‘𝐶) = (comp‘𝐶)
112	30	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋))
113	100	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1 ‘𝑃) ∈ (𝑃(Hom ‘𝐶)𝑃))
114	16, 9, 109, 37, 13, 110, 111, 37, 112, 113	yon2 18252	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)) = (𝐾(⟨𝑃, 𝑃⟩(comp‘𝐶)𝑋)( 1 ‘𝑃)))
115	9, 13, 99, 109, 37, 111, 110, 112	catrid 17658	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝐾(⟨𝑃, 𝑃⟩(comp‘𝐶)𝑋)( 1 ‘𝑃)) = 𝐾)
116	114, 115	eqtrd 2765	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)) = 𝐾)
117	116	fveq2d 6894	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑃)‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))) = ((𝑎‘𝑃)‘𝐾))
118		eqid 2725	. . . . . . . . . . . . . . 15 ⊢ (Hom ‘𝑂) = (Hom ‘𝑂)
119	10, 118, 70, 47, 28, 27	funcf2 17848	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃):(𝑋(Hom ‘𝑂)𝑃)⟶(((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)))
120	13, 8	oppchom 17690	. . . . . . . . . . . . . . 15 ⊢ (𝑋(Hom ‘𝑂)𝑃) = (𝑃(Hom ‘𝐶)𝑋)
121	30, 120	eleqtrrdi 2836	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ (𝑋(Hom ‘𝑂)𝑃))
122	119, 121	ffvelcdmd 7088	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)))
123	51, 28	ffvelcdmd 7088	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋) ∈ 𝑈)
124	18, 22, 70, 123, 52	elsetchom 18064	. . . . . . . . . . . . 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 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)⟶((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃))
127	9, 13, 99, 17, 28	catidcl 17656	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( 1 ‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋))
128	16, 9, 17, 28, 13, 28	yon11 18250	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋) = (𝑋(Hom ‘𝐶)𝑋))
129	127, 128	eleqtrrd 2828	. . . . . . . . . . . 12 ⊢ (𝜑 → ( 1 ‘𝑋) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋))
130	129	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1 ‘𝑋) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋))
131		fvco3 6990	. . . . . . . . . . 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 582	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑎‘𝑃) ∘ ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾))‘( 1 ‘𝑋)) = ((𝑎‘𝑃)‘(((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)‘( 1 ‘𝑋))))
133	121	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐾 ∈ (𝑋(Hom ‘𝑂)𝑃))
134	7, 69, 10, 118, 11, 110, 37, 133	nati 17939	. . . . . . . . . . . 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 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋) ∈ 𝑈)
136	18, 40, 11, 135, 53, 61, 126, 73	setcco 18066	. . . . . . . . . . . 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 7088	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘𝐹)‘𝑋) ∈ 𝑈)
138	137	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘𝐹)‘𝑋) ∈ 𝑈)
139	7, 69, 10, 70, 110	natcl 17937	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝑎‘𝑋) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑋)))
140	18, 40, 70, 135, 138	elsetchom 18064	. . . . . . . . . . . . . 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 17848	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋(2^nd ‘𝐹)𝑃):(𝑋(Hom ‘𝑂)𝑃)⟶(((1^st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑃)))
143	142, 121	ffvelcdmd 7088	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∈ (((1^st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑃)))
144	18, 22, 70, 137, 60	elsetchom 18064	. . . . . . . . . . . . . . 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 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾):((1^st ‘𝐹)‘𝑋)⟶((1^st ‘𝐹)‘𝑃))
147	18, 40, 11, 135, 138, 61, 141, 146	setcco 18066	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)(⟨((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋), ((1^st ‘𝐹)‘𝑋)⟩(comp‘𝑆)((1^st ‘𝐹)‘𝑃))(𝑎‘𝑋)) = (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋)))
148	134, 136, 147	3eqtr3d 2773	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑃) ∘ ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)) = (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋)))
149	148	fveq1d 6892	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑎‘𝑃) ∘ ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾))‘( 1 ‘𝑋)) = ((((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋))‘( 1 ‘𝑋)))
150	127	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1 ‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋))
151	16, 9, 109, 110, 13, 110, 111, 37, 112, 150	yon12 18251	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)‘( 1 ‘𝑋)) = (( 1 ‘𝑋)(⟨𝑃, 𝑋⟩(comp‘𝐶)𝑋)𝐾))
152	9, 13, 99, 109, 37, 111, 110, 112	catlid 17657	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (( 1 ‘𝑋)(⟨𝑃, 𝑋⟩(comp‘𝐶)𝑋)𝐾) = 𝐾)
153	151, 152	eqtrd 2765	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)‘( 1 ‘𝑋)) = 𝐾)
154	153	fveq2d 6894	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑃)‘(((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)‘( 1 ‘𝑋))) = ((𝑎‘𝑃)‘𝐾))
155	132, 149, 154	3eqtr3d 2773	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋))‘( 1 ‘𝑋)) = ((𝑎‘𝑃)‘𝐾))
156		fvco3 6990	. . . . . . . . . 10 ⊢ (((𝑎‘𝑋):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)⟶((1^st ‘𝐹)‘𝑋) ∧ ( 1 ‘𝑋) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)) → ((((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋))‘( 1 ‘𝑋)) = (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))
157	141, 130, 156	syl2anc 582	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋))‘( 1 ‘𝑋)) = (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))
158	117, 155, 157	3eqtr2d 2771	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑃)‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))) = (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))
159	158	fveq2d 6894	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴‘𝑃)‘((𝑎‘𝑃)‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)))) = ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋)))))
160	108, 159	eqtrd 2765	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴‘𝑃) ∘ (𝑎‘𝑃))‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))) = ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋)))))
161	98, 105, 160	3eqtrd 2769	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃)‘( 1 ‘𝑃)) = ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋)))))
162	161	mpteq2dva 5244	. . . 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 2777	. . 3 ⊢ (𝜑 → (𝑏 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃)‘( 1 ‘𝑃))) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))))
164		eqid 2725	. . . . . . . . . . 11 ⊢ (𝑄 ×_c 𝑂) = (𝑄 ×_c 𝑂)
165	164, 43, 10	xpcbas 18163	. . . . . . . . . 10 ⊢ ((𝑂 Func 𝑆) × 𝐵) = (Base‘(𝑄 ×_c 𝑂))
166		eqid 2725	. . . . . . . . . 10 ⊢ (Hom ‘(𝑄 ×_c 𝑂)) = (Hom ‘(𝑄 ×_c 𝑂))
167		eqid 2725	. . . . . . . . . 10 ⊢ (Hom ‘𝑇) = (Hom ‘𝑇)
168		relfunc 17842	. . . . . . . . . . 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 18258	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑍 ∈ ((𝑄 ×_c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×_c 𝑂) Func 𝑇)))
175	174	simpld 493	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑍 ∈ ((𝑄 ×_c 𝑂) Func 𝑇))
176		1st2ndbr 8040	. . . . . . . . . . 11 ⊢ ((Rel ((𝑄 ×_c 𝑂) Func 𝑇) ∧ 𝑍 ∈ ((𝑄 ×_c 𝑂) Func 𝑇)) → (1^st ‘𝑍)((𝑄 ×_c 𝑂) Func 𝑇)(2^nd ‘𝑍))
177	168, 175, 176	sylancr 585	. . . . . . . . . 10 ⊢ (𝜑 → (1^st ‘𝑍)((𝑄 ×_c 𝑂) Func 𝑇)(2^nd ‘𝑍))
178	54, 28	opelxpd 5712	. . . . . . . . . 10 ⊢ (𝜑 → ⟨𝐹, 𝑋⟩ ∈ ((𝑂 Func 𝑆) × 𝐵))
179	62, 27	opelxpd 5712	. . . . . . . . . 10 ⊢ (𝜑 → ⟨𝐺, 𝑃⟩ ∈ ((𝑂 Func 𝑆) × 𝐵))
180	165, 166, 167, 177, 178, 179	funcf2 17848	. . . . . . . . 9 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩):(⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×_c 𝑂))⟨𝐺, 𝑃⟩)⟶(((1^st ‘𝑍)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝑍)‘⟨𝐺, 𝑃⟩)))
181	164, 43, 10, 14, 118, 54, 28, 62, 27, 166	xpchom2 18171	. . . . . . . . . . 11 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×_c 𝑂))⟨𝐺, 𝑃⟩) = ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑋(Hom ‘𝑂)𝑃)))
182	120	xpeq2i 5700	. . . . . . . . . . 11 ⊢ ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑋(Hom ‘𝑂)𝑃)) = ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))
183	181, 182	eqtrdi 2781	. . . . . . . . . 10 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×_c 𝑂))⟨𝐺, 𝑃⟩) = ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋)))
184		df-ov 7416	. . . . . . . . . . . . 13 ⊢ (𝐹(1^st ‘𝑍)𝑋) = ((1^st ‘𝑍)‘⟨𝐹, 𝑋⟩)
185		df-ov 7416	. . . . . . . . . . . . 13 ⊢ (𝐺(1^st ‘𝑍)𝑃) = ((1^st ‘𝑍)‘⟨𝐺, 𝑃⟩)
186	184, 185	oveq12i 7425	. . . . . . . . . . . 12 ⊢ ((𝐹(1^st ‘𝑍)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝑍)𝑃)) = (((1^st ‘𝑍)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝑍)‘⟨𝐺, 𝑃⟩))
187	186	eqcomi 2734	. . . . . . . . . . 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 6712	. . . . . . . . 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 7587	. . . . . . 7 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾) ∈ ((𝐹(1^st ‘𝑍)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝑍)𝑃)))
192		eqid 2725	. . . . . . . . . . 11 ⊢ (Base‘𝑇) = (Base‘𝑇)
193	165, 192, 177	funcf1 17846	. . . . . . . . . 10 ⊢ (𝜑 → (1^st ‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
194	193, 54, 28	fovcdmd 7587	. . . . . . . . 9 ⊢ (𝜑 → (𝐹(1^st ‘𝑍)𝑋) ∈ (Base‘𝑇))
195	169, 19	setcbas 18061	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 = (Base‘𝑇))
196	194, 195	eleqtrrd 2828	. . . . . . . 8 ⊢ (𝜑 → (𝐹(1^st ‘𝑍)𝑋) ∈ 𝑉)
197	193, 62, 27	fovcdmd 7587	. . . . . . . . 9 ⊢ (𝜑 → (𝐺(1^st ‘𝑍)𝑃) ∈ (Base‘𝑇))
198	197, 195	eleqtrrd 2828	. . . . . . . 8 ⊢ (𝜑 → (𝐺(1^st ‘𝑍)𝑃) ∈ 𝑉)
199	169, 19, 167, 196, 198	elsetchom 18064	. . . . . . 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 18264	. . . . . . . 8 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾) = (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(2^nd ‘𝐻)⟨((1^st ‘𝑌)‘𝑃), 𝐺⟩)𝐴))
202	8	oppccat 17698	. . . . . . . . . . 11 ⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat)
203	17, 202	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑂 ∈ Cat)
204	18	setccat 18068	. . . . . . . . . . 11 ⊢ (𝑈 ∈ V → 𝑆 ∈ Cat)
205	22, 204	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ Cat)
206	6, 203, 205	fuccat 17956	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ Cat)
207	170, 206, 43, 14, 45, 54, 82, 62, 12, 31, 34	hof2val 18242	. . . . . . . 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 2765	. . . . . . 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 18259	. . . . . . 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 18259	. . . . . . 7 ⊢ (𝜑 → (𝐺(1^st ‘𝑍)𝑃) = (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺))
211	208, 209, 210	feq123d 6706	. . . . . 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 2725	. . . . . 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 7113	. . . . 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 18260	. . . . 5 ⊢ (𝜑 → ((𝐺𝑀𝑃) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺) ↦ ((𝑎‘𝑃)‘( 1 ‘𝑃))) ∧ (𝐺𝑀𝑃):(𝐺(1^st ‘𝑍)𝑃)⟶(𝐺(1^st ‘𝐸)𝑃)))
218	217	simpld 493	. . . 4 ⊢ (𝜑 → (𝐺𝑀𝑃) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺) ↦ ((𝑎‘𝑃)‘( 1 ‘𝑃))))
219		fveq1 6889	. . . . 5 ⊢ (𝑎 = ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)) → (𝑎‘𝑃) = (((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃))
220	219	fveq1d 6892	. . . 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 2725	. . . . . . 7 ⊢ (⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩) = (⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)
223	172, 203, 205, 10, 118, 11, 7, 54, 62, 28, 27, 222, 34, 121	evlf2val 18205	. . . . . 6 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) = ((𝐴‘𝑃)(⟨((1^st ‘𝐹)‘𝑋), ((1^st ‘𝐹)‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)))
224	18, 22, 11, 137, 60, 67, 145, 77	setcco 18066	. . . . . 6 ⊢ (𝜑 → ((𝐴‘𝑃)(⟨((1^st ‘𝐹)‘𝑋), ((1^st ‘𝐹)‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)) = ((𝐴‘𝑃) ∘ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)))
225	223, 224	eqtrd 2765	. . . . 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 18260	. . . . . . . 8 ⊢ (𝜑 → ((𝐹𝑀𝑋) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋))) ∧ (𝐹𝑀𝑋):(𝐹(1^st ‘𝑍)𝑋)⟶(𝐹(1^st ‘𝐸)𝑋)))
228	227	simprd 494	. . . . . . 7 ⊢ (𝜑 → (𝐹𝑀𝑋):(𝐹(1^st ‘𝑍)𝑋)⟶(𝐹(1^st ‘𝐸)𝑋))
229	227	simpld 493	. . . . . . . 8 ⊢ (𝜑 → (𝐹𝑀𝑋) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋))))
230	172, 203, 205, 10, 54, 28	evlf1 18206	. . . . . . . 8 ⊢ (𝜑 → (𝐹(1^st ‘𝐸)𝑋) = ((1^st ‘𝐹)‘𝑋))
231	229, 209, 230	feq123d 6706	. . . . . . 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 2725	. . . . . . 7 ⊢ (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋))) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋)))
234	233	fmpt 7113	. . . . . 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 582	. . . . 5 ⊢ (𝜑 → ((𝐴‘𝑃) ∘ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)) = (𝑦 ∈ ((1^st ‘𝐹)‘𝑋) ↦ ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘𝑦))))
238		2fveq3 6895	. . . . 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 2765	. . 3 ⊢ (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) ∘ (𝐹𝑀𝑋)) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))))
241	163, 221, 240	3eqtr4d 2775	. 2 ⊢ (𝜑 → ((𝐺𝑀𝑃) ∘ (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾)) = ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) ∘ (𝐹𝑀𝑋)))
242		eqid 2725	. . 3 ⊢ (comp‘𝑇) = (comp‘𝑇)
243	174	simprd 494	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ ((𝑄 ×_c 𝑂) Func 𝑇))
244		1st2ndbr 8040	. . . . . . 7 ⊢ ((Rel ((𝑄 ×_c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×_c 𝑂) Func 𝑇)) → (1^st ‘𝐸)((𝑄 ×_c 𝑂) Func 𝑇)(2^nd ‘𝐸))
245	168, 243, 244	sylancr 585	. . . . . 6 ⊢ (𝜑 → (1^st ‘𝐸)((𝑄 ×_c 𝑂) Func 𝑇)(2^nd ‘𝐸))
246	165, 192, 245	funcf1 17846	. . . . 5 ⊢ (𝜑 → (1^st ‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
247	246, 62, 27	fovcdmd 7587	. . . 4 ⊢ (𝜑 → (𝐺(1^st ‘𝐸)𝑃) ∈ (Base‘𝑇))
248	247, 195	eleqtrrd 2828	. . 3 ⊢ (𝜑 → (𝐺(1^st ‘𝐸)𝑃) ∈ 𝑉)
249	217	simprd 494	. . 3 ⊢ (𝜑 → (𝐺𝑀𝑃):(𝐺(1^st ‘𝑍)𝑃)⟶(𝐺(1^st ‘𝐸)𝑃))
250	169, 19, 242, 196, 198, 248, 200, 249	setcco 18066	. 2 ⊢ (𝜑 → ((𝐺𝑀𝑃)(⟨(𝐹(1^st ‘𝑍)𝑋), (𝐺(1^st ‘𝑍)𝑃)⟩(comp‘𝑇)(𝐺(1^st ‘𝐸)𝑃))(𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾)) = ((𝐺𝑀𝑃) ∘ (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾)))
251	246, 54, 28	fovcdmd 7587	. . . 4 ⊢ (𝜑 → (𝐹(1^st ‘𝐸)𝑋) ∈ (Base‘𝑇))
252	251, 195	eleqtrrd 2828	. . 3 ⊢ (𝜑 → (𝐹(1^st ‘𝐸)𝑋) ∈ 𝑉)
253	165, 166, 167, 245, 178, 179	funcf2 17848	. . . . . 6 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩):(⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×_c 𝑂))⟨𝐺, 𝑃⟩)⟶(((1^st ‘𝐸)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝐸)‘⟨𝐺, 𝑃⟩)))
254		df-ov 7416	. . . . . . . . . 10 ⊢ (𝐹(1^st ‘𝐸)𝑋) = ((1^st ‘𝐸)‘⟨𝐹, 𝑋⟩)
255		df-ov 7416	. . . . . . . . . 10 ⊢ (𝐺(1^st ‘𝐸)𝑃) = ((1^st ‘𝐸)‘⟨𝐺, 𝑃⟩)
256	254, 255	oveq12i 7425	. . . . . . . . 9 ⊢ ((𝐹(1^st ‘𝐸)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝐸)𝑃)) = (((1^st ‘𝐸)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝐸)‘⟨𝐺, 𝑃⟩))
257	256	eqcomi 2734	. . . . . . . 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 6712	. . . . . 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 7587	. . . 4 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) ∈ ((𝐹(1^st ‘𝐸)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝐸)𝑃)))
262	169, 19, 167, 252, 248	elsetchom 18064	. . . 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 18066	. 2 ⊢ (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾)(⟨(𝐹(1^st ‘𝑍)𝑋), (𝐹(1^st ‘𝐸)𝑋)⟩(comp‘𝑇)(𝐺(1^st ‘𝐸)𝑃))(𝐹𝑀𝑋)) = ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) ∘ (𝐹𝑀𝑋)))
265	241, 250, 264	3eqtr4d 2775	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 394 = wceq 1533 ∈ wcel 2098 ∀wral 3051 Vcvv 3463 ∪ cun 3939 ⊆ wss 3941 ⟨cop 4631 class class class wbr 5144 ↦ cmpt 5227 × cxp 5671 ran crn 5674 ∘ ccom 5677 Rel wrel 5678 ⟶wf 6539 ‘cfv 6543 (class class class)co 7413 ∈ cmpo 7415 1^st c1st 7985 2^nd c2nd 7986 tpos ctpos 8224 Basecbs 17174 Hom chom 17238 compcco 17239 Catccat 17638 Idccid 17639 Hom_f chomf 17640 oppCatcoppc 17685 Func cfunc 17834 ∘_func ccofu 17836 Nat cnat 17925 FuncCat cfuc 17926 SetCatcsetc 18058 ×_c cxpc 18153 1^st_F c1stf 18154 2^nd_F c2ndf 18155 ⟨,⟩_F cprf 18156 eval_F cevlf 18195 Hom_Fchof 18234 Yoncyon 18235

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5281 ax-sep 5295 ax-nul 5302 ax-pow 5360 ax-pr 5424 ax-un 7735 ax-cnex 11189 ax-resscn 11190 ax-1cn 11191 ax-icn 11192 ax-addcl 11193 ax-addrcl 11194 ax-mulcl 11195 ax-mulrcl 11196 ax-mulcom 11197 ax-addass 11198 ax-mulass 11199 ax-distr 11200 ax-i2m1 11201 ax-1ne0 11202 ax-1rid 11203 ax-rnegex 11204 ax-rrecex 11205 ax-cnre 11206 ax-pre-lttri 11207 ax-pre-lttrn 11208 ax-pre-ltadd 11209 ax-pre-mulgt0 11210

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3465 df-sbc 3771 df-csb 3887 df-dif 3944 df-un 3946 df-in 3948 df-ss 3958 df-pss 3961 df-nul 4320 df-if 4526 df-pw 4601 df-sn 4626 df-pr 4628 df-tp 4630 df-op 4632 df-uni 4905 df-iun 4994 df-br 5145 df-opab 5207 df-mpt 5228 df-tr 5262 df-id 5571 df-eprel 5577 df-po 5585 df-so 5586 df-fr 5628 df-we 5630 df-xp 5679 df-rel 5680 df-cnv 5681 df-co 5682 df-dm 5683 df-rn 5684 df-res 5685 df-ima 5686 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7369 df-ov 7416 df-oprab 7417 df-mpo 7418 df-om 7866 df-1st 7987 df-2nd 7988 df-tpos 8225 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-1o 8480 df-er 8718 df-map 8840 df-pm 8841 df-ixp 8910 df-en 8958 df-dom 8959 df-sdom 8960 df-fin 8961 df-pnf 11275 df-mnf 11276 df-xr 11277 df-ltxr 11278 df-le 11279 df-sub 11471 df-neg 11472 df-nn 12238 df-2 12300 df-3 12301 df-4 12302 df-5 12303 df-6 12304 df-7 12305 df-8 12306 df-9 12307 df-n0 12498 df-z 12584 df-dec 12703 df-uz 12848 df-fz 13512 df-struct 17110 df-sets 17127 df-slot 17145 df-ndx 17157 df-base 17175 df-ress 17204 df-hom 17251 df-cco 17252 df-cat 17642 df-cid 17643 df-homf 17644 df-comf 17645 df-oppc 17686 df-ssc 17787 df-resc 17788 df-subc 17789 df-func 17838 df-cofu 17840 df-nat 17927 df-fuc 17928 df-setc 18059 df-xpc 18157 df-1stf 18158 df-2ndf 18159 df-prf 18160 df-evlf 18199 df-curf 18200 df-hof 18236 df-yon 18237

This theorem is referenced by: yonedalem3 18266

W3C validator