Theorem cutneg

Description: The simplest number greater than a negative number is zero. (Contributed by Scott Fenton, 4-Sep-2025)

	Ref	Expression
Hypotheses	cutneg.1	$$⊢\phi \to A\in \mathrm{No}$$
	cutneg.2	$$⊢\phi \to A{<}_s{0}_s$$
Assertion	cutneg	$$⊢\phi \to \left\{A\right\}{|}_s\varnothing =0_s$$

Proof

Step	Hyp	Ref	Expression
1		cutneg.1	$$⊢\phi \to A\in \mathrm{No}$$
2		cutneg.2	$$⊢\phi \to A{<}_s{0}_s$$
3		0sno	$$⊢0_s\in \mathrm{No}$$
4	3	a1i	$$⊢\phi \to 0_s\in \mathrm{No}$$
5	1 4 2	ssltsn	$$⊢\phi \to \left\{A\right\}{\ll }_s\left\{0_s\right\}$$
6		snelpwi	$$⊢0_s\in \mathrm{No}\to \left\{0_s\right\}\in 𝒫\mathrm{No}$$
7	3 6	ax-mp	$$⊢\left\{0_s\right\}\in 𝒫\mathrm{No}$$
8		nulssgt	$$⊢\left\{0_s\right\}\in 𝒫\mathrm{No}\to \left\{0_s\right\}{\ll }_s\varnothing$$
9	7 8	mp1i	$$⊢\phi \to \left\{0_s\right\}{\ll }_s\varnothing$$
10	5 9	cuteq0	$$⊢\phi \to \left\{A\right\}{|}_s\varnothing =0_s$$