Theorem discbas

Description: A discrete category (a category whose only morphisms are the identity morphisms) can be constructed for any base set. (Contributed by Zhi Wang, 20-Oct-2025)

	Ref	Expression
Hypotheses	discthin.k	⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝐵 ) ⟩ }
	discthin.c	⊢ 𝐶 = ( ProsetToCat ‘ 𝐾 )
Assertion	discbas	⊢ ( 𝐵 ∈ 𝑉 → 𝐵 = ( Base ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		discthin.k	⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝐵 ) ⟩ }
2		discthin.c	⊢ 𝐶 = ( ProsetToCat ‘ 𝐾 )
3	2	a1i	⊢ ( 𝐵 ∈ 𝑉 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
4	1	resipos	⊢ ( 𝐵 ∈ 𝑉 → 𝐾 ∈ Poset )
5		posprs	⊢ ( 𝐾 ∈ Poset → 𝐾 ∈ Proset )
6	4 5	syl	⊢ ( 𝐵 ∈ 𝑉 → 𝐾 ∈ Proset )
7	1	resiposbas	⊢ ( 𝐵 ∈ 𝑉 → 𝐵 = ( Base ‘ 𝐾 ) )
8	3 6 7	prstcbas	⊢ ( 𝐵 ∈ 𝑉 → 𝐵 = ( Base ‘ 𝐶 ) )