Theorem yonedainv 16968

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 2651	. . . 4 ⊢ (𝑄 ×c 𝑂) = (𝑄 ×c 𝑂)
3		yoneda.q	. . . . 5 ⊢ 𝑄 = (𝑂 FuncCat 𝑆)
4	3	fucbas 16667	. . . 4 ⊢ (𝑂 Func 𝑆) = (Base‘𝑄)
5		yoneda.o	. . . . 5 ⊢ 𝑂 = (oppCat‘𝐶)
6		yoneda.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐶)
7	5, 6	oppcbas 16425	. . . 4 ⊢ 𝐵 = (Base‘𝑂)
8	2, 4, 7	xpcbas 16865	. . 3 ⊢ ((𝑂 Func 𝑆) × 𝐵) = (Base‘(𝑄 ×c 𝑂))
9		eqid 2651	. . 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 16959	. . . 4 ⊢ (𝜑 → (𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)))
22	21	simpld 474	. . 3 ⊢ (𝜑 → 𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇))
23	21	simprd 478	. . 3 ⊢ (𝜑 → 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇))
24		yonedainv.i	. . 3 ⊢ 𝐼 = (Inv‘𝑅)
25		eqid 2651	. . 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 16967	. . 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 809	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ℎ ∈ (𝑂 Func 𝑆))
33		simprr 811	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → 𝑤 ∈ 𝐵)
34	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33, 26	yonedalem3a 16961	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))) ∧ (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤)))
35	34	simprd 478	. . . . . . . . 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 817	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → ℎ ∈ (𝑂 Func 𝑆))
41		simplrr 818	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑤 ∈ 𝐵)
42		yonedainv.n	. . . . . . . . . . . 12 ⊢ 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))))
43		simpr 476	. . . . . . . . . . . 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 16964	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑁𝑤)‘𝑏) ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
45		eqid 2651	. . . . . . . . . . 11 ⊢ (𝑏 ∈ ((1st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏)) = (𝑏 ∈ ((1st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏))
46	44, 45	fmptd 6425	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑏 ∈ ((1st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏)):((1st ‘ℎ)‘𝑤)⟶(((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
47		fvex 6239	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐶) ∈ V
48	6, 47	eqeltri 2726	. . . . . . . . . . . . . . 15 ⊢ 𝐵 ∈ V
49	48	mptex 6527	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢))) ∈ V
50		eqid 2651	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))) = (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢))))
51	49, 50	fnmpti 6060	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))) Fn ((1st ‘ℎ)‘𝑤)
52		simpl 472	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → 𝑓 = ℎ)
53	52	fveq2d 6233	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → (1st ‘𝑓) = (1st ‘ℎ))
54		simpr 476	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → 𝑥 = 𝑤)
55	53, 54	fveq12d 6235	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → ((1st ‘𝑓)‘𝑥) = ((1st ‘ℎ)‘𝑤))
56		simplr 807	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → 𝑥 = 𝑤)
57	56	oveq2d 6706	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (𝑦(Hom ‘𝐶)𝑥) = (𝑦(Hom ‘𝐶)𝑤))
58		simpll 805	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → 𝑓 = ℎ)
59	58	fveq2d 6233	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (2nd ‘𝑓) = (2nd ‘ℎ))
60		eqidd 2652	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → 𝑦 = 𝑦)
61	59, 56, 60	oveq123d 6711	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (𝑥(2nd ‘𝑓)𝑦) = (𝑤(2nd ‘ℎ)𝑦))
62	61	fveq1d 6231	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → ((𝑥(2nd ‘𝑓)𝑦)‘𝑔) = ((𝑤(2nd ‘ℎ)𝑦)‘𝑔))
63	62	fveq1d 6231	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢) = (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢))
64	57, 63	mpteq12dv 4766	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢)) = (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))
65	64	mpteq2dva 4777	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢))) = (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢))))
66	55, 65	mpteq12dv 4766	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))) = (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))))
67		fvex 6239	. . . . . . . . . . . . . . . . 17 ⊢ ((1st ‘ℎ)‘𝑤) ∈ V
68	67	mptex 6527	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))) ∈ V
69	66, 42, 68	ovmpt2a 6833	. . . . . . . . . . . . . . 15 ⊢ ((ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵) → (ℎ𝑁𝑤) = (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))))
70	69	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤) = (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))))
71	70	fneq1d 6019	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑁𝑤) Fn ((1st ‘ℎ)‘𝑤) ↔ (𝑢 ∈ ((1st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))) Fn ((1st ‘ℎ)‘𝑤)))
72	51, 71	mpbiri 248	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤) Fn ((1st ‘ℎ)‘𝑤))
73		dffn5 6280	. . . . . . . . . . . 12 ⊢ ((ℎ𝑁𝑤) Fn ((1st ‘ℎ)‘𝑤) ↔ (ℎ𝑁𝑤) = (𝑏 ∈ ((1st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏)))
74	72, 73	sylib 208	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤) = (𝑏 ∈ ((1st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏)))
75	5	oppccat 16429	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat)
76	17, 75	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑂 ∈ Cat)
77	76	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → 𝑂 ∈ Cat)
78	20	unssbd 3824	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 ⊆ 𝑉)
79	18, 78	ssexd 4838	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ∈ V)
80	12	setccat 16782	. . . . . . . . . . . . . 14 ⊢ (𝑈 ∈ V → 𝑆 ∈ Cat)
81	79, 80	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ∈ Cat)
82	81	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → 𝑆 ∈ Cat)
83	15, 77, 82, 7, 32, 33	evlf1 16907	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ(1st ‘𝐸)𝑤) = ((1st ‘ℎ)‘𝑤))
84	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33	yonedalem21 16960	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ(1st ‘𝑍)𝑤) = (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
85	74, 83, 84	feq123d 6072	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑁𝑤):(ℎ(1st ‘𝐸)𝑤)⟶(ℎ(1st ‘𝑍)𝑤) ↔ (𝑏 ∈ ((1st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏)):((1st ‘ℎ)‘𝑤)⟶(((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ)))
86	46, 85	mpbird 247	. . . . . . . . 9 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤):(ℎ(1st ‘𝐸)𝑤)⟶(ℎ(1st ‘𝑍)𝑤))
87		fcompt 6440	. . . . . . . . . . 11 ⊢ (((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤):(ℎ(1st ‘𝐸)𝑤)⟶(ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑀𝑤) ∘ (ℎ𝑁𝑤)) = (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘))))
88	35, 86, 87	syl2anc 694	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤) ∘ (ℎ𝑁𝑤)) = (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘))))
89	83	eleq2d 2716	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↔ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)))
90	89	biimpa 500	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ (ℎ(1st ‘𝐸)𝑤)) → 𝑘 ∈ ((1st ‘ℎ)‘𝑤))
91	28	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → 𝐶 ∈ Cat)
92	29	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑉 ∈ 𝑊)
93	30	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ran (Homf ‘𝐶) ⊆ 𝑈)
94	31	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
95		simplrl 817	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ℎ ∈ (𝑂 Func 𝑆))
96		simplrr 818	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑤 ∈ 𝐵)
97	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 91, 92, 93, 94, 95, 96, 26	yonedalem3a 16961	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑀𝑤) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))) ∧ (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤)))
98	97	simpld 474	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (ℎ𝑀𝑤) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))))
99	98	fveq1d 6231	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘)) = ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘((ℎ𝑁𝑤)‘𝑘)))
100		fvexd 6241	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑁𝑤)‘𝑏) ∈ V)
101	100, 74, 44	fmpt2d 6433	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤):((1st ‘ℎ)‘𝑤)⟶(((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
102	101	ffvelrnda 6399	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑁𝑤)‘𝑘) ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
103		fveq1 6228	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ((ℎ𝑁𝑤)‘𝑘) → (𝑎‘𝑤) = (((ℎ𝑁𝑤)‘𝑘)‘𝑤))
104	103	fveq1d 6231	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ((ℎ𝑁𝑤)‘𝑘) → ((𝑎‘𝑤)‘( 1 ‘𝑤)) = ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)))
105		eqid 2651	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))
106		fvex 6239	. . . . . . . . . . . . . . . 16 ⊢ ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)) ∈ V
107	104, 105, 106	fvmpt 6321	. . . . . . . . . . . . . . 15 ⊢ (((ℎ𝑁𝑤)‘𝑘) ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) → ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘((ℎ𝑁𝑤)‘𝑘)) = ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)))
108	102, 107	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘((ℎ𝑁𝑤)‘𝑘)) = ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)))
109		simpr 476	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑘 ∈ ((1st ‘ℎ)‘𝑤))
110		eqid 2651	. . . . . . . . . . . . . . . . 17 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
111	6, 110, 11, 91, 96	catidcl 16390	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ( 1 ‘𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤))
112	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 91, 92, 93, 94, 95, 96, 42, 109, 96, 111	yonedalem4b 16963	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)) = (((𝑤(2nd ‘ℎ)𝑤)‘( 1 ‘𝑤))‘𝑘))
113		eqid 2651	. . . . . . . . . . . . . . . . . 18 ⊢ (Id‘𝑂) = (Id‘𝑂)
114		eqid 2651	. . . . . . . . . . . . . . . . . 18 ⊢ (Id‘𝑆) = (Id‘𝑆)
115		relfunc 16569	. . . . . . . . . . . . . . . . . . 19 ⊢ Rel (𝑂 Func 𝑆)
116		1st2ndbr 7261	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Rel (𝑂 Func 𝑆) ∧ ℎ ∈ (𝑂 Func 𝑆)) → (1st ‘ℎ)(𝑂 Func 𝑆)(2nd ‘ℎ))
117	115, 95, 116	sylancr 696	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (1st ‘ℎ)(𝑂 Func 𝑆)(2nd ‘ℎ))
118	7, 113, 114, 117, 96	funcid 16577	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((𝑤(2nd ‘ℎ)𝑤)‘((Id‘𝑂)‘𝑤)) = ((Id‘𝑆)‘((1st ‘ℎ)‘𝑤)))
119	5, 11	oppcid 16428	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐶 ∈ Cat → (Id‘𝑂) = 1 )
120	91, 119	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (Id‘𝑂) = 1 )
121	120	fveq1d 6231	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((Id‘𝑂)‘𝑤) = ( 1 ‘𝑤))
122	121	fveq2d 6233	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((𝑤(2nd ‘ℎ)𝑤)‘((Id‘𝑂)‘𝑤)) = ((𝑤(2nd ‘ℎ)𝑤)‘( 1 ‘𝑤)))
123	79	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑈 ∈ V)
124		eqid 2651	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Base‘𝑆) = (Base‘𝑆)
125	7, 124, 117	funcf1 16573	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (1st ‘ℎ):𝐵⟶(Base‘𝑆))
126	12, 123	setcbas 16775	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → 𝑈 = (Base‘𝑆))
127	126	feq3d 6070	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((1st ‘ℎ):𝐵⟶𝑈 ↔ (1st ‘ℎ):𝐵⟶(Base‘𝑆)))
128	125, 127	mpbird 247	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (1st ‘ℎ):𝐵⟶𝑈)
129	128, 96	ffvelrnd 6400	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((1st ‘ℎ)‘𝑤) ∈ 𝑈)
130	12, 114, 123, 129	setcid 16783	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((Id‘𝑆)‘((1st ‘ℎ)‘𝑤)) = ( I ↾ ((1st ‘ℎ)‘𝑤)))
131	118, 122, 130	3eqtr3d 2693	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((𝑤(2nd ‘ℎ)𝑤)‘( 1 ‘𝑤)) = ( I ↾ ((1st ‘ℎ)‘𝑤)))
132	131	fveq1d 6231	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (((𝑤(2nd ‘ℎ)𝑤)‘( 1 ‘𝑤))‘𝑘) = (( I ↾ ((1st ‘ℎ)‘𝑤))‘𝑘))
133		fvresi 6480	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ((1st ‘ℎ)‘𝑤) → (( I ↾ ((1st ‘ℎ)‘𝑤))‘𝑘) = 𝑘)
134	133	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → (( I ↾ ((1st ‘ℎ)‘𝑤))‘𝑘) = 𝑘)
135	112, 132, 134	3eqtrd 2689	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)) = 𝑘)
136	99, 108, 135	3eqtrd 2689	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1st ‘ℎ)‘𝑤)) → ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘)) = 𝑘)
137	90, 136	syldan 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ (ℎ(1st ‘𝐸)𝑤)) → ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘)) = 𝑘)
138	137	mpteq2dva 4777	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘))) = (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ 𝑘))
139		mptresid 5491	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ 𝑘) = ( I ↾ (ℎ(1st ‘𝐸)𝑤))
140	138, 139	syl6eq 2701	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑘 ∈ (ℎ(1st ‘𝐸)𝑤) ↦ ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘))) = ( I ↾ (ℎ(1st ‘𝐸)𝑤)))
141	88, 140	eqtrd 2685	. . . . . . . . 9 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤) ∘ (ℎ𝑁𝑤)) = ( I ↾ (ℎ(1st ‘𝐸)𝑤)))
142		fcompt 6440	. . . . . . . . . . 11 ⊢ (((ℎ𝑁𝑤):(ℎ(1st ‘𝐸)𝑤)⟶(ℎ(1st ‘𝑍)𝑤) ∧ (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤)) → ((ℎ𝑁𝑤) ∘ (ℎ𝑀𝑤)) = (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))))
143	86, 35, 142	syl2anc 694	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑁𝑤) ∘ (ℎ𝑀𝑤)) = (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))))
144		eqid 2651	. . . . . . . . . . . . . 14 ⊢ (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆)
145	28	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝐶 ∈ Cat)
146	29	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑉 ∈ 𝑊)
147	30	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ran (Homf ‘𝐶) ⊆ 𝑈)
148	31	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
149		simplrl 817	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ℎ ∈ (𝑂 Func 𝑆))
150		simplrr 818	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑤 ∈ 𝐵)
151	83	feq3d 6070	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤) ↔ (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶((1st ‘ℎ)‘𝑤)))
152	35, 151	mpbid 222	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶((1st ‘ℎ)‘𝑤))
153	152	ffvelrnda 6399	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑀𝑤)‘𝑏) ∈ ((1st ‘ℎ)‘𝑤))
154	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 145, 146, 147, 148, 149, 150, 42, 153	yonedalem4c 16964	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
155	144, 154	nat1st2nd 16658	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) ∈ (⟨(1st ‘((1st ‘𝑌)‘𝑤)), (2nd ‘((1st ‘𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st ‘ℎ), (2nd ‘ℎ)⟩))
156	144, 155, 7	natfn 16661	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) Fn 𝐵)
157	84	eleq2d 2716	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↔ 𝑏 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ)))
158	157	biimpa 500	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑏 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
159	144, 158	nat1st2nd 16658	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑏 ∈ (⟨(1st ‘((1st ‘𝑌)‘𝑤)), (2nd ‘((1st ‘𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st ‘ℎ), (2nd ‘ℎ)⟩))
160	144, 159, 7	natfn 16661	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑏 Fn 𝐵)
161	145	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → 𝐶 ∈ Cat)
162	150	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → 𝑤 ∈ 𝐵)
163		simpr 476	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵)
164	10, 6, 161, 162, 110, 163	yon11 16951	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) = (𝑧(Hom ‘𝐶)𝑤))
165	164	eleq2d 2716	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑘 ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) ↔ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))
166	165	biimpa 500	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)) → 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤))
167	161	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝐶 ∈ Cat)
168	146	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑉 ∈ 𝑊)
169	147	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ran (Homf ‘𝐶) ⊆ 𝑈)
170	148	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ran (Homf ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
171	149	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ℎ ∈ (𝑂 Func 𝑆))
172	162	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑤 ∈ 𝐵)
173	153	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ𝑀𝑤)‘𝑏) ∈ ((1st ‘ℎ)‘𝑤))
174		simplr 807	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑧 ∈ 𝐵)
175		simpr 476	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤))
176	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 167, 168, 169, 170, 171, 172, 42, 173, 174, 175	yonedalem4b 16963	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((ℎ𝑀𝑤)‘𝑏)))
177	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 167, 168, 169, 170, 171, 172, 26	yonedalem3a 16961	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ𝑀𝑤) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))) ∧ (ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤)))
178	177	simpld 474	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ℎ𝑀𝑤) = (𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))))
179	178	fveq1d 6231	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ𝑀𝑤)‘𝑏) = ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘𝑏))
180	158	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑏 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
181		fveq1 6228	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑏 → (𝑎‘𝑤) = (𝑏‘𝑤))
182	181	fveq1d 6231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑏 → ((𝑎‘𝑤)‘( 1 ‘𝑤)) = ((𝑏‘𝑤)‘( 1 ‘𝑤)))
183		fvex 6239	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏‘𝑤)‘( 1 ‘𝑤)) ∈ V
184	182, 105, 183	fvmpt 6321	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) → ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘𝑏) = ((𝑏‘𝑤)‘( 1 ‘𝑤)))
185	180, 184	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑎 ∈ (((1st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘𝑏) = ((𝑏‘𝑤)‘( 1 ‘𝑤)))
186	179, 185	eqtrd 2685	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ𝑀𝑤)‘𝑏) = ((𝑏‘𝑤)‘( 1 ‘𝑤)))
187	186	fveq2d 6233	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((ℎ𝑀𝑤)‘𝑏)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))))
188	159	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑏 ∈ (⟨(1st ‘((1st ‘𝑌)‘𝑤)), (2nd ‘((1st ‘𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st ‘ℎ), (2nd ‘ℎ)⟩))
189		eqid 2651	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Hom ‘𝑂) = (Hom ‘𝑂)
190		eqid 2651	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (comp‘𝑆) = (comp‘𝑆)
191	110, 5	oppchom 16422	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤(Hom ‘𝑂)𝑧) = (𝑧(Hom ‘𝐶)𝑤)
192	175, 191	syl6eleqr 2741	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑘 ∈ (𝑤(Hom ‘𝑂)𝑧))
193	144, 188, 7, 189, 190, 172, 174, 192	nati 16662	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧)(⟨((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤), ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)⟩(comp‘𝑆)((1st ‘ℎ)‘𝑧))((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)(⟨((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤), ((1st ‘ℎ)‘𝑤)⟩(comp‘𝑆)((1st ‘ℎ)‘𝑧))(𝑏‘𝑤)))
194	79	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑈 ∈ V)
195	194	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → 𝑈 ∈ V)
196	195	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑈 ∈ V)
197		relfunc 16569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ Rel (𝐶 Func 𝑄)
198	10, 17, 5, 12, 3, 79, 19	yoncl 16949	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → 𝑌 ∈ (𝐶 Func 𝑄))
199		1st2ndbr 7261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((Rel (𝐶 Func 𝑄) ∧ 𝑌 ∈ (𝐶 Func 𝑄)) → (1st ‘𝑌)(𝐶 Func 𝑄)(2nd ‘𝑌))
200	197, 198, 199	sylancr 696	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (1st ‘𝑌)(𝐶 Func 𝑄)(2nd ‘𝑌))
201	6, 4, 200	funcf1 16573	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (1st ‘𝑌):𝐵⟶(𝑂 Func 𝑆))
202	201	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘𝑌):𝐵⟶(𝑂 Func 𝑆))
203	202, 150	ffvelrnd 6400	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘𝑌)‘𝑤) ∈ (𝑂 Func 𝑆))
204		1st2ndbr 7261	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Rel (𝑂 Func 𝑆) ∧ ((1st ‘𝑌)‘𝑤) ∈ (𝑂 Func 𝑆)) → (1st ‘((1st ‘𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st ‘𝑌)‘𝑤)))
205	115, 203, 204	sylancr 696	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘((1st ‘𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st ‘𝑌)‘𝑤)))
206	7, 124, 205	funcf1 16573	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘((1st ‘𝑌)‘𝑤)):𝐵⟶(Base‘𝑆))
207	12, 194	setcbas 16775	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → 𝑈 = (Base‘𝑆))
208	207	feq3d 6070	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘((1st ‘𝑌)‘𝑤)):𝐵⟶𝑈 ↔ (1st ‘((1st ‘𝑌)‘𝑤)):𝐵⟶(Base‘𝑆)))
209	206, 208	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘((1st ‘𝑌)‘𝑤)):𝐵⟶𝑈)
210	209, 150	ffvelrnd 6400	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤) ∈ 𝑈)
211	210	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤) ∈ 𝑈)
212	209	ffvelrnda 6399	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) ∈ 𝑈)
213	212	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) ∈ 𝑈)
214	115, 149, 116	sylancr 696	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘ℎ)(𝑂 Func 𝑆)(2nd ‘ℎ))
215	7, 124, 214	funcf1 16573	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘ℎ):𝐵⟶(Base‘𝑆))
216	207	feq3d 6070	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘ℎ):𝐵⟶𝑈 ↔ (1st ‘ℎ):𝐵⟶(Base‘𝑆)))
217	215, 216	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (1st ‘ℎ):𝐵⟶𝑈)
218	217	ffvelrnda 6399	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((1st ‘ℎ)‘𝑧) ∈ 𝑈)
219	218	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘ℎ)‘𝑧) ∈ 𝑈)
220		eqid 2651	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Hom ‘𝑆) = (Hom ‘𝑆)
221	205	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1st ‘((1st ‘𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st ‘𝑌)‘𝑤)))
222	7, 189, 220, 221, 172, 174	funcf2 16575	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧):(𝑤(Hom ‘𝑂)𝑧)⟶(((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)))
223	222, 192	ffvelrnd 6400	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)))
224	12, 196, 220, 211, 213	elsetchom 16778	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)) ↔ ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)⟶((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)))
225	223, 224	mpbid 222	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)⟶((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧))
226	159	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → 𝑏 ∈ (⟨(1st ‘((1st ‘𝑌)‘𝑤)), (2nd ‘((1st ‘𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st ‘ℎ), (2nd ‘ℎ)⟩))
227	144, 226, 7, 220, 163	natcl 16660	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑏‘𝑧) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)))
228	12, 195, 220, 212, 218	elsetchom 16778	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((𝑏‘𝑧) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)) ↔ (𝑏‘𝑧):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)⟶((1st ‘ℎ)‘𝑧)))
229	227, 228	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑏‘𝑧):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)⟶((1st ‘ℎ)‘𝑧))
230	229	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑏‘𝑧):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)⟶((1st ‘ℎ)‘𝑧))
231	12, 196, 190, 211, 213, 219, 225, 230	setcco 16780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧)(⟨((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤), ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)⟩(comp‘𝑆)((1st ‘ℎ)‘𝑧))((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)) = ((𝑏‘𝑧) ∘ ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)))
232	217, 150	ffvelrnd 6400	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘ℎ)‘𝑤) ∈ 𝑈)
233	232	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st ‘ℎ)‘𝑤) ∈ 𝑈)
234	144, 159, 7, 220, 150	natcl 16660	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (𝑏‘𝑤) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘ℎ)‘𝑤)))
235	12, 194, 220, 210, 232	elsetchom 16778	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((𝑏‘𝑤) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1st ‘ℎ)‘𝑤)) ↔ (𝑏‘𝑤):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)⟶((1st ‘ℎ)‘𝑤)))
236	234, 235	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → (𝑏‘𝑤):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)⟶((1st ‘ℎ)‘𝑤))
237	236	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑏‘𝑤):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)⟶((1st ‘ℎ)‘𝑤))
238	115, 171, 116	sylancr 696	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1st ‘ℎ)(𝑂 Func 𝑆)(2nd ‘ℎ))
239	7, 189, 220, 238, 172, 174	funcf2 16575	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑤(2nd ‘ℎ)𝑧):(𝑤(Hom ‘𝑂)𝑧)⟶(((1st ‘ℎ)‘𝑤)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)))
240	239, 192	ffvelrnd 6400	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∈ (((1st ‘ℎ)‘𝑤)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)))
241	12, 196, 220, 233, 219	elsetchom 16778	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∈ (((1st ‘ℎ)‘𝑤)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)) ↔ ((𝑤(2nd ‘ℎ)𝑧)‘𝑘):((1st ‘ℎ)‘𝑤)⟶((1st ‘ℎ)‘𝑧)))
242	240, 241	mpbid 222	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2nd ‘ℎ)𝑧)‘𝑘):((1st ‘ℎ)‘𝑤)⟶((1st ‘ℎ)‘𝑧))
243	12, 196, 190, 211, 233, 219, 237, 242	setcco 16780	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)(⟨((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤), ((1st ‘ℎ)‘𝑤)⟩(comp‘𝑆)((1st ‘ℎ)‘𝑧))(𝑏‘𝑤)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤)))
244	193, 231, 243	3eqtr3d 2693	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧) ∘ ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤)))
245	244	fveq1d 6231	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑏‘𝑧) ∘ ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘))‘( 1 ‘𝑤)) = ((((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤))‘( 1 ‘𝑤)))
246	6, 110, 11, 145, 150	catidcl 16390	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ( 1 ‘𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤))
247	10, 6, 145, 150, 110, 150	yon11 16951	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤) = (𝑤(Hom ‘𝐶)𝑤))
248	246, 247	eleqtrrd 2733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ( 1 ‘𝑤) ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤))
249	248	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ( 1 ‘𝑤) ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤))
250		fvco3 6314	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)⟶((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) ∧ ( 1 ‘𝑤) ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)) → (((𝑏‘𝑧) ∘ ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘))‘( 1 ‘𝑤)) = ((𝑏‘𝑧)‘(((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤))))
251	225, 249, 250	syl2anc 694	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑏‘𝑧) ∘ ((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘))‘( 1 ‘𝑤)) = ((𝑏‘𝑧)‘(((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤))))
252		fvco3 6314	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑏‘𝑤):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)⟶((1st ‘ℎ)‘𝑤) ∧ ( 1 ‘𝑤) ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑤)) → ((((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤))‘( 1 ‘𝑤)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))))
253	236, 248, 252	syl2anc 694	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤))‘( 1 ‘𝑤)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))))
254	253	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((𝑤(2nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤))‘( 1 ‘𝑤)) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))))
255	245, 251, 254	3eqtr3d 2693	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧)‘(((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤))) = (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))))
256		eqid 2651	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (comp‘𝐶) = (comp‘𝐶)
257	246	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ( 1 ‘𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤))
258	10, 6, 167, 172, 110, 172, 256, 174, 175, 257	yon12 16952	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤)) = (( 1 ‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐶)𝑤)𝑘))
259	6, 110, 11, 167, 174, 256, 172, 175	catlid 16391	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (( 1 ‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐶)𝑤)𝑘) = 𝑘)
260	258, 259	eqtrd 2685	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤)) = 𝑘)
261	260	fveq2d 6233	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧)‘(((𝑤(2nd ‘((1st ‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤))) = ((𝑏‘𝑧)‘𝑘))
262	255, 261	eqtr3d 2687	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))) = ((𝑏‘𝑧)‘𝑘))
263	176, 187, 262	3eqtrd 2689	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = ((𝑏‘𝑧)‘𝑘))
264	166, 263	syldan 486	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)) → ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = ((𝑏‘𝑧)‘𝑘))
265	264	mpteq2dva 4777	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑘 ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) ↦ ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘)) = (𝑘 ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) ↦ ((𝑏‘𝑧)‘𝑘)))
266	155	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) ∈ (⟨(1st ‘((1st ‘𝑌)‘𝑤)), (2nd ‘((1st ‘𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1st ‘ℎ), (2nd ‘ℎ)⟩))
267	144, 266, 7, 220, 163	natcl 16660	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)))
268	12, 195, 220, 212, 218	elsetchom 16778	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧) ∈ (((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1st ‘ℎ)‘𝑧)) ↔ (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)⟶((1st ‘ℎ)‘𝑧)))
269	267, 268	mpbid 222	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧):((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧)⟶((1st ‘ℎ)‘𝑧))
270	269	feqmptd 6288	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧) = (𝑘 ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) ↦ ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘)))
271	229	feqmptd 6288	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑏‘𝑧) = (𝑘 ∈ ((1st ‘((1st ‘𝑌)‘𝑤))‘𝑧) ↦ ((𝑏‘𝑧)‘𝑘)))
272	265, 270, 271	3eqtr4d 2695	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧) = (𝑏‘𝑧))
273	156, 160, 272	eqfnfvd 6354	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1st ‘𝑍)𝑤)) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) = 𝑏)
274	273	mpteq2dva 4777	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))) = (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ 𝑏))
275		mptresid 5491	. . . . . . . . . . 11 ⊢ (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ 𝑏) = ( I ↾ (ℎ(1st ‘𝑍)𝑤))
276	274, 275	syl6eq 2701	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑏 ∈ (ℎ(1st ‘𝑍)𝑤) ↦ ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))) = ( I ↾ (ℎ(1st ‘𝑍)𝑤)))
277	143, 276	eqtrd 2685	. . . . . . . . 9 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑁𝑤) ∘ (ℎ𝑀𝑤)) = ( I ↾ (ℎ(1st ‘𝑍)𝑤)))
278		fcof1o 6591	. . . . . . . . 9 ⊢ ((((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)⟶(ℎ(1st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤):(ℎ(1st ‘𝐸)𝑤)⟶(ℎ(1st ‘𝑍)𝑤)) ∧ (((ℎ𝑀𝑤) ∘ (ℎ𝑁𝑤)) = ( I ↾ (ℎ(1st ‘𝐸)𝑤)) ∧ ((ℎ𝑁𝑤) ∘ (ℎ𝑀𝑤)) = ( I ↾ (ℎ(1st ‘𝑍)𝑤)))) → ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ ◡(ℎ𝑀𝑤) = (ℎ𝑁𝑤)))
279	35, 86, 141, 277, 278	syl22anc 1367	. . . . . . . 8 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ ◡(ℎ𝑀𝑤) = (ℎ𝑁𝑤)))
280		eqcom 2658	. . . . . . . . 9 ⊢ (◡(ℎ𝑀𝑤) = (ℎ𝑁𝑤) ↔ (ℎ𝑁𝑤) = ◡(ℎ𝑀𝑤))
281	280	anbi2i 730	. . . . . . . 8 ⊢ (((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ ◡(ℎ𝑀𝑤) = (ℎ𝑁𝑤)) ↔ ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤) = ◡(ℎ𝑀𝑤)))
282	279, 281	sylib 208	. . . . . . 7 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤) = ◡(ℎ𝑀𝑤)))
283		eqid 2651	. . . . . . . . . . 11 ⊢ (Base‘𝑇) = (Base‘𝑇)
284		relfunc 16569	. . . . . . . . . . . 12 ⊢ Rel ((𝑄 ×c 𝑂) Func 𝑇)
285		1st2ndbr 7261	. . . . . . . . . . . 12 ⊢ ((Rel ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st ‘𝑍)((𝑄 ×c 𝑂) Func 𝑇)(2nd ‘𝑍))
286	284, 22, 285	sylancr 696	. . . . . . . . . . 11 ⊢ (𝜑 → (1st ‘𝑍)((𝑄 ×c 𝑂) Func 𝑇)(2nd ‘𝑍))
287	8, 283, 286	funcf1 16573	. . . . . . . . . 10 ⊢ (𝜑 → (1st ‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
288	13, 18	setcbas 16775	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 = (Base‘𝑇))
289	288	feq3d 6070	. . . . . . . . . 10 ⊢ (𝜑 → ((1st ‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶𝑉 ↔ (1st ‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇)))
290	287, 289	mpbird 247	. . . . . . . . 9 ⊢ (𝜑 → (1st ‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶𝑉)
291	290	fovrnda 6847	. . . . . . . 8 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ(1st ‘𝑍)𝑤) ∈ 𝑉)
292		1st2ndbr 7261	. . . . . . . . . . . 12 ⊢ ((Rel ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)) → (1st ‘𝐸)((𝑄 ×c 𝑂) Func 𝑇)(2nd ‘𝐸))
293	284, 23, 292	sylancr 696	. . . . . . . . . . 11 ⊢ (𝜑 → (1st ‘𝐸)((𝑄 ×c 𝑂) Func 𝑇)(2nd ‘𝐸))
294	8, 283, 293	funcf1 16573	. . . . . . . . . 10 ⊢ (𝜑 → (1st ‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
295	288	feq3d 6070	. . . . . . . . . 10 ⊢ (𝜑 → ((1st ‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶𝑉 ↔ (1st ‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇)))
296	294, 295	mpbird 247	. . . . . . . . 9 ⊢ (𝜑 → (1st ‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶𝑉)
297	296	fovrnda 6847	. . . . . . . 8 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ(1st ‘𝐸)𝑤) ∈ 𝑉)
298	13, 29, 291, 297, 25	setcinv 16787	. . . . . . 7 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤)((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤))(ℎ𝑁𝑤) ↔ ((ℎ𝑀𝑤):(ℎ(1st ‘𝑍)𝑤)–1-1-onto→(ℎ(1st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤) = ◡(ℎ𝑀𝑤))))
299	282, 298	mpbird 247	. . . . . 6 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑀𝑤)((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤))(ℎ𝑁𝑤))
300	299	ralrimivva 3000	. . . . 5 ⊢ (𝜑 → ∀ℎ ∈ (𝑂 Func 𝑆)∀𝑤 ∈ 𝐵 (ℎ𝑀𝑤)((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤))(ℎ𝑁𝑤))
301		fveq2 6229	. . . . . . . 8 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → (𝑀‘𝑧) = (𝑀‘⟨ℎ, 𝑤⟩))
302		df-ov 6693	. . . . . . . 8 ⊢ (ℎ𝑀𝑤) = (𝑀‘⟨ℎ, 𝑤⟩)
303	301, 302	syl6eqr 2703	. . . . . . 7 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → (𝑀‘𝑧) = (ℎ𝑀𝑤))
304		fveq2 6229	. . . . . . . . 9 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → ((1st ‘𝑍)‘𝑧) = ((1st ‘𝑍)‘⟨ℎ, 𝑤⟩))
305		df-ov 6693	. . . . . . . . 9 ⊢ (ℎ(1st ‘𝑍)𝑤) = ((1st ‘𝑍)‘⟨ℎ, 𝑤⟩)
306	304, 305	syl6eqr 2703	. . . . . . . 8 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → ((1st ‘𝑍)‘𝑧) = (ℎ(1st ‘𝑍)𝑤))
307		fveq2 6229	. . . . . . . . 9 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → ((1st ‘𝐸)‘𝑧) = ((1st ‘𝐸)‘⟨ℎ, 𝑤⟩))
308		df-ov 6693	. . . . . . . . 9 ⊢ (ℎ(1st ‘𝐸)𝑤) = ((1st ‘𝐸)‘⟨ℎ, 𝑤⟩)
309	307, 308	syl6eqr 2703	. . . . . . . 8 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → ((1st ‘𝐸)‘𝑧) = (ℎ(1st ‘𝐸)𝑤))
310	306, 309	oveq12d 6708	. . . . . . 7 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → (((1st ‘𝑍)‘𝑧)(Inv‘𝑇)((1st ‘𝐸)‘𝑧)) = ((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤)))
311		fveq2 6229	. . . . . . . 8 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → (𝑁‘𝑧) = (𝑁‘⟨ℎ, 𝑤⟩))
312		df-ov 6693	. . . . . . . 8 ⊢ (ℎ𝑁𝑤) = (𝑁‘⟨ℎ, 𝑤⟩)
313	311, 312	syl6eqr 2703	. . . . . . 7 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → (𝑁‘𝑧) = (ℎ𝑁𝑤))
314	303, 310, 313	breq123d 4699	. . . . . 6 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → ((𝑀‘𝑧)(((1st ‘𝑍)‘𝑧)(Inv‘𝑇)((1st ‘𝐸)‘𝑧))(𝑁‘𝑧) ↔ (ℎ𝑀𝑤)((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤))(ℎ𝑁𝑤)))
315	314	ralxp 5296	. . . . 5 ⊢ (∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑀‘𝑧)(((1st ‘𝑍)‘𝑧)(Inv‘𝑇)((1st ‘𝐸)‘𝑧))(𝑁‘𝑧) ↔ ∀ℎ ∈ (𝑂 Func 𝑆)∀𝑤 ∈ 𝐵 (ℎ𝑀𝑤)((ℎ(1st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1st ‘𝐸)𝑤))(ℎ𝑁𝑤))
316	300, 315	sylibr 224	. . . 4 ⊢ (𝜑 → ∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑀‘𝑧)(((1st ‘𝑍)‘𝑧)(Inv‘𝑇)((1st ‘𝐸)‘𝑧))(𝑁‘𝑧))
317	316	r19.21bi 2961	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)) → (𝑀‘𝑧)(((1st ‘𝑍)‘𝑧)(Inv‘𝑇)((1st ‘𝐸)‘𝑧))(𝑁‘𝑧))
318	1, 8, 9, 22, 23, 24, 25, 27, 317	invfuc 16681	. 2 ⊢ (𝜑 → 𝑀(𝑍𝐼𝐸)(𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁‘𝑧)))
319		fvex 6239	. . . . 5 ⊢ ((1st ‘𝑓)‘𝑥) ∈ V
320	319	mptex 6527	. . . 4 ⊢ (𝑢 ∈ ((1st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))) ∈ V
321	42, 320	fnmpt2i 7284	. . 3 ⊢ 𝑁 Fn ((𝑂 Func 𝑆) × 𝐵)
322		dffn5 6280	. . 3 ⊢ (𝑁 Fn ((𝑂 Func 𝑆) × 𝐵) ↔ 𝑁 = (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁‘𝑧)))
323	321, 322	mpbi 220	. 2 ⊢ 𝑁 = (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁‘𝑧))
324	318, 323	syl6breqr 4727	1 ⊢ (𝜑 → 𝑀(𝑍𝐼𝐸)𝑁)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1523   ∈ wcel 2030  ∀wral 2941  Vcvv 3231   ∪ cun 3605   ⊆ wss 3607  ⟨cop 4216   class class class wbr 4685   ↦ cmpt 4762   I cid 5052   × cxp 5141  ^◡ccnv 5142  ran crn 5144   ↾ cres 5145   ∘ ccom 5147  Rel wrel 5148   Fn wfn 5921  ⟶wf 5922  –1-1-onto→wf1o 5925  ‘cfv 5926  (class class class)co 6690   ↦ cmpt2 6692  1^st c1st 7208  2^nd c2nd 7209  tpos ctpos 7396  Basecbs 15904  Hom chom 15999  compcco 16000  Catccat 16372  Idccid 16373  Hom_f chomf 16374  oppCatcoppc 16418  Invcinv 16452   Func cfunc 16561   ∘_func ccofu 16563   Nat cnat 16648   FuncCat cfuc 16649  SetCatcsetc 16772   ×_c cxpc 16855   1^st_F c1stf 16856   2^nd_F c2ndf 16857   ⟨,⟩_F cprf 16858   eval_F cevlf 16896  Hom_Fchof 16935  Yoncyon 16936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-tpos 7397  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-fz 12365  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-hom 16013  df-cco 16014  df-cat 16376  df-cid 16377  df-homf 16378  df-comf 16379  df-oppc 16419  df-sect 16454  df-inv 16455  df-ssc 16517  df-resc 16518  df-subc 16519  df-func 16565  df-cofu 16567  df-nat 16650  df-fuc 16651  df-setc 16773  df-xpc 16859  df-1stf 16860  df-2ndf 16861  df-prf 16862  df-evlf 16900  df-curf 16901  df-hof 16937  df-yon 16938

This theorem is referenced by:  yonffthlem  16969  yoneda  16970