yonffthlem

	Ref	Expression
Hypotheses	yoneda.y	$⊢ Y = Yon (C)$
	yoneda.b	$⊢ B = {Base}_{C}$
	yoneda.1	$⊢ \underset{˙}{1} = Id (C)$
	yoneda.o	$⊢ O = oppCat (C)$
	yoneda.s	$⊢ S = SetCat (U)$
	yoneda.t	$⊢ T = SetCat (V)$
	yoneda.q	$⊢ Q = O FuncCat S$
	yoneda.h	$⊢ H = {Hom}_{F} (Q)$
	yoneda.r	$⊢ R = (Q \times_{c} O) FuncCat T$
	yoneda.e	$⊢ E = O {eval}_{F} S$
	yoneda.z	$⊢ Z = H \circ_{func} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O))$
	yoneda.c	$⊢ φ \to C \in Cat$
	yoneda.w	$⊢ φ \to V \in W$
	yoneda.u	$⊢ φ \to ran {Hom}_{𝑓} (C) \subseteq U$
	yoneda.v	$⊢ φ \to ran {Hom}_{𝑓} (Q) \cup U \subseteq V$
	yoneda.m	$⊢ M = (f \in (O Func S), x \in B ⟼ (a \in (1^{st} (Y) (x) (O Nat S) f) ⟼ a (x) (\underset{˙}{1} (x))))$
	yonedainv.i	$⊢ I = Inv (R)$
	yonedainv.n	$⊢ N = (f \in (O Func S), x \in B ⟼ (u \in 1^{st} (f) (x) ⟼ (y \in B ⟼ (g \in (y Hom (C) x) ⟼ (x 2^{nd} (f) y) (g) (u)))))$
Assertion	yonffthlem	$⊢ φ \to Y \in ((C Full Q) \cap (C Faith Q))$

Proof

Step	Hyp	Ref	Expression
1		yoneda.y	$⊢ Y = Yon (C)$
2		yoneda.b	$⊢ B = {Base}_{C}$
3		yoneda.1	$⊢ \underset{˙}{1} = Id (C)$
4		yoneda.o	$⊢ O = oppCat (C)$
5		yoneda.s	$⊢ S = SetCat (U)$
6		yoneda.t	$⊢ T = SetCat (V)$
7		yoneda.q	$⊢ Q = O FuncCat S$
8		yoneda.h	$⊢ H = {Hom}_{F} (Q)$
9		yoneda.r	$⊢ R = (Q \times_{c} O) FuncCat T$
10		yoneda.e	$⊢ E = O {eval}_{F} S$
11		yoneda.z	$⊢ Z = H \circ_{func} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O))$
12		yoneda.c	$⊢ φ \to C \in Cat$
13		yoneda.w	$⊢ φ \to V \in W$
14		yoneda.u	$⊢ φ \to ran {Hom}_{𝑓} (C) \subseteq U$
15		yoneda.v	$⊢ φ \to ran {Hom}_{𝑓} (Q) \cup U \subseteq V$
16		yoneda.m	$⊢ M = (f \in (O Func S), x \in B ⟼ (a \in (1^{st} (Y) (x) (O Nat S) f) ⟼ a (x) (\underset{˙}{1} (x))))$
17		yonedainv.i	$⊢ I = Inv (R)$
18		yonedainv.n	$⊢ N = (f \in (O Func S), x \in B ⟼ (u \in 1^{st} (f) (x) ⟼ (y \in B ⟼ (g \in (y Hom (C) x) ⟼ (x 2^{nd} (f) y) (g) (u)))))$
19		relfunc	$⊢ Rel (C Func Q)$
20	15	unssbd	$⊢ φ \to U \subseteq V$
21	13 20	ssexd	$⊢ φ \to U \in V$
22	1 12 4 5 7 21 14	yoncl	$⊢ φ \to Y \in (C Func Q)$
23		1st2nd	$⊢ (Rel (C Func Q) \land Y \in (C Func Q)) \to Y = ⟨1^{st} (Y), 2^{nd} (Y)⟩$
24	19 22 23	sylancr	$⊢ φ \to Y = ⟨1^{st} (Y), 2^{nd} (Y)⟩$
25		1st2ndbr	$⊢ (Rel (C Func Q) \land Y \in (C Func Q)) \to 1^{st} (Y) (C Func Q) 2^{nd} (Y)$
26	19 22 25	sylancr	$⊢ φ \to 1^{st} (Y) (C Func Q) 2^{nd} (Y)$
27		fveq2	$⊢ v = ⟨1^{st} (Y) (w), z⟩ \to N (v) = N (⟨1^{st} (Y) (w), z⟩)$
28		df-ov	$⊢ 1^{st} (Y) (w) N z = N (⟨1^{st} (Y) (w), z⟩)$
29	27 28	eqtr4di	$⊢ v = ⟨1^{st} (Y) (w), z⟩ \to N (v) = 1^{st} (Y) (w) N z$
30		fveq2	$⊢ v = ⟨1^{st} (Y) (w), z⟩ \to 1^{st} (E) (v) = 1^{st} (E) (⟨1^{st} (Y) (w), z⟩)$
31		df-ov	$⊢ 1^{st} (Y) (w) 1^{st} (E) z = 1^{st} (E) (⟨1^{st} (Y) (w), z⟩)$
32	30 31	eqtr4di	$⊢ v = ⟨1^{st} (Y) (w), z⟩ \to 1^{st} (E) (v) = 1^{st} (Y) (w) 1^{st} (E) z$
33		fveq2	$⊢ v = ⟨1^{st} (Y) (w), z⟩ \to 1^{st} (Z) (v) = 1^{st} (Z) (⟨1^{st} (Y) (w), z⟩)$
34		df-ov	$⊢ 1^{st} (Y) (w) 1^{st} (Z) z = 1^{st} (Z) (⟨1^{st} (Y) (w), z⟩)$
35	33 34	eqtr4di	$⊢ v = ⟨1^{st} (Y) (w), z⟩ \to 1^{st} (Z) (v) = 1^{st} (Y) (w) 1^{st} (Z) z$
36	32 35	oveq12d	$⊢ v = ⟨1^{st} (Y) (w), z⟩ \to 1^{st} (E) (v) Iso (T) 1^{st} (Z) (v) = (1^{st} (Y) (w) 1^{st} (E) z) Iso (T) (1^{st} (Y) (w) 1^{st} (Z) z)$
37	29 36	eleq12d	$⊢ v = ⟨1^{st} (Y) (w), z⟩ \to (N (v) \in (1^{st} (E) (v) Iso (T) 1^{st} (Z) (v)) \leftrightarrow 1^{st} (Y) (w) N z \in ((1^{st} (Y) (w) 1^{st} (E) z) Iso (T) (1^{st} (Y) (w) 1^{st} (Z) z)))$
38	9	fucbas	$⊢ (Q \times_{c} O) Func T = {Base}_{R}$
39	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	yonedalem1	$⊢ φ \to (Z \in ((Q \times_{c} O) Func T) \land E \in ((Q \times_{c} O) Func T))$
40	39	simpld	$⊢ φ \to Z \in ((Q \times_{c} O) Func T)$
41		funcrcl	$⊢ Z \in ((Q \times_{c} O) Func T) \to (Q \times_{c} O \in Cat \land T \in Cat)$
42	40 41	syl	$⊢ φ \to (Q \times_{c} O \in Cat \land T \in Cat)$
43	42	simpld	$⊢ φ \to Q \times_{c} O \in Cat$
44	42	simprd	$⊢ φ \to T \in Cat$
45	9 43 44	fuccat	$⊢ φ \to R \in Cat$
46	39	simprd	$⊢ φ \to E \in ((Q \times_{c} O) Func T)$
47		eqid	$⊢ Iso (R) = Iso (R)$
48	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18	yonedainv	$⊢ φ \to M (Z I E) N$
49	38 17 45 40 46 47 48	inviso2	$⊢ φ \to N \in (E Iso (R) Z)$
50		eqid	$⊢ Q \times_{c} O = Q \times_{c} O$
51	7	fucbas	$⊢ O Func S = {Base}_{Q}$
52	4 2	oppcbas	$⊢ B = {Base}_{O}$
53	50 51 52	xpcbas	$⊢ (O Func S) \times B = {Base}_{(Q \times_{c} O)}$
54		eqid	$⊢ (Q \times_{c} O) Nat T = (Q \times_{c} O) Nat T$
55		eqid	$⊢ Iso (T) = Iso (T)$
56	9 53 54 46 40 47 55	fuciso	$⊢ φ \to (N \in (E Iso (R) Z) \leftrightarrow (N \in (E ((Q \times_{c} O) Nat T) Z) \land \forall v \in ((O Func S) \times B) N (v) \in (1^{st} (E) (v) Iso (T) 1^{st} (Z) (v))))$
57	49 56	mpbid	$⊢ φ \to (N \in (E ((Q \times_{c} O) Nat T) Z) \land \forall v \in ((O Func S) \times B) N (v) \in (1^{st} (E) (v) Iso (T) 1^{st} (Z) (v)))$
58	57	simprd	$⊢ φ \to \forall v \in ((O Func S) \times B) N (v) \in (1^{st} (E) (v) Iso (T) 1^{st} (Z) (v))$
59	58	adantr	$⊢ (φ \land (z \in B \land w \in B)) \to \forall v \in ((O Func S) \times B) N (v) \in (1^{st} (E) (v) Iso (T) 1^{st} (Z) (v))$
60	2 51 26	funcf1	$⊢ φ \to 1^{st} (Y) : B ⟶ O Func S$
61	60	adantr	$⊢ (φ \land (z \in B \land w \in B)) \to 1^{st} (Y) : B ⟶ O Func S$
62		simprr	$⊢ (φ \land (z \in B \land w \in B)) \to w \in B$
63	61 62	ffvelrnd	$⊢ (φ \land (z \in B \land w \in B)) \to 1^{st} (Y) (w) \in (O Func S)$
64		simprl	$⊢ (φ \land (z \in B \land w \in B)) \to z \in B$
65	63 64	opelxpd	$⊢ (φ \land (z \in B \land w \in B)) \to ⟨1^{st} (Y) (w), z⟩ \in ((O Func S) \times B)$
66	37 59 65	rspcdva	$⊢ (φ \land (z \in B \land w \in B)) \to 1^{st} (Y) (w) N z \in ((1^{st} (Y) (w) 1^{st} (E) z) Iso (T) (1^{st} (Y) (w) 1^{st} (Z) z))$
67	4	oppccat	$⊢ C \in Cat \to O \in Cat$
68	12 67	syl	$⊢ φ \to O \in Cat$
69	68	adantr	$⊢ (φ \land (z \in B \land w \in B)) \to O \in Cat$
70	5	setccat	$⊢ U \in V \to S \in Cat$
71	21 70	syl	$⊢ φ \to S \in Cat$
72	71	adantr	$⊢ (φ \land (z \in B \land w \in B)) \to S \in Cat$
73	10 69 72 52 63 64	evlf1	$⊢ (φ \land (z \in B \land w \in B)) \to 1^{st} (Y) (w) 1^{st} (E) z = 1^{st} (1^{st} (Y) (w)) (z)$
74	12	adantr	$⊢ (φ \land (z \in B \land w \in B)) \to C \in Cat$
75		eqid	$⊢ Hom (C) = Hom (C)$
76	1 2 74 62 75 64	yon11	$⊢ (φ \land (z \in B \land w \in B)) \to 1^{st} (1^{st} (Y) (w)) (z) = z Hom (C) w$
77	73 76	eqtrd	$⊢ (φ \land (z \in B \land w \in B)) \to 1^{st} (Y) (w) 1^{st} (E) z = z Hom (C) w$
78	13	adantr	$⊢ (φ \land (z \in B \land w \in B)) \to V \in W$
79	14	adantr	$⊢ (φ \land (z \in B \land w \in B)) \to ran {Hom}_{𝑓} (C) \subseteq U$
80	15	adantr	$⊢ (φ \land (z \in B \land w \in B)) \to ran {Hom}_{𝑓} (Q) \cup U \subseteq V$
81	1 2 3 4 5 6 7 8 9 10 11 74 78 79 80 63 64	yonedalem21	$⊢ (φ \land (z \in B \land w \in B)) \to 1^{st} (Y) (w) 1^{st} (Z) z = 1^{st} (Y) (z) (O Nat S) 1^{st} (Y) (w)$
82	77 81	oveq12d	$⊢ (φ \land (z \in B \land w \in B)) \to (1^{st} (Y) (w) 1^{st} (E) z) Iso (T) (1^{st} (Y) (w) 1^{st} (Z) z) = (z Hom (C) w) Iso (T) (1^{st} (Y) (z) (O Nat S) 1^{st} (Y) (w))$
83	66 82	eleqtrd	$⊢ (φ \land (z \in B \land w \in B)) \to 1^{st} (Y) (w) N z \in ((z Hom (C) w) Iso (T) (1^{st} (Y) (z) (O Nat S) 1^{st} (Y) (w)))$
84	20	adantr	$⊢ (φ \land (z \in B \land w \in B)) \to U \subseteq V$
85		eqid	$⊢ {Base}_{S} = {Base}_{S}$
86		relfunc	$⊢ Rel (O Func S)$
87		1st2ndbr	$⊢ (Rel (O Func S) \land 1^{st} (Y) (w) \in (O Func S)) \to 1^{st} (1^{st} (Y) (w)) (O Func S) 2^{nd} (1^{st} (Y) (w))$
88	86 63 87	sylancr	$⊢ (φ \land (z \in B \land w \in B)) \to 1^{st} (1^{st} (Y) (w)) (O Func S) 2^{nd} (1^{st} (Y) (w))$
89	52 85 88	funcf1	$⊢ (φ \land (z \in B \land w \in B)) \to 1^{st} (1^{st} (Y) (w)) : B ⟶ {Base}_{S}$
90	89 64	ffvelrnd	$⊢ (φ \land (z \in B \land w \in B)) \to 1^{st} (1^{st} (Y) (w)) (z) \in {Base}_{S}$
91	5 21	setcbas	$⊢ φ \to U = {Base}_{S}$
92	91	adantr	$⊢ (φ \land (z \in B \land w \in B)) \to U = {Base}_{S}$
93	90 92	eleqtrrd	$⊢ (φ \land (z \in B \land w \in B)) \to 1^{st} (1^{st} (Y) (w)) (z) \in U$
94	76 93	eqeltrrd	$⊢ (φ \land (z \in B \land w \in B)) \to z Hom (C) w \in U$
95	84 94	sseldd	$⊢ (φ \land (z \in B \land w \in B)) \to z Hom (C) w \in V$
96		eqid	$⊢ {Hom}_{𝑓} (Q) = {Hom}_{𝑓} (Q)$
97		eqid	$⊢ O Nat S = O Nat S$
98	7 97	fuchom	$⊢ O Nat S = Hom (Q)$
99	61 64	ffvelrnd	$⊢ (φ \land (z \in B \land w \in B)) \to 1^{st} (Y) (z) \in (O Func S)$
100	96 51 98 99 63	homfval	$⊢ (φ \land (z \in B \land w \in B)) \to 1^{st} (Y) (z) {Hom}_{𝑓} (Q) 1^{st} (Y) (w) = 1^{st} (Y) (z) (O Nat S) 1^{st} (Y) (w)$
101	15	unssad	$⊢ φ \to ran {Hom}_{𝑓} (Q) \subseteq V$
102	101	adantr	$⊢ (φ \land (z \in B \land w \in B)) \to ran {Hom}_{𝑓} (Q) \subseteq V$
103	96 51	homffn	$⊢ {Hom}_{𝑓} (Q) Fn ((O Func S) \times (O Func S))$
104		fnovrn	$⊢ ({Hom}_{𝑓} (Q) Fn ((O Func S) \times (O Func S)) \land 1^{st} (Y) (z) \in (O Func S) \land 1^{st} (Y) (w) \in (O Func S)) \to 1^{st} (Y) (z) {Hom}_{𝑓} (Q) 1^{st} (Y) (w) \in ran {Hom}_{𝑓} (Q)$
105	103 99 63 104	mp3an2i	$⊢ (φ \land (z \in B \land w \in B)) \to 1^{st} (Y) (z) {Hom}_{𝑓} (Q) 1^{st} (Y) (w) \in ran {Hom}_{𝑓} (Q)$
106	102 105	sseldd	$⊢ (φ \land (z \in B \land w \in B)) \to 1^{st} (Y) (z) {Hom}_{𝑓} (Q) 1^{st} (Y) (w) \in V$
107	100 106	eqeltrrd	$⊢ (φ \land (z \in B \land w \in B)) \to 1^{st} (Y) (z) (O Nat S) 1^{st} (Y) (w) \in V$
108	6 78 95 107 55	setciso	$⊢ (φ \land (z \in B \land w \in B)) \to (1^{st} (Y) (w) N z \in ((z Hom (C) w) Iso (T) (1^{st} (Y) (z) (O Nat S) 1^{st} (Y) (w))) \leftrightarrow (1^{st} (Y) (w) N z) : z Hom (C) w \underset{1-1 onto}{⟶} 1^{st} (Y) (z) (O Nat S) 1^{st} (Y) (w))$
109	83 108	mpbid	$⊢ (φ \land (z \in B \land w \in B)) \to (1^{st} (Y) (w) N z) : z Hom (C) w \underset{1-1 onto}{⟶} 1^{st} (Y) (z) (O Nat S) 1^{st} (Y) (w)$
110	74	adantr	$⊢ ((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \to C \in Cat$
111	110	adantr	$⊢ (((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \to C \in Cat$
112	64	adantr	$⊢ ((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \to z \in B$
113	112	adantr	$⊢ (((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \to z \in B$
114		simpr	$⊢ (((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \to y \in B$
115	1 2 111 113 75 114	yon11	$⊢ (((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \to 1^{st} (1^{st} (Y) (z)) (y) = y Hom (C) z$
116	115	eqcomd	$⊢ (((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \to y Hom (C) z = 1^{st} (1^{st} (Y) (z)) (y)$
117	111	adantr	$⊢ ((((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \land g \in (y Hom (C) z)) \to C \in Cat$
118	62	ad3antrrr	$⊢ ((((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \land g \in (y Hom (C) z)) \to w \in B$
119	113	adantr	$⊢ ((((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \land g \in (y Hom (C) z)) \to z \in B$
120		eqid	$⊢ comp (C) = comp (C)$
121	114	adantr	$⊢ ((((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \land g \in (y Hom (C) z)) \to y \in B$
122		simpr	$⊢ ((((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \land g \in (y Hom (C) z)) \to g \in (y Hom (C) z)$
123		simpllr	$⊢ ((((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \land g \in (y Hom (C) z)) \to h \in (z Hom (C) w)$
124	1 2 117 118 75 119 120 121 122 123	yon12	$⊢ ((((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \land g \in (y Hom (C) z)) \to (z 2^{nd} (1^{st} (Y) (w)) y) (g) (h) = h (⟨y, z⟩ comp (C) w) g$
125	1 2 117 119 75 118 120 121 123 122	yon2	$⊢ ((((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \land g \in (y Hom (C) z)) \to (z 2^{nd} (Y) w) (h) (y) (g) = h (⟨y, z⟩ comp (C) w) g$
126	124 125	eqtr4d	$⊢ ((((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \land g \in (y Hom (C) z)) \to (z 2^{nd} (1^{st} (Y) (w)) y) (g) (h) = (z 2^{nd} (Y) w) (h) (y) (g)$
127	116 126	mpteq12dva	$⊢ (((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \to (g \in (y Hom (C) z) ⟼ (z 2^{nd} (1^{st} (Y) (w)) y) (g) (h)) = (g \in 1^{st} (1^{st} (Y) (z)) (y) ⟼ (z 2^{nd} (Y) w) (h) (y) (g))$
128	26	adantr	$⊢ (φ \land (z \in B \land w \in B)) \to 1^{st} (Y) (C Func Q) 2^{nd} (Y)$
129	2 75 98 128 64 62	funcf2	$⊢ (φ \land (z \in B \land w \in B)) \to (z 2^{nd} (Y) w) : z Hom (C) w ⟶ 1^{st} (Y) (z) (O Nat S) 1^{st} (Y) (w)$
130	129	ffvelrnda	$⊢ ((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \to (z 2^{nd} (Y) w) (h) \in (1^{st} (Y) (z) (O Nat S) 1^{st} (Y) (w))$
131	97 130	nat1st2nd	$⊢ ((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \to (z 2^{nd} (Y) w) (h) \in (⟨1^{st} (1^{st} (Y) (z)), 2^{nd} (1^{st} (Y) (z))⟩ (O Nat S) ⟨1^{st} (1^{st} (Y) (w)), 2^{nd} (1^{st} (Y) (w))⟩)$
132	131	adantr	$⊢ (((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \to (z 2^{nd} (Y) w) (h) \in (⟨1^{st} (1^{st} (Y) (z)), 2^{nd} (1^{st} (Y) (z))⟩ (O Nat S) ⟨1^{st} (1^{st} (Y) (w)), 2^{nd} (1^{st} (Y) (w))⟩)$
133		eqid	$⊢ Hom (S) = Hom (S)$
134	97 132 52 133 114	natcl	$⊢ (((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \to (z 2^{nd} (Y) w) (h) (y) \in (1^{st} (1^{st} (Y) (z)) (y) Hom (S) 1^{st} (1^{st} (Y) (w)) (y))$
135	21	adantr	$⊢ (φ \land (z \in B \land w \in B)) \to U \in V$
136	135	ad2antrr	$⊢ (((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \to U \in V$
137	60	ad2antrr	$⊢ ((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \to 1^{st} (Y) : B ⟶ O Func S$
138	137 112	ffvelrnd	$⊢ ((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \to 1^{st} (Y) (z) \in (O Func S)$
139		1st2ndbr	$⊢ (Rel (O Func S) \land 1^{st} (Y) (z) \in (O Func S)) \to 1^{st} (1^{st} (Y) (z)) (O Func S) 2^{nd} (1^{st} (Y) (z))$
140	86 138 139	sylancr	$⊢ ((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \to 1^{st} (1^{st} (Y) (z)) (O Func S) 2^{nd} (1^{st} (Y) (z))$
141	52 85 140	funcf1	$⊢ ((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \to 1^{st} (1^{st} (Y) (z)) : B ⟶ {Base}_{S}$
142	141	ffvelrnda	$⊢ (((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \to 1^{st} (1^{st} (Y) (z)) (y) \in {Base}_{S}$
143	92	ad2antrr	$⊢ (((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \to U = {Base}_{S}$
144	142 143	eleqtrrd	$⊢ (((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \to 1^{st} (1^{st} (Y) (z)) (y) \in U$
145	89	adantr	$⊢ ((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \to 1^{st} (1^{st} (Y) (w)) : B ⟶ {Base}_{S}$
146	145	ffvelrnda	$⊢ (((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \to 1^{st} (1^{st} (Y) (w)) (y) \in {Base}_{S}$
147	146 143	eleqtrrd	$⊢ (((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \to 1^{st} (1^{st} (Y) (w)) (y) \in U$
148	5 136 133 144 147	elsetchom	$⊢ (((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \to ((z 2^{nd} (Y) w) (h) (y) \in (1^{st} (1^{st} (Y) (z)) (y) Hom (S) 1^{st} (1^{st} (Y) (w)) (y)) \leftrightarrow (z 2^{nd} (Y) w) (h) (y) : 1^{st} (1^{st} (Y) (z)) (y) ⟶ 1^{st} (1^{st} (Y) (w)) (y))$
149	134 148	mpbid	$⊢ (((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \to (z 2^{nd} (Y) w) (h) (y) : 1^{st} (1^{st} (Y) (z)) (y) ⟶ 1^{st} (1^{st} (Y) (w)) (y)$
150	149	feqmptd	$⊢ (((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \to (z 2^{nd} (Y) w) (h) (y) = (g \in 1^{st} (1^{st} (Y) (z)) (y) ⟼ (z 2^{nd} (Y) w) (h) (y) (g))$
151	127 150	eqtr4d	$⊢ (((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \land y \in B) \to (g \in (y Hom (C) z) ⟼ (z 2^{nd} (1^{st} (Y) (w)) y) (g) (h)) = (z 2^{nd} (Y) w) (h) (y)$
152	151	mpteq2dva	$⊢ ((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \to (y \in B ⟼ (g \in (y Hom (C) z) ⟼ (z 2^{nd} (1^{st} (Y) (w)) y) (g) (h))) = (y \in B ⟼ (z 2^{nd} (Y) w) (h) (y))$
153	78	adantr	$⊢ ((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \to V \in W$
154	79	adantr	$⊢ ((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \to ran {Hom}_{𝑓} (C) \subseteq U$
155	80	adantr	$⊢ ((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \to ran {Hom}_{𝑓} (Q) \cup U \subseteq V$
156	63	adantr	$⊢ ((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \to 1^{st} (Y) (w) \in (O Func S)$
157	76	eleq2d	$⊢ (φ \land (z \in B \land w \in B)) \to (h \in 1^{st} (1^{st} (Y) (w)) (z) \leftrightarrow h \in (z Hom (C) w))$
158	157	biimpar	$⊢ ((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \to h \in 1^{st} (1^{st} (Y) (w)) (z)$
159	1 2 3 4 5 6 7 8 9 10 11 110 153 154 155 156 112 18 158	yonedalem4a	$⊢ ((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \to (1^{st} (Y) (w) N z) (h) = (y \in B ⟼ (g \in (y Hom (C) z) ⟼ (z 2^{nd} (1^{st} (Y) (w)) y) (g) (h)))$
160	97 131 52	natfn	$⊢ ((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \to (z 2^{nd} (Y) w) (h) Fn B$
161		dffn5	$⊢ (z 2^{nd} (Y) w) (h) Fn B \leftrightarrow (z 2^{nd} (Y) w) (h) = (y \in B ⟼ (z 2^{nd} (Y) w) (h) (y))$
162	160 161	sylib	$⊢ ((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \to (z 2^{nd} (Y) w) (h) = (y \in B ⟼ (z 2^{nd} (Y) w) (h) (y))$
163	152 159 162	3eqtr4d	$⊢ ((φ \land (z \in B \land w \in B)) \land h \in (z Hom (C) w)) \to (1^{st} (Y) (w) N z) (h) = (z 2^{nd} (Y) w) (h)$
164	163	mpteq2dva	$⊢ (φ \land (z \in B \land w \in B)) \to (h \in (z Hom (C) w) ⟼ (1^{st} (Y) (w) N z) (h)) = (h \in (z Hom (C) w) ⟼ (z 2^{nd} (Y) w) (h))$
165		f1of	$⊢ (1^{st} (Y) (w) N z) : z Hom (C) w \underset{1-1 onto}{⟶} 1^{st} (Y) (z) (O Nat S) 1^{st} (Y) (w) \to (1^{st} (Y) (w) N z) : z Hom (C) w ⟶ 1^{st} (Y) (z) (O Nat S) 1^{st} (Y) (w)$
166	109 165	syl	$⊢ (φ \land (z \in B \land w \in B)) \to (1^{st} (Y) (w) N z) : z Hom (C) w ⟶ 1^{st} (Y) (z) (O Nat S) 1^{st} (Y) (w)$
167	166	feqmptd	$⊢ (φ \land (z \in B \land w \in B)) \to 1^{st} (Y) (w) N z = (h \in (z Hom (C) w) ⟼ (1^{st} (Y) (w) N z) (h))$
168	129	feqmptd	$⊢ (φ \land (z \in B \land w \in B)) \to z 2^{nd} (Y) w = (h \in (z Hom (C) w) ⟼ (z 2^{nd} (Y) w) (h))$
169	164 167 168	3eqtr4d	$⊢ (φ \land (z \in B \land w \in B)) \to 1^{st} (Y) (w) N z = z 2^{nd} (Y) w$
170		f1oeq1	$⊢ 1^{st} (Y) (w) N z = z 2^{nd} (Y) w \to ((1^{st} (Y) (w) N z) : z Hom (C) w \underset{1-1 onto}{⟶} 1^{st} (Y) (z) (O Nat S) 1^{st} (Y) (w) \leftrightarrow (z 2^{nd} (Y) w) : z Hom (C) w \underset{1-1 onto}{⟶} 1^{st} (Y) (z) (O Nat S) 1^{st} (Y) (w))$
171	169 170	syl	$⊢ (φ \land (z \in B \land w \in B)) \to ((1^{st} (Y) (w) N z) : z Hom (C) w \underset{1-1 onto}{⟶} 1^{st} (Y) (z) (O Nat S) 1^{st} (Y) (w) \leftrightarrow (z 2^{nd} (Y) w) : z Hom (C) w \underset{1-1 onto}{⟶} 1^{st} (Y) (z) (O Nat S) 1^{st} (Y) (w))$
172	109 171	mpbid	$⊢ (φ \land (z \in B \land w \in B)) \to (z 2^{nd} (Y) w) : z Hom (C) w \underset{1-1 onto}{⟶} 1^{st} (Y) (z) (O Nat S) 1^{st} (Y) (w)$
173	172	ralrimivva	$⊢ φ \to \forall z \in B \forall w \in B (z 2^{nd} (Y) w) : z Hom (C) w \underset{1-1 onto}{⟶} 1^{st} (Y) (z) (O Nat S) 1^{st} (Y) (w)$
174	2 75 98	isffth2	$⊢ 1^{st} (Y) ((C Full Q) \cap (C Faith Q)) 2^{nd} (Y) \leftrightarrow (1^{st} (Y) (C Func Q) 2^{nd} (Y) \land \forall z \in B \forall w \in B (z 2^{nd} (Y) w) : z Hom (C) w \underset{1-1 onto}{⟶} 1^{st} (Y) (z) (O Nat S) 1^{st} (Y) (w))$
175	26 173 174	sylanbrc	$⊢ φ \to 1^{st} (Y) ((C Full Q) \cap (C Faith Q)) 2^{nd} (Y)$
176		df-br	$⊢ 1^{st} (Y) ((C Full Q) \cap (C Faith Q)) 2^{nd} (Y) \leftrightarrow ⟨1^{st} (Y), 2^{nd} (Y)⟩ \in ((C Full Q) \cap (C Faith Q))$
177	175 176	sylib	$⊢ φ \to ⟨1^{st} (Y), 2^{nd} (Y)⟩ \in ((C Full Q) \cap (C Faith Q))$
178	24 177	eqeltrd	$⊢ φ \to Y \in ((C Full Q) \cap (C Faith Q))$

Metamath Proof Explorer

Theorem yonffthlem

Proof