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 ⊢ ( 𝜑 → 𝑁 ∈ ℤs )
peano5uzs.2 ⊢ ( 𝜑 → 𝑁 ∈ 𝐴 )
peano5uzs.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 +s 1s ) ∈ 𝐴 )
Assertion peano5uzs ( 𝜑 → { 𝑘 ∈ ℤs ∣ 𝑁 ≤s 𝑘 } ⊆ 𝐴 )

Proof

Step Hyp Ref Expression
1 peano5uzs.1 ⊢ ( 𝜑 → 𝑁 ∈ ℤs )
2 peano5uzs.2 ⊢ ( 𝜑 → 𝑁 ∈ 𝐴 )
3 peano5uzs.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 +s 1s ) ∈ 𝐴 )
4 breq2 ⊢ ( 𝑘 = 𝑛 → ( 𝑁 ≤s 𝑘 ↔ 𝑁 ≤s 𝑛 ) )
5 4 elrab ⊢ ( 𝑛 ∈ { 𝑘 ∈ ℤs ∣ 𝑁 ≤s 𝑘 } ↔ ( 𝑛 ∈ ℤs ∧ 𝑁 ≤s 𝑛 ) )
6 zno ⊢ ( 𝑛 ∈ ℤs → 𝑛 ∈ No )
7 6 adantr ⊢ ( ( 𝑛 ∈ ℤs ∧ 𝑁 ≤s 𝑛 ) → 𝑛 ∈ No )
8 1 znod ⊢ ( 𝜑 → 𝑁 ∈ No )
9 npcans ⊢ ( ( 𝑛 ∈ No ∧ 𝑁 ∈ No ) → ( ( 𝑛 -s 𝑁 ) +s 𝑁 ) = 𝑛 )
10 7 8 9 syl2anr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℤs ∧ 𝑁 ≤s 𝑛 ) ) → ( ( 𝑛 -s 𝑁 ) +s 𝑁 ) = 𝑛 )
11 simprl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℤs ∧ 𝑁 ≤s 𝑛 ) ) → 𝑛 ∈ ℤs )
12 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℤs ∧ 𝑁 ≤s 𝑛 ) ) → 𝑁 ∈ ℤs )
13 11 12 zsubscld ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℤs ∧ 𝑁 ≤s 𝑛 ) ) → ( 𝑛 -s 𝑁 ) ∈ ℤs )
14 6 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℤs ) → 𝑛 ∈ No )
15 8 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℤs ) → 𝑁 ∈ No )
16 14 15 subsge0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℤs ) → ( 0s ≤s ( 𝑛 -s 𝑁 ) ↔ 𝑁 ≤s 𝑛 ) )
17 16 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℤs ) ∧ 𝑁 ≤s 𝑛 ) → 0s ≤s ( 𝑛 -s 𝑁 ) )
18 17 anasss ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℤs ∧ 𝑁 ≤s 𝑛 ) ) → 0s ≤s ( 𝑛 -s 𝑁 ) )
19 13 18 jca ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℤs ∧ 𝑁 ≤s 𝑛 ) ) → ( ( 𝑛 -s 𝑁 ) ∈ ℤs ∧ 0s ≤s ( 𝑛 -s 𝑁 ) ) )
20 eln0zs ⊢ ( ( 𝑛 -s 𝑁 ) ∈ ℕ0s ↔ ( ( 𝑛 -s 𝑁 ) ∈ ℤs ∧ 0s ≤s ( 𝑛 -s 𝑁 ) ) )
21 19 20 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℤs ∧ 𝑁 ≤s 𝑛 ) ) → ( 𝑛 -s 𝑁 ) ∈ ℕ0s )
22 21 ex ⊢ ( 𝜑 → ( ( 𝑛 ∈ ℤs ∧ 𝑁 ≤s 𝑛 ) → ( 𝑛 -s 𝑁 ) ∈ ℕ0s ) )
23 oveq1 ⊢ ( 𝑧 = 0s → ( 𝑧 +s 𝑁 ) = ( 0s +s 𝑁 ) )
24 23 eleq1d ⊢ ( 𝑧 = 0s → ( ( 𝑧 +s 𝑁 ) ∈ 𝐴 ↔ ( 0s +s 𝑁 ) ∈ 𝐴 ) )
25 24 imbi2d ⊢ ( 𝑧 = 0s → ( ( 𝜑 → ( 𝑧 +s 𝑁 ) ∈ 𝐴 ) ↔ ( 𝜑 → ( 0s +s 𝑁 ) ∈ 𝐴 ) ) )
26 oveq1 ⊢ ( 𝑧 = 𝑦 → ( 𝑧 +s 𝑁 ) = ( 𝑦 +s 𝑁 ) )
27 26 eleq1d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 +s 𝑁 ) ∈ 𝐴 ↔ ( 𝑦 +s 𝑁 ) ∈ 𝐴 ) )
28 27 imbi2d ⊢ ( 𝑧 = 𝑦 → ( ( 𝜑 → ( 𝑧 +s 𝑁 ) ∈ 𝐴 ) ↔ ( 𝜑 → ( 𝑦 +s 𝑁 ) ∈ 𝐴 ) ) )
29 oveq1 ⊢ ( 𝑧 = ( 𝑦 +s 1s ) → ( 𝑧 +s 𝑁 ) = ( ( 𝑦 +s 1s ) +s 𝑁 ) )
30 29 eleq1d ⊢ ( 𝑧 = ( 𝑦 +s 1s ) → ( ( 𝑧 +s 𝑁 ) ∈ 𝐴 ↔ ( ( 𝑦 +s 1s ) +s 𝑁 ) ∈ 𝐴 ) )
31 30 imbi2d ⊢ ( 𝑧 = ( 𝑦 +s 1s ) → ( ( 𝜑 → ( 𝑧 +s 𝑁 ) ∈ 𝐴 ) ↔ ( 𝜑 → ( ( 𝑦 +s 1s ) +s 𝑁 ) ∈ 𝐴 ) ) )
32 oveq1 ⊢ ( 𝑧 = ( 𝑛 -s 𝑁 ) → ( 𝑧 +s 𝑁 ) = ( ( 𝑛 -s 𝑁 ) +s 𝑁 ) )
33 32 eleq1d ⊢ ( 𝑧 = ( 𝑛 -s 𝑁 ) → ( ( 𝑧 +s 𝑁 ) ∈ 𝐴 ↔ ( ( 𝑛 -s 𝑁 ) +s 𝑁 ) ∈ 𝐴 ) )
34 33 imbi2d ⊢ ( 𝑧 = ( 𝑛 -s 𝑁 ) → ( ( 𝜑 → ( 𝑧 +s 𝑁 ) ∈ 𝐴 ) ↔ ( 𝜑 → ( ( 𝑛 -s 𝑁 ) +s 𝑁 ) ∈ 𝐴 ) ) )
35 addslid ⊢ ( 𝑁 ∈ No → ( 0s +s 𝑁 ) = 𝑁 )
36 8 35 syl ⊢ ( 𝜑 → ( 0s +s 𝑁 ) = 𝑁 )
37 36 2 eqeltrd ⊢ ( 𝜑 → ( 0s +s 𝑁 ) ∈ 𝐴 )
38 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝑥 +s 1s ) ∈ 𝐴 )
39 oveq1 ⊢ ( 𝑥 = ( 𝑦 +s 𝑁 ) → ( 𝑥 +s 1s ) = ( ( 𝑦 +s 𝑁 ) +s 1s ) )
40 39 eleq1d ⊢ ( 𝑥 = ( 𝑦 +s 𝑁 ) → ( ( 𝑥 +s 1s ) ∈ 𝐴 ↔ ( ( 𝑦 +s 𝑁 ) +s 1s ) ∈ 𝐴 ) )
41 40 rspccv ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 +s 1s ) ∈ 𝐴 → ( ( 𝑦 +s 𝑁 ) ∈ 𝐴 → ( ( 𝑦 +s 𝑁 ) +s 1s ) ∈ 𝐴 ) )
42 38 41 syl ⊢ ( 𝜑 → ( ( 𝑦 +s 𝑁 ) ∈ 𝐴 → ( ( 𝑦 +s 𝑁 ) +s 1s ) ∈ 𝐴 ) )
43 42 adantl ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( ( 𝑦 +s 𝑁 ) ∈ 𝐴 → ( ( 𝑦 +s 𝑁 ) +s 1s ) ∈ 𝐴 ) )
44 n0no ⊢ ( 𝑦 ∈ ℕ0s → 𝑦 ∈ No )
45 44 adantr ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → 𝑦 ∈ No )
46 1no ⊢ 1s ∈ No
47 46 a1i ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → 1s ∈ No )
48 8 adantl ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → 𝑁 ∈ No )
49 45 47 48 adds32d ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( ( 𝑦 +s 1s ) +s 𝑁 ) = ( ( 𝑦 +s 𝑁 ) +s 1s ) )
50 49 eleq1d ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( ( ( 𝑦 +s 1s ) +s 𝑁 ) ∈ 𝐴 ↔ ( ( 𝑦 +s 𝑁 ) +s 1s ) ∈ 𝐴 ) )
51 43 50 sylibrd ⊢ ( ( 𝑦 ∈ ℕ0s ∧ 𝜑 ) → ( ( 𝑦 +s 𝑁 ) ∈ 𝐴 → ( ( 𝑦 +s 1s ) +s 𝑁 ) ∈ 𝐴 ) )
52 51 ex ⊢ ( 𝑦 ∈ ℕ0s → ( 𝜑 → ( ( 𝑦 +s 𝑁 ) ∈ 𝐴 → ( ( 𝑦 +s 1s ) +s 𝑁 ) ∈ 𝐴 ) ) )
53 52 a2d ⊢ ( 𝑦 ∈ ℕ0s → ( ( 𝜑 → ( 𝑦 +s 𝑁 ) ∈ 𝐴 ) → ( 𝜑 → ( ( 𝑦 +s 1s ) +s 𝑁 ) ∈ 𝐴 ) ) )
54 25 28 31 34 37 53 n0sind ⊢ ( ( 𝑛 -s 𝑁 ) ∈ ℕ0s → ( 𝜑 → ( ( 𝑛 -s 𝑁 ) +s 𝑁 ) ∈ 𝐴 ) )
55 54 com12 ⊢ ( 𝜑 → ( ( 𝑛 -s 𝑁 ) ∈ ℕ0s → ( ( 𝑛 -s 𝑁 ) +s 𝑁 ) ∈ 𝐴 ) )
56 22 55 syld ⊢ ( 𝜑 → ( ( 𝑛 ∈ ℤs ∧ 𝑁 ≤s 𝑛 ) → ( ( 𝑛 -s 𝑁 ) +s 𝑁 ) ∈ 𝐴 ) )
57 56 imp ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℤs ∧ 𝑁 ≤s 𝑛 ) ) → ( ( 𝑛 -s 𝑁 ) +s 𝑁 ) ∈ 𝐴 )
58 10 57 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℤs ∧ 𝑁 ≤s 𝑛 ) ) → 𝑛 ∈ 𝐴 )
59 58 ex ⊢ ( 𝜑 → ( ( 𝑛 ∈ ℤs ∧ 𝑁 ≤s 𝑛 ) → 𝑛 ∈ 𝐴 ) )
60 5 59 biimtrid ⊢ ( 𝜑 → ( 𝑛 ∈ { 𝑘 ∈ ℤs ∣ 𝑁 ≤s 𝑘 } → 𝑛 ∈ 𝐴 ) )
61 60 ssrdv ⊢ ( 𝜑 → { 𝑘 ∈ ℤs ∣ 𝑁 ≤s 𝑘 } ⊆ 𝐴 )