Theorem n0on

Description: A surreal natural is a surreal ordinal. (Contributed by Scott Fenton, 2-Apr-2025)

	Ref	Expression
Assertion	n0on	⊢ ( 𝐴 ∈ ℕ0s → 𝐴 ∈ Ons )

Proof

Step	Hyp	Ref	Expression
1		n0no	⊢ ( 𝐴 ∈ ℕ0s → 𝐴 ∈ No )
2		1no	⊢ 1s ∈ No
3		subscl	⊢ ( ( 𝐴 ∈ No ∧ 1s ∈ No ) → ( 𝐴 -s 1s ) ∈ No )
4	1 2 3	sylancl	⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 -s 1s ) ∈ No )
5		ovex	⊢ ( 𝐴 -s 1s ) ∈ V
6	5	snelpw	⊢ ( ( 𝐴 -s 1s ) ∈ No ↔ { ( 𝐴 -s 1s ) } ∈ 𝒫 No )
7	4 6	sylib	⊢ ( 𝐴 ∈ ℕ0s → { ( 𝐴 -s 1s ) } ∈ 𝒫 No )
8		n0cut	⊢ ( 𝐴 ∈ ℕ0s → 𝐴 = ( { ( 𝐴 -s 1s ) } |s ∅ ) )
9		oveq1	⊢ ( 𝑥 = { ( 𝐴 -s 1s ) } → ( 𝑥 |s ∅ ) = ( { ( 𝐴 -s 1s ) } |s ∅ ) )
10	9	eqeq2d	⊢ ( 𝑥 = { ( 𝐴 -s 1s ) } → ( 𝐴 = ( 𝑥 |s ∅ ) ↔ 𝐴 = ( { ( 𝐴 -s 1s ) } |s ∅ ) ) )
11	10	rspcev	⊢ ( ( { ( 𝐴 -s 1s ) } ∈ 𝒫 No ∧ 𝐴 = ( { ( 𝐴 -s 1s ) } |s ∅ ) ) → ∃ 𝑥 ∈ 𝒫 No 𝐴 = ( 𝑥 |s ∅ ) )
12	7 8 11	syl2anc	⊢ ( 𝐴 ∈ ℕ0s → ∃ 𝑥 ∈ 𝒫 No 𝐴 = ( 𝑥 |s ∅ ) )
13		elons2	⊢ ( 𝐴 ∈ Ons ↔ ∃ 𝑥 ∈ 𝒫 No 𝐴 = ( 𝑥 |s ∅ ) )
14	12 13	sylibr	⊢ ( 𝐴 ∈ ℕ0s → 𝐴 ∈ Ons )