yonedalem4c

	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 ‘ 𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 )
	yonedalem21.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑂 Func 𝑆 ) )
	yonedalem21.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	yonedalem4.n	⊢ 𝑁 = ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥 ∈ 𝐵 ↦ ( 𝑢 ∈ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ↦ ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑢 ) ) ) ) )
	yonedalem4.p	⊢ ( 𝜑 → 𝐴 ∈ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) )
Assertion	yonedalem4c	⊢ ( 𝜑 → ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) )

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		yonedalem21.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑂 Func 𝑆 ) )
17		yonedalem21.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
18		yonedalem4.n	⊢ 𝑁 = ( 𝑓 ∈ ( 𝑂 Func 𝑆 ) , 𝑥 ∈ 𝐵 ↦ ( 𝑢 ∈ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ↦ ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ↦ ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝑢 ) ) ) ) )
19		yonedalem4.p	⊢ ( 𝜑 → 𝐴 ∈ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) )
20	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19	yonedalem4a	⊢ ( 𝜑 → ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) )
21		oveq1	⊢ ( 𝑦 = 𝑧 → ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) = ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) )
22		oveq2	⊢ ( 𝑦 = 𝑧 → ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑦 ) = ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) )
23	22	fveq1d	⊢ ( 𝑦 = 𝑧 → ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) = ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) )
24	23	fveq1d	⊢ ( 𝑦 = 𝑧 → ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) = ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) )
25	21 24	mpteq12dv	⊢ ( 𝑦 = 𝑧 → ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) = ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) )
26	25	cbvmptv	⊢ ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) = ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) )
27	20 26	eqtrdi	⊢ ( 𝜑 → ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) = ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) )
28	4 2	oppcbas	⊢ 𝐵 = ( Base ‘ 𝑂 )
29		eqid	⊢ ( Hom ‘ 𝑂 ) = ( Hom ‘ 𝑂 )
30		eqid	⊢ ( Hom ‘ 𝑆 ) = ( Hom ‘ 𝑆 )
31		relfunc	⊢ Rel ( 𝑂 Func 𝑆 )
32		1st2ndbr	⊢ ( ( Rel ( 𝑂 Func 𝑆 ) ∧ 𝐹 ∈ ( 𝑂 Func 𝑆 ) ) → ( 1^st ‘ 𝐹 ) ( 𝑂 Func 𝑆 ) ( 2^nd ‘ 𝐹 ) )
33	31 16 32	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝑂 Func 𝑆 ) ( 2^nd ‘ 𝐹 ) )
34	33	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 1^st ‘ 𝐹 ) ( 𝑂 Func 𝑆 ) ( 2^nd ‘ 𝐹 ) )
35	17	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
36		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
37	28 29 30 34 35 36	funcf2	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) : ( 𝑋 ( Hom ‘ 𝑂 ) 𝑧 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) )
38	37	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) : ( 𝑋 ( Hom ‘ 𝑂 ) 𝑧 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) )
39		simpr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) )
40		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
41	40 4	oppchom	⊢ ( 𝑋 ( Hom ‘ 𝑂 ) 𝑧 ) = ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 )
42	39 41	eleqtrrdi	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑔 ∈ ( 𝑋 ( Hom ‘ 𝑂 ) 𝑧 ) )
43	38 42	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) )
44	15	unssbd	⊢ ( 𝜑 → 𝑈 ⊆ 𝑉 )
45	13 44	ssexd	⊢ ( 𝜑 → 𝑈 ∈ V )
46	45	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝑈 ∈ V )
47	46	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑈 ∈ V )
48		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
49	28 48 33	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ ( Base ‘ 𝑆 ) )
50	5 45	setcbas	⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝑆 ) )
51	50	feq3d	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ 𝑈 ↔ ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ ( Base ‘ 𝑆 ) ) )
52	49 51	mpbird	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ 𝑈 )
53	52 17	ffvelrnd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ∈ 𝑈 )
54	53	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ∈ 𝑈 )
55	52	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑈 )
56	55	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑈 )
57	5 47 30 54 56	elsetchom	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ↔ ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) : ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) )
58	43 57	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) : ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) )
59	19	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝐴 ∈ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) )
60	58 59	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ∈ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) )
61	60	fmpttd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) : ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) )
62	12	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝐶 ∈ Cat )
63	1 2 62 35 40 36	yon11	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) = ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) )
64	63	feq2d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ↔ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) : ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) )
65	61 64	mpbird	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) )
66	1 2 12 17 4 5 45 14	yon1cl	⊢ ( 𝜑 → ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ∈ ( 𝑂 Func 𝑆 ) )
67		1st2ndbr	⊢ ( ( Rel ( 𝑂 Func 𝑆 ) ∧ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ∈ ( 𝑂 Func 𝑆 ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ( 𝑂 Func 𝑆 ) ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) )
68	31 66 67	sylancr	⊢ ( 𝜑 → ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ( 𝑂 Func 𝑆 ) ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) )
69	28 48 68	funcf1	⊢ ( 𝜑 → ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) : 𝐵 ⟶ ( Base ‘ 𝑆 ) )
70	50	feq3d	⊢ ( 𝜑 → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) : 𝐵 ⟶ 𝑈 ↔ ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) : 𝐵 ⟶ ( Base ‘ 𝑆 ) ) )
71	69 70	mpbird	⊢ ( 𝜑 → ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) : 𝐵 ⟶ 𝑈 )
72	71	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ∈ 𝑈 )
73	5 46 30 72 55	elsetchom	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ∈ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ↔ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) )
74	65 73	mpbird	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ∈ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) )
75	74	ralrimiva	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ∈ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) )
76	2	fvexi	⊢ 𝐵 ∈ V
77		mptelixpg	⊢ ( 𝐵 ∈ V → ( ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) ∈ X 𝑧 ∈ 𝐵 ( ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝐵 ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ∈ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ) )
78	76 77	ax-mp	⊢ ( ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) ∈ X 𝑧 ∈ 𝐵 ( ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝐵 ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ∈ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) )
79	75 78	sylibr	⊢ ( 𝜑 → ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) ∈ X 𝑧 ∈ 𝐵 ( ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) )
80	27 79	eqeltrd	⊢ ( 𝜑 → ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ∈ X 𝑧 ∈ 𝐵 ( ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) )
81	12	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → 𝐶 ∈ Cat )
82	17	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → 𝑋 ∈ 𝐵 )
83		simpr1	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → 𝑧 ∈ 𝐵 )
84	1 2 81 82 40 83	yon11	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) = ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) )
85	84	eleq2d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( 𝑘 ∈ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ↔ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) )
86	85	biimpa	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ) → 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) )
87		eqid	⊢ ( comp ‘ 𝑂 ) = ( comp ‘ 𝑂 )
88		eqid	⊢ ( comp ‘ 𝑆 ) = ( comp ‘ 𝑆 )
89	33	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( 1^st ‘ 𝐹 ) ( 𝑂 Func 𝑆 ) ( 2^nd ‘ 𝐹 ) )
90	89	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( 1^st ‘ 𝐹 ) ( 𝑂 Func 𝑆 ) ( 2^nd ‘ 𝐹 ) )
91	82	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑋 ∈ 𝐵 )
92	83	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑧 ∈ 𝐵 )
93		simpr2	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → 𝑤 ∈ 𝐵 )
94	93	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑤 ∈ 𝐵 )
95		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) )
96	95 41	eleqtrrdi	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝑂 ) 𝑧 ) )
97		simplr3	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) )
98	28 29 87 88 90 91 92 94 96 97	funcco	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ( ℎ ( ⟨ 𝑋 , 𝑧 ⟩ ( comp ‘ 𝑂 ) 𝑤 ) 𝑘 ) ) = ( ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑤 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑘 ) ) )
99		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
100	2 99 4 91 92 94	oppcco	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ℎ ( ⟨ 𝑋 , 𝑧 ⟩ ( comp ‘ 𝑂 ) 𝑤 ) 𝑘 ) = ( 𝑘 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ℎ ) )
101	100	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ( ℎ ( ⟨ 𝑋 , 𝑧 ⟩ ( comp ‘ 𝑂 ) 𝑤 ) 𝑘 ) ) = ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ( 𝑘 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ℎ ) ) )
102	45	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → 𝑈 ∈ V )
103	102	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑈 ∈ V )
104	53	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ∈ 𝑈 )
105	55	3ad2antr1	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑈 )
106	105	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ∈ 𝑈 )
107	52	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ 𝑈 )
108	107 93	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑤 ) ∈ 𝑈 )
109	108	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑤 ) ∈ 𝑈 )
110	28 29 30 89 82 83	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) : ( 𝑋 ( Hom ‘ 𝑂 ) 𝑧 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) )
111	110	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) : ( 𝑋 ( Hom ‘ 𝑂 ) 𝑧 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) )
112	111 96	ffvelrnd	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑘 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) )
113	5 103 30 104 106	elsetchom	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑘 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) ↔ ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑘 ) : ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) )
114	112 113	mpbid	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑘 ) : ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) )
115	28 29 30 89 83 93	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) : ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑤 ) ) )
116		simpr3	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) )
117	115 116	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑤 ) ) )
118	5 102 30 105 108	elsetchom	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑤 ) ) ↔ ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) : ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑤 ) ) )
119	117 118	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) : ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑤 ) )
120	119	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) : ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑤 ) )
121	5 103 88 104 106 109 114 120	setcco	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑤 ) ) ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑘 ) ) = ( ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) ∘ ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑘 ) ) )
122	98 101 121	3eqtr3d	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ( 𝑘 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ℎ ) ) = ( ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) ∘ ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑘 ) ) )
123	122	fveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ( 𝑘 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ℎ ) ) ‘ 𝐴 ) = ( ( ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) ∘ ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑘 ) ) ‘ 𝐴 ) )
124	19	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝐴 ∈ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) )
125		fvco3	⊢ ( ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑘 ) : ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ∧ 𝐴 ∈ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ) → ( ( ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) ∘ ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑘 ) ) ‘ 𝐴 ) = ( ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) ‘ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑘 ) ‘ 𝐴 ) ) )
126	114 124 125	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) ∘ ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑘 ) ) ‘ 𝐴 ) = ( ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) ‘ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑘 ) ‘ 𝐴 ) ) )
127	123 126	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ( 𝑘 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ℎ ) ) ‘ 𝐴 ) = ( ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) ‘ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑘 ) ‘ 𝐴 ) ) )
128	81	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝐶 ∈ Cat )
129	40 4	oppchom	⊢ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) = ( 𝑤 ( Hom ‘ 𝐶 ) 𝑧 )
130	97 129	eleqtrdi	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ℎ ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑧 ) )
131	1 2 128 91 40 92 99 94 130 95	yon12	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ℎ ) ‘ 𝑘 ) = ( 𝑘 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ℎ ) )
132	131	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ‘ ( ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ℎ ) ‘ 𝑘 ) ) = ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ‘ ( 𝑘 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ℎ ) ) )
133	13	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑉 ∈ 𝑊 )
134	14	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ran ( Hom_f ‘ 𝐶 ) ⊆ 𝑈 )
135	15	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ran ( Hom_f ‘ 𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 )
136	16	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝐹 ∈ ( 𝑂 Func 𝑆 ) )
137	2 40 99 128 94 92 91 130 95	catcocl	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( 𝑘 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ℎ ) ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑋 ) )
138	1 2 3 4 5 6 7 8 9 10 11 128 133 134 135 136 91 18 124 94 137	yonedalem4b	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ‘ ( 𝑘 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ℎ ) ) = ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ( 𝑘 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ℎ ) ) ‘ 𝐴 ) )
139	132 138	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ‘ ( ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ℎ ) ‘ 𝑘 ) ) = ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ( 𝑘 ( ⟨ 𝑤 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ℎ ) ) ‘ 𝐴 ) )
140	1 2 3 4 5 6 7 8 9 10 11 128 133 134 135 136 91 18 124 92 95	yonedalem4b	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ‘ 𝑘 ) = ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑘 ) ‘ 𝐴 ) )
141	140	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) ‘ ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ‘ 𝑘 ) ) = ( ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) ‘ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑘 ) ‘ 𝐴 ) ) )
142	127 139 141	3eqtr4d	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ‘ ( ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ℎ ) ‘ 𝑘 ) ) = ( ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) ‘ ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ‘ 𝑘 ) ) )
143	86 142	syldan	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) ∧ 𝑘 ∈ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ) → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ‘ ( ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ℎ ) ‘ 𝑘 ) ) = ( ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) ‘ ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ‘ 𝑘 ) ) )
144	143	mpteq2dva	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( 𝑘 ∈ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ↦ ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ‘ ( ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ℎ ) ‘ 𝑘 ) ) ) = ( 𝑘 ∈ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ↦ ( ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) ‘ ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ‘ 𝑘 ) ) ) )
145		fveq2	⊢ ( 𝑧 = 𝑤 → ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) = ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) )
146		fveq2	⊢ ( 𝑧 = 𝑤 → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) = ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑤 ) )
147		fveq2	⊢ ( 𝑧 = 𝑤 → ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) = ( ( 1^st ‘ 𝐹 ) ‘ 𝑤 ) )
148	145 146 147	feq123d	⊢ ( 𝑧 = 𝑤 → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ↔ ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑤 ) ) )
149	27	fveq1d	⊢ ( 𝜑 → ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) = ( ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) ‘ 𝑧 ) )
150		ovex	⊢ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ∈ V
151	150	mptex	⊢ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ∈ V
152		eqid	⊢ ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) = ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) )
153	152	fvmpt2	⊢ ( ( 𝑧 ∈ 𝐵 ∧ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ∈ V ) → ( ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) ‘ 𝑧 ) = ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) )
154	151 153	mpan2	⊢ ( 𝑧 ∈ 𝐵 → ( ( 𝑧 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) ) ‘ 𝑧 ) = ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) )
155	149 154	sylan9eq	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) = ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) )
156	155	feq1d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ↔ ( 𝑔 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑋 ) ↦ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑧 ) ‘ 𝑔 ) ‘ 𝐴 ) ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) )
157	65 156	mpbird	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) )
158	157	ralrimiva	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) )
159	158	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ∀ 𝑧 ∈ 𝐵 ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) )
160	148 159 93	rspcdva	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑤 ) )
161	68	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ( 𝑂 Func 𝑆 ) ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) )
162	28 29 30 161 83 93	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑤 ) : ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ⟶ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ) )
163	162 116	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ℎ ) ∈ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ) )
164	72	3ad2antr1	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ∈ 𝑈 )
165	71	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) : 𝐵 ⟶ 𝑈 )
166	165 93	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ∈ 𝑈 )
167	5 102 30 164 166	elsetchom	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( 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 ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ) )
168	163 167	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ℎ ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑤 ) )
169		fcompt	⊢ ( ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑤 ) ∧ ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ℎ ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ) → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ∘ ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ℎ ) ) = ( 𝑘 ∈ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ↦ ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ‘ ( ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ℎ ) ‘ 𝑘 ) ) ) )
170	160 168 169	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ∘ ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ℎ ) ) = ( 𝑘 ∈ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ↦ ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ‘ ( ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ℎ ) ‘ 𝑘 ) ) ) )
171	157	3ad2antr1	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) )
172		fcompt	⊢ ( ( ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) : ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑤 ) ∧ ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ⟶ ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ) → ( ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) ∘ ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ) = ( 𝑘 ∈ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ↦ ( ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) ‘ ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ‘ 𝑘 ) ) ) )
173	119 171 172	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) ∘ ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ) = ( 𝑘 ∈ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ↦ ( ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) ‘ ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ‘ 𝑘 ) ) ) )
174	144 170 173	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ∘ ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ℎ ) ) = ( ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) ∘ ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ) )
175	5 102 88 164 166 108 168 160	setcco	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑤 ) ⟩ ( comp ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑤 ) ) ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ℎ ) ) = ( ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑤 ) ∘ ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) 𝑤 ) ‘ ℎ ) ) )
176	5 102 88 164 105 108 171 119	setcco	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝑂 ) 𝑤 ) ) ) → ( ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) ( ⟨ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) , ( ( 1^st ‘ 𝐹 ) ‘ 𝑧 ) ⟩ ( comp ‘ 𝑆 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑤 ) ) ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ) = ( ( ( 𝑧 ( 2^nd ‘ 𝐹 ) 𝑤 ) ‘ ℎ ) ∘ ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ) )
177	174 175 176	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ ( 𝑧 ( 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 ‘ 𝐹 ) ‘ 𝑤 ) ) ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ) )
178	177	ralrimivvva	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ∀ ℎ ∈ ( 𝑧 ( 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 ‘ 𝐹 ) ‘ 𝑤 ) ) ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ) )
179		eqid	⊢ ( 𝑂 Nat 𝑆 ) = ( 𝑂 Nat 𝑆 )
180	179 28 29 30 88 66 16	isnat2	⊢ ( 𝜑 → ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) ↔ ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ∈ X 𝑧 ∈ 𝐵 ( ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ) ‘ 𝑧 ) ( Hom ‘ 𝑆 ) ( ( 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 ‘ 𝐹 ) ‘ 𝑤 ) ) ( ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ‘ 𝑧 ) ) ) ) )
181	80 178 180	mpbir2and	⊢ ( 𝜑 → ( ( 𝐹 𝑁 𝑋 ) ‘ 𝐴 ) ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑋 ) ( 𝑂 Nat 𝑆 ) 𝐹 ) )

Metamath Proof Explorer

Theorem yonedalem4c

Proof