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

Metamath Proof Explorer

Theorem termcbas2

Description: The base of a terminal category is given by its object. (Contributed by Zhi Wang, 20-Oct-2025)

Ref Expression
Hypotheses termcbas.c ⊢ ( 𝜑 → 𝐶 ∈ TermCat )
termcbas.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
termcbasmo.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion termcbas2 ( 𝜑 → 𝐵 = { 𝑋 } )

Proof

Step Hyp Ref Expression
1 termcbas.c ⊢ ( 𝜑 → 𝐶 ∈ TermCat )
2 termcbas.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 termcbasmo.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
4 1 2 termcbas ⊢ ( 𝜑 → ∃ 𝑥 𝐵 = { 𝑥 } )
5 simpr ⊢ ( ( 𝜑 ∧ 𝐵 = { 𝑥 } ) → 𝐵 = { 𝑥 } )
6 3 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = { 𝑥 } ) → 𝑋 ∈ 𝐵 )
7 6 5 eleqtrd ⊢ ( ( 𝜑 ∧ 𝐵 = { 𝑥 } ) → 𝑋 ∈ { 𝑥 } )
8 elsni ⊢ ( 𝑋 ∈ { 𝑥 } → 𝑋 = 𝑥 )
9 8 sneqd ⊢ ( 𝑋 ∈ { 𝑥 } → { 𝑋 } = { 𝑥 } )
10 7 9 syl ⊢ ( ( 𝜑 ∧ 𝐵 = { 𝑥 } ) → { 𝑋 } = { 𝑥 } )
11 5 10 eqtr4d ⊢ ( ( 𝜑 ∧ 𝐵 = { 𝑥 } ) → 𝐵 = { 𝑋 } )
12 4 11 exlimddv ⊢ ( 𝜑 → 𝐵 = { 𝑋 } )