Metamath Proof Explorer

Theorem dfnns2

Description: Alternate definition of the positive surreal integers. Compare df-nn . (Contributed by Scott Fenton, 6-Aug-2025)

Ref Expression
Assertion dfnns2 
|- NN_s = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) " _om )

Proof

Step Hyp Ref Expression
1 elnns 
 |-  ( i e. NN_s <-> ( i e. NN0_s /\ i =/= 0s ) )
2 df-ne 
 |-  ( i =/= 0s <-> -. i = 0s )
3 n0s0suc 
 |-  ( i e. NN0_s -> ( i = 0s \/ E. j e. NN0_s i = ( j +s 1s ) ) )
4 3 ord 
 |-  ( i e. NN0_s -> ( -. i = 0s -> E. j e. NN0_s i = ( j +s 1s ) ) )
5 2 4 biimtrid 
 |-  ( i e. NN0_s -> ( i =/= 0s -> E. j e. NN0_s i = ( j +s 1s ) ) )
6 5 imp 
 |-  ( ( i e. NN0_s /\ i =/= 0s ) -> E. j e. NN0_s i = ( j +s 1s ) )
7 oveq1 
 |-  ( i = 0s -> ( i +s 1s ) = ( 0s +s 1s ) )
8 1sno 
 |-  1s e. No
9 addslid 
 |-  ( 1s e. No -> ( 0s +s 1s ) = 1s )
10 8 9 ax-mp 
 |-  ( 0s +s 1s ) = 1s
11 7 10 eqtrdi 
 |-  ( i = 0s -> ( i +s 1s ) = 1s )
12 11 eqeq2d 
 |-  ( i = 0s -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = ( i +s 1s ) <-> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = 1s ) )
13 12 rexbidv 
 |-  ( i = 0s -> ( E. y e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = ( i +s 1s ) <-> E. y e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = 1s ) )
14 oveq1 
 |-  ( i = k -> ( i +s 1s ) = ( k +s 1s ) )
15 14 eqeq2d 
 |-  ( i = k -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = ( i +s 1s ) <-> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = ( k +s 1s ) ) )
16 15 rexbidv 
 |-  ( i = k -> ( E. y e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = ( i +s 1s ) <-> E. y e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = ( k +s 1s ) ) )
17 oveq1 
 |-  ( i = ( k +s 1s ) -> ( i +s 1s ) = ( ( k +s 1s ) +s 1s ) )
18 17 eqeq2d 
 |-  ( i = ( k +s 1s ) -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = ( i +s 1s ) <-> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = ( ( k +s 1s ) +s 1s ) ) )
19 18 rexbidv 
 |-  ( i = ( k +s 1s ) -> ( E. y e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = ( i +s 1s ) <-> E. y e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = ( ( k +s 1s ) +s 1s ) ) )
20 fveqeq2 
 |-  ( y = z -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = ( ( k +s 1s ) +s 1s ) <-> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` z ) = ( ( k +s 1s ) +s 1s ) ) )
21 20 cbvrexvw 
 |-  ( E. y e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = ( ( k +s 1s ) +s 1s ) <-> E. z e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` z ) = ( ( k +s 1s ) +s 1s ) )
22 19 21 bitrdi 
 |-  ( i = ( k +s 1s ) -> ( E. y e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = ( i +s 1s ) <-> E. z e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` z ) = ( ( k +s 1s ) +s 1s ) ) )
23 oveq1 
 |-  ( i = j -> ( i +s 1s ) = ( j +s 1s ) )
24 23 eqeq2d 
 |-  ( i = j -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = ( i +s 1s ) <-> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = ( j +s 1s ) ) )
25 24 rexbidv 
 |-  ( i = j -> ( E. y e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = ( i +s 1s ) <-> E. y e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = ( j +s 1s ) ) )
26 peano1 
 |-  (/) e. _om
27 1nns 
 |-  1s e. NN_s
28 fr0g 
 |-  ( 1s e. NN_s -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` (/) ) = 1s )
29 27 28 ax-mp 
 |-  ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` (/) ) = 1s
30 fveqeq2 
 |-  ( y = (/) -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = 1s <-> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` (/) ) = 1s ) )
31 30 rspcev 
 |-  ( ( (/) e. _om /\ ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` (/) ) = 1s ) -> E. y e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = 1s )
32 26 29 31 mp2an 
 |-  E. y e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = 1s
33 fveqeq2 
 |-  ( z = suc y -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` z ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) +s 1s ) <-> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` suc y ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) +s 1s ) ) )
34 peano2 
 |-  ( y e. _om -> suc y e. _om )
35 ovex 
 |-  ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) +s 1s ) e. _V
36 eqid 
 |-  ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om )
37 oveq1 
 |-  ( z = x -> ( z +s 1s ) = ( x +s 1s ) )
38 oveq1 
 |-  ( z = ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) -> ( z +s 1s ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) +s 1s ) )
39 36 37 38 frsucmpt2 
 |-  ( ( y e. _om /\ ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) +s 1s ) e. _V ) -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` suc y ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) +s 1s ) )
40 35 39 mpan2 
 |-  ( y e. _om -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` suc y ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) +s 1s ) )
41 33 34 40 rspcedvdw 
 |-  ( y e. _om -> E. z e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` z ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) +s 1s ) )
42 41 adantl 
 |-  ( ( k e. NN0_s /\ y e. _om ) -> E. z e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` z ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) +s 1s ) )
43 oveq1 
 |-  ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = ( k +s 1s ) -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) +s 1s ) = ( ( k +s 1s ) +s 1s ) )
44 43 eqeq2d 
 |-  ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = ( k +s 1s ) -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` z ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) +s 1s ) <-> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` z ) = ( ( k +s 1s ) +s 1s ) ) )
45 44 rexbidv 
 |-  ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = ( k +s 1s ) -> ( E. z e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` z ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) +s 1s ) <-> E. z e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` z ) = ( ( k +s 1s ) +s 1s ) ) )
46 42 45 syl5ibcom 
 |-  ( ( k e. NN0_s /\ y e. _om ) -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = ( k +s 1s ) -> E. z e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` z ) = ( ( k +s 1s ) +s 1s ) ) )
47 46 rexlimdva 
 |-  ( k e. NN0_s -> ( E. y e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = ( k +s 1s ) -> E. z e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` z ) = ( ( k +s 1s ) +s 1s ) ) )
48 13 16 22 25 32 47 n0sind 
 |-  ( j e. NN0_s -> E. y e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = ( j +s 1s ) )
49 frfnom 
 |-  ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) Fn _om
50 fvelrnb 
 |-  ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) Fn _om -> ( ( j +s 1s ) e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) <-> E. y e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = ( j +s 1s ) ) )
51 49 50 ax-mp 
 |-  ( ( j +s 1s ) e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) <-> E. y e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` y ) = ( j +s 1s ) )
52 48 51 sylibr 
 |-  ( j e. NN0_s -> ( j +s 1s ) e. ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) )
53 df-ima 
 |-  ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) " _om ) = ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om )
54 52 53 eleqtrrdi 
 |-  ( j e. NN0_s -> ( j +s 1s ) e. ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) " _om ) )
55 eleq1 
 |-  ( i = ( j +s 1s ) -> ( i e. ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) " _om ) <-> ( j +s 1s ) e. ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) " _om ) ) )
56 54 55 syl5ibrcom 
 |-  ( j e. NN0_s -> ( i = ( j +s 1s ) -> i e. ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) " _om ) ) )
57 56 rexlimiv 
 |-  ( E. j e. NN0_s i = ( j +s 1s ) -> i e. ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) " _om ) )
58 6 57 syl 
 |-  ( ( i e. NN0_s /\ i =/= 0s ) -> i e. ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) " _om ) )
59 1 58 sylbi 
 |-  ( i e. NN_s -> i e. ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) " _om ) )
60 59 ssriv 
 |-  NN_s C_ ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) " _om )
61 fveq2 
 |-  ( k = (/) -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` k ) = ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` (/) ) )
62 61 eleq1d 
 |-  ( k = (/) -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` k ) e. NN_s <-> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` (/) ) e. NN_s ) )
63 fveq2 
 |-  ( k = j -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` k ) = ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` j ) )
64 63 eleq1d 
 |-  ( k = j -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` k ) e. NN_s <-> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` j ) e. NN_s ) )
65 fveq2 
 |-  ( k = suc j -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` k ) = ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` suc j ) )
66 65 eleq1d 
 |-  ( k = suc j -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` k ) e. NN_s <-> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` suc j ) e. NN_s ) )
67 fveq2 
 |-  ( k = i -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` k ) = ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` i ) )
68 67 eleq1d 
 |-  ( k = i -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` k ) e. NN_s <-> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` i ) e. NN_s ) )
69 29 27 eqeltri 
 |-  ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` (/) ) e. NN_s
70 peano2nns 
 |-  ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` j ) e. NN_s -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` j ) +s 1s ) e. NN_s )
71 ovex 
 |-  ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` j ) +s 1s ) e. _V
72 oveq1 
 |-  ( y = x -> ( y +s 1s ) = ( x +s 1s ) )
73 oveq1 
 |-  ( y = ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` j ) -> ( y +s 1s ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` j ) +s 1s ) )
74 36 72 73 frsucmpt2 
 |-  ( ( j e. _om /\ ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` j ) +s 1s ) e. _V ) -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` suc j ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` j ) +s 1s ) )
75 71 74 mpan2 
 |-  ( j e. _om -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` suc j ) = ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` j ) +s 1s ) )
76 75 eleq1d 
 |-  ( j e. _om -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` suc j ) e. NN_s <-> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` j ) +s 1s ) e. NN_s ) )
77 70 76 imbitrrid 
 |-  ( j e. _om -> ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` j ) e. NN_s -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` suc j ) e. NN_s ) )
78 62 64 66 68 69 77 finds 
 |-  ( i e. _om -> ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` i ) e. NN_s )
79 78 rgen 
 |-  A. i e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` i ) e. NN_s
80 fnfvrnss 
 |-  ( ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) Fn _om /\ A. i e. _om ( ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) ` i ) e. NN_s ) -> ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) C_ NN_s )
81 49 79 80 mp2an 
 |-  ran ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) |` _om ) C_ NN_s
82 53 81 eqsstri 
 |-  ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) " _om ) C_ NN_s
83 60 82 eqssi 
 |-  NN_s = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 1s ) " _om )