yonffthlem

	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	yonffthlem	⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) )

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		relfunc	⊢ Rel ( 𝐶 Func 𝑄 )
20	15	unssbd	⊢ ( 𝜑 → 𝑈 ⊆ 𝑉 )
21	13 20	ssexd	⊢ ( 𝜑 → 𝑈 ∈ V )
22	1 12 4 5 7 21 14	yoncl	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐶 Func 𝑄 ) )
23		1st2nd	⊢ ( ( Rel ( 𝐶 Func 𝑄 ) ∧ 𝑌 ∈ ( 𝐶 Func 𝑄 ) ) → 𝑌 = ⟨ ( 1^st ‘ 𝑌 ) , ( 2^nd ‘ 𝑌 ) ⟩ )
24	19 22 23	sylancr	⊢ ( 𝜑 → 𝑌 = ⟨ ( 1^st ‘ 𝑌 ) , ( 2^nd ‘ 𝑌 ) ⟩ )
25		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝑄 ) ∧ 𝑌 ∈ ( 𝐶 Func 𝑄 ) ) → ( 1^st ‘ 𝑌 ) ( 𝐶 Func 𝑄 ) ( 2^nd ‘ 𝑌 ) )
26	19 22 25	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝑌 ) ( 𝐶 Func 𝑄 ) ( 2^nd ‘ 𝑌 ) )
27		fveq2	⊢ ( 𝑣 = ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) , 𝑧 ⟩ → ( 𝑁 ‘ 𝑣 ) = ( 𝑁 ‘ ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) , 𝑧 ⟩ ) )
28		df-ov	⊢ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) 𝑁 𝑧 ) = ( 𝑁 ‘ ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) , 𝑧 ⟩ )
29	27 28	eqtr4di	⊢ ( 𝑣 = ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) , 𝑧 ⟩ → ( 𝑁 ‘ 𝑣 ) = ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) 𝑁 𝑧 ) )
30		fveq2	⊢ ( 𝑣 = ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) , 𝑧 ⟩ → ( ( 1^st ‘ 𝐸 ) ‘ 𝑣 ) = ( ( 1^st ‘ 𝐸 ) ‘ ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) , 𝑧 ⟩ ) )
31		df-ov	⊢ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ( 1^st ‘ 𝐸 ) 𝑧 ) = ( ( 1^st ‘ 𝐸 ) ‘ ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) , 𝑧 ⟩ )
32	30 31	eqtr4di	⊢ ( 𝑣 = ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) , 𝑧 ⟩ → ( ( 1^st ‘ 𝐸 ) ‘ 𝑣 ) = ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ( 1^st ‘ 𝐸 ) 𝑧 ) )
33		fveq2	⊢ ( 𝑣 = ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) , 𝑧 ⟩ → ( ( 1^st ‘ 𝑍 ) ‘ 𝑣 ) = ( ( 1^st ‘ 𝑍 ) ‘ ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) , 𝑧 ⟩ ) )
34		df-ov	⊢ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ( 1^st ‘ 𝑍 ) 𝑧 ) = ( ( 1^st ‘ 𝑍 ) ‘ ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) , 𝑧 ⟩ )
35	33 34	eqtr4di	⊢ ( 𝑣 = ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) , 𝑧 ⟩ → ( ( 1^st ‘ 𝑍 ) ‘ 𝑣 ) = ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ( 1^st ‘ 𝑍 ) 𝑧 ) )
36	32 35	oveq12d	⊢ ( 𝑣 = ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) , 𝑧 ⟩ → ( ( ( 1^st ‘ 𝐸 ) ‘ 𝑣 ) ( Iso ‘ 𝑇 ) ( ( 1^st ‘ 𝑍 ) ‘ 𝑣 ) ) = ( ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ( 1^st ‘ 𝐸 ) 𝑧 ) ( Iso ‘ 𝑇 ) ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ( 1^st ‘ 𝑍 ) 𝑧 ) ) )
37	29 36	eleq12d	⊢ ( 𝑣 = ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) , 𝑧 ⟩ → ( ( 𝑁 ‘ 𝑣 ) ∈ ( ( ( 1^st ‘ 𝐸 ) ‘ 𝑣 ) ( Iso ‘ 𝑇 ) ( ( 1^st ‘ 𝑍 ) ‘ 𝑣 ) ) ↔ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) 𝑁 𝑧 ) ∈ ( ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ( 1^st ‘ 𝐸 ) 𝑧 ) ( Iso ‘ 𝑇 ) ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ( 1^st ‘ 𝑍 ) 𝑧 ) ) ) )
38	9	fucbas	⊢ ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) = ( Base ‘ 𝑅 )
39	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	yonedalem1	⊢ ( 𝜑 → ( 𝑍 ∈ ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) ∧ 𝐸 ∈ ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) ) )
40	39	simpld	⊢ ( 𝜑 → 𝑍 ∈ ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) )
41		funcrcl	⊢ ( 𝑍 ∈ ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) → ( ( 𝑄 ×_c 𝑂 ) ∈ Cat ∧ 𝑇 ∈ Cat ) )
42	40 41	syl	⊢ ( 𝜑 → ( ( 𝑄 ×_c 𝑂 ) ∈ Cat ∧ 𝑇 ∈ Cat ) )
43	42	simpld	⊢ ( 𝜑 → ( 𝑄 ×_c 𝑂 ) ∈ Cat )
44	42	simprd	⊢ ( 𝜑 → 𝑇 ∈ Cat )
45	9 43 44	fuccat	⊢ ( 𝜑 → 𝑅 ∈ Cat )
46	39	simprd	⊢ ( 𝜑 → 𝐸 ∈ ( ( 𝑄 ×_c 𝑂 ) Func 𝑇 ) )
47		eqid	⊢ ( Iso ‘ 𝑅 ) = ( Iso ‘ 𝑅 )
48	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18	yonedainv	⊢ ( 𝜑 → 𝑀 ( 𝑍 𝐼 𝐸 ) 𝑁 )
49	38 17 45 40 46 47 48	inviso2	⊢ ( 𝜑 → 𝑁 ∈ ( 𝐸 ( Iso ‘ 𝑅 ) 𝑍 ) )
50		eqid	⊢ ( 𝑄 ×_c 𝑂 ) = ( 𝑄 ×_c 𝑂 )
51	7	fucbas	⊢ ( 𝑂 Func 𝑆 ) = ( Base ‘ 𝑄 )
52	4 2	oppcbas	⊢ 𝐵 = ( Base ‘ 𝑂 )
53	50 51 52	xpcbas	⊢ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) = ( Base ‘ ( 𝑄 ×_c 𝑂 ) )
54		eqid	⊢ ( ( 𝑄 ×_c 𝑂 ) Nat 𝑇 ) = ( ( 𝑄 ×_c 𝑂 ) Nat 𝑇 )
55		eqid	⊢ ( Iso ‘ 𝑇 ) = ( Iso ‘ 𝑇 )
56	9 53 54 46 40 47 55	fuciso	⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝐸 ( Iso ‘ 𝑅 ) 𝑍 ) ↔ ( 𝑁 ∈ ( 𝐸 ( ( 𝑄 ×_c 𝑂 ) Nat 𝑇 ) 𝑍 ) ∧ ∀ 𝑣 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ( 𝑁 ‘ 𝑣 ) ∈ ( ( ( 1^st ‘ 𝐸 ) ‘ 𝑣 ) ( Iso ‘ 𝑇 ) ( ( 1^st ‘ 𝑍 ) ‘ 𝑣 ) ) ) ) )
57	49 56	mpbid	⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝐸 ( ( 𝑄 ×_c 𝑂 ) Nat 𝑇 ) 𝑍 ) ∧ ∀ 𝑣 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ( 𝑁 ‘ 𝑣 ) ∈ ( ( ( 1^st ‘ 𝐸 ) ‘ 𝑣 ) ( Iso ‘ 𝑇 ) ( ( 1^st ‘ 𝑍 ) ‘ 𝑣 ) ) ) )
58	57	simprd	⊢ ( 𝜑 → ∀ 𝑣 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ( 𝑁 ‘ 𝑣 ) ∈ ( ( ( 1^st ‘ 𝐸 ) ‘ 𝑣 ) ( Iso ‘ 𝑇 ) ( ( 1^st ‘ 𝑍 ) ‘ 𝑣 ) ) )
59	58	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ∀ 𝑣 ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) ( 𝑁 ‘ 𝑣 ) ∈ ( ( ( 1^st ‘ 𝐸 ) ‘ 𝑣 ) ( Iso ‘ 𝑇 ) ( ( 1^st ‘ 𝑍 ) ‘ 𝑣 ) ) )
60	2 51 26	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝑌 ) : 𝐵 ⟶ ( 𝑂 Func 𝑆 ) )
61	60	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 1^st ‘ 𝑌 ) : 𝐵 ⟶ ( 𝑂 Func 𝑆 ) )
62		simprr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → 𝑤 ∈ 𝐵 )
63	61 62	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ∈ ( 𝑂 Func 𝑆 ) )
64		simprl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → 𝑧 ∈ 𝐵 )
65	63 64	opelxpd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ⟨ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) , 𝑧 ⟩ ∈ ( ( 𝑂 Func 𝑆 ) × 𝐵 ) )
66	37 59 65	rspcdva	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) 𝑁 𝑧 ) ∈ ( ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ( 1^st ‘ 𝐸 ) 𝑧 ) ( Iso ‘ 𝑇 ) ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ( 1^st ‘ 𝑍 ) 𝑧 ) ) )
67	4	oppccat	⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
68	12 67	syl	⊢ ( 𝜑 → 𝑂 ∈ Cat )
69	68	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → 𝑂 ∈ Cat )
70	5	setccat	⊢ ( 𝑈 ∈ V → 𝑆 ∈ Cat )
71	21 70	syl	⊢ ( 𝜑 → 𝑆 ∈ Cat )
72	71	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → 𝑆 ∈ Cat )
73	10 69 72 52 63 64	evlf1	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ( 1^st ‘ 𝐸 ) 𝑧 ) = ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ‘ 𝑧 ) )
74	12	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → 𝐶 ∈ Cat )
75		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
76	1 2 74 62 75 64	yon11	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ‘ 𝑧 ) = ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) )
77	73 76	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ( 1^st ‘ 𝐸 ) 𝑧 ) = ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) )
78	13	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → 𝑉 ∈ 𝑊 )
79	14	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ran ( Hom_f ‘ 𝐶 ) ⊆ 𝑈 )
80	15	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ran ( Hom_f ‘ 𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 )
81	1 2 3 4 5 6 7 8 9 10 11 74 78 79 80 63 64	yonedalem21	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ( 1^st ‘ 𝑍 ) 𝑧 ) = ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) )
82	77 81	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ( 1^st ‘ 𝐸 ) 𝑧 ) ( Iso ‘ 𝑇 ) ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ( 1^st ‘ 𝑍 ) 𝑧 ) ) = ( ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ( Iso ‘ 𝑇 ) ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ) )
83	66 82	eleqtrd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) 𝑁 𝑧 ) ∈ ( ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ( Iso ‘ 𝑇 ) ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ) )
84	20	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → 𝑈 ⊆ 𝑉 )
85		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
86		relfunc	⊢ Rel ( 𝑂 Func 𝑆 )
87		1st2ndbr	⊢ ( ( Rel ( 𝑂 Func 𝑆 ) ∧ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ∈ ( 𝑂 Func 𝑆 ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ( 𝑂 Func 𝑆 ) ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) )
88	86 63 87	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ( 𝑂 Func 𝑆 ) ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) )
89	52 85 88	funcf1	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) : 𝐵 ⟶ ( Base ‘ 𝑆 ) )
90	89 64	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ‘ 𝑧 ) ∈ ( Base ‘ 𝑆 ) )
91	5 21	setcbas	⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝑆 ) )
92	91	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → 𝑈 = ( Base ‘ 𝑆 ) )
93	90 92	eleqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ‘ 𝑧 ) ∈ 𝑈 )
94	76 93	eqeltrrd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ∈ 𝑈 )
95	84 94	sseldd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ∈ 𝑉 )
96		eqid	⊢ ( Hom_f ‘ 𝑄 ) = ( Hom_f ‘ 𝑄 )
97		eqid	⊢ ( 𝑂 Nat 𝑆 ) = ( 𝑂 Nat 𝑆 )
98	7 97	fuchom	⊢ ( 𝑂 Nat 𝑆 ) = ( Hom ‘ 𝑄 )
99	61 64	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ∈ ( 𝑂 Func 𝑆 ) )
100	96 51 98 99 63	homfval	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ( Hom_f ‘ 𝑄 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) = ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) )
101	15	unssad	⊢ ( 𝜑 → ran ( Hom_f ‘ 𝑄 ) ⊆ 𝑉 )
102	101	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ran ( Hom_f ‘ 𝑄 ) ⊆ 𝑉 )
103	96 51	homffn	⊢ ( Hom_f ‘ 𝑄 ) Fn ( ( 𝑂 Func 𝑆 ) × ( 𝑂 Func 𝑆 ) )
104		fnovrn	⊢ ( ( ( Hom_f ‘ 𝑄 ) Fn ( ( 𝑂 Func 𝑆 ) × ( 𝑂 Func 𝑆 ) ) ∧ ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ∈ ( 𝑂 Func 𝑆 ) ∧ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ∈ ( 𝑂 Func 𝑆 ) ) → ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ( Hom_f ‘ 𝑄 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ∈ ran ( Hom_f ‘ 𝑄 ) )
105	103 99 63 104	mp3an2i	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ( Hom_f ‘ 𝑄 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ∈ ran ( Hom_f ‘ 𝑄 ) )
106	102 105	sseldd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ( Hom_f ‘ 𝑄 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ∈ 𝑉 )
107	100 106	eqeltrrd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ∈ 𝑉 )
108	6 78 95 107 55	setciso	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) 𝑁 𝑧 ) ∈ ( ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ( Iso ‘ 𝑇 ) ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ) ↔ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) 𝑁 𝑧 ) : ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) –1-1-onto→ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ) )
109	83 108	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) 𝑁 𝑧 ) : ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) –1-1-onto→ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) )
110	74	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) → 𝐶 ∈ Cat )
111	110	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ Cat )
112	64	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) → 𝑧 ∈ 𝐵 )
113	112	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
114		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
115	1 2 111 113 75 114	yon11	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ) ‘ 𝑦 ) = ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
116	115	eqcomd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) = ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ) ‘ 𝑦 ) )
117	111	adantr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) → 𝐶 ∈ Cat )
118	62	ad3antrrr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) → 𝑤 ∈ 𝐵 )
119	113	adantr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) → 𝑧 ∈ 𝐵 )
120		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
121	114	adantr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) → 𝑦 ∈ 𝐵 )
122		simpr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
123		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) → ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) )
124	1 2 117 118 75 119 120 121 122 123	yon12	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) → ( ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) 𝑦 ) ‘ 𝑔 ) ‘ ℎ ) = ( ℎ ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑔 ) )
125	1 2 117 119 75 118 120 121 123 122	yon2	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) → ( ( ( ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) ‘ ℎ ) ‘ 𝑦 ) ‘ 𝑔 ) = ( ℎ ( ⟨ 𝑦 , 𝑧 ⟩ ( comp ‘ 𝐶 ) 𝑤 ) 𝑔 ) )
126	124 125	eqtr4d	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) → ( ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) 𝑦 ) ‘ 𝑔 ) ‘ ℎ ) = ( ( ( ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) ‘ ℎ ) ‘ 𝑦 ) ‘ 𝑔 ) )
127	116 126	mpteq12dva	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ↦ ( ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) 𝑦 ) ‘ 𝑔 ) ‘ ℎ ) ) = ( 𝑔 ∈ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ) ‘ 𝑦 ) ↦ ( ( ( ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) ‘ ℎ ) ‘ 𝑦 ) ‘ 𝑔 ) ) )
128	26	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 1^st ‘ 𝑌 ) ( 𝐶 Func 𝑄 ) ( 2^nd ‘ 𝑌 ) )
129	2 75 98 128 64 62	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) : ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ⟶ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) )
130	129	ffvelrnda	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) → ( ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) ‘ ℎ ) ∈ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) )
131	97 130	nat1st2nd	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) → ( ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) ‘ ℎ ) ∈ ( ⟨ ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ) , ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ) ⟩ ( 𝑂 Nat 𝑆 ) ⟨ ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) , ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ⟩ ) )
132	131	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) ‘ ℎ ) ∈ ( ⟨ ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ) , ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ) ⟩ ( 𝑂 Nat 𝑆 ) ⟨ ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) , ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ⟩ ) )
133		eqid	⊢ ( Hom ‘ 𝑆 ) = ( Hom ‘ 𝑆 )
134	97 132 52 133 114	natcl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) ‘ ℎ ) ‘ 𝑦 ) ∈ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ) ‘ 𝑦 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ‘ 𝑦 ) ) )
135	21	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → 𝑈 ∈ V )
136	135	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑈 ∈ V )
137	60	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) → ( 1^st ‘ 𝑌 ) : 𝐵 ⟶ ( 𝑂 Func 𝑆 ) )
138	137 112	ffvelrnd	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) → ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ∈ ( 𝑂 Func 𝑆 ) )
139		1st2ndbr	⊢ ( ( Rel ( 𝑂 Func 𝑆 ) ∧ ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ∈ ( 𝑂 Func 𝑆 ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ) ( 𝑂 Func 𝑆 ) ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ) )
140	86 138 139	sylancr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ) ( 𝑂 Func 𝑆 ) ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ) )
141	52 85 140	funcf1	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ) : 𝐵 ⟶ ( Base ‘ 𝑆 ) )
142	141	ffvelrnda	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑆 ) )
143	92	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑈 = ( Base ‘ 𝑆 ) )
144	142 143	eleqtrrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ) ‘ 𝑦 ) ∈ 𝑈 )
145	89	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) : 𝐵 ⟶ ( Base ‘ 𝑆 ) )
146	145	ffvelrnda	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑆 ) )
147	146 143	eleqtrrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ‘ 𝑦 ) ∈ 𝑈 )
148	5 136 133 144 147	elsetchom	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( ( ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) ‘ ℎ ) ‘ 𝑦 ) ∈ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ) ‘ 𝑦 ) ( Hom ‘ 𝑆 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ‘ 𝑦 ) ) ↔ ( ( ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) ‘ ℎ ) ‘ 𝑦 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ) ‘ 𝑦 ) ⟶ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ‘ 𝑦 ) ) )
149	134 148	mpbid	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) ‘ ℎ ) ‘ 𝑦 ) : ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ) ‘ 𝑦 ) ⟶ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ‘ 𝑦 ) )
150	149	feqmptd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) ‘ ℎ ) ‘ 𝑦 ) = ( 𝑔 ∈ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ) ‘ 𝑦 ) ↦ ( ( ( ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) ‘ ℎ ) ‘ 𝑦 ) ‘ 𝑔 ) ) )
151	127 150	eqtr4d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ↦ ( ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) 𝑦 ) ‘ 𝑔 ) ‘ ℎ ) ) = ( ( ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) ‘ ℎ ) ‘ 𝑦 ) )
152	151	mpteq2dva	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) → ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ↦ ( ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) 𝑦 ) ‘ 𝑔 ) ‘ ℎ ) ) ) = ( 𝑦 ∈ 𝐵 ↦ ( ( ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) ‘ ℎ ) ‘ 𝑦 ) ) )
153	78	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) → 𝑉 ∈ 𝑊 )
154	79	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) → ran ( Hom_f ‘ 𝐶 ) ⊆ 𝑈 )
155	80	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) → ( ran ( Hom_f ‘ 𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 )
156	63	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) → ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ∈ ( 𝑂 Func 𝑆 ) )
157	76	eleq2d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ℎ ∈ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ‘ 𝑧 ) ↔ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) )
158	157	biimpar	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) → ℎ ∈ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ‘ 𝑧 ) )
159	1 2 3 4 5 6 7 8 9 10 11 110 153 154 155 156 112 18 158	yonedalem4a	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) → ( ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) 𝑁 𝑧 ) ‘ ℎ ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ↦ ( ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) 𝑦 ) ‘ 𝑔 ) ‘ ℎ ) ) ) )
160	97 131 52	natfn	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) → ( ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) ‘ ℎ ) Fn 𝐵 )
161		dffn5	⊢ ( ( ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) ‘ ℎ ) Fn 𝐵 ↔ ( ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) ‘ ℎ ) = ( 𝑦 ∈ 𝐵 ↦ ( ( ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) ‘ ℎ ) ‘ 𝑦 ) ) )
162	160 161	sylib	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) → ( ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) ‘ ℎ ) = ( 𝑦 ∈ 𝐵 ↦ ( ( ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) ‘ ℎ ) ‘ 𝑦 ) ) )
163	152 159 162	3eqtr4d	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) ∧ ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ) → ( ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) 𝑁 𝑧 ) ‘ ℎ ) = ( ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) ‘ ℎ ) )
164	163	mpteq2dva	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ↦ ( ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) 𝑁 𝑧 ) ‘ ℎ ) ) = ( ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ↦ ( ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) ‘ ℎ ) ) )
165		f1of	⊢ ( ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) 𝑁 𝑧 ) : ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) –1-1-onto→ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) → ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) 𝑁 𝑧 ) : ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ⟶ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) )
166	109 165	syl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) 𝑁 𝑧 ) : ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ⟶ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) )
167	166	feqmptd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) 𝑁 𝑧 ) = ( ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ↦ ( ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) 𝑁 𝑧 ) ‘ ℎ ) ) )
168	129	feqmptd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) = ( ℎ ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) ↦ ( ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) ‘ ℎ ) ) )
169	164 167 168	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) 𝑁 𝑧 ) = ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) )
170		f1oeq1	⊢ ( ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) 𝑁 𝑧 ) = ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) → ( ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) 𝑁 𝑧 ) : ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) –1-1-onto→ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ↔ ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) : ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) –1-1-onto→ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ) )
171	169 170	syl	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) 𝑁 𝑧 ) : ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) –1-1-onto→ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ↔ ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) : ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) –1-1-onto→ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ) )
172	109 171	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) : ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) –1-1-onto→ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) )
173	172	ralrimivva	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) : ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) –1-1-onto→ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) )
174	2 75 98	isffth2	⊢ ( ( 1^st ‘ 𝑌 ) ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) ( 2^nd ‘ 𝑌 ) ↔ ( ( 1^st ‘ 𝑌 ) ( 𝐶 Func 𝑄 ) ( 2^nd ‘ 𝑌 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 ( 2^nd ‘ 𝑌 ) 𝑤 ) : ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) –1-1-onto→ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑧 ) ( 𝑂 Nat 𝑆 ) ( ( 1^st ‘ 𝑌 ) ‘ 𝑤 ) ) ) )
175	26 173 174	sylanbrc	⊢ ( 𝜑 → ( 1^st ‘ 𝑌 ) ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) ( 2^nd ‘ 𝑌 ) )
176		df-br	⊢ ( ( 1^st ‘ 𝑌 ) ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) ( 2^nd ‘ 𝑌 ) ↔ ⟨ ( 1^st ‘ 𝑌 ) , ( 2^nd ‘ 𝑌 ) ⟩ ∈ ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) )
177	175 176	sylib	⊢ ( 𝜑 → ⟨ ( 1^st ‘ 𝑌 ) , ( 2^nd ‘ 𝑌 ) ⟩ ∈ ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) )
178	24 177	eqeltrd	⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) )

Metamath Proof Explorer

Theorem yonffthlem

Proof