Metamath Proof Explorer


Theorem 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 ( 1st𝑌 ) )
yoniso.v ( 𝜑𝑉𝑋 )
yoniso.c ( 𝜑𝐶𝐵 )
yoniso.u ( 𝜑𝑈𝑊 )
yoniso.h ( 𝜑 → ran ( Homf𝐶 ) ⊆ 𝑈 )
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 ( 1st𝑌 ) )
9 yoniso.v ( 𝜑𝑉𝑋 )
10 yoniso.c ( 𝜑𝐶𝐵 )
11 yoniso.u ( 𝜑𝑈𝑊 )
12 yoniso.h ( 𝜑 → ran ( Homf𝐶 ) ⊆ 𝑈 )
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 𝑄 ) ) → 𝑌 = ⟨ ( 1st𝑌 ) , ( 2nd𝑌 ) ⟩ )
22 15 20 21 sylancr ( 𝜑𝑌 = ⟨ ( 1st𝑌 ) , ( 2nd𝑌 ) ⟩ )
23 1 2 3 7 19 11 12 yonffth ( 𝜑𝑌 ∈ ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) )
24 22 23 eqeltrrd ( 𝜑 → ⟨ ( 1st𝑌 ) , ( 2nd𝑌 ) ⟩ ∈ ( ( 𝐶 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 ( 1st𝑌 ) ∈ V
32 31 rnex ran ( 1st𝑌 ) ∈ V
33 32 a1i ( 𝜑 → ran ( 1st𝑌 ) ∈ V )
34 7 fucbas ( 𝑂 Func 𝑆 ) = ( Base ‘ 𝑄 )
35 1st2ndbr ( ( Rel ( 𝐶 Func 𝑄 ) ∧ 𝑌 ∈ ( 𝐶 Func 𝑄 ) ) → ( 1st𝑌 ) ( 𝐶 Func 𝑄 ) ( 2nd𝑌 ) )
36 15 20 35 sylancr ( 𝜑 → ( 1st𝑌 ) ( 𝐶 Func 𝑄 ) ( 2nd𝑌 ) )
37 25 34 36 funcf1 ( 𝜑 → ( 1st𝑌 ) : ( Base ‘ 𝐶 ) ⟶ ( 𝑂 Func 𝑆 ) )
38 37 ffnd ( 𝜑 → ( 1st𝑌 ) Fn ( Base ‘ 𝐶 ) )
39 dffn3 ( ( 1st𝑌 ) Fn ( Base ‘ 𝐶 ) ↔ ( 1st𝑌 ) : ( Base ‘ 𝐶 ) ⟶ ran ( 1st𝑌 ) )
40 38 39 sylib ( 𝜑 → ( 1st𝑌 ) : ( Base ‘ 𝐶 ) ⟶ ran ( 1st𝑌 ) )
41 25 8 30 33 40 ffthres2c ( 𝜑 → ( ( 1st𝑌 ) ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) ( 2nd𝑌 ) ↔ ( 1st𝑌 ) ( ( 𝐶 Full 𝐸 ) ∩ ( 𝐶 Faith 𝐸 ) ) ( 2nd𝑌 ) ) )
42 df-br ( ( 1st𝑌 ) ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) ( 2nd𝑌 ) ↔ ⟨ ( 1st𝑌 ) , ( 2nd𝑌 ) ⟩ ∈ ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) )
43 df-br ( ( 1st𝑌 ) ( ( 𝐶 Full 𝐸 ) ∩ ( 𝐶 Faith 𝐸 ) ) ( 2nd𝑌 ) ↔ ⟨ ( 1st𝑌 ) , ( 2nd𝑌 ) ⟩ ∈ ( ( 𝐶 Full 𝐸 ) ∩ ( 𝐶 Faith 𝐸 ) ) )
44 41 42 43 3bitr3g ( 𝜑 → ( ⟨ ( 1st𝑌 ) , ( 2nd𝑌 ) ⟩ ∈ ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) ↔ ⟨ ( 1st𝑌 ) , ( 2nd𝑌 ) ⟩ ∈ ( ( 𝐶 Full 𝐸 ) ∩ ( 𝐶 Faith 𝐸 ) ) ) )
45 24 44 mpbid ( 𝜑 → ⟨ ( 1st𝑌 ) , ( 2nd𝑌 ) ⟩ ∈ ( ( 𝐶 Full 𝐸 ) ∩ ( 𝐶 Faith 𝐸 ) ) )
46 22 45 eqeltrd ( 𝜑𝑌 ∈ ( ( 𝐶 Full 𝐸 ) ∩ ( 𝐶 Faith 𝐸 ) ) )
47 fveq2 ( ( ( 1st𝑌 ) ‘ 𝑥 ) = ( ( 1st𝑌 ) ‘ 𝑦 ) → ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑥 ) ) = ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑦 ) ) )
48 47 fveq1d ( ( ( 1st𝑌 ) ‘ 𝑥 ) = ( ( 1st𝑌 ) ‘ 𝑦 ) → ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑥 ) ) ‘ 𝑥 ) = ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑦 ) ) ‘ 𝑥 ) )
49 48 fveq2d ( ( ( 1st𝑌 ) ‘ 𝑥 ) = ( ( 1st𝑌 ) ‘ 𝑦 ) → ( 𝐹 ‘ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑥 ) ) ‘ 𝑥 ) ) = ( 𝐹 ‘ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑦 ) ) ‘ 𝑥 ) ) )
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 ( 𝑦 = 𝑥 → ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑦 ) ) = ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑥 ) ) )
56 55 fveq1d ( 𝑦 = 𝑥 → ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑦 ) ) ‘ 𝑥 ) = ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑥 ) ) ‘ 𝑥 ) )
57 56 fveq2d ( 𝑦 = 𝑥 → ( 𝐹 ‘ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑦 ) ) ‘ 𝑥 ) ) = ( 𝐹 ‘ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑥 ) ) ‘ 𝑥 ) ) )
58 id ( 𝑦 = 𝑥𝑦 = 𝑥 )
59 57 58 eqeq12d ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑦 ) ) ‘ 𝑥 ) ) = 𝑦 ↔ ( 𝐹 ‘ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑥 ) ) ‘ 𝑥 ) ) = 𝑥 ) )
60 54 59 imbi12d ( 𝑦 = 𝑥 → ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝐹 ‘ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑦 ) ) ‘ 𝑥 ) ) = 𝑦 ) ↔ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝐹 ‘ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑥 ) ) ‘ 𝑥 ) ) = 𝑥 ) ) )
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 ‘ 𝐶 ) ) ) → ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑦 ) ) ‘ 𝑥 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
66 65 fveq2d ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝐹 ‘ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑦 ) ) ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) )
67 66 14 eqtrd ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝐹 ‘ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑦 ) ) ‘ 𝑥 ) ) = 𝑦 )
68 60 67 chvarvv ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝐹 ‘ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑥 ) ) ‘ 𝑥 ) ) = 𝑥 )
69 51 68 sylan2 ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝐹 ‘ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑥 ) ) ‘ 𝑥 ) ) = 𝑥 )
70 69 67 eqeq12d ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 𝐹 ‘ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑥 ) ) ‘ 𝑥 ) ) = ( 𝐹 ‘ ( ( 1st ‘ ( ( 1st𝑌 ) ‘ 𝑦 ) ) ‘ 𝑥 ) ) ↔ 𝑥 = 𝑦 ) )
71 49 70 syl5ib ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( 1st𝑌 ) ‘ 𝑥 ) = ( ( 1st𝑌 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
72 71 ralrimivva ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ( ( 1st𝑌 ) ‘ 𝑥 ) = ( ( 1st𝑌 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
73 dff13 ( ( 1st𝑌 ) : ( Base ‘ 𝐶 ) –1-1→ ( 𝑂 Func 𝑆 ) ↔ ( ( 1st𝑌 ) : ( Base ‘ 𝐶 ) ⟶ ( 𝑂 Func 𝑆 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ( ( 1st𝑌 ) ‘ 𝑥 ) = ( ( 1st𝑌 ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
74 37 72 73 sylanbrc ( 𝜑 → ( 1st𝑌 ) : ( Base ‘ 𝐶 ) –1-1→ ( 𝑂 Func 𝑆 ) )
75 f1f1orn ( ( 1st𝑌 ) : ( Base ‘ 𝐶 ) –1-1→ ( 𝑂 Func 𝑆 ) → ( 1st𝑌 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ran ( 1st𝑌 ) )
76 74 75 syl ( 𝜑 → ( 1st𝑌 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ran ( 1st𝑌 ) )
77 37 frnd ( 𝜑 → ran ( 1st𝑌 ) ⊆ ( 𝑂 Func 𝑆 ) )
78 8 34 ressbas2 ( ran ( 1st𝑌 ) ⊆ ( 𝑂 Func 𝑆 ) → ran ( 1st𝑌 ) = ( Base ‘ 𝐸 ) )
79 77 78 syl ( 𝜑 → ran ( 1st𝑌 ) = ( Base ‘ 𝐸 ) )
80 79 f1oeq3d ( 𝜑 → ( ( 1st𝑌 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ran ( 1st𝑌 ) ↔ ( 1st𝑌 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( Base ‘ 𝐸 ) ) )
81 76 80 mpbid ( 𝜑 → ( 1st𝑌 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( Base ‘ 𝐸 ) )
82 eqid ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
83 4 5 25 82 9 10 13 6 catciso ( 𝜑 → ( 𝑌 ∈ ( 𝐶 𝐼 𝐸 ) ↔ ( 𝑌 ∈ ( ( 𝐶 Full 𝐸 ) ∩ ( 𝐶 Faith 𝐸 ) ) ∧ ( 1st𝑌 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( Base ‘ 𝐸 ) ) ) )
84 46 81 83 mpbir2and ( 𝜑𝑌 ∈ ( 𝐶 𝐼 𝐸 ) )