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	|- ( A e. NN0_s -> A = ( { x e. NN0_s | x

Proof

Step	Hyp	Ref	Expression
1		n0ons	|- ( A e. NN0_s -> A e. On_s )
2		onscutlt	|- ( A e. On_s -> A = ( { x e. On_s | x
3	1 2	syl	|- ( A e. NN0_s -> A = ( { x e. On_s | x
4		onltn0s	|- ( ( x e. On_s /\ A e. NN0_s /\ x x e. NN0_s )
5	4	3expib	|- ( x e. On_s -> ( ( A e. NN0_s /\ x x e. NN0_s ) )
6	5	com12	|- ( ( A e. NN0_s /\ x ( x e. On_s -> x e. NN0_s ) )
7		n0ons	|- ( x e. NN0_s -> x e. On_s )
8	6 7	impbid1	|- ( ( A e. NN0_s /\ x ( x e. On_s <-> x e. NN0_s ) )
9	8	ex	|- ( A e. NN0_s -> ( x ( x e. On_s <-> x e. NN0_s ) ) )
10	9	pm5.32rd	|- ( A e. NN0_s -> ( ( x e. On_s /\ x ( x e. NN0_s /\ x
11	10	rabbidva2	|- ( A e. NN0_s -> { x e. On_s | x
12	11	oveq1d	|- ( A e. NN0_s -> ( { x e. On_s | x
13	3 12	eqtrd	|- ( A e. NN0_s -> A = ( { x e. NN0_s | x