This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem discsnterm

Description: A discrete category (a category whose only morphisms are the identity morphisms) with a singlegon base is terminal. Corollary of example 3.3(4)(c) of Adamek p. 24 and example 3.26(1) of Adamek p. 33. (Contributed by Zhi Wang, 20-Oct-2025)

Ref Expression
Hypotheses discthin.k ⊢ K = Base ndx B ≤ ndx I ↾ B
discthin.c ⊢ C = ProsetToCat ⁡ K
Assertion discsnterm Could not format assertion : No typesetting found for |- ( E. x B = { x } -> C e. TermCat ) with typecode |-

Proof

Step Hyp Ref Expression
1 discthin.k ⊢ K = Base ndx B ≤ ndx I ↾ B
2 discthin.c ⊢ C = ProsetToCat ⁡ K
3 discsntermlem ⊢ ∃ x B = x → B ∈ b | ∃ x b = x
4 1 2 discthin ⊢ B ∈ b | ∃ x b = x → C ∈ ThinCat
5 3 4 syl ⊢ ∃ x B = x → C ∈ ThinCat
6 elex ⊢ B ∈ b | ∃ x b = x → B ∈ V
7 1 2 discbas ⊢ B ∈ V → B = Base C
8 7 eqeq1d ⊢ B ∈ V → B = x ↔ Base C = x
9 8 exbidv ⊢ B ∈ V → ∃ x B = x ↔ ∃ x Base C = x
10 3 6 9 3syl ⊢ ∃ x B = x → ∃ x B = x ↔ ∃ x Base C = x
11 10 ibi ⊢ ∃ x B = x → ∃ x Base C = x
12 eqid ⊢ Base C = Base C
13 12 istermc Could not format ( C e. TermCat <-> ( C e. ThinCat /\ E. x ( Base ` C ) = { x } ) ) : No typesetting found for |- ( C e. TermCat <-> ( C e. ThinCat /\ E. x ( Base ` C ) = { x } ) ) with typecode |-
14 5 11 13 sylanbrc Could not format ( E. x B = { x } -> C e. TermCat ) : No typesetting found for |- ( E. x B = { x } -> C e. TermCat ) with typecode |-