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 ⊢M∈ℕ→∀p∈RePart⁡MX∈p⁡0p⁡M→∃i∈0..^MX∈p⁡ip⁡i+1

Proof

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