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	Could not format assertion : No typesetting found for |- ( ph -> X e. On_s ) with typecode |-

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	Could not format ( X e. On_s <-> E. a e. ~P No X = ( a |s (/) ) ) : No typesetting found for |- ( X e. On_s <-> E. a e. ~P No X = ( a |s (/) ) ) with typecode |-
10	8 9	sylibr	Could not format ( ph -> X e. On_s ) : No typesetting found for |- ( ph -> X e. On_s ) with typecode |-