yoniso

Description: If the codomain is recoverable from a hom-set, then the Yoneda embedding is injective on objects, and hence is an isomorphism from C into a full subcategory of a presheaf category. (Contributed by Mario Carneiro, 30-Jan-2017)

	Ref	Expression
Hypotheses	yoniso.y	$⊢ Y = Yon (C)$
	yoniso.o	$⊢ O = oppCat (C)$
	yoniso.s	$⊢ S = SetCat (U)$
	yoniso.d	$⊢ D = CatCat (V)$
	yoniso.b	$⊢ B = {Base}_{D}$
	yoniso.i	$⊢ I = Iso (D)$
	yoniso.q	$⊢ Q = O FuncCat S$
	yoniso.e	$⊢ E = Q ↾_{𝑠} ran 1^{st} (Y)$
	yoniso.v	$⊢ φ \to V \in X$
	yoniso.c	$⊢ φ \to C \in B$
	yoniso.u	$⊢ φ \to U \in W$
	yoniso.h	$⊢ φ \to ran {Hom}_{𝑓} (C) \subseteq U$
	yoniso.eb	$⊢ φ \to E \in B$
	yoniso.1	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to F (x Hom (C) y) = y$
Assertion	yoniso	$⊢ φ \to Y \in (C I E)$

Proof

Step	Hyp	Ref	Expression
1		yoniso.y	$⊢ Y = Yon (C)$
2		yoniso.o	$⊢ O = oppCat (C)$
3		yoniso.s	$⊢ S = SetCat (U)$
4		yoniso.d	$⊢ D = CatCat (V)$
5		yoniso.b	$⊢ B = {Base}_{D}$
6		yoniso.i	$⊢ I = Iso (D)$
7		yoniso.q	$⊢ Q = O FuncCat S$
8		yoniso.e	$⊢ E = Q ↾_{𝑠} ran 1^{st} (Y)$
9		yoniso.v	$⊢ φ \to V \in X$
10		yoniso.c	$⊢ φ \to C \in B$
11		yoniso.u	$⊢ φ \to U \in W$
12		yoniso.h	$⊢ φ \to ran {Hom}_{𝑓} (C) \subseteq U$
13		yoniso.eb	$⊢ φ \to E \in B$
14		yoniso.1	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to F (x Hom (C) y) = y$
15		relfunc	$⊢ Rel (C Func Q)$
16	4 5 9	catcbas	$⊢ φ \to B = V \cap Cat$
17		inss2	$⊢ V \cap Cat \subseteq Cat$
18	16 17	eqsstrdi	$⊢ φ \to B \subseteq Cat$
19	18 10	sseldd	$⊢ φ \to C \in Cat$
20	1 19 2 3 7 11 12	yoncl	$⊢ φ \to Y \in (C Func Q)$
21		1st2nd	$⊢ (Rel (C Func Q) \land Y \in (C Func Q)) \to Y = ⟨1^{st} (Y), 2^{nd} (Y)⟩$
22	15 20 21	sylancr	$⊢ φ \to Y = ⟨1^{st} (Y), 2^{nd} (Y)⟩$
23	1 2 3 7 19 11 12	yonffth	$⊢ φ \to Y \in ((C Full Q) \cap (C Faith Q))$
24	22 23	eqeltrrd	$⊢ φ \to ⟨1^{st} (Y), 2^{nd} (Y)⟩ \in ((C Full Q) \cap (C Faith Q))$
25		eqid	$⊢ {Base}_{C} = {Base}_{C}$
26	2	oppccat	$⊢ C \in Cat \to O \in Cat$
27	19 26	syl	$⊢ φ \to O \in Cat$
28	3	setccat	$⊢ U \in W \to S \in Cat$
29	11 28	syl	$⊢ φ \to S \in Cat$
30	7 27 29	fuccat	$⊢ φ \to Q \in Cat$
31		fvex	$⊢ 1^{st} (Y) \in V$
32	31	rnex	$⊢ ran 1^{st} (Y) \in V$
33	32	a1i	$⊢ φ \to ran 1^{st} (Y) \in V$
34	7	fucbas	$⊢ O Func S = {Base}_{Q}$
35		1st2ndbr	$⊢ (Rel (C Func Q) \land Y \in (C Func Q)) \to 1^{st} (Y) (C Func Q) 2^{nd} (Y)$
36	15 20 35	sylancr	$⊢ φ \to 1^{st} (Y) (C Func Q) 2^{nd} (Y)$
37	25 34 36	funcf1	$⊢ φ \to 1^{st} (Y) : {Base}_{C} ⟶ O Func S$
38	37	ffnd	$⊢ φ \to 1^{st} (Y) Fn {Base}_{C}$
39		dffn3	$⊢ 1^{st} (Y) Fn {Base}_{C} \leftrightarrow 1^{st} (Y) : {Base}_{C} ⟶ ran 1^{st} (Y)$
40	38 39	sylib	$⊢ φ \to 1^{st} (Y) : {Base}_{C} ⟶ ran 1^{st} (Y)$
41	25 8 30 33 40	ffthres2c	$⊢ φ \to (1^{st} (Y) ((C Full Q) \cap (C Faith Q)) 2^{nd} (Y) \leftrightarrow 1^{st} (Y) ((C Full E) \cap (C Faith E)) 2^{nd} (Y))$
42		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))$
43		df-br	$⊢ 1^{st} (Y) ((C Full E) \cap (C Faith E)) 2^{nd} (Y) \leftrightarrow ⟨1^{st} (Y), 2^{nd} (Y)⟩ \in ((C Full E) \cap (C Faith E))$
44	41 42 43	3bitr3g	$⊢ φ \to (⟨1^{st} (Y), 2^{nd} (Y)⟩ \in ((C Full Q) \cap (C Faith Q)) \leftrightarrow ⟨1^{st} (Y), 2^{nd} (Y)⟩ \in ((C Full E) \cap (C Faith E)))$
45	24 44	mpbid	$⊢ φ \to ⟨1^{st} (Y), 2^{nd} (Y)⟩ \in ((C Full E) \cap (C Faith E))$
46	22 45	eqeltrd	$⊢ φ \to Y \in ((C Full E) \cap (C Faith E))$
47		fveq2	$⊢ 1^{st} (Y) (x) = 1^{st} (Y) (y) \to 1^{st} (1^{st} (Y) (x)) = 1^{st} (1^{st} (Y) (y))$
48	47	fveq1d	$⊢ 1^{st} (Y) (x) = 1^{st} (Y) (y) \to 1^{st} (1^{st} (Y) (x)) (x) = 1^{st} (1^{st} (Y) (y)) (x)$
49	48	fveq2d	$⊢ 1^{st} (Y) (x) = 1^{st} (Y) (y) \to F (1^{st} (1^{st} (Y) (x)) (x)) = F (1^{st} (1^{st} (Y) (y)) (x))$
50		simpl	$⊢ (x \in {Base}_{C} \land y \in {Base}_{C}) \to x \in {Base}_{C}$
51	50 50	jca	$⊢ (x \in {Base}_{C} \land y \in {Base}_{C}) \to (x \in {Base}_{C} \land x \in {Base}_{C})$
52		eleq1w	$⊢ y = x \to (y \in {Base}_{C} \leftrightarrow x \in {Base}_{C})$
53	52	anbi2d	$⊢ y = x \to ((x \in {Base}_{C} \land y \in {Base}_{C}) \leftrightarrow (x \in {Base}_{C} \land x \in {Base}_{C}))$
54	53	anbi2d	$⊢ y = x \to ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \leftrightarrow (φ \land (x \in {Base}_{C} \land x \in {Base}_{C})))$
55		2fveq3	$⊢ y = x \to 1^{st} (1^{st} (Y) (y)) = 1^{st} (1^{st} (Y) (x))$
56	55	fveq1d	$⊢ y = x \to 1^{st} (1^{st} (Y) (y)) (x) = 1^{st} (1^{st} (Y) (x)) (x)$
57	56	fveq2d	$⊢ y = x \to F (1^{st} (1^{st} (Y) (y)) (x)) = F (1^{st} (1^{st} (Y) (x)) (x))$
58		id	$⊢ y = x \to y = x$
59	57 58	eqeq12d	$⊢ y = x \to (F (1^{st} (1^{st} (Y) (y)) (x)) = y \leftrightarrow F (1^{st} (1^{st} (Y) (x)) (x)) = x)$
60	54 59	imbi12d	$⊢ y = x \to (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to F (1^{st} (1^{st} (Y) (y)) (x)) = y) \leftrightarrow ((φ \land (x \in {Base}_{C} \land x \in {Base}_{C})) \to F (1^{st} (1^{st} (Y) (x)) (x)) = x))$
61	19	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to C \in Cat$
62		simprr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to y \in {Base}_{C}$
63		eqid	$⊢ Hom (C) = Hom (C)$
64		simprl	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x \in {Base}_{C}$
65	1 25 61 62 63 64	yon11	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (1^{st} (Y) (y)) (x) = x Hom (C) y$
66	65	fveq2d	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to F (1^{st} (1^{st} (Y) (y)) (x)) = F (x Hom (C) y)$
67	66 14	eqtrd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to F (1^{st} (1^{st} (Y) (y)) (x)) = y$
68	60 67	chvarvv	$⊢ (φ \land (x \in {Base}_{C} \land x \in {Base}_{C})) \to F (1^{st} (1^{st} (Y) (x)) (x)) = x$
69	51 68	sylan2	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to F (1^{st} (1^{st} (Y) (x)) (x)) = x$
70	69 67	eqeq12d	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (F (1^{st} (1^{st} (Y) (x)) (x)) = F (1^{st} (1^{st} (Y) (y)) (x)) \leftrightarrow x = y)$
71	49 70	imbitrid	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (1^{st} (Y) (x) = 1^{st} (Y) (y) \to x = y)$
72	71	ralrimivva	$⊢ φ \to \forall x \in {Base}_{C} \forall y \in {Base}_{C} (1^{st} (Y) (x) = 1^{st} (Y) (y) \to x = y)$
73		dff13	$⊢ 1^{st} (Y) : {Base}_{C} \underset{1-1}{⟶} O Func S \leftrightarrow (1^{st} (Y) : {Base}_{C} ⟶ O Func S \land \forall x \in {Base}_{C} \forall y \in {Base}_{C} (1^{st} (Y) (x) = 1^{st} (Y) (y) \to x = y))$
74	37 72 73	sylanbrc	$⊢ φ \to 1^{st} (Y) : {Base}_{C} \underset{1-1}{⟶} O Func S$
75		f1f1orn	$⊢ 1^{st} (Y) : {Base}_{C} \underset{1-1}{⟶} O Func S \to 1^{st} (Y) : {Base}_{C} \underset{1-1 onto}{⟶} ran 1^{st} (Y)$
76	74 75	syl	$⊢ φ \to 1^{st} (Y) : {Base}_{C} \underset{1-1 onto}{⟶} ran 1^{st} (Y)$
77	37	frnd	$⊢ φ \to ran 1^{st} (Y) \subseteq O Func S$
78	8 34	ressbas2	$⊢ ran 1^{st} (Y) \subseteq O Func S \to ran 1^{st} (Y) = {Base}_{E}$
79	77 78	syl	$⊢ φ \to ran 1^{st} (Y) = {Base}_{E}$
80	79	f1oeq3d	$⊢ φ \to (1^{st} (Y) : {Base}_{C} \underset{1-1 onto}{⟶} ran 1^{st} (Y) \leftrightarrow 1^{st} (Y) : {Base}_{C} \underset{1-1 onto}{⟶} {Base}_{E})$
81	76 80	mpbid	$⊢ φ \to 1^{st} (Y) : {Base}_{C} \underset{1-1 onto}{⟶} {Base}_{E}$
82		eqid	$⊢ {Base}_{E} = {Base}_{E}$
83	4 5 25 82 9 10 13 6	catciso	$⊢ φ \to (Y \in (C I E) \leftrightarrow (Y \in ((C Full E) \cap (C Faith E)) \land 1^{st} (Y) : {Base}_{C} \underset{1-1 onto}{⟶} {Base}_{E}))$
84	46 81 83	mpbir2and	$⊢ φ \to Y \in (C I E)$

Metamath Proof Explorer

Theorem yoniso

Proof