Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stoweidlem59 Structured version   Visualization version   GIF version

Theorem stoweidlem59 44010
Description: This lemma proves that there exists a function π‘₯ as in the proof in [BrosowskiDeutsh] p. 91, after Lemma 2: xj is in the subalgebra, 0 <= xj <= 1, xj < Ξ΅ / n on Aj (meaning A in the paper), xj > 1 - \epsilon / n on Bj. Here 𝐷 is used to represent A in the paper (because A is used for the subalgebra of functions), 𝐸 is used to represent Ξ΅. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem59.1 Ⅎ𝑑𝐹
stoweidlem59.2 β„²π‘‘πœ‘
stoweidlem59.3 𝐾 = (topGenβ€˜ran (,))
stoweidlem59.4 𝑇 = βˆͺ 𝐽
stoweidlem59.5 𝐢 = (𝐽 Cn 𝐾)
stoweidlem59.6 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)})
stoweidlem59.7 𝐡 = (𝑗 ∈ (0...𝑁) ↦ {𝑑 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)})
stoweidlem59.8 π‘Œ = {𝑦 ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘¦β€˜π‘‘) ∧ (π‘¦β€˜π‘‘) ≀ 1)}
stoweidlem59.9 𝐻 = (𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))})
stoweidlem59.10 (πœ‘ β†’ 𝐽 ∈ Comp)
stoweidlem59.11 (πœ‘ β†’ 𝐴 βŠ† 𝐢)
stoweidlem59.12 ((πœ‘ ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)
stoweidlem59.13 ((πœ‘ ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴)
stoweidlem59.14 ((πœ‘ ∧ 𝑦 ∈ ℝ) β†’ (𝑑 ∈ 𝑇 ↦ 𝑦) ∈ 𝐴)
stoweidlem59.15 ((πœ‘ ∧ (π‘Ÿ ∈ 𝑇 ∧ 𝑑 ∈ 𝑇 ∧ π‘Ÿ β‰  𝑑)) β†’ βˆƒπ‘ž ∈ 𝐴 (π‘žβ€˜π‘Ÿ) β‰  (π‘žβ€˜π‘‘))
stoweidlem59.16 (πœ‘ β†’ 𝐹 ∈ 𝐢)
stoweidlem59.17 (πœ‘ β†’ 𝐸 ∈ ℝ+)
stoweidlem59.18 (πœ‘ β†’ 𝐸 < (1 / 3))
stoweidlem59.19 (πœ‘ β†’ 𝑁 ∈ β„•)
Assertion
Ref Expression
stoweidlem59 (πœ‘ β†’ βˆƒπ‘₯(π‘₯:(0...𝑁)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑁)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < ((π‘₯β€˜π‘—)β€˜π‘‘))))
Distinct variable groups:   𝑑,𝑗,𝑦   𝑦,𝐡   𝑦,𝐷   𝑗,𝑁,𝑑,𝑦   𝑗,π‘Œ   𝑓,𝑔,𝑗,π‘ž,π‘Ÿ,𝑑,𝑁   π‘₯,𝑓,𝑔,𝑗,𝑑,𝑁   𝑦,𝑓,π‘ž,π‘Ÿ,𝐴   𝐴,𝑔,π‘ž,π‘Ÿ,𝑑   𝐡,𝑓,𝑔,π‘ž,π‘Ÿ   𝐷,𝑓,𝑔,π‘ž,π‘Ÿ   𝑓,𝐸,𝑔,π‘Ÿ,𝑑   𝑓,𝐽,𝑔,π‘Ÿ,𝑑   𝑇,𝑓,𝑔,π‘ž,π‘Ÿ,𝑑   πœ‘,𝑓,𝑔,𝑗,π‘ž,π‘Ÿ   π‘₯,𝑦,𝐴   π‘₯,𝐡   π‘₯,𝐷   π‘₯,𝐸,𝑦   π‘₯,𝑇,𝑦   πœ‘,𝑦   𝑑,𝐾   π‘₯,𝐻   π‘₯,π‘Œ   πœ‘,π‘₯
Allowed substitution hints:   πœ‘(𝑑)   𝐴(𝑗)   𝐡(𝑑,𝑗)   𝐢(π‘₯,𝑦,𝑑,𝑓,𝑔,𝑗,π‘Ÿ,π‘ž)   𝐷(𝑑,𝑗)   𝑇(𝑗)   𝐸(𝑗,π‘ž)   𝐹(π‘₯,𝑦,𝑑,𝑓,𝑔,𝑗,π‘Ÿ,π‘ž)   𝐻(𝑦,𝑑,𝑓,𝑔,𝑗,π‘Ÿ,π‘ž)   𝐽(π‘₯,𝑦,𝑗,π‘ž)   𝐾(π‘₯,𝑦,𝑓,𝑔,𝑗,π‘Ÿ,π‘ž)   π‘Œ(𝑦,𝑑,𝑓,𝑔,π‘Ÿ,π‘ž)

Proof of Theorem stoweidlem59
Dummy variables π‘Ž 𝑀 β„Ž 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 stoweidlem59.8 . . . . . . . . . 10 π‘Œ = {𝑦 ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘¦β€˜π‘‘) ∧ (π‘¦β€˜π‘‘) ≀ 1)}
2 nfrab1 3425 . . . . . . . . . 10 Ⅎ𝑦{𝑦 ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘¦β€˜π‘‘) ∧ (π‘¦β€˜π‘‘) ≀ 1)}
31, 2nfcxfr 2904 . . . . . . . . 9 β„²π‘¦π‘Œ
4 nfcv 2906 . . . . . . . . 9 β„²π‘§π‘Œ
5 nfv 1918 . . . . . . . . 9 Ⅎ𝑧(βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))
6 nfv 1918 . . . . . . . . 9 Ⅎ𝑦(βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘§β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘§β€˜π‘‘))
7 fveq1 6837 . . . . . . . . . . . 12 (𝑦 = 𝑧 β†’ (π‘¦β€˜π‘‘) = (π‘§β€˜π‘‘))
87breq1d 5114 . . . . . . . . . . 11 (𝑦 = 𝑧 β†’ ((π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ↔ (π‘§β€˜π‘‘) < (𝐸 / 𝑁)))
98ralbidv 3173 . . . . . . . . . 10 (𝑦 = 𝑧 β†’ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ↔ βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘§β€˜π‘‘) < (𝐸 / 𝑁)))
107breq2d 5116 . . . . . . . . . . 11 (𝑦 = 𝑧 β†’ ((1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘) ↔ (1 βˆ’ (𝐸 / 𝑁)) < (π‘§β€˜π‘‘)))
1110ralbidv 3173 . . . . . . . . . 10 (𝑦 = 𝑧 β†’ (βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘) ↔ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘§β€˜π‘‘)))
129, 11anbi12d 632 . . . . . . . . 9 (𝑦 = 𝑧 β†’ ((βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘)) ↔ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘§β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘§β€˜π‘‘))))
133, 4, 5, 6, 12cbvrabw 3438 . . . . . . . 8 {𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))} = {𝑧 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘§β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘§β€˜π‘‘))}
14 ovexd 7385 . . . . . . . . . 10 (πœ‘ β†’ (𝐽 Cn 𝐾) ∈ V)
15 stoweidlem59.11 . . . . . . . . . . 11 (πœ‘ β†’ 𝐴 βŠ† 𝐢)
16 stoweidlem59.5 . . . . . . . . . . 11 𝐢 = (𝐽 Cn 𝐾)
1715, 16sseqtrdi 3993 . . . . . . . . . 10 (πœ‘ β†’ 𝐴 βŠ† (𝐽 Cn 𝐾))
1814, 17ssexd 5280 . . . . . . . . 9 (πœ‘ β†’ 𝐴 ∈ V)
191, 18rabexd 5289 . . . . . . . 8 (πœ‘ β†’ π‘Œ ∈ V)
2013, 19rabexd 5289 . . . . . . 7 (πœ‘ β†’ {𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))} ∈ V)
2120ralrimivw 3146 . . . . . 6 (πœ‘ β†’ βˆ€π‘— ∈ (0...𝑁){𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))} ∈ V)
22 stoweidlem59.9 . . . . . . 7 𝐻 = (𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))})
2322fnmpt 6637 . . . . . 6 (βˆ€π‘— ∈ (0...𝑁){𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))} ∈ V β†’ 𝐻 Fn (0...𝑁))
2421, 23syl 17 . . . . 5 (πœ‘ β†’ 𝐻 Fn (0...𝑁))
25 fzfi 13806 . . . . 5 (0...𝑁) ∈ Fin
26 fnfi 9059 . . . . 5 ((𝐻 Fn (0...𝑁) ∧ (0...𝑁) ∈ Fin) β†’ 𝐻 ∈ Fin)
2724, 25, 26sylancl 587 . . . 4 (πœ‘ β†’ 𝐻 ∈ Fin)
28 rnfi 9213 . . . 4 (𝐻 ∈ Fin β†’ ran 𝐻 ∈ Fin)
2927, 28syl 17 . . 3 (πœ‘ β†’ ran 𝐻 ∈ Fin)
30 fnchoice 42967 . . 3 (ran 𝐻 ∈ Fin β†’ βˆƒβ„Ž(β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀)))
3129, 30syl 17 . 2 (πœ‘ β†’ βˆƒβ„Ž(β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀)))
32 simprl 770 . . . . 5 ((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) β†’ β„Ž Fn ran 𝐻)
33 ovex 7383 . . . . . . . 8 (0...𝑁) ∈ V
3433mptex 7168 . . . . . . 7 (𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))}) ∈ V
3522, 34eqeltri 2835 . . . . . 6 𝐻 ∈ V
3635rnex 7840 . . . . 5 ran 𝐻 ∈ V
37 fnex 7162 . . . . 5 ((β„Ž Fn ran 𝐻 ∧ ran 𝐻 ∈ V) β†’ β„Ž ∈ V)
3832, 36, 37sylancl 587 . . . 4 ((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) β†’ β„Ž ∈ V)
39 coexg 7857 . . . 4 ((β„Ž ∈ V ∧ 𝐻 ∈ V) β†’ (β„Ž ∘ 𝐻) ∈ V)
4038, 35, 39sylancl 587 . . 3 ((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) β†’ (β„Ž ∘ 𝐻) ∈ V)
41 dffn3 6677 . . . . . . 7 (β„Ž Fn ran 𝐻 ↔ β„Ž:ran 𝐻⟢ran β„Ž)
4232, 41sylib 217 . . . . . 6 ((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) β†’ β„Ž:ran 𝐻⟢ran β„Ž)
43 nfv 1918 . . . . . . . . . 10 β„²π‘€πœ‘
44 nfv 1918 . . . . . . . . . . 11 Ⅎ𝑀 β„Ž Fn ran 𝐻
45 nfra1 3266 . . . . . . . . . . 11 β„²π‘€βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀)
4644, 45nfan 1903 . . . . . . . . . 10 Ⅎ𝑀(β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))
4743, 46nfan 1903 . . . . . . . . 9 Ⅎ𝑀(πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀)))
48 simplrr 777 . . . . . . . . . . 11 (((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) ∧ 𝑀 ∈ ran 𝐻) β†’ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))
49 simpr 486 . . . . . . . . . . 11 (((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) ∧ 𝑀 ∈ ran 𝐻) β†’ 𝑀 ∈ ran 𝐻)
50 fvelrnb 6899 . . . . . . . . . . . . . . . 16 (𝐻 Fn (0...𝑁) β†’ (𝑀 ∈ ran 𝐻 ↔ βˆƒπ‘Ž ∈ (0...𝑁)(π»β€˜π‘Ž) = 𝑀))
51 nfv 1918 . . . . . . . . . . . . . . . . 17 β„²π‘Ž(π»β€˜π‘—) = 𝑀
52 nfmpt1 5212 . . . . . . . . . . . . . . . . . . . 20 Ⅎ𝑗(𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))})
5322, 52nfcxfr 2904 . . . . . . . . . . . . . . . . . . 19 Ⅎ𝑗𝐻
54 nfcv 2906 . . . . . . . . . . . . . . . . . . 19 β„²π‘—π‘Ž
5553, 54nffv 6848 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑗(π»β€˜π‘Ž)
56 nfcv 2906 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑗𝑀
5755, 56nfeq 2919 . . . . . . . . . . . . . . . . 17 Ⅎ𝑗(π»β€˜π‘Ž) = 𝑀
58 fveq2 6838 . . . . . . . . . . . . . . . . . 18 (𝑗 = π‘Ž β†’ (π»β€˜π‘—) = (π»β€˜π‘Ž))
5958eqeq1d 2740 . . . . . . . . . . . . . . . . 17 (𝑗 = π‘Ž β†’ ((π»β€˜π‘—) = 𝑀 ↔ (π»β€˜π‘Ž) = 𝑀))
6051, 57, 59cbvrexw 3289 . . . . . . . . . . . . . . . 16 (βˆƒπ‘— ∈ (0...𝑁)(π»β€˜π‘—) = 𝑀 ↔ βˆƒπ‘Ž ∈ (0...𝑁)(π»β€˜π‘Ž) = 𝑀)
6150, 60bitr4di 289 . . . . . . . . . . . . . . 15 (𝐻 Fn (0...𝑁) β†’ (𝑀 ∈ ran 𝐻 ↔ βˆƒπ‘— ∈ (0...𝑁)(π»β€˜π‘—) = 𝑀))
6224, 61syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑀 ∈ ran 𝐻 ↔ βˆƒπ‘— ∈ (0...𝑁)(π»β€˜π‘—) = 𝑀))
6362biimpa 478 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀 ∈ ran 𝐻) β†’ βˆƒπ‘— ∈ (0...𝑁)(π»β€˜π‘—) = 𝑀)
64 simp3 1139 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁) ∧ (π»β€˜π‘—) = 𝑀) β†’ (π»β€˜π‘—) = 𝑀)
65 simpr 486 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ 𝑗 ∈ (0...𝑁))
6620adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ {𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))} ∈ V)
6722fvmpt2 6955 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ (0...𝑁) ∧ {𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))} ∈ V) β†’ (π»β€˜π‘—) = {𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))})
6865, 66, 67syl2anc 585 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ (π»β€˜π‘—) = {𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))})
69 stoweidlem59.6 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)})
70 nfcv 2906 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ⅎ𝑑(0...𝑁)
71 nfrab1 3425 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ⅎ𝑑{𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)}
7270, 71nfmpt 5211 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑑(𝑗 ∈ (0...𝑁) ↦ {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)})
7369, 72nfcxfr 2904 . . . . . . . . . . . . . . . . . . . . . . . 24 Ⅎ𝑑𝐷
74 nfcv 2906 . . . . . . . . . . . . . . . . . . . . . . . 24 Ⅎ𝑑𝑗
7573, 74nffv 6848 . . . . . . . . . . . . . . . . . . . . . . 23 Ⅎ𝑑(π·β€˜π‘—)
76 nfcv 2906 . . . . . . . . . . . . . . . . . . . . . . . 24 Ⅎ𝑑𝑇
77 stoweidlem59.7 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝐡 = (𝑗 ∈ (0...𝑁) ↦ {𝑑 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)})
78 nfrab1 3425 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ⅎ𝑑{𝑑 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)}
7970, 78nfmpt 5211 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ⅎ𝑑(𝑗 ∈ (0...𝑁) ↦ {𝑑 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)})
8077, 79nfcxfr 2904 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑑𝐡
8180, 74nffv 6848 . . . . . . . . . . . . . . . . . . . . . . . 24 Ⅎ𝑑(π΅β€˜π‘—)
8276, 81nfdif 4084 . . . . . . . . . . . . . . . . . . . . . . 23 Ⅎ𝑑(𝑇 βˆ– (π΅β€˜π‘—))
83 stoweidlem59.2 . . . . . . . . . . . . . . . . . . . . . . . 24 β„²π‘‘πœ‘
84 nfv 1918 . . . . . . . . . . . . . . . . . . . . . . . 24 Ⅎ𝑑 𝑗 ∈ (0...𝑁)
8583, 84nfan 1903 . . . . . . . . . . . . . . . . . . . . . . 23 Ⅎ𝑑(πœ‘ ∧ 𝑗 ∈ (0...𝑁))
86 stoweidlem59.3 . . . . . . . . . . . . . . . . . . . . . . 23 𝐾 = (topGenβ€˜ran (,))
87 stoweidlem59.4 . . . . . . . . . . . . . . . . . . . . . . 23 𝑇 = βˆͺ 𝐽
88 stoweidlem59.10 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 𝐽 ∈ Comp)
8988adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ 𝐽 ∈ Comp)
9015adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ 𝐴 βŠ† 𝐢)
91 stoweidlem59.12 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)
92913adant1r 1178 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) + (π‘”β€˜π‘‘))) ∈ 𝐴)
93 stoweidlem59.13 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴)
94933adant1r 1178 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) β†’ (𝑑 ∈ 𝑇 ↦ ((π‘“β€˜π‘‘) Β· (π‘”β€˜π‘‘))) ∈ 𝐴)
95 stoweidlem59.14 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑦 ∈ ℝ) β†’ (𝑑 ∈ 𝑇 ↦ 𝑦) ∈ 𝐴)
9695adantlr 714 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ ℝ) β†’ (𝑑 ∈ 𝑇 ↦ 𝑦) ∈ 𝐴)
97 stoweidlem59.15 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (π‘Ÿ ∈ 𝑇 ∧ 𝑑 ∈ 𝑇 ∧ π‘Ÿ β‰  𝑑)) β†’ βˆƒπ‘ž ∈ 𝐴 (π‘žβ€˜π‘Ÿ) β‰  (π‘žβ€˜π‘‘))
9897adantlr 714 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘Ÿ ∈ 𝑇 ∧ 𝑑 ∈ 𝑇 ∧ π‘Ÿ β‰  𝑑)) β†’ βˆƒπ‘ž ∈ 𝐴 (π‘žβ€˜π‘Ÿ) β‰  (π‘žβ€˜π‘‘))
9988uniexd 7670 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ βˆͺ 𝐽 ∈ V)
10087, 99eqeltrid 2843 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ 𝑇 ∈ V)
101100adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ 𝑇 ∈ V)
102 rabexg 5287 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑇 ∈ V β†’ {𝑑 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)} ∈ V)
103101, 102syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ {𝑑 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)} ∈ V)
10477fvmpt2 6955 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗 ∈ (0...𝑁) ∧ {𝑑 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)} ∈ V) β†’ (π΅β€˜π‘—) = {𝑑 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)})
10565, 103, 104syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ (π΅β€˜π‘—) = {𝑑 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)})
106 stoweidlem59.1 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑑𝐹
107 eqid 2738 . . . . . . . . . . . . . . . . . . . . . . . . 25 {𝑑 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)} = {𝑑 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)}
108 elfzelz 13370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0...𝑁) β†’ 𝑗 ∈ β„€)
109108zred 12540 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (0...𝑁) β†’ 𝑗 ∈ ℝ)
110 3re 12167 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3 ∈ ℝ
111 3ne0 12193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3 β‰  0
112110, 111rereccli 11854 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (1 / 3) ∈ ℝ
113 readdcl 11068 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ) β†’ (𝑗 + (1 / 3)) ∈ ℝ)
114109, 112, 113sylancl 587 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑁) β†’ (𝑗 + (1 / 3)) ∈ ℝ)
115114adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ (𝑗 + (1 / 3)) ∈ ℝ)
116 stoweidlem59.17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ 𝐸 ∈ ℝ+)
117116rpred 12886 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ 𝐸 ∈ ℝ)
118117adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ 𝐸 ∈ ℝ)
119115, 118remulcld 11119 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ ((𝑗 + (1 / 3)) Β· 𝐸) ∈ ℝ)
120 stoweidlem59.16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ 𝐹 ∈ 𝐢)
121120, 16eleqtrdi 2849 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ 𝐹 ∈ (𝐽 Cn 𝐾))
122121adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ 𝐹 ∈ (𝐽 Cn 𝐾))
123106, 86, 87, 107, 119, 122rfcnpre3 42971 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ {𝑑 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)} ∈ (Clsdβ€˜π½))
124105, 123eqeltrd 2839 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ (π΅β€˜π‘—) ∈ (Clsdβ€˜π½))
125 rabexg 5287 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑇 ∈ V β†’ {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)} ∈ V)
126101, 125syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)} ∈ V)
12769fvmpt2 6955 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗 ∈ (0...𝑁) ∧ {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)} ∈ V) β†’ (π·β€˜π‘—) = {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)})
12865, 126, 127syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ (π·β€˜π‘—) = {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)})
129 eqid 2738 . . . . . . . . . . . . . . . . . . . . . . . . 25 {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)} = {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)}
130 resubcl 11399 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ) β†’ (𝑗 βˆ’ (1 / 3)) ∈ ℝ)
131109, 112, 130sylancl 587 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑁) β†’ (𝑗 βˆ’ (1 / 3)) ∈ ℝ)
132131adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ (𝑗 βˆ’ (1 / 3)) ∈ ℝ)
133132, 118remulcld 11119 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸) ∈ ℝ)
134106, 86, 87, 129, 133, 122rfcnpre4 42972 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)} ∈ (Clsdβ€˜π½))
135128, 134eqeltrd 2839 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ (π·β€˜π‘—) ∈ (Clsdβ€˜π½))
136133adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑑 ∈ (π΅β€˜π‘—)) β†’ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸) ∈ ℝ)
137119adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑑 ∈ (π΅β€˜π‘—)) β†’ ((𝑗 + (1 / 3)) Β· 𝐸) ∈ ℝ)
13886, 87, 16, 120fcnre 42963 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (πœ‘ β†’ 𝐹:π‘‡βŸΆβ„)
139138ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑑 ∈ (π΅β€˜π‘—)) β†’ 𝐹:π‘‡βŸΆβ„)
140 ssrab2 4036 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 {𝑑 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)} βŠ† 𝑇
141105, 140eqsstrdi 3997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ (π΅β€˜π‘—) βŠ† 𝑇)
142141sselda 3943 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑑 ∈ (π΅β€˜π‘—)) β†’ 𝑑 ∈ 𝑇)
143139, 142ffvelcdmd 7031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑑 ∈ (π΅β€˜π‘—)) β†’ (πΉβ€˜π‘‘) ∈ ℝ)
144112, 130mpan2 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ β†’ (𝑗 βˆ’ (1 / 3)) ∈ ℝ)
145 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ β†’ 𝑗 ∈ ℝ)
146112, 113mpan2 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ β†’ (𝑗 + (1 / 3)) ∈ ℝ)
147 3pos 12192 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 0 < 3
148110, 147recgt0ii 11995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 0 < (1 / 3)
149112, 148elrpii 12847 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (1 / 3) ∈ ℝ+
150 ltsubrp 12880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ+) β†’ (𝑗 βˆ’ (1 / 3)) < 𝑗)
151149, 150mpan2 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ β†’ (𝑗 βˆ’ (1 / 3)) < 𝑗)
152 ltaddrp 12881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ+) β†’ 𝑗 < (𝑗 + (1 / 3)))
153149, 152mpan2 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ β†’ 𝑗 < (𝑗 + (1 / 3)))
154144, 145, 146, 151, 153lttrd 11250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 ∈ ℝ β†’ (𝑗 βˆ’ (1 / 3)) < (𝑗 + (1 / 3)))
155109, 154syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 ∈ (0...𝑁) β†’ (𝑗 βˆ’ (1 / 3)) < (𝑗 + (1 / 3)))
156155adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ (𝑗 βˆ’ (1 / 3)) < (𝑗 + (1 / 3)))
157116rpregt0d 12892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (πœ‘ β†’ (𝐸 ∈ ℝ ∧ 0 < 𝐸))
158157adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ (𝐸 ∈ ℝ ∧ 0 < 𝐸))
159 ltmul1 11939 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑗 βˆ’ (1 / 3)) ∈ ℝ ∧ (𝑗 + (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) β†’ ((𝑗 βˆ’ (1 / 3)) < (𝑗 + (1 / 3)) ↔ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸) < ((𝑗 + (1 / 3)) Β· 𝐸)))
160132, 115, 158, 159syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ ((𝑗 βˆ’ (1 / 3)) < (𝑗 + (1 / 3)) ↔ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸) < ((𝑗 + (1 / 3)) Β· 𝐸)))
161156, 160mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸) < ((𝑗 + (1 / 3)) Β· 𝐸))
162161adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑑 ∈ (π΅β€˜π‘—)) β†’ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸) < ((𝑗 + (1 / 3)) Β· 𝐸))
163105eleq2d 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ (𝑑 ∈ (π΅β€˜π‘—) ↔ 𝑑 ∈ {𝑑 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)}))
164163biimpa 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑑 ∈ (π΅β€˜π‘—)) β†’ 𝑑 ∈ {𝑑 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)})
165 rabid 3426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑑 ∈ {𝑑 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)} ↔ (𝑑 ∈ 𝑇 ∧ ((𝑗 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)))
166164, 165sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑑 ∈ (π΅β€˜π‘—)) β†’ (𝑑 ∈ 𝑇 ∧ ((𝑗 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)))
167166simprd 497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑑 ∈ (π΅β€˜π‘—)) β†’ ((𝑗 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘))
168136, 137, 143, 162, 167ltletrd 11249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑑 ∈ (π΅β€˜π‘—)) β†’ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸) < (πΉβ€˜π‘‘))
169136, 143ltnled 11236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑑 ∈ (π΅β€˜π‘—)) β†’ (((𝑗 βˆ’ (1 / 3)) Β· 𝐸) < (πΉβ€˜π‘‘) ↔ Β¬ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)))
170168, 169mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑑 ∈ (π΅β€˜π‘—)) β†’ Β¬ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸))
171170intnand 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑑 ∈ (π΅β€˜π‘—)) β†’ Β¬ (𝑑 ∈ 𝑇 ∧ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)))
172 rabid 3426 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑑 ∈ {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)} ↔ (𝑑 ∈ 𝑇 ∧ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)))
173171, 172sylnibr 329 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑑 ∈ (π΅β€˜π‘—)) β†’ Β¬ 𝑑 ∈ {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)})
174128adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑑 ∈ (π΅β€˜π‘—)) β†’ (π·β€˜π‘—) = {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)})
175173, 174neleqtrrd 2861 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑑 ∈ (π΅β€˜π‘—)) β†’ Β¬ 𝑑 ∈ (π·β€˜π‘—))
176175ex 414 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ (𝑑 ∈ (π΅β€˜π‘—) β†’ Β¬ 𝑑 ∈ (π·β€˜π‘—)))
17785, 176ralrimi 3239 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ βˆ€π‘‘ ∈ (π΅β€˜π‘—) Β¬ 𝑑 ∈ (π·β€˜π‘—))
178 disj 4406 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((π΅β€˜π‘—) ∩ (π·β€˜π‘—)) = βˆ… ↔ βˆ€π‘Ž ∈ (π΅β€˜π‘—) Β¬ π‘Ž ∈ (π·β€˜π‘—))
179 nfcv 2906 . . . . . . . . . . . . . . . . . . . . . . . . . 26 β„²π‘Ž(π΅β€˜π‘—)
18075nfcri 2893 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ⅎ𝑑 π‘Ž ∈ (π·β€˜π‘—)
181180nfn 1861 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Ⅎ𝑑 Β¬ π‘Ž ∈ (π·β€˜π‘—)
182 nfv 1918 . . . . . . . . . . . . . . . . . . . . . . . . . 26 β„²π‘Ž Β¬ 𝑑 ∈ (π·β€˜π‘—)
183 eleq1 2826 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (π‘Ž = 𝑑 β†’ (π‘Ž ∈ (π·β€˜π‘—) ↔ 𝑑 ∈ (π·β€˜π‘—)))
184183notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘Ž = 𝑑 β†’ (Β¬ π‘Ž ∈ (π·β€˜π‘—) ↔ Β¬ 𝑑 ∈ (π·β€˜π‘—)))
185179, 81, 181, 182, 184cbvralfw 3286 . . . . . . . . . . . . . . . . . . . . . . . . 25 (βˆ€π‘Ž ∈ (π΅β€˜π‘—) Β¬ π‘Ž ∈ (π·β€˜π‘—) ↔ βˆ€π‘‘ ∈ (π΅β€˜π‘—) Β¬ 𝑑 ∈ (π·β€˜π‘—))
186178, 185bitri 275 . . . . . . . . . . . . . . . . . . . . . . . 24 (((π΅β€˜π‘—) ∩ (π·β€˜π‘—)) = βˆ… ↔ βˆ€π‘‘ ∈ (π΅β€˜π‘—) Β¬ 𝑑 ∈ (π·β€˜π‘—))
187177, 186sylibr 233 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ ((π΅β€˜π‘—) ∩ (π·β€˜π‘—)) = βˆ…)
188 eqid 2738 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑇 βˆ– (π΅β€˜π‘—)) = (𝑇 βˆ– (π΅β€˜π‘—))
189 stoweidlem59.19 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ 𝑁 ∈ β„•)
190189nnrpd 12884 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝑁 ∈ ℝ+)
191116, 190rpdivcld 12903 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (𝐸 / 𝑁) ∈ ℝ+)
192191adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ (𝐸 / 𝑁) ∈ ℝ+)
193117, 189nndivred 12141 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ (𝐸 / 𝑁) ∈ ℝ)
194112a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ (1 / 3) ∈ ℝ)
195189nnge1d 12135 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ 1 ≀ 𝑁)
196 1re 11089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 1 ∈ ℝ
197 0lt1 11611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 0 < 1
198196, 197pm3.2i 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (1 ∈ ℝ ∧ 0 < 1)
199198a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ (1 ∈ ℝ ∧ 0 < 1))
200189nnred 12102 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ 𝑁 ∈ ℝ)
201189nngt0d 12136 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ 0 < 𝑁)
202 lediv2 11979 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((1 ∈ ℝ ∧ 0 < 1) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) β†’ (1 ≀ 𝑁 ↔ (𝐸 / 𝑁) ≀ (𝐸 / 1)))
203199, 200, 201, 157, 202syl121anc 1376 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ (1 ≀ 𝑁 ↔ (𝐸 / 𝑁) ≀ (𝐸 / 1)))
204195, 203mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ (𝐸 / 𝑁) ≀ (𝐸 / 1))
205116rpcnd 12888 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ 𝐸 ∈ β„‚)
206205div1d 11857 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ (𝐸 / 1) = 𝐸)
207204, 206breqtrd 5130 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ (𝐸 / 𝑁) ≀ 𝐸)
208 stoweidlem59.18 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝐸 < (1 / 3))
209193, 117, 194, 207, 208lelttrd 11247 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (𝐸 / 𝑁) < (1 / 3))
210209adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ (𝐸 / 𝑁) < (1 / 3))
21175, 82, 85, 86, 87, 16, 89, 90, 92, 94, 96, 98, 124, 135, 187, 188, 192, 210stoweidlem58 44009 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ βˆƒπ‘₯ ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘₯β€˜π‘‘) ∧ (π‘₯β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘₯β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘₯β€˜π‘‘)))
212 df-rex 3073 . . . . . . . . . . . . . . . . . . . . . 22 (βˆƒπ‘₯ ∈ 𝐴 (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘₯β€˜π‘‘) ∧ (π‘₯β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘₯β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘₯β€˜π‘‘)) ↔ βˆƒπ‘₯(π‘₯ ∈ 𝐴 ∧ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘₯β€˜π‘‘) ∧ (π‘₯β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘₯β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘₯β€˜π‘‘))))
213211, 212sylib 217 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ βˆƒπ‘₯(π‘₯ ∈ 𝐴 ∧ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘₯β€˜π‘‘) ∧ (π‘₯β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘₯β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘₯β€˜π‘‘))))
214 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘₯ ∈ 𝐴 ∧ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘₯β€˜π‘‘) ∧ (π‘₯β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘₯β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘₯β€˜π‘‘)))) β†’ π‘₯ ∈ 𝐴)
215 simprr1 1222 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘₯ ∈ 𝐴 ∧ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘₯β€˜π‘‘) ∧ (π‘₯β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘₯β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘₯β€˜π‘‘)))) β†’ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘₯β€˜π‘‘) ∧ (π‘₯β€˜π‘‘) ≀ 1))
216 fveq1 6837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 = π‘₯ β†’ (π‘¦β€˜π‘‘) = (π‘₯β€˜π‘‘))
217216breq2d 5116 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = π‘₯ β†’ (0 ≀ (π‘¦β€˜π‘‘) ↔ 0 ≀ (π‘₯β€˜π‘‘)))
218216breq1d 5114 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = π‘₯ β†’ ((π‘¦β€˜π‘‘) ≀ 1 ↔ (π‘₯β€˜π‘‘) ≀ 1))
219217, 218anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = π‘₯ β†’ ((0 ≀ (π‘¦β€˜π‘‘) ∧ (π‘¦β€˜π‘‘) ≀ 1) ↔ (0 ≀ (π‘₯β€˜π‘‘) ∧ (π‘₯β€˜π‘‘) ≀ 1)))
220219ralbidv 3173 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = π‘₯ β†’ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘¦β€˜π‘‘) ∧ (π‘¦β€˜π‘‘) ≀ 1) ↔ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘₯β€˜π‘‘) ∧ (π‘₯β€˜π‘‘) ≀ 1)))
221220, 1elrab2 3647 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ ∈ π‘Œ ↔ (π‘₯ ∈ 𝐴 ∧ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘₯β€˜π‘‘) ∧ (π‘₯β€˜π‘‘) ≀ 1)))
222214, 215, 221sylanbrc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘₯ ∈ 𝐴 ∧ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘₯β€˜π‘‘) ∧ (π‘₯β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘₯β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘₯β€˜π‘‘)))) β†’ π‘₯ ∈ π‘Œ)
223 simprr2 1223 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘₯ ∈ 𝐴 ∧ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘₯β€˜π‘‘) ∧ (π‘₯β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘₯β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘₯β€˜π‘‘)))) β†’ βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘₯β€˜π‘‘) < (𝐸 / 𝑁))
224 simprr3 1224 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘₯ ∈ 𝐴 ∧ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘₯β€˜π‘‘) ∧ (π‘₯β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘₯β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘₯β€˜π‘‘)))) β†’ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘₯β€˜π‘‘))
225223, 224jca 513 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘₯ ∈ 𝐴 ∧ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘₯β€˜π‘‘) ∧ (π‘₯β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘₯β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘₯β€˜π‘‘)))) β†’ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘₯β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘₯β€˜π‘‘)))
226 nfcv 2906 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑦π‘₯
227 nfv 1918 . . . . . . . . . . . . . . . . . . . . . . . . 25 Ⅎ𝑦(βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘₯β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘₯β€˜π‘‘))
228216breq1d 5114 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = π‘₯ β†’ ((π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ↔ (π‘₯β€˜π‘‘) < (𝐸 / 𝑁)))
229228ralbidv 3173 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = π‘₯ β†’ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ↔ βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘₯β€˜π‘‘) < (𝐸 / 𝑁)))
230216breq2d 5116 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = π‘₯ β†’ ((1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘) ↔ (1 βˆ’ (𝐸 / 𝑁)) < (π‘₯β€˜π‘‘)))
231230ralbidv 3173 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = π‘₯ β†’ (βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘) ↔ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘₯β€˜π‘‘)))
232229, 231anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = π‘₯ β†’ ((βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘)) ↔ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘₯β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘₯β€˜π‘‘))))
233226, 3, 227, 232elrabf 3640 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘₯ ∈ {𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))} ↔ (π‘₯ ∈ π‘Œ ∧ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘₯β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘₯β€˜π‘‘))))
234222, 225, 233sylanbrc 584 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ (π‘₯ ∈ 𝐴 ∧ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘₯β€˜π‘‘) ∧ (π‘₯β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘₯β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘₯β€˜π‘‘)))) β†’ π‘₯ ∈ {𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))})
235234ex 414 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ ((π‘₯ ∈ 𝐴 ∧ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘₯β€˜π‘‘) ∧ (π‘₯β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘₯β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘₯β€˜π‘‘))) β†’ π‘₯ ∈ {𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))}))
236235eximdv 1921 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ (βˆƒπ‘₯(π‘₯ ∈ 𝐴 ∧ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘₯β€˜π‘‘) ∧ (π‘₯β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘₯β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘₯β€˜π‘‘))) β†’ βˆƒπ‘₯ π‘₯ ∈ {𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))}))
237213, 236mpd 15 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ βˆƒπ‘₯ π‘₯ ∈ {𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))})
238 ne0i 4293 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ ∈ {𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))} β†’ {𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))} β‰  βˆ…)
239238exlimiv 1934 . . . . . . . . . . . . . . . . . . . 20 (βˆƒπ‘₯ π‘₯ ∈ {𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))} β†’ {𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))} β‰  βˆ…)
240237, 239syl 17 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ {𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))} β‰  βˆ…)
24168, 240eqnetrd 3010 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ (π»β€˜π‘—) β‰  βˆ…)
2422413adant3 1133 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁) ∧ (π»β€˜π‘—) = 𝑀) β†’ (π»β€˜π‘—) β‰  βˆ…)
24364, 242eqnetrrd 3011 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁) ∧ (π»β€˜π‘—) = 𝑀) β†’ 𝑀 β‰  βˆ…)
2442433exp 1120 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑗 ∈ (0...𝑁) β†’ ((π»β€˜π‘—) = 𝑀 β†’ 𝑀 β‰  βˆ…)))
245244rexlimdv 3149 . . . . . . . . . . . . . 14 (πœ‘ β†’ (βˆƒπ‘— ∈ (0...𝑁)(π»β€˜π‘—) = 𝑀 β†’ 𝑀 β‰  βˆ…))
246245adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀 ∈ ran 𝐻) β†’ (βˆƒπ‘— ∈ (0...𝑁)(π»β€˜π‘—) = 𝑀 β†’ 𝑀 β‰  βˆ…))
24763, 246mpd 15 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑀 ∈ ran 𝐻) β†’ 𝑀 β‰  βˆ…)
248247adantlr 714 . . . . . . . . . . 11 (((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) ∧ 𝑀 ∈ ran 𝐻) β†’ 𝑀 β‰  βˆ…)
249 rsp 3229 . . . . . . . . . . 11 (βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀) β†’ (𝑀 ∈ ran 𝐻 β†’ (𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀)))
25048, 49, 248, 249syl3c 66 . . . . . . . . . 10 (((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) ∧ 𝑀 ∈ ran 𝐻) β†’ (β„Žβ€˜π‘€) ∈ 𝑀)
251250ex 414 . . . . . . . . 9 ((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) β†’ (𝑀 ∈ ran 𝐻 β†’ (β„Žβ€˜π‘€) ∈ 𝑀))
25247, 251ralrimi 3239 . . . . . . . 8 ((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) β†’ βˆ€π‘€ ∈ ran 𝐻(β„Žβ€˜π‘€) ∈ 𝑀)
253 chfnrn 6995 . . . . . . . 8 ((β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(β„Žβ€˜π‘€) ∈ 𝑀) β†’ ran β„Ž βŠ† βˆͺ ran 𝐻)
25432, 252, 253syl2anc 585 . . . . . . 7 ((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) β†’ ran β„Ž βŠ† βˆͺ ran 𝐻)
255 nfv 1918 . . . . . . . . . 10 β„²π‘¦πœ‘
256 nfcv 2906 . . . . . . . . . . . 12 β„²π‘¦β„Ž
257 nfcv 2906 . . . . . . . . . . . . . . 15 Ⅎ𝑦(0...𝑁)
258 nfrab1 3425 . . . . . . . . . . . . . . 15 Ⅎ𝑦{𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))}
259257, 258nfmpt 5211 . . . . . . . . . . . . . 14 Ⅎ𝑦(𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))})
26022, 259nfcxfr 2904 . . . . . . . . . . . . 13 Ⅎ𝑦𝐻
261260nfrn 5904 . . . . . . . . . . . 12 Ⅎ𝑦ran 𝐻
262256, 261nffn 6597 . . . . . . . . . . 11 Ⅎ𝑦 β„Ž Fn ran 𝐻
263 nfv 1918 . . . . . . . . . . . 12 Ⅎ𝑦(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀)
264261, 263nfralw 3293 . . . . . . . . . . 11 β„²π‘¦βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀)
265262, 264nfan 1903 . . . . . . . . . 10 Ⅎ𝑦(β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))
266255, 265nfan 1903 . . . . . . . . 9 Ⅎ𝑦(πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀)))
267261nfuni 4871 . . . . . . . . 9 Ⅎ𝑦βˆͺ ran 𝐻
268 fnunirn 7196 . . . . . . . . . . . . . . 15 (𝐻 Fn (0...𝑁) β†’ (𝑦 ∈ βˆͺ ran 𝐻 ↔ βˆƒπ‘§ ∈ (0...𝑁)𝑦 ∈ (π»β€˜π‘§)))
269 nfcv 2906 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑗𝑧
27053, 269nffv 6848 . . . . . . . . . . . . . . . . 17 Ⅎ𝑗(π»β€˜π‘§)
271270nfcri 2893 . . . . . . . . . . . . . . . 16 Ⅎ𝑗 𝑦 ∈ (π»β€˜π‘§)
272 nfv 1918 . . . . . . . . . . . . . . . 16 Ⅎ𝑧 𝑦 ∈ (π»β€˜π‘—)
273 fveq2 6838 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑗 β†’ (π»β€˜π‘§) = (π»β€˜π‘—))
274273eleq2d 2824 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑗 β†’ (𝑦 ∈ (π»β€˜π‘§) ↔ 𝑦 ∈ (π»β€˜π‘—)))
275271, 272, 274cbvrexw 3289 . . . . . . . . . . . . . . 15 (βˆƒπ‘§ ∈ (0...𝑁)𝑦 ∈ (π»β€˜π‘§) ↔ βˆƒπ‘— ∈ (0...𝑁)𝑦 ∈ (π»β€˜π‘—))
276268, 275bitrdi 287 . . . . . . . . . . . . . 14 (𝐻 Fn (0...𝑁) β†’ (𝑦 ∈ βˆͺ ran 𝐻 ↔ βˆƒπ‘— ∈ (0...𝑁)𝑦 ∈ (π»β€˜π‘—)))
27724, 276syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑦 ∈ βˆͺ ran 𝐻 ↔ βˆƒπ‘— ∈ (0...𝑁)𝑦 ∈ (π»β€˜π‘—)))
278277biimpa 478 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ βˆͺ ran 𝐻) β†’ βˆƒπ‘— ∈ (0...𝑁)𝑦 ∈ (π»β€˜π‘—))
279 nfv 1918 . . . . . . . . . . . . . 14 β„²π‘—πœ‘
28053nfrn 5904 . . . . . . . . . . . . . . . 16 Ⅎ𝑗ran 𝐻
281280nfuni 4871 . . . . . . . . . . . . . . 15 Ⅎ𝑗βˆͺ ran 𝐻
282281nfcri 2893 . . . . . . . . . . . . . 14 Ⅎ𝑗 𝑦 ∈ βˆͺ ran 𝐻
283279, 282nfan 1903 . . . . . . . . . . . . 13 Ⅎ𝑗(πœ‘ ∧ 𝑦 ∈ βˆͺ ran 𝐻)
284 nfv 1918 . . . . . . . . . . . . 13 Ⅎ𝑗 𝑦 ∈ π‘Œ
285 simp1l 1198 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑦 ∈ βˆͺ ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (π»β€˜π‘—)) β†’ πœ‘)
286 simp2 1138 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑦 ∈ βˆͺ ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (π»β€˜π‘—)) β†’ 𝑗 ∈ (0...𝑁))
287 simp3 1139 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑦 ∈ βˆͺ ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (π»β€˜π‘—)) β†’ 𝑦 ∈ (π»β€˜π‘—))
28868eleq2d 2824 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ (𝑦 ∈ (π»β€˜π‘—) ↔ 𝑦 ∈ {𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))}))
289288biimpa 478 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (π»β€˜π‘—)) β†’ 𝑦 ∈ {𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))})
290 rabid 3426 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))} ↔ (𝑦 ∈ π‘Œ ∧ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))))
291289, 290sylib 217 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (π»β€˜π‘—)) β†’ (𝑦 ∈ π‘Œ ∧ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))))
292291simpld 496 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (π»β€˜π‘—)) β†’ 𝑦 ∈ π‘Œ)
293285, 286, 287, 292syl21anc 837 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑦 ∈ βˆͺ ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (π»β€˜π‘—)) β†’ 𝑦 ∈ π‘Œ)
2942933exp 1120 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑦 ∈ βˆͺ ran 𝐻) β†’ (𝑗 ∈ (0...𝑁) β†’ (𝑦 ∈ (π»β€˜π‘—) β†’ 𝑦 ∈ π‘Œ)))
295283, 284, 294rexlimd 3248 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑦 ∈ βˆͺ ran 𝐻) β†’ (βˆƒπ‘— ∈ (0...𝑁)𝑦 ∈ (π»β€˜π‘—) β†’ 𝑦 ∈ π‘Œ))
296278, 295mpd 15 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑦 ∈ βˆͺ ran 𝐻) β†’ 𝑦 ∈ π‘Œ)
297296adantlr 714 . . . . . . . . . 10 (((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) ∧ 𝑦 ∈ βˆͺ ran 𝐻) β†’ 𝑦 ∈ π‘Œ)
298297ex 414 . . . . . . . . 9 ((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) β†’ (𝑦 ∈ βˆͺ ran 𝐻 β†’ 𝑦 ∈ π‘Œ))
299266, 267, 3, 298ssrd 3948 . . . . . . . 8 ((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) β†’ βˆͺ ran 𝐻 βŠ† π‘Œ)
300 ssrab2 4036 . . . . . . . . 9 {𝑦 ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘¦β€˜π‘‘) ∧ (π‘¦β€˜π‘‘) ≀ 1)} βŠ† 𝐴
3011, 300eqsstri 3977 . . . . . . . 8 π‘Œ βŠ† 𝐴
302299, 301sstrdi 3955 . . . . . . 7 ((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) β†’ βˆͺ ran 𝐻 βŠ† 𝐴)
303254, 302sstrd 3953 . . . . . 6 ((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) β†’ ran β„Ž βŠ† 𝐴)
30442, 303fssd 6682 . . . . 5 ((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) β†’ β„Ž:ran 𝐻⟢𝐴)
305 dffn3 6677 . . . . . . 7 (𝐻 Fn (0...𝑁) ↔ 𝐻:(0...𝑁)⟢ran 𝐻)
30624, 305sylib 217 . . . . . 6 (πœ‘ β†’ 𝐻:(0...𝑁)⟢ran 𝐻)
307306adantr 482 . . . . 5 ((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) β†’ 𝐻:(0...𝑁)⟢ran 𝐻)
308 fco 6688 . . . . 5 ((β„Ž:ran 𝐻⟢𝐴 ∧ 𝐻:(0...𝑁)⟢ran 𝐻) β†’ (β„Ž ∘ 𝐻):(0...𝑁)⟢𝐴)
309304, 307, 308syl2anc 585 . . . 4 ((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) β†’ (β„Ž ∘ 𝐻):(0...𝑁)⟢𝐴)
310 nfcv 2906 . . . . . . . 8 β„²π‘—β„Ž
311310, 280nffn 6597 . . . . . . 7 Ⅎ𝑗 β„Ž Fn ran 𝐻
312 nfv 1918 . . . . . . . 8 Ⅎ𝑗(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀)
313280, 312nfralw 3293 . . . . . . 7 β„²π‘—βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀)
314311, 313nfan 1903 . . . . . 6 Ⅎ𝑗(β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))
315279, 314nfan 1903 . . . . 5 Ⅎ𝑗(πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀)))
316 simpll 766 . . . . . . . . . 10 (((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) ∧ 𝑗 ∈ (0...𝑁)) β†’ πœ‘)
317 simpr 486 . . . . . . . . . 10 (((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) ∧ 𝑗 ∈ (0...𝑁)) β†’ 𝑗 ∈ (0...𝑁))
31824ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) ∧ 𝑗 ∈ (0...𝑁)) β†’ 𝐻 Fn (0...𝑁))
319 fvco2 6934 . . . . . . . . . . . 12 ((𝐻 Fn (0...𝑁) ∧ 𝑗 ∈ (0...𝑁)) β†’ ((β„Ž ∘ 𝐻)β€˜π‘—) = (β„Žβ€˜(π»β€˜π‘—)))
320318, 319sylancom 589 . . . . . . . . . . 11 (((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) ∧ 𝑗 ∈ (0...𝑁)) β†’ ((β„Ž ∘ 𝐻)β€˜π‘—) = (β„Žβ€˜(π»β€˜π‘—)))
321 simplrr 777 . . . . . . . . . . . . 13 (((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) ∧ 𝑗 ∈ (0...𝑁)) β†’ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))
322 fnfun 6598 . . . . . . . . . . . . . . . 16 (𝐻 Fn (0...𝑁) β†’ Fun 𝐻)
32324, 322syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ Fun 𝐻)
324323ad2antrr 725 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) ∧ 𝑗 ∈ (0...𝑁)) β†’ Fun 𝐻)
32524fndmd 6603 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ dom 𝐻 = (0...𝑁))
326325adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ dom 𝐻 = (0...𝑁))
32765, 326eleqtrrd 2842 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) β†’ 𝑗 ∈ dom 𝐻)
328327adantlr 714 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) ∧ 𝑗 ∈ (0...𝑁)) β†’ 𝑗 ∈ dom 𝐻)
329 fvelrn 7023 . . . . . . . . . . . . . 14 ((Fun 𝐻 ∧ 𝑗 ∈ dom 𝐻) β†’ (π»β€˜π‘—) ∈ ran 𝐻)
330324, 328, 329syl2anc 585 . . . . . . . . . . . . 13 (((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) ∧ 𝑗 ∈ (0...𝑁)) β†’ (π»β€˜π‘—) ∈ ran 𝐻)
331321, 330jca 513 . . . . . . . . . . . 12 (((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) ∧ 𝑗 ∈ (0...𝑁)) β†’ (βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀) ∧ (π»β€˜π‘—) ∈ ran 𝐻))
332241adantlr 714 . . . . . . . . . . . 12 (((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) ∧ 𝑗 ∈ (0...𝑁)) β†’ (π»β€˜π‘—) β‰  βˆ…)
333 neeq1 3005 . . . . . . . . . . . . . 14 (𝑀 = (π»β€˜π‘—) β†’ (𝑀 β‰  βˆ… ↔ (π»β€˜π‘—) β‰  βˆ…))
334 fveq2 6838 . . . . . . . . . . . . . . 15 (𝑀 = (π»β€˜π‘—) β†’ (β„Žβ€˜π‘€) = (β„Žβ€˜(π»β€˜π‘—)))
335 id 22 . . . . . . . . . . . . . . 15 (𝑀 = (π»β€˜π‘—) β†’ 𝑀 = (π»β€˜π‘—))
336334, 335eleq12d 2833 . . . . . . . . . . . . . 14 (𝑀 = (π»β€˜π‘—) β†’ ((β„Žβ€˜π‘€) ∈ 𝑀 ↔ (β„Žβ€˜(π»β€˜π‘—)) ∈ (π»β€˜π‘—)))
337333, 336imbi12d 345 . . . . . . . . . . . . 13 (𝑀 = (π»β€˜π‘—) β†’ ((𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀) ↔ ((π»β€˜π‘—) β‰  βˆ… β†’ (β„Žβ€˜(π»β€˜π‘—)) ∈ (π»β€˜π‘—))))
338337rspccva 3579 . . . . . . . . . . . 12 ((βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀) ∧ (π»β€˜π‘—) ∈ ran 𝐻) β†’ ((π»β€˜π‘—) β‰  βˆ… β†’ (β„Žβ€˜(π»β€˜π‘—)) ∈ (π»β€˜π‘—)))
339331, 332, 338sylc 65 . . . . . . . . . . 11 (((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) ∧ 𝑗 ∈ (0...𝑁)) β†’ (β„Žβ€˜(π»β€˜π‘—)) ∈ (π»β€˜π‘—))
340320, 339eqeltrd 2839 . . . . . . . . . 10 (((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) ∧ 𝑗 ∈ (0...𝑁)) β†’ ((β„Ž ∘ 𝐻)β€˜π‘—) ∈ (π»β€˜π‘—))
341256, 260nfco 5818 . . . . . . . . . . . . 13 Ⅎ𝑦(β„Ž ∘ 𝐻)
342 nfcv 2906 . . . . . . . . . . . . 13 Ⅎ𝑦𝑗
343341, 342nffv 6848 . . . . . . . . . . . 12 Ⅎ𝑦((β„Ž ∘ 𝐻)β€˜π‘—)
344 nfv 1918 . . . . . . . . . . . . . 14 Ⅎ𝑦(πœ‘ ∧ 𝑗 ∈ (0...𝑁))
345260, 342nffv 6848 . . . . . . . . . . . . . . 15 Ⅎ𝑦(π»β€˜π‘—)
346343, 345nfel 2920 . . . . . . . . . . . . . 14 Ⅎ𝑦((β„Ž ∘ 𝐻)β€˜π‘—) ∈ (π»β€˜π‘—)
347344, 346nfan 1903 . . . . . . . . . . . . 13 Ⅎ𝑦((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((β„Ž ∘ 𝐻)β€˜π‘—) ∈ (π»β€˜π‘—))
348343, 3nfel 2920 . . . . . . . . . . . . 13 Ⅎ𝑦((β„Ž ∘ 𝐻)β€˜π‘—) ∈ π‘Œ
349347, 348nfim 1900 . . . . . . . . . . . 12 Ⅎ𝑦(((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((β„Ž ∘ 𝐻)β€˜π‘—) ∈ (π»β€˜π‘—)) β†’ ((β„Ž ∘ 𝐻)β€˜π‘—) ∈ π‘Œ)
350 eleq1 2826 . . . . . . . . . . . . . 14 (𝑦 = ((β„Ž ∘ 𝐻)β€˜π‘—) β†’ (𝑦 ∈ (π»β€˜π‘—) ↔ ((β„Ž ∘ 𝐻)β€˜π‘—) ∈ (π»β€˜π‘—)))
351350anbi2d 630 . . . . . . . . . . . . 13 (𝑦 = ((β„Ž ∘ 𝐻)β€˜π‘—) β†’ (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (π»β€˜π‘—)) ↔ ((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((β„Ž ∘ 𝐻)β€˜π‘—) ∈ (π»β€˜π‘—))))
352 eleq1 2826 . . . . . . . . . . . . 13 (𝑦 = ((β„Ž ∘ 𝐻)β€˜π‘—) β†’ (𝑦 ∈ π‘Œ ↔ ((β„Ž ∘ 𝐻)β€˜π‘—) ∈ π‘Œ))
353351, 352imbi12d 345 . . . . . . . . . . . 12 (𝑦 = ((β„Ž ∘ 𝐻)β€˜π‘—) β†’ ((((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (π»β€˜π‘—)) β†’ 𝑦 ∈ π‘Œ) ↔ (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((β„Ž ∘ 𝐻)β€˜π‘—) ∈ (π»β€˜π‘—)) β†’ ((β„Ž ∘ 𝐻)β€˜π‘—) ∈ π‘Œ)))
354343, 349, 353, 292vtoclgf 3522 . . . . . . . . . . 11 (((β„Ž ∘ 𝐻)β€˜π‘—) ∈ (π»β€˜π‘—) β†’ (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((β„Ž ∘ 𝐻)β€˜π‘—) ∈ (π»β€˜π‘—)) β†’ ((β„Ž ∘ 𝐻)β€˜π‘—) ∈ π‘Œ))
355354anabsi7 670 . . . . . . . . . 10 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((β„Ž ∘ 𝐻)β€˜π‘—) ∈ (π»β€˜π‘—)) β†’ ((β„Ž ∘ 𝐻)β€˜π‘—) ∈ π‘Œ)
356316, 317, 340, 355syl21anc 837 . . . . . . . . 9 (((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) ∧ 𝑗 ∈ (0...𝑁)) β†’ ((β„Ž ∘ 𝐻)β€˜π‘—) ∈ π‘Œ)
3571eleq2i 2830 . . . . . . . . . 10 (((β„Ž ∘ 𝐻)β€˜π‘—) ∈ π‘Œ ↔ ((β„Ž ∘ 𝐻)β€˜π‘—) ∈ {𝑦 ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘¦β€˜π‘‘) ∧ (π‘¦β€˜π‘‘) ≀ 1)})
358 nfcv 2906 . . . . . . . . . . 11 Ⅎ𝑦𝐴
359 nfcv 2906 . . . . . . . . . . . 12 Ⅎ𝑦𝑇
360 nfcv 2906 . . . . . . . . . . . . . 14 Ⅎ𝑦0
361 nfcv 2906 . . . . . . . . . . . . . 14 Ⅎ𝑦 ≀
362 nfcv 2906 . . . . . . . . . . . . . . 15 Ⅎ𝑦𝑑
363343, 362nffv 6848 . . . . . . . . . . . . . 14 Ⅎ𝑦(((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘)
364360, 361, 363nfbr 5151 . . . . . . . . . . . . 13 Ⅎ𝑦0 ≀ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘)
365 nfcv 2906 . . . . . . . . . . . . . 14 Ⅎ𝑦1
366363, 361, 365nfbr 5151 . . . . . . . . . . . . 13 Ⅎ𝑦(((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ≀ 1
367364, 366nfan 1903 . . . . . . . . . . . 12 Ⅎ𝑦(0 ≀ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ∧ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ≀ 1)
368359, 367nfralw 3293 . . . . . . . . . . 11 β„²π‘¦βˆ€π‘‘ ∈ 𝑇 (0 ≀ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ∧ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ≀ 1)
369 nfcv 2906 . . . . . . . . . . . . 13 Ⅎ𝑑𝑦
370 nfcv 2906 . . . . . . . . . . . . . . 15 β„²π‘‘β„Ž
371 nfra1 3266 . . . . . . . . . . . . . . . . . . 19 β„²π‘‘βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁)
372 nfra1 3266 . . . . . . . . . . . . . . . . . . 19 β„²π‘‘βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘)
373371, 372nfan 1903 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑑(βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))
374 nfra1 3266 . . . . . . . . . . . . . . . . . . . 20 β„²π‘‘βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘¦β€˜π‘‘) ∧ (π‘¦β€˜π‘‘) ≀ 1)
375 nfcv 2906 . . . . . . . . . . . . . . . . . . . 20 Ⅎ𝑑𝐴
376374, 375nfrabw 3439 . . . . . . . . . . . . . . . . . . 19 Ⅎ𝑑{𝑦 ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘¦β€˜π‘‘) ∧ (π‘¦β€˜π‘‘) ≀ 1)}
3771, 376nfcxfr 2904 . . . . . . . . . . . . . . . . . 18 β„²π‘‘π‘Œ
378373, 377nfrabw 3439 . . . . . . . . . . . . . . . . 17 Ⅎ𝑑{𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))}
37970, 378nfmpt 5211 . . . . . . . . . . . . . . . 16 Ⅎ𝑑(𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ π‘Œ ∣ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))})
38022, 379nfcxfr 2904 . . . . . . . . . . . . . . 15 Ⅎ𝑑𝐻
381370, 380nfco 5818 . . . . . . . . . . . . . 14 Ⅎ𝑑(β„Ž ∘ 𝐻)
382381, 74nffv 6848 . . . . . . . . . . . . 13 Ⅎ𝑑((β„Ž ∘ 𝐻)β€˜π‘—)
383369, 382nfeq 2919 . . . . . . . . . . . 12 Ⅎ𝑑 𝑦 = ((β„Ž ∘ 𝐻)β€˜π‘—)
384 fveq1 6837 . . . . . . . . . . . . . 14 (𝑦 = ((β„Ž ∘ 𝐻)β€˜π‘—) β†’ (π‘¦β€˜π‘‘) = (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘))
385384breq2d 5116 . . . . . . . . . . . . 13 (𝑦 = ((β„Ž ∘ 𝐻)β€˜π‘—) β†’ (0 ≀ (π‘¦β€˜π‘‘) ↔ 0 ≀ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘)))
386384breq1d 5114 . . . . . . . . . . . . 13 (𝑦 = ((β„Ž ∘ 𝐻)β€˜π‘—) β†’ ((π‘¦β€˜π‘‘) ≀ 1 ↔ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ≀ 1))
387385, 386anbi12d 632 . . . . . . . . . . . 12 (𝑦 = ((β„Ž ∘ 𝐻)β€˜π‘—) β†’ ((0 ≀ (π‘¦β€˜π‘‘) ∧ (π‘¦β€˜π‘‘) ≀ 1) ↔ (0 ≀ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ∧ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ≀ 1)))
388383, 387ralbid 3255 . . . . . . . . . . 11 (𝑦 = ((β„Ž ∘ 𝐻)β€˜π‘—) β†’ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘¦β€˜π‘‘) ∧ (π‘¦β€˜π‘‘) ≀ 1) ↔ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ∧ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ≀ 1)))
389343, 358, 368, 388elrabf 3640 . . . . . . . . . 10 (((β„Ž ∘ 𝐻)β€˜π‘—) ∈ {𝑦 ∈ 𝐴 ∣ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (π‘¦β€˜π‘‘) ∧ (π‘¦β€˜π‘‘) ≀ 1)} ↔ (((β„Ž ∘ 𝐻)β€˜π‘—) ∈ 𝐴 ∧ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ∧ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ≀ 1)))
390357, 389bitri 275 . . . . . . . . 9 (((β„Ž ∘ 𝐻)β€˜π‘—) ∈ π‘Œ ↔ (((β„Ž ∘ 𝐻)β€˜π‘—) ∈ 𝐴 ∧ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ∧ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ≀ 1)))
391356, 390sylib 217 . . . . . . . 8 (((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) ∧ 𝑗 ∈ (0...𝑁)) β†’ (((β„Ž ∘ 𝐻)β€˜π‘—) ∈ 𝐴 ∧ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ∧ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ≀ 1)))
392391simprd 497 . . . . . . 7 (((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) ∧ 𝑗 ∈ (0...𝑁)) β†’ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ∧ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ≀ 1))
393 nfcv 2906 . . . . . . . . . . . 12 Ⅎ𝑦(π·β€˜π‘—)
394 nfcv 2906 . . . . . . . . . . . . 13 Ⅎ𝑦 <
395 nfcv 2906 . . . . . . . . . . . . 13 Ⅎ𝑦(𝐸 / 𝑁)
396363, 394, 395nfbr 5151 . . . . . . . . . . . 12 Ⅎ𝑦(((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁)
397393, 396nfralw 3293 . . . . . . . . . . 11 β„²π‘¦βˆ€π‘‘ ∈ (π·β€˜π‘—)(((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁)
398347, 397nfim 1900 . . . . . . . . . 10 Ⅎ𝑦(((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((β„Ž ∘ 𝐻)β€˜π‘—) ∈ (π»β€˜π‘—)) β†’ βˆ€π‘‘ ∈ (π·β€˜π‘—)(((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁))
399384breq1d 5114 . . . . . . . . . . . 12 (𝑦 = ((β„Ž ∘ 𝐻)β€˜π‘—) β†’ ((π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ↔ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁)))
400383, 399ralbid 3255 . . . . . . . . . . 11 (𝑦 = ((β„Ž ∘ 𝐻)β€˜π‘—) β†’ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ↔ βˆ€π‘‘ ∈ (π·β€˜π‘—)(((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁)))
401351, 400imbi12d 345 . . . . . . . . . 10 (𝑦 = ((β„Ž ∘ 𝐻)β€˜π‘—) β†’ ((((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (π»β€˜π‘—)) β†’ βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁)) ↔ (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((β„Ž ∘ 𝐻)β€˜π‘—) ∈ (π»β€˜π‘—)) β†’ βˆ€π‘‘ ∈ (π·β€˜π‘—)(((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁))))
402291simprd 497 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (π»β€˜π‘—)) β†’ (βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘)))
403402simpld 496 . . . . . . . . . 10 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (π»β€˜π‘—)) β†’ βˆ€π‘‘ ∈ (π·β€˜π‘—)(π‘¦β€˜π‘‘) < (𝐸 / 𝑁))
404343, 398, 401, 403vtoclgf 3522 . . . . . . . . 9 (((β„Ž ∘ 𝐻)β€˜π‘—) ∈ (π»β€˜π‘—) β†’ (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((β„Ž ∘ 𝐻)β€˜π‘—) ∈ (π»β€˜π‘—)) β†’ βˆ€π‘‘ ∈ (π·β€˜π‘—)(((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁)))
405404anabsi7 670 . . . . . . . 8 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((β„Ž ∘ 𝐻)β€˜π‘—) ∈ (π»β€˜π‘—)) β†’ βˆ€π‘‘ ∈ (π·β€˜π‘—)(((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁))
406316, 317, 340, 405syl21anc 837 . . . . . . 7 (((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) ∧ 𝑗 ∈ (0...𝑁)) β†’ βˆ€π‘‘ ∈ (π·β€˜π‘—)(((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁))
407 nfcv 2906 . . . . . . . . . . . 12 Ⅎ𝑦(π΅β€˜π‘—)
408 nfcv 2906 . . . . . . . . . . . . 13 Ⅎ𝑦(1 βˆ’ (𝐸 / 𝑁))
409408, 394, 363nfbr 5151 . . . . . . . . . . . 12 Ⅎ𝑦(1 βˆ’ (𝐸 / 𝑁)) < (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘)
410407, 409nfralw 3293 . . . . . . . . . . 11 β„²π‘¦βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘)
411347, 410nfim 1900 . . . . . . . . . 10 Ⅎ𝑦(((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((β„Ž ∘ 𝐻)β€˜π‘—) ∈ (π»β€˜π‘—)) β†’ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘))
412384breq2d 5116 . . . . . . . . . . . 12 (𝑦 = ((β„Ž ∘ 𝐻)β€˜π‘—) β†’ ((1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘) ↔ (1 βˆ’ (𝐸 / 𝑁)) < (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘)))
413383, 412ralbid 3255 . . . . . . . . . . 11 (𝑦 = ((β„Ž ∘ 𝐻)β€˜π‘—) β†’ (βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘) ↔ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘)))
414351, 413imbi12d 345 . . . . . . . . . 10 (𝑦 = ((β„Ž ∘ 𝐻)β€˜π‘—) β†’ ((((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (π»β€˜π‘—)) β†’ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘)) ↔ (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((β„Ž ∘ 𝐻)β€˜π‘—) ∈ (π»β€˜π‘—)) β†’ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘))))
415402simprd 497 . . . . . . . . . 10 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (π»β€˜π‘—)) β†’ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (π‘¦β€˜π‘‘))
416343, 411, 414, 415vtoclgf 3522 . . . . . . . . 9 (((β„Ž ∘ 𝐻)β€˜π‘—) ∈ (π»β€˜π‘—) β†’ (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((β„Ž ∘ 𝐻)β€˜π‘—) ∈ (π»β€˜π‘—)) β†’ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘)))
417416anabsi7 670 . . . . . . . 8 (((πœ‘ ∧ 𝑗 ∈ (0...𝑁)) ∧ ((β„Ž ∘ 𝐻)β€˜π‘—) ∈ (π»β€˜π‘—)) β†’ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘))
418316, 317, 340, 417syl21anc 837 . . . . . . 7 (((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) ∧ 𝑗 ∈ (0...𝑁)) β†’ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘))
419392, 406, 4183jca 1129 . . . . . 6 (((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) ∧ 𝑗 ∈ (0...𝑁)) β†’ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ∧ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)(((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘)))
420419ex 414 . . . . 5 ((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) β†’ (𝑗 ∈ (0...𝑁) β†’ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ∧ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)(((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘))))
421315, 420ralrimi 3239 . . . 4 ((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) β†’ βˆ€π‘— ∈ (0...𝑁)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ∧ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)(((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘)))
422309, 421jca 513 . . 3 ((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) β†’ ((β„Ž ∘ 𝐻):(0...𝑁)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑁)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ∧ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)(((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘))))
423 feq1 6645 . . . . 5 (π‘₯ = (β„Ž ∘ 𝐻) β†’ (π‘₯:(0...𝑁)⟢𝐴 ↔ (β„Ž ∘ 𝐻):(0...𝑁)⟢𝐴))
424 nfcv 2906 . . . . . . 7 Ⅎ𝑗π‘₯
425310, 53nfco 5818 . . . . . . 7 Ⅎ𝑗(β„Ž ∘ 𝐻)
426424, 425nfeq 2919 . . . . . 6 Ⅎ𝑗 π‘₯ = (β„Ž ∘ 𝐻)
427 nfcv 2906 . . . . . . . . 9 Ⅎ𝑑π‘₯
428427, 381nfeq 2919 . . . . . . . 8 Ⅎ𝑑 π‘₯ = (β„Ž ∘ 𝐻)
429 fveq1 6837 . . . . . . . . . . 11 (π‘₯ = (β„Ž ∘ 𝐻) β†’ (π‘₯β€˜π‘—) = ((β„Ž ∘ 𝐻)β€˜π‘—))
430429fveq1d 6840 . . . . . . . . . 10 (π‘₯ = (β„Ž ∘ 𝐻) β†’ ((π‘₯β€˜π‘—)β€˜π‘‘) = (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘))
431430breq2d 5116 . . . . . . . . 9 (π‘₯ = (β„Ž ∘ 𝐻) β†’ (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ↔ 0 ≀ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘)))
432430breq1d 5114 . . . . . . . . 9 (π‘₯ = (β„Ž ∘ 𝐻) β†’ (((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1 ↔ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ≀ 1))
433431, 432anbi12d 632 . . . . . . . 8 (π‘₯ = (β„Ž ∘ 𝐻) β†’ ((0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ↔ (0 ≀ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ∧ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ≀ 1)))
434428, 433ralbid 3255 . . . . . . 7 (π‘₯ = (β„Ž ∘ 𝐻) β†’ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ↔ βˆ€π‘‘ ∈ 𝑇 (0 ≀ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ∧ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ≀ 1)))
435430breq1d 5114 . . . . . . . 8 (π‘₯ = (β„Ž ∘ 𝐻) β†’ (((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁) ↔ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁)))
436428, 435ralbid 3255 . . . . . . 7 (π‘₯ = (β„Ž ∘ 𝐻) β†’ (βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁) ↔ βˆ€π‘‘ ∈ (π·β€˜π‘—)(((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁)))
437430breq2d 5116 . . . . . . . 8 (π‘₯ = (β„Ž ∘ 𝐻) β†’ ((1 βˆ’ (𝐸 / 𝑁)) < ((π‘₯β€˜π‘—)β€˜π‘‘) ↔ (1 βˆ’ (𝐸 / 𝑁)) < (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘)))
438428, 437ralbid 3255 . . . . . . 7 (π‘₯ = (β„Ž ∘ 𝐻) β†’ (βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < ((π‘₯β€˜π‘—)β€˜π‘‘) ↔ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘)))
439434, 436, 4383anbi123d 1437 . . . . . 6 (π‘₯ = (β„Ž ∘ 𝐻) β†’ ((βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < ((π‘₯β€˜π‘—)β€˜π‘‘)) ↔ (βˆ€π‘‘ ∈ 𝑇 (0 ≀ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ∧ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)(((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘))))
440426, 439ralbid 3255 . . . . 5 (π‘₯ = (β„Ž ∘ 𝐻) β†’ (βˆ€π‘— ∈ (0...𝑁)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < ((π‘₯β€˜π‘—)β€˜π‘‘)) ↔ βˆ€π‘— ∈ (0...𝑁)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ∧ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)(((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘))))
441423, 440anbi12d 632 . . . 4 (π‘₯ = (β„Ž ∘ 𝐻) β†’ ((π‘₯:(0...𝑁)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑁)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < ((π‘₯β€˜π‘—)β€˜π‘‘))) ↔ ((β„Ž ∘ 𝐻):(0...𝑁)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑁)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ∧ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)(((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘)))))
442441spcegv 3555 . . 3 ((β„Ž ∘ 𝐻) ∈ V β†’ (((β„Ž ∘ 𝐻):(0...𝑁)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑁)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ∧ (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)(((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < (((β„Ž ∘ 𝐻)β€˜π‘—)β€˜π‘‘))) β†’ βˆƒπ‘₯(π‘₯:(0...𝑁)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑁)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < ((π‘₯β€˜π‘—)β€˜π‘‘)))))
44340, 422, 442sylc 65 . 2 ((πœ‘ ∧ (β„Ž Fn ran 𝐻 ∧ βˆ€π‘€ ∈ ran 𝐻(𝑀 β‰  βˆ… β†’ (β„Žβ€˜π‘€) ∈ 𝑀))) β†’ βˆƒπ‘₯(π‘₯:(0...𝑁)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑁)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < ((π‘₯β€˜π‘—)β€˜π‘‘))))
44431, 443exlimddv 1939 1 (πœ‘ β†’ βˆƒπ‘₯(π‘₯:(0...𝑁)⟢𝐴 ∧ βˆ€π‘— ∈ (0...𝑁)(βˆ€π‘‘ ∈ 𝑇 (0 ≀ ((π‘₯β€˜π‘—)β€˜π‘‘) ∧ ((π‘₯β€˜π‘—)β€˜π‘‘) ≀ 1) ∧ βˆ€π‘‘ ∈ (π·β€˜π‘—)((π‘₯β€˜π‘—)β€˜π‘‘) < (𝐸 / 𝑁) ∧ βˆ€π‘‘ ∈ (π΅β€˜π‘—)(1 βˆ’ (𝐸 / 𝑁)) < ((π‘₯β€˜π‘—)β€˜π‘‘))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542  βˆƒwex 1782  β„²wnf 1786   ∈ wcel 2107  β„²wnfc 2886   β‰  wne 2942  βˆ€wral 3063  βˆƒwrex 3072  {crab 3406  Vcvv 3444   βˆ– cdif 3906   ∩ cin 3908   βŠ† wss 3909  βˆ…c0 4281  βˆͺ cuni 4864   class class class wbr 5104   ↦ cmpt 5187  dom cdm 5631  ran crn 5632   ∘ ccom 5635  Fun wfun 6486   Fn wfn 6487  βŸΆwf 6488  β€˜cfv 6492  (class class class)co 7350  Fincfn 8817  β„cr 10984  0cc0 10985  1c1 10986   + caddc 10988   Β· cmul 10990   < clt 11123   ≀ cle 11124   βˆ’ cmin 11319   / cdiv 11746  β„•cn 12087  3c3 12143  β„+crp 12844  (,)cioo 13193  ...cfz 13353  topGenctg 17254  Clsdccld 22289   Cn ccn 22497  Compccmp 22659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709  ax-rep 5241  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7663  ax-inf2 9511  ax-cnex 11041  ax-resscn 11042  ax-1cn 11043  ax-icn 11044  ax-addcl 11045  ax-addrcl 11046  ax-mulcl 11047  ax-mulrcl 11048  ax-mulcom 11049  ax-addass 11050  ax-mulass 11051  ax-distr 11052  ax-i2m1 11053  ax-1ne0 11054  ax-1rid 11055  ax-rnegex 11056  ax-rrecex 11057  ax-cnre 11058  ax-pre-lttri 11059  ax-pre-lttrn 11060  ax-pre-ltadd 11061  ax-pre-mulgt0 11062  ax-pre-sup 11063  ax-mulf 11065
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-uni 4865  df-int 4907  df-iun 4955  df-iin 4956  df-br 5105  df-opab 5167  df-mpt 5188  df-tr 5222  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-se 5587  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6250  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6444  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7306  df-ov 7353  df-oprab 7354  df-mpo 7355  df-of 7608  df-om 7794  df-1st 7912  df-2nd 7913  df-supp 8061  df-frecs 8180  df-wrecs 8211  df-recs 8285  df-rdg 8324  df-1o 8380  df-2o 8381  df-er 8582  df-map 8701  df-pm 8702  df-ixp 8770  df-en 8818  df-dom 8819  df-sdom 8820  df-fin 8821  df-fsupp 9240  df-fi 9281  df-sup 9312  df-inf 9313  df-oi 9380  df-card 9809  df-pnf 11125  df-mnf 11126  df-xr 11127  df-ltxr 11128  df-le 11129  df-sub 11321  df-neg 11322  df-div 11747  df-nn 12088  df-2 12150  df-3 12151  df-4 12152  df-5 12153  df-6 12154  df-7 12155  df-8 12156  df-9 12157  df-n0 12348  df-z 12434  df-dec 12552  df-uz 12697  df-q 12803  df-rp 12845  df-xneg 12962  df-xadd 12963  df-xmul 12964  df-ioo 13197  df-ioc 13198  df-ico 13199  df-icc 13200  df-fz 13354  df-fzo 13497  df-fl 13626  df-seq 13836  df-exp 13897  df-hash 14159  df-cj 14918  df-re 14919  df-im 14920  df-sqrt 15054  df-abs 15055  df-clim 15305  df-rlim 15306  df-sum 15506  df-struct 16954  df-sets 16971  df-slot 16989  df-ndx 17001  df-base 17019  df-ress 17048  df-plusg 17081  df-mulr 17082  df-starv 17083  df-sca 17084  df-vsca 17085  df-ip 17086  df-tset 17087  df-ple 17088  df-ds 17090  df-unif 17091  df-hom 17092  df-cco 17093  df-rest 17239  df-topn 17240  df-0g 17258  df-gsum 17259  df-topgen 17260  df-pt 17261  df-prds 17264  df-xrs 17319  df-qtop 17324  df-imas 17325  df-xps 17327  df-mre 17401  df-mrc 17402  df-acs 17404  df-mgm 18432  df-sgrp 18481  df-mnd 18492  df-submnd 18537  df-mulg 18807  df-cntz 19029  df-cmn 19493  df-psmet 20711  df-xmet 20712  df-met 20713  df-bl 20714  df-mopn 20715  df-cnfld 20720  df-top 22165  df-topon 22182  df-topsp 22204  df-bases 22218  df-cld 22292  df-cn 22500  df-cnp 22501  df-cmp 22660  df-tx 22835  df-hmeo 23028  df-xms 23595  df-ms 23596  df-tms 23597
This theorem is referenced by:  stoweidlem60  44011
  Copyright terms: Public domain W3C validator