Metamath Proof Explorer


Theorem iccelpart

Description: An element of any partitioned half-open interval of extended reals is an element of a part of this partition. (Contributed by AV, 18-Jul-2020)

Ref Expression
Assertion iccelpart ( 𝑀 ∈ ℕ → ∀ 𝑝 ∈ ( RePart ‘ 𝑀 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑀 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 ( 𝑥 = 1 → ( RePart ‘ 𝑥 ) = ( RePart ‘ 1 ) )
2 fveq2 ( 𝑥 = 1 → ( 𝑝𝑥 ) = ( 𝑝 ‘ 1 ) )
3 2 oveq2d ( 𝑥 = 1 → ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑥 ) ) = ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 1 ) ) )
4 3 eleq2d ( 𝑥 = 1 → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑥 ) ) ↔ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 1 ) ) ) )
5 oveq2 ( 𝑥 = 1 → ( 0 ..^ 𝑥 ) = ( 0 ..^ 1 ) )
6 fzo01 ( 0 ..^ 1 ) = { 0 }
7 5 6 eqtrdi ( 𝑥 = 1 → ( 0 ..^ 𝑥 ) = { 0 } )
8 7 rexeqdv ( 𝑥 = 1 → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑥 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ↔ ∃ 𝑖 ∈ { 0 } 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) )
9 4 8 imbi12d ( 𝑥 = 1 → ( ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑥 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑥 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ↔ ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 1 ) ) → ∃ 𝑖 ∈ { 0 } 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) )
10 1 9 raleqbidv ( 𝑥 = 1 → ( ∀ 𝑝 ∈ ( RePart ‘ 𝑥 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑥 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑥 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ↔ ∀ 𝑝 ∈ ( RePart ‘ 1 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 1 ) ) → ∃ 𝑖 ∈ { 0 } 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) )
11 fveq2 ( 𝑥 = 𝑦 → ( RePart ‘ 𝑥 ) = ( RePart ‘ 𝑦 ) )
12 fveq2 ( 𝑥 = 𝑦 → ( 𝑝𝑥 ) = ( 𝑝𝑦 ) )
13 12 oveq2d ( 𝑥 = 𝑦 → ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑥 ) ) = ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) )
14 13 eleq2d ( 𝑥 = 𝑦 → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑥 ) ) ↔ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) ) )
15 oveq2 ( 𝑥 = 𝑦 → ( 0 ..^ 𝑥 ) = ( 0 ..^ 𝑦 ) )
16 15 rexeqdv ( 𝑥 = 𝑦 → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑥 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ↔ ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) )
17 14 16 imbi12d ( 𝑥 = 𝑦 → ( ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑥 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑥 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ↔ ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) )
18 11 17 raleqbidv ( 𝑥 = 𝑦 → ( ∀ 𝑝 ∈ ( RePart ‘ 𝑥 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑥 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑥 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ↔ ∀ 𝑝 ∈ ( RePart ‘ 𝑦 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) )
19 fveq2 ( 𝑥 = ( 𝑦 + 1 ) → ( RePart ‘ 𝑥 ) = ( RePart ‘ ( 𝑦 + 1 ) ) )
20 fveq2 ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑝𝑥 ) = ( 𝑝 ‘ ( 𝑦 + 1 ) ) )
21 20 oveq2d ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑥 ) ) = ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) )
22 21 eleq2d ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑥 ) ) ↔ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) )
23 oveq2 ( 𝑥 = ( 𝑦 + 1 ) → ( 0 ..^ 𝑥 ) = ( 0 ..^ ( 𝑦 + 1 ) ) )
24 23 rexeqdv ( 𝑥 = ( 𝑦 + 1 ) → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑥 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ↔ ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) )
25 22 24 imbi12d ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑥 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑥 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ↔ ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) )
26 19 25 raleqbidv ( 𝑥 = ( 𝑦 + 1 ) → ( ∀ 𝑝 ∈ ( RePart ‘ 𝑥 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑥 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑥 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ↔ ∀ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) )
27 fveq2 ( 𝑥 = 𝑀 → ( RePart ‘ 𝑥 ) = ( RePart ‘ 𝑀 ) )
28 fveq2 ( 𝑥 = 𝑀 → ( 𝑝𝑥 ) = ( 𝑝𝑀 ) )
29 28 oveq2d ( 𝑥 = 𝑀 → ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑥 ) ) = ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑀 ) ) )
30 29 eleq2d ( 𝑥 = 𝑀 → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑥 ) ) ↔ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑀 ) ) ) )
31 oveq2 ( 𝑥 = 𝑀 → ( 0 ..^ 𝑥 ) = ( 0 ..^ 𝑀 ) )
32 31 rexeqdv ( 𝑥 = 𝑀 → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑥 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ↔ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) )
33 30 32 imbi12d ( 𝑥 = 𝑀 → ( ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑥 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑥 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ↔ ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑀 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) )
34 27 33 raleqbidv ( 𝑥 = 𝑀 → ( ∀ 𝑝 ∈ ( RePart ‘ 𝑥 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑥 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑥 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ↔ ∀ 𝑝 ∈ ( RePart ‘ 𝑀 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑀 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) )
35 0nn0 0 ∈ ℕ0
36 fveq2 ( 𝑖 = 0 → ( 𝑝𝑖 ) = ( 𝑝 ‘ 0 ) )
37 fv0p1e1 ( 𝑖 = 0 → ( 𝑝 ‘ ( 𝑖 + 1 ) ) = ( 𝑝 ‘ 1 ) )
38 36 37 oveq12d ( 𝑖 = 0 → ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 1 ) ) )
39 38 eleq2d ( 𝑖 = 0 → ( 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ↔ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 1 ) ) ) )
40 39 rexsng ( 0 ∈ ℕ0 → ( ∃ 𝑖 ∈ { 0 } 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ↔ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 1 ) ) ) )
41 35 40 ax-mp ( ∃ 𝑖 ∈ { 0 } 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ↔ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 1 ) ) )
42 41 biimpri ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 1 ) ) → ∃ 𝑖 ∈ { 0 } 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) )
43 42 rgenw 𝑝 ∈ ( RePart ‘ 1 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 1 ) ) → ∃ 𝑖 ∈ { 0 } 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) )
44 nfv 𝑝 𝑦 ∈ ℕ
45 nfra1 𝑝𝑝 ∈ ( RePart ‘ 𝑦 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) )
46 44 45 nfan 𝑝 ( 𝑦 ∈ ℕ ∧ ∀ 𝑝 ∈ ( RePart ‘ 𝑦 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) )
47 nnnn0 ( 𝑦 ∈ ℕ → 𝑦 ∈ ℕ0 )
48 fzonn0p1 ( 𝑦 ∈ ℕ0𝑦 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) )
49 47 48 syl ( 𝑦 ∈ ℕ → 𝑦 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) )
50 49 ad2antrr ( ( ( 𝑦 ∈ ℕ ∧ ( 𝑝𝑦 ) ≤ 𝑋 ) ∧ ( 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ∧ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) ) → 𝑦 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) )
51 fveq2 ( 𝑖 = 𝑦 → ( 𝑝𝑖 ) = ( 𝑝𝑦 ) )
52 fvoveq1 ( 𝑖 = 𝑦 → ( 𝑝 ‘ ( 𝑖 + 1 ) ) = ( 𝑝 ‘ ( 𝑦 + 1 ) ) )
53 51 52 oveq12d ( 𝑖 = 𝑦 → ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑝𝑦 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) )
54 53 eleq2d ( 𝑖 = 𝑦 → ( 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ↔ 𝑋 ∈ ( ( 𝑝𝑦 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) )
55 54 adantl ( ( ( ( 𝑦 ∈ ℕ ∧ ( 𝑝𝑦 ) ≤ 𝑋 ) ∧ ( 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ∧ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) ) ∧ 𝑖 = 𝑦 ) → ( 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ↔ 𝑋 ∈ ( ( 𝑝𝑦 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) )
56 peano2nn ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) ∈ ℕ )
57 56 adantr ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( 𝑦 + 1 ) ∈ ℕ )
58 simpr ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) )
59 56 nnnn0d ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) ∈ ℕ0 )
60 0elfz ( ( 𝑦 + 1 ) ∈ ℕ0 → 0 ∈ ( 0 ... ( 𝑦 + 1 ) ) )
61 59 60 syl ( 𝑦 ∈ ℕ → 0 ∈ ( 0 ... ( 𝑦 + 1 ) ) )
62 61 adantr ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → 0 ∈ ( 0 ... ( 𝑦 + 1 ) ) )
63 57 58 62 iccpartxr ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( 𝑝 ‘ 0 ) ∈ ℝ* )
64 nn0fz0 ( ( 𝑦 + 1 ) ∈ ℕ0 ↔ ( 𝑦 + 1 ) ∈ ( 0 ... ( 𝑦 + 1 ) ) )
65 59 64 sylib ( 𝑦 ∈ ℕ → ( 𝑦 + 1 ) ∈ ( 0 ... ( 𝑦 + 1 ) ) )
66 65 adantr ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( 𝑦 + 1 ) ∈ ( 0 ... ( 𝑦 + 1 ) ) )
67 57 58 66 iccpartxr ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( 𝑝 ‘ ( 𝑦 + 1 ) ) ∈ ℝ* )
68 63 67 jca ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( ( 𝑝 ‘ 0 ) ∈ ℝ* ∧ ( 𝑝 ‘ ( 𝑦 + 1 ) ) ∈ ℝ* ) )
69 68 adantlr ( ( ( 𝑦 ∈ ℕ ∧ ( 𝑝𝑦 ) ≤ 𝑋 ) ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( ( 𝑝 ‘ 0 ) ∈ ℝ* ∧ ( 𝑝 ‘ ( 𝑦 + 1 ) ) ∈ ℝ* ) )
70 elico1 ( ( ( 𝑝 ‘ 0 ) ∈ ℝ* ∧ ( 𝑝 ‘ ( 𝑦 + 1 ) ) ∈ ℝ* ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ↔ ( 𝑋 ∈ ℝ* ∧ ( 𝑝 ‘ 0 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) )
71 69 70 syl ( ( ( 𝑦 ∈ ℕ ∧ ( 𝑝𝑦 ) ≤ 𝑋 ) ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ↔ ( 𝑋 ∈ ℝ* ∧ ( 𝑝 ‘ 0 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) )
72 simp1 ( ( 𝑋 ∈ ℝ* ∧ ( 𝑝 ‘ 0 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → 𝑋 ∈ ℝ* )
73 72 adantl ( ( ( 𝑝𝑦 ) ≤ 𝑋 ∧ ( 𝑋 ∈ ℝ* ∧ ( 𝑝 ‘ 0 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) → 𝑋 ∈ ℝ* )
74 simpl ( ( ( 𝑝𝑦 ) ≤ 𝑋 ∧ ( 𝑋 ∈ ℝ* ∧ ( 𝑝 ‘ 0 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) → ( 𝑝𝑦 ) ≤ 𝑋 )
75 simpr3 ( ( ( 𝑝𝑦 ) ≤ 𝑋 ∧ ( 𝑋 ∈ ℝ* ∧ ( 𝑝 ‘ 0 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) → 𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) )
76 73 74 75 3jca ( ( ( 𝑝𝑦 ) ≤ 𝑋 ∧ ( 𝑋 ∈ ℝ* ∧ ( 𝑝 ‘ 0 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) → ( 𝑋 ∈ ℝ* ∧ ( 𝑝𝑦 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) )
77 76 ex ( ( 𝑝𝑦 ) ≤ 𝑋 → ( ( 𝑋 ∈ ℝ* ∧ ( 𝑝 ‘ 0 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ( 𝑋 ∈ ℝ* ∧ ( 𝑝𝑦 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) )
78 77 adantl ( ( 𝑦 ∈ ℕ ∧ ( 𝑝𝑦 ) ≤ 𝑋 ) → ( ( 𝑋 ∈ ℝ* ∧ ( 𝑝 ‘ 0 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ( 𝑋 ∈ ℝ* ∧ ( 𝑝𝑦 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) )
79 78 adantr ( ( ( 𝑦 ∈ ℕ ∧ ( 𝑝𝑦 ) ≤ 𝑋 ) ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( ( 𝑋 ∈ ℝ* ∧ ( 𝑝 ‘ 0 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ( 𝑋 ∈ ℝ* ∧ ( 𝑝𝑦 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) )
80 71 79 sylbid ( ( ( 𝑦 ∈ ℕ ∧ ( 𝑝𝑦 ) ≤ 𝑋 ) ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ( 𝑋 ∈ ℝ* ∧ ( 𝑝𝑦 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) )
81 80 impr ( ( ( 𝑦 ∈ ℕ ∧ ( 𝑝𝑦 ) ≤ 𝑋 ) ∧ ( 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ∧ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) ) → ( 𝑋 ∈ ℝ* ∧ ( 𝑝𝑦 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) )
82 nn0fz0 ( 𝑦 ∈ ℕ0𝑦 ∈ ( 0 ... 𝑦 ) )
83 47 82 sylib ( 𝑦 ∈ ℕ → 𝑦 ∈ ( 0 ... 𝑦 ) )
84 fzelp1 ( 𝑦 ∈ ( 0 ... 𝑦 ) → 𝑦 ∈ ( 0 ... ( 𝑦 + 1 ) ) )
85 83 84 syl ( 𝑦 ∈ ℕ → 𝑦 ∈ ( 0 ... ( 𝑦 + 1 ) ) )
86 85 adantr ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → 𝑦 ∈ ( 0 ... ( 𝑦 + 1 ) ) )
87 57 58 86 iccpartxr ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( 𝑝𝑦 ) ∈ ℝ* )
88 87 67 jca ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( ( 𝑝𝑦 ) ∈ ℝ* ∧ ( 𝑝 ‘ ( 𝑦 + 1 ) ) ∈ ℝ* ) )
89 88 ad2ant2r ( ( ( 𝑦 ∈ ℕ ∧ ( 𝑝𝑦 ) ≤ 𝑋 ) ∧ ( 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ∧ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) ) → ( ( 𝑝𝑦 ) ∈ ℝ* ∧ ( 𝑝 ‘ ( 𝑦 + 1 ) ) ∈ ℝ* ) )
90 elico1 ( ( ( 𝑝𝑦 ) ∈ ℝ* ∧ ( 𝑝 ‘ ( 𝑦 + 1 ) ) ∈ ℝ* ) → ( 𝑋 ∈ ( ( 𝑝𝑦 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ↔ ( 𝑋 ∈ ℝ* ∧ ( 𝑝𝑦 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) )
91 89 90 syl ( ( ( 𝑦 ∈ ℕ ∧ ( 𝑝𝑦 ) ≤ 𝑋 ) ∧ ( 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ∧ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) ) → ( 𝑋 ∈ ( ( 𝑝𝑦 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ↔ ( 𝑋 ∈ ℝ* ∧ ( 𝑝𝑦 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) )
92 81 91 mpbird ( ( ( 𝑦 ∈ ℕ ∧ ( 𝑝𝑦 ) ≤ 𝑋 ) ∧ ( 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ∧ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) ) → 𝑋 ∈ ( ( 𝑝𝑦 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) )
93 50 55 92 rspcedvd ( ( ( 𝑦 ∈ ℕ ∧ ( 𝑝𝑦 ) ≤ 𝑋 ) ∧ ( 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ∧ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) )
94 93 exp43 ( 𝑦 ∈ ℕ → ( ( 𝑝𝑦 ) ≤ 𝑋 → ( 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) ) )
95 94 adantr ( ( 𝑦 ∈ ℕ ∧ ∀ 𝑝 ∈ ( RePart ‘ 𝑦 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) → ( ( 𝑝𝑦 ) ≤ 𝑋 → ( 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) ) )
96 iccpartres ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ ( RePart ‘ 𝑦 ) )
97 rspsbca ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ ( RePart ‘ 𝑦 ) ∧ ∀ 𝑝 ∈ ( RePart ‘ 𝑦 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) → [ ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ] ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) )
98 vex 𝑝 ∈ V
99 98 resex ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V
100 sbcimg ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( [ ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ] ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ↔ ( [ ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ] 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) → [ ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ]𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) )
101 sbcel2 ( [ ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ] 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) ↔ 𝑋 ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) )
102 csbov12g ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) = ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( 𝑝 ‘ 0 ) [,) ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( 𝑝𝑦 ) ) )
103 csbfv12 ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( 𝑝 ‘ 0 ) = ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 𝑝 ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 0 )
104 csbvarg ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 𝑝 = ( 𝑝 ↾ ( 0 ... 𝑦 ) ) )
105 csbconstg ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 0 = 0 )
106 104 105 fveq12d ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 𝑝 ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 0 ) = ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) )
107 103 106 syl5eq ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( 𝑝 ‘ 0 ) = ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) )
108 csbfv12 ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( 𝑝𝑦 ) = ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 𝑝 ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 𝑦 )
109 csbconstg ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 𝑦 = 𝑦 )
110 104 109 fveq12d ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 𝑝 ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 𝑦 ) = ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) )
111 108 110 syl5eq ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( 𝑝𝑦 ) = ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) )
112 107 111 oveq12d ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( 𝑝 ‘ 0 ) [,) ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( 𝑝𝑦 ) ) = ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) ) )
113 102 112 eqtrd ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) = ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) ) )
114 113 eleq2d ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( 𝑋 ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) ↔ 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) ) ) )
115 101 114 syl5bb ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( [ ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ] 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) ↔ 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) ) ) )
116 sbcrex ( [ ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ]𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ↔ ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) [ ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ] 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) )
117 sbcel2 ( [ ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ] 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ↔ 𝑋 ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) )
118 csbov12g ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( 𝑝𝑖 ) [,) ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) )
119 csbfv12 ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( 𝑝𝑖 ) = ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 𝑝 ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 𝑖 )
120 csbconstg ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 𝑖 = 𝑖 )
121 104 120 fveq12d ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 𝑝 ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 𝑖 ) = ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) )
122 119 121 syl5eq ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( 𝑝𝑖 ) = ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) )
123 csbfv12 ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( 𝑝 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 𝑝 ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( 𝑖 + 1 ) )
124 csbconstg ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( 𝑖 + 1 ) = ( 𝑖 + 1 ) )
125 104 124 fveq12d ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 𝑝 ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( 𝑖 + 1 ) ) = ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) )
126 123 125 syl5eq ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( 𝑝 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) )
127 122 126 oveq12d ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( 𝑝𝑖 ) [,) ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) = ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) )
128 118 127 eqtrd ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) = ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) )
129 128 eleq2d ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( 𝑋 ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ↔ 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) ) )
130 117 129 syl5bb ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( [ ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ] 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ↔ 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) ) )
131 130 rexbidv ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) [ ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ] 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ↔ ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) ) )
132 116 131 syl5bb ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( [ ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ]𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ↔ ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) ) )
133 115 132 imbi12d ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( ( [ ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ] 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) → [ ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ]𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ↔ ( 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) ) ) )
134 100 133 bitrd ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( [ ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ] ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ↔ ( 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) ) ) )
135 99 134 ax-mp ( [ ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ] ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ↔ ( 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) ) )
136 68 70 syl ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ↔ ( 𝑋 ∈ ℝ* ∧ ( 𝑝 ‘ 0 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) )
137 136 adantr ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ ¬ ( 𝑝𝑦 ) ≤ 𝑋 ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ↔ ( 𝑋 ∈ ℝ* ∧ ( 𝑝 ‘ 0 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) )
138 72 adantl ( ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ ¬ ( 𝑝𝑦 ) ≤ 𝑋 ) ∧ ( 𝑋 ∈ ℝ* ∧ ( 𝑝 ‘ 0 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) → 𝑋 ∈ ℝ* )
139 simpr2 ( ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ ¬ ( 𝑝𝑦 ) ≤ 𝑋 ) ∧ ( 𝑋 ∈ ℝ* ∧ ( 𝑝 ‘ 0 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) → ( 𝑝 ‘ 0 ) ≤ 𝑋 )
140 xrltnle ( ( 𝑋 ∈ ℝ* ∧ ( 𝑝𝑦 ) ∈ ℝ* ) → ( 𝑋 < ( 𝑝𝑦 ) ↔ ¬ ( 𝑝𝑦 ) ≤ 𝑋 ) )
141 72 87 140 syl2anr ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ ( 𝑋 ∈ ℝ* ∧ ( 𝑝 ‘ 0 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) → ( 𝑋 < ( 𝑝𝑦 ) ↔ ¬ ( 𝑝𝑦 ) ≤ 𝑋 ) )
142 141 exbiri ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( ( 𝑋 ∈ ℝ* ∧ ( 𝑝 ‘ 0 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ( ¬ ( 𝑝𝑦 ) ≤ 𝑋𝑋 < ( 𝑝𝑦 ) ) ) )
143 142 com23 ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( ¬ ( 𝑝𝑦 ) ≤ 𝑋 → ( ( 𝑋 ∈ ℝ* ∧ ( 𝑝 ‘ 0 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → 𝑋 < ( 𝑝𝑦 ) ) ) )
144 143 imp31 ( ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ ¬ ( 𝑝𝑦 ) ≤ 𝑋 ) ∧ ( 𝑋 ∈ ℝ* ∧ ( 𝑝 ‘ 0 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) → 𝑋 < ( 𝑝𝑦 ) )
145 138 139 144 3jca ( ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ ¬ ( 𝑝𝑦 ) ≤ 𝑋 ) ∧ ( 𝑋 ∈ ℝ* ∧ ( 𝑝 ‘ 0 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) → ( 𝑋 ∈ ℝ* ∧ ( 𝑝 ‘ 0 ) ≤ 𝑋𝑋 < ( 𝑝𝑦 ) ) )
146 63 87 jca ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( ( 𝑝 ‘ 0 ) ∈ ℝ* ∧ ( 𝑝𝑦 ) ∈ ℝ* ) )
147 146 ad2antrr ( ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ ¬ ( 𝑝𝑦 ) ≤ 𝑋 ) ∧ ( 𝑋 ∈ ℝ* ∧ ( 𝑝 ‘ 0 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) → ( ( 𝑝 ‘ 0 ) ∈ ℝ* ∧ ( 𝑝𝑦 ) ∈ ℝ* ) )
148 elico1 ( ( ( 𝑝 ‘ 0 ) ∈ ℝ* ∧ ( 𝑝𝑦 ) ∈ ℝ* ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) ↔ ( 𝑋 ∈ ℝ* ∧ ( 𝑝 ‘ 0 ) ≤ 𝑋𝑋 < ( 𝑝𝑦 ) ) ) )
149 147 148 syl ( ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ ¬ ( 𝑝𝑦 ) ≤ 𝑋 ) ∧ ( 𝑋 ∈ ℝ* ∧ ( 𝑝 ‘ 0 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) ↔ ( 𝑋 ∈ ℝ* ∧ ( 𝑝 ‘ 0 ) ≤ 𝑋𝑋 < ( 𝑝𝑦 ) ) ) )
150 145 149 mpbird ( ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ ¬ ( 𝑝𝑦 ) ≤ 𝑋 ) ∧ ( 𝑋 ∈ ℝ* ∧ ( 𝑝 ‘ 0 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) ) → 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) )
151 150 ex ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ ¬ ( 𝑝𝑦 ) ≤ 𝑋 ) → ( ( 𝑋 ∈ ℝ* ∧ ( 𝑝 ‘ 0 ) ≤ 𝑋𝑋 < ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) ) )
152 137 151 sylbid ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ ¬ ( 𝑝𝑦 ) ≤ 𝑋 ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) ) )
153 0elfz ( 𝑦 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑦 ) )
154 47 153 syl ( 𝑦 ∈ ℕ → 0 ∈ ( 0 ... 𝑦 ) )
155 154 adantr ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → 0 ∈ ( 0 ... 𝑦 ) )
156 fvres ( 0 ∈ ( 0 ... 𝑦 ) → ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) = ( 𝑝 ‘ 0 ) )
157 155 156 syl ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) = ( 𝑝 ‘ 0 ) )
158 157 eqcomd ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( 𝑝 ‘ 0 ) = ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) )
159 83 adantr ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → 𝑦 ∈ ( 0 ... 𝑦 ) )
160 fvres ( 𝑦 ∈ ( 0 ... 𝑦 ) → ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) = ( 𝑝𝑦 ) )
161 159 160 syl ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) = ( 𝑝𝑦 ) )
162 161 eqcomd ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( 𝑝𝑦 ) = ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) )
163 158 162 oveq12d ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) = ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) ) )
164 163 eleq2d ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) ↔ 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) ) ) )
165 164 biimpa ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) ) → 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) ) )
166 elfzofz ( 𝑖 ∈ ( 0 ..^ 𝑦 ) → 𝑖 ∈ ( 0 ... 𝑦 ) )
167 166 adantl ( ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑦 ) ) → 𝑖 ∈ ( 0 ... 𝑦 ) )
168 fvres ( 𝑖 ∈ ( 0 ... 𝑦 ) → ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) = ( 𝑝𝑖 ) )
169 167 168 syl ( ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑦 ) ) → ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) = ( 𝑝𝑖 ) )
170 fzofzp1 ( 𝑖 ∈ ( 0 ..^ 𝑦 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑦 ) )
171 170 adantl ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑦 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑦 ) )
172 fvres ( ( 𝑖 + 1 ) ∈ ( 0 ... 𝑦 ) → ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) = ( 𝑝 ‘ ( 𝑖 + 1 ) ) )
173 171 172 syl ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑦 ) ) → ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) = ( 𝑝 ‘ ( 𝑖 + 1 ) ) )
174 173 adantlr ( ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑦 ) ) → ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) = ( 𝑝 ‘ ( 𝑖 + 1 ) ) )
175 169 174 oveq12d ( ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑦 ) ) → ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) = ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) )
176 175 eleq2d ( ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑦 ) ) → ( 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) ↔ 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) )
177 176 rexbidva ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) ) → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) ↔ ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) )
178 nnz ( 𝑦 ∈ ℕ → 𝑦 ∈ ℤ )
179 uzid ( 𝑦 ∈ ℤ → 𝑦 ∈ ( ℤ𝑦 ) )
180 178 179 syl ( 𝑦 ∈ ℕ → 𝑦 ∈ ( ℤ𝑦 ) )
181 peano2uz ( 𝑦 ∈ ( ℤ𝑦 ) → ( 𝑦 + 1 ) ∈ ( ℤ𝑦 ) )
182 fzoss2 ( ( 𝑦 + 1 ) ∈ ( ℤ𝑦 ) → ( 0 ..^ 𝑦 ) ⊆ ( 0 ..^ ( 𝑦 + 1 ) ) )
183 180 181 182 3syl ( 𝑦 ∈ ℕ → ( 0 ..^ 𝑦 ) ⊆ ( 0 ..^ ( 𝑦 + 1 ) ) )
184 183 ad2antrr ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) ) → ( 0 ..^ 𝑦 ) ⊆ ( 0 ..^ ( 𝑦 + 1 ) ) )
185 ssrexv ( ( 0 ..^ 𝑦 ) ⊆ ( 0 ..^ ( 𝑦 + 1 ) ) → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) )
186 184 185 syl ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) ) → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) )
187 177 186 sylbid ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) ) → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) )
188 165 187 embantd ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) ) → ( ( 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) )
189 188 ex ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) → ( ( 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) )
190 189 adantr ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ ¬ ( 𝑝𝑦 ) ≤ 𝑋 ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) → ( ( 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) )
191 152 190 syld ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ ¬ ( 𝑝𝑦 ) ≤ 𝑋 ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ( ( 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) )
192 191 ex ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( ¬ ( 𝑝𝑦 ) ≤ 𝑋 → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ( ( 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) ) )
193 192 com34 ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( ¬ ( 𝑝𝑦 ) ≤ 𝑋 → ( ( 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) ) )
194 193 com13 ( ( 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) ) → ( ¬ ( 𝑝𝑦 ) ≤ 𝑋 → ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) ) )
195 135 194 sylbi ( [ ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ] ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) → ( ¬ ( 𝑝𝑦 ) ≤ 𝑋 → ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) ) )
196 97 195 syl ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ ( RePart ‘ 𝑦 ) ∧ ∀ 𝑝 ∈ ( RePart ‘ 𝑦 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) → ( ¬ ( 𝑝𝑦 ) ≤ 𝑋 → ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) ) )
197 196 ex ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ ( RePart ‘ 𝑦 ) → ( ∀ 𝑝 ∈ ( RePart ‘ 𝑦 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) → ( ¬ ( 𝑝𝑦 ) ≤ 𝑋 → ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) ) ) )
198 197 com24 ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ ( RePart ‘ 𝑦 ) → ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( ¬ ( 𝑝𝑦 ) ≤ 𝑋 → ( ∀ 𝑝 ∈ ( RePart ‘ 𝑦 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) ) ) )
199 96 198 mpcom ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( ¬ ( 𝑝𝑦 ) ≤ 𝑋 → ( ∀ 𝑝 ∈ ( RePart ‘ 𝑦 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) ) )
200 199 ex ( 𝑦 ∈ ℕ → ( 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) → ( ¬ ( 𝑝𝑦 ) ≤ 𝑋 → ( ∀ 𝑝 ∈ ( RePart ‘ 𝑦 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) ) ) )
201 200 com24 ( 𝑦 ∈ ℕ → ( ∀ 𝑝 ∈ ( RePart ‘ 𝑦 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) → ( ¬ ( 𝑝𝑦 ) ≤ 𝑋 → ( 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) ) ) )
202 201 imp ( ( 𝑦 ∈ ℕ ∧ ∀ 𝑝 ∈ ( RePart ‘ 𝑦 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) → ( ¬ ( 𝑝𝑦 ) ≤ 𝑋 → ( 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) ) )
203 95 202 pm2.61d ( ( 𝑦 ∈ ℕ ∧ ∀ 𝑝 ∈ ( RePart ‘ 𝑦 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) → ( 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) )
204 46 203 ralrimi ( ( 𝑦 ∈ ℕ ∧ ∀ 𝑝 ∈ ( RePart ‘ 𝑦 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) → ∀ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) )
205 204 ex ( 𝑦 ∈ ℕ → ( ∀ 𝑝 ∈ ( RePart ‘ 𝑦 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) → ∀ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) )
206 10 18 26 34 43 205 nnind ( 𝑀 ∈ ℕ → ∀ 𝑝 ∈ ( RePart ‘ 𝑀 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝𝑀 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑋 ∈ ( ( 𝑝𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) )