Theorem yonedainv 18187

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 2729	. . . 4 ⊢ (𝑄 ×c 𝑂) = (𝑄 ×c 𝑂)
3		yoneda.q	. . . . 5 ⊢ 𝑄 = (𝑂 FuncCat 𝑆)
4	3	fucbas 17870	. . . 4 ⊢ (𝑂 Func 𝑆) = (Base‘𝑄)
5		yoneda.o	. . . . 5 ⊢ 𝑂 = (oppCat‘𝐶)
6		yoneda.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐶)
7	5, 6	oppcbas 17624	. . . 4 ⊢ 𝐵 = (Base‘𝑂)
8	2, 4, 7	xpcbas 18084	. . 3 ⊢ ((𝑂 Func 𝑆) × 𝐵) = (Base‘(𝑄 ×c 𝑂))
9		eqid 2729	. . 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 18178	. . . 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 2729	. . 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 18186	. . 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 18180	. . . . . . . . . 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 18183	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑁𝑤)‘𝑏) ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
45	44	fmpttd 7049	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑏 ∈ ((1st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏)):((1st ‘ℎ)‘𝑤)⟶(((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
46	6	fvexi 6836	. . . . . . . . . . . . . . 15 ⊢ 𝐵 ∈ V
47	46	mptex 7159	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢))) ∈ V
48		eqid 2729	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))) = (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢))))
49	47, 48	fnmpti 6625	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))) Fn ((1st ‘ℎ)‘𝑤)
50		simpl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → 𝑓 = ℎ)
51	50	fveq2d 6826	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → (1st ‘𝑓) = (1st ‘ℎ))
52		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → 𝑥 = 𝑤)
53	51, 52	fveq12d 6829	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → ((1st ‘𝑓)‘𝑥) = ((1st ‘ℎ)‘𝑤))
54		simplr 768	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → 𝑥 = 𝑤)
55	54	oveq2d 7365	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (𝑦(Hom ‘𝐶)𝑥) = (𝑦(Hom ‘𝐶)𝑤))
56		simpll 766	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → 𝑓 = ℎ)
57	56	fveq2d 6826	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (2nd ‘𝑓) = (2nd ‘ℎ))
58		eqidd 2730	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → 𝑦 = 𝑦)
59	57, 54, 58	oveq123d 7370	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (𝑥(2nd ‘𝑓)𝑦) = (𝑤(2nd ‘ℎ)𝑦))
60	59	fveq1d 6824	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → ((𝑥(2nd ‘𝑓)𝑦)‘𝑔) = ((𝑤(2nd ‘ℎ)𝑦)‘𝑔))
61	60	fveq1d 6824	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢) = (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢))
62	55, 61	mpteq12dv 5179	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢)) = (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))
63	62	mpteq2dva 5185	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢))) = (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢))))
64	53, 63	mpteq12dv 5179	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))) = (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))))
65		fvex 6835	. . . . . . . . . . . . . . . . 17 ⊢ ((1st ‘ℎ)‘𝑤) ∈ V
66	65	mptex 7159	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))) ∈ V
67	64, 42, 66	ovmpoa 7504	. . . . . . . . . . . . . . 15 ⊢ ((ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵) → (ℎ𝑁𝑤) = (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))))
68	67	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤) = (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))))
69	68	fneq1d 6575	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑁𝑤) Fn ((1st ‘ℎ)‘𝑤) ↔ (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))) Fn ((1st ‘ℎ)‘𝑤)))
70	49, 69	mpbiri 258	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤) Fn ((1st ‘ℎ)‘𝑤))
71		dffn5 6881	. . . . . . . . . . . 12 ⊢ ((ℎ𝑁𝑤) Fn ((1st ‘ℎ)‘𝑤) ↔ (ℎ𝑁𝑤) = (𝑏 ∈ ((1st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏)))
72	70, 71	sylib 218	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤) = (𝑏 ∈ ((1st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏)))
73	5	oppccat 17628	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat)
74	17, 73	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑂 ∈ Cat)
75	74	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → 𝑂 ∈ Cat)
76	20	unssbd 4145	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 ⊆ 𝑉)
77	18, 76	ssexd 5263	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ∈ V)
78	12	setccat 17992	. . . . . . . . . . . . . 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 18126	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ(1st ‘𝐸)𝑤) = ((1st ‘ℎ)‘𝑤))
82	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33	yonedalem21 18179	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ(1st ‘𝑍)𝑤) = (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
83	72, 81, 82	feq123d 6641	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑁𝑤):(ℎ(1st ‘𝐸)𝑤)⟶(ℎ(1st ‘𝑍)𝑤) ↔ (𝑏 ∈ ((1st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏)):((1st ‘ℎ)‘𝑤)⟶(((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ)))
84	45, 83	mpbird 257	. . . . . . . . 9 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤):(ℎ(1st ‘𝐸)𝑤)⟶(ℎ(1st ‘𝑍)𝑤))
85		fcompt 7067	. . . . . . . . . . 11 ⊢ (((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤):(ℎ(1st ‘𝐸)𝑤)⟶(ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑀𝑤) ∘ (ℎ𝑁𝑤)) = (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘))))
86	35, 84, 85	syl2anc 584	. . . . . . . . . 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 18180	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑀𝑤) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))) ∧ (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤)))
96	95	simpld 494	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (ℎ𝑀𝑤) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))))
97	96	fveq1d 6824	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘)) = ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘((ℎ𝑁𝑤)‘𝑘)))
98	72, 44	fmpt3d 7050	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤):((1st ‘ℎ)‘𝑤)⟶(((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
99	98	ffvelcdmda 7018	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑁𝑤)‘𝑘) ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
100		fveq1 6821	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ((ℎ𝑁𝑤)‘𝑘) → (𝑎‘𝑤) = (((ℎ𝑁𝑤)‘𝑘)‘𝑤))
101	100	fveq1d 6824	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ((ℎ𝑁𝑤)‘𝑘) → ((𝑎‘𝑤)‘( 1 ‘𝑤)) = ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)))
102		eqid 2729	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))
103		fvex 6835	. . . . . . . . . . . . . . . 16 ⊢ ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)) ∈ V
104	101, 102, 103	fvmpt 6930	. . . . . . . . . . . . . . 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 2729	. . . . . . . . . . . . . . . . 17 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
108	6, 107, 11, 89, 94	catidcl 17588	. . . . . . . . . . . . . . . 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 18182	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)) = (((𝑤(2nd ‘ℎ)𝑤)‘( 1 ‘𝑤))‘𝑘))
110		eqid 2729	. . . . . . . . . . . . . . . . . 18 ⊢ (Id‘𝑂) = (Id‘𝑂)
111		eqid 2729	. . . . . . . . . . . . . . . . . 18 ⊢ (Id‘𝑆) = (Id‘𝑆)
112		relfunc 17769	. . . . . . . . . . . . . . . . . . 19 ⊢ Rel (𝑂 Func 𝑆)
113		1st2ndbr 7977	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Rel (𝑂 Func 𝑆) ∧ ℎ ∈ (𝑂 Func 𝑆)) → (1st ‘ℎ)(𝑂 Func 𝑆)(2nd ‘ℎ))
114	112, 93, 113	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (1st ‘ℎ)(𝑂 Func 𝑆)(2nd ‘ℎ))
115	7, 110, 111, 114, 94	funcid 17777	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((𝑤(2nd ‘ℎ)𝑤)‘((Id‘𝑂)‘𝑤)) = ((Id‘𝑆)‘((1st ‘ℎ)‘𝑤)))
116	5, 11	oppcid 17627	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐶 ∈ Cat → (Id‘𝑂) = 1 )
117	89, 116	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (Id‘𝑂) = 1 )
118	117	fveq1d 6824	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((Id‘𝑂)‘𝑤) = ( 1 ‘𝑤))
119	118	fveq2d 6826	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((𝑤(2nd ‘ℎ)𝑤)‘((Id‘𝑂)‘𝑤)) = ((𝑤(2nd ‘ℎ)𝑤)‘( 1 ‘𝑤)))
120	77	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑈 ∈ V)
121		eqid 2729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Base‘𝑆) = (Base‘𝑆)
122	7, 121, 114	funcf1 17773	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (1st ‘ℎ):𝐵⟶(Base‘𝑆))
123	12, 120	setcbas 17985	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑈 = (Base‘𝑆))
124	123	feq3d 6637	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((1st ‘ℎ):𝐵⟶𝑈 ↔ (1st ‘ℎ):𝐵⟶(Base‘𝑆)))
125	122, 124	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (1st ‘ℎ):𝐵⟶𝑈)
126	125, 94	ffvelcdmd 7019	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((1st ‘ℎ)‘𝑤) ∈ 𝑈)
127	12, 111, 120, 126	setcid 17993	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((Id‘𝑆)‘((1st ‘ℎ)‘𝑤)) = ( I ↾ ((1st ‘ℎ)‘𝑤)))
128	115, 119, 127	3eqtr3d 2772	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((𝑤(2nd ‘ℎ)𝑤)‘( 1 ‘𝑤)) = ( I ↾ ((1st ‘ℎ)‘𝑤)))
129	128	fveq1d 6824	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (((𝑤(2nd ‘ℎ)𝑤)‘( 1 ‘𝑤))‘𝑘) = (( I ↾ ((1st ‘ℎ)‘𝑤))‘𝑘))
130		fvresi 7109	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ((1st ‘ℎ)‘𝑤) → (( I ↾ ((1st ‘ℎ)‘𝑤))‘𝑘) = 𝑘)
131	130	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (( I ↾ ((1st ‘ℎ)‘𝑤))‘𝑘) = 𝑘)
132	109, 129, 131	3eqtrd 2768	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)) = 𝑘)
133	97, 105, 132	3eqtrd 2768	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘)) = 𝑘)
134	88, 133	syldan 591	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ (ℎ(1st ‘𝐸)𝑤)) → ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘)) = 𝑘)
135	134	mpteq2dva 5185	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘))) = (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ 𝑘))
136		mptresid 6002	. . . . . . . . . . 11 ⊢ ( I ↾ (ℎ(1st ‘𝐸)𝑤)) = (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ 𝑘)
137	135, 136	eqtr4di 2782	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘))) = ( I ↾ (ℎ(1st ‘𝐸)𝑤)))
138	86, 137	eqtrd 2764	. . . . . . . . 9 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤) ∘ (ℎ𝑁𝑤)) = ( I ↾ (ℎ(1st ‘𝐸)𝑤)))
139		fcompt 7067	. . . . . . . . . . 11 ⊢ (((ℎ𝑁𝑤):(ℎ(1st ‘𝐸)𝑤)⟶(ℎ(1st ‘𝑍)𝑤) ∧ (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤)) → ((ℎ𝑁𝑤) ∘ (ℎ𝑀𝑤)) = (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))))
140	84, 35, 139	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑁𝑤) ∘ (ℎ𝑀𝑤)) = (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))))
141		eqid 2729	. . . . . . . . . . . . . 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 6637	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤) ↔ (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶((1st ‘ℎ)‘𝑤)))
149	35, 148	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶((1st ‘ℎ)‘𝑤))
150	149	ffvelcdmda 7018	. . . . . . . . . . . . . . . 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 18183	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
152	141, 151	nat1st2nd 17861	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) ∈ (⟨(1st ‘((1st ‘𝑌)‘𝑤)), (2nd ‘((1st ‘𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st ‘ℎ), (2nd ‘ℎ)⟩))
153	141, 152, 7	natfn 17864	. . . . . . . . . . . . 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 17861	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑏 ∈ (⟨(1st ‘((1st ‘𝑌)‘𝑤)), (2nd ‘((1st ‘𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st ‘ℎ), (2nd ‘ℎ)⟩))
157	141, 156, 7	natfn 17864	. . . . . . . . . . . . 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 18170	. . . . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑉 ∈ 𝑊)
166	144	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ran (Homf ‘𝐶) ⊆ 𝑈)
167	145	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
168	146	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ℎ ∈ (𝑂 Func 𝑆))
169	159	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑤 ∈ 𝐵)
170	150	ad2antrr 726	. . . . . . . . . . . . . . . . . 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 18182	. . . . . . . . . . . . . . . . 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 18180	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ𝑀𝑤) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))) ∧ (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤)))
175	174	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ℎ𝑀𝑤) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))))
176	175	fveq1d 6824	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ𝑀𝑤)‘𝑏) = ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘𝑏))
177	155	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑏 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
178		fveq1 6821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑏 → (𝑎‘𝑤) = (𝑏‘𝑤))
179	178	fveq1d 6824	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑏 → ((𝑎‘𝑤)‘( 1 ‘𝑤)) = ((𝑏‘𝑤)‘( 1 ‘𝑤)))
180		fvex 6835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏‘𝑤)‘( 1 ‘𝑤)) ∈ V
181	179, 102, 180	fvmpt 6930	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) → ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘𝑏) = ((𝑏‘𝑤)‘( 1 ‘𝑤)))
182	177, 181	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘𝑏) = ((𝑏‘𝑤)‘( 1 ‘𝑤)))
183	176, 182	eqtrd 2764	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ𝑀𝑤)‘𝑏) = ((𝑏‘𝑤)‘( 1 ‘𝑤)))
184	183	fveq2d 6826	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((ℎ𝑀𝑤)‘𝑏)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))))
185	156	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑏 ∈ (⟨(1st ‘((1st ‘𝑌)‘𝑤)), (2nd ‘((1st ‘𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st ‘ℎ), (2nd ‘ℎ)⟩))
186		eqid 2729	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Hom ‘𝑂) = (Hom ‘𝑂)
187		eqid 2729	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (comp‘𝑆) = (comp‘𝑆)
188	107, 5	oppchom 17621	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤(Hom ‘𝑂)𝑧) = (𝑧(Hom ‘𝐶)𝑤)
189	172, 188	eleqtrrdi 2839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑘 ∈ (𝑤(Hom ‘𝑂)𝑧))
190	141, 185, 7, 186, 187, 169, 171, 189	nati 17865	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧)(⟨((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤), ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)⟩(comp‘𝑆)((1st ‘ℎ)‘𝑧))((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)(⟨((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤), ((1st ‘ℎ)‘𝑤)⟩(comp‘𝑆)((1st ‘ℎ)‘𝑧))(𝑏‘𝑤)))
191	77	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑈 ∈ V)
192	191	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → 𝑈 ∈ V)
193	192	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑈 ∈ V)
194		relfunc 17769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ Rel (𝐶 Func 𝑄)
195	10, 17, 5, 12, 3, 77, 19	yoncl 18168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → 𝑌 ∈ (𝐶 Func 𝑄))
196		1st2ndbr 7977	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((Rel (𝐶 Func 𝑄) ∧ 𝑌 ∈ (𝐶 Func 𝑄)) → (1st ‘𝑌)(𝐶 Func 𝑄)(2nd ‘𝑌))
197	194, 195, 196	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (1st ‘𝑌)(𝐶 Func 𝑄)(2nd ‘𝑌))
198	6, 4, 197	funcf1 17773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (1st ‘𝑌):𝐵⟶(𝑂 Func 𝑆))
199	198	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘𝑌):𝐵⟶(𝑂 Func 𝑆))
200	199, 147	ffvelcdmd 7019	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘𝑌)‘𝑤) ∈ (𝑂 Func 𝑆))
201		1st2ndbr 7977	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Rel (𝑂 Func 𝑆) ∧ ((1st ‘𝑌)‘𝑤) ∈ (𝑂 Func 𝑆)) → (1st ‘((1st ‘𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st ‘𝑌)‘𝑤)))
202	112, 200, 201	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘((1st ‘𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st ‘𝑌)‘𝑤)))
203	7, 121, 202	funcf1 17773	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘((1st ‘𝑌)‘𝑤)):𝐵⟶(Base‘𝑆))
204	12, 191	setcbas 17985	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑈 = (Base‘𝑆))
205	204	feq3d 6637	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘((1st ‘𝑌)‘𝑤)):𝐵⟶𝑈 ↔ (1st ‘((1st ‘𝑌)‘𝑤)):𝐵⟶(Base‘𝑆)))
206	203, 205	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘((1st ‘𝑌)‘𝑤)):𝐵⟶𝑈)
207	206, 147	ffvelcdmd 7019	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤) ∈ 𝑈)
208	207	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤) ∈ 𝑈)
209	206	ffvelcdmda 7018	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) ∈ 𝑈)
210	209	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) ∈ 𝑈)
211	112, 146, 113	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘ℎ)(𝑂 Func 𝑆)(2nd ‘ℎ))
212	7, 121, 211	funcf1 17773	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘ℎ):𝐵⟶(Base‘𝑆))
213	204	feq3d 6637	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘ℎ):𝐵⟶𝑈 ↔ (1st ‘ℎ):𝐵⟶(Base‘𝑆)))
214	212, 213	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘ℎ):𝐵⟶𝑈)
215	214	ffvelcdmda 7018	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((1st ‘ℎ)‘𝑧) ∈ 𝑈)
216	215	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘ℎ)‘𝑧) ∈ 𝑈)
217		eqid 2729	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Hom ‘𝑆) = (Hom ‘𝑆)
218	202	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1st ‘((1st ‘𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st ‘𝑌)‘𝑤)))
219	7, 186, 217, 218, 169, 171	funcf2 17775	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧):(𝑤(Hom ‘𝑂)𝑧)⟶(((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)))
220	219, 189	ffvelcdmd 7019	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)))
221	12, 193, 217, 208, 210	elsetchom 17988	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)) ↔ ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)⟶((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)))
222	220, 221	mpbid 232	. . . . . . . . . . . . . . . . . . . . . 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 17863	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑏‘𝑧) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)))
225	12, 192, 217, 209, 215	elsetchom 17988	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((𝑏‘𝑧) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)) ↔ (𝑏‘𝑧):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)⟶((1st ‘ℎ)‘𝑧)))
226	224, 225	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . 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 17990	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧)(⟨((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤), ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)⟩(comp‘𝑆)((1st ‘ℎ)‘𝑧))((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)) = ((𝑏‘𝑧) ∘ ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)))
229	214, 147	ffvelcdmd 7019	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘ℎ)‘𝑤) ∈ 𝑈)
230	229	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘ℎ)‘𝑤) ∈ 𝑈)
231	141, 156, 7, 217, 147	natcl 17863	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (𝑏‘𝑤) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘ℎ)‘𝑤)))
232	12, 191, 217, 207, 229	elsetchom 17988	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((𝑏‘𝑤) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘ℎ)‘𝑤)) ↔ (𝑏‘𝑤):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)⟶((1st ‘ℎ)‘𝑤)))
233	231, 232	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (𝑏‘𝑤):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)⟶((1st ‘ℎ)‘𝑤))
234	233	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑏‘𝑤):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)⟶((1st ‘ℎ)‘𝑤))
235	112, 168, 113	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1st ‘ℎ)(𝑂 Func 𝑆)(2nd ‘ℎ))
236	7, 186, 217, 235, 169, 171	funcf2 17775	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑤(2nd ‘ℎ)𝑧):(𝑤(Hom ‘𝑂)𝑧)⟶(((1st ‘ℎ)‘𝑤)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)))
237	236, 189	ffvelcdmd 7019	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∈ (((1st ‘ℎ)‘𝑤)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)))
238	12, 193, 217, 230, 216	elsetchom 17988	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∈ (((1st ‘ℎ)‘𝑤)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)) ↔ ((𝑤(2nd ‘ℎ)𝑧)‘𝑘):((1st ‘ℎ)‘𝑤)⟶((1st ‘ℎ)‘𝑧)))
239	237, 238	mpbid 232	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘ℎ)𝑧)‘𝑘):((1st ‘ℎ)‘𝑤)⟶((1st ‘ℎ)‘𝑧))
240	12, 193, 187, 208, 230, 216, 234, 239	setcco 17990	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)(⟨((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤), ((1st ‘ℎ)‘𝑤)⟩(comp‘𝑆)((1st ‘ℎ)‘𝑧))(𝑏‘𝑤)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤)))
241	190, 228, 240	3eqtr3d 2772	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧) ∘ ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤)))
242	241	fveq1d 6824	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑏‘𝑧) ∘ ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘))‘( 1 ‘𝑤)) = ((((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤))‘( 1 ‘𝑤)))
243	6, 107, 11, 142, 147	catidcl 17588	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ( 1 ‘𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤))
244	10, 6, 142, 147, 107, 147	yon11 18170	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤) = (𝑤(Hom ‘𝐶)𝑤))
245	243, 244	eleqtrrd 2831	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ( 1 ‘𝑤) ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤))
246	245	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ( 1 ‘𝑤) ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤))
247	222, 246	fvco3d 6923	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑏‘𝑧) ∘ ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘))‘( 1 ‘𝑤)) = ((𝑏‘𝑧)‘(((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤))))
248	233, 245	fvco3d 6923	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤))‘( 1 ‘𝑤)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))))
249	248	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤))‘( 1 ‘𝑤)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))))
250	242, 247, 249	3eqtr3d 2772	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧)‘(((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤))) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))))
251		eqid 2729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (comp‘𝐶) = (comp‘𝐶)
252	243	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ( 1 ‘𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤))
253	10, 6, 164, 169, 107, 169, 251, 171, 172, 252	yon12 18171	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤)) = (( 1 ‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐶)𝑤)𝑘))
254	6, 107, 11, 164, 171, 251, 169, 172	catlid 17589	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (( 1 ‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐶)𝑤)𝑘) = 𝑘)
255	253, 254	eqtrd 2764	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤)) = 𝑘)
256	255	fveq2d 6826	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧)‘(((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤))) = ((𝑏‘𝑧)‘𝑘))
257	250, 256	eqtr3d 2766	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))) = ((𝑏‘𝑧)‘𝑘))
258	173, 184, 257	3eqtrd 2768	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = ((𝑏‘𝑧)‘𝑘))
259	163, 258	syldan 591	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)) → ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = ((𝑏‘𝑧)‘𝑘))
260	259	mpteq2dva 5185	. . . . . . . . . . . . . 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 17863	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)))
263	12, 192, 217, 209, 215	elsetchom 17988	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)) ↔ (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)⟶((1st ‘ℎ)‘𝑧)))
264	262, 263	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)⟶((1st ‘ℎ)‘𝑧))
265	264	feqmptd 6891	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧) = (𝑘 ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) ↦ ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘)))
266	226	feqmptd 6891	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑏‘𝑧) = (𝑘 ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) ↦ ((𝑏‘𝑧)‘𝑘)))
267	260, 265, 266	3eqtr4d 2774	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧) = (𝑏‘𝑧))
268	153, 157, 267	eqfnfvd 6968	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) = 𝑏)
269	268	mpteq2dva 5185	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))) = (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ 𝑏))
270		mptresid 6002	. . . . . . . . . . 11 ⊢ ( I ↾ (ℎ(1st ‘𝑍)𝑤)) = (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ 𝑏)
271	269, 270	eqtr4di 2782	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))) = ( I ↾ (ℎ(1st ‘𝑍)𝑤)))
272	140, 271	eqtrd 2764	. . . . . . . . 9 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑁𝑤) ∘ (ℎ𝑀𝑤)) = ( I ↾ (ℎ(1st ‘𝑍)𝑤)))
273		fcof1o 7233	. . . . . . . . 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 2736	. . . . . . . . 9 ⊢ (◡(ℎ𝑀𝑤) = (ℎ𝑁𝑤) ↔ (ℎ𝑁𝑤) = ◡(ℎ𝑀𝑤))
276	275	anbi2i 623	. . . . . . . 8 ⊢ (((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ ◡(ℎ𝑀𝑤) = (ℎ𝑁𝑤)) ↔ ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤) = ◡(ℎ𝑀𝑤)))
277	274, 276	sylib 218	. . . . . . 7 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤) = ◡(ℎ𝑀𝑤)))
278		eqid 2729	. . . . . . . . . . 11 ⊢ (Base‘𝑇) = (Base‘𝑇)
279		relfunc 17769	. . . . . . . . . . . 12 ⊢ Rel ((𝑄 ×c 𝑂) Func 𝑇)
280		1st2ndbr 7977	. . . . . . . . . . . 12 ⊢ ((Rel ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st ‘𝑍)((𝑄 ×c 𝑂) Func 𝑇)(2nd ‘𝑍))
281	279, 22, 280	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → (1st ‘𝑍)((𝑄 ×c 𝑂) Func 𝑇)(2nd ‘𝑍))
282	8, 278, 281	funcf1 17773	. . . . . . . . . 10 ⊢ (𝜑 → (1st ‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
283	13, 18	setcbas 17985	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 = (Base‘𝑇))
284	283	feq3d 6637	. . . . . . . . . 10 ⊢ (𝜑 → ((1st ‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶𝑉 ↔ (1st ‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇)))
285	282, 284	mpbird 257	. . . . . . . . 9 ⊢ (𝜑 → (1st ‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶𝑉)
286	285	fovcdmda 7520	. . . . . . . 8 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ(1st ‘𝑍)𝑤) ∈ 𝑉)
287		1st2ndbr 7977	. . . . . . . . . . . 12 ⊢ ((Rel ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st ‘𝐸)((𝑄 ×c 𝑂) Func 𝑇)(2nd ‘𝐸))
288	279, 23, 287	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → (1st ‘𝐸)((𝑄 ×c 𝑂) Func 𝑇)(2nd ‘𝐸))
289	8, 278, 288	funcf1 17773	. . . . . . . . . 10 ⊢ (𝜑 → (1st ‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
290	283	feq3d 6637	. . . . . . . . . 10 ⊢ (𝜑 → ((1st ‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶𝑉 ↔ (1st ‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇)))
291	289, 290	mpbird 257	. . . . . . . . 9 ⊢ (𝜑 → (1st ‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶𝑉)
292	291	fovcdmda 7520	. . . . . . . 8 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ(1st ‘𝐸)𝑤) ∈ 𝑉)
293	13, 29, 286, 292, 25	setcinv 17997	. . . . . . 7 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤)((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤))(ℎ𝑁𝑤) ↔ ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤) = ◡(ℎ𝑀𝑤))))
294	277, 293	mpbird 257	. . . . . 6 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑀𝑤)((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤))(ℎ𝑁𝑤))
295	294	ralrimivva 3172	. . . . 5 ⊢ (𝜑 → ∀ℎ ∈ (𝑂 Func 𝑆)∀𝑤 ∈ 𝐵 (ℎ𝑀𝑤)((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤))(ℎ𝑁𝑤))
296		fveq2 6822	. . . . . . . 8 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → (𝑀‘𝑧) = (𝑀‘⟨ℎ, 𝑤⟩))
297		df-ov 7352	. . . . . . . 8 ⊢ (ℎ𝑀𝑤) = (𝑀‘⟨ℎ, 𝑤⟩)
298	296, 297	eqtr4di 2782	. . . . . . 7 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → (𝑀‘𝑧) = (ℎ𝑀𝑤))
299		fveq2 6822	. . . . . . . . 9 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → ((1st ‘𝑍)‘𝑧) = ((1st ‘𝑍)‘⟨ℎ, 𝑤⟩))
300		df-ov 7352	. . . . . . . . 9 ⊢ (ℎ(1st ‘𝑍)𝑤) = ((1st ‘𝑍)‘⟨ℎ, 𝑤⟩)
301	299, 300	eqtr4di 2782	. . . . . . . 8 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → ((1st ‘𝑍)‘𝑧) = (ℎ(1st ‘𝑍)𝑤))
302		fveq2 6822	. . . . . . . . 9 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → ((1st ‘𝐸)‘𝑧) = ((1st ‘𝐸)‘⟨ℎ, 𝑤⟩))
303		df-ov 7352	. . . . . . . . 9 ⊢ (ℎ(1st ‘𝐸)𝑤) = ((1st ‘𝐸)‘⟨ℎ, 𝑤⟩)
304	302, 303	eqtr4di 2782	. . . . . . . 8 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → ((1st ‘𝐸)‘𝑧) = (ℎ(1st ‘𝐸)𝑤))
305	301, 304	oveq12d 7367	. . . . . . 7 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → (((1st ‘𝑍)‘𝑧)(Inv‘𝑇)((1st ‘𝐸)‘𝑧)) = ((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤)))
306		fveq2 6822	. . . . . . . 8 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → (𝑁‘𝑧) = (𝑁‘⟨ℎ, 𝑤⟩))
307		df-ov 7352	. . . . . . . 8 ⊢ (ℎ𝑁𝑤) = (𝑁‘⟨ℎ, 𝑤⟩)
308	306, 307	eqtr4di 2782	. . . . . . 7 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → (𝑁‘𝑧) = (ℎ𝑁𝑤))
309	298, 305, 308	breq123d 5106	. . . . . 6 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → ((𝑀‘𝑧)(((1st ‘𝑍)‘𝑧)(Inv‘𝑇)((1st ‘𝐸)‘𝑧))(𝑁‘𝑧) ↔ (ℎ𝑀𝑤)((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤))(ℎ𝑁𝑤)))
310	309	ralxp 5784	. . . . 5 ⊢ (∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑀‘𝑧)(((1st ‘𝑍)‘𝑧)(Inv‘𝑇)((1st ‘𝐸)‘𝑧))(𝑁‘𝑧) ↔ ∀ℎ ∈ (𝑂 Func 𝑆)∀𝑤 ∈ 𝐵 (ℎ𝑀𝑤)((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤))(ℎ𝑁𝑤))
311	295, 310	sylibr 234	. . . 4 ⊢ (𝜑 → ∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑀‘𝑧)(((1st ‘𝑍)‘𝑧)(Inv‘𝑇)((1st ‘𝐸)‘𝑧))(𝑁‘𝑧))
312	311	r19.21bi 3221	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)) → (𝑀‘𝑧)(((1st ‘𝑍)‘𝑧)(Inv‘𝑇)((1st ‘𝐸)‘𝑧))(𝑁‘𝑧))
313	1, 8, 9, 22, 23, 24, 25, 27, 312	invfuc 17884	. 2 ⊢ (𝜑 → 𝑀(𝑍𝐼𝐸)(𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁‘𝑧)))
314		fvex 6835	. . . . 5 ⊢ ((1st ‘𝑓)‘𝑥) ∈ V
315	314	mptex 7159	. . . 4 ⊢ (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))) ∈ V
316	42, 315	fnmpoi 8005	. . 3 ⊢ 𝑁 Fn ((𝑂 Func 𝑆) × 𝐵)
317		dffn5 6881	. . 3 ⊢ (𝑁 Fn ((𝑂 Func 𝑆) × 𝐵) ↔ 𝑁 = (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁‘𝑧)))
318	316, 317	mpbi 230	. 2 ⊢ 𝑁 = (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁‘𝑧))
319	313, 318	breqtrrdi 5134	1 ⊢ (𝜑 → 𝑀(𝑍𝐼𝐸)𝑁)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044  Vcvv 3436   ∪ cun 3901   ⊆ wss 3903  ⟨cop 4583   class class class wbr 5092   ↦ cmpt 5173   I cid 5513   × cxp 5617  ^◡ccnv 5618  ran crn 5620   ↾ cres 5621   ∘ ccom 5623  Rel wrel 5624   Fn wfn 6477  ⟶wf 6478  –1-1-onto→wf1o 6481  ‘cfv 6482  (class class class)co 7349   ∈ cmpo 7351  1^st c1st 7922  2^nd c2nd 7923  tpos ctpos 8158  Basecbs 17120  Hom chom 17172  compcco 17173  Catccat 17570  Idccid 17571  Hom_f chomf 17572  oppCatcoppc 17617  Invcinv 17652   Func cfunc 17761   ∘_func ccofu 17763   Nat cnat 17851   FuncCat cfuc 17852  SetCatcsetc 17982   ×_c cxpc 18074   1^st_F c1stf 18075   2^nd_F c2ndf 18076   ⟨,⟩_F cprf 18077   eval_F cevlf 18115  Hom_Fchof 18154  Yoncyon 18155

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5218  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3343  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-tp 4582  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-1st 7924  df-2nd 7925  df-tpos 8159  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-1o 8388  df-er 8625  df-map 8755  df-pm 8756  df-ixp 8825  df-en 8873  df-dom 8874  df-sdom 8875  df-fin 8876  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-nn 12129  df-2 12191  df-3 12192  df-4 12193  df-5 12194  df-6 12195  df-7 12196  df-8 12197  df-9 12198  df-n0 12385  df-z 12472  df-dec 12592  df-uz 12736  df-fz 13411  df-struct 17058  df-sets 17075  df-slot 17093  df-ndx 17105  df-base 17121  df-ress 17142  df-hom 17185  df-cco 17186  df-cat 17574  df-cid 17575  df-homf 17576  df-comf 17577  df-oppc 17618  df-sect 17654  df-inv 17655  df-ssc 17717  df-resc 17718  df-subc 17719  df-func 17765  df-cofu 17767  df-nat 17853  df-fuc 17854  df-setc 17983  df-xpc 18078  df-1stf 18079  df-2ndf 18080  df-prf 18081  df-evlf 18119  df-curf 18120  df-hof 18156  df-yon 18157

This theorem is referenced by:  yonffthlem  18188  yoneda  18189