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	⊢ ( 𝐴 ∈ Ons ↔ ∃ 𝑎 ∈ 𝒫 No 𝐴 = ( 𝑎 |s ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		leftssno	⊢ ( L ‘ 𝐴 ) ⊆ No
2		fvex	⊢ ( L ‘ 𝐴 ) ∈ V
3	2	elpw	⊢ ( ( L ‘ 𝐴 ) ∈ 𝒫 No ↔ ( L ‘ 𝐴 ) ⊆ No )
4	1 3	mpbir	⊢ ( L ‘ 𝐴 ) ∈ 𝒫 No
5		onno	⊢ ( 𝐴 ∈ Ons → 𝐴 ∈ No )
6		lrcut	⊢ ( 𝐴 ∈ No → ( ( L ‘ 𝐴 ) |s ( R ‘ 𝐴 ) ) = 𝐴 )
7	5 6	syl	⊢ ( 𝐴 ∈ Ons → ( ( L ‘ 𝐴 ) |s ( R ‘ 𝐴 ) ) = 𝐴 )
8		elons	⊢ ( 𝐴 ∈ Ons ↔ ( 𝐴 ∈ No ∧ ( R ‘ 𝐴 ) = ∅ ) )
9	8	simprbi	⊢ ( 𝐴 ∈ Ons → ( R ‘ 𝐴 ) = ∅ )
10	9	oveq2d	⊢ ( 𝐴 ∈ Ons → ( ( L ‘ 𝐴 ) |s ( R ‘ 𝐴 ) ) = ( ( L ‘ 𝐴 ) |s ∅ ) )
11	7 10	eqtr3d	⊢ ( 𝐴 ∈ Ons → 𝐴 = ( ( L ‘ 𝐴 ) |s ∅ ) )
12		oveq1	⊢ ( 𝑎 = ( L ‘ 𝐴 ) → ( 𝑎 |s ∅ ) = ( ( L ‘ 𝐴 ) |s ∅ ) )
13	12	rspceeqv	⊢ ( ( ( L ‘ 𝐴 ) ∈ 𝒫 No ∧ 𝐴 = ( ( L ‘ 𝐴 ) |s ∅ ) ) → ∃ 𝑎 ∈ 𝒫 No 𝐴 = ( 𝑎 |s ∅ ) )
14	4 11 13	sylancr	⊢ ( 𝐴 ∈ Ons → ∃ 𝑎 ∈ 𝒫 No 𝐴 = ( 𝑎 |s ∅ ) )
15		nulsgts	⊢ ( 𝑎 ∈ 𝒫 No → 𝑎 <<s ∅ )
16	15	cutscld	⊢ ( 𝑎 ∈ 𝒫 No → ( 𝑎 |s ∅ ) ∈ No )
17		eqidd	⊢ ( 𝑎 ∈ 𝒫 No → ( 𝑎 |s ∅ ) = ( 𝑎 |s ∅ ) )
18	15 17	cofcutr2d	⊢ ( 𝑎 ∈ 𝒫 No → ∀ 𝑥 ∈ ( R ‘ ( 𝑎 |s ∅ ) ) ∃ 𝑦 ∈ ∅ 𝑦 ≤s 𝑥 )
19		rex0	⊢ ¬ ∃ 𝑦 ∈ ∅ 𝑦 ≤s 𝑥
20		jcn	⊢ ( 𝑥 ∈ ( R ‘ ( 𝑎 |s ∅ ) ) → ( ¬ ∃ 𝑦 ∈ ∅ 𝑦 ≤s 𝑥 → ¬ ( 𝑥 ∈ ( R ‘ ( 𝑎 |s ∅ ) ) → ∃ 𝑦 ∈ ∅ 𝑦 ≤s 𝑥 ) ) )
21	19 20	mpi	⊢ ( 𝑥 ∈ ( R ‘ ( 𝑎 |s ∅ ) ) → ¬ ( 𝑥 ∈ ( R ‘ ( 𝑎 |s ∅ ) ) → ∃ 𝑦 ∈ ∅ 𝑦 ≤s 𝑥 ) )
22	21	con2i	⊢ ( ( 𝑥 ∈ ( R ‘ ( 𝑎 |s ∅ ) ) → ∃ 𝑦 ∈ ∅ 𝑦 ≤s 𝑥 ) → ¬ 𝑥 ∈ ( R ‘ ( 𝑎 |s ∅ ) ) )
23	22	alimi	⊢ ( ∀ 𝑥 ( 𝑥 ∈ ( R ‘ ( 𝑎 |s ∅ ) ) → ∃ 𝑦 ∈ ∅ 𝑦 ≤s 𝑥 ) → ∀ 𝑥 ¬ 𝑥 ∈ ( R ‘ ( 𝑎 |s ∅ ) ) )
24		df-ral	⊢ ( ∀ 𝑥 ∈ ( R ‘ ( 𝑎 |s ∅ ) ) ∃ 𝑦 ∈ ∅ 𝑦 ≤s 𝑥 ↔ ∀ 𝑥 ( 𝑥 ∈ ( R ‘ ( 𝑎 |s ∅ ) ) → ∃ 𝑦 ∈ ∅ 𝑦 ≤s 𝑥 ) )
25		eq0	⊢ ( ( R ‘ ( 𝑎 |s ∅ ) ) = ∅ ↔ ∀ 𝑥 ¬ 𝑥 ∈ ( R ‘ ( 𝑎 |s ∅ ) ) )
26	23 24 25	3imtr4i	⊢ ( ∀ 𝑥 ∈ ( R ‘ ( 𝑎 |s ∅ ) ) ∃ 𝑦 ∈ ∅ 𝑦 ≤s 𝑥 → ( R ‘ ( 𝑎 |s ∅ ) ) = ∅ )
27	18 26	syl	⊢ ( 𝑎 ∈ 𝒫 No → ( R ‘ ( 𝑎 |s ∅ ) ) = ∅ )
28		elons	⊢ ( ( 𝑎 |s ∅ ) ∈ Ons ↔ ( ( 𝑎 |s ∅ ) ∈ No ∧ ( R ‘ ( 𝑎 |s ∅ ) ) = ∅ ) )
29	16 27 28	sylanbrc	⊢ ( 𝑎 ∈ 𝒫 No → ( 𝑎 |s ∅ ) ∈ Ons )
30		eleq1	⊢ ( 𝐴 = ( 𝑎 |s ∅ ) → ( 𝐴 ∈ Ons ↔ ( 𝑎 |s ∅ ) ∈ Ons ) )
31	29 30	syl5ibrcom	⊢ ( 𝑎 ∈ 𝒫 No → ( 𝐴 = ( 𝑎 |s ∅ ) → 𝐴 ∈ Ons ) )
32	31	rexlimiv	⊢ ( ∃ 𝑎 ∈ 𝒫 No 𝐴 = ( 𝑎 |s ∅ ) → 𝐴 ∈ Ons )
33	14 32	impbii	⊢ ( 𝐴 ∈ Ons ↔ ∃ 𝑎 ∈ 𝒫 No 𝐴 = ( 𝑎 |s ∅ ) )