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 e. On_s <-> E. a e. ~P No A = ( a |s (/) ) )

Proof

Step	Hyp	Ref	Expression
1		leftssno	|- ( _Left ` A ) C_ No
2		fvex	|- ( _Left ` A ) e. _V
3	2	elpw	|- ( ( _Left ` A ) e. ~P No <-> ( _Left ` A ) C_ No )
4	1 3	mpbir	|- ( _Left ` A ) e. ~P No
5		onsno	|- ( A e. On_s -> A e. No )
6		lrcut	|- ( A e. No -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A )
7	5 6	syl	|- ( A e. On_s -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A )
8		elons	|- ( A e. On_s <-> ( A e. No /\ ( _Right ` A ) = (/) ) )
9	8	simprbi	|- ( A e. On_s -> ( _Right ` A ) = (/) )
10	9	oveq2d	|- ( A e. On_s -> ( ( _Left ` A ) |s ( _Right ` A ) ) = ( ( _Left ` A ) |s (/) ) )
11	7 10	eqtr3d	|- ( A e. On_s -> A = ( ( _Left ` A ) |s (/) ) )
12		oveq1	|- ( a = ( _Left ` A ) -> ( a |s (/) ) = ( ( _Left ` A ) |s (/) ) )
13	12	rspceeqv	|- ( ( ( _Left ` A ) e. ~P No /\ A = ( ( _Left ` A ) |s (/) ) ) -> E. a e. ~P No A = ( a |s (/) ) )
14	4 11 13	sylancr	|- ( A e. On_s -> E. a e. ~P No A = ( a |s (/) ) )
15		nulssgt	|- ( a e. ~P No -> a <
16	15	scutcld	|- ( a e. ~P No -> ( a |s (/) ) e. No )
17		eqidd	|- ( a e. ~P No -> ( a |s (/) ) = ( a |s (/) ) )
18	15 17	cofcutr2d	|- ( a e. ~P No -> A. x e. ( _Right ` ( a |s (/) ) ) E. y e. (/) y <_s x )
19		rex0	|- -. E. y e. (/) y <_s x
20		jcn	|- ( x e. ( _Right ` ( a |s (/) ) ) -> ( -. E. y e. (/) y <_s x -> -. ( x e. ( _Right ` ( a |s (/) ) ) -> E. y e. (/) y <_s x ) ) )
21	19 20	mpi	|- ( x e. ( _Right ` ( a |s (/) ) ) -> -. ( x e. ( _Right ` ( a |s (/) ) ) -> E. y e. (/) y <_s x ) )
22	21	con2i	|- ( ( x e. ( _Right ` ( a |s (/) ) ) -> E. y e. (/) y <_s x ) -> -. x e. ( _Right ` ( a |s (/) ) ) )
23	22	alimi	|- ( A. x ( x e. ( _Right ` ( a |s (/) ) ) -> E. y e. (/) y <_s x ) -> A. x -. x e. ( _Right ` ( a |s (/) ) ) )
24		df-ral	|- ( A. x e. ( _Right ` ( a |s (/) ) ) E. y e. (/) y <_s x <-> A. x ( x e. ( _Right ` ( a |s (/) ) ) -> E. y e. (/) y <_s x ) )
25		eq0	|- ( ( _Right ` ( a |s (/) ) ) = (/) <-> A. x -. x e. ( _Right ` ( a |s (/) ) ) )
26	23 24 25	3imtr4i	|- ( A. x e. ( _Right ` ( a |s (/) ) ) E. y e. (/) y <_s x -> ( _Right ` ( a |s (/) ) ) = (/) )
27	18 26	syl	|- ( a e. ~P No -> ( _Right ` ( a |s (/) ) ) = (/) )
28		elons	|- ( ( a |s (/) ) e. On_s <-> ( ( a |s (/) ) e. No /\ ( _Right ` ( a |s (/) ) ) = (/) ) )
29	16 27 28	sylanbrc	|- ( a e. ~P No -> ( a |s (/) ) e. On_s )
30		eleq1	|- ( A = ( a |s (/) ) -> ( A e. On_s <-> ( a |s (/) ) e. On_s ) )
31	29 30	syl5ibrcom	|- ( a e. ~P No -> ( A = ( a |s (/) ) -> A e. On_s ) )
32	31	rexlimiv	|- ( E. a e. ~P No A = ( a |s (/) ) -> A e. On_s )
33	14 32	impbii	|- ( A e. On_s <-> E. a e. ~P No A = ( a |s (/) ) )