Theorem n0cutlt

Description: A non-negative surreal integer is the simplest number greater than all previous non-negative surreal integers. (Contributed by Scott Fenton, 7-Nov-2025)

	Ref	Expression
Assertion	n0cutlt	⊢ ( 𝐴 ∈ ℕ0s → 𝐴 = ( { 𝑥 ∈ ℕ0s ∣ 𝑥 <s 𝐴 } |s ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		n0on	⊢ ( 𝐴 ∈ ℕ0s → 𝐴 ∈ Ons )
2		oncutlt	⊢ ( 𝐴 ∈ Ons → 𝐴 = ( { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } |s ∅ ) )
3	1 2	syl	⊢ ( 𝐴 ∈ ℕ0s → 𝐴 = ( { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } |s ∅ ) )
4		onltn0s	⊢ ( ( 𝑥 ∈ Ons ∧ 𝐴 ∈ ℕ0s ∧ 𝑥 <s 𝐴 ) → 𝑥 ∈ ℕ0s )
5	4	3expib	⊢ ( 𝑥 ∈ Ons → ( ( 𝐴 ∈ ℕ0s ∧ 𝑥 <s 𝐴 ) → 𝑥 ∈ ℕ0s ) )
6	5	com12	⊢ ( ( 𝐴 ∈ ℕ0s ∧ 𝑥 <s 𝐴 ) → ( 𝑥 ∈ Ons → 𝑥 ∈ ℕ0s ) )
7		n0on	⊢ ( 𝑥 ∈ ℕ0s → 𝑥 ∈ Ons )
8	6 7	impbid1	⊢ ( ( 𝐴 ∈ ℕ0s ∧ 𝑥 <s 𝐴 ) → ( 𝑥 ∈ Ons ↔ 𝑥 ∈ ℕ0s ) )
9	8	ex	⊢ ( 𝐴 ∈ ℕ0s → ( 𝑥 <s 𝐴 → ( 𝑥 ∈ Ons ↔ 𝑥 ∈ ℕ0s ) ) )
10	9	pm5.32rd	⊢ ( 𝐴 ∈ ℕ0s → ( ( 𝑥 ∈ Ons ∧ 𝑥 <s 𝐴 ) ↔ ( 𝑥 ∈ ℕ0s ∧ 𝑥 <s 𝐴 ) ) )
11	10	rabbidva2	⊢ ( 𝐴 ∈ ℕ0s → { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } = { 𝑥 ∈ ℕ0s ∣ 𝑥 <s 𝐴 } )
12	11	oveq1d	⊢ ( 𝐴 ∈ ℕ0s → ( { 𝑥 ∈ Ons ∣ 𝑥 <s 𝐴 } |s ∅ ) = ( { 𝑥 ∈ ℕ0s ∣ 𝑥 <s 𝐴 } |s ∅ ) )
13	3 12	eqtrd	⊢ ( 𝐴 ∈ ℕ0s → 𝐴 = ( { 𝑥 ∈ ℕ0s ∣ 𝑥 <s 𝐴 } |s ∅ ) )