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

Metamath Proof Explorer

Theorem istermc

Description: The predicate "is a terminal category". A terminal category is a thin category with a singleton base set. (Contributed by Zhi Wang, 16-Oct-2025)

Ref Expression
Hypothesis istermc.b ⊢ B = Base C
Assertion istermc Could not format assertion : No typesetting found for |- ( C e. TermCat <-> ( C e. ThinCat /\ E. x B = { x } ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 istermc.b ⊢ B = Base C
2 fveqeq2 ⊢ c = C → Base c = x ↔ Base C = x
3 2 exbidv ⊢ c = C → ∃ x Base c = x ↔ ∃ x Base C = x
4 1 eqeq1i ⊢ B = x ↔ Base C = x
5 4 exbii ⊢ ∃ x B = x ↔ ∃ x Base C = x
6 3 5 bitr4di ⊢ c = C → ∃ x Base c = x ↔ ∃ x B = x
7 df-termc Could not format TermCat = { c e. ThinCat | E. x ( Base ` c ) = { x } } : No typesetting found for |- TermCat = { c e. ThinCat | E. x ( Base ` c ) = { x } } with typecode |-
8 6 7 elrab2 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 |-