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