Theorem 0n0s

Description: Peano postulate: 0s is a non-negative surreal integer. (Contributed by Scott Fenton, 17-Mar-2025)

	Ref	Expression
Assertion	0n0s	Could not format assertion : No typesetting found for |- 0s e. NN0_s with typecode |-

Proof

Step	Hyp	Ref	Expression
1		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
2		fr0g	Could not format ( 0s e. No -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` (/) ) = 0s ) : No typesetting found for |- ( 0s e. No -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` (/) ) = 0s ) with typecode |-
3	1 2	ax-mp	Could not format ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` (/) ) = 0s : No typesetting found for |- ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` (/) ) = 0s with typecode |-
4		frfnom	Could not format ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) Fn _om : No typesetting found for |- ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) Fn _om with typecode |-
5		peano1	$$⊢\varnothing \in \mathrm{\omega }$$
6		fnfvelrn	Could not format ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) Fn _om /\ (/) e. _om ) -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` (/) ) e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ) : No typesetting found for |- ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) Fn _om /\ (/) e. _om ) -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` (/) ) e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ) with typecode |-
7	4 5 6	mp2an	Could not format ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` (/) ) e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) : No typesetting found for |- ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` (/) ) e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) with typecode |-
8	3 7	eqeltrri	Could not format 0s e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) : No typesetting found for |- 0s e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) with typecode |-
9		df-n0s	Could not format NN0_s = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) " _om ) : No typesetting found for |- NN0_s = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) " _om ) with typecode |-
10		df-ima	Could not format ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) " _om ) = ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) : No typesetting found for |- ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) " _om ) = ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) with typecode |-
11	9 10	eqtri	Could not format NN0_s = ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) : No typesetting found for |- NN0_s = ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) with typecode |-
12	8 11	eleqtrri	Could not format 0s e. NN0_s : No typesetting found for |- 0s e. NN0_s with typecode |-