yonedainv

Description: The Yoneda Lemma with explicit inverse. (Contributed by Mario Carneiro, 29-Jan-2017)

	Ref	Expression
Hypotheses	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	yonedainv	⊢ ( 𝜑 → 𝑀 ( 𝑍 𝐼 𝐸 ) 𝑁 )

Proof

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

Metamath Proof Explorer

Theorem yonedainv

Proof