Metamath Proof Explorer

Theorem uzsind

Description: Induction on the upper surreal integers that start at M . (Contributed by Scott Fenton, 25-Jul-2025)

Ref Expression
Hypotheses uzsind.1 ⊢ ( 𝑗 = 𝑀 → ( 𝜑 ↔ 𝜓 ) )
uzsind.2 ⊢ ( 𝑗 = 𝑘 → ( 𝜑 ↔ 𝜒 ) )
uzsind.3 ⊢ ( 𝑗 = ( 𝑘 +s 1s ) → ( 𝜑 ↔ 𝜃 ) )
uzsind.4 ⊢ ( 𝑗 = 𝑁 → ( 𝜑 ↔ 𝜏 ) )
uzsind.5 ⊢ ( 𝑀 ∈ ℤs → 𝜓 )
uzsind.6 ⊢ ( ( 𝑀 ∈ ℤs ∧ 𝑘 ∈ ℤs ∧ 𝑀 ≤s 𝑘 ) → ( 𝜒 → 𝜃 ) )
Assertion uzsind ( ( 𝑀 ∈ ℤs ∧ 𝑁 ∈ ℤs ∧ 𝑀 ≤s 𝑁 ) → 𝜏 )

Proof

Step Hyp Ref Expression
1 uzsind.1 ⊢ ( 𝑗 = 𝑀 → ( 𝜑 ↔ 𝜓 ) )
2 uzsind.2 ⊢ ( 𝑗 = 𝑘 → ( 𝜑 ↔ 𝜒 ) )
3 uzsind.3 ⊢ ( 𝑗 = ( 𝑘 +s 1s ) → ( 𝜑 ↔ 𝜃 ) )
4 uzsind.4 ⊢ ( 𝑗 = 𝑁 → ( 𝜑 ↔ 𝜏 ) )
5 uzsind.5 ⊢ ( 𝑀 ∈ ℤs → 𝜓 )
6 uzsind.6 ⊢ ( ( 𝑀 ∈ ℤs ∧ 𝑘 ∈ ℤs ∧ 𝑀 ≤s 𝑘 ) → ( 𝜒 → 𝜃 ) )
7 id ⊢ ( 𝑀 ∈ ℤs → 𝑀 ∈ ℤs )
8 zno ⊢ ( 𝑀 ∈ ℤs → 𝑀 ∈ No )
9 lesid ⊢ ( 𝑀 ∈ No → 𝑀 ≤s 𝑀 )
10 8 9 syl ⊢ ( 𝑀 ∈ ℤs → 𝑀 ≤s 𝑀 )
11 7 10 5 jca32 ⊢ ( 𝑀 ∈ ℤs → ( 𝑀 ∈ ℤs ∧ ( 𝑀 ≤s 𝑀 ∧ 𝜓 ) ) )
12 breq2 ⊢ ( 𝑗 = 𝑀 → ( 𝑀 ≤s 𝑗 ↔ 𝑀 ≤s 𝑀 ) )
13 12 1 anbi12d ⊢ ( 𝑗 = 𝑀 → ( ( 𝑀 ≤s 𝑗 ∧ 𝜑 ) ↔ ( 𝑀 ≤s 𝑀 ∧ 𝜓 ) ) )
14 13 elrab ⊢ ( 𝑀 ∈ { 𝑗 ∈ ℤs ∣ ( 𝑀 ≤s 𝑗 ∧ 𝜑 ) } ↔ ( 𝑀 ∈ ℤs ∧ ( 𝑀 ≤s 𝑀 ∧ 𝜓 ) ) )
15 11 14 sylibr ⊢ ( 𝑀 ∈ ℤs → 𝑀 ∈ { 𝑗 ∈ ℤs ∣ ( 𝑀 ≤s 𝑗 ∧ 𝜑 ) } )
16 simpl ⊢ ( ( 𝑀 ∈ ℤs ∧ ( 𝑘 ∈ ℤs ∧ ( 𝑀 ≤s 𝑘 ∧ 𝜒 ) ) ) → 𝑀 ∈ ℤs )
17 simprl ⊢ ( ( 𝑀 ∈ ℤs ∧ ( 𝑘 ∈ ℤs ∧ ( 𝑀 ≤s 𝑘 ∧ 𝜒 ) ) ) → 𝑘 ∈ ℤs )
18 simprrl ⊢ ( ( 𝑀 ∈ ℤs ∧ ( 𝑘 ∈ ℤs ∧ ( 𝑀 ≤s 𝑘 ∧ 𝜒 ) ) ) → 𝑀 ≤s 𝑘 )
19 simprrr ⊢ ( ( 𝑀 ∈ ℤs ∧ ( 𝑘 ∈ ℤs ∧ ( 𝑀 ≤s 𝑘 ∧ 𝜒 ) ) ) → 𝜒 )
20 id ⊢ ( 𝑘 ∈ ℤs → 𝑘 ∈ ℤs )
21 1zs ⊢ 1s ∈ ℤs
22 21 a1i ⊢ ( 𝑘 ∈ ℤs → 1s ∈ ℤs )
23 20 22 zaddscld ⊢ ( 𝑘 ∈ ℤs → ( 𝑘 +s 1s ) ∈ ℤs )
24 23 3ad2ant2 ⊢ ( ( 𝑀 ∈ ℤs ∧ 𝑘 ∈ ℤs ∧ 𝑀 ≤s 𝑘 ) → ( 𝑘 +s 1s ) ∈ ℤs )
25 24 adantr ⊢ ( ( ( 𝑀 ∈ ℤs ∧ 𝑘 ∈ ℤs ∧ 𝑀 ≤s 𝑘 ) ∧ 𝜒 ) → ( 𝑘 +s 1s ) ∈ ℤs )
26 8 3ad2ant1 ⊢ ( ( 𝑀 ∈ ℤs ∧ 𝑘 ∈ ℤs ∧ 𝑀 ≤s 𝑘 ) → 𝑀 ∈ No )
27 23 znod ⊢ ( 𝑘 ∈ ℤs → ( 𝑘 +s 1s ) ∈ No )
28 27 3ad2ant2 ⊢ ( ( 𝑀 ∈ ℤs ∧ 𝑘 ∈ ℤs ∧ 𝑀 ≤s 𝑘 ) → ( 𝑘 +s 1s ) ∈ No )
29 zno ⊢ ( 𝑘 ∈ ℤs → 𝑘 ∈ No )
30 29 3ad2ant2 ⊢ ( ( 𝑀 ∈ ℤs ∧ 𝑘 ∈ ℤs ∧ 𝑀 ≤s 𝑘 ) → 𝑘 ∈ No )
31 simp3 ⊢ ( ( 𝑀 ∈ ℤs ∧ 𝑘 ∈ ℤs ∧ 𝑀 ≤s 𝑘 ) → 𝑀 ≤s 𝑘 )
32 29 ltsp1d ⊢ ( 𝑘 ∈ ℤs → 𝑘 <s ( 𝑘 +s 1s ) )
33 32 3ad2ant2 ⊢ ( ( 𝑀 ∈ ℤs ∧ 𝑘 ∈ ℤs ∧ 𝑀 ≤s 𝑘 ) → 𝑘 <s ( 𝑘 +s 1s ) )
34 26 30 28 31 33 leltstrd ⊢ ( ( 𝑀 ∈ ℤs ∧ 𝑘 ∈ ℤs ∧ 𝑀 ≤s 𝑘 ) → 𝑀 <s ( 𝑘 +s 1s ) )
35 26 28 34 ltlesd ⊢ ( ( 𝑀 ∈ ℤs ∧ 𝑘 ∈ ℤs ∧ 𝑀 ≤s 𝑘 ) → 𝑀 ≤s ( 𝑘 +s 1s ) )
36 35 adantr ⊢ ( ( ( 𝑀 ∈ ℤs ∧ 𝑘 ∈ ℤs ∧ 𝑀 ≤s 𝑘 ) ∧ 𝜒 ) → 𝑀 ≤s ( 𝑘 +s 1s ) )
37 6 imp ⊢ ( ( ( 𝑀 ∈ ℤs ∧ 𝑘 ∈ ℤs ∧ 𝑀 ≤s 𝑘 ) ∧ 𝜒 ) → 𝜃 )
38 25 36 37 jca32 ⊢ ( ( ( 𝑀 ∈ ℤs ∧ 𝑘 ∈ ℤs ∧ 𝑀 ≤s 𝑘 ) ∧ 𝜒 ) → ( ( 𝑘 +s 1s ) ∈ ℤs ∧ ( 𝑀 ≤s ( 𝑘 +s 1s ) ∧ 𝜃 ) ) )
39 16 17 18 19 38 syl31anc ⊢ ( ( 𝑀 ∈ ℤs ∧ ( 𝑘 ∈ ℤs ∧ ( 𝑀 ≤s 𝑘 ∧ 𝜒 ) ) ) → ( ( 𝑘 +s 1s ) ∈ ℤs ∧ ( 𝑀 ≤s ( 𝑘 +s 1s ) ∧ 𝜃 ) ) )
40 breq2 ⊢ ( 𝑗 = 𝑘 → ( 𝑀 ≤s 𝑗 ↔ 𝑀 ≤s 𝑘 ) )
41 40 2 anbi12d ⊢ ( 𝑗 = 𝑘 → ( ( 𝑀 ≤s 𝑗 ∧ 𝜑 ) ↔ ( 𝑀 ≤s 𝑘 ∧ 𝜒 ) ) )
42 41 elrab ⊢ ( 𝑘 ∈ { 𝑗 ∈ ℤs ∣ ( 𝑀 ≤s 𝑗 ∧ 𝜑 ) } ↔ ( 𝑘 ∈ ℤs ∧ ( 𝑀 ≤s 𝑘 ∧ 𝜒 ) ) )
43 42 anbi2i ⊢ ( ( 𝑀 ∈ ℤs ∧ 𝑘 ∈ { 𝑗 ∈ ℤs ∣ ( 𝑀 ≤s 𝑗 ∧ 𝜑 ) } ) ↔ ( 𝑀 ∈ ℤs ∧ ( 𝑘 ∈ ℤs ∧ ( 𝑀 ≤s 𝑘 ∧ 𝜒 ) ) ) )
44 breq2 ⊢ ( 𝑗 = ( 𝑘 +s 1s ) → ( 𝑀 ≤s 𝑗 ↔ 𝑀 ≤s ( 𝑘 +s 1s ) ) )
45 44 3 anbi12d ⊢ ( 𝑗 = ( 𝑘 +s 1s ) → ( ( 𝑀 ≤s 𝑗 ∧ 𝜑 ) ↔ ( 𝑀 ≤s ( 𝑘 +s 1s ) ∧ 𝜃 ) ) )
46 45 elrab ⊢ ( ( 𝑘 +s 1s ) ∈ { 𝑗 ∈ ℤs ∣ ( 𝑀 ≤s 𝑗 ∧ 𝜑 ) } ↔ ( ( 𝑘 +s 1s ) ∈ ℤs ∧ ( 𝑀 ≤s ( 𝑘 +s 1s ) ∧ 𝜃 ) ) )
47 39 43 46 3imtr4i ⊢ ( ( 𝑀 ∈ ℤs ∧ 𝑘 ∈ { 𝑗 ∈ ℤs ∣ ( 𝑀 ≤s 𝑗 ∧ 𝜑 ) } ) → ( 𝑘 +s 1s ) ∈ { 𝑗 ∈ ℤs ∣ ( 𝑀 ≤s 𝑗 ∧ 𝜑 ) } )
48 7 15 47 peano5uzs ⊢ ( 𝑀 ∈ ℤs → { 𝑤 ∈ ℤs ∣ 𝑀 ≤s 𝑤 } ⊆ { 𝑗 ∈ ℤs ∣ ( 𝑀 ≤s 𝑗 ∧ 𝜑 ) } )
49 48 sseld ⊢ ( 𝑀 ∈ ℤs → ( 𝑁 ∈ { 𝑤 ∈ ℤs ∣ 𝑀 ≤s 𝑤 } → 𝑁 ∈ { 𝑗 ∈ ℤs ∣ ( 𝑀 ≤s 𝑗 ∧ 𝜑 ) } ) )
50 breq2 ⊢ ( 𝑤 = 𝑁 → ( 𝑀 ≤s 𝑤 ↔ 𝑀 ≤s 𝑁 ) )
51 50 elrab ⊢ ( 𝑁 ∈ { 𝑤 ∈ ℤs ∣ 𝑀 ≤s 𝑤 } ↔ ( 𝑁 ∈ ℤs ∧ 𝑀 ≤s 𝑁 ) )
52 breq2 ⊢ ( 𝑗 = 𝑁 → ( 𝑀 ≤s 𝑗 ↔ 𝑀 ≤s 𝑁 ) )
53 52 4 anbi12d ⊢ ( 𝑗 = 𝑁 → ( ( 𝑀 ≤s 𝑗 ∧ 𝜑 ) ↔ ( 𝑀 ≤s 𝑁 ∧ 𝜏 ) ) )
54 53 elrab ⊢ ( 𝑁 ∈ { 𝑗 ∈ ℤs ∣ ( 𝑀 ≤s 𝑗 ∧ 𝜑 ) } ↔ ( 𝑁 ∈ ℤs ∧ ( 𝑀 ≤s 𝑁 ∧ 𝜏 ) ) )
55 49 51 54 3imtr3g ⊢ ( 𝑀 ∈ ℤs → ( ( 𝑁 ∈ ℤs ∧ 𝑀 ≤s 𝑁 ) → ( 𝑁 ∈ ℤs ∧ ( 𝑀 ≤s 𝑁 ∧ 𝜏 ) ) ) )
56 55 3impib ⊢ ( ( 𝑀 ∈ ℤs ∧ 𝑁 ∈ ℤs ∧ 𝑀 ≤s 𝑁 ) → ( 𝑁 ∈ ℤs ∧ ( 𝑀 ≤s 𝑁 ∧ 𝜏 ) ) )
57 56 simprrd ⊢ ( ( 𝑀 ∈ ℤs ∧ 𝑁 ∈ ℤs ∧ 𝑀 ≤s 𝑁 ) → 𝜏 )