Theorem scottn0f

Description: A version of scott0f with inequalities instead of equalities. (Contributed by Giovanni Mascellani, 19-Aug-2018)

	Ref	Expression
Hypotheses	scottn0f.1	$$⊢\underset{\_}{Ⅎ}yA$$
	scottn0f.2	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	scottn0f	$$⊢A\ne \varnothing \leftrightarrow \left\{x\in A|\forall y\in A\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right\}\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		scottn0f.1	$$⊢\underset{\_}{Ⅎ}yA$$
2		scottn0f.2	$$⊢\underset{\_}{Ⅎ}xA$$
3	1 2	scott0f	$$⊢A=\varnothing \leftrightarrow \left\{x\in A|\forall y\in A\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right\}=\varnothing$$
4	3	necon3bii	$$⊢A\ne \varnothing \leftrightarrow \left\{x\in A|\forall y\in A\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right\}\ne \varnothing$$