Theorem yonedainv 18264

Description: The Yoneda Lemma with explicit inverse. (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	⊢ 𝐻 = (HomF‘𝑄)
yoneda.r	⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)
yoneda.e	⊢ 𝐸 = (𝑂 evalF 𝑆)
yoneda.z	⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))
yoneda.c	⊢ (𝜑 → 𝐶 ∈ Cat)
yoneda.w	⊢ (𝜑 → 𝑉 ∈ 𝑊)
yoneda.u	⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)
yoneda.v	⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
yoneda.m	⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥))))
yonedainv.i	⊢ 𝐼 = (Inv‘𝑅)
yonedainv.n	⊢ 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))))

Assertion

Ref	Expression
yonedainv	⊢ (𝜑 → 𝑀(𝑍𝐼𝐸)𝑁)

Distinct variable groups:   𝑓,𝑎,𝑔,𝑥,𝑦, 1   𝑢,𝑎,𝑔,𝑦,𝐶,𝑓,𝑥   𝐸,𝑎,𝑓,𝑔,𝑢,𝑦   𝐵,𝑎,𝑓,𝑔,𝑢,𝑥,𝑦   𝑁,𝑎   𝑂,𝑎,𝑓,𝑔,𝑢,𝑥,𝑦   𝑆,𝑎,𝑓,𝑔,𝑢,𝑥,𝑦   𝑔,𝑀,𝑢,𝑦   𝑄,𝑎,𝑓,𝑔,𝑢,𝑥   𝑇,𝑓,𝑔,𝑢,𝑦   𝜑,𝑎,𝑓,𝑔,𝑢,𝑥,𝑦   𝑢,𝑅   𝑌,𝑎,𝑓,𝑔,𝑢,𝑥,𝑦   𝑍,𝑎,𝑓,𝑔,𝑢,𝑥,𝑦

Allowed substitution hints:   𝑄(𝑦)   𝑅(𝑥,𝑦,𝑓,𝑔,𝑎)   𝑇(𝑥,𝑎)   𝑈(𝑥,𝑦,𝑢,𝑓,𝑔,𝑎)   1 (𝑢)   𝐸(𝑥)   𝐻(𝑥,𝑦,𝑢,𝑓,𝑔,𝑎)   𝐼(𝑥,𝑦,𝑢,𝑓,𝑔,𝑎)   𝑀(𝑥,𝑓,𝑎)   𝑁(𝑥,𝑦,𝑢,𝑓,𝑔)   𝑉(𝑥,𝑦,𝑢,𝑓,𝑔,𝑎)   𝑊(𝑥,𝑦,𝑢,𝑓,𝑔,𝑎)

Proof of Theorem yonedainv

Dummy variables 𝑏 ℎ 𝑘 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		yoneda.r	. . 3 ⊢ 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)
2		eqid 2727	. . . 4 ⊢ (𝑄 ×c 𝑂) = (𝑄 ×c 𝑂)
3		yoneda.q	. . . . 5 ⊢ 𝑄 = (𝑂 FuncCat 𝑆)
4	3	fucbas 17942	. . . 4 ⊢ (𝑂 Func 𝑆) = (Base‘𝑄)
5		yoneda.o	. . . . 5 ⊢ 𝑂 = (oppCat‘𝐶)
6		yoneda.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐶)
7	5, 6	oppcbas 17690	. . . 4 ⊢ 𝐵 = (Base‘𝑂)
8	2, 4, 7	xpcbas 18160	. . 3 ⊢ ((𝑂 Func 𝑆) × 𝐵) = (Base‘(𝑄 ×c 𝑂))
9		eqid 2727	. . 3 ⊢ ((𝑄 ×c 𝑂) Nat 𝑇) = ((𝑄 ×c 𝑂) Nat 𝑇)
10		yoneda.y	. . . . 5 ⊢ 𝑌 = (Yon‘𝐶)
11		yoneda.1	. . . . 5 ⊢ 1 = (Id‘𝐶)
12		yoneda.s	. . . . 5 ⊢ 𝑆 = (SetCat‘𝑈)
13		yoneda.t	. . . . 5 ⊢ 𝑇 = (SetCat‘𝑉)
14		yoneda.h	. . . . 5 ⊢ 𝐻 = (HomF‘𝑄)
15		yoneda.e	. . . . 5 ⊢ 𝐸 = (𝑂 evalF 𝑆)
16		yoneda.z	. . . . 5 ⊢ 𝑍 = (𝐻 ∘func ((⟨(1st ‘𝑌), tpos (2nd ‘𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))
17		yoneda.c	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ Cat)
18		yoneda.w	. . . . 5 ⊢ (𝜑 → 𝑉 ∈ 𝑊)
19		yoneda.u	. . . . 5 ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)
20		yoneda.v	. . . . 5 ⊢ (𝜑 → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
21	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 17, 18, 19, 20	yonedalem1 18255	. . . 4 ⊢ (𝜑 → (𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)))
22	21	simpld 494	. . 3 ⊢ (𝜑 → 𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇))
23	21	simprd 495	. . 3 ⊢ (𝜑 → 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇))
24		yonedainv.i	. . 3 ⊢ 𝐼 = (Inv‘𝑅)
25		eqid 2727	. . 3 ⊢ (Inv‘𝑇) = (Inv‘𝑇)
26		yoneda.m	. . . 4 ⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥))))
27	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 17, 18, 19, 20, 26	yonedalem3 18263	. . 3 ⊢ (𝜑 → 𝑀 ∈ (𝑍((𝑄 ×c 𝑂) Nat 𝑇)𝐸))
28	17	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → 𝐶 ∈ Cat)
29	18	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → 𝑉 ∈ 𝑊)
30	19	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ran (Homf ‘𝐶) ⊆ 𝑈)
31	20	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
32		simprl 770	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ℎ ∈ (𝑂 Func 𝑆))
33		simprr 772	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → 𝑤 ∈ 𝐵)
34	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33, 26	yonedalem3a 18257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))) ∧ (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤)))
35	34	simprd 495	. . . . . . . . 9 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤))
36	28	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → 𝐶 ∈ Cat)
37	29	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑉 ∈ 𝑊)
38	30	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → ran (Homf ‘𝐶) ⊆ 𝑈)
39	31	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
40		simplrl 776	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → ℎ ∈ (𝑂 Func 𝑆))
41		simplrr 777	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑤 ∈ 𝐵)
42		yonedainv.n	. . . . . . . . . . . 12 ⊢ 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))))
43		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑏 ∈ ((1st ‘ℎ)‘𝑤))
44	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 36, 37, 38, 39, 40, 41, 42, 43	yonedalem4c 18260	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑁𝑤)‘𝑏) ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
45	44	fmpttd 7119	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑏 ∈ ((1st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏)):((1st ‘ℎ)‘𝑤)⟶(((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
46	6	fvexi 6905	. . . . . . . . . . . . . . 15 ⊢ 𝐵 ∈ V
47	46	mptex 7229	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢))) ∈ V
48		eqid 2727	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))) = (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢))))
49	47, 48	fnmpti 6692	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))) Fn ((1st ‘ℎ)‘𝑤)
50		simpl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → 𝑓 = ℎ)
51	50	fveq2d 6895	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → (1st ‘𝑓) = (1st ‘ℎ))
52		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → 𝑥 = 𝑤)
53	51, 52	fveq12d 6898	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → ((1st ‘𝑓)‘𝑥) = ((1st ‘ℎ)‘𝑤))
54		simplr 768	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → 𝑥 = 𝑤)
55	54	oveq2d 7430	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (𝑦(Hom ‘𝐶)𝑥) = (𝑦(Hom ‘𝐶)𝑤))
56		simpll 766	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → 𝑓 = ℎ)
57	56	fveq2d 6895	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (2nd ‘𝑓) = (2nd ‘ℎ))
58		eqidd 2728	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → 𝑦 = 𝑦)
59	57, 54, 58	oveq123d 7435	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (𝑥(2nd ‘𝑓)𝑦) = (𝑤(2nd ‘ℎ)𝑦))
60	59	fveq1d 6893	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → ((𝑥(2nd ‘𝑓)𝑦)‘𝑔) = ((𝑤(2nd ‘ℎ)𝑦)‘𝑔))
61	60	fveq1d 6893	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢) = (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢))
62	55, 61	mpteq12dv 5233	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢)) = (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))
63	62	mpteq2dva 5242	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢))) = (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢))))
64	53, 63	mpteq12dv 5233	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))) = (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))))
65		fvex 6904	. . . . . . . . . . . . . . . . 17 ⊢ ((1st ‘ℎ)‘𝑤) ∈ V
66	65	mptex 7229	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))) ∈ V
67	64, 42, 66	ovmpoa 7570	. . . . . . . . . . . . . . 15 ⊢ ((ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵) → (ℎ𝑁𝑤) = (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))))
68	67	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤) = (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))))
69	68	fneq1d 6641	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑁𝑤) Fn ((1st ‘ℎ)‘𝑤) ↔ (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))) Fn ((1st ‘ℎ)‘𝑤)))
70	49, 69	mpbiri 258	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤) Fn ((1st ‘ℎ)‘𝑤))
71		dffn5 6951	. . . . . . . . . . . 12 ⊢ ((ℎ𝑁𝑤) Fn ((1st ‘ℎ)‘𝑤) ↔ (ℎ𝑁𝑤) = (𝑏 ∈ ((1st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏)))
72	70, 71	sylib 217	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤) = (𝑏 ∈ ((1st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏)))
73	5	oppccat 17695	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat)
74	17, 73	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑂 ∈ Cat)
75	74	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → 𝑂 ∈ Cat)
76	20	unssbd 4184	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 ⊆ 𝑉)
77	18, 76	ssexd 5318	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ∈ V)
78	12	setccat 18065	. . . . . . . . . . . . . 14 ⊢ (𝑈 ∈ V → 𝑆 ∈ Cat)
79	77, 78	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ∈ Cat)
80	79	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → 𝑆 ∈ Cat)
81	15, 75, 80, 7, 32, 33	evlf1 18203	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ(1st ‘𝐸)𝑤) = ((1st ‘ℎ)‘𝑤))
82	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33	yonedalem21 18256	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ(1st ‘𝑍)𝑤) = (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
83	72, 81, 82	feq123d 6705	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑁𝑤):(ℎ(1st ‘𝐸)𝑤)⟶(ℎ(1st ‘𝑍)𝑤) ↔ (𝑏 ∈ ((1st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏)):((1st ‘ℎ)‘𝑤)⟶(((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ)))
84	45, 83	mpbird 257	. . . . . . . . 9 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤):(ℎ(1st ‘𝐸)𝑤)⟶(ℎ(1st ‘𝑍)𝑤))
85		fcompt 7136	. . . . . . . . . . 11 ⊢ (((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤):(ℎ(1st ‘𝐸)𝑤)⟶(ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑀𝑤) ∘ (ℎ𝑁𝑤)) = (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘))))
86	35, 84, 85	syl2anc 583	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤) ∘ (ℎ𝑁𝑤)) = (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘))))
87	81	eleq2d 2814	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↔ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)))
88	87	biimpa 476	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ (ℎ(1st ‘𝐸)𝑤)) → 𝑘 ∈ ((1st ‘ℎ)‘𝑤))
89	28	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → 𝐶 ∈ Cat)
90	29	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑉 ∈ 𝑊)
91	30	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ran (Homf ‘𝐶) ⊆ 𝑈)
92	31	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
93		simplrl 776	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ℎ ∈ (𝑂 Func 𝑆))
94		simplrr 777	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑤 ∈ 𝐵)
95	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 89, 90, 91, 92, 93, 94, 26	yonedalem3a 18257	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑀𝑤) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))) ∧ (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤)))
96	95	simpld 494	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (ℎ𝑀𝑤) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))))
97	96	fveq1d 6893	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘)) = ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘((ℎ𝑁𝑤)‘𝑘)))
98	72, 44	fmpt3d 7120	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤):((1st ‘ℎ)‘𝑤)⟶(((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
99	98	ffvelcdmda 7088	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑁𝑤)‘𝑘) ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
100		fveq1 6890	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ((ℎ𝑁𝑤)‘𝑘) → (𝑎‘𝑤) = (((ℎ𝑁𝑤)‘𝑘)‘𝑤))
101	100	fveq1d 6893	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ((ℎ𝑁𝑤)‘𝑘) → ((𝑎‘𝑤)‘( 1 ‘𝑤)) = ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)))
102		eqid 2727	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))
103		fvex 6904	. . . . . . . . . . . . . . . 16 ⊢ ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)) ∈ V
104	101, 102, 103	fvmpt 6999	. . . . . . . . . . . . . . 15 ⊢ (((ℎ𝑁𝑤)‘𝑘) ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) → ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘((ℎ𝑁𝑤)‘𝑘)) = ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)))
105	99, 104	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘((ℎ𝑁𝑤)‘𝑘)) = ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)))
106		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑘 ∈ ((1st ‘ℎ)‘𝑤))
107		eqid 2727	. . . . . . . . . . . . . . . . 17 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
108	6, 107, 11, 89, 94	catidcl 17653	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ( 1 ‘𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤))
109	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 89, 90, 91, 92, 93, 94, 42, 106, 94, 108	yonedalem4b 18259	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)) = (((𝑤(2nd ‘ℎ)𝑤)‘( 1 ‘𝑤))‘𝑘))
110		eqid 2727	. . . . . . . . . . . . . . . . . 18 ⊢ (Id‘𝑂) = (Id‘𝑂)
111		eqid 2727	. . . . . . . . . . . . . . . . . 18 ⊢ (Id‘𝑆) = (Id‘𝑆)
112		relfunc 17839	. . . . . . . . . . . . . . . . . . 19 ⊢ Rel (𝑂 Func 𝑆)
113		1st2ndbr 8040	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Rel (𝑂 Func 𝑆) ∧ ℎ ∈ (𝑂 Func 𝑆)) → (1st ‘ℎ)(𝑂 Func 𝑆)(2nd ‘ℎ))
114	112, 93, 113	sylancr 586	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (1st ‘ℎ)(𝑂 Func 𝑆)(2nd ‘ℎ))
115	7, 110, 111, 114, 94	funcid 17847	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((𝑤(2nd ‘ℎ)𝑤)‘((Id‘𝑂)‘𝑤)) = ((Id‘𝑆)‘((1st ‘ℎ)‘𝑤)))
116	5, 11	oppcid 17694	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐶 ∈ Cat → (Id‘𝑂) = 1 )
117	89, 116	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (Id‘𝑂) = 1 )
118	117	fveq1d 6893	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((Id‘𝑂)‘𝑤) = ( 1 ‘𝑤))
119	118	fveq2d 6895	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((𝑤(2nd ‘ℎ)𝑤)‘((Id‘𝑂)‘𝑤)) = ((𝑤(2nd ‘ℎ)𝑤)‘( 1 ‘𝑤)))
120	77	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑈 ∈ V)
121		eqid 2727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Base‘𝑆) = (Base‘𝑆)
122	7, 121, 114	funcf1 17843	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (1st ‘ℎ):𝐵⟶(Base‘𝑆))
123	12, 120	setcbas 18058	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑈 = (Base‘𝑆))
124	123	feq3d 6703	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((1st ‘ℎ):𝐵⟶𝑈 ↔ (1st ‘ℎ):𝐵⟶(Base‘𝑆)))
125	122, 124	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (1st ‘ℎ):𝐵⟶𝑈)
126	125, 94	ffvelcdmd 7089	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((1st ‘ℎ)‘𝑤) ∈ 𝑈)
127	12, 111, 120, 126	setcid 18066	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((Id‘𝑆)‘((1st ‘ℎ)‘𝑤)) = ( I ↾ ((1st ‘ℎ)‘𝑤)))
128	115, 119, 127	3eqtr3d 2775	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((𝑤(2nd ‘ℎ)𝑤)‘( 1 ‘𝑤)) = ( I ↾ ((1st ‘ℎ)‘𝑤)))
129	128	fveq1d 6893	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (((𝑤(2nd ‘ℎ)𝑤)‘( 1 ‘𝑤))‘𝑘) = (( I ↾ ((1st ‘ℎ)‘𝑤))‘𝑘))
130		fvresi 7176	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ((1st ‘ℎ)‘𝑤) → (( I ↾ ((1st ‘ℎ)‘𝑤))‘𝑘) = 𝑘)
131	130	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (( I ↾ ((1st ‘ℎ)‘𝑤))‘𝑘) = 𝑘)
132	109, 129, 131	3eqtrd 2771	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)) = 𝑘)
133	97, 105, 132	3eqtrd 2771	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘)) = 𝑘)
134	88, 133	syldan 590	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ (ℎ(1st ‘𝐸)𝑤)) → ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘)) = 𝑘)
135	134	mpteq2dva 5242	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘))) = (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ 𝑘))
136		mptresid 6048	. . . . . . . . . . 11 ⊢ ( I ↾ (ℎ(1st ‘𝐸)𝑤)) = (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ 𝑘)
137	135, 136	eqtr4di 2785	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘))) = ( I ↾ (ℎ(1st ‘𝐸)𝑤)))
138	86, 137	eqtrd 2767	. . . . . . . . 9 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤) ∘ (ℎ𝑁𝑤)) = ( I ↾ (ℎ(1st ‘𝐸)𝑤)))
139		fcompt 7136	. . . . . . . . . . 11 ⊢ (((ℎ𝑁𝑤):(ℎ(1st ‘𝐸)𝑤)⟶(ℎ(1st ‘𝑍)𝑤) ∧ (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤)) → ((ℎ𝑁𝑤) ∘ (ℎ𝑀𝑤)) = (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))))
140	84, 35, 139	syl2anc 583	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑁𝑤) ∘ (ℎ𝑀𝑤)) = (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))))
141		eqid 2727	. . . . . . . . . . . . . 14 ⊢ (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆)
142	28	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝐶 ∈ Cat)
143	29	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑉 ∈ 𝑊)
144	30	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ran (Homf ‘𝐶) ⊆ 𝑈)
145	31	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
146		simplrl 776	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ℎ ∈ (𝑂 Func 𝑆))
147		simplrr 777	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑤 ∈ 𝐵)
148	81	feq3d 6703	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤) ↔ (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶((1st ‘ℎ)‘𝑤)))
149	35, 148	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶((1st ‘ℎ)‘𝑤))
150	149	ffvelcdmda 7088	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑀𝑤)‘𝑏) ∈ ((1st ‘ℎ)‘𝑤))
151	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 142, 143, 144, 145, 146, 147, 42, 150	yonedalem4c 18260	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
152	141, 151	nat1st2nd 17932	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) ∈ (⟨(1st ‘((1st ‘𝑌)‘𝑤)), (2nd ‘((1st ‘𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st ‘ℎ), (2nd ‘ℎ)⟩))
153	141, 152, 7	natfn 17935	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) Fn 𝐵)
154	82	eleq2d 2814	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↔ 𝑏 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ)))
155	154	biimpa 476	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑏 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
156	141, 155	nat1st2nd 17932	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑏 ∈ (⟨(1st ‘((1st ‘𝑌)‘𝑤)), (2nd ‘((1st ‘𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st ‘ℎ), (2nd ‘ℎ)⟩))
157	141, 156, 7	natfn 17935	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑏 Fn 𝐵)
158	142	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → 𝐶 ∈ Cat)
159	147	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → 𝑤 ∈ 𝐵)
160		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵)
161	10, 6, 158, 159, 107, 160	yon11 18247	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) = (𝑧(Hom ‘𝐶)𝑤))
162	161	eleq2d 2814	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑘 ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) ↔ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))
163	162	biimpa 476	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)) → 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤))
164	158	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝐶 ∈ Cat)
165	143	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑉 ∈ 𝑊)
166	144	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ran (Homf ‘𝐶) ⊆ 𝑈)
167	145	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
168	146	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ℎ ∈ (𝑂 Func 𝑆))
169	159	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑤 ∈ 𝐵)
170	150	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ𝑀𝑤)‘𝑏) ∈ ((1st ‘ℎ)‘𝑤))
171		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑧 ∈ 𝐵)
172		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤))
173	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 164, 165, 166, 167, 168, 169, 42, 170, 171, 172	yonedalem4b 18259	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((ℎ𝑀𝑤)‘𝑏)))
174	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 164, 165, 166, 167, 168, 169, 26	yonedalem3a 18257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ𝑀𝑤) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))) ∧ (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤)))
175	174	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ℎ𝑀𝑤) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))))
176	175	fveq1d 6893	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ𝑀𝑤)‘𝑏) = ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘𝑏))
177	155	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑏 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
178		fveq1 6890	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑏 → (𝑎‘𝑤) = (𝑏‘𝑤))
179	178	fveq1d 6893	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑏 → ((𝑎‘𝑤)‘( 1 ‘𝑤)) = ((𝑏‘𝑤)‘( 1 ‘𝑤)))
180		fvex 6904	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏‘𝑤)‘( 1 ‘𝑤)) ∈ V
181	179, 102, 180	fvmpt 6999	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) → ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘𝑏) = ((𝑏‘𝑤)‘( 1 ‘𝑤)))
182	177, 181	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘𝑏) = ((𝑏‘𝑤)‘( 1 ‘𝑤)))
183	176, 182	eqtrd 2767	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ𝑀𝑤)‘𝑏) = ((𝑏‘𝑤)‘( 1 ‘𝑤)))
184	183	fveq2d 6895	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((ℎ𝑀𝑤)‘𝑏)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))))
185	156	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑏 ∈ (⟨(1st ‘((1st ‘𝑌)‘𝑤)), (2nd ‘((1st ‘𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st ‘ℎ), (2nd ‘ℎ)⟩))
186		eqid 2727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Hom ‘𝑂) = (Hom ‘𝑂)
187		eqid 2727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (comp‘𝑆) = (comp‘𝑆)
188	107, 5	oppchom 17687	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤(Hom ‘𝑂)𝑧) = (𝑧(Hom ‘𝐶)𝑤)
189	172, 188	eleqtrrdi 2839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑘 ∈ (𝑤(Hom ‘𝑂)𝑧))
190	141, 185, 7, 186, 187, 169, 171, 189	nati 17936	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧)(⟨((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤), ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)⟩(comp‘𝑆)((1st ‘ℎ)‘𝑧))((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)(⟨((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤), ((1st ‘ℎ)‘𝑤)⟩(comp‘𝑆)((1st ‘ℎ)‘𝑧))(𝑏‘𝑤)))
191	77	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑈 ∈ V)
192	191	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → 𝑈 ∈ V)
193	192	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑈 ∈ V)
194		relfunc 17839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ Rel (𝐶 Func 𝑄)
195	10, 17, 5, 12, 3, 77, 19	yoncl 18245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → 𝑌 ∈ (𝐶 Func 𝑄))
196		1st2ndbr 8040	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((Rel (𝐶 Func 𝑄) ∧ 𝑌 ∈ (𝐶 Func 𝑄)) → (1st ‘𝑌)(𝐶 Func 𝑄)(2nd ‘𝑌))
197	194, 195, 196	sylancr 586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (1st ‘𝑌)(𝐶 Func 𝑄)(2nd ‘𝑌))
198	6, 4, 197	funcf1 17843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (1st ‘𝑌):𝐵⟶(𝑂 Func 𝑆))
199	198	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘𝑌):𝐵⟶(𝑂 Func 𝑆))
200	199, 147	ffvelcdmd 7089	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘𝑌)‘𝑤) ∈ (𝑂 Func 𝑆))
201		1st2ndbr 8040	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Rel (𝑂 Func 𝑆) ∧ ((1st ‘𝑌)‘𝑤) ∈ (𝑂 Func 𝑆)) → (1st ‘((1st ‘𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st ‘𝑌)‘𝑤)))
202	112, 200, 201	sylancr 586	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘((1st ‘𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st ‘𝑌)‘𝑤)))
203	7, 121, 202	funcf1 17843	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘((1st ‘𝑌)‘𝑤)):𝐵⟶(Base‘𝑆))
204	12, 191	setcbas 18058	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑈 = (Base‘𝑆))
205	204	feq3d 6703	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘((1st ‘𝑌)‘𝑤)):𝐵⟶𝑈 ↔ (1st ‘((1st ‘𝑌)‘𝑤)):𝐵⟶(Base‘𝑆)))
206	203, 205	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘((1st ‘𝑌)‘𝑤)):𝐵⟶𝑈)
207	206, 147	ffvelcdmd 7089	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤) ∈ 𝑈)
208	207	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤) ∈ 𝑈)
209	206	ffvelcdmda 7088	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) ∈ 𝑈)
210	209	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) ∈ 𝑈)
211	112, 146, 113	sylancr 586	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘ℎ)(𝑂 Func 𝑆)(2nd ‘ℎ))
212	7, 121, 211	funcf1 17843	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘ℎ):𝐵⟶(Base‘𝑆))
213	204	feq3d 6703	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘ℎ):𝐵⟶𝑈 ↔ (1st ‘ℎ):𝐵⟶(Base‘𝑆)))
214	212, 213	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘ℎ):𝐵⟶𝑈)
215	214	ffvelcdmda 7088	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((1st ‘ℎ)‘𝑧) ∈ 𝑈)
216	215	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘ℎ)‘𝑧) ∈ 𝑈)
217		eqid 2727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Hom ‘𝑆) = (Hom ‘𝑆)
218	202	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1st ‘((1st ‘𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st ‘𝑌)‘𝑤)))
219	7, 186, 217, 218, 169, 171	funcf2 17845	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧):(𝑤(Hom ‘𝑂)𝑧)⟶(((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)))
220	219, 189	ffvelcdmd 7089	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)))
221	12, 193, 217, 208, 210	elsetchom 18061	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)) ↔ ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)⟶((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)))
222	220, 221	mpbid 231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)⟶((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧))
223	156	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → 𝑏 ∈ (⟨(1st ‘((1st ‘𝑌)‘𝑤)), (2nd ‘((1st ‘𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st ‘ℎ), (2nd ‘ℎ)⟩))
224	141, 223, 7, 217, 160	natcl 17934	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑏‘𝑧) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)))
225	12, 192, 217, 209, 215	elsetchom 18061	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((𝑏‘𝑧) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)) ↔ (𝑏‘𝑧):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)⟶((1st ‘ℎ)‘𝑧)))
226	224, 225	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑏‘𝑧):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)⟶((1st ‘ℎ)‘𝑧))
227	226	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑏‘𝑧):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)⟶((1st ‘ℎ)‘𝑧))
228	12, 193, 187, 208, 210, 216, 222, 227	setcco 18063	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧)(⟨((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤), ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)⟩(comp‘𝑆)((1st ‘ℎ)‘𝑧))((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)) = ((𝑏‘𝑧) ∘ ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)))
229	214, 147	ffvelcdmd 7089	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘ℎ)‘𝑤) ∈ 𝑈)
230	229	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘ℎ)‘𝑤) ∈ 𝑈)
231	141, 156, 7, 217, 147	natcl 17934	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (𝑏‘𝑤) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘ℎ)‘𝑤)))
232	12, 191, 217, 207, 229	elsetchom 18061	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((𝑏‘𝑤) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘ℎ)‘𝑤)) ↔ (𝑏‘𝑤):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)⟶((1st ‘ℎ)‘𝑤)))
233	231, 232	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (𝑏‘𝑤):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)⟶((1st ‘ℎ)‘𝑤))
234	233	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑏‘𝑤):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)⟶((1st ‘ℎ)‘𝑤))
235	112, 168, 113	sylancr 586	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1st ‘ℎ)(𝑂 Func 𝑆)(2nd ‘ℎ))
236	7, 186, 217, 235, 169, 171	funcf2 17845	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑤(2nd ‘ℎ)𝑧):(𝑤(Hom ‘𝑂)𝑧)⟶(((1st ‘ℎ)‘𝑤)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)))
237	236, 189	ffvelcdmd 7089	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∈ (((1st ‘ℎ)‘𝑤)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)))
238	12, 193, 217, 230, 216	elsetchom 18061	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∈ (((1st ‘ℎ)‘𝑤)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)) ↔ ((𝑤(2nd ‘ℎ)𝑧)‘𝑘):((1st ‘ℎ)‘𝑤)⟶((1st ‘ℎ)‘𝑧)))
239	237, 238	mpbid 231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘ℎ)𝑧)‘𝑘):((1st ‘ℎ)‘𝑤)⟶((1st ‘ℎ)‘𝑧))
240	12, 193, 187, 208, 230, 216, 234, 239	setcco 18063	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)(⟨((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤), ((1st ‘ℎ)‘𝑤)⟩(comp‘𝑆)((1st ‘ℎ)‘𝑧))(𝑏‘𝑤)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤)))
241	190, 228, 240	3eqtr3d 2775	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧) ∘ ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤)))
242	241	fveq1d 6893	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑏‘𝑧) ∘ ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘))‘( 1 ‘𝑤)) = ((((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤))‘( 1 ‘𝑤)))
243	6, 107, 11, 142, 147	catidcl 17653	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ( 1 ‘𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤))
244	10, 6, 142, 147, 107, 147	yon11 18247	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤) = (𝑤(Hom ‘𝐶)𝑤))
245	243, 244	eleqtrrd 2831	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ( 1 ‘𝑤) ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤))
246	245	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ( 1 ‘𝑤) ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤))
247	222, 246	fvco3d 6992	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑏‘𝑧) ∘ ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘))‘( 1 ‘𝑤)) = ((𝑏‘𝑧)‘(((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤))))
248	233, 245	fvco3d 6992	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤))‘( 1 ‘𝑤)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))))
249	248	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤))‘( 1 ‘𝑤)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))))
250	242, 247, 249	3eqtr3d 2775	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧)‘(((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤))) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))))
251		eqid 2727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (comp‘𝐶) = (comp‘𝐶)
252	243	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ( 1 ‘𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤))
253	10, 6, 164, 169, 107, 169, 251, 171, 172, 252	yon12 18248	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤)) = (( 1 ‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐶)𝑤)𝑘))
254	6, 107, 11, 164, 171, 251, 169, 172	catlid 17654	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (( 1 ‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐶)𝑤)𝑘) = 𝑘)
255	253, 254	eqtrd 2767	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤)) = 𝑘)
256	255	fveq2d 6895	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧)‘(((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤))) = ((𝑏‘𝑧)‘𝑘))
257	250, 256	eqtr3d 2769	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))) = ((𝑏‘𝑧)‘𝑘))
258	173, 184, 257	3eqtrd 2771	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = ((𝑏‘𝑧)‘𝑘))
259	163, 258	syldan 590	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)) → ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = ((𝑏‘𝑧)‘𝑘))
260	259	mpteq2dva 5242	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑘 ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) ↦ ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘)) = (𝑘 ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) ↦ ((𝑏‘𝑧)‘𝑘)))
261	152	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) ∈ (⟨(1st ‘((1st ‘𝑌)‘𝑤)), (2nd ‘((1st ‘𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st ‘ℎ), (2nd ‘ℎ)⟩))
262	141, 261, 7, 217, 160	natcl 17934	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)))
263	12, 192, 217, 209, 215	elsetchom 18061	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)) ↔ (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)⟶((1st ‘ℎ)‘𝑧)))
264	262, 263	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)⟶((1st ‘ℎ)‘𝑧))
265	264	feqmptd 6961	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧) = (𝑘 ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) ↦ ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘)))
266	226	feqmptd 6961	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑏‘𝑧) = (𝑘 ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) ↦ ((𝑏‘𝑧)‘𝑘)))
267	260, 265, 266	3eqtr4d 2777	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧) = (𝑏‘𝑧))
268	153, 157, 267	eqfnfvd 7037	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) = 𝑏)
269	268	mpteq2dva 5242	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))) = (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ 𝑏))
270		mptresid 6048	. . . . . . . . . . 11 ⊢ ( I ↾ (ℎ(1st ‘𝑍)𝑤)) = (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ 𝑏)
271	269, 270	eqtr4di 2785	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))) = ( I ↾ (ℎ(1st ‘𝑍)𝑤)))
272	140, 271	eqtrd 2767	. . . . . . . . 9 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑁𝑤) ∘ (ℎ𝑀𝑤)) = ( I ↾ (ℎ(1st ‘𝑍)𝑤)))
273		fcof1o 7299	. . . . . . . . 9 ⊢ ((((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤):(ℎ(1st ‘𝐸)𝑤)⟶(ℎ(1st ‘𝑍)𝑤)) ∧ (((ℎ𝑀𝑤) ∘ (ℎ𝑁𝑤)) = ( I ↾ (ℎ(1st ‘𝐸)𝑤)) ∧ ((ℎ𝑁𝑤) ∘ (ℎ𝑀𝑤)) = ( I ↾ (ℎ(1st ‘𝑍)𝑤)))) → ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ ◡(ℎ𝑀𝑤) = (ℎ𝑁𝑤)))
274	35, 84, 138, 272, 273	syl22anc 838	. . . . . . . 8 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ ◡(ℎ𝑀𝑤) = (ℎ𝑁𝑤)))
275		eqcom 2734	. . . . . . . . 9 ⊢ (◡(ℎ𝑀𝑤) = (ℎ𝑁𝑤) ↔ (ℎ𝑁𝑤) = ◡(ℎ𝑀𝑤))
276	275	anbi2i 622	. . . . . . . 8 ⊢ (((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ ◡(ℎ𝑀𝑤) = (ℎ𝑁𝑤)) ↔ ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤) = ◡(ℎ𝑀𝑤)))
277	274, 276	sylib 217	. . . . . . 7 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤) = ◡(ℎ𝑀𝑤)))
278		eqid 2727	. . . . . . . . . . 11 ⊢ (Base‘𝑇) = (Base‘𝑇)
279		relfunc 17839	. . . . . . . . . . . 12 ⊢ Rel ((𝑄 ×c 𝑂) Func 𝑇)
280		1st2ndbr 8040	. . . . . . . . . . . 12 ⊢ ((Rel ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st ‘𝑍)((𝑄 ×c 𝑂) Func 𝑇)(2nd ‘𝑍))
281	279, 22, 280	sylancr 586	. . . . . . . . . . 11 ⊢ (𝜑 → (1st ‘𝑍)((𝑄 ×c 𝑂) Func 𝑇)(2nd ‘𝑍))
282	8, 278, 281	funcf1 17843	. . . . . . . . . 10 ⊢ (𝜑 → (1st ‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
283	13, 18	setcbas 18058	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 = (Base‘𝑇))
284	283	feq3d 6703	. . . . . . . . . 10 ⊢ (𝜑 → ((1st ‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶𝑉 ↔ (1st ‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇)))
285	282, 284	mpbird 257	. . . . . . . . 9 ⊢ (𝜑 → (1st ‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶𝑉)
286	285	fovcdmda 7586	. . . . . . . 8 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ(1st ‘𝑍)𝑤) ∈ 𝑉)
287		1st2ndbr 8040	. . . . . . . . . . . 12 ⊢ ((Rel ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st ‘𝐸)((𝑄 ×c 𝑂) Func 𝑇)(2nd ‘𝐸))
288	279, 23, 287	sylancr 586	. . . . . . . . . . 11 ⊢ (𝜑 → (1st ‘𝐸)((𝑄 ×c 𝑂) Func 𝑇)(2nd ‘𝐸))
289	8, 278, 288	funcf1 17843	. . . . . . . . . 10 ⊢ (𝜑 → (1st ‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
290	283	feq3d 6703	. . . . . . . . . 10 ⊢ (𝜑 → ((1st ‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶𝑉 ↔ (1st ‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇)))
291	289, 290	mpbird 257	. . . . . . . . 9 ⊢ (𝜑 → (1st ‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶𝑉)
292	291	fovcdmda 7586	. . . . . . . 8 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ(1st ‘𝐸)𝑤) ∈ 𝑉)
293	13, 29, 286, 292, 25	setcinv 18070	. . . . . . 7 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤)((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤))(ℎ𝑁𝑤) ↔ ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤) = ◡(ℎ𝑀𝑤))))
294	277, 293	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑀𝑤)((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤))(ℎ𝑁𝑤))
295	294	ralrimivva 3195	. . . . 5 ⊢ (𝜑 → ∀ℎ ∈ (𝑂 Func 𝑆)∀𝑤 ∈ 𝐵 (ℎ𝑀𝑤)((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤))(ℎ𝑁𝑤))
296		fveq2 6891	. . . . . . . 8 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → (𝑀‘𝑧) = (𝑀‘⟨ℎ, 𝑤⟩))
297		df-ov 7417	. . . . . . . 8 ⊢ (ℎ𝑀𝑤) = (𝑀‘⟨ℎ, 𝑤⟩)
298	296, 297	eqtr4di 2785	. . . . . . 7 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → (𝑀‘𝑧) = (ℎ𝑀𝑤))
299		fveq2 6891	. . . . . . . . 9 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → ((1st ‘𝑍)‘𝑧) = ((1st ‘𝑍)‘⟨ℎ, 𝑤⟩))
300		df-ov 7417	. . . . . . . . 9 ⊢ (ℎ(1st ‘𝑍)𝑤) = ((1st ‘𝑍)‘⟨ℎ, 𝑤⟩)
301	299, 300	eqtr4di 2785	. . . . . . . 8 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → ((1st ‘𝑍)‘𝑧) = (ℎ(1st ‘𝑍)𝑤))
302		fveq2 6891	. . . . . . . . 9 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → ((1st ‘𝐸)‘𝑧) = ((1st ‘𝐸)‘⟨ℎ, 𝑤⟩))
303		df-ov 7417	. . . . . . . . 9 ⊢ (ℎ(1st ‘𝐸)𝑤) = ((1st ‘𝐸)‘⟨ℎ, 𝑤⟩)
304	302, 303	eqtr4di 2785	. . . . . . . 8 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → ((1st ‘𝐸)‘𝑧) = (ℎ(1st ‘𝐸)𝑤))
305	301, 304	oveq12d 7432	. . . . . . 7 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → (((1st ‘𝑍)‘𝑧)(Inv‘𝑇)((1st ‘𝐸)‘𝑧)) = ((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤)))
306		fveq2 6891	. . . . . . . 8 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → (𝑁‘𝑧) = (𝑁‘⟨ℎ, 𝑤⟩))
307		df-ov 7417	. . . . . . . 8 ⊢ (ℎ𝑁𝑤) = (𝑁‘⟨ℎ, 𝑤⟩)
308	306, 307	eqtr4di 2785	. . . . . . 7 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → (𝑁‘𝑧) = (ℎ𝑁𝑤))
309	298, 305, 308	breq123d 5156	. . . . . 6 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → ((𝑀‘𝑧)(((1st ‘𝑍)‘𝑧)(Inv‘𝑇)((1st ‘𝐸)‘𝑧))(𝑁‘𝑧) ↔ (ℎ𝑀𝑤)((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤))(ℎ𝑁𝑤)))
310	309	ralxp 5838	. . . . 5 ⊢ (∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑀‘𝑧)(((1st ‘𝑍)‘𝑧)(Inv‘𝑇)((1st ‘𝐸)‘𝑧))(𝑁‘𝑧) ↔ ∀ℎ ∈ (𝑂 Func 𝑆)∀𝑤 ∈ 𝐵 (ℎ𝑀𝑤)((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤))(ℎ𝑁𝑤))
311	295, 310	sylibr 233	. . . 4 ⊢ (𝜑 → ∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑀‘𝑧)(((1st ‘𝑍)‘𝑧)(Inv‘𝑇)((1st ‘𝐸)‘𝑧))(𝑁‘𝑧))
312	311	r19.21bi 3243	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)) → (𝑀‘𝑧)(((1st ‘𝑍)‘𝑧)(Inv‘𝑇)((1st ‘𝐸)‘𝑧))(𝑁‘𝑧))
313	1, 8, 9, 22, 23, 24, 25, 27, 312	invfuc 17957	. 2 ⊢ (𝜑 → 𝑀(𝑍𝐼𝐸)(𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁‘𝑧)))
314		fvex 6904	. . . . 5 ⊢ ((1st ‘𝑓)‘𝑥) ∈ V
315	314	mptex 7229	. . . 4 ⊢ (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))) ∈ V
316	42, 315	fnmpoi 8068	. . 3 ⊢ 𝑁 Fn ((𝑂 Func 𝑆) × 𝐵)
317		dffn5 6951	. . 3 ⊢ (𝑁 Fn ((𝑂 Func 𝑆) × 𝐵) ↔ 𝑁 = (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁‘𝑧)))
318	316, 317	mpbi 229	. 2 ⊢ 𝑁 = (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁‘𝑧))
319	313, 318	breqtrrdi 5184	1 ⊢ (𝜑 → 𝑀(𝑍𝐼𝐸)𝑁)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1534   ∈ wcel 2099  ∀wral 3056  Vcvv 3469   ∪ cun 3942   ⊆ wss 3944  ⟨cop 4630   class class class wbr 5142   ↦ cmpt 5225   I cid 5569   × cxp 5670  ^◡ccnv 5671  ran crn 5673   ↾ cres 5674   ∘ ccom 5676  Rel wrel 5677   Fn wfn 6537  ⟶wf 6538  –1-1-onto→wf1o 6541  ‘cfv 6542  (class class class)co 7414   ∈ cmpo 7416  1^st c1st 7985  2^nd c2nd 7986  tpos ctpos 8224  Basecbs 17171  Hom chom 17235  compcco 17236  Catccat 17635  Idccid 17636  Hom_f chomf 17637  oppCatcoppc 17682  Invcinv 17719   Func cfunc 17831   ∘_func ccofu 17833   Nat cnat 17922   FuncCat cfuc 17923  SetCatcsetc 18055   ×_c cxpc 18150   1^st_F c1stf 18151   2^nd_F c2ndf 18152   ⟨,⟩_F cprf 18153   eval_F cevlf 18192  Hom_Fchof 18231  Yoncyon 18232

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  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 8838  df-pm 8839  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 11468  df-neg 11469  df-nn 12235  df-2 12297  df-3 12298  df-4 12299  df-5 12300  df-6 12301  df-7 12302  df-8 12303  df-9 12304  df-n0 12495  df-z 12581  df-dec 12700  df-uz 12845  df-fz 13509  df-struct 17107  df-sets 17124  df-slot 17142  df-ndx 17154  df-base 17172  df-ress 17201  df-hom 17248  df-cco 17249  df-cat 17639  df-cid 17640  df-homf 17641  df-comf 17642  df-oppc 17683  df-sect 17721  df-inv 17722  df-ssc 17784  df-resc 17785  df-subc 17786  df-func 17835  df-cofu 17837  df-nat 17924  df-fuc 17925  df-setc 18056  df-xpc 18154  df-1stf 18155  df-2ndf 18156  df-prf 18157  df-evlf 18196  df-curf 18197  df-hof 18233  df-yon 18234

This theorem is referenced by:  yonffthlem  18265  yoneda  18266