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

Metamath Proof Explorer

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