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 17529

Description: Lemma for yoneda 17533. (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 7164	. . . . . . . 8 ⊢ (𝑏 = 𝑎 → (𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏) = (𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎))
2	1	oveq1d 7171	. . . . . . 7 ⊢ (𝑏 = 𝑎 → ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)) = ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)))
3	2	fveq1d 6672	. . . . . 6 ⊢ (𝑏 = 𝑎 → (((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃) = (((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃))
4	3	fveq1d 6672	. . . . 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 5169	. . . 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 2821	. . . . . . . . 9 ⊢ (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆)
8		yoneda.o	. . . . . . . . . 10 ⊢ 𝑂 = (oppCat‘𝐶)
9		yoneda.b	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝐶)
10	8, 9	oppcbas 16988	. . . . . . . . 9 ⊢ 𝐵 = (Base‘𝑂)
11		eqid 2821	. . . . . . . . 9 ⊢ (comp‘𝑆) = (comp‘𝑆)
12		eqid 2821	. . . . . . . . 9 ⊢ (comp‘𝑄) = (comp‘𝑄)
13		eqid 2821	. . . . . . . . . . . 12 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
14	6, 7	fuchom 17231	. . . . . . . . . . . 12 ⊢ (𝑂 Nat 𝑆) = (Hom ‘𝑄)
15		relfunc 17132	. . . . . . . . . . . . 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 4164	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 ⊆ 𝑉)
22	19, 21	ssexd 5228	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ∈ V)
23		yoneda.u	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran (Hom_f ‘𝐶) ⊆ 𝑈)
24	16, 17, 8, 18, 6, 22, 23	yoncl 17512	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ∈ (𝐶 Func 𝑄))
25		1st2ndbr 7741	. . . . . . . . . . . . 13 ⊢ ((Rel (𝐶 Func 𝑄) ∧ 𝑌 ∈ (𝐶 Func 𝑄)) → (1^st ‘𝑌)(𝐶 Func 𝑄)(2^nd ‘𝑌))
26	15, 24, 25	sylancr 589	. . . . . . . . . . . 12 ⊢ (𝜑 → (1^st ‘𝑌)(𝐶 Func 𝑄)(2^nd ‘𝑌))
27		yonedalem22.p	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ 𝐵)
28		yonedalem21.x	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
29	9, 13, 14, 26, 27, 28	funcf2 17138	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃(2^nd ‘𝑌)𝑋):(𝑃(Hom ‘𝐶)𝑋)⟶(((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑋)))
30		yonedalem22.k	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋))
31	29, 30	ffvelrnd 6852	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑃(2^nd ‘𝑌)𝑋)‘𝐾) ∈ (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑋)))
32	31	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑃(2^nd ‘𝑌)𝑋)‘𝐾) ∈ (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑋)))
33		simpr 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹))
34		yonedalem22.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺))
35	34	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐴 ∈ (𝐹(𝑂 Nat 𝑆)𝐺))
36	6, 7, 12, 33, 35	fuccocl 17234	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎) ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐺))
37	27	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑃 ∈ 𝐵)
38	6, 7, 10, 11, 12, 32, 36, 37	fuccoval 17233	. . . . . . . 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 17233	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)‘𝑃) = ((𝐴‘𝑃)(⟨((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃), ((1^st ‘𝐹)‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))(𝑎‘𝑃)))
40	22	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑈 ∈ V)
41		eqid 2821	. . . . . . . . . . . . . . 15 ⊢ (Base‘𝑆) = (Base‘𝑆)
42		relfunc 17132	. . . . . . . . . . . . . . . 16 ⊢ Rel (𝑂 Func 𝑆)
43	6	fucbas 17230	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑂 Func 𝑆) = (Base‘𝑄)
44	9, 43, 26	funcf1 17136	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1^st ‘𝑌):𝐵⟶(𝑂 Func 𝑆))
45	44, 28	ffvelrnd 6852	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1^st ‘𝑌)‘𝑋) ∈ (𝑂 Func 𝑆))
46		1st2ndbr 7741	. . . . . . . . . . . . . . . 16 ⊢ ((Rel (𝑂 Func 𝑆) ∧ ((1^st ‘𝑌)‘𝑋) ∈ (𝑂 Func 𝑆)) → (1^st ‘((1^st ‘𝑌)‘𝑋))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑋)))
47	42, 45, 46	sylancr 589	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1^st ‘((1^st ‘𝑌)‘𝑋))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑋)))
48	10, 41, 47	funcf1 17136	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1^st ‘((1^st ‘𝑌)‘𝑋)):𝐵⟶(Base‘𝑆))
49	18, 22	setcbas 17338	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 = (Base‘𝑆))
50	49	feq3d 6501	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑋)):𝐵⟶𝑈 ↔ (1^st ‘((1^st ‘𝑌)‘𝑋)):𝐵⟶(Base‘𝑆)))
51	48, 50	mpbird 259	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1^st ‘((1^st ‘𝑌)‘𝑋)):𝐵⟶𝑈)
52	51, 27	ffvelrnd 6852	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃) ∈ 𝑈)
53	52	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃) ∈ 𝑈)
54		yonedalem21.f	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹 ∈ (𝑂 Func 𝑆))
55		1st2ndbr 7741	. . . . . . . . . . . . . . . 16 ⊢ ((Rel (𝑂 Func 𝑆) ∧ 𝐹 ∈ (𝑂 Func 𝑆)) → (1^st ‘𝐹)(𝑂 Func 𝑆)(2^nd ‘𝐹))
56	42, 54, 55	sylancr 589	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1^st ‘𝐹)(𝑂 Func 𝑆)(2^nd ‘𝐹))
57	10, 41, 56	funcf1 17136	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1^st ‘𝐹):𝐵⟶(Base‘𝑆))
58	49	feq3d 6501	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘𝐹):𝐵⟶𝑈 ↔ (1^st ‘𝐹):𝐵⟶(Base‘𝑆)))
59	57, 58	mpbird 259	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1^st ‘𝐹):𝐵⟶𝑈)
60	59, 27	ffvelrnd 6852	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1^st ‘𝐹)‘𝑃) ∈ 𝑈)
61	60	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘𝐹)‘𝑃) ∈ 𝑈)
62		yonedalem22.g	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐺 ∈ (𝑂 Func 𝑆))
63		1st2ndbr 7741	. . . . . . . . . . . . . . . 16 ⊢ ((Rel (𝑂 Func 𝑆) ∧ 𝐺 ∈ (𝑂 Func 𝑆)) → (1^st ‘𝐺)(𝑂 Func 𝑆)(2^nd ‘𝐺))
64	42, 62, 63	sylancr 589	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1^st ‘𝐺)(𝑂 Func 𝑆)(2^nd ‘𝐺))
65	10, 41, 64	funcf1 17136	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (1^st ‘𝐺):𝐵⟶(Base‘𝑆))
66	65, 27	ffvelrnd 6852	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1^st ‘𝐺)‘𝑃) ∈ (Base‘𝑆))
67	66, 49	eleqtrrd 2916	. . . . . . . . . . . 12 ⊢ (𝜑 → ((1^st ‘𝐺)‘𝑃) ∈ 𝑈)
68	67	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘𝐺)‘𝑃) ∈ 𝑈)
69	7, 33	nat1st2nd 17221	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑎 ∈ (⟨(1^st ‘((1^st ‘𝑌)‘𝑋)), (2^nd ‘((1^st ‘𝑌)‘𝑋))⟩(𝑂 Nat 𝑆)⟨(1^st ‘𝐹), (2^nd ‘𝐹)⟩))
70		eqid 2821	. . . . . . . . . . . . 13 ⊢ (Hom ‘𝑆) = (Hom ‘𝑆)
71	7, 69, 10, 70, 37	natcl 17223	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝑎‘𝑃) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑃)))
72	18, 40, 70, 53, 61	elsetchom 17341	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑃) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑃)) ↔ (𝑎‘𝑃):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟶((1^st ‘𝐹)‘𝑃)))
73	71, 72	mpbid 234	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝑎‘𝑃):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟶((1^st ‘𝐹)‘𝑃))
74	7, 34	nat1st2nd 17221	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ∈ (⟨(1^st ‘𝐹), (2^nd ‘𝐹)⟩(𝑂 Nat 𝑆)⟨(1^st ‘𝐺), (2^nd ‘𝐺)⟩))
75	7, 74, 10, 70, 27	natcl 17223	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴‘𝑃) ∈ (((1^st ‘𝐹)‘𝑃)(Hom ‘𝑆)((1^st ‘𝐺)‘𝑃)))
76	18, 22, 70, 60, 67	elsetchom 17341	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴‘𝑃) ∈ (((1^st ‘𝐹)‘𝑃)(Hom ‘𝑆)((1^st ‘𝐺)‘𝑃)) ↔ (𝐴‘𝑃):((1^st ‘𝐹)‘𝑃)⟶((1^st ‘𝐺)‘𝑃)))
77	75, 76	mpbid 234	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴‘𝑃):((1^st ‘𝐹)‘𝑃)⟶((1^st ‘𝐺)‘𝑃))
78	77	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝐴‘𝑃):((1^st ‘𝐹)‘𝑃)⟶((1^st ‘𝐺)‘𝑃))
79	18, 40, 11, 53, 61, 68, 73, 78	setcco 17343	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴‘𝑃)(⟨((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃), ((1^st ‘𝐹)‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))(𝑎‘𝑃)) = ((𝐴‘𝑃) ∘ (𝑎‘𝑃)))
80	39, 79	eqtrd 2856	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)‘𝑃) = ((𝐴‘𝑃) ∘ (𝑎‘𝑃)))
81	80	oveq1d 7171	. . . . . . . 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	ffvelrnd 6852	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘𝑌)‘𝑃) ∈ (𝑂 Func 𝑆))
83		1st2ndbr 7741	. . . . . . . . . . . . . 14 ⊢ ((Rel (𝑂 Func 𝑆) ∧ ((1^st ‘𝑌)‘𝑃) ∈ (𝑂 Func 𝑆)) → (1^st ‘((1^st ‘𝑌)‘𝑃))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑃)))
84	42, 82, 83	sylancr 589	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1^st ‘((1^st ‘𝑌)‘𝑃))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑃)))
85	10, 41, 84	funcf1 17136	. . . . . . . . . . . 12 ⊢ (𝜑 → (1^st ‘((1^st ‘𝑌)‘𝑃)):𝐵⟶(Base‘𝑆))
86	85, 27	ffvelrnd 6852	. . . . . . . . . . 11 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃) ∈ (Base‘𝑆))
87	86, 49	eleqtrrd 2916	. . . . . . . . . 10 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃) ∈ 𝑈)
88	87	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃) ∈ 𝑈)
89	7, 31	nat1st2nd 17221	. . . . . . . . . . . 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 17223	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃)(Hom ‘𝑆)((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)))
91	18, 22, 70, 87, 52	elsetchom 17341	. . . . . . . . . . 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 234	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃):((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃)⟶((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃))
93	92	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃):((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃)⟶((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃))
94		fco 6531	. . . . . . . . . 10 ⊢ (((𝐴‘𝑃):((1^st ‘𝐹)‘𝑃)⟶((1^st ‘𝐺)‘𝑃) ∧ (𝑎‘𝑃):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟶((1^st ‘𝐹)‘𝑃)) → ((𝐴‘𝑃) ∘ (𝑎‘𝑃)):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟶((1^st ‘𝐺)‘𝑃))
95	78, 73, 94	syl2anc 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴‘𝑃) ∘ (𝑎‘𝑃)):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟶((1^st ‘𝐺)‘𝑃))
96	18, 40, 11, 88, 53, 68, 93, 95	setcco 17343	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴‘𝑃) ∘ (𝑎‘𝑃))(⟨((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃), ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))(((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)) = (((𝐴‘𝑃) ∘ (𝑎‘𝑃)) ∘ (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)))
97	38, 81, 96	3eqtrd 2860	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃) = (((𝐴‘𝑃) ∘ (𝑎‘𝑃)) ∘ (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)))
98	97	fveq1d 6672	. . . . . 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 16953	. . . . . . . . 9 ⊢ (𝜑 → ( 1 ‘𝑃) ∈ (𝑃(Hom ‘𝐶)𝑃))
101	16, 9, 17, 27, 13, 27	yon11 17514	. . . . . . . . 9 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃) = (𝑃(Hom ‘𝐶)𝑃))
102	100, 101	eleqtrrd 2916	. . . . . . . 8 ⊢ (𝜑 → ( 1 ‘𝑃) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃))
103	102	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1 ‘𝑃) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑃))‘𝑃))
104		fvco3 6760	. . . . . . 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 586	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝐴‘𝑃) ∘ (𝑎‘𝑃)) ∘ (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃))‘( 1 ‘𝑃)) = (((𝐴‘𝑃) ∘ (𝑎‘𝑃))‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))))
106	93, 103	ffvelrnd 6852	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃))
107		fvco3 6760	. . . . . . . 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 586	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴‘𝑃) ∘ (𝑎‘𝑃))‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))) = ((𝐴‘𝑃)‘((𝑎‘𝑃)‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)))))
109	17	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐶 ∈ Cat)
110	28	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝑋 ∈ 𝐵)
111		eqid 2821	. . . . . . . . . . . 12 ⊢ (comp‘𝐶) = (comp‘𝐶)
112	30	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐾 ∈ (𝑃(Hom ‘𝐶)𝑋))
113	100	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1 ‘𝑃) ∈ (𝑃(Hom ‘𝐶)𝑃))
114	16, 9, 109, 37, 13, 110, 111, 37, 112, 113	yon2 17516	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)) = (𝐾(⟨𝑃, 𝑃⟩(comp‘𝐶)𝑋)( 1 ‘𝑃)))
115	9, 13, 99, 109, 37, 111, 110, 112	catrid 16955	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝐾(⟨𝑃, 𝑃⟩(comp‘𝐶)𝑋)( 1 ‘𝑃)) = 𝐾)
116	114, 115	eqtrd 2856	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)) = 𝐾)
117	116	fveq2d 6674	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑃)‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))) = ((𝑎‘𝑃)‘𝐾))
118		eqid 2821	. . . . . . . . . . . . . . 15 ⊢ (Hom ‘𝑂) = (Hom ‘𝑂)
119	10, 118, 70, 47, 28, 27	funcf2 17138	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃):(𝑋(Hom ‘𝑂)𝑃)⟶(((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)))
120	13, 8	oppchom 16985	. . . . . . . . . . . . . . 15 ⊢ (𝑋(Hom ‘𝑂)𝑃) = (𝑃(Hom ‘𝐶)𝑋)
121	30, 120	eleqtrrdi 2924	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ (𝑋(Hom ‘𝑂)𝑃))
122	119, 121	ffvelrnd 6852	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃)))
123	51, 28	ffvelrnd 6852	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋) ∈ 𝑈)
124	18, 22, 70, 123, 52	elsetchom 17341	. . . . . . . . . . . . 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 234	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)⟶((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃))
126	125	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)⟶((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑃))
127	9, 13, 99, 17, 28	catidcl 16953	. . . . . . . . . . . . 13 ⊢ (𝜑 → ( 1 ‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋))
128	16, 9, 17, 28, 13, 28	yon11 17514	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋) = (𝑋(Hom ‘𝐶)𝑋))
129	127, 128	eleqtrrd 2916	. . . . . . . . . . . 12 ⊢ (𝜑 → ( 1 ‘𝑋) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋))
130	129	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1 ‘𝑋) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋))
131		fvco3 6760	. . . . . . . . . . 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 586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑎‘𝑃) ∘ ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾))‘( 1 ‘𝑋)) = ((𝑎‘𝑃)‘(((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)‘( 1 ‘𝑋))))
133	121	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → 𝐾 ∈ (𝑋(Hom ‘𝑂)𝑃))
134	7, 69, 10, 118, 11, 110, 37, 133	nati 17225	. . . . . . . . . . . 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 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋) ∈ 𝑈)
136	18, 40, 11, 135, 53, 61, 126, 73	setcco 17343	. . . . . . . . . . . 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	ffvelrnd 6852	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((1^st ‘𝐹)‘𝑋) ∈ 𝑈)
138	137	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((1^st ‘𝐹)‘𝑋) ∈ 𝑈)
139	7, 69, 10, 70, 110	natcl 17223	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝑎‘𝑋) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑋)))
140	18, 40, 70, 135, 138	elsetchom 17341	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑋) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑋)) ↔ (𝑎‘𝑋):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)⟶((1^st ‘𝐹)‘𝑋)))
141	139, 140	mpbid 234	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (𝑎‘𝑋):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)⟶((1^st ‘𝐹)‘𝑋))
142	10, 118, 70, 56, 28, 27	funcf2 17138	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑋(2^nd ‘𝐹)𝑃):(𝑋(Hom ‘𝑂)𝑃)⟶(((1^st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑃)))
143	142, 121	ffvelrnd 6852	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∈ (((1^st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑃)))
144	18, 22, 70, 137, 60	elsetchom 17341	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∈ (((1^st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1^st ‘𝐹)‘𝑃)) ↔ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾):((1^st ‘𝐹)‘𝑋)⟶((1^st ‘𝐹)‘𝑃)))
145	143, 144	mpbid 234	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾):((1^st ‘𝐹)‘𝑋)⟶((1^st ‘𝐹)‘𝑃))
146	145	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾):((1^st ‘𝐹)‘𝑋)⟶((1^st ‘𝐹)‘𝑃))
147	18, 40, 11, 135, 138, 61, 141, 146	setcco 17343	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)(⟨((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋), ((1^st ‘𝐹)‘𝑋)⟩(comp‘𝑆)((1^st ‘𝐹)‘𝑃))(𝑎‘𝑋)) = (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋)))
148	134, 136, 147	3eqtr3d 2864	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑃) ∘ ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)) = (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋)))
149	148	fveq1d 6672	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑎‘𝑃) ∘ ((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾))‘( 1 ‘𝑋)) = ((((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋))‘( 1 ‘𝑋)))
150	127	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ( 1 ‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋))
151	16, 9, 109, 110, 13, 110, 111, 37, 112, 150	yon12 17515	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)‘( 1 ‘𝑋)) = (( 1 ‘𝑋)(⟨𝑃, 𝑋⟩(comp‘𝐶)𝑋)𝐾))
152	9, 13, 99, 109, 37, 111, 110, 112	catlid 16954	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (( 1 ‘𝑋)(⟨𝑃, 𝑋⟩(comp‘𝐶)𝑋)𝐾) = 𝐾)
153	151, 152	eqtrd 2856	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)‘( 1 ‘𝑋)) = 𝐾)
154	153	fveq2d 6674	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑃)‘(((𝑋(2^nd ‘((1^st ‘𝑌)‘𝑋))𝑃)‘𝐾)‘( 1 ‘𝑋))) = ((𝑎‘𝑃)‘𝐾))
155	132, 149, 154	3eqtr3d 2864	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋))‘( 1 ‘𝑋)) = ((𝑎‘𝑃)‘𝐾))
156		fvco3 6760	. . . . . . . . . 10 ⊢ (((𝑎‘𝑋):((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)⟶((1^st ‘𝐹)‘𝑋) ∧ ( 1 ‘𝑋) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑋))‘𝑋)) → ((((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋))‘( 1 ‘𝑋)) = (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))
157	141, 130, 156	syl2anc 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝑋(2^nd ‘𝐹)𝑃)‘𝐾) ∘ (𝑎‘𝑋))‘( 1 ‘𝑋)) = (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))
158	117, 155, 157	3eqtr2d 2862	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝑎‘𝑃)‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))) = (((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))
159	158	fveq2d 6674	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((𝐴‘𝑃)‘((𝑎‘𝑃)‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃)))) = ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋)))))
160	108, 159	eqtrd 2856	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → (((𝐴‘𝑃) ∘ (𝑎‘𝑃))‘((((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)‘𝑃)‘( 1 ‘𝑃))) = ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋)))))
161	98, 105, 160	3eqtrd 2860	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) → ((((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃)‘( 1 ‘𝑃)) = ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋)))))
162	161	mpteq2dva 5161	. . . 4 ⊢ (𝜑 → (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑎)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃)‘( 1 ‘𝑃))) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))))
163	5, 162	syl5eq 2868	. . 3 ⊢ (𝜑 → (𝑏 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃)‘( 1 ‘𝑃))) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))))
164		eqid 2821	. . . . . . . . . . 11 ⊢ (𝑄 ×_c 𝑂) = (𝑄 ×_c 𝑂)
165	164, 43, 10	xpcbas 17428	. . . . . . . . . 10 ⊢ ((𝑂 Func 𝑆) × 𝐵) = (Base‘(𝑄 ×_c 𝑂))
166		eqid 2821	. . . . . . . . . 10 ⊢ (Hom ‘(𝑄 ×_c 𝑂)) = (Hom ‘(𝑄 ×_c 𝑂))
167		eqid 2821	. . . . . . . . . 10 ⊢ (Hom ‘𝑇) = (Hom ‘𝑇)
168		relfunc 17132	. . . . . . . . . . 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 17522	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑍 ∈ ((𝑄 ×_c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×_c 𝑂) Func 𝑇)))
175	174	simpld 497	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑍 ∈ ((𝑄 ×_c 𝑂) Func 𝑇))
176		1st2ndbr 7741	. . . . . . . . . . 11 ⊢ ((Rel ((𝑄 ×_c 𝑂) Func 𝑇) ∧ 𝑍 ∈ ((𝑄 ×_c 𝑂) Func 𝑇)) → (1^st ‘𝑍)((𝑄 ×_c 𝑂) Func 𝑇)(2^nd ‘𝑍))
177	168, 175, 176	sylancr 589	. . . . . . . . . 10 ⊢ (𝜑 → (1^st ‘𝑍)((𝑄 ×_c 𝑂) Func 𝑇)(2^nd ‘𝑍))
178	54, 28	opelxpd 5593	. . . . . . . . . 10 ⊢ (𝜑 → ⟨𝐹, 𝑋⟩ ∈ ((𝑂 Func 𝑆) × 𝐵))
179	62, 27	opelxpd 5593	. . . . . . . . . 10 ⊢ (𝜑 → ⟨𝐺, 𝑃⟩ ∈ ((𝑂 Func 𝑆) × 𝐵))
180	165, 166, 167, 177, 178, 179	funcf2 17138	. . . . . . . . 9 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩):(⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×_c 𝑂))⟨𝐺, 𝑃⟩)⟶(((1^st ‘𝑍)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝑍)‘⟨𝐺, 𝑃⟩)))
181	164, 43, 10, 14, 118, 54, 28, 62, 27, 166	xpchom2 17436	. . . . . . . . . . 11 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×_c 𝑂))⟨𝐺, 𝑃⟩) = ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑋(Hom ‘𝑂)𝑃)))
182	120	xpeq2i 5582	. . . . . . . . . . 11 ⊢ ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑋(Hom ‘𝑂)𝑃)) = ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))
183	181, 182	syl6eq 2872	. . . . . . . . . 10 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×_c 𝑂))⟨𝐺, 𝑃⟩) = ((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋)))
184		df-ov 7159	. . . . . . . . . . . . 13 ⊢ (𝐹(1^st ‘𝑍)𝑋) = ((1^st ‘𝑍)‘⟨𝐹, 𝑋⟩)
185		df-ov 7159	. . . . . . . . . . . . 13 ⊢ (𝐺(1^st ‘𝑍)𝑃) = ((1^st ‘𝑍)‘⟨𝐺, 𝑃⟩)
186	184, 185	oveq12i 7168	. . . . . . . . . . . 12 ⊢ ((𝐹(1^st ‘𝑍)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝑍)𝑃)) = (((1^st ‘𝑍)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝑍)‘⟨𝐺, 𝑃⟩))
187	186	eqcomi 2830	. . . . . . . . . . 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 6509	. . . . . . . . 9 ⊢ (𝜑 → ((⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩):(⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×_c 𝑂))⟨𝐺, 𝑃⟩)⟶(((1^st ‘𝑍)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝑍)‘⟨𝐺, 𝑃⟩)) ↔ (⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩):((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))⟶((𝐹(1^st ‘𝑍)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝑍)𝑃))))
190	180, 189	mpbid 234	. . . . . . . 8 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩):((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))⟶((𝐹(1^st ‘𝑍)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝑍)𝑃)))
191	190, 34, 30	fovrnd 7320	. . . . . . 7 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾) ∈ ((𝐹(1^st ‘𝑍)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝑍)𝑃)))
192		eqid 2821	. . . . . . . . . . 11 ⊢ (Base‘𝑇) = (Base‘𝑇)
193	165, 192, 177	funcf1 17136	. . . . . . . . . 10 ⊢ (𝜑 → (1^st ‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
194	193, 54, 28	fovrnd 7320	. . . . . . . . 9 ⊢ (𝜑 → (𝐹(1^st ‘𝑍)𝑋) ∈ (Base‘𝑇))
195	169, 19	setcbas 17338	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 = (Base‘𝑇))
196	194, 195	eleqtrrd 2916	. . . . . . . 8 ⊢ (𝜑 → (𝐹(1^st ‘𝑍)𝑋) ∈ 𝑉)
197	193, 62, 27	fovrnd 7320	. . . . . . . . 9 ⊢ (𝜑 → (𝐺(1^st ‘𝑍)𝑃) ∈ (Base‘𝑇))
198	197, 195	eleqtrrd 2916	. . . . . . . 8 ⊢ (𝜑 → (𝐺(1^st ‘𝑍)𝑃) ∈ 𝑉)
199	169, 19, 167, 196, 198	elsetchom 17341	. . . . . . 7 ⊢ (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾) ∈ ((𝐹(1^st ‘𝑍)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝑍)𝑃)) ↔ (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾):(𝐹(1^st ‘𝑍)𝑋)⟶(𝐺(1^st ‘𝑍)𝑃)))
200	191, 199	mpbid 234	. . . . . 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 17528	. . . . . . . 8 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾) = (((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(2^nd ‘𝐻)⟨((1^st ‘𝑌)‘𝑃), 𝐺⟩)𝐴))
202	8	oppccat 16992	. . . . . . . . . . 11 ⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat)
203	17, 202	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑂 ∈ Cat)
204	18	setccat 17345	. . . . . . . . . . 11 ⊢ (𝑈 ∈ V → 𝑆 ∈ Cat)
205	22, 204	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ Cat)
206	6, 203, 205	fuccat 17240	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 ∈ Cat)
207	170, 206, 43, 14, 45, 54, 82, 62, 12, 31, 34	hof2val 17506	. . . . . . . 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 2856	. . . . . . 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 17523	. . . . . . 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 17523	. . . . . . 7 ⊢ (𝜑 → (𝐺(1^st ‘𝑍)𝑃) = (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺))
211	208, 209, 210	feq123d 6503	. . . . . 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 234	. . . . 5 ⊢ (𝜑 → (𝑏 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))):(((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)⟶(((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺))
213		eqid 2821	. . . . . 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 6874	. . . . 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 236	. . . 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 17524	. . . . 5 ⊢ (𝜑 → ((𝐺𝑀𝑃) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺) ↦ ((𝑎‘𝑃)‘( 1 ‘𝑃))) ∧ (𝐺𝑀𝑃):(𝐺(1^st ‘𝑍)𝑃)⟶(𝐺(1^st ‘𝐸)𝑃)))
218	217	simpld 497	. . . 4 ⊢ (𝜑 → (𝐺𝑀𝑃) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑃)(𝑂 Nat 𝑆)𝐺) ↦ ((𝑎‘𝑃)‘( 1 ‘𝑃))))
219		fveq1 6669	. . . . 5 ⊢ (𝑎 = ((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾)) → (𝑎‘𝑃) = (((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃))
220	219	fveq1d 6672	. . . 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 6892	. . 3 ⊢ (𝜑 → ((𝐺𝑀𝑃) ∘ (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾)) = (𝑏 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((((𝐴(⟨((1^st ‘𝑌)‘𝑋), 𝐹⟩(comp‘𝑄)𝐺)𝑏)(⟨((1^st ‘𝑌)‘𝑃), ((1^st ‘𝑌)‘𝑋)⟩(comp‘𝑄)𝐺)((𝑃(2^nd ‘𝑌)𝑋)‘𝐾))‘𝑃)‘( 1 ‘𝑃))))
222		eqid 2821	. . . . . . 7 ⊢ (⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩) = (⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)
223	172, 203, 205, 10, 118, 11, 7, 54, 62, 28, 27, 222, 34, 121	evlf2val 17469	. . . . . 6 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) = ((𝐴‘𝑃)(⟨((1^st ‘𝐹)‘𝑋), ((1^st ‘𝐹)‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)))
224	18, 22, 11, 137, 60, 67, 145, 77	setcco 17343	. . . . . 6 ⊢ (𝜑 → ((𝐴‘𝑃)(⟨((1^st ‘𝐹)‘𝑋), ((1^st ‘𝐹)‘𝑃)⟩(comp‘𝑆)((1^st ‘𝐺)‘𝑃))((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)) = ((𝐴‘𝑃) ∘ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)))
225	223, 224	eqtrd 2856	. . . . 5 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) = ((𝐴‘𝑃) ∘ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)))
226	225	coeq1d 5732	. . . 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 17524	. . . . . . . 8 ⊢ (𝜑 → ((𝐹𝑀𝑋) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋))) ∧ (𝐹𝑀𝑋):(𝐹(1^st ‘𝑍)𝑋)⟶(𝐹(1^st ‘𝐸)𝑋)))
228	227	simprd 498	. . . . . . 7 ⊢ (𝜑 → (𝐹𝑀𝑋):(𝐹(1^st ‘𝑍)𝑋)⟶(𝐹(1^st ‘𝐸)𝑋))
229	227	simpld 497	. . . . . . . 8 ⊢ (𝜑 → (𝐹𝑀𝑋) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋))))
230	172, 203, 205, 10, 54, 28	evlf1 17470	. . . . . . . 8 ⊢ (𝜑 → (𝐹(1^st ‘𝐸)𝑋) = ((1^st ‘𝐹)‘𝑋))
231	229, 209, 230	feq123d 6503	. . . . . . 7 ⊢ (𝜑 → ((𝐹𝑀𝑋):(𝐹(1^st ‘𝑍)𝑋)⟶(𝐹(1^st ‘𝐸)𝑋) ↔ (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋))):(((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)⟶((1^st ‘𝐹)‘𝑋)))
232	228, 231	mpbid 234	. . . . . 6 ⊢ (𝜑 → (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋))):(((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)⟶((1^st ‘𝐹)‘𝑋))
233		eqid 2821	. . . . . . 7 ⊢ (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋))) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋)))
234	233	fmpt 6874	. . . . . 6 ⊢ (∀𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)((𝑎‘𝑋)‘( 1 ‘𝑋)) ∈ ((1^st ‘𝐹)‘𝑋) ↔ (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝑎‘𝑋)‘( 1 ‘𝑋))):(((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)⟶((1^st ‘𝐹)‘𝑋))
235	232, 234	sylibr 236	. . . . 5 ⊢ (𝜑 → ∀𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)((𝑎‘𝑋)‘( 1 ‘𝑋)) ∈ ((1^st ‘𝐹)‘𝑋))
236		fcompt 6895	. . . . . 6 ⊢ (((𝐴‘𝑃):((1^st ‘𝐹)‘𝑃)⟶((1^st ‘𝐺)‘𝑃) ∧ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾):((1^st ‘𝐹)‘𝑋)⟶((1^st ‘𝐹)‘𝑃)) → ((𝐴‘𝑃) ∘ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)) = (𝑦 ∈ ((1^st ‘𝐹)‘𝑋) ↦ ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘𝑦))))
237	77, 145, 236	syl2anc 586	. . . . 5 ⊢ (𝜑 → ((𝐴‘𝑃) ∘ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)) = (𝑦 ∈ ((1^st ‘𝐹)‘𝑋) ↦ ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘𝑦))))
238		2fveq3 6675	. . . . 5 ⊢ (𝑦 = ((𝑎‘𝑋)‘( 1 ‘𝑋)) → ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘𝑦)) = ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋)))))
239	235, 229, 237, 238	fmptcof 6892	. . . 4 ⊢ (𝜑 → (((𝐴‘𝑃) ∘ ((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)) ∘ (𝐹𝑀𝑋)) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))))
240	226, 239	eqtrd 2856	. . 3 ⊢ (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) ∘ (𝐹𝑀𝑋)) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↦ ((𝐴‘𝑃)‘(((𝑋(2^nd ‘𝐹)𝑃)‘𝐾)‘((𝑎‘𝑋)‘( 1 ‘𝑋))))))
241	163, 221, 240	3eqtr4d 2866	. 2 ⊢ (𝜑 → ((𝐺𝑀𝑃) ∘ (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾)) = ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) ∘ (𝐹𝑀𝑋)))
242		eqid 2821	. . 3 ⊢ (comp‘𝑇) = (comp‘𝑇)
243	174	simprd 498	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ ((𝑄 ×_c 𝑂) Func 𝑇))
244		1st2ndbr 7741	. . . . . . 7 ⊢ ((Rel ((𝑄 ×_c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×_c 𝑂) Func 𝑇)) → (1^st ‘𝐸)((𝑄 ×_c 𝑂) Func 𝑇)(2^nd ‘𝐸))
245	168, 243, 244	sylancr 589	. . . . . 6 ⊢ (𝜑 → (1^st ‘𝐸)((𝑄 ×_c 𝑂) Func 𝑇)(2^nd ‘𝐸))
246	165, 192, 245	funcf1 17136	. . . . 5 ⊢ (𝜑 → (1^st ‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
247	246, 62, 27	fovrnd 7320	. . . 4 ⊢ (𝜑 → (𝐺(1^st ‘𝐸)𝑃) ∈ (Base‘𝑇))
248	247, 195	eleqtrrd 2916	. . 3 ⊢ (𝜑 → (𝐺(1^st ‘𝐸)𝑃) ∈ 𝑉)
249	217	simprd 498	. . 3 ⊢ (𝜑 → (𝐺𝑀𝑃):(𝐺(1^st ‘𝑍)𝑃)⟶(𝐺(1^st ‘𝐸)𝑃))
250	169, 19, 242, 196, 198, 248, 200, 249	setcco 17343	. 2 ⊢ (𝜑 → ((𝐺𝑀𝑃)(⟨(𝐹(1^st ‘𝑍)𝑋), (𝐺(1^st ‘𝑍)𝑃)⟩(comp‘𝑇)(𝐺(1^st ‘𝐸)𝑃))(𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾)) = ((𝐺𝑀𝑃) ∘ (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝑍)⟨𝐺, 𝑃⟩)𝐾)))
251	246, 54, 28	fovrnd 7320	. . . 4 ⊢ (𝜑 → (𝐹(1^st ‘𝐸)𝑋) ∈ (Base‘𝑇))
252	251, 195	eleqtrrd 2916	. . 3 ⊢ (𝜑 → (𝐹(1^st ‘𝐸)𝑋) ∈ 𝑉)
253	165, 166, 167, 245, 178, 179	funcf2 17138	. . . . . 6 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩):(⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×_c 𝑂))⟨𝐺, 𝑃⟩)⟶(((1^st ‘𝐸)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝐸)‘⟨𝐺, 𝑃⟩)))
254		df-ov 7159	. . . . . . . . . 10 ⊢ (𝐹(1^st ‘𝐸)𝑋) = ((1^st ‘𝐸)‘⟨𝐹, 𝑋⟩)
255		df-ov 7159	. . . . . . . . . 10 ⊢ (𝐺(1^st ‘𝐸)𝑃) = ((1^st ‘𝐸)‘⟨𝐺, 𝑃⟩)
256	254, 255	oveq12i 7168	. . . . . . . . 9 ⊢ ((𝐹(1^st ‘𝐸)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝐸)𝑃)) = (((1^st ‘𝐸)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝐸)‘⟨𝐺, 𝑃⟩))
257	256	eqcomi 2830	. . . . . . . 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 6509	. . . . . 6 ⊢ (𝜑 → ((⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩):(⟨𝐹, 𝑋⟩(Hom ‘(𝑄 ×_c 𝑂))⟨𝐺, 𝑃⟩)⟶(((1^st ‘𝐸)‘⟨𝐹, 𝑋⟩)(Hom ‘𝑇)((1^st ‘𝐸)‘⟨𝐺, 𝑃⟩)) ↔ (⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩):((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))⟶((𝐹(1^st ‘𝐸)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝐸)𝑃))))
260	253, 259	mpbid 234	. . . . 5 ⊢ (𝜑 → (⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩):((𝐹(𝑂 Nat 𝑆)𝐺) × (𝑃(Hom ‘𝐶)𝑋))⟶((𝐹(1^st ‘𝐸)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝐸)𝑃)))
261	260, 34, 30	fovrnd 7320	. . . 4 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) ∈ ((𝐹(1^st ‘𝐸)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝐸)𝑃)))
262	169, 19, 167, 252, 248	elsetchom 17341	. . . 4 ⊢ (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) ∈ ((𝐹(1^st ‘𝐸)𝑋)(Hom ‘𝑇)(𝐺(1^st ‘𝐸)𝑃)) ↔ (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾):(𝐹(1^st ‘𝐸)𝑋)⟶(𝐺(1^st ‘𝐸)𝑃)))
263	261, 262	mpbid 234	. . 3 ⊢ (𝜑 → (𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾):(𝐹(1^st ‘𝐸)𝑋)⟶(𝐺(1^st ‘𝐸)𝑃))
264	169, 19, 242, 196, 252, 248, 228, 263	setcco 17343	. 2 ⊢ (𝜑 → ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾)(⟨(𝐹(1^st ‘𝑍)𝑋), (𝐹(1^st ‘𝐸)𝑋)⟩(comp‘𝑇)(𝐺(1^st ‘𝐸)𝑃))(𝐹𝑀𝑋)) = ((𝐴(⟨𝐹, 𝑋⟩(2^nd ‘𝐸)⟨𝐺, 𝑃⟩)𝐾) ∘ (𝐹𝑀𝑋)))
265	241, 250, 264	3eqtr4d 2866	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 398 = wceq 1537 ∈ wcel 2114 ∀wral 3138 Vcvv 3494 ∪ cun 3934 ⊆ wss 3936 ⟨cop 4573 class class class wbr 5066 ↦ cmpt 5146 × cxp 5553 ran crn 5556 ∘ ccom 5559 Rel wrel 5560 ⟶wf 6351 ‘cfv 6355 (class class class)co 7156 ∈ cmpo 7158 1^st c1st 7687 2^nd c2nd 7688 tpos ctpos 7891 Basecbs 16483 Hom chom 16576 compcco 16577 Catccat 16935 Idccid 16936 Hom_f chomf 16937 oppCatcoppc 16981 Func cfunc 17124 ∘_func ccofu 17126 Nat cnat 17211 FuncCat cfuc 17212 SetCatcsetc 17335 ×_c cxpc 17418 1^st_F c1stf 17419 2^nd_F c2ndf 17420 ⟨,⟩_F cprf 17421 eval_F cevlf 17459 Hom_Fchof 17498 Yoncyon 17499

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-rep 5190 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 ax-cnex 10593 ax-resscn 10594 ax-1cn 10595 ax-icn 10596 ax-addcl 10597 ax-addrcl 10598 ax-mulcl 10599 ax-mulrcl 10600 ax-mulcom 10601 ax-addass 10602 ax-mulass 10603 ax-distr 10604 ax-i2m1 10605 ax-1ne0 10606 ax-1rid 10607 ax-rnegex 10608 ax-rrecex 10609 ax-cnre 10610 ax-pre-lttri 10611 ax-pre-lttrn 10612 ax-pre-ltadd 10613 ax-pre-mulgt0 10614

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-fal 1550 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-int 4877 df-iun 4921 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-pred 6148 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-om 7581 df-1st 7689 df-2nd 7690 df-tpos 7892 df-wrecs 7947 df-recs 8008 df-rdg 8046 df-1o 8102 df-oadd 8106 df-er 8289 df-map 8408 df-pm 8409 df-ixp 8462 df-en 8510 df-dom 8511 df-sdom 8512 df-fin 8513 df-pnf 10677 df-mnf 10678 df-xr 10679 df-ltxr 10680 df-le 10681 df-sub 10872 df-neg 10873 df-nn 11639 df-2 11701 df-3 11702 df-4 11703 df-5 11704 df-6 11705 df-7 11706 df-8 11707 df-9 11708 df-n0 11899 df-z 11983 df-dec 12100 df-uz 12245 df-fz 12894 df-struct 16485 df-ndx 16486 df-slot 16487 df-base 16489 df-sets 16490 df-ress 16491 df-hom 16589 df-cco 16590 df-cat 16939 df-cid 16940 df-homf 16941 df-comf 16942 df-oppc 16982 df-ssc 17080 df-resc 17081 df-subc 17082 df-func 17128 df-cofu 17130 df-nat 17213 df-fuc 17214 df-setc 17336 df-xpc 17422 df-1stf 17423 df-2ndf 17424 df-prf 17425 df-evlf 17463 df-curf 17464 df-hof 17500 df-yon 17501

This theorem is referenced by: yonedalem3 17530

W3C validator