Metamath Proof Explorer

Theorem idfudiag1

Description: If the identity functor of a category is the same as a constant functor to the category, then the category is terminal. (Contributed by Zhi Wang, 19-Oct-2025)

Ref Expression
Hypotheses idfudiag1.i ⊢ I = id func ⁡ C
idfudiag1.l ⊢ L = C Δ func C
idfudiag1.c ⊢ φ → C ∈ Cat
idfudiag1.b ⊢ B = Base C
idfudiag1.x ⊢ φ → X ∈ B
idfudiag1.k ⊢ K = 1 st ⁡ L ⁡ X
idfudiag1.e ⊢ φ → I = K
Assertion idfudiag1 Could not format assertion : No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-

Proof

Step Hyp Ref Expression
1 idfudiag1.i ⊢ I = id func ⁡ C
2 idfudiag1.l ⊢ L = C Δ func C
3 idfudiag1.c ⊢ φ → C ∈ Cat
4 idfudiag1.b ⊢ B = Base C
5 idfudiag1.x ⊢ φ → X ∈ B
6 idfudiag1.k ⊢ K = 1 st ⁡ L ⁡ X
7 idfudiag1.e ⊢ φ → I = K
8 4 a1i ⊢ φ → B = Base C
9 eqidd ⊢ φ → Hom ⁡ C = Hom ⁡ C
10 fveq2 ⊢ p = y z → Hom ⁡ C ⁡ p = Hom ⁡ C ⁡ y z
11 df-ov ⊢ y Hom ⁡ C z = Hom ⁡ C ⁡ y z
12 10 11 eqtr4di ⊢ p = y z → Hom ⁡ C ⁡ p = y Hom ⁡ C z
13 12 reseq2d ⊢ p = y z → I ↾ Hom ⁡ C ⁡ p = I ↾ y Hom ⁡ C z
14 13 mpompt ⊢ p ∈ B × B ⟼ I ↾ Hom ⁡ C ⁡ p = y ∈ B , z ∈ B ⟼ I ↾ y Hom ⁡ C z
15 14 a1i ⊢ φ → p ∈ B × B ⟼ I ↾ Hom ⁡ C ⁡ p = y ∈ B , z ∈ B ⟼ I ↾ y Hom ⁡ C z
16 ovex ⊢ y Hom ⁡ C z ∈ V
17 resiexg ⊢ y Hom ⁡ C z ∈ V → I ↾ y Hom ⁡ C z ∈ V
18 16 17 mp1i ⊢ φ ∧ y ∈ B ∧ z ∈ B → I ↾ y Hom ⁡ C z ∈ V
19 15 18 ovmpt4d ⊢ φ ∧ y ∈ B ∧ z ∈ B → y p ∈ B × B ⟼ I ↾ Hom ⁡ C ⁡ p z = I ↾ y Hom ⁡ C z
20 eqid ⊢ Hom ⁡ C = Hom ⁡ C
21 1 4 3 20 idfuval ⊢ φ → I = I ↾ B p ∈ B × B ⟼ I ↾ Hom ⁡ C ⁡ p
22 eqid ⊢ Id ⁡ C = Id ⁡ C
23 2 3 3 4 5 6 4 20 22 diag1a ⊢ φ → K = B × X y ∈ B , z ∈ B ⟼ y Hom ⁡ C z × Id ⁡ C ⁡ X
24 7 21 23 3eqtr3d ⊢ φ → I ↾ B p ∈ B × B ⟼ I ↾ Hom ⁡ C ⁡ p = B × X y ∈ B , z ∈ B ⟼ y Hom ⁡ C z × Id ⁡ C ⁡ X
25 4 fvexi ⊢ B ∈ V
26 resiexg ⊢ B ∈ V → I ↾ B ∈ V
27 25 26 ax-mp ⊢ I ↾ B ∈ V
28 25 25 xpex ⊢ B × B ∈ V
29 28 mptex ⊢ p ∈ B × B ⟼ I ↾ Hom ⁡ C ⁡ p ∈ V
30 27 29 opth ⊢ I ↾ B p ∈ B × B ⟼ I ↾ Hom ⁡ C ⁡ p = B × X y ∈ B , z ∈ B ⟼ y Hom ⁡ C z × Id ⁡ C ⁡ X ↔ I ↾ B = B × X ∧ p ∈ B × B ⟼ I ↾ Hom ⁡ C ⁡ p = y ∈ B , z ∈ B ⟼ y Hom ⁡ C z × Id ⁡ C ⁡ X
31 30 simprbi ⊢ I ↾ B p ∈ B × B ⟼ I ↾ Hom ⁡ C ⁡ p = B × X y ∈ B , z ∈ B ⟼ y Hom ⁡ C z × Id ⁡ C ⁡ X → p ∈ B × B ⟼ I ↾ Hom ⁡ C ⁡ p = y ∈ B , z ∈ B ⟼ y Hom ⁡ C z × Id ⁡ C ⁡ X
32 24 31 syl ⊢ φ → p ∈ B × B ⟼ I ↾ Hom ⁡ C ⁡ p = y ∈ B , z ∈ B ⟼ y Hom ⁡ C z × Id ⁡ C ⁡ X
33 snex ⊢ Id ⁡ C ⁡ X ∈ V
34 16 33 xpex ⊢ y Hom ⁡ C z × Id ⁡ C ⁡ X ∈ V
35 34 a1i ⊢ φ ∧ y ∈ B ∧ z ∈ B → y Hom ⁡ C z × Id ⁡ C ⁡ X ∈ V
36 32 35 ovmpt4d ⊢ φ ∧ y ∈ B ∧ z ∈ B → y p ∈ B × B ⟼ I ↾ Hom ⁡ C ⁡ p z = y Hom ⁡ C z × Id ⁡ C ⁡ X
37 19 36 eqtr3d ⊢ φ ∧ y ∈ B ∧ z ∈ B → I ↾ y Hom ⁡ C z = y Hom ⁡ C z × Id ⁡ C ⁡ X
38 3 adantr ⊢ φ ∧ y ∈ B ∧ z ∈ B → C ∈ Cat
39 simprl ⊢ φ ∧ y ∈ B ∧ z ∈ B → y ∈ B
40 4 20 22 38 39 catidcl ⊢ φ ∧ y ∈ B ∧ z ∈ B → Id ⁡ C ⁡ y ∈ y Hom ⁡ C y
41 1 2 3 4 5 6 7 idfudiag1bas ⊢ φ → B = X
42 41 adantr ⊢ φ ∧ y ∈ B ∧ z ∈ B → B = X
43 39 42 eleqtrd ⊢ φ ∧ y ∈ B ∧ z ∈ B → y ∈ X
44 elsni ⊢ y ∈ X → y = X
45 43 44 syl ⊢ φ ∧ y ∈ B ∧ z ∈ B → y = X
46 simprr ⊢ φ ∧ y ∈ B ∧ z ∈ B → z ∈ B
47 46 42 eleqtrd ⊢ φ ∧ y ∈ B ∧ z ∈ B → z ∈ X
48 elsni ⊢ z ∈ X → z = X
49 47 48 syl ⊢ φ ∧ y ∈ B ∧ z ∈ B → z = X
50 45 49 eqtr4d ⊢ φ ∧ y ∈ B ∧ z ∈ B → y = z
51 50 oveq2d ⊢ φ ∧ y ∈ B ∧ z ∈ B → y Hom ⁡ C y = y Hom ⁡ C z
52 40 51 eleqtrd ⊢ φ ∧ y ∈ B ∧ z ∈ B → Id ⁡ C ⁡ y ∈ y Hom ⁡ C z
53 52 ne0d ⊢ φ ∧ y ∈ B ∧ z ∈ B → y Hom ⁡ C z ≠ ∅
54 37 53 idfudiag1lem ⊢ φ ∧ y ∈ B ∧ z ∈ B → y Hom ⁡ C z = Id ⁡ C ⁡ X
55 mosn ⊢ y Hom ⁡ C z = Id ⁡ C ⁡ X → ∃* f f ∈ y Hom ⁡ C z
56 54 55 syl ⊢ φ ∧ y ∈ B ∧ z ∈ B → ∃* f f ∈ y Hom ⁡ C z
57 8 9 56 3 isthincd ⊢ φ → C ∈ ThinCat
58 sneq ⊢ x = X → x = X
59 58 eqeq2d ⊢ x = X → B = x ↔ B = X
60 5 41 59 spcedv ⊢ φ → ∃ x B = x
61 4 istermc Could not format ( C e. TermCat <-> ( C e. ThinCat /\ E. x B = { x } ) ) : No typesetting found for |- ( C e. TermCat <-> ( C e. ThinCat /\ E. x B = { x } ) ) with typecode |-
62 57 60 61 sylanbrc Could not format ( ph -> C e. TermCat ) : No typesetting found for |- ( ph -> C e. TermCat ) with typecode |-