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	⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝐵 ) ⟩ }
	discthin.c	⊢ 𝐶 = ( ProsetToCat ‘ 𝐾 )
Assertion	discsnterm	⊢ ( ∃ 𝑥 𝐵 = { 𝑥 } → 𝐶 ∈ TermCat )

Proof

Step	Hyp	Ref	Expression
1		discthin.k	⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝐵 ) ⟩ }
2		discthin.c	⊢ 𝐶 = ( ProsetToCat ‘ 𝐾 )
3		discsntermlem	⊢ ( ∃ 𝑥 𝐵 = { 𝑥 } → 𝐵 ∈ { 𝑏 ∣ ∃ 𝑥 𝑏 = { 𝑥 } } )
4	1 2	discthin	⊢ ( 𝐵 ∈ { 𝑏 ∣ ∃ 𝑥 𝑏 = { 𝑥 } } → 𝐶 ∈ ThinCat )
5	3 4	syl	⊢ ( ∃ 𝑥 𝐵 = { 𝑥 } → 𝐶 ∈ ThinCat )
6		elex	⊢ ( 𝐵 ∈ { 𝑏 ∣ ∃ 𝑥 𝑏 = { 𝑥 } } → 𝐵 ∈ V )
7	1 2	discbas	⊢ ( 𝐵 ∈ V → 𝐵 = ( Base ‘ 𝐶 ) )
8	7	eqeq1d	⊢ ( 𝐵 ∈ V → ( 𝐵 = { 𝑥 } ↔ ( Base ‘ 𝐶 ) = { 𝑥 } ) )
9	8	exbidv	⊢ ( 𝐵 ∈ V → ( ∃ 𝑥 𝐵 = { 𝑥 } ↔ ∃ 𝑥 ( Base ‘ 𝐶 ) = { 𝑥 } ) )
10	3 6 9	3syl	⊢ ( ∃ 𝑥 𝐵 = { 𝑥 } → ( ∃ 𝑥 𝐵 = { 𝑥 } ↔ ∃ 𝑥 ( Base ‘ 𝐶 ) = { 𝑥 } ) )
11	10	ibi	⊢ ( ∃ 𝑥 𝐵 = { 𝑥 } → ∃ 𝑥 ( Base ‘ 𝐶 ) = { 𝑥 } )
12		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
13	12	istermc	⊢ ( 𝐶 ∈ TermCat ↔ ( 𝐶 ∈ ThinCat ∧ ∃ 𝑥 ( Base ‘ 𝐶 ) = { 𝑥 } ) )
14	5 11 13	sylanbrc	⊢ ( ∃ 𝑥 𝐵 = { 𝑥 } → 𝐶 ∈ TermCat )

Metamath Proof Explorer

Theorem discsnterm

Proof