Theorem setc2othin

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

	Ref	Expression
Assertion	setc2othin	Could not format assertion : No typesetting found for |- ( SetCat ` 2o ) e. ThinCat with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eqidd	$$⊢\top \to \mathrm{SetCat}\left(2_{𝑜}\right)=\mathrm{SetCat}\left(2_{𝑜}\right)$$
2		2oex	$$⊢2_{𝑜}\in \mathrm{V}$$
3	2	a1i	$$⊢\top \to 2_{𝑜}\in \mathrm{V}$$
4		elpri	$$⊢x\in \left\{\varnothing ,\left\{\varnothing \right\}\right\}\to \left(x=\varnothing \vee x=\left\{\varnothing \right\}\right)$$
5		0ex	$$⊢\varnothing \in \mathrm{V}$$
6		sneq	$$⊢y=\varnothing \to \left\{y\right\}=\left\{\varnothing \right\}$$
7	6	eqeq2d	$$⊢y=\varnothing \to \left(x=\left\{y\right\}\leftrightarrow x=\left\{\varnothing \right\}\right)$$
8	5 7	spcev	$$⊢x=\left\{\varnothing \right\}\to \exists yx=\left\{y\right\}$$
9	8	orim2i	$$⊢\left(x=\varnothing \vee x=\left\{\varnothing \right\}\right)\to \left(x=\varnothing \vee \exists yx=\left\{y\right\}\right)$$
10		mo0sn	$$⊢{\exists }^{*}zz\in x\leftrightarrow \left(x=\varnothing \vee \exists yx=\left\{y\right\}\right)$$
11	10	biimpri	$$⊢\left(x=\varnothing \vee \exists yx=\left\{y\right\}\right)\to {\exists }^{*}zz\in x$$
12	4 9 11	3syl	$$⊢x\in \left\{\varnothing ,\left\{\varnothing \right\}\right\}\to {\exists }^{*}zz\in x$$
13		df2o2	$$⊢2_{𝑜}=\left\{\varnothing ,\left\{\varnothing \right\}\right\}$$
14	12 13	eleq2s	$$⊢x\in 2_{𝑜}\to {\exists }^{*}zz\in x$$
15	14	rgen	$$⊢\forall x\in 2_{𝑜}{\exists }^{*}zz\in x$$
16	15	a1i	$$⊢\top \to \forall x\in 2_{𝑜}{\exists }^{*}zz\in x$$
17	1 3 16	setcthin	Could not format ( T. -> ( SetCat ` 2o ) e. ThinCat ) : No typesetting found for |- ( T. -> ( SetCat ` 2o ) e. ThinCat ) with typecode |-
18	17	mptru	Could not format ( SetCat ` 2o ) e. ThinCat : No typesetting found for |- ( SetCat ` 2o ) e. ThinCat with typecode |-