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

Metamath Proof Explorer

Theorem setc2othin

Description: The category ( SetCat2o ) is thin. A special case of setcthin . (Contributed by Zhi Wang, 20-Sep-2024)

Ref Expression
Assertion setc2othin ⊢ SetCat ⁡ 2 𝑜 ∈ ThinCat

Proof

Step Hyp Ref Expression
1 eqidd ⊢ ⊤ → SetCat ⁡ 2 𝑜 = SetCat ⁡ 2 𝑜
2 2oex ⊢ 2 𝑜 ∈ V
3 2 a1i ⊢ ⊤ → 2 𝑜 ∈ V
4 elpri ⊢ x ∈ ∅ ∅ → x = ∅ ∨ x = ∅
5 0ex ⊢ ∅ ∈ V
6 sneq ⊢ y = ∅ → y = ∅
7 6 eqeq2d ⊢ y = ∅ → x = y ↔ x = ∅
8 5 7 spcev ⊢ x = ∅ → ∃ y x = y
9 8 orim2i ⊢ x = ∅ ∨ x = ∅ → x = ∅ ∨ ∃ y x = y
10 mo0sn ⊢ ∃* z z ∈ x ↔ x = ∅ ∨ ∃ y x = y
11 10 biimpri ⊢ x = ∅ ∨ ∃ y x = y → ∃* z z ∈ x
12 4 9 11 3syl ⊢ x ∈ ∅ ∅ → ∃* z z ∈ x
13 df2o2 ⊢ 2 𝑜 = ∅ ∅
14 12 13 eleq2s ⊢ x ∈ 2 𝑜 → ∃* z z ∈ x
15 14 rgen ⊢ ∀ x ∈ 2 𝑜 ∃* z z ∈ x
16 15 a1i ⊢ ⊤ → ∀ x ∈ 2 𝑜 ∃* z z ∈ x
17 1 3 16 setcthin ⊢ ⊤ → SetCat ⁡ 2 𝑜 ∈ ThinCat
18 17 mptru ⊢ SetCat ⁡ 2 𝑜 ∈ ThinCat