Theorem peano2n0s

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

	Ref	Expression
Assertion	peano2n0s	Could not format assertion : No typesetting found for |- ( A e. NN0_s -> ( A +s 1s ) e. NN0_s ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		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 |-
2		fvelrnb	Could not format ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) Fn _om -> ( A e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) <-> E. y e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) = A ) ) : No typesetting found for |- ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) Fn _om -> ( A e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) <-> E. y e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) = A ) ) with typecode |-
3	1 2	ax-mp	Could not format ( A e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) <-> E. y e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) = A ) : No typesetting found for |- ( A e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) <-> E. y e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) = A ) with typecode |-
4		ovex	Could not format ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) +s 1s ) e. _V : No typesetting found for |- ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) +s 1s ) e. _V with typecode |-
5		eqid	Could not format ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) : No typesetting found for |- ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) with typecode |-
6		oveq1	Could not format ( z = x -> ( z +s 1s ) = ( x +s 1s ) ) : No typesetting found for |- ( z = x -> ( z +s 1s ) = ( x +s 1s ) ) with typecode |-
7		oveq1	Could not format ( z = ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) -> ( z +s 1s ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) +s 1s ) ) : No typesetting found for |- ( z = ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) -> ( z +s 1s ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) +s 1s ) ) with typecode |-
8	5 6 7	frsucmpt2	Could not format ( ( y e. _om /\ ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) +s 1s ) e. _V ) -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` suc y ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) +s 1s ) ) : No typesetting found for |- ( ( y e. _om /\ ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) +s 1s ) e. _V ) -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` suc y ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) +s 1s ) ) with typecode |-
9	4 8	mpan2	Could not format ( y e. _om -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` suc y ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) +s 1s ) ) : No typesetting found for |- ( y e. _om -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` suc y ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) +s 1s ) ) with typecode |-
10		peano2	$$⊢y\in \mathrm{\omega }\to \mathrm{suc}y\in \mathrm{\omega }$$
11		fnfvelrn	Could not format ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) Fn _om /\ suc y e. _om ) -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` suc y ) 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 /\ suc y e. _om ) -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` suc y ) e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ) with typecode |-
12	1 10 11	sylancr	Could not format ( y e. _om -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` suc y ) e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ) : No typesetting found for |- ( y e. _om -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` suc y ) e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ) with typecode |-
13		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 |-
14		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 |-
15	13 14	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 |-
16	12 15	eleqtrrdi	Could not format ( y e. _om -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` suc y ) e. NN0_s ) : No typesetting found for |- ( y e. _om -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` suc y ) e. NN0_s ) with typecode |-
17	9 16	eqeltrrd	Could not format ( y e. _om -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) +s 1s ) e. NN0_s ) : No typesetting found for |- ( y e. _om -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) +s 1s ) e. NN0_s ) with typecode |-
18		oveq1	Could not format ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) = A -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) +s 1s ) = ( A +s 1s ) ) : No typesetting found for |- ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) = A -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) +s 1s ) = ( A +s 1s ) ) with typecode |-
19	18	eleq1d	Could not format ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) = A -> ( ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) +s 1s ) e. NN0_s <-> ( A +s 1s ) e. NN0_s ) ) : No typesetting found for |- ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) = A -> ( ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) +s 1s ) e. NN0_s <-> ( A +s 1s ) e. NN0_s ) ) with typecode |-
20	17 19	syl5ibcom	Could not format ( y e. _om -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) = A -> ( A +s 1s ) e. NN0_s ) ) : No typesetting found for |- ( y e. _om -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) = A -> ( A +s 1s ) e. NN0_s ) ) with typecode |-
21	20	rexlimiv	Could not format ( E. y e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) = A -> ( A +s 1s ) e. NN0_s ) : No typesetting found for |- ( E. y e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) ` y ) = A -> ( A +s 1s ) e. NN0_s ) with typecode |-
22	3 21	sylbi	Could not format ( A e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) -> ( A +s 1s ) e. NN0_s ) : No typesetting found for |- ( A e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) |` _om ) -> ( A +s 1s ) e. NN0_s ) with typecode |-
23	22 15	eleq2s	Could not format ( A e. NN0_s -> ( A +s 1s ) e. NN0_s ) : No typesetting found for |- ( A e. NN0_s -> ( A +s 1s ) e. NN0_s ) with typecode |-