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	Could not format assertion : No typesetting found for |- ( A e. On_s <-> E. a e. ~P No A = ( a |s (/) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		leftssno	Could not format ( _Left ` A ) C_ No : No typesetting found for |- ( _Left ` A ) C_ No with typecode |-
2		fvex	Could not format ( _Left ` A ) e. _V : No typesetting found for |- ( _Left ` A ) e. _V with typecode |-
3	2	elpw	Could not format ( ( _Left ` A ) e. ~P No <-> ( _Left ` A ) C_ No ) : No typesetting found for |- ( ( _Left ` A ) e. ~P No <-> ( _Left ` A ) C_ No ) with typecode |-
4	1 3	mpbir	Could not format ( _Left ` A ) e. ~P No : No typesetting found for |- ( _Left ` A ) e. ~P No with typecode |-
5		onsno	Could not format ( A e. On_s -> A e. No ) : No typesetting found for |- ( A e. On_s -> A e. No ) with typecode |-
6		lrcut	Could not format ( A e. No -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A ) : No typesetting found for |- ( A e. No -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A ) with typecode |-
7	5 6	syl	Could not format ( A e. On_s -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A ) : No typesetting found for |- ( A e. On_s -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A ) with typecode |-
8		elons	Could not format ( A e. On_s <-> ( A e. No /\ ( _Right ` A ) = (/) ) ) : No typesetting found for |- ( A e. On_s <-> ( A e. No /\ ( _Right ` A ) = (/) ) ) with typecode |-
9	8	simprbi	Could not format ( A e. On_s -> ( _Right ` A ) = (/) ) : No typesetting found for |- ( A e. On_s -> ( _Right ` A ) = (/) ) with typecode |-
10	9	oveq2d	Could not format ( A e. On_s -> ( ( _Left ` A ) |s ( _Right ` A ) ) = ( ( _Left ` A ) |s (/) ) ) : No typesetting found for |- ( A e. On_s -> ( ( _Left ` A ) |s ( _Right ` A ) ) = ( ( _Left ` A ) |s (/) ) ) with typecode |-
11	7 10	eqtr3d	Could not format ( A e. On_s -> A = ( ( _Left ` A ) |s (/) ) ) : No typesetting found for |- ( A e. On_s -> A = ( ( _Left ` A ) |s (/) ) ) with typecode |-
12		oveq1	Could not format ( a = ( _Left ` A ) -> ( a |s (/) ) = ( ( _Left ` A ) |s (/) ) ) : No typesetting found for |- ( a = ( _Left ` A ) -> ( a |s (/) ) = ( ( _Left ` A ) |s (/) ) ) with typecode |-
13	12	rspceeqv	Could not format ( ( ( _Left ` A ) e. ~P No /\ A = ( ( _Left ` A ) |s (/) ) ) -> E. a e. ~P No A = ( a |s (/) ) ) : No typesetting found for |- ( ( ( _Left ` A ) e. ~P No /\ A = ( ( _Left ` A ) |s (/) ) ) -> E. a e. ~P No A = ( a |s (/) ) ) with typecode |-
14	4 11 13	sylancr	Could not format ( A e. On_s -> E. a e. ~P No A = ( a |s (/) ) ) : No typesetting found for |- ( A e. On_s -> E. a e. ~P No A = ( a |s (/) ) ) with typecode |-
15		nulssgt	$$⊢a\in 𝒫\mathrm{No}\to a{\ll }_s\varnothing$$
16	15	scutcld	$$⊢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	Could not format ( a e. ~P No -> A. x e. ( _Right ` ( a |s (/) ) ) E. y e. (/) y <_s x ) : No typesetting found for |- ( a e. ~P No -> A. x e. ( _Right ` ( a |s (/) ) ) E. y e. (/) y <_s x ) with typecode |-
19		rex0	$$⊢\neg \exists y\in \varnothing y{\le }_{s}x$$
20		jcn	Could not format ( x e. ( _Right ` ( a |s (/) ) ) -> ( -. E. y e. (/) y <_s x -> -. ( x e. ( _Right ` ( a |s (/) ) ) -> E. y e. (/) y <_s x ) ) ) : No typesetting found for |- ( x e. ( _Right ` ( a |s (/) ) ) -> ( -. E. y e. (/) y <_s x -> -. ( x e. ( _Right ` ( a |s (/) ) ) -> E. y e. (/) y <_s x ) ) ) with typecode |-
21	19 20	mpi	Could not format ( x e. ( _Right ` ( a |s (/) ) ) -> -. ( x e. ( _Right ` ( a |s (/) ) ) -> E. y e. (/) y <_s x ) ) : No typesetting found for |- ( x e. ( _Right ` ( a |s (/) ) ) -> -. ( x e. ( _Right ` ( a |s (/) ) ) -> E. y e. (/) y <_s x ) ) with typecode |-
22	21	con2i	Could not format ( ( x e. ( _Right ` ( a |s (/) ) ) -> E. y e. (/) y <_s x ) -> -. x e. ( _Right ` ( a |s (/) ) ) ) : No typesetting found for |- ( ( x e. ( _Right ` ( a |s (/) ) ) -> E. y e. (/) y <_s x ) -> -. x e. ( _Right ` ( a |s (/) ) ) ) with typecode |-
23	22	alimi	Could not format ( A. x ( x e. ( _Right ` ( a |s (/) ) ) -> E. y e. (/) y <_s x ) -> A. x -. x e. ( _Right ` ( a |s (/) ) ) ) : No typesetting found for |- ( A. x ( x e. ( _Right ` ( a |s (/) ) ) -> E. y e. (/) y <_s x ) -> A. x -. x e. ( _Right ` ( a |s (/) ) ) ) with typecode |-
24		df-ral	Could not format ( 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 ) ) : No typesetting found for |- ( 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 ) ) with typecode |-
25		eq0	Could not format ( ( _Right ` ( a |s (/) ) ) = (/) <-> A. x -. x e. ( _Right ` ( a |s (/) ) ) ) : No typesetting found for |- ( ( _Right ` ( a |s (/) ) ) = (/) <-> A. x -. x e. ( _Right ` ( a |s (/) ) ) ) with typecode |-
26	23 24 25	3imtr4i	Could not format ( A. x e. ( _Right ` ( a |s (/) ) ) E. y e. (/) y <_s x -> ( _Right ` ( a |s (/) ) ) = (/) ) : No typesetting found for |- ( A. x e. ( _Right ` ( a |s (/) ) ) E. y e. (/) y <_s x -> ( _Right ` ( a |s (/) ) ) = (/) ) with typecode |-
27	18 26	syl	Could not format ( a e. ~P No -> ( _Right ` ( a |s (/) ) ) = (/) ) : No typesetting found for |- ( a e. ~P No -> ( _Right ` ( a |s (/) ) ) = (/) ) with typecode |-
28		elons	Could not format ( ( a |s (/) ) e. On_s <-> ( ( a |s (/) ) e. No /\ ( _Right ` ( a |s (/) ) ) = (/) ) ) : No typesetting found for |- ( ( a |s (/) ) e. On_s <-> ( ( a |s (/) ) e. No /\ ( _Right ` ( a |s (/) ) ) = (/) ) ) with typecode |-
29	16 27 28	sylanbrc	Could not format ( a e. ~P No -> ( a |s (/) ) e. On_s ) : No typesetting found for |- ( a e. ~P No -> ( a |s (/) ) e. On_s ) with typecode |-
30		eleq1	Could not format ( A = ( a |s (/) ) -> ( A e. On_s <-> ( a |s (/) ) e. On_s ) ) : No typesetting found for |- ( A = ( a |s (/) ) -> ( A e. On_s <-> ( a |s (/) ) e. On_s ) ) with typecode |-
31	29 30	syl5ibrcom	Could not format ( a e. ~P No -> ( A = ( a |s (/) ) -> A e. On_s ) ) : No typesetting found for |- ( a e. ~P No -> ( A = ( a |s (/) ) -> A e. On_s ) ) with typecode |-
32	31	rexlimiv	Could not format ( E. a e. ~P No A = ( a |s (/) ) -> A e. On_s ) : No typesetting found for |- ( E. a e. ~P No A = ( a |s (/) ) -> A e. On_s ) with typecode |-
33	14 32	impbii	Could not format ( A e. On_s <-> E. a e. ~P No A = ( a |s (/) ) ) : No typesetting found for |- ( A e. On_s <-> E. a e. ~P No A = ( a |s (/) ) ) with typecode |-