Theorem yonedainv 18315

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 2764	. . . 4 ⊢ (𝑄 ×c 𝑂) = (𝑄 ×c 𝑂)
3		yoneda.q	. . . . 5 ⊢ 𝑄 = (𝑂 FuncCat 𝑆)
4	3	fucbas 17998	. . . 4 ⊢ (𝑂 Func 𝑆) = (Base‘𝑄)
5		yoneda.o	. . . . 5 ⊢ 𝑂 = (oppCat‘𝐶)
6		yoneda.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐶)
7	5, 6	oppcbas 17752	. . . 4 ⊢ 𝐵 = (Base‘𝑂)
8	2, 4, 7	xpcbas 18212	. . 3 ⊢ ((𝑂 Func 𝑆) × 𝐵) = (Base‘(𝑄 ×c 𝑂))
9		eqid 2764	. . 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 18306	. . . 4 ⊢ (𝜑 → (𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)))
22	21	simpld 498	. . 3 ⊢ (𝜑 → 𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇))
23	21	simprd 499	. . 3 ⊢ (𝜑 → 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇))
24		yonedainv.i	. . 3 ⊢ 𝐼 = (Inv‘𝑅)
25		eqid 2764	. . 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 18314	. . 3 ⊢ (𝜑 → 𝑀 ∈ (𝑍((𝑄 ×c 𝑂) Nat 𝑇)𝐸))
28	17	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → 𝐶 ∈ Cat)
29	18	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → 𝑉 ∈ 𝑊)
30	19	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ran (Homf ‘𝐶) ⊆ 𝑈)
31	20	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
32		simprl 780	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ℎ ∈ (𝑂 Func 𝑆))
33		simprr 782	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → 𝑤 ∈ 𝐵)
34	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33, 26	yonedalem3a 18308	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))) ∧ (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤)))
35	34	simprd 499	. . . . . . . . 9 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤))
36	28	adantr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → 𝐶 ∈ Cat)
37	29	adantr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑉 ∈ 𝑊)
38	30	adantr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → ran (Homf ‘𝐶) ⊆ 𝑈)
39	31	adantr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
40		simplrl 786	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → ℎ ∈ (𝑂 Func 𝑆))
41		simplrr 787	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑤 ∈ 𝐵)
42		yonedainv.n	. . . . . . . . . . . 12 ⊢ 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))))
43		simpr 488	. . . . . . . . . . . 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 18311	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑁𝑤)‘𝑏) ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
45	44	fmpttd 7098	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑏 ∈ ((1st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏)):((1st ‘ℎ)‘𝑤)⟶(((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
46	6	fvexi 6883	. . . . . . . . . . . . . . 15 ⊢ 𝐵 ∈ V
47	46	mptex 7209	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢))) ∈ V
48		eqid 2764	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))) = (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢))))
49	47, 48	fnmpti 6666	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))) Fn ((1st ‘ℎ)‘𝑤)
50		simpl 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → 𝑓 = ℎ)
51	50	fveq2d 6873	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → (1st ‘𝑓) = (1st ‘ℎ))
52		simpr 488	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → 𝑥 = 𝑤)
53	51, 52	fveq12d 6876	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → ((1st ‘𝑓)‘𝑥) = ((1st ‘ℎ)‘𝑤))
54		simplr 778	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → 𝑥 = 𝑤)
55	54	oveq2d 7414	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (𝑦(Hom ‘𝐶)𝑥) = (𝑦(Hom ‘𝐶)𝑤))
56		simpll 776	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → 𝑓 = ℎ)
57	56	fveq2d 6873	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (2nd ‘𝑓) = (2nd ‘ℎ))
58		eqidd 2765	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → 𝑦 = 𝑦)
59	57, 54, 58	oveq123d 7419	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (𝑥(2nd ‘𝑓)𝑦) = (𝑤(2nd ‘ℎ)𝑦))
60	59	fveq1d 6871	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → ((𝑥(2nd ‘𝑓)𝑦)‘𝑔) = ((𝑤(2nd ‘ℎ)𝑦)‘𝑔))
61	60	fveq1d 6871	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢) = (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢))
62	55, 61	mpteq12dv 5189	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢)) = (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))
63	62	mpteq2dva 5195	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢))) = (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢))))
64	53, 63	mpteq12dv 5189	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))) = (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))))
65		fvex 6882	. . . . . . . . . . . . . . . . 17 ⊢ ((1st ‘ℎ)‘𝑤) ∈ V
66	65	mptex 7209	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))) ∈ V
67	64, 42, 66	ovmpoa 7553	. . . . . . . . . . . . . . 15 ⊢ ((ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵) → (ℎ𝑁𝑤) = (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))))
68	67	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤) = (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))))
69	68	fneq1d 6616	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑁𝑤) Fn ((1st ‘ℎ)‘𝑤) ↔ (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))) Fn ((1st ‘ℎ)‘𝑤)))
70	49, 69	mpbiri 260	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤) Fn ((1st ‘ℎ)‘𝑤))
71		dffn5 6927	. . . . . . . . . . . 12 ⊢ ((ℎ𝑁𝑤) Fn ((1st ‘ℎ)‘𝑤) ↔ (ℎ𝑁𝑤) = (𝑏 ∈ ((1st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏)))
72	70, 71	sylib 220	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤) = (𝑏 ∈ ((1st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏)))
73	5	oppccat 17756	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat)
74	17, 73	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑂 ∈ Cat)
75	74	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → 𝑂 ∈ Cat)
76	20	unssbd 4148	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 ⊆ 𝑉)
77	18, 76	ssexd 5282	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ∈ V)
78	12	setccat 18120	. . . . . . . . . . . . . 14 ⊢ (𝑈 ∈ V → 𝑆 ∈ Cat)
79	77, 78	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ∈ Cat)
80	79	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → 𝑆 ∈ Cat)
81	15, 75, 80, 7, 32, 33	evlf1 18254	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ(1st ‘𝐸)𝑤) = ((1st ‘ℎ)‘𝑤))
82	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33	yonedalem21 18307	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ(1st ‘𝑍)𝑤) = (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
83	72, 81, 82	feq123d 6682	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑁𝑤):(ℎ(1st ‘𝐸)𝑤)⟶(ℎ(1st ‘𝑍)𝑤) ↔ (𝑏 ∈ ((1st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏)):((1st ‘ℎ)‘𝑤)⟶(((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ)))
84	45, 83	mpbird 259	. . . . . . . . 9 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤):(ℎ(1st ‘𝐸)𝑤)⟶(ℎ(1st ‘𝑍)𝑤))
85		fcompt 7117	. . . . . . . . . . 11 ⊢ (((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤):(ℎ(1st ‘𝐸)𝑤)⟶(ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑀𝑤) ∘ (ℎ𝑁𝑤)) = (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘))))
86	35, 84, 85	syl2anc 593	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤) ∘ (ℎ𝑁𝑤)) = (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘))))
87	81	eleq2d 2850	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↔ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)))
88	87	biimpa 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ (ℎ(1st ‘𝐸)𝑤)) → 𝑘 ∈ ((1st ‘ℎ)‘𝑤))
89	28	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → 𝐶 ∈ Cat)
90	29	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑉 ∈ 𝑊)
91	30	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ran (Homf ‘𝐶) ⊆ 𝑈)
92	31	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
93		simplrl 786	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ℎ ∈ (𝑂 Func 𝑆))
94		simplrr 787	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑤 ∈ 𝐵)
95	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 89, 90, 91, 92, 93, 94, 26	yonedalem3a 18308	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑀𝑤) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))) ∧ (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤)))
96	95	simpld 498	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (ℎ𝑀𝑤) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))))
97	96	fveq1d 6871	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘)) = ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘((ℎ𝑁𝑤)‘𝑘)))
98	72, 44	fmpt3d 7099	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤):((1st ‘ℎ)‘𝑤)⟶(((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
99	98	ffvelcdmda 7067	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑁𝑤)‘𝑘) ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
100		fveq1 6868	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ((ℎ𝑁𝑤)‘𝑘) → (𝑎‘𝑤) = (((ℎ𝑁𝑤)‘𝑘)‘𝑤))
101	100	fveq1d 6871	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ((ℎ𝑁𝑤)‘𝑘) → ((𝑎‘𝑤)‘( 1 ‘𝑤)) = ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)))
102		eqid 2764	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))
103		fvex 6882	. . . . . . . . . . . . . . . 16 ⊢ ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)) ∈ V
104	101, 102, 103	fvmpt 6977	. . . . . . . . . . . . . . 15 ⊢ (((ℎ𝑁𝑤)‘𝑘) ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) → ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘((ℎ𝑁𝑤)‘𝑘)) = ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)))
105	99, 104	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘((ℎ𝑁𝑤)‘𝑘)) = ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)))
106		simpr 488	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑘 ∈ ((1st ‘ℎ)‘𝑤))
107		eqid 2764	. . . . . . . . . . . . . . . . 17 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
108	6, 107, 11, 89, 94	catidcl 17716	. . . . . . . . . . . . . . . 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 18310	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)) = (((𝑤(2nd ‘ℎ)𝑤)‘( 1 ‘𝑤))‘𝑘))
110		eqid 2764	. . . . . . . . . . . . . . . . . 18 ⊢ (Id‘𝑂) = (Id‘𝑂)
111		eqid 2764	. . . . . . . . . . . . . . . . . 18 ⊢ (Id‘𝑆) = (Id‘𝑆)
112		relfunc 17897	. . . . . . . . . . . . . . . . . . 19 ⊢ Rel (𝑂 Func 𝑆)
113		1st2ndbr 8025	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Rel (𝑂 Func 𝑆) ∧ ℎ ∈ (𝑂 Func 𝑆)) → (1st ‘ℎ)(𝑂 Func 𝑆)(2nd ‘ℎ))
114	112, 93, 113	sylancr 596	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (1st ‘ℎ)(𝑂 Func 𝑆)(2nd ‘ℎ))
115	7, 110, 111, 114, 94	funcid 17905	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((𝑤(2nd ‘ℎ)𝑤)‘((Id‘𝑂)‘𝑤)) = ((Id‘𝑆)‘((1st ‘ℎ)‘𝑤)))
116	5, 11	oppcid 17755	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐶 ∈ Cat → (Id‘𝑂) = 1 )
117	89, 116	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (Id‘𝑂) = 1 )
118	117	fveq1d 6871	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((Id‘𝑂)‘𝑤) = ( 1 ‘𝑤))
119	118	fveq2d 6873	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((𝑤(2nd ‘ℎ)𝑤)‘((Id‘𝑂)‘𝑤)) = ((𝑤(2nd ‘ℎ)𝑤)‘( 1 ‘𝑤)))
120	77	ad2antrr 736	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑈 ∈ V)
121		eqid 2764	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Base‘𝑆) = (Base‘𝑆)
122	7, 121, 114	funcf1 17901	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (1st ‘ℎ):𝐵⟶(Base‘𝑆))
123	12, 120	setcbas 18113	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑈 = (Base‘𝑆))
124	123	feq3d 6678	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((1st ‘ℎ):𝐵⟶𝑈 ↔ (1st ‘ℎ):𝐵⟶(Base‘𝑆)))
125	122, 124	mpbird 259	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (1st ‘ℎ):𝐵⟶𝑈)
126	125, 94	ffvelcdmd 7068	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((1st ‘ℎ)‘𝑤) ∈ 𝑈)
127	12, 111, 120, 126	setcid 18121	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((Id‘𝑆)‘((1st ‘ℎ)‘𝑤)) = ( I ↾ ((1st ‘ℎ)‘𝑤)))
128	115, 119, 127	3eqtr3d 2807	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((𝑤(2nd ‘ℎ)𝑤)‘( 1 ‘𝑤)) = ( I ↾ ((1st ‘ℎ)‘𝑤)))
129	128	fveq1d 6871	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (((𝑤(2nd ‘ℎ)𝑤)‘( 1 ‘𝑤))‘𝑘) = (( I ↾ ((1st ‘ℎ)‘𝑤))‘𝑘))
130		fvresi 7159	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ((1st ‘ℎ)‘𝑤) → (( I ↾ ((1st ‘ℎ)‘𝑤))‘𝑘) = 𝑘)
131	130	adantl 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (( I ↾ ((1st ‘ℎ)‘𝑤))‘𝑘) = 𝑘)
132	109, 129, 131	3eqtrd 2803	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)) = 𝑘)
133	97, 105, 132	3eqtrd 2803	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘)) = 𝑘)
134	88, 133	syldan 600	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ (ℎ(1st ‘𝐸)𝑤)) → ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘)) = 𝑘)
135	134	mpteq2dva 5195	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘))) = (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ 𝑘))
136		mptresid 6042	. . . . . . . . . . 11 ⊢ ( I ↾ (ℎ(1st ‘𝐸)𝑤)) = (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ 𝑘)
137	135, 136	eqtr4di 2817	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘))) = ( I ↾ (ℎ(1st ‘𝐸)𝑤)))
138	86, 137	eqtrd 2799	. . . . . . . . 9 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤) ∘ (ℎ𝑁𝑤)) = ( I ↾ (ℎ(1st ‘𝐸)𝑤)))
139		fcompt 7117	. . . . . . . . . . 11 ⊢ (((ℎ𝑁𝑤):(ℎ(1st ‘𝐸)𝑤)⟶(ℎ(1st ‘𝑍)𝑤) ∧ (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤)) → ((ℎ𝑁𝑤) ∘ (ℎ𝑀𝑤)) = (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))))
140	84, 35, 139	syl2anc 593	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑁𝑤) ∘ (ℎ𝑀𝑤)) = (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))))
141		eqid 2764	. . . . . . . . . . . . . 14 ⊢ (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆)
142	28	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝐶 ∈ Cat)
143	29	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑉 ∈ 𝑊)
144	30	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ran (Homf ‘𝐶) ⊆ 𝑈)
145	31	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
146		simplrl 786	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ℎ ∈ (𝑂 Func 𝑆))
147		simplrr 787	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑤 ∈ 𝐵)
148	81	feq3d 6678	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤) ↔ (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶((1st ‘ℎ)‘𝑤)))
149	35, 148	mpbid 234	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶((1st ‘ℎ)‘𝑤))
150	149	ffvelcdmda 7067	. . . . . . . . . . . . . . . 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 18311	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
152	141, 151	nat1st2nd 17989	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) ∈ (⟨(1st ‘((1st ‘𝑌)‘𝑤)), (2nd ‘((1st ‘𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st ‘ℎ), (2nd ‘ℎ)⟩))
153	141, 152, 7	natfn 17992	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) Fn 𝐵)
154	82	eleq2d 2850	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↔ 𝑏 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ)))
155	154	biimpa 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑏 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
156	141, 155	nat1st2nd 17989	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑏 ∈ (⟨(1st ‘((1st ‘𝑌)‘𝑤)), (2nd ‘((1st ‘𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st ‘ℎ), (2nd ‘ℎ)⟩))
157	141, 156, 7	natfn 17992	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑏 Fn 𝐵)
158	142	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → 𝐶 ∈ Cat)
159	147	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → 𝑤 ∈ 𝐵)
160		simpr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵)
161	10, 6, 158, 159, 107, 160	yon11 18298	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) = (𝑧(Hom ‘𝐶)𝑤))
162	161	eleq2d 2850	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑘 ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) ↔ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))
163	162	biimpa 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)) → 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤))
164	158	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝐶 ∈ Cat)
165	143	ad2antrr 736	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑉 ∈ 𝑊)
166	144	ad2antrr 736	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ran (Homf ‘𝐶) ⊆ 𝑈)
167	145	ad2antrr 736	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
168	146	ad2antrr 736	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ℎ ∈ (𝑂 Func 𝑆))
169	159	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑤 ∈ 𝐵)
170	150	ad2antrr 736	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ𝑀𝑤)‘𝑏) ∈ ((1st ‘ℎ)‘𝑤))
171		simplr 778	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑧 ∈ 𝐵)
172		simpr 488	. . . . . . . . . . . . . . . . . 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 18310	. . . . . . . . . . . . . . . . 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 18308	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ𝑀𝑤) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))) ∧ (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤)))
175	174	simpld 498	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ℎ𝑀𝑤) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))))
176	175	fveq1d 6871	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ𝑀𝑤)‘𝑏) = ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘𝑏))
177	155	ad2antrr 736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑏 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
178		fveq1 6868	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑏 → (𝑎‘𝑤) = (𝑏‘𝑤))
179	178	fveq1d 6871	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑏 → ((𝑎‘𝑤)‘( 1 ‘𝑤)) = ((𝑏‘𝑤)‘( 1 ‘𝑤)))
180		fvex 6882	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏‘𝑤)‘( 1 ‘𝑤)) ∈ V
181	179, 102, 180	fvmpt 6977	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) → ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘𝑏) = ((𝑏‘𝑤)‘( 1 ‘𝑤)))
182	177, 181	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘𝑏) = ((𝑏‘𝑤)‘( 1 ‘𝑤)))
183	176, 182	eqtrd 2799	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ𝑀𝑤)‘𝑏) = ((𝑏‘𝑤)‘( 1 ‘𝑤)))
184	183	fveq2d 6873	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((ℎ𝑀𝑤)‘𝑏)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))))
185	156	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑏 ∈ (⟨(1st ‘((1st ‘𝑌)‘𝑤)), (2nd ‘((1st ‘𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st ‘ℎ), (2nd ‘ℎ)⟩))
186		eqid 2764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Hom ‘𝑂) = (Hom ‘𝑂)
187		eqid 2764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (comp‘𝑆) = (comp‘𝑆)
188	107, 5	oppchom 17749	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤(Hom ‘𝑂)𝑧) = (𝑧(Hom ‘𝐶)𝑤)
189	172, 188	eleqtrrdi 2875	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑘 ∈ (𝑤(Hom ‘𝑂)𝑧))
190	141, 185, 7, 186, 187, 169, 171, 189	nati 17993	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧)(⟨((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤), ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)⟩(comp‘𝑆)((1st ‘ℎ)‘𝑧))((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)(⟨((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤), ((1st ‘ℎ)‘𝑤)⟩(comp‘𝑆)((1st ‘ℎ)‘𝑧))(𝑏‘𝑤)))
191	77	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑈 ∈ V)
192	191	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → 𝑈 ∈ V)
193	192	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑈 ∈ V)
194		relfunc 17897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ Rel (𝐶 Func 𝑄)
195	10, 17, 5, 12, 3, 77, 19	yoncl 18296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → 𝑌 ∈ (𝐶 Func 𝑄))
196		1st2ndbr 8025	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((Rel (𝐶 Func 𝑄) ∧ 𝑌 ∈ (𝐶 Func 𝑄)) → (1st ‘𝑌)(𝐶 Func 𝑄)(2nd ‘𝑌))
197	194, 195, 196	sylancr 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (1st ‘𝑌)(𝐶 Func 𝑄)(2nd ‘𝑌))
198	6, 4, 197	funcf1 17901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (1st ‘𝑌):𝐵⟶(𝑂 Func 𝑆))
199	198	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘𝑌):𝐵⟶(𝑂 Func 𝑆))
200	199, 147	ffvelcdmd 7068	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘𝑌)‘𝑤) ∈ (𝑂 Func 𝑆))
201		1st2ndbr 8025	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Rel (𝑂 Func 𝑆) ∧ ((1st ‘𝑌)‘𝑤) ∈ (𝑂 Func 𝑆)) → (1st ‘((1st ‘𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st ‘𝑌)‘𝑤)))
202	112, 200, 201	sylancr 596	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘((1st ‘𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st ‘𝑌)‘𝑤)))
203	7, 121, 202	funcf1 17901	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘((1st ‘𝑌)‘𝑤)):𝐵⟶(Base‘𝑆))
204	12, 191	setcbas 18113	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑈 = (Base‘𝑆))
205	204	feq3d 6678	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘((1st ‘𝑌)‘𝑤)):𝐵⟶𝑈 ↔ (1st ‘((1st ‘𝑌)‘𝑤)):𝐵⟶(Base‘𝑆)))
206	203, 205	mpbird 259	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘((1st ‘𝑌)‘𝑤)):𝐵⟶𝑈)
207	206, 147	ffvelcdmd 7068	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤) ∈ 𝑈)
208	207	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤) ∈ 𝑈)
209	206	ffvelcdmda 7067	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) ∈ 𝑈)
210	209	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) ∈ 𝑈)
211	112, 146, 113	sylancr 596	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘ℎ)(𝑂 Func 𝑆)(2nd ‘ℎ))
212	7, 121, 211	funcf1 17901	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘ℎ):𝐵⟶(Base‘𝑆))
213	204	feq3d 6678	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘ℎ):𝐵⟶𝑈 ↔ (1st ‘ℎ):𝐵⟶(Base‘𝑆)))
214	212, 213	mpbird 259	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘ℎ):𝐵⟶𝑈)
215	214	ffvelcdmda 7067	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((1st ‘ℎ)‘𝑧) ∈ 𝑈)
216	215	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘ℎ)‘𝑧) ∈ 𝑈)
217		eqid 2764	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Hom ‘𝑆) = (Hom ‘𝑆)
218	202	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1st ‘((1st ‘𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st ‘𝑌)‘𝑤)))
219	7, 186, 217, 218, 169, 171	funcf2 17903	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧):(𝑤(Hom ‘𝑂)𝑧)⟶(((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)))
220	219, 189	ffvelcdmd 7068	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)))
221	12, 193, 217, 208, 210	elsetchom 18116	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)) ↔ ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)⟶((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)))
222	220, 221	mpbid 234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)⟶((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧))
223	156	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → 𝑏 ∈ (⟨(1st ‘((1st ‘𝑌)‘𝑤)), (2nd ‘((1st ‘𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st ‘ℎ), (2nd ‘ℎ)⟩))
224	141, 223, 7, 217, 160	natcl 17991	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑏‘𝑧) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)))
225	12, 192, 217, 209, 215	elsetchom 18116	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((𝑏‘𝑧) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)) ↔ (𝑏‘𝑧):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)⟶((1st ‘ℎ)‘𝑧)))
226	224, 225	mpbid 234	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑏‘𝑧):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)⟶((1st ‘ℎ)‘𝑧))
227	226	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑏‘𝑧):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)⟶((1st ‘ℎ)‘𝑧))
228	12, 193, 187, 208, 210, 216, 222, 227	setcco 18118	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧)(⟨((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤), ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)⟩(comp‘𝑆)((1st ‘ℎ)‘𝑧))((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)) = ((𝑏‘𝑧) ∘ ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)))
229	214, 147	ffvelcdmd 7068	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘ℎ)‘𝑤) ∈ 𝑈)
230	229	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘ℎ)‘𝑤) ∈ 𝑈)
231	141, 156, 7, 217, 147	natcl 17991	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (𝑏‘𝑤) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘ℎ)‘𝑤)))
232	12, 191, 217, 207, 229	elsetchom 18116	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((𝑏‘𝑤) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘ℎ)‘𝑤)) ↔ (𝑏‘𝑤):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)⟶((1st ‘ℎ)‘𝑤)))
233	231, 232	mpbid 234	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (𝑏‘𝑤):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)⟶((1st ‘ℎ)‘𝑤))
234	233	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑏‘𝑤):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)⟶((1st ‘ℎ)‘𝑤))
235	112, 168, 113	sylancr 596	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1st ‘ℎ)(𝑂 Func 𝑆)(2nd ‘ℎ))
236	7, 186, 217, 235, 169, 171	funcf2 17903	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑤(2nd ‘ℎ)𝑧):(𝑤(Hom ‘𝑂)𝑧)⟶(((1st ‘ℎ)‘𝑤)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)))
237	236, 189	ffvelcdmd 7068	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∈ (((1st ‘ℎ)‘𝑤)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)))
238	12, 193, 217, 230, 216	elsetchom 18116	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∈ (((1st ‘ℎ)‘𝑤)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)) ↔ ((𝑤(2nd ‘ℎ)𝑧)‘𝑘):((1st ‘ℎ)‘𝑤)⟶((1st ‘ℎ)‘𝑧)))
239	237, 238	mpbid 234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘ℎ)𝑧)‘𝑘):((1st ‘ℎ)‘𝑤)⟶((1st ‘ℎ)‘𝑧))
240	12, 193, 187, 208, 230, 216, 234, 239	setcco 18118	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)(⟨((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤), ((1st ‘ℎ)‘𝑤)⟩(comp‘𝑆)((1st ‘ℎ)‘𝑧))(𝑏‘𝑤)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤)))
241	190, 228, 240	3eqtr3d 2807	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧) ∘ ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤)))
242	241	fveq1d 6871	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑏‘𝑧) ∘ ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘))‘( 1 ‘𝑤)) = ((((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤))‘( 1 ‘𝑤)))
243	6, 107, 11, 142, 147	catidcl 17716	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ( 1 ‘𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤))
244	10, 6, 142, 147, 107, 147	yon11 18298	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤) = (𝑤(Hom ‘𝐶)𝑤))
245	243, 244	eleqtrrd 2867	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ( 1 ‘𝑤) ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤))
246	245	ad2antrr 736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ( 1 ‘𝑤) ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤))
247	222, 246	fvco3d 6970	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑏‘𝑧) ∘ ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘))‘( 1 ‘𝑤)) = ((𝑏‘𝑧)‘(((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤))))
248	233, 245	fvco3d 6970	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤))‘( 1 ‘𝑤)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))))
249	248	ad2antrr 736	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤))‘( 1 ‘𝑤)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))))
250	242, 247, 249	3eqtr3d 2807	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧)‘(((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤))) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))))
251		eqid 2764	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (comp‘𝐶) = (comp‘𝐶)
252	243	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ( 1 ‘𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤))
253	10, 6, 164, 169, 107, 169, 251, 171, 172, 252	yon12 18299	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤)) = (( 1 ‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐶)𝑤)𝑘))
254	6, 107, 11, 164, 171, 251, 169, 172	catlid 17717	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (( 1 ‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐶)𝑤)𝑘) = 𝑘)
255	253, 254	eqtrd 2799	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤)) = 𝑘)
256	255	fveq2d 6873	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧)‘(((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤))) = ((𝑏‘𝑧)‘𝑘))
257	250, 256	eqtr3d 2801	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))) = ((𝑏‘𝑧)‘𝑘))
258	173, 184, 257	3eqtrd 2803	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = ((𝑏‘𝑧)‘𝑘))
259	163, 258	syldan 600	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)) → ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = ((𝑏‘𝑧)‘𝑘))
260	259	mpteq2dva 5195	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑘 ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) ↦ ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘)) = (𝑘 ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) ↦ ((𝑏‘𝑧)‘𝑘)))
261	152	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) ∈ (⟨(1st ‘((1st ‘𝑌)‘𝑤)), (2nd ‘((1st ‘𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st ‘ℎ), (2nd ‘ℎ)⟩))
262	141, 261, 7, 217, 160	natcl 17991	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)))
263	12, 192, 217, 209, 215	elsetchom 18116	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)) ↔ (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)⟶((1st ‘ℎ)‘𝑧)))
264	262, 263	mpbid 234	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)⟶((1st ‘ℎ)‘𝑧))
265	264	feqmptd 6937	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧) = (𝑘 ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) ↦ ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘)))
266	226	feqmptd 6937	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑏‘𝑧) = (𝑘 ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) ↦ ((𝑏‘𝑧)‘𝑘)))
267	260, 265, 266	3eqtr4d 2809	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧) = (𝑏‘𝑧))
268	153, 157, 267	eqfnfvd 7016	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) = 𝑏)
269	268	mpteq2dva 5195	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))) = (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ 𝑏))
270		mptresid 6042	. . . . . . . . . . 11 ⊢ ( I ↾ (ℎ(1st ‘𝑍)𝑤)) = (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ 𝑏)
271	269, 270	eqtr4di 2817	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))) = ( I ↾ (ℎ(1st ‘𝑍)𝑤)))
272	140, 271	eqtrd 2799	. . . . . . . . 9 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑁𝑤) ∘ (ℎ𝑀𝑤)) = ( I ↾ (ℎ(1st ‘𝑍)𝑤)))
273		fcof1o 7282	. . . . . . . . 9 ⊢ ((((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤):(ℎ(1st ‘𝐸)𝑤)⟶(ℎ(1st ‘𝑍)𝑤)) ∧ (((ℎ𝑀𝑤) ∘ (ℎ𝑁𝑤)) = ( I ↾ (ℎ(1st ‘𝐸)𝑤)) ∧ ((ℎ𝑁𝑤) ∘ (ℎ𝑀𝑤)) = ( I ↾ (ℎ(1st ‘𝑍)𝑤)))) → ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ ◡(ℎ𝑀𝑤) = (ℎ𝑁𝑤)))
274	35, 84, 138, 272, 273	syl22anc 849	. . . . . . . 8 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ ◡(ℎ𝑀𝑤) = (ℎ𝑁𝑤)))
275		eqcom 2771	. . . . . . . . 9 ⊢ (◡(ℎ𝑀𝑤) = (ℎ𝑁𝑤) ↔ (ℎ𝑁𝑤) = ◡(ℎ𝑀𝑤))
276	275	anbi2i 632	. . . . . . . 8 ⊢ (((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ ◡(ℎ𝑀𝑤) = (ℎ𝑁𝑤)) ↔ ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤) = ◡(ℎ𝑀𝑤)))
277	274, 276	sylib 220	. . . . . . 7 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤) = ◡(ℎ𝑀𝑤)))
278		eqid 2764	. . . . . . . . . . 11 ⊢ (Base‘𝑇) = (Base‘𝑇)
279		relfunc 17897	. . . . . . . . . . . 12 ⊢ Rel ((𝑄 ×c 𝑂) Func 𝑇)
280		1st2ndbr 8025	. . . . . . . . . . . 12 ⊢ ((Rel ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st ‘𝑍)((𝑄 ×c 𝑂) Func 𝑇)(2nd ‘𝑍))
281	279, 22, 280	sylancr 596	. . . . . . . . . . 11 ⊢ (𝜑 → (1st ‘𝑍)((𝑄 ×c 𝑂) Func 𝑇)(2nd ‘𝑍))
282	8, 278, 281	funcf1 17901	. . . . . . . . . 10 ⊢ (𝜑 → (1st ‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
283	13, 18	setcbas 18113	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 = (Base‘𝑇))
284	283	feq3d 6678	. . . . . . . . . 10 ⊢ (𝜑 → ((1st ‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶𝑉 ↔ (1st ‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇)))
285	282, 284	mpbird 259	. . . . . . . . 9 ⊢ (𝜑 → (1st ‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶𝑉)
286	285	fovcdmda 7569	. . . . . . . 8 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ(1st ‘𝑍)𝑤) ∈ 𝑉)
287		1st2ndbr 8025	. . . . . . . . . . . 12 ⊢ ((Rel ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st ‘𝐸)((𝑄 ×c 𝑂) Func 𝑇)(2nd ‘𝐸))
288	279, 23, 287	sylancr 596	. . . . . . . . . . 11 ⊢ (𝜑 → (1st ‘𝐸)((𝑄 ×c 𝑂) Func 𝑇)(2nd ‘𝐸))
289	8, 278, 288	funcf1 17901	. . . . . . . . . 10 ⊢ (𝜑 → (1st ‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
290	283	feq3d 6678	. . . . . . . . . 10 ⊢ (𝜑 → ((1st ‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶𝑉 ↔ (1st ‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇)))
291	289, 290	mpbird 259	. . . . . . . . 9 ⊢ (𝜑 → (1st ‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶𝑉)
292	291	fovcdmda 7569	. . . . . . . 8 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ(1st ‘𝐸)𝑤) ∈ 𝑉)
293	13, 29, 286, 292, 25	setcinv 18125	. . . . . . 7 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤)((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤))(ℎ𝑁𝑤) ↔ ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤) = ◡(ℎ𝑀𝑤))))
294	277, 293	mpbird 259	. . . . . 6 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑀𝑤)((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤))(ℎ𝑁𝑤))
295	294	ralrimivva 3207	. . . . 5 ⊢ (𝜑 → ∀ℎ ∈ (𝑂 Func 𝑆)∀𝑤 ∈ 𝐵 (ℎ𝑀𝑤)((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤))(ℎ𝑁𝑤))
296		fveq2 6869	. . . . . . . 8 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → (𝑀‘𝑧) = (𝑀‘⟨ℎ, 𝑤⟩))
297		df-ov 7401	. . . . . . . 8 ⊢ (ℎ𝑀𝑤) = (𝑀‘⟨ℎ, 𝑤⟩)
298	296, 297	eqtr4di 2817	. . . . . . 7 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → (𝑀‘𝑧) = (ℎ𝑀𝑤))
299		fveq2 6869	. . . . . . . . 9 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → ((1st ‘𝑍)‘𝑧) = ((1st ‘𝑍)‘⟨ℎ, 𝑤⟩))
300		df-ov 7401	. . . . . . . . 9 ⊢ (ℎ(1st ‘𝑍)𝑤) = ((1st ‘𝑍)‘⟨ℎ, 𝑤⟩)
301	299, 300	eqtr4di 2817	. . . . . . . 8 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → ((1st ‘𝑍)‘𝑧) = (ℎ(1st ‘𝑍)𝑤))
302		fveq2 6869	. . . . . . . . 9 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → ((1st ‘𝐸)‘𝑧) = ((1st ‘𝐸)‘⟨ℎ, 𝑤⟩))
303		df-ov 7401	. . . . . . . . 9 ⊢ (ℎ(1st ‘𝐸)𝑤) = ((1st ‘𝐸)‘⟨ℎ, 𝑤⟩)
304	302, 303	eqtr4di 2817	. . . . . . . 8 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → ((1st ‘𝐸)‘𝑧) = (ℎ(1st ‘𝐸)𝑤))
305	301, 304	oveq12d 7416	. . . . . . 7 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → (((1st ‘𝑍)‘𝑧)(Inv‘𝑇)((1st ‘𝐸)‘𝑧)) = ((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤)))
306		fveq2 6869	. . . . . . . 8 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → (𝑁‘𝑧) = (𝑁‘⟨ℎ, 𝑤⟩))
307		df-ov 7401	. . . . . . . 8 ⊢ (ℎ𝑁𝑤) = (𝑁‘⟨ℎ, 𝑤⟩)
308	306, 307	eqtr4di 2817	. . . . . . 7 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → (𝑁‘𝑧) = (ℎ𝑁𝑤))
309	298, 305, 308	breq123d 5116	. . . . . 6 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → ((𝑀‘𝑧)(((1st ‘𝑍)‘𝑧)(Inv‘𝑇)((1st ‘𝐸)‘𝑧))(𝑁‘𝑧) ↔ (ℎ𝑀𝑤)((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤))(ℎ𝑁𝑤)))
310	309	ralxp 5815	. . . . 5 ⊢ (∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑀‘𝑧)(((1st ‘𝑍)‘𝑧)(Inv‘𝑇)((1st ‘𝐸)‘𝑧))(𝑁‘𝑧) ↔ ∀ℎ ∈ (𝑂 Func 𝑆)∀𝑤 ∈ 𝐵 (ℎ𝑀𝑤)((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤))(ℎ𝑁𝑤))
311	295, 310	sylibr 236	. . . 4 ⊢ (𝜑 → ∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑀‘𝑧)(((1st ‘𝑍)‘𝑧)(Inv‘𝑇)((1st ‘𝐸)‘𝑧))(𝑁‘𝑧))
312	311	r19.21bi 3256	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)) → (𝑀‘𝑧)(((1st ‘𝑍)‘𝑧)(Inv‘𝑇)((1st ‘𝐸)‘𝑧))(𝑁‘𝑧))
313	1, 8, 9, 22, 23, 24, 25, 27, 312	invfuc 18012	. 2 ⊢ (𝜑 → 𝑀(𝑍𝐼𝐸)(𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁‘𝑧)))
314		fvex 6882	. . . . 5 ⊢ ((1st ‘𝑓)‘𝑥) ∈ V
315	314	mptex 7209	. . . 4 ⊢ (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))) ∈ V
316	42, 315	fnmpoi 8053	. . 3 ⊢ 𝑁 Fn ((𝑂 Func 𝑆) × 𝐵)
317		dffn5 6927	. . 3 ⊢ (𝑁 Fn ((𝑂 Func 𝑆) × 𝐵) ↔ 𝑁 = (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁‘𝑧)))
318	316, 317	mpbi 232	. 2 ⊢ 𝑁 = (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁‘𝑧))
319	313, 318	breqtrrdi 5144	1 ⊢ (𝜑 → 𝑀(𝑍𝐼𝐸)𝑁)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1562   ∈ wcel 2144  ∀wral 3078  Vcvv 3456   ∪ cun 3904   ⊆ wss 3906  ⟨cop 4590   class class class wbr 5102   ↦ cmpt 5183   I cid 5543   × cxp 5647  ^◡ccnv 5648  ran crn 5650   ↾ cres 5651   ∘ ccom 5653  Rel wrel 5654   Fn wfn 6518  ⟶wf 6519  –1-1-onto→wf1o 6522  ‘cfv 6523  (class class class)co 7398   ∈ cmpo 7400  1^st c1st 7970  2^nd c2nd 7971  tpos ctpos 8207  Basecbs 17247  Hom chom 17299  compcco 17300  Catccat 17698  Idccid 17699  Hom_f chomf 17700  oppCatcoppc 17745  Invcinv 17780   Func cfunc 17889   ∘_func ccofu 17891   Nat cnat 17979   FuncCat cfuc 17980  SetCatcsetc 18110   ×_c cxpc 18202   1^st_F c1stf 18203   2^nd_F c2ndf 18204   ⟨,⟩_F cprf 18205   eval_F cevlf 18243  Hom_Fchof 18282  Yoncyon 18283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-rep 5229  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5544  df-eprel 5549  df-po 5557  df-so 5558  df-fr 5602  df-we 5604  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-pred 6290  df-ord 6351  df-on 6352  df-lim 6353  df-suc 6354  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-riota 7355  df-ov 7401  df-oprab 7402  df-mpo 7403  df-om 7849  df-1st 7972  df-2nd 7973  df-tpos 8208  df-frecs 8264  df-wrecs 8295  df-recs 8344  df-rdg 8383  df-1o 8439  df-er 8680  df-map 8812  df-pm 8813  df-ixp 8882  df-en 8930  df-dom 8931  df-sdom 8932  df-fin 8933  df-pnf 11220  df-mnf 11221  df-xr 11222  df-ltxr 11223  df-le 11224  df-sub 11418  df-neg 11419  df-nn 12213  df-2 12282  df-3 12283  df-4 12284  df-5 12285  df-6 12286  df-7 12287  df-8 12288  df-9 12289  df-n0 12484  df-z 12571  df-dec 12691  df-uz 12842  df-fz 13515  df-struct 17185  df-sets 17202  df-slot 17220  df-ndx 17232  df-base 17248  df-ress 17269  df-hom 17312  df-cco 17313  df-cat 17702  df-cid 17703  df-homf 17704  df-comf 17705  df-oppc 17746  df-sect 17782  df-inv 17783  df-ssc 17845  df-resc 17846  df-subc 17847  df-func 17893  df-cofu 17895  df-nat 17981  df-fuc 17982  df-setc 18111  df-xpc 18206  df-1stf 18207  df-2ndf 18208  df-prf 18209  df-evlf 18247  df-curf 18248  df-hof 18284  df-yon 18285

This theorem is referenced by:  yonffthlem  18316  yoneda  18317