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 ) e. ThinCat

Proof

Step	Hyp	Ref	Expression
1		eqidd	|- ( T. -> ( SetCat ` 2o ) = ( SetCat ` 2o ) )
2		2oex	|- 2o e. _V
3	2	a1i	|- ( T. -> 2o e. _V )
4		elpri	|- ( x e. { (/) , { (/) } } -> ( x = (/) \/ x = { (/) } ) )
5		0ex	|- (/) e. _V
6		sneq	|- ( y = (/) -> { y } = { (/) } )
7	6	eqeq2d	|- ( y = (/) -> ( x = { y } <-> x = { (/) } ) )
8	5 7	spcev	|- ( x = { (/) } -> E. y x = { y } )
9	8	orim2i	|- ( ( x = (/) \/ x = { (/) } ) -> ( x = (/) \/ E. y x = { y } ) )
10		mo0sn	|- ( E* z z e. x <-> ( x = (/) \/ E. y x = { y } ) )
11	10	biimpri	|- ( ( x = (/) \/ E. y x = { y } ) -> E* z z e. x )
12	4 9 11	3syl	|- ( x e. { (/) , { (/) } } -> E* z z e. x )
13		df2o2	|- 2o = { (/) , { (/) } }
14	12 13	eleq2s	|- ( x e. 2o -> E* z z e. x )
15	14	rgen	|- A. x e. 2o E* z z e. x
16	15	a1i	|- ( T. -> A. x e. 2o E* z z e. x )
17	1 3 16	setcthin	|- ( T. -> ( SetCat ` 2o ) e. ThinCat )
18	17	mptru	|- ( SetCat ` 2o ) e. ThinCat