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 ‘ 2o ) ∈ ThinCat

Proof

Step Hyp Ref Expression
1 eqidd ⊢ ( ⊤ → ( SetCat ‘ 2o ) = ( SetCat ‘ 2o ) )
2 2oex ⊢ 2o ∈ V
3 2 a1i ⊢ ( ⊤ → 2o ∈ V )
4 elpri ⊢ ( 𝑥 ∈ { ∅ , { ∅ } } → ( 𝑥 = ∅ ∨ 𝑥 = { ∅ } ) )
5 0ex ⊢ ∅ ∈ V
6 sneq ⊢ ( 𝑦 = ∅ → { 𝑦 } = { ∅ } )
7 6 eqeq2d ⊢ ( 𝑦 = ∅ → ( 𝑥 = { 𝑦 } ↔ 𝑥 = { ∅ } ) )
8 5 7 spcev ⊢ ( 𝑥 = { ∅ } → ∃ 𝑦 𝑥 = { 𝑦 } )
9 8 orim2i ⊢ ( ( 𝑥 = ∅ ∨ 𝑥 = { ∅ } ) → ( 𝑥 = ∅ ∨ ∃ 𝑦 𝑥 = { 𝑦 } ) )
10 mo0sn ⊢ ( ∃* 𝑧 𝑧 ∈ 𝑥 ↔ ( 𝑥 = ∅ ∨ ∃ 𝑦 𝑥 = { 𝑦 } ) )
11 10 biimpri ⊢ ( ( 𝑥 = ∅ ∨ ∃ 𝑦 𝑥 = { 𝑦 } ) → ∃* 𝑧 𝑧 ∈ 𝑥 )
12 4 9 11 3syl ⊢ ( 𝑥 ∈ { ∅ , { ∅ } } → ∃* 𝑧 𝑧 ∈ 𝑥 )
13 df2o2 ⊢ 2o = { ∅ , { ∅ } }
14 12 13 eleq2s ⊢ ( 𝑥 ∈ 2o → ∃* 𝑧 𝑧 ∈ 𝑥 )
15 14 rgen ⊢ ∀ 𝑥 ∈ 2o ∃* 𝑧 𝑧 ∈ 𝑥
16 15 a1i ⊢ ( ⊤ → ∀ 𝑥 ∈ 2o ∃* 𝑧 𝑧 ∈ 𝑥 )
17 1 3 16 setcthin ⊢ ( ⊤ → ( SetCat ‘ 2o ) ∈ ThinCat )
18 17 mptru ⊢ ( SetCat ‘ 2o ) ∈ ThinCat