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	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	elons2d.2	⊢ ( 𝜑 → 𝐴 ⊆ No )
	elons2d.3	⊢ ( 𝜑 → 𝑋 = ( 𝐴 |s ∅ ) )
Assertion	elons2d	⊢ ( 𝜑 → 𝑋 ∈ Ons )

Proof

Step	Hyp	Ref	Expression
1		elons2d.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		elons2d.2	⊢ ( 𝜑 → 𝐴 ⊆ No )
3		elons2d.3	⊢ ( 𝜑 → 𝑋 = ( 𝐴 |s ∅ ) )
4	1 2	elpwd	⊢ ( 𝜑 → 𝐴 ∈ 𝒫 No )
5		oveq1	⊢ ( 𝑎 = 𝐴 → ( 𝑎 |s ∅ ) = ( 𝐴 |s ∅ ) )
6	5	eqeq2d	⊢ ( 𝑎 = 𝐴 → ( 𝑋 = ( 𝑎 |s ∅ ) ↔ 𝑋 = ( 𝐴 |s ∅ ) ) )
7	6	rspcev	⊢ ( ( 𝐴 ∈ 𝒫 No ∧ 𝑋 = ( 𝐴 |s ∅ ) ) → ∃ 𝑎 ∈ 𝒫 No 𝑋 = ( 𝑎 |s ∅ ) )
8	4 3 7	syl2anc	⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝒫 No 𝑋 = ( 𝑎 |s ∅ ) )
9		elons2	⊢ ( 𝑋 ∈ Ons ↔ ∃ 𝑎 ∈ 𝒫 No 𝑋 = ( 𝑎 |s ∅ ) )
10	8 9	sylibr	⊢ ( 𝜑 → 𝑋 ∈ Ons )