Theorem setcsnterm

Description: The category of one set, either a singleton set or an empty set, is terminal. (Contributed by Zhi Wang, 18-Oct-2025)

	Ref	Expression
Assertion	setcsnterm	⊢ ( SetCat ‘ { { 𝐴 } } ) ∈ TermCat

Proof

Step	Hyp	Ref	Expression
1		eqidd	⊢ ( ⊤ → ( SetCat ‘ { { 𝐴 } } ) = ( SetCat ‘ { { 𝐴 } } ) )
2		snex	⊢ { { 𝐴 } } ∈ V
3	2	a1i	⊢ ( ⊤ → { { 𝐴 } } ∈ V )
4		velsn	⊢ ( 𝑥 ∈ { { 𝐴 } } ↔ 𝑥 = { 𝐴 } )
5		mosn	⊢ ( 𝑥 = { 𝐴 } → ∃* 𝑝 𝑝 ∈ 𝑥 )
6	4 5	sylbi	⊢ ( 𝑥 ∈ { { 𝐴 } } → ∃* 𝑝 𝑝 ∈ 𝑥 )
7	6	rgen	⊢ ∀ 𝑥 ∈ { { 𝐴 } } ∃* 𝑝 𝑝 ∈ 𝑥
8	7	a1i	⊢ ( ⊤ → ∀ 𝑥 ∈ { { 𝐴 } } ∃* 𝑝 𝑝 ∈ 𝑥 )
9	1 3 8	setcthin	⊢ ( ⊤ → ( SetCat ‘ { { 𝐴 } } ) ∈ ThinCat )
10	9	mptru	⊢ ( SetCat ‘ { { 𝐴 } } ) ∈ ThinCat
11		snex	⊢ { 𝐴 } ∈ V
12	11	ensn1	⊢ { { 𝐴 } } ≈ 1o
13		eqid	⊢ ( SetCat ‘ { { 𝐴 } } ) = ( SetCat ‘ { { 𝐴 } } )
14	13 3	setcbas	⊢ ( ⊤ → { { 𝐴 } } = ( Base ‘ ( SetCat ‘ { { 𝐴 } } ) ) )
15	14	mptru	⊢ { { 𝐴 } } = ( Base ‘ ( SetCat ‘ { { 𝐴 } } ) )
16	15	istermc3	⊢ ( ( SetCat ‘ { { 𝐴 } } ) ∈ TermCat ↔ ( ( SetCat ‘ { { 𝐴 } } ) ∈ ThinCat ∧ { { 𝐴 } } ≈ 1o ) )
17	10 12 16	mpbir2an	⊢ ( SetCat ‘ { { 𝐴 } } ) ∈ TermCat