Metamath Proof Explorer

Theorem peano5n0s

Description: Peano's inductive postulate for non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025)

Ref Expression
Assertion peano5n0s Could not format assertion : No typesetting found for |- ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> NN0_s C_ A ) with typecode |-

Proof

Step Hyp Ref Expression
1 df-n0s Could not format NN0_s = ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) " _om ) : No typesetting found for |- NN0_s = ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) " _om ) with typecode |-
2 df-ima Could not format ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) " _om ) = ran ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) : No typesetting found for |- ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) " _om ) = ran ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) with typecode |-
3 1 2 eqtri Could not format NN0_s = ran ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) : No typesetting found for |- NN0_s = ran ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) with typecode |-
4 frfnom Could not format ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) Fn _om : No typesetting found for |- ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) Fn _om with typecode |-
5 4 a1i Could not format ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) Fn _om ) : No typesetting found for |- ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) Fn _om ) with typecode |-
6 fveq2 Could not format ( y = (/) -> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` y ) = ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` (/) ) ) : No typesetting found for |- ( y = (/) -> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` y ) = ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` (/) ) ) with typecode |-
7 6 eleq1d Could not format ( y = (/) -> ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` y ) e. A <-> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` (/) ) e. A ) ) : No typesetting found for |- ( y = (/) -> ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` y ) e. A <-> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` (/) ) e. A ) ) with typecode |-
8 fveq2 Could not format ( y = z -> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` y ) = ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) ) : No typesetting found for |- ( y = z -> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` y ) = ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) ) with typecode |-
9 8 eleq1d Could not format ( y = z -> ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` y ) e. A <-> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) e. A ) ) : No typesetting found for |- ( y = z -> ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` y ) e. A <-> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) e. A ) ) with typecode |-
10 fveq2 Could not format ( y = suc z -> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` y ) = ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` suc z ) ) : No typesetting found for |- ( y = suc z -> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` y ) = ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` suc z ) ) with typecode |-
11 10 eleq1d Could not format ( y = suc z -> ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` y ) e. A <-> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` suc z ) e. A ) ) : No typesetting found for |- ( y = suc z -> ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` y ) e. A <-> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` suc z ) e. A ) ) with typecode |-
12 fr0g Could not format ( 0s e. A -> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` (/) ) = 0s ) : No typesetting found for |- ( 0s e. A -> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` (/) ) = 0s ) with typecode |-
13 id Could not format ( 0s e. A -> 0s e. A ) : No typesetting found for |- ( 0s e. A -> 0s e. A ) with typecode |-
14 12 13 eqeltrd Could not format ( 0s e. A -> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` (/) ) e. A ) : No typesetting found for |- ( 0s e. A -> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` (/) ) e. A ) with typecode |-
15 14 adantr Could not format ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` (/) ) e. A ) : No typesetting found for |- ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` (/) ) e. A ) with typecode |-
16 oveq1 Could not format ( x = ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) -> ( x +s 1s ) = ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) +s 1s ) ) : No typesetting found for |- ( x = ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) -> ( x +s 1s ) = ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) +s 1s ) ) with typecode |-
17 16 eleq1d Could not format ( x = ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) -> ( ( x +s 1s ) e. A <-> ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) +s 1s ) e. A ) ) : No typesetting found for |- ( x = ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) -> ( ( x +s 1s ) e. A <-> ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) +s 1s ) e. A ) ) with typecode |-
18 17 rspccv Could not format ( A. x e. A ( x +s 1s ) e. A -> ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) e. A -> ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) +s 1s ) e. A ) ) : No typesetting found for |- ( A. x e. A ( x +s 1s ) e. A -> ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) e. A -> ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) +s 1s ) e. A ) ) with typecode |-
19 18 adantl Could not format ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) e. A -> ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) +s 1s ) e. A ) ) : No typesetting found for |- ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) e. A -> ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) +s 1s ) e. A ) ) with typecode |-
20 19 imp Could not format ( ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) /\ ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) e. A ) -> ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) +s 1s ) e. A ) : No typesetting found for |- ( ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) /\ ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) e. A ) -> ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) +s 1s ) e. A ) with typecode |-
21 ovex Could not format ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) +s 1s ) e. _V : No typesetting found for |- ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) +s 1s ) e. _V with typecode |-
22 eqid Could not format ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) = ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) : No typesetting found for |- ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) = ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) with typecode |-
23 oveq1 Could not format ( y = n -> ( y +s 1s ) = ( n +s 1s ) ) : No typesetting found for |- ( y = n -> ( y +s 1s ) = ( n +s 1s ) ) with typecode |-
24 oveq1 Could not format ( y = ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) -> ( y +s 1s ) = ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) +s 1s ) ) : No typesetting found for |- ( y = ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) -> ( y +s 1s ) = ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) +s 1s ) ) with typecode |-
25 22 23 24 frsucmpt2 Could not format ( ( z e. _om /\ ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) +s 1s ) e. _V ) -> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` suc z ) = ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) +s 1s ) ) : No typesetting found for |- ( ( z e. _om /\ ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) +s 1s ) e. _V ) -> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` suc z ) = ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) +s 1s ) ) with typecode |-
26 21 25 mpan2 Could not format ( z e. _om -> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` suc z ) = ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) +s 1s ) ) : No typesetting found for |- ( z e. _om -> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` suc z ) = ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) +s 1s ) ) with typecode |-
27 26 eleq1d Could not format ( z e. _om -> ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` suc z ) e. A <-> ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) +s 1s ) e. A ) ) : No typesetting found for |- ( z e. _om -> ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` suc z ) e. A <-> ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) +s 1s ) e. A ) ) with typecode |-
28 20 27 imbitrrid Could not format ( z e. _om -> ( ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) /\ ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) e. A ) -> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` suc z ) e. A ) ) : No typesetting found for |- ( z e. _om -> ( ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) /\ ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) e. A ) -> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` suc z ) e. A ) ) with typecode |-
29 28 expd Could not format ( z e. _om -> ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) e. A -> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` suc z ) e. A ) ) ) : No typesetting found for |- ( z e. _om -> ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> ( ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` z ) e. A -> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` suc z ) e. A ) ) ) with typecode |-
30 7 9 11 15 29 finds2 Could not format ( y e. _om -> ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` y ) e. A ) ) : No typesetting found for |- ( y e. _om -> ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` y ) e. A ) ) with typecode |-
31 30 com12 Could not format ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> ( y e. _om -> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` y ) e. A ) ) : No typesetting found for |- ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> ( y e. _om -> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` y ) e. A ) ) with typecode |-
32 31 ralrimiv Could not format ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> A. y e. _om ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` y ) e. A ) : No typesetting found for |- ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> A. y e. _om ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` y ) e. A ) with typecode |-
33 ffnfv Could not format ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) : _om --> A <-> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) Fn _om /\ A. y e. _om ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` y ) e. A ) ) : No typesetting found for |- ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) : _om --> A <-> ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) Fn _om /\ A. y e. _om ( ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) ` y ) e. A ) ) with typecode |-
34 5 32 33 sylanbrc Could not format ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) : _om --> A ) : No typesetting found for |- ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) : _om --> A ) with typecode |-
35 34 frnd Could not format ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> ran ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) C_ A ) : No typesetting found for |- ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> ran ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) |` _om ) C_ A ) with typecode |-
36 3 35 eqsstrid Could not format ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> NN0_s C_ A ) : No typesetting found for |- ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> NN0_s C_ A ) with typecode |-