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	⊢ 𝑌 = ( Yon ‘ 𝐶 )
	yoniso.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	yoniso.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
	yoniso.d	⊢ 𝐷 = ( CatCat ‘ 𝑉 )
	yoniso.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	yoniso.i	⊢ 𝐼 = ( Iso ‘ 𝐷 )
	yoniso.q	⊢ 𝑄 = ( 𝑂 FuncCat 𝑆 )
	yoniso.e	⊢ 𝐸 = ( 𝑄 ↾_s ran ( 1^st ‘ 𝑌 ) )
	yoniso.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑋 )
	yoniso.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
	yoniso.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑊 )
	yoniso.h	⊢ ( 𝜑 → ran ( Hom_f ‘ 𝐶 ) ⊆ 𝑈 )
	yoniso.eb	⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )
	yoniso.1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) = 𝑦 )
Assertion	yoniso	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐶 𝐼 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		yoniso.y	⊢ 𝑌 = ( Yon ‘ 𝐶 )
2		yoniso.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
3		yoniso.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
4		yoniso.d	⊢ 𝐷 = ( CatCat ‘ 𝑉 )
5		yoniso.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
6		yoniso.i	⊢ 𝐼 = ( Iso ‘ 𝐷 )
7		yoniso.q	⊢ 𝑄 = ( 𝑂 FuncCat 𝑆 )
8		yoniso.e	⊢ 𝐸 = ( 𝑄 ↾_s ran ( 1^st ‘ 𝑌 ) )
9		yoniso.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑋 )
10		yoniso.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
11		yoniso.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑊 )
12		yoniso.h	⊢ ( 𝜑 → ran ( Hom_f ‘ 𝐶 ) ⊆ 𝑈 )
13		yoniso.eb	⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )
14		yoniso.1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) = 𝑦 )
15		relfunc	⊢ Rel ( 𝐶 Func 𝑄 )
16	4 5 9	catcbas	⊢ ( 𝜑 → 𝐵 = ( 𝑉 ∩ Cat ) )
17		inss2	⊢ ( 𝑉 ∩ Cat ) ⊆ Cat
18	16 17	eqsstrdi	⊢ ( 𝜑 → 𝐵 ⊆ Cat )
19	18 10	sseldd	⊢ ( 𝜑 → 𝐶 ∈ Cat )
20	1 19 2 3 7 11 12	yoncl	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐶 Func 𝑄 ) )
21		1st2nd	⊢ ( ( Rel ( 𝐶 Func 𝑄 ) ∧ 𝑌 ∈ ( 𝐶 Func 𝑄 ) ) → 𝑌 = ⟨ ( 1^st ‘ 𝑌 ) , ( 2^nd ‘ 𝑌 ) ⟩ )
22	15 20 21	sylancr	⊢ ( 𝜑 → 𝑌 = ⟨ ( 1^st ‘ 𝑌 ) , ( 2^nd ‘ 𝑌 ) ⟩ )
23	1 2 3 7 19 11 12	yonffth	⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) )
24	22 23	eqeltrrd	⊢ ( 𝜑 → ⟨ ( 1^st ‘ 𝑌 ) , ( 2^nd ‘ 𝑌 ) ⟩ ∈ ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) )
25		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
26	2	oppccat	⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
27	19 26	syl	⊢ ( 𝜑 → 𝑂 ∈ Cat )
28	3	setccat	⊢ ( 𝑈 ∈ 𝑊 → 𝑆 ∈ Cat )
29	11 28	syl	⊢ ( 𝜑 → 𝑆 ∈ Cat )
30	7 27 29	fuccat	⊢ ( 𝜑 → 𝑄 ∈ Cat )
31		fvex	⊢ ( 1^st ‘ 𝑌 ) ∈ V
32	31	rnex	⊢ ran ( 1^st ‘ 𝑌 ) ∈ V
33	32	a1i	⊢ ( 𝜑 → ran ( 1^st ‘ 𝑌 ) ∈ V )
34	7	fucbas	⊢ ( 𝑂 Func 𝑆 ) = ( Base ‘ 𝑄 )
35		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝑄 ) ∧ 𝑌 ∈ ( 𝐶 Func 𝑄 ) ) → ( 1^st ‘ 𝑌 ) ( 𝐶 Func 𝑄 ) ( 2^nd ‘ 𝑌 ) )
36	15 20 35	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝑌 ) ( 𝐶 Func 𝑄 ) ( 2^nd ‘ 𝑌 ) )
37	25 34 36	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝑌 ) : ( Base ‘ 𝐶 ) ⟶ ( 𝑂 Func 𝑆 ) )
38	37	ffnd	⊢ ( 𝜑 → ( 1^st ‘ 𝑌 ) Fn ( Base ‘ 𝐶 ) )
39		dffn3	⊢ ( ( 1^st ‘ 𝑌 ) Fn ( Base ‘ 𝐶 ) ↔ ( 1^st ‘ 𝑌 ) : ( Base ‘ 𝐶 ) ⟶ ran ( 1^st ‘ 𝑌 ) )
40	38 39	sylib	⊢ ( 𝜑 → ( 1^st ‘ 𝑌 ) : ( Base ‘ 𝐶 ) ⟶ ran ( 1^st ‘ 𝑌 ) )
41	25 8 30 33 40	ffthres2c	⊢ ( 𝜑 → ( ( 1^st ‘ 𝑌 ) ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) ( 2^nd ‘ 𝑌 ) ↔ ( 1^st ‘ 𝑌 ) ( ( 𝐶 Full 𝐸 ) ∩ ( 𝐶 Faith 𝐸 ) ) ( 2^nd ‘ 𝑌 ) ) )
42		df-br	⊢ ( ( 1^st ‘ 𝑌 ) ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) ( 2^nd ‘ 𝑌 ) ↔ ⟨ ( 1^st ‘ 𝑌 ) , ( 2^nd ‘ 𝑌 ) ⟩ ∈ ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) )
43		df-br	⊢ ( ( 1^st ‘ 𝑌 ) ( ( 𝐶 Full 𝐸 ) ∩ ( 𝐶 Faith 𝐸 ) ) ( 2^nd ‘ 𝑌 ) ↔ ⟨ ( 1^st ‘ 𝑌 ) , ( 2^nd ‘ 𝑌 ) ⟩ ∈ ( ( 𝐶 Full 𝐸 ) ∩ ( 𝐶 Faith 𝐸 ) ) )
44	41 42 43	3bitr3g	⊢ ( 𝜑 → ( ⟨ ( 1^st ‘ 𝑌 ) , ( 2^nd ‘ 𝑌 ) ⟩ ∈ ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) ↔ ⟨ ( 1^st ‘ 𝑌 ) , ( 2^nd ‘ 𝑌 ) ⟩ ∈ ( ( 𝐶 Full 𝐸 ) ∩ ( 𝐶 Faith 𝐸 ) ) ) )
45	24 44	mpbid	⊢ ( 𝜑 → ⟨ ( 1^st ‘ 𝑌 ) , ( 2^nd ‘ 𝑌 ) ⟩ ∈ ( ( 𝐶 Full 𝐸 ) ∩ ( 𝐶 Faith 𝐸 ) ) )
46	22 45	eqeltrd	⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝐶 Full 𝐸 ) ∩ ( 𝐶 Faith 𝐸 ) ) )
47		fveq2	⊢ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝑌 ) ‘ 𝑦 ) → ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) ) = ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑦 ) ) )
48	47	fveq1d	⊢ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝑌 ) ‘ 𝑦 ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) ) ‘ 𝑥 ) = ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑦 ) ) ‘ 𝑥 ) )
49	48	fveq2d	⊢ ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝑌 ) ‘ 𝑦 ) → ( 𝐹 ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) ) ‘ 𝑥 ) ) = ( 𝐹 ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑦 ) ) ‘ 𝑥 ) ) )
50		simpl	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
51	50 50	jca	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) )
52		eleq1w	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ ( Base ‘ 𝐶 ) ↔ 𝑥 ∈ ( Base ‘ 𝐶 ) ) )
53	52	anbi2d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ) )
54	53	anbi2d	⊢ ( 𝑦 = 𝑥 → ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ↔ ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ) ) )
55		2fveq3	⊢ ( 𝑦 = 𝑥 → ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑦 ) ) = ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) ) )
56	55	fveq1d	⊢ ( 𝑦 = 𝑥 → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑦 ) ) ‘ 𝑥 ) = ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) ) ‘ 𝑥 ) )
57	56	fveq2d	⊢ ( 𝑦 = 𝑥 → ( 𝐹 ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑦 ) ) ‘ 𝑥 ) ) = ( 𝐹 ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) ) ‘ 𝑥 ) ) )
58		id	⊢ ( 𝑦 = 𝑥 → 𝑦 = 𝑥 )
59	57 58	eqeq12d	⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑦 ) ) ‘ 𝑥 ) ) = 𝑦 ↔ ( 𝐹 ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) ) ‘ 𝑥 ) ) = 𝑥 ) )
60	54 59	imbi12d	⊢ ( 𝑦 = 𝑥 → ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝐹 ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑦 ) ) ‘ 𝑥 ) ) = 𝑦 ) ↔ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝐹 ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) ) ‘ 𝑥 ) ) = 𝑥 ) ) )
61	19	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐶 ∈ Cat )
62		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
63		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
64		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
65	1 25 61 62 63 64	yon11	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑦 ) ) ‘ 𝑥 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
66	65	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝐹 ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑦 ) ) ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) )
67	66 14	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝐹 ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑦 ) ) ‘ 𝑥 ) ) = 𝑦 )
68	60 67	chvarvv	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝐹 ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) ) ‘ 𝑥 ) ) = 𝑥 )
69	51 68	sylan2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝐹 ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) ) ‘ 𝑥 ) ) = 𝑥 )
70	69 67	eqeq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 𝐹 ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) ) ‘ 𝑥 ) ) = ( 𝐹 ‘ ( ( 1^st ‘ ( ( 1^st ‘ 𝑌 ) ‘ 𝑦 ) ) ‘ 𝑥 ) ) ↔ 𝑥 = 𝑦 ) )
71	49 70	imbitrid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝑌 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
72	71	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝑌 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
73		dff13	⊢ ( ( 1^st ‘ 𝑌 ) : ( Base ‘ 𝐶 ) –1-1→ ( 𝑂 Func 𝑆 ) ↔ ( ( 1^st ‘ 𝑌 ) : ( Base ‘ 𝐶 ) ⟶ ( 𝑂 Func 𝑆 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ( ( 1^st ‘ 𝑌 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝑌 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
74	37 72 73	sylanbrc	⊢ ( 𝜑 → ( 1^st ‘ 𝑌 ) : ( Base ‘ 𝐶 ) –1-1→ ( 𝑂 Func 𝑆 ) )
75		f1f1orn	⊢ ( ( 1^st ‘ 𝑌 ) : ( Base ‘ 𝐶 ) –1-1→ ( 𝑂 Func 𝑆 ) → ( 1^st ‘ 𝑌 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ran ( 1^st ‘ 𝑌 ) )
76	74 75	syl	⊢ ( 𝜑 → ( 1^st ‘ 𝑌 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ran ( 1^st ‘ 𝑌 ) )
77	37	frnd	⊢ ( 𝜑 → ran ( 1^st ‘ 𝑌 ) ⊆ ( 𝑂 Func 𝑆 ) )
78	8 34	ressbas2	⊢ ( ran ( 1^st ‘ 𝑌 ) ⊆ ( 𝑂 Func 𝑆 ) → ran ( 1^st ‘ 𝑌 ) = ( Base ‘ 𝐸 ) )
79	77 78	syl	⊢ ( 𝜑 → ran ( 1^st ‘ 𝑌 ) = ( Base ‘ 𝐸 ) )
80	79	f1oeq3d	⊢ ( 𝜑 → ( ( 1^st ‘ 𝑌 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ran ( 1^st ‘ 𝑌 ) ↔ ( 1^st ‘ 𝑌 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( Base ‘ 𝐸 ) ) )
81	76 80	mpbid	⊢ ( 𝜑 → ( 1^st ‘ 𝑌 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( Base ‘ 𝐸 ) )
82		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
83	4 5 25 82 9 10 13 6	catciso	⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝐶 𝐼 𝐸 ) ↔ ( 𝑌 ∈ ( ( 𝐶 Full 𝐸 ) ∩ ( 𝐶 Faith 𝐸 ) ) ∧ ( 1^st ‘ 𝑌 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( Base ‘ 𝐸 ) ) ) )
84	46 81 83	mpbir2and	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐶 𝐼 𝐸 ) )

Metamath Proof Explorer

Theorem yoniso

Proof