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 Could not format assertion : No typesetting found for |- ( SetCat ` { { A } } ) e. TermCat with typecode |-

Proof

Step Hyp Ref Expression
1 eqidd ⊢ ⊤ → SetCat ⁡ A = SetCat ⁡ A
2 snex ⊢ A ∈ V
3 2 a1i ⊢ ⊤ → A ∈ V
4 velsn ⊢ x ∈ A ↔ x = A
5 mosn ⊢ x = A → ∃* p p ∈ x
6 4 5 sylbi ⊢ x ∈ A → ∃* p p ∈ x
7 6 rgen ⊢ ∀ x ∈ A ∃* p p ∈ x
8 7 a1i ⊢ ⊤ → ∀ x ∈ A ∃* p p ∈ x
9 1 3 8 setcthin ⊢ ⊤ → SetCat ⁡ A ∈ ThinCat
10 9 mptru ⊢ SetCat ⁡ A ∈ ThinCat
11 snex ⊢ A ∈ V
12 11 ensn1 ⊢ A ≈ 1 𝑜
13 eqid ⊢ SetCat ⁡ A = SetCat ⁡ A
14 13 3 setcbas ⊢ ⊤ → A = Base SetCat ⁡ A
15 14 mptru ⊢ A = Base SetCat ⁡ A
16 15 istermc3 Could not format ( ( SetCat ` { { A } } ) e. TermCat <-> ( ( SetCat ` { { A } } ) e. ThinCat /\ { { A } } ~~ 1o ) ) : No typesetting found for |- ( ( SetCat ` { { A } } ) e. TermCat <-> ( ( SetCat ` { { A } } ) e. ThinCat /\ { { A } } ~~ 1o ) ) with typecode |-
17 10 12 16 mpbir2an Could not format ( SetCat ` { { A } } ) e. TermCat : No typesetting found for |- ( SetCat ` { { A } } ) e. TermCat with typecode |-