This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrid ⊢ ( ( 𝑝 ↾ ( 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 eqtrid ⊢ ( ( 𝑝 ↾ ( 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 bitrid ⊢ ( ( 𝑝 ↾ ( 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 eqtrid ⊢ ( ( 𝑝 ↾ ( 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 eqtrid ⊢ ( ( 𝑝 ↾ ( 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 bitrid ⊢ ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( [ ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ] 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ↔ 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) ) )
131 130 rexbidv ⊢ ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ V → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) [ ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ] 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ↔ ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) ) )
132 116 131 bitrid ⊢ ( ( 𝑝 ↾ ( 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 peano2uz ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑦 ) → ( 𝑦 + 1 ) ∈ ( ℤ≥ ‘ 𝑦 ) )
181 fzoss2 ⊢ ( ( 𝑦 + 1 ) ∈ ( ℤ≥ ‘ 𝑦 ) → ( 0 ..^ 𝑦 ) ⊆ ( 0 ..^ ( 𝑦 + 1 ) ) )
182 178 179 180 181 4syl ⊢ ( 𝑦 ∈ ℕ → ( 0 ..^ 𝑦 ) ⊆ ( 0 ..^ ( 𝑦 + 1 ) ) )
183 182 ad2antrr ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑦 ) ) ) → ( 0 ..^ 𝑦 ) ⊆ ( 0 ..^ ( 𝑦 + 1 ) ) )
184 ssrexv ⊢ ( ( 0 ..^ 𝑦 ) ⊆ ( 0 ..^ ( 𝑦 + 1 ) ) → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) )
185 183 184 syl ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑦 ) ) ) → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) )
186 177 185 sylbid ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑦 ) ) ) → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) )
187 165 186 embantd ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑦 ) ) ) → ( ( 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) )
188 187 ex ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑦 ) ) → ( ( 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) )
189 188 adantr ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ ¬ ( 𝑝 ‘ 𝑦 ) ≤ 𝑋 ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑦 ) ) → ( ( 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) )
190 152 189 syld ⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) ∧ ¬ ( 𝑝 ‘ 𝑦 ) ≤ 𝑋 ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ( ( 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) )
191 190 ex ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( ¬ ( 𝑝 ‘ 𝑦 ) ≤ 𝑋 → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ( ( 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) ) )
192 191 com34 ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( ¬ ( 𝑝 ‘ 𝑦 ) ≤ 𝑋 → ( ( 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) ) )
193 192 com13 ⊢ ( ( 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 0 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ 𝑖 ) [,) ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ‘ ( 𝑖 + 1 ) ) ) ) → ( ¬ ( 𝑝 ‘ 𝑦 ) ≤ 𝑋 → ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) ) )
194 135 193 sylbi ⊢ ( [ ( 𝑝 ↾ ( 0 ... 𝑦 ) ) / 𝑝 ] ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) → ( ¬ ( 𝑝 ‘ 𝑦 ) ≤ 𝑋 → ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) ) )
195 97 194 syl ⊢ ( ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ ( RePart ‘ 𝑦 ) ∧ ∀ 𝑝 ∈ ( RePart ‘ 𝑦 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) → ( ¬ ( 𝑝 ‘ 𝑦 ) ≤ 𝑋 → ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) ) )
196 195 ex ⊢ ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ ( RePart ‘ 𝑦 ) → ( ∀ 𝑝 ∈ ( RePart ‘ 𝑦 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) → ( ¬ ( 𝑝 ‘ 𝑦 ) ≤ 𝑋 → ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) ) ) )
197 196 com24 ⊢ ( ( 𝑝 ↾ ( 0 ... 𝑦 ) ) ∈ ( RePart ‘ 𝑦 ) → ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( ¬ ( 𝑝 ‘ 𝑦 ) ≤ 𝑋 → ( ∀ 𝑝 ∈ ( RePart ‘ 𝑦 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) ) ) )
198 96 197 mpcom ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ) → ( ¬ ( 𝑝 ‘ 𝑦 ) ≤ 𝑋 → ( ∀ 𝑝 ∈ ( RePart ‘ 𝑦 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) ) )
199 198 ex ⊢ ( 𝑦 ∈ ℕ → ( 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) → ( ¬ ( 𝑝 ‘ 𝑦 ) ≤ 𝑋 → ( ∀ 𝑝 ∈ ( RePart ‘ 𝑦 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) ) ) )
200 199 com24 ⊢ ( 𝑦 ∈ ℕ → ( ∀ 𝑝 ∈ ( RePart ‘ 𝑦 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) → ( ¬ ( 𝑝 ‘ 𝑦 ) ≤ 𝑋 → ( 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) ) ) )
201 200 imp ⊢ ( ( 𝑦 ∈ ℕ ∧ ∀ 𝑝 ∈ ( RePart ‘ 𝑦 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) → ( ¬ ( 𝑝 ‘ 𝑦 ) ≤ 𝑋 → ( 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) ) )
202 95 201 pm2.61d ⊢ ( ( 𝑦 ∈ ℕ ∧ ∀ 𝑝 ∈ ( RePart ‘ 𝑦 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) → ( 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) → ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) )
203 46 202 ralrimi ⊢ ( ( 𝑦 ∈ ℕ ∧ ∀ 𝑝 ∈ ( RePart ‘ 𝑦 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) → ∀ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) )
204 203 ex ⊢ ( 𝑦 ∈ ℕ → ( ∀ 𝑝 ∈ ( RePart ‘ 𝑦 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑦 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑦 ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) → ∀ 𝑝 ∈ ( RePart ‘ ( 𝑦 + 1 ) ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ ( 𝑦 + 1 ) ) ) → ∃ 𝑖 ∈ ( 0 ..^ ( 𝑦 + 1 ) ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) ) )
205 10 18 26 34 43 204 nnind ⊢ ( 𝑀 ∈ ℕ → ∀ 𝑝 ∈ ( RePart ‘ 𝑀 ) ( 𝑋 ∈ ( ( 𝑝 ‘ 0 ) [,) ( 𝑝 ‘ 𝑀 ) ) → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) 𝑋 ∈ ( ( 𝑝 ‘ 𝑖 ) [,) ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) )