Theorem elons2

Description: A surreal is ordinal iff it is the cut of some set of surreals and the empty set. Definition from Conway p. 27. (Contributed by Scott Fenton, 19-Mar-2025)

	Ref	Expression
Assertion	elons2	$$⊢A\in {On}_s\leftrightarrow \exists a\in 𝒫\mathrm{No}A=a{|}_s\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		leftssno	$$⊢L\left(A\right)\subseteq \mathrm{No}$$
2		fvex	$$⊢L\left(A\right)\in \mathrm{V}$$
3	2	elpw	$$⊢L\left(A\right)\in 𝒫\mathrm{No}\leftrightarrow L\left(A\right)\subseteq \mathrm{No}$$
4	1 3	mpbir	$$⊢L\left(A\right)\in 𝒫\mathrm{No}$$
5		onno	$$⊢A\in {On}_s\to A\in \mathrm{No}$$
6		lrcut	$$⊢A\in \mathrm{No}\to L\left(A\right){|}_{s}R\left(A\right)=A$$
7	5 6	syl	$$⊢A\in {On}_s\to L\left(A\right){|}_{s}R\left(A\right)=A$$
8		elons	$$⊢A\in {On}_s\leftrightarrow \left(A\in \mathrm{No}\wedge R\left(A\right)=\varnothing \right)$$
9	8	simprbi	$$⊢A\in {On}_s\to R\left(A\right)=\varnothing$$
10	9	oveq2d	$$⊢A\in {On}_s\to L\left(A\right){|}_{s}R\left(A\right)=L\left(A\right){|}_s\varnothing$$
11	7 10	eqtr3d	$$⊢A\in {On}_s\to A=L\left(A\right){|}_s\varnothing$$
12		oveq1	$$⊢a=L\left(A\right)\to a{|}_s\varnothing =L\left(A\right){|}_s\varnothing$$
13	12	rspceeqv	$$⊢\left(L\left(A\right)\in 𝒫\mathrm{No}\wedge A=L\left(A\right){|}_s\varnothing \right)\to \exists a\in 𝒫\mathrm{No}A=a{|}_s\varnothing$$
14	4 11 13	sylancr	$$⊢A\in {On}_s\to \exists a\in 𝒫\mathrm{No}A=a{|}_s\varnothing$$
15		nulsgts	$$⊢a\in 𝒫\mathrm{No}\to a{\ll }_s\varnothing$$
16	15	cutscld	$$⊢a\in 𝒫\mathrm{No}\to a{|}_s\varnothing \in \mathrm{No}$$
17		eqidd	$$⊢a\in 𝒫\mathrm{No}\to a{|}_s\varnothing =a{|}_s\varnothing$$
18	15 17	cofcutr2d	$$⊢a\in 𝒫\mathrm{No}\to \forall x\in R\left(a{|}_s\varnothing \right)\exists y\in \varnothing y{\le }_{s}x$$
19		rex0	$$⊢\neg \exists y\in \varnothing y{\le }_{s}x$$
20		jcn	$$⊢x\in R\left(a{|}_s\varnothing \right)\to \left(\neg \exists y\in \varnothing y{\le }_{s}x\to \neg \left(x\in R\left(a{|}_s\varnothing \right)\to \exists y\in \varnothing y{\le }_{s}x\right)\right)$$
21	19 20	mpi	$$⊢x\in R\left(a{|}_s\varnothing \right)\to \neg \left(x\in R\left(a{|}_s\varnothing \right)\to \exists y\in \varnothing y{\le }_{s}x\right)$$
22	21	con2i	$$⊢\left(x\in R\left(a{|}_s\varnothing \right)\to \exists y\in \varnothing y{\le }_{s}x\right)\to \neg x\in R\left(a{|}_s\varnothing \right)$$
23	22	alimi	$$⊢\forall x\left(x\in R\left(a{|}_s\varnothing \right)\to \exists y\in \varnothing y{\le }_{s}x\right)\to \forall x\neg x\in R\left(a{|}_s\varnothing \right)$$
24		df-ral	$$⊢\forall x\in R\left(a{|}_s\varnothing \right)\exists y\in \varnothing y{\le }_{s}x\leftrightarrow \forall x\left(x\in R\left(a{|}_s\varnothing \right)\to \exists y\in \varnothing y{\le }_{s}x\right)$$
25		eq0	$$⊢R\left(a{|}_s\varnothing \right)=\varnothing \leftrightarrow \forall x\neg x\in R\left(a{|}_s\varnothing \right)$$
26	23 24 25	3imtr4i	$$⊢\forall x\in R\left(a{|}_s\varnothing \right)\exists y\in \varnothing y{\le }_{s}x\to R\left(a{|}_s\varnothing \right)=\varnothing$$
27	18 26	syl	$$⊢a\in 𝒫\mathrm{No}\to R\left(a{|}_s\varnothing \right)=\varnothing$$
28		elons	$$⊢a{|}_s\varnothing \in {On}_s\leftrightarrow \left(a{|}_s\varnothing \in \mathrm{No}\wedge R\left(a{|}_s\varnothing \right)=\varnothing \right)$$
29	16 27 28	sylanbrc	$$⊢a\in 𝒫\mathrm{No}\to a{|}_s\varnothing \in {On}_s$$
30		eleq1	$$⊢A=a{|}_s\varnothing \to \left(A\in {On}_s\leftrightarrow a{|}_s\varnothing \in {On}_s\right)$$
31	29 30	syl5ibrcom	$$⊢a\in 𝒫\mathrm{No}\to \left(A=a{|}_s\varnothing \to A\in {On}_s\right)$$
32	31	rexlimiv	$$⊢\exists a\in 𝒫\mathrm{No}A=a{|}_s\varnothing \to A\in {On}_s$$
33	14 32	impbii	$$⊢A\in {On}_s\leftrightarrow \exists a\in 𝒫\mathrm{No}A=a{|}_s\varnothing$$