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

Metamath Proof Explorer

Theorem termcpropd

Description: Two structures with the same base, hom-sets and composition operation are either both terminal categories or neither. (Contributed by Zhi Wang, 16-Oct-2025)

Ref Expression
Hypotheses termcpropd.1 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
termcpropd.2 ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D
termcpropd.3 ⊢ φ → C ∈ V
termcpropd.4 ⊢ φ → D ∈ W
Assertion termcpropd Could not format assertion : No typesetting found for |- ( ph -> ( C e. TermCat <-> D e. TermCat ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 termcpropd.1 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
2 termcpropd.2 ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D
3 termcpropd.3 ⊢ φ → C ∈ V
4 termcpropd.4 ⊢ φ → D ∈ W
5 1 2 3 4 thincpropd ⊢ φ → C ∈ ThinCat ↔ D ∈ ThinCat
6 1 homfeqbas ⊢ φ → Base C = Base D
7 6 eqeq1d ⊢ φ → Base C = x ↔ Base D = x
8 7 exbidv ⊢ φ → ∃ x Base C = x ↔ ∃ x Base D = x
9 5 8 anbi12d ⊢ φ → C ∈ ThinCat ∧ ∃ x Base C = x ↔ D ∈ ThinCat ∧ ∃ x Base D = x
10 eqid ⊢ Base C = Base C
11 10 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 |-
12 eqid ⊢ Base D = Base D
13 12 istermc Could not format ( D e. TermCat <-> ( D e. ThinCat /\ E. x ( Base ` D ) = { x } ) ) : No typesetting found for |- ( D e. TermCat <-> ( D e. ThinCat /\ E. x ( Base ` D ) = { x } ) ) with typecode |-
14 9 11 13 3bitr4g Could not format ( ph -> ( C e. TermCat <-> D e. TermCat ) ) : No typesetting found for |- ( ph -> ( C e. TermCat <-> D e. TermCat ) ) with typecode |-