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 ⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion istermc ( 𝐶 ∈ TermCat ↔ ( 𝐶 ∈ ThinCat ∧ ∃ 𝑥 𝐵 = { 𝑥 } ) )

Proof

Step Hyp Ref Expression
1 istermc.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 fveqeq2 ⊢ ( 𝑐 = 𝐶 → ( ( Base ‘ 𝑐 ) = { 𝑥 } ↔ ( Base ‘ 𝐶 ) = { 𝑥 } ) )
3 2 exbidv ⊢ ( 𝑐 = 𝐶 → ( ∃ 𝑥 ( Base ‘ 𝑐 ) = { 𝑥 } ↔ ∃ 𝑥 ( Base ‘ 𝐶 ) = { 𝑥 } ) )
4 1 eqeq1i ⊢ ( 𝐵 = { 𝑥 } ↔ ( Base ‘ 𝐶 ) = { 𝑥 } )
5 4 exbii ⊢ ( ∃ 𝑥 𝐵 = { 𝑥 } ↔ ∃ 𝑥 ( Base ‘ 𝐶 ) = { 𝑥 } )
6 3 5 bitr4di ⊢ ( 𝑐 = 𝐶 → ( ∃ 𝑥 ( Base ‘ 𝑐 ) = { 𝑥 } ↔ ∃ 𝑥 𝐵 = { 𝑥 } ) )
7 df-termc ⊢ TermCat = { 𝑐 ∈ ThinCat ∣ ∃ 𝑥 ( Base ‘ 𝑐 ) = { 𝑥 } }
8 6 7 elrab2 ⊢ ( 𝐶 ∈ TermCat ↔ ( 𝐶 ∈ ThinCat ∧ ∃ 𝑥 𝐵 = { 𝑥 } ) )