Metamath Proof Explorer

Theorem iccpartres

Description: The restriction of a partition is a partition. (Contributed by AV, 16-Jul-2020)

Ref Expression
Assertion iccpartres ( ( 𝑀 ∈ ℕ ∧ 𝑃 ∈ ( RePart ‘ ( 𝑀 + 1 ) ) ) → ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ∈ ( RePart ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 peano2nn ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 + 1 ) ∈ ℕ )
2 iccpart ⊢ ( ( 𝑀 + 1 ) ∈ ℕ → ( 𝑃 ∈ ( RePart ‘ ( 𝑀 + 1 ) ) ↔ ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑀 + 1 ) ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) )
3 1 2 syl ⊢ ( 𝑀 ∈ ℕ → ( 𝑃 ∈ ( RePart ‘ ( 𝑀 + 1 ) ) ↔ ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑀 + 1 ) ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) )
4 simpl ⊢ ( ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑀 + 1 ) ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) → 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) )
5 nnz ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℤ )
6 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
7 5 6 syl ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
8 peano2uz ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
9 7 8 syl ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
10 fzss2 ⊢ ( ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 0 ... 𝑀 ) ⊆ ( 0 ... ( 𝑀 + 1 ) ) )
11 9 10 syl ⊢ ( 𝑀 ∈ ℕ → ( 0 ... 𝑀 ) ⊆ ( 0 ... ( 𝑀 + 1 ) ) )
12 elmapssres ⊢ ( ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) ∧ ( 0 ... 𝑀 ) ⊆ ( 0 ... ( 𝑀 + 1 ) ) ) → ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) )
13 4 11 12 syl2anr ⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑀 + 1 ) ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) )
14 fzoss2 ⊢ ( ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 0 ..^ 𝑀 ) ⊆ ( 0 ..^ ( 𝑀 + 1 ) ) )
15 9 14 syl ⊢ ( 𝑀 ∈ ℕ → ( 0 ..^ 𝑀 ) ⊆ ( 0 ..^ ( 𝑀 + 1 ) ) )
16 ssralv ⊢ ( ( 0 ..^ 𝑀 ) ⊆ ( 0 ..^ ( 𝑀 + 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑀 + 1 ) ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) )
17 15 16 syl ⊢ ( 𝑀 ∈ ℕ → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝑀 + 1 ) ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) )
18 17 adantld ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑀 + 1 ) ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) )
19 18 imp ⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑀 + 1 ) ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
20 fzossfz ⊢ ( 0 ..^ 𝑀 ) ⊆ ( 0 ... 𝑀 )
21 20 a1i ⊢ ( ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) ∧ 𝑀 ∈ ℕ ) → ( 0 ..^ 𝑀 ) ⊆ ( 0 ... 𝑀 ) )
22 21 sselda ⊢ ( ( ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
23 fvres ⊢ ( 𝑖 ∈ ( 0 ... 𝑀 ) → ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ‘ 𝑖 ) = ( 𝑃 ‘ 𝑖 ) )
24 23 eqcomd ⊢ ( 𝑖 ∈ ( 0 ... 𝑀 ) → ( 𝑃 ‘ 𝑖 ) = ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ‘ 𝑖 ) )
25 22 24 syl ⊢ ( ( ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑃 ‘ 𝑖 ) = ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ‘ 𝑖 ) )
26 simpr ⊢ ( ( ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
27 elfzouz ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( ℤ≥ ‘ 0 ) )
28 27 adantl ⊢ ( ( ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( ℤ≥ ‘ 0 ) )
29 fzofzp1b ⊢ ( 𝑖 ∈ ( ℤ≥ ‘ 0 ) → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↔ ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) ) )
30 28 29 syl ⊢ ( ( ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↔ ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) ) )
31 26 30 mpbid ⊢ ( ( ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
32 fvres ⊢ ( ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) → ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ‘ ( 𝑖 + 1 ) ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
33 31 32 syl ⊢ ( ( ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ‘ ( 𝑖 + 1 ) ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
34 33 eqcomd ⊢ ( ( ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑃 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ‘ ( 𝑖 + 1 ) ) )
35 25 34 breq12d ⊢ ( ( ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ↔ ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ‘ 𝑖 ) < ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ‘ ( 𝑖 + 1 ) ) ) )
36 35 biimpd ⊢ ( ( ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) ∧ 𝑀 ∈ ℕ ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) → ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ‘ 𝑖 ) < ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ‘ ( 𝑖 + 1 ) ) ) )
37 36 ralimdva ⊢ ( ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) ∧ 𝑀 ∈ ℕ ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ‘ 𝑖 ) < ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ‘ ( 𝑖 + 1 ) ) ) )
38 37 ex ⊢ ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) → ( 𝑀 ∈ ℕ → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ‘ 𝑖 ) < ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ‘ ( 𝑖 + 1 ) ) ) ) )
39 38 adantr ⊢ ( ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑀 + 1 ) ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑀 ∈ ℕ → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ‘ 𝑖 ) < ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ‘ ( 𝑖 + 1 ) ) ) ) )
40 39 impcom ⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑀 + 1 ) ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ‘ 𝑖 ) < ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ‘ ( 𝑖 + 1 ) ) ) )
41 19 40 mpd ⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑀 + 1 ) ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ‘ 𝑖 ) < ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ‘ ( 𝑖 + 1 ) ) )
42 iccpart ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ∈ ( RePart ‘ 𝑀 ) ↔ ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ‘ 𝑖 ) < ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ‘ ( 𝑖 + 1 ) ) ) ) )
43 42 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑀 + 1 ) ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ∈ ( RePart ‘ 𝑀 ) ↔ ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ‘ 𝑖 ) < ( ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ‘ ( 𝑖 + 1 ) ) ) ) )
44 13 41 43 mpbir2and ⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑀 + 1 ) ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ∈ ( RePart ‘ 𝑀 ) )
45 44 ex ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... ( 𝑀 + 1 ) ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝑀 + 1 ) ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ∈ ( RePart ‘ 𝑀 ) ) )
46 3 45 sylbid ⊢ ( 𝑀 ∈ ℕ → ( 𝑃 ∈ ( RePart ‘ ( 𝑀 + 1 ) ) → ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ∈ ( RePart ‘ 𝑀 ) ) )
47 46 imp ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑃 ∈ ( RePart ‘ ( 𝑀 + 1 ) ) ) → ( 𝑃 ↾ ( 0 ... 𝑀 ) ) ∈ ( RePart ‘ 𝑀 ) )