yonedainv - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > yonedainv		Structured version Visualization version GIF version

Theorem yonedainv 18230

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	⊢ 𝐻 = (Hom_F‘𝑄)
yoneda.r	⊢ 𝑅 = ((𝑄 ×_c 𝑂) FuncCat 𝑇)
yoneda.e	⊢ 𝐸 = (𝑂 eval_F 𝑆)
yoneda.z	⊢ 𝑍 = (𝐻 ∘_func ((⟨(1^st ‘𝑌), tpos (2^nd ‘𝑌)⟩ ∘_func (𝑄 2^nd_F 𝑂)) ⟨,⟩_F (𝑄 1^st_F 𝑂)))
yoneda.c	⊢ (𝜑 → 𝐶 ∈ Cat)
yoneda.w	⊢ (𝜑 → 𝑉 ∈ 𝑊)
yoneda.u	⊢ (𝜑 → ran (Hom_f ‘𝐶) ⊆ 𝑈)
yoneda.v	⊢ (𝜑 → (ran (Hom_f ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
yoneda.m	⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1^st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥))))
yonedainv.i	⊢ 𝐼 = (Inv‘𝑅)
yonedainv.n	⊢ 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑢 ∈ ((1^st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2^nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))))

**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 2732	. . . 4 ⊢ (𝑄 ×_c 𝑂) = (𝑄 ×_c 𝑂)
3		yoneda.q	. . . . 5 ⊢ 𝑄 = (𝑂 FuncCat 𝑆)
4	3	fucbas 17908	. . . 4 ⊢ (𝑂 Func 𝑆) = (Base‘𝑄)
5		yoneda.o	. . . . 5 ⊢ 𝑂 = (oppCat‘𝐶)
6		yoneda.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐶)
7	5, 6	oppcbas 17659	. . . 4 ⊢ 𝐵 = (Base‘𝑂)
8	2, 4, 7	xpcbas 18126	. . 3 ⊢ ((𝑂 Func 𝑆) × 𝐵) = (Base‘(𝑄 ×_c 𝑂))
9		eqid 2732	. . 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 ⊢ 𝐻 = (Hom_F‘𝑄)
15		yoneda.e	. . . . 5 ⊢ 𝐸 = (𝑂 eval_F 𝑆)
16		yoneda.z	. . . . 5 ⊢ 𝑍 = (𝐻 ∘_func ((⟨(1^st ‘𝑌), tpos (2^nd ‘𝑌)⟩ ∘_func (𝑄 2^nd_F 𝑂)) ⟨,⟩_F (𝑄 1^st_F 𝑂)))
17		yoneda.c	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ Cat)
18		yoneda.w	. . . . 5 ⊢ (𝜑 → 𝑉 ∈ 𝑊)
19		yoneda.u	. . . . 5 ⊢ (𝜑 → ran (Hom_f ‘𝐶) ⊆ 𝑈)
20		yoneda.v	. . . . 5 ⊢ (𝜑 → (ran (Hom_f ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
21	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 17, 18, 19, 20	yonedalem1 18221	. . . 4 ⊢ (𝜑 → (𝑍 ∈ ((𝑄 ×_c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×_c 𝑂) Func 𝑇)))
22	21	simpld 495	. . 3 ⊢ (𝜑 → 𝑍 ∈ ((𝑄 ×_c 𝑂) Func 𝑇))
23	21	simprd 496	. . 3 ⊢ (𝜑 → 𝐸 ∈ ((𝑄 ×_c 𝑂) Func 𝑇))
24		yonedainv.i	. . 3 ⊢ 𝐼 = (Inv‘𝑅)
25		eqid 2732	. . 3 ⊢ (Inv‘𝑇) = (Inv‘𝑇)
26		yoneda.m	. . . 4 ⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1^st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥))))
27	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 17, 18, 19, 20, 26	yonedalem3 18229	. . 3 ⊢ (𝜑 → 𝑀 ∈ (𝑍((𝑄 ×_c 𝑂) Nat 𝑇)𝐸))
28	17	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → 𝐶 ∈ Cat)
29	18	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → 𝑉 ∈ 𝑊)
30	19	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ran (Hom_f ‘𝐶) ⊆ 𝑈)
31	20	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ran (Hom_f ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
32		simprl 769	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ℎ ∈ (𝑂 Func 𝑆))
33		simprr 771	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → 𝑤 ∈ 𝐵)
34	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33, 26	yonedalem3a 18223	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))) ∧ (ℎ𝑀𝑤):(ℎ(1^st ‘𝑍)𝑤)⟶(ℎ(1^st ‘𝐸)𝑤)))
35	34	simprd 496	. . . . . . . . 9 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑀𝑤):(ℎ(1^st ‘𝑍)𝑤)⟶(ℎ(1^st ‘𝐸)𝑤))
36	28	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1^st ‘ℎ)‘𝑤)) → 𝐶 ∈ Cat)
37	29	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1^st ‘ℎ)‘𝑤)) → 𝑉 ∈ 𝑊)
38	30	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1^st ‘ℎ)‘𝑤)) → ran (Hom_f ‘𝐶) ⊆ 𝑈)
39	31	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1^st ‘ℎ)‘𝑤)) → (ran (Hom_f ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
40		simplrl 775	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1^st ‘ℎ)‘𝑤)) → ℎ ∈ (𝑂 Func 𝑆))
41		simplrr 776	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1^st ‘ℎ)‘𝑤)) → 𝑤 ∈ 𝐵)
42		yonedainv.n	. . . . . . . . . . . 12 ⊢ 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑢 ∈ ((1^st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2^nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))))
43		simpr 485	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1^st ‘ℎ)‘𝑤)) → 𝑏 ∈ ((1^st ‘ℎ)‘𝑤))
44	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 36, 37, 38, 39, 40, 41, 42, 43	yonedalem4c 18226	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ ((1^st ‘ℎ)‘𝑤)) → ((ℎ𝑁𝑤)‘𝑏) ∈ (((1^st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
45	44	fmpttd 7111	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑏 ∈ ((1^st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏)):((1^st ‘ℎ)‘𝑤)⟶(((1^st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
46	6	fvexi 6902	. . . . . . . . . . . . . . 15 ⊢ 𝐵 ∈ V
47	46	mptex 7221	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2^nd ‘ℎ)𝑦)‘𝑔)‘𝑢))) ∈ V
48		eqid 2732	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ ((1^st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2^nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))) = (𝑢 ∈ ((1^st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2^nd ‘ℎ)𝑦)‘𝑔)‘𝑢))))
49	47, 48	fnmpti 6690	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ ((1^st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2^nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))) Fn ((1^st ‘ℎ)‘𝑤)
50		simpl 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → 𝑓 = ℎ)
51	50	fveq2d 6892	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → (1^st ‘𝑓) = (1^st ‘ℎ))
52		simpr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → 𝑥 = 𝑤)
53	51, 52	fveq12d 6895	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → ((1^st ‘𝑓)‘𝑥) = ((1^st ‘ℎ)‘𝑤))
54		simplr 767	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → 𝑥 = 𝑤)
55	54	oveq2d 7421	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (𝑦(Hom ‘𝐶)𝑥) = (𝑦(Hom ‘𝐶)𝑤))
56		simpll 765	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → 𝑓 = ℎ)
57	56	fveq2d 6892	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (2^nd ‘𝑓) = (2^nd ‘ℎ))
58		eqidd 2733	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → 𝑦 = 𝑦)
59	57, 54, 58	oveq123d 7426	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (𝑥(2^nd ‘𝑓)𝑦) = (𝑤(2^nd ‘ℎ)𝑦))
60	59	fveq1d 6890	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → ((𝑥(2^nd ‘𝑓)𝑦)‘𝑔) = ((𝑤(2^nd ‘ℎ)𝑦)‘𝑔))
61	60	fveq1d 6890	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (((𝑥(2^nd ‘𝑓)𝑦)‘𝑔)‘𝑢) = (((𝑤(2^nd ‘ℎ)𝑦)‘𝑔)‘𝑢))
62	55, 61	mpteq12dv 5238	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑓 = ℎ ∧ 𝑥 = 𝑤) ∧ 𝑦 ∈ 𝐵) → (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2^nd ‘𝑓)𝑦)‘𝑔)‘𝑢)) = (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2^nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))
63	62	mpteq2dva 5247	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2^nd ‘𝑓)𝑦)‘𝑔)‘𝑢))) = (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2^nd ‘ℎ)𝑦)‘𝑔)‘𝑢))))
64	53, 63	mpteq12dv 5238	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓 = ℎ ∧ 𝑥 = 𝑤) → (𝑢 ∈ ((1^st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2^nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))) = (𝑢 ∈ ((1^st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2^nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))))
65		fvex 6901	. . . . . . . . . . . . . . . . 17 ⊢ ((1^st ‘ℎ)‘𝑤) ∈ V
66	65	mptex 7221	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ ((1^st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2^nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))) ∈ V
67	64, 42, 66	ovmpoa 7559	. . . . . . . . . . . . . . 15 ⊢ ((ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵) → (ℎ𝑁𝑤) = (𝑢 ∈ ((1^st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2^nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))))
68	67	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤) = (𝑢 ∈ ((1^st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2^nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))))
69	68	fneq1d 6639	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑁𝑤) Fn ((1^st ‘ℎ)‘𝑤) ↔ (𝑢 ∈ ((1^st ‘ℎ)‘𝑤) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑤) ↦ (((𝑤(2^nd ‘ℎ)𝑦)‘𝑔)‘𝑢)))) Fn ((1^st ‘ℎ)‘𝑤)))
70	49, 69	mpbiri 257	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤) Fn ((1^st ‘ℎ)‘𝑤))
71		dffn5 6947	. . . . . . . . . . . 12 ⊢ ((ℎ𝑁𝑤) Fn ((1^st ‘ℎ)‘𝑤) ↔ (ℎ𝑁𝑤) = (𝑏 ∈ ((1^st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏)))
72	70, 71	sylib 217	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤) = (𝑏 ∈ ((1^st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏)))
73	5	oppccat 17664	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat)
74	17, 73	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑂 ∈ Cat)
75	74	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → 𝑂 ∈ Cat)
76	20	unssbd 4187	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑈 ⊆ 𝑉)
77	18, 76	ssexd 5323	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ∈ V)
78	12	setccat 18031	. . . . . . . . . . . . . 14 ⊢ (𝑈 ∈ V → 𝑆 ∈ Cat)
79	77, 78	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ∈ Cat)
80	79	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → 𝑆 ∈ Cat)
81	15, 75, 80, 7, 32, 33	evlf1 18169	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ(1^st ‘𝐸)𝑤) = ((1^st ‘ℎ)‘𝑤))
82	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 28, 29, 30, 31, 32, 33	yonedalem21 18222	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ(1^st ‘𝑍)𝑤) = (((1^st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
83	72, 81, 82	feq123d 6703	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑁𝑤):(ℎ(1^st ‘𝐸)𝑤)⟶(ℎ(1^st ‘𝑍)𝑤) ↔ (𝑏 ∈ ((1^st ‘ℎ)‘𝑤) ↦ ((ℎ𝑁𝑤)‘𝑏)):((1^st ‘ℎ)‘𝑤)⟶(((1^st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ)))
84	45, 83	mpbird 256	. . . . . . . . 9 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤):(ℎ(1^st ‘𝐸)𝑤)⟶(ℎ(1^st ‘𝑍)𝑤))
85		fcompt 7127	. . . . . . . . . . 11 ⊢ (((ℎ𝑀𝑤):(ℎ(1^st ‘𝑍)𝑤)⟶(ℎ(1^st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤):(ℎ(1^st ‘𝐸)𝑤)⟶(ℎ(1^st ‘𝑍)𝑤)) → ((ℎ𝑀𝑤) ∘ (ℎ𝑁𝑤)) = (𝑘 ∈ (ℎ(1^st ‘𝐸)𝑤) ↦ ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘))))
86	35, 84, 85	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤) ∘ (ℎ𝑁𝑤)) = (𝑘 ∈ (ℎ(1^st ‘𝐸)𝑤) ↦ ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘))))
87	81	eleq2d 2819	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑘 ∈ (ℎ(1^st ‘𝐸)𝑤) ↔ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)))
88	87	biimpa 477	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ (ℎ(1^st ‘𝐸)𝑤)) → 𝑘 ∈ ((1^st ‘ℎ)‘𝑤))
89	28	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → 𝐶 ∈ Cat)
90	29	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → 𝑉 ∈ 𝑊)
91	30	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → ran (Hom_f ‘𝐶) ⊆ 𝑈)
92	31	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → (ran (Hom_f ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
93		simplrl 775	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → ℎ ∈ (𝑂 Func 𝑆))
94		simplrr 776	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → 𝑤 ∈ 𝐵)
95	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 89, 90, 91, 92, 93, 94, 26	yonedalem3a 18223	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → ((ℎ𝑀𝑤) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))) ∧ (ℎ𝑀𝑤):(ℎ(1^st ‘𝑍)𝑤)⟶(ℎ(1^st ‘𝐸)𝑤)))
96	95	simpld 495	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → (ℎ𝑀𝑤) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))))
97	96	fveq1d 6890	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘)) = ((𝑎 ∈ (((1^st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘((ℎ𝑁𝑤)‘𝑘)))
98	72, 44	fmpt3d 7112	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑁𝑤):((1^st ‘ℎ)‘𝑤)⟶(((1^st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
99	98	ffvelcdmda 7083	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → ((ℎ𝑁𝑤)‘𝑘) ∈ (((1^st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
100		fveq1 6887	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ((ℎ𝑁𝑤)‘𝑘) → (𝑎‘𝑤) = (((ℎ𝑁𝑤)‘𝑘)‘𝑤))
101	100	fveq1d 6890	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ((ℎ𝑁𝑤)‘𝑘) → ((𝑎‘𝑤)‘( 1 ‘𝑤)) = ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)))
102		eqid 2732	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ (((1^st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))
103		fvex 6901	. . . . . . . . . . . . . . . 16 ⊢ ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)) ∈ V
104	101, 102, 103	fvmpt 6995	. . . . . . . . . . . . . . 15 ⊢ (((ℎ𝑁𝑤)‘𝑘) ∈ (((1^st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) → ((𝑎 ∈ (((1^st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘((ℎ𝑁𝑤)‘𝑘)) = ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)))
105	99, 104	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → ((𝑎 ∈ (((1^st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘((ℎ𝑁𝑤)‘𝑘)) = ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)))
106		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → 𝑘 ∈ ((1^st ‘ℎ)‘𝑤))
107		eqid 2732	. . . . . . . . . . . . . . . . 17 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
108	6, 107, 11, 89, 94	catidcl 17622	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → ( 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 18225	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)) = (((𝑤(2^nd ‘ℎ)𝑤)‘( 1 ‘𝑤))‘𝑘))
110		eqid 2732	. . . . . . . . . . . . . . . . . 18 ⊢ (Id‘𝑂) = (Id‘𝑂)
111		eqid 2732	. . . . . . . . . . . . . . . . . 18 ⊢ (Id‘𝑆) = (Id‘𝑆)
112		relfunc 17808	. . . . . . . . . . . . . . . . . . 19 ⊢ Rel (𝑂 Func 𝑆)
113		1st2ndbr 8024	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Rel (𝑂 Func 𝑆) ∧ ℎ ∈ (𝑂 Func 𝑆)) → (1^st ‘ℎ)(𝑂 Func 𝑆)(2^nd ‘ℎ))
114	112, 93, 113	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → (1^st ‘ℎ)(𝑂 Func 𝑆)(2^nd ‘ℎ))
115	7, 110, 111, 114, 94	funcid 17816	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → ((𝑤(2^nd ‘ℎ)𝑤)‘((Id‘𝑂)‘𝑤)) = ((Id‘𝑆)‘((1^st ‘ℎ)‘𝑤)))
116	5, 11	oppcid 17663	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐶 ∈ Cat → (Id‘𝑂) = 1 )
117	89, 116	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → (Id‘𝑂) = 1 )
118	117	fveq1d 6890	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → ((Id‘𝑂)‘𝑤) = ( 1 ‘𝑤))
119	118	fveq2d 6892	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → ((𝑤(2^nd ‘ℎ)𝑤)‘((Id‘𝑂)‘𝑤)) = ((𝑤(2^nd ‘ℎ)𝑤)‘( 1 ‘𝑤)))
120	77	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → 𝑈 ∈ V)
121		eqid 2732	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Base‘𝑆) = (Base‘𝑆)
122	7, 121, 114	funcf1 17812	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → (1^st ‘ℎ):𝐵⟶(Base‘𝑆))
123	12, 120	setcbas 18024	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → 𝑈 = (Base‘𝑆))
124	123	feq3d 6701	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → ((1^st ‘ℎ):𝐵⟶𝑈 ↔ (1^st ‘ℎ):𝐵⟶(Base‘𝑆)))
125	122, 124	mpbird 256	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → (1^st ‘ℎ):𝐵⟶𝑈)
126	125, 94	ffvelcdmd 7084	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → ((1^st ‘ℎ)‘𝑤) ∈ 𝑈)
127	12, 111, 120, 126	setcid 18032	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → ((Id‘𝑆)‘((1^st ‘ℎ)‘𝑤)) = ( I ↾ ((1^st ‘ℎ)‘𝑤)))
128	115, 119, 127	3eqtr3d 2780	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → ((𝑤(2^nd ‘ℎ)𝑤)‘( 1 ‘𝑤)) = ( I ↾ ((1^st ‘ℎ)‘𝑤)))
129	128	fveq1d 6890	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → (((𝑤(2^nd ‘ℎ)𝑤)‘( 1 ‘𝑤))‘𝑘) = (( I ↾ ((1^st ‘ℎ)‘𝑤))‘𝑘))
130		fvresi 7167	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ((1^st ‘ℎ)‘𝑤) → (( I ↾ ((1^st ‘ℎ)‘𝑤))‘𝑘) = 𝑘)
131	130	adantl 482	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → (( I ↾ ((1^st ‘ℎ)‘𝑤))‘𝑘) = 𝑘)
132	109, 129, 131	3eqtrd 2776	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → ((((ℎ𝑁𝑤)‘𝑘)‘𝑤)‘( 1 ‘𝑤)) = 𝑘)
133	97, 105, 132	3eqtrd 2776	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ ((1^st ‘ℎ)‘𝑤)) → ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘)) = 𝑘)
134	88, 133	syldan 591	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑘 ∈ (ℎ(1^st ‘𝐸)𝑤)) → ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘)) = 𝑘)
135	134	mpteq2dva 5247	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑘 ∈ (ℎ(1^st ‘𝐸)𝑤) ↦ ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘))) = (𝑘 ∈ (ℎ(1^st ‘𝐸)𝑤) ↦ 𝑘))
136		mptresid 6048	. . . . . . . . . . 11 ⊢ ( I ↾ (ℎ(1^st ‘𝐸)𝑤)) = (𝑘 ∈ (ℎ(1^st ‘𝐸)𝑤) ↦ 𝑘)
137	135, 136	eqtr4di 2790	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑘 ∈ (ℎ(1^st ‘𝐸)𝑤) ↦ ((ℎ𝑀𝑤)‘((ℎ𝑁𝑤)‘𝑘))) = ( I ↾ (ℎ(1^st ‘𝐸)𝑤)))
138	86, 137	eqtrd 2772	. . . . . . . . 9 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤) ∘ (ℎ𝑁𝑤)) = ( I ↾ (ℎ(1^st ‘𝐸)𝑤)))
139		fcompt 7127	. . . . . . . . . . 11 ⊢ (((ℎ𝑁𝑤):(ℎ(1^st ‘𝐸)𝑤)⟶(ℎ(1^st ‘𝑍)𝑤) ∧ (ℎ𝑀𝑤):(ℎ(1^st ‘𝑍)𝑤)⟶(ℎ(1^st ‘𝐸)𝑤)) → ((ℎ𝑁𝑤) ∘ (ℎ𝑀𝑤)) = (𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤) ↦ ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))))
140	84, 35, 139	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑁𝑤) ∘ (ℎ𝑀𝑤)) = (𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤) ↦ ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))))
141		eqid 2732	. . . . . . . . . . . . . 14 ⊢ (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆)
142	28	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → 𝐶 ∈ Cat)
143	29	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → 𝑉 ∈ 𝑊)
144	30	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → ran (Hom_f ‘𝐶) ⊆ 𝑈)
145	31	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → (ran (Hom_f ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
146		simplrl 775	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → ℎ ∈ (𝑂 Func 𝑆))
147		simplrr 776	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → 𝑤 ∈ 𝐵)
148	81	feq3d 6701	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤):(ℎ(1^st ‘𝑍)𝑤)⟶(ℎ(1^st ‘𝐸)𝑤) ↔ (ℎ𝑀𝑤):(ℎ(1^st ‘𝑍)𝑤)⟶((1^st ‘ℎ)‘𝑤)))
149	35, 148	mpbid 231	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑀𝑤):(ℎ(1^st ‘𝑍)𝑤)⟶((1^st ‘ℎ)‘𝑤))
150	149	ffvelcdmda 7083	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → ((ℎ𝑀𝑤)‘𝑏) ∈ ((1^st ‘ℎ)‘𝑤))
151	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 142, 143, 144, 145, 146, 147, 42, 150	yonedalem4c 18226	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) ∈ (((1^st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
152	141, 151	nat1st2nd 17898	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) ∈ (⟨(1^st ‘((1^st ‘𝑌)‘𝑤)), (2^nd ‘((1^st ‘𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1^st ‘ℎ), (2^nd ‘ℎ)⟩))
153	141, 152, 7	natfn 17901	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) Fn 𝐵)
154	82	eleq2d 2819	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤) ↔ 𝑏 ∈ (((1^st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ)))
155	154	biimpa 477	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → 𝑏 ∈ (((1^st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
156	141, 155	nat1st2nd 17898	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → 𝑏 ∈ (⟨(1^st ‘((1^st ‘𝑌)‘𝑤)), (2^nd ‘((1^st ‘𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1^st ‘ℎ), (2^nd ‘ℎ)⟩))
157	141, 156, 7	natfn 17901	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → 𝑏 Fn 𝐵)
158	142	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → 𝐶 ∈ Cat)
159	147	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → 𝑤 ∈ 𝐵)
160		simpr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵)
161	10, 6, 158, 159, 107, 160	yon11 18213	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧) = (𝑧(Hom ‘𝐶)𝑤))
162	161	eleq2d 2819	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑘 ∈ ((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧) ↔ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)))
163	162	biimpa 477	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ ((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧)) → 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤))
164	158	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝐶 ∈ Cat)
165	143	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑉 ∈ 𝑊)
166	144	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ran (Hom_f ‘𝐶) ⊆ 𝑈)
167	145	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ran (Hom_f ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
168	146	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ℎ ∈ (𝑂 Func 𝑆))
169	159	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑤 ∈ 𝐵)
170	150	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ𝑀𝑤)‘𝑏) ∈ ((1^st ‘ℎ)‘𝑤))
171		simplr 767	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑧 ∈ 𝐵)
172		simpr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(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 18225	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = (((𝑤(2^nd ‘ℎ)𝑧)‘𝑘)‘((ℎ𝑀𝑤)‘𝑏)))
174	10, 6, 11, 5, 12, 13, 3, 14, 1, 15, 16, 164, 165, 166, 167, 168, 169, 26	yonedalem3a 18223	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ𝑀𝑤) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))) ∧ (ℎ𝑀𝑤):(ℎ(1^st ‘𝑍)𝑤)⟶(ℎ(1^st ‘𝐸)𝑤)))
175	174	simpld 495	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ℎ𝑀𝑤) = (𝑎 ∈ (((1^st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤))))
176	175	fveq1d 6890	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ𝑀𝑤)‘𝑏) = ((𝑎 ∈ (((1^st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘𝑏))
177	155	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑏 ∈ (((1^st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ))
178		fveq1 6887	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑏 → (𝑎‘𝑤) = (𝑏‘𝑤))
179	178	fveq1d 6890	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑏 → ((𝑎‘𝑤)‘( 1 ‘𝑤)) = ((𝑏‘𝑤)‘( 1 ‘𝑤)))
180		fvex 6901	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑏‘𝑤)‘( 1 ‘𝑤)) ∈ V
181	179, 102, 180	fvmpt 6995	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ (((1^st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) → ((𝑎 ∈ (((1^st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘𝑏) = ((𝑏‘𝑤)‘( 1 ‘𝑤)))
182	177, 181	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑎 ∈ (((1^st ‘𝑌)‘𝑤)(𝑂 Nat 𝑆)ℎ) ↦ ((𝑎‘𝑤)‘( 1 ‘𝑤)))‘𝑏) = ((𝑏‘𝑤)‘( 1 ‘𝑤)))
183	176, 182	eqtrd 2772	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((ℎ𝑀𝑤)‘𝑏) = ((𝑏‘𝑤)‘( 1 ‘𝑤)))
184	183	fveq2d 6892	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2^nd ‘ℎ)𝑧)‘𝑘)‘((ℎ𝑀𝑤)‘𝑏)) = (((𝑤(2^nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))))
185	156	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑏 ∈ (⟨(1^st ‘((1^st ‘𝑌)‘𝑤)), (2^nd ‘((1^st ‘𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1^st ‘ℎ), (2^nd ‘ℎ)⟩))
186		eqid 2732	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Hom ‘𝑂) = (Hom ‘𝑂)
187		eqid 2732	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (comp‘𝑆) = (comp‘𝑆)
188	107, 5	oppchom 17656	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤(Hom ‘𝑂)𝑧) = (𝑧(Hom ‘𝐶)𝑤)
189	172, 188	eleqtrrdi 2844	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑘 ∈ (𝑤(Hom ‘𝑂)𝑧))
190	141, 185, 7, 186, 187, 169, 171, 189	nati 17902	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧)(⟨((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑤), ((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧)⟩(comp‘𝑆)((1^st ‘ℎ)‘𝑧))((𝑤(2^nd ‘((1^st ‘𝑌)‘𝑤))𝑧)‘𝑘)) = (((𝑤(2^nd ‘ℎ)𝑧)‘𝑘)(⟨((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑤), ((1^st ‘ℎ)‘𝑤)⟩(comp‘𝑆)((1^st ‘ℎ)‘𝑧))(𝑏‘𝑤)))
191	77	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → 𝑈 ∈ V)
192	191	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → 𝑈 ∈ V)
193	192	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑈 ∈ V)
194		relfunc 17808	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ Rel (𝐶 Func 𝑄)
195	10, 17, 5, 12, 3, 77, 19	yoncl 18211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝜑 → 𝑌 ∈ (𝐶 Func 𝑄))
196		1st2ndbr 8024	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((Rel (𝐶 Func 𝑄) ∧ 𝑌 ∈ (𝐶 Func 𝑄)) → (1^st ‘𝑌)(𝐶 Func 𝑄)(2^nd ‘𝑌))
197	194, 195, 196	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝜑 → (1^st ‘𝑌)(𝐶 Func 𝑄)(2^nd ‘𝑌))
198	6, 4, 197	funcf1 17812	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (1^st ‘𝑌):𝐵⟶(𝑂 Func 𝑆))
199	198	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → (1^st ‘𝑌):𝐵⟶(𝑂 Func 𝑆))
200	199, 147	ffvelcdmd 7084	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → ((1^st ‘𝑌)‘𝑤) ∈ (𝑂 Func 𝑆))
201		1st2ndbr 8024	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((Rel (𝑂 Func 𝑆) ∧ ((1^st ‘𝑌)‘𝑤) ∈ (𝑂 Func 𝑆)) → (1^st ‘((1^st ‘𝑌)‘𝑤))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑤)))
202	112, 200, 201	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → (1^st ‘((1^st ‘𝑌)‘𝑤))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑤)))
203	7, 121, 202	funcf1 17812	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → (1^st ‘((1^st ‘𝑌)‘𝑤)):𝐵⟶(Base‘𝑆))
204	12, 191	setcbas 18024	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → 𝑈 = (Base‘𝑆))
205	204	feq3d 6701	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → ((1^st ‘((1^st ‘𝑌)‘𝑤)):𝐵⟶𝑈 ↔ (1^st ‘((1^st ‘𝑌)‘𝑤)):𝐵⟶(Base‘𝑆)))
206	203, 205	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → (1^st ‘((1^st ‘𝑌)‘𝑤)):𝐵⟶𝑈)
207	206, 147	ffvelcdmd 7084	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → ((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑤) ∈ 𝑈)
208	207	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑤) ∈ 𝑈)
209	206	ffvelcdmda 7083	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧) ∈ 𝑈)
210	209	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧) ∈ 𝑈)
211	112, 146, 113	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → (1^st ‘ℎ)(𝑂 Func 𝑆)(2^nd ‘ℎ))
212	7, 121, 211	funcf1 17812	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → (1^st ‘ℎ):𝐵⟶(Base‘𝑆))
213	204	feq3d 6701	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → ((1^st ‘ℎ):𝐵⟶𝑈 ↔ (1^st ‘ℎ):𝐵⟶(Base‘𝑆)))
214	212, 213	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → (1^st ‘ℎ):𝐵⟶𝑈)
215	214	ffvelcdmda 7083	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((1^st ‘ℎ)‘𝑧) ∈ 𝑈)
216	215	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1^st ‘ℎ)‘𝑧) ∈ 𝑈)
217		eqid 2732	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (Hom ‘𝑆) = (Hom ‘𝑆)
218	202	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1^st ‘((1^st ‘𝑌)‘𝑤))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑤)))
219	7, 186, 217, 218, 169, 171	funcf2 17814	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑤(2^nd ‘((1^st ‘𝑌)‘𝑤))𝑧):(𝑤(Hom ‘𝑂)𝑧)⟶(((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧)))
220	219, 189	ffvelcdmd 7084	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2^nd ‘((1^st ‘𝑌)‘𝑤))𝑧)‘𝑘) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧)))
221	12, 193, 217, 208, 210	elsetchom 18027	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2^nd ‘((1^st ‘𝑌)‘𝑤))𝑧)‘𝑘) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧)) ↔ ((𝑤(2^nd ‘((1^st ‘𝑌)‘𝑤))𝑧)‘𝑘):((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑤)⟶((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧)))
222	220, 221	mpbid 231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2^nd ‘((1^st ‘𝑌)‘𝑤))𝑧)‘𝑘):((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑤)⟶((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧))
223	156	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → 𝑏 ∈ (⟨(1^st ‘((1^st ‘𝑌)‘𝑤)), (2^nd ‘((1^st ‘𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1^st ‘ℎ), (2^nd ‘ℎ)⟩))
224	141, 223, 7, 217, 160	natcl 17900	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑏‘𝑧) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1^st ‘ℎ)‘𝑧)))
225	12, 192, 217, 209, 215	elsetchom 18027	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((𝑏‘𝑧) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1^st ‘ℎ)‘𝑧)) ↔ (𝑏‘𝑧):((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧)⟶((1^st ‘ℎ)‘𝑧)))
226	224, 225	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑏‘𝑧):((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧)⟶((1^st ‘ℎ)‘𝑧))
227	226	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑏‘𝑧):((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧)⟶((1^st ‘ℎ)‘𝑧))
228	12, 193, 187, 208, 210, 216, 222, 227	setcco 18029	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧)(⟨((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑤), ((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧)⟩(comp‘𝑆)((1^st ‘ℎ)‘𝑧))((𝑤(2^nd ‘((1^st ‘𝑌)‘𝑤))𝑧)‘𝑘)) = ((𝑏‘𝑧) ∘ ((𝑤(2^nd ‘((1^st ‘𝑌)‘𝑤))𝑧)‘𝑘)))
229	214, 147	ffvelcdmd 7084	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → ((1^st ‘ℎ)‘𝑤) ∈ 𝑈)
230	229	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1^st ‘ℎ)‘𝑤) ∈ 𝑈)
231	141, 156, 7, 217, 147	natcl 17900	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → (𝑏‘𝑤) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1^st ‘ℎ)‘𝑤)))
232	12, 191, 217, 207, 229	elsetchom 18027	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → ((𝑏‘𝑤) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑤)(Hom ‘𝑆)((1^st ‘ℎ)‘𝑤)) ↔ (𝑏‘𝑤):((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑤)⟶((1^st ‘ℎ)‘𝑤)))
233	231, 232	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → (𝑏‘𝑤):((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑤)⟶((1^st ‘ℎ)‘𝑤))
234	233	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑏‘𝑤):((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑤)⟶((1^st ‘ℎ)‘𝑤))
235	112, 168, 113	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1^st ‘ℎ)(𝑂 Func 𝑆)(2^nd ‘ℎ))
236	7, 186, 217, 235, 169, 171	funcf2 17814	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑤(2^nd ‘ℎ)𝑧):(𝑤(Hom ‘𝑂)𝑧)⟶(((1^st ‘ℎ)‘𝑤)(Hom ‘𝑆)((1^st ‘ℎ)‘𝑧)))
237	236, 189	ffvelcdmd 7084	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2^nd ‘ℎ)𝑧)‘𝑘) ∈ (((1^st ‘ℎ)‘𝑤)(Hom ‘𝑆)((1^st ‘ℎ)‘𝑧)))
238	12, 193, 217, 230, 216	elsetchom 18027	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2^nd ‘ℎ)𝑧)‘𝑘) ∈ (((1^st ‘ℎ)‘𝑤)(Hom ‘𝑆)((1^st ‘ℎ)‘𝑧)) ↔ ((𝑤(2^nd ‘ℎ)𝑧)‘𝑘):((1^st ‘ℎ)‘𝑤)⟶((1^st ‘ℎ)‘𝑧)))
239	237, 238	mpbid 231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑤(2^nd ‘ℎ)𝑧)‘𝑘):((1^st ‘ℎ)‘𝑤)⟶((1^st ‘ℎ)‘𝑧))
240	12, 193, 187, 208, 230, 216, 234, 239	setcco 18029	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2^nd ‘ℎ)𝑧)‘𝑘)(⟨((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑤), ((1^st ‘ℎ)‘𝑤)⟩(comp‘𝑆)((1^st ‘ℎ)‘𝑧))(𝑏‘𝑤)) = (((𝑤(2^nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤)))
241	190, 228, 240	3eqtr3d 2780	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧) ∘ ((𝑤(2^nd ‘((1^st ‘𝑌)‘𝑤))𝑧)‘𝑘)) = (((𝑤(2^nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤)))
242	241	fveq1d 6890	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑏‘𝑧) ∘ ((𝑤(2^nd ‘((1^st ‘𝑌)‘𝑤))𝑧)‘𝑘))‘( 1 ‘𝑤)) = ((((𝑤(2^nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤))‘( 1 ‘𝑤)))
243	6, 107, 11, 142, 147	catidcl 17622	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → ( 1 ‘𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤))
244	10, 6, 142, 147, 107, 147	yon11 18213	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → ((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑤) = (𝑤(Hom ‘𝐶)𝑤))
245	243, 244	eleqtrrd 2836	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → ( 1 ‘𝑤) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑤))
246	245	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ( 1 ‘𝑤) ∈ ((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑤))
247	222, 246	fvco3d 6988	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑏‘𝑧) ∘ ((𝑤(2^nd ‘((1^st ‘𝑌)‘𝑤))𝑧)‘𝑘))‘( 1 ‘𝑤)) = ((𝑏‘𝑧)‘(((𝑤(2^nd ‘((1^st ‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤))))
248	233, 245	fvco3d 6988	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → ((((𝑤(2^nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤))‘( 1 ‘𝑤)) = (((𝑤(2^nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))))
249	248	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((𝑤(2^nd ‘ℎ)𝑧)‘𝑘) ∘ (𝑏‘𝑤))‘( 1 ‘𝑤)) = (((𝑤(2^nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))))
250	242, 247, 249	3eqtr3d 2780	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧)‘(((𝑤(2^nd ‘((1^st ‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤))) = (((𝑤(2^nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))))
251		eqid 2732	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (comp‘𝐶) = (comp‘𝐶)
252	243	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ( 1 ‘𝑤) ∈ (𝑤(Hom ‘𝐶)𝑤))
253	10, 6, 164, 169, 107, 169, 251, 171, 172, 252	yon12 18214	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2^nd ‘((1^st ‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤)) = (( 1 ‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐶)𝑤)𝑘))
254	6, 107, 11, 164, 171, 251, 169, 172	catlid 17623	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (( 1 ‘𝑤)(⟨𝑧, 𝑤⟩(comp‘𝐶)𝑤)𝑘) = 𝑘)
255	253, 254	eqtrd 2772	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2^nd ‘((1^st ‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤)) = 𝑘)
256	255	fveq2d 6892	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑏‘𝑧)‘(((𝑤(2^nd ‘((1^st ‘𝑌)‘𝑤))𝑧)‘𝑘)‘( 1 ‘𝑤))) = ((𝑏‘𝑧)‘𝑘))
257	250, 256	eqtr3d 2774	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → (((𝑤(2^nd ‘ℎ)𝑧)‘𝑘)‘((𝑏‘𝑤)‘( 1 ‘𝑤))) = ((𝑏‘𝑧)‘𝑘))
258	173, 184, 257	3eqtrd 2776	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = ((𝑏‘𝑧)‘𝑘))
259	163, 258	syldan 591	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) ∧ 𝑘 ∈ ((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧)) → ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘) = ((𝑏‘𝑧)‘𝑘))
260	259	mpteq2dva 5247	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑘 ∈ ((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧) ↦ ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘)) = (𝑘 ∈ ((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧) ↦ ((𝑏‘𝑧)‘𝑘)))
261	152	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) ∈ (⟨(1^st ‘((1^st ‘𝑌)‘𝑤)), (2^nd ‘((1^st ‘𝑌)‘𝑤))⟩(𝑂 Nat 𝑆)⟨(1^st ‘ℎ), (2^nd ‘ℎ)⟩))
262	141, 261, 7, 217, 160	natcl 17900	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1^st ‘ℎ)‘𝑧)))
263	12, 192, 217, 209, 215	elsetchom 18027	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧)(Hom ‘𝑆)((1^st ‘ℎ)‘𝑧)) ↔ (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧):((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧)⟶((1^st ‘ℎ)‘𝑧)))
264	262, 263	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧):((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧)⟶((1^st ‘ℎ)‘𝑧))
265	264	feqmptd 6957	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧) = (𝑘 ∈ ((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧) ↦ ((((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧)‘𝑘)))
266	226	feqmptd 6957	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (𝑏‘𝑧) = (𝑘 ∈ ((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧) ↦ ((𝑏‘𝑧)‘𝑘)))
267	260, 265, 266	3eqtr4d 2782	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) ∧ 𝑧 ∈ 𝐵) → (((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))‘𝑧) = (𝑏‘𝑧))
268	153, 157, 267	eqfnfvd 7032	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) ∧ 𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤)) → ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏)) = 𝑏)
269	268	mpteq2dva 5247	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤) ↦ ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))) = (𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤) ↦ 𝑏))
270		mptresid 6048	. . . . . . . . . . 11 ⊢ ( I ↾ (ℎ(1^st ‘𝑍)𝑤)) = (𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤) ↦ 𝑏)
271	269, 270	eqtr4di 2790	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (𝑏 ∈ (ℎ(1^st ‘𝑍)𝑤) ↦ ((ℎ𝑁𝑤)‘((ℎ𝑀𝑤)‘𝑏))) = ( I ↾ (ℎ(1^st ‘𝑍)𝑤)))
272	140, 271	eqtrd 2772	. . . . . . . . 9 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑁𝑤) ∘ (ℎ𝑀𝑤)) = ( I ↾ (ℎ(1^st ‘𝑍)𝑤)))
273		fcof1o 7290	. . . . . . . . 9 ⊢ ((((ℎ𝑀𝑤):(ℎ(1^st ‘𝑍)𝑤)⟶(ℎ(1^st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤):(ℎ(1^st ‘𝐸)𝑤)⟶(ℎ(1^st ‘𝑍)𝑤)) ∧ (((ℎ𝑀𝑤) ∘ (ℎ𝑁𝑤)) = ( I ↾ (ℎ(1^st ‘𝐸)𝑤)) ∧ ((ℎ𝑁𝑤) ∘ (ℎ𝑀𝑤)) = ( I ↾ (ℎ(1^st ‘𝑍)𝑤)))) → ((ℎ𝑀𝑤):(ℎ(1^st ‘𝑍)𝑤)–1-1-onto→(ℎ(1^st ‘𝐸)𝑤) ∧ ^◡(ℎ𝑀𝑤) = (ℎ𝑁𝑤)))
274	35, 84, 138, 272, 273	syl22anc 837	. . . . . . . 8 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤):(ℎ(1^st ‘𝑍)𝑤)–1-1-onto→(ℎ(1^st ‘𝐸)𝑤) ∧ ^◡(ℎ𝑀𝑤) = (ℎ𝑁𝑤)))
275		eqcom 2739	. . . . . . . . 9 ⊢ (^◡(ℎ𝑀𝑤) = (ℎ𝑁𝑤) ↔ (ℎ𝑁𝑤) = ^◡(ℎ𝑀𝑤))
276	275	anbi2i 623	. . . . . . . 8 ⊢ (((ℎ𝑀𝑤):(ℎ(1^st ‘𝑍)𝑤)–1-1-onto→(ℎ(1^st ‘𝐸)𝑤) ∧ ^◡(ℎ𝑀𝑤) = (ℎ𝑁𝑤)) ↔ ((ℎ𝑀𝑤):(ℎ(1^st ‘𝑍)𝑤)–1-1-onto→(ℎ(1^st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤) = ^◡(ℎ𝑀𝑤)))
277	274, 276	sylib 217	. . . . . . 7 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤):(ℎ(1^st ‘𝑍)𝑤)–1-1-onto→(ℎ(1^st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤) = ^◡(ℎ𝑀𝑤)))
278		eqid 2732	. . . . . . . . . . 11 ⊢ (Base‘𝑇) = (Base‘𝑇)
279		relfunc 17808	. . . . . . . . . . . 12 ⊢ Rel ((𝑄 ×_c 𝑂) Func 𝑇)
280		1st2ndbr 8024	. . . . . . . . . . . 12 ⊢ ((Rel ((𝑄 ×_c 𝑂) Func 𝑇) ∧ 𝑍 ∈ ((𝑄 ×_c 𝑂) Func 𝑇)) → (1^st ‘𝑍)((𝑄 ×_c 𝑂) Func 𝑇)(2^nd ‘𝑍))
281	279, 22, 280	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → (1^st ‘𝑍)((𝑄 ×_c 𝑂) Func 𝑇)(2^nd ‘𝑍))
282	8, 278, 281	funcf1 17812	. . . . . . . . . 10 ⊢ (𝜑 → (1^st ‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
283	13, 18	setcbas 18024	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 = (Base‘𝑇))
284	283	feq3d 6701	. . . . . . . . . 10 ⊢ (𝜑 → ((1^st ‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶𝑉 ↔ (1^st ‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇)))
285	282, 284	mpbird 256	. . . . . . . . 9 ⊢ (𝜑 → (1^st ‘𝑍):((𝑂 Func 𝑆) × 𝐵)⟶𝑉)
286	285	fovcdmda 7574	. . . . . . . 8 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ(1^st ‘𝑍)𝑤) ∈ 𝑉)
287		1st2ndbr 8024	. . . . . . . . . . . 12 ⊢ ((Rel ((𝑄 ×_c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×_c 𝑂) Func 𝑇)) → (1^st ‘𝐸)((𝑄 ×_c 𝑂) Func 𝑇)(2^nd ‘𝐸))
288	279, 23, 287	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → (1^st ‘𝐸)((𝑄 ×_c 𝑂) Func 𝑇)(2^nd ‘𝐸))
289	8, 278, 288	funcf1 17812	. . . . . . . . . 10 ⊢ (𝜑 → (1^st ‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇))
290	283	feq3d 6701	. . . . . . . . . 10 ⊢ (𝜑 → ((1^st ‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶𝑉 ↔ (1^st ‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶(Base‘𝑇)))
291	289, 290	mpbird 256	. . . . . . . . 9 ⊢ (𝜑 → (1^st ‘𝐸):((𝑂 Func 𝑆) × 𝐵)⟶𝑉)
292	291	fovcdmda 7574	. . . . . . . 8 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ(1^st ‘𝐸)𝑤) ∈ 𝑉)
293	13, 29, 286, 292, 25	setcinv 18036	. . . . . . 7 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → ((ℎ𝑀𝑤)((ℎ(1^st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1^st ‘𝐸)𝑤))(ℎ𝑁𝑤) ↔ ((ℎ𝑀𝑤):(ℎ(1^st ‘𝑍)𝑤)–1-1-onto→(ℎ(1^st ‘𝐸)𝑤) ∧ (ℎ𝑁𝑤) = ^◡(ℎ𝑀𝑤))))
294	277, 293	mpbird 256	. . . . . 6 ⊢ ((𝜑 ∧ (ℎ ∈ (𝑂 Func 𝑆) ∧ 𝑤 ∈ 𝐵)) → (ℎ𝑀𝑤)((ℎ(1^st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1^st ‘𝐸)𝑤))(ℎ𝑁𝑤))
295	294	ralrimivva 3200	. . . . 5 ⊢ (𝜑 → ∀ℎ ∈ (𝑂 Func 𝑆)∀𝑤 ∈ 𝐵 (ℎ𝑀𝑤)((ℎ(1^st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1^st ‘𝐸)𝑤))(ℎ𝑁𝑤))
296		fveq2 6888	. . . . . . . 8 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → (𝑀‘𝑧) = (𝑀‘⟨ℎ, 𝑤⟩))
297		df-ov 7408	. . . . . . . 8 ⊢ (ℎ𝑀𝑤) = (𝑀‘⟨ℎ, 𝑤⟩)
298	296, 297	eqtr4di 2790	. . . . . . 7 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → (𝑀‘𝑧) = (ℎ𝑀𝑤))
299		fveq2 6888	. . . . . . . . 9 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → ((1^st ‘𝑍)‘𝑧) = ((1^st ‘𝑍)‘⟨ℎ, 𝑤⟩))
300		df-ov 7408	. . . . . . . . 9 ⊢ (ℎ(1^st ‘𝑍)𝑤) = ((1^st ‘𝑍)‘⟨ℎ, 𝑤⟩)
301	299, 300	eqtr4di 2790	. . . . . . . 8 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → ((1^st ‘𝑍)‘𝑧) = (ℎ(1^st ‘𝑍)𝑤))
302		fveq2 6888	. . . . . . . . 9 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → ((1^st ‘𝐸)‘𝑧) = ((1^st ‘𝐸)‘⟨ℎ, 𝑤⟩))
303		df-ov 7408	. . . . . . . . 9 ⊢ (ℎ(1^st ‘𝐸)𝑤) = ((1^st ‘𝐸)‘⟨ℎ, 𝑤⟩)
304	302, 303	eqtr4di 2790	. . . . . . . 8 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → ((1^st ‘𝐸)‘𝑧) = (ℎ(1^st ‘𝐸)𝑤))
305	301, 304	oveq12d 7423	. . . . . . 7 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → (((1^st ‘𝑍)‘𝑧)(Inv‘𝑇)((1^st ‘𝐸)‘𝑧)) = ((ℎ(1^st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1^st ‘𝐸)𝑤)))
306		fveq2 6888	. . . . . . . 8 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → (𝑁‘𝑧) = (𝑁‘⟨ℎ, 𝑤⟩))
307		df-ov 7408	. . . . . . . 8 ⊢ (ℎ𝑁𝑤) = (𝑁‘⟨ℎ, 𝑤⟩)
308	306, 307	eqtr4di 2790	. . . . . . 7 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → (𝑁‘𝑧) = (ℎ𝑁𝑤))
309	298, 305, 308	breq123d 5161	. . . . . 6 ⊢ (𝑧 = ⟨ℎ, 𝑤⟩ → ((𝑀‘𝑧)(((1^st ‘𝑍)‘𝑧)(Inv‘𝑇)((1^st ‘𝐸)‘𝑧))(𝑁‘𝑧) ↔ (ℎ𝑀𝑤)((ℎ(1^st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1^st ‘𝐸)𝑤))(ℎ𝑁𝑤)))
310	309	ralxp 5839	. . . . 5 ⊢ (∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑀‘𝑧)(((1^st ‘𝑍)‘𝑧)(Inv‘𝑇)((1^st ‘𝐸)‘𝑧))(𝑁‘𝑧) ↔ ∀ℎ ∈ (𝑂 Func 𝑆)∀𝑤 ∈ 𝐵 (ℎ𝑀𝑤)((ℎ(1^st ‘𝑍)𝑤)(Inv‘𝑇)(ℎ(1^st ‘𝐸)𝑤))(ℎ𝑁𝑤))
311	295, 310	sylibr 233	. . . 4 ⊢ (𝜑 → ∀𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑀‘𝑧)(((1^st ‘𝑍)‘𝑧)(Inv‘𝑇)((1^st ‘𝐸)‘𝑧))(𝑁‘𝑧))
312	311	r19.21bi 3248	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵)) → (𝑀‘𝑧)(((1^st ‘𝑍)‘𝑧)(Inv‘𝑇)((1^st ‘𝐸)‘𝑧))(𝑁‘𝑧))
313	1, 8, 9, 22, 23, 24, 25, 27, 312	invfuc 17923	. 2 ⊢ (𝜑 → 𝑀(𝑍𝐼𝐸)(𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁‘𝑧)))
314		fvex 6901	. . . . 5 ⊢ ((1^st ‘𝑓)‘𝑥) ∈ V
315	314	mptex 7221	. . . 4 ⊢ (𝑢 ∈ ((1^st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2^nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))) ∈ V
316	42, 315	fnmpoi 8052	. . 3 ⊢ 𝑁 Fn ((𝑂 Func 𝑆) × 𝐵)
317		dffn5 6947	. . 3 ⊢ (𝑁 Fn ((𝑂 Func 𝑆) × 𝐵) ↔ 𝑁 = (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁‘𝑧)))
318	316, 317	mpbi 229	. 2 ⊢ 𝑁 = (𝑧 ∈ ((𝑂 Func 𝑆) × 𝐵) ↦ (𝑁‘𝑧))
319	313, 318	breqtrrdi 5189	1 ⊢ (𝜑 → 𝑀(𝑍𝐼𝐸)𝑁)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∀wral 3061 Vcvv 3474 ∪ cun 3945 ⊆ wss 3947 ⟨cop 4633 class class class wbr 5147 ↦ cmpt 5230 I cid 5572 × cxp 5673 ^◡ccnv 5674 ran crn 5676 ↾ cres 5677 ∘ ccom 5679 Rel wrel 5680 Fn wfn 6535 ⟶wf 6536 –1-1-onto→wf1o 6539 ‘cfv 6540 (class class class)co 7405 ∈ cmpo 7407 1^st c1st 7969 2^nd c2nd 7970 tpos ctpos 8206 Basecbs 17140 Hom chom 17204 compcco 17205 Catccat 17604 Idccid 17605 Hom_f chomf 17606 oppCatcoppc 17651 Invcinv 17688 Func cfunc 17800 ∘_func ccofu 17802 Nat cnat 17888 FuncCat cfuc 17889 SetCatcsetc 18021 ×_c cxpc 18116 1^st_F c1stf 18117 2^nd_F c2ndf 18118 ⟨,⟩_F cprf 18119 eval_F cevlf 18158 Hom_Fchof 18197 Yoncyon 18198

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-tp 4632 df-op 4634 df-uni 4908 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6297 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7852 df-1st 7971 df-2nd 7972 df-tpos 8207 df-frecs 8262 df-wrecs 8293 df-recs 8367 df-rdg 8406 df-1o 8462 df-er 8699 df-map 8818 df-pm 8819 df-ixp 8888 df-en 8936 df-dom 8937 df-sdom 8938 df-fin 8939 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11442 df-neg 11443 df-nn 12209 df-2 12271 df-3 12272 df-4 12273 df-5 12274 df-6 12275 df-7 12276 df-8 12277 df-9 12278 df-n0 12469 df-z 12555 df-dec 12674 df-uz 12819 df-fz 13481 df-struct 17076 df-sets 17093 df-slot 17111 df-ndx 17123 df-base 17141 df-ress 17170 df-hom 17217 df-cco 17218 df-cat 17608 df-cid 17609 df-homf 17610 df-comf 17611 df-oppc 17652 df-sect 17690 df-inv 17691 df-ssc 17753 df-resc 17754 df-subc 17755 df-func 17804 df-cofu 17806 df-nat 17890 df-fuc 17891 df-setc 18022 df-xpc 18120 df-1stf 18121 df-2ndf 18122 df-prf 18123 df-evlf 18162 df-curf 18163 df-hof 18199 df-yon 18200

This theorem is referenced by: yonffthlem 18231 yoneda 18232

W3C validator