Theorem hashgt1

Description: Restate "set contains at least two elements" in terms of elementhood. (Contributed by Thierry Arnoux, 21-Nov-2023)

	Ref	Expression
Assertion	hashgt1	$$⊢A\in V\to \left(\neg A\in {\left|.\right|}^{-1}\left[\left\{0,1\right\}\right]\leftrightarrow 1<\left|A\right|\right)$$

Proof

Step	Hyp	Ref	Expression
1		hashf	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}$$
2		ffn	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}\to \left|.\right|Fn\mathrm{V}$$
3		elpreima	$$⊢\left|.\right|Fn\mathrm{V}\to \left(A\in {\left|.\right|}^{-1}\left[\left\{0,1\right\}\right]\leftrightarrow \left(A\in \mathrm{V}\wedge \left|A\right|\in \left\{0,1\right\}\right)\right)$$
4	1 2 3	mp2b	$$⊢A\in {\left|.\right|}^{-1}\left[\left\{0,1\right\}\right]\leftrightarrow \left(A\in \mathrm{V}\wedge \left|A\right|\in \left\{0,1\right\}\right)$$
5		elex	$$⊢A\in V\to A\in \mathrm{V}$$
6	5	biantrurd	$$⊢A\in V\to \left(\left|A\right|\in \left\{0,1\right\}\leftrightarrow \left(A\in \mathrm{V}\wedge \left|A\right|\in \left\{0,1\right\}\right)\right)$$
7	4 6	bitr4id	$$⊢A\in V\to \left(A\in {\left|.\right|}^{-1}\left[\left\{0,1\right\}\right]\leftrightarrow \left|A\right|\in \left\{0,1\right\}\right)$$
8	7	notbid	$$⊢A\in V\to \left(\neg A\in {\left|.\right|}^{-1}\left[\left\{0,1\right\}\right]\leftrightarrow \neg \left|A\right|\in \left\{0,1\right\}\right)$$
9		hashxnn0	$$⊢A\in V\to \left|A\right|\in {\mathbb{N}}_0^{*}$$
10		xnn01gt	$$⊢\left|A\right|\in {\mathbb{N}}_0^{*}\to \left(\neg \left|A\right|\in \left\{0,1\right\}\leftrightarrow 1<\left|A\right|\right)$$
11	9 10	syl	$$⊢A\in V\to \left(\neg \left|A\right|\in \left\{0,1\right\}\leftrightarrow 1<\left|A\right|\right)$$
12	8 11	bitrd	$$⊢A\in V\to \left(\neg A\in {\left|.\right|}^{-1}\left[\left\{0,1\right\}\right]\leftrightarrow 1<\left|A\right|\right)$$