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	|- ( ph -> A e. V )
	elons2d.2	|- ( ph -> A C_ No )
	elons2d.3	|- ( ph -> X = ( A |s (/) ) )
Assertion	elons2d	|- ( ph -> X e. On_s )

Proof

Step	Hyp	Ref	Expression
1		elons2d.1	|- ( ph -> A e. V )
2		elons2d.2	|- ( ph -> A C_ No )
3		elons2d.3	|- ( ph -> X = ( A |s (/) ) )
4	1 2	elpwd	|- ( ph -> A e. ~P No )
5		oveq1	|- ( a = A -> ( a |s (/) ) = ( A |s (/) ) )
6	5	eqeq2d	|- ( a = A -> ( X = ( a |s (/) ) <-> X = ( A |s (/) ) ) )
7	6	rspcev	|- ( ( A e. ~P No /\ X = ( A |s (/) ) ) -> E. a e. ~P No X = ( a |s (/) ) )
8	4 3 7	syl2anc	|- ( ph -> E. a e. ~P No X = ( a |s (/) ) )
9		elons2	|- ( X e. On_s <-> E. a e. ~P No X = ( a |s (/) ) )
10	8 9	sylibr	|- ( ph -> X e. On_s )