Theorem n0cutlt

Description: A non-negative surreal integer is the simplest number greater than all previous non-negative surreal integers. (Contributed by Scott Fenton, 7-Nov-2025)

	Ref	Expression
Assertion	n0cutlt	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A=\left\{x\in {\mathbb{N}}_{\mathrm{0s}}|x{<}_{s}A\right\}{|}_s\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		n0on	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A\in {On}_s$$
2		oncutlt	$$⊢A\in {On}_s\to A=\left\{x\in {On}_s|x{<}_{s}A\right\}{|}_s\varnothing$$
3	1 2	syl	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A=\left\{x\in {On}_s|x{<}_{s}A\right\}{|}_s\varnothing$$
4		onltn0s	$$⊢\left(x\in {On}_s\wedge A\in {\mathbb{N}}_{\mathrm{0s}}\wedge x{<}_{s}A\right)\to x\in {\mathbb{N}}_{\mathrm{0s}}$$
5	4	3expib	$$⊢x\in {On}_s\to \left(\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge x{<}_{s}A\right)\to x\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
6	5	com12	$$⊢\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge x{<}_{s}A\right)\to \left(x\in {On}_s\to x\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
7		n0on	$$⊢x\in {\mathbb{N}}_{\mathrm{0s}}\to x\in {On}_s$$
8	6 7	impbid1	$$⊢\left(A\in {\mathbb{N}}_{\mathrm{0s}}\wedge x{<}_{s}A\right)\to \left(x\in {On}_s\leftrightarrow x\in {\mathbb{N}}_{\mathrm{0s}}\right)$$
9	8	ex	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(x{<}_{s}A\to \left(x\in {On}_s\leftrightarrow x\in {\mathbb{N}}_{\mathrm{0s}}\right)\right)$$
10	9	pm5.32rd	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left(\left(x\in {On}_s\wedge x{<}_{s}A\right)\leftrightarrow \left(x\in {\mathbb{N}}_{\mathrm{0s}}\wedge x{<}_{s}A\right)\right)$$
11	10	rabbidva2	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left\{x\in {On}_s|x{<}_{s}A\right\}=\left\{x\in {\mathbb{N}}_{\mathrm{0s}}|x{<}_{s}A\right\}$$
12	11	oveq1d	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left\{x\in {On}_s|x{<}_{s}A\right\}{|}_s\varnothing =\left\{x\in {\mathbb{N}}_{\mathrm{0s}}|x{<}_{s}A\right\}{|}_s\varnothing$$
13	3 12	eqtrd	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A=\left\{x\in {\mathbb{N}}_{\mathrm{0s}}|x{<}_{s}A\right\}{|}_s\varnothing$$