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

Metamath Proof Explorer

Theorem yoniso

Proof