Metamath Proof Explorer

Theorem peano5uzs

Description: Peano's inductive postulate for upper surreal integers. (Contributed by Scott Fenton, 25-Jul-2025)

Ref Expression
Hypotheses peano5uzs.1 
|- ( ph -> N e. ZZ_s )
peano5uzs.2 
|- ( ph -> N e. A )
peano5uzs.3 
|- ( ( ph /\ x e. A ) -> ( x +s 1s ) e. A )
Assertion peano5uzs 
|- ( ph -> { k e. ZZ_s | N <_s k } C_ A )

Proof

Step Hyp Ref Expression
1 peano5uzs.1 
 |-  ( ph -> N e. ZZ_s )
2 peano5uzs.2 
 |-  ( ph -> N e. A )
3 peano5uzs.3 
 |-  ( ( ph /\ x e. A ) -> ( x +s 1s ) e. A )
4 breq2 
 |-  ( k = n -> ( N <_s k <-> N <_s n ) )
5 4 elrab 
 |-  ( n e. { k e. ZZ_s | N <_s k } <-> ( n e. ZZ_s /\ N <_s n ) )
6 zno 
 |-  ( n e. ZZ_s -> n e. No )
7 6 adantr 
 |-  ( ( n e. ZZ_s /\ N <_s n ) -> n e. No )
8 1 znod 
 |-  ( ph -> N e. No )
9 npcans 
 |-  ( ( n e. No /\ N e. No ) -> ( ( n -s N ) +s N ) = n )
10 7 8 9 syl2anr 
 |-  ( ( ph /\ ( n e. ZZ_s /\ N <_s n ) ) -> ( ( n -s N ) +s N ) = n )
11 simprl 
 |-  ( ( ph /\ ( n e. ZZ_s /\ N <_s n ) ) -> n e. ZZ_s )
12 1 adantr 
 |-  ( ( ph /\ ( n e. ZZ_s /\ N <_s n ) ) -> N e. ZZ_s )
13 11 12 zsubscld 
 |-  ( ( ph /\ ( n e. ZZ_s /\ N <_s n ) ) -> ( n -s N ) e. ZZ_s )
14 6 adantl 
 |-  ( ( ph /\ n e. ZZ_s ) -> n e. No )
15 8 adantr 
 |-  ( ( ph /\ n e. ZZ_s ) -> N e. No )
16 14 15 subsge0d 
 |-  ( ( ph /\ n e. ZZ_s ) -> ( 0s <_s ( n -s N ) <-> N <_s n ) )
17 16 biimpar 
 |-  ( ( ( ph /\ n e. ZZ_s ) /\ N <_s n ) -> 0s <_s ( n -s N ) )
18 17 anasss 
 |-  ( ( ph /\ ( n e. ZZ_s /\ N <_s n ) ) -> 0s <_s ( n -s N ) )
19 13 18 jca 
 |-  ( ( ph /\ ( n e. ZZ_s /\ N <_s n ) ) -> ( ( n -s N ) e. ZZ_s /\ 0s <_s ( n -s N ) ) )
20 eln0zs 
 |-  ( ( n -s N ) e. NN0_s <-> ( ( n -s N ) e. ZZ_s /\ 0s <_s ( n -s N ) ) )
21 19 20 sylibr 
 |-  ( ( ph /\ ( n e. ZZ_s /\ N <_s n ) ) -> ( n -s N ) e. NN0_s )
22 21 ex 
 |-  ( ph -> ( ( n e. ZZ_s /\ N <_s n ) -> ( n -s N ) e. NN0_s ) )
23 oveq1 
 |-  ( z = 0s -> ( z +s N ) = ( 0s +s N ) )
24 23 eleq1d 
 |-  ( z = 0s -> ( ( z +s N ) e. A <-> ( 0s +s N ) e. A ) )
25 24 imbi2d 
 |-  ( z = 0s -> ( ( ph -> ( z +s N ) e. A ) <-> ( ph -> ( 0s +s N ) e. A ) ) )
26 oveq1 
 |-  ( z = y -> ( z +s N ) = ( y +s N ) )
27 26 eleq1d 
 |-  ( z = y -> ( ( z +s N ) e. A <-> ( y +s N ) e. A ) )
28 27 imbi2d 
 |-  ( z = y -> ( ( ph -> ( z +s N ) e. A ) <-> ( ph -> ( y +s N ) e. A ) ) )
29 oveq1 
 |-  ( z = ( y +s 1s ) -> ( z +s N ) = ( ( y +s 1s ) +s N ) )
30 29 eleq1d 
 |-  ( z = ( y +s 1s ) -> ( ( z +s N ) e. A <-> ( ( y +s 1s ) +s N ) e. A ) )
31 30 imbi2d 
 |-  ( z = ( y +s 1s ) -> ( ( ph -> ( z +s N ) e. A ) <-> ( ph -> ( ( y +s 1s ) +s N ) e. A ) ) )
32 oveq1 
 |-  ( z = ( n -s N ) -> ( z +s N ) = ( ( n -s N ) +s N ) )
33 32 eleq1d 
 |-  ( z = ( n -s N ) -> ( ( z +s N ) e. A <-> ( ( n -s N ) +s N ) e. A ) )
34 33 imbi2d 
 |-  ( z = ( n -s N ) -> ( ( ph -> ( z +s N ) e. A ) <-> ( ph -> ( ( n -s N ) +s N ) e. A ) ) )
35 addslid 
 |-  ( N e. No -> ( 0s +s N ) = N )
36 8 35 syl 
 |-  ( ph -> ( 0s +s N ) = N )
37 36 2 eqeltrd 
 |-  ( ph -> ( 0s +s N ) e. A )
38 3 ralrimiva 
 |-  ( ph -> A. x e. A ( x +s 1s ) e. A )
39 oveq1 
 |-  ( x = ( y +s N ) -> ( x +s 1s ) = ( ( y +s N ) +s 1s ) )
40 39 eleq1d 
 |-  ( x = ( y +s N ) -> ( ( x +s 1s ) e. A <-> ( ( y +s N ) +s 1s ) e. A ) )
41 40 rspccv 
 |-  ( A. x e. A ( x +s 1s ) e. A -> ( ( y +s N ) e. A -> ( ( y +s N ) +s 1s ) e. A ) )
42 38 41 syl 
 |-  ( ph -> ( ( y +s N ) e. A -> ( ( y +s N ) +s 1s ) e. A ) )
43 42 adantl 
 |-  ( ( y e. NN0_s /\ ph ) -> ( ( y +s N ) e. A -> ( ( y +s N ) +s 1s ) e. A ) )
44 n0sno 
 |-  ( y e. NN0_s -> y e. No )
45 44 adantr 
 |-  ( ( y e. NN0_s /\ ph ) -> y e. No )
46 1sno 
 |-  1s e. No
47 46 a1i 
 |-  ( ( y e. NN0_s /\ ph ) -> 1s e. No )
48 8 adantl 
 |-  ( ( y e. NN0_s /\ ph ) -> N e. No )
49 45 47 48 adds32d 
 |-  ( ( y e. NN0_s /\ ph ) -> ( ( y +s 1s ) +s N ) = ( ( y +s N ) +s 1s ) )
50 49 eleq1d 
 |-  ( ( y e. NN0_s /\ ph ) -> ( ( ( y +s 1s ) +s N ) e. A <-> ( ( y +s N ) +s 1s ) e. A ) )
51 43 50 sylibrd 
 |-  ( ( y e. NN0_s /\ ph ) -> ( ( y +s N ) e. A -> ( ( y +s 1s ) +s N ) e. A ) )
52 51 ex 
 |-  ( y e. NN0_s -> ( ph -> ( ( y +s N ) e. A -> ( ( y +s 1s ) +s N ) e. A ) ) )
53 52 a2d 
 |-  ( y e. NN0_s -> ( ( ph -> ( y +s N ) e. A ) -> ( ph -> ( ( y +s 1s ) +s N ) e. A ) ) )
54 25 28 31 34 37 53 n0sind 
 |-  ( ( n -s N ) e. NN0_s -> ( ph -> ( ( n -s N ) +s N ) e. A ) )
55 54 com12 
 |-  ( ph -> ( ( n -s N ) e. NN0_s -> ( ( n -s N ) +s N ) e. A ) )
56 22 55 syld 
 |-  ( ph -> ( ( n e. ZZ_s /\ N <_s n ) -> ( ( n -s N ) +s N ) e. A ) )
57 56 imp 
 |-  ( ( ph /\ ( n e. ZZ_s /\ N <_s n ) ) -> ( ( n -s N ) +s N ) e. A )
58 10 57 eqeltrrd 
 |-  ( ( ph /\ ( n e. ZZ_s /\ N <_s n ) ) -> n e. A )
59 58 ex 
 |-  ( ph -> ( ( n e. ZZ_s /\ N <_s n ) -> n e. A ) )
60 5 59 biimtrid 
 |-  ( ph -> ( n e. { k e. ZZ_s | N <_s k } -> n e. A ) )
61 60 ssrdv 
 |-  ( ph -> { k e. ZZ_s | N <_s k } C_ A )