Theorem elons2d

Description: The cut of any set of surreals and the empty set is a surreal ordinal. (Contributed by Scott Fenton, 19-Mar-2025)

	Ref	Expression
Hypotheses	elons2d.1	$$⊢\phi \to A\in V$$
	elons2d.2	$$⊢\phi \to A\subseteq \mathrm{No}$$
	elons2d.3	$$⊢\phi \to X=A{|}_s\varnothing$$
Assertion	elons2d	$$⊢\phi \to X\in {On}_s$$

Proof

Step	Hyp	Ref	Expression
1		elons2d.1	$$⊢\phi \to A\in V$$
2		elons2d.2	$$⊢\phi \to A\subseteq \mathrm{No}$$
3		elons2d.3	$$⊢\phi \to X=A{|}_s\varnothing$$
4	1 2	elpwd	$$⊢\phi \to A\in 𝒫\mathrm{No}$$
5		oveq1	$$⊢a=A\to a{|}_s\varnothing =A{|}_s\varnothing$$
6	5	eqeq2d	$$⊢a=A\to \left(X=a{|}_s\varnothing \leftrightarrow X=A{|}_s\varnothing \right)$$
7	6	rspcev	$$⊢\left(A\in 𝒫\mathrm{No}\wedge X=A{|}_s\varnothing \right)\to \exists a\in 𝒫\mathrm{No}X=a{|}_s\varnothing$$
8	4 3 7	syl2anc	$$⊢\phi \to \exists a\in 𝒫\mathrm{No}X=a{|}_s\varnothing$$
9		elons2	$$⊢X\in {On}_s\leftrightarrow \exists a\in 𝒫\mathrm{No}X=a{|}_s\varnothing$$
10	8 9	sylibr	$$⊢\phi \to X\in {On}_s$$