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 40039
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 - \epslon / 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 3117 . . . . . . . . . 10 𝑦{𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)}
31, 2nfcxfr 2760 . . . . . . . . 9 𝑦𝑌
4 nfcv 2762 . . . . . . . . 9 𝑧𝑌
5 nfv 1841 . . . . . . . . 9 𝑧(∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))
6 nfv 1841 . . . . . . . . 9 𝑦(∀𝑡 ∈ (𝐷𝑗)(𝑧𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑧𝑡))
7 fveq1 6177 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝑦𝑡) = (𝑧𝑡))
87breq1d 4654 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝑦𝑡) < (𝐸 / 𝑁) ↔ (𝑧𝑡) < (𝐸 / 𝑁)))
98ralbidv 2983 . . . . . . . . . 10 (𝑦 = 𝑧 → (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷𝑗)(𝑧𝑡) < (𝐸 / 𝑁)))
107breq2d 4656 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ (1 − (𝐸 / 𝑁)) < (𝑧𝑡)))
1110ralbidv 2983 . . . . . . . . . 10 (𝑦 = 𝑧 → (∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑧𝑡)))
129, 11anbi12d 746 . . . . . . . . 9 (𝑦 = 𝑧 → ((∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡)) ↔ (∀𝑡 ∈ (𝐷𝑗)(𝑧𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑧𝑡))))
133, 4, 5, 6, 12cbvrab 3193 . . . . . . . 8 {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} = {𝑧𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑧𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑧𝑡))}
14 ovexd 6665 . . . . . . . . . 10 (𝜑 → (𝐽 Cn 𝐾) ∈ V)
15 stoweidlem59.11 . . . . . . . . . . 11 (𝜑𝐴𝐶)
16 stoweidlem59.5 . . . . . . . . . . 11 𝐶 = (𝐽 Cn 𝐾)
1715, 16syl6sseq 3643 . . . . . . . . . 10 (𝜑𝐴 ⊆ (𝐽 Cn 𝐾))
1814, 17ssexd 4796 . . . . . . . . 9 (𝜑𝐴 ∈ V)
191, 18rabexd 4805 . . . . . . . 8 (𝜑𝑌 ∈ V)
2013, 19rabexd 4805 . . . . . . 7 (𝜑 → {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ∈ V)
2120ralrimivw 2964 . . . . . 6 (𝜑 → ∀𝑗 ∈ (0...𝑁){𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ∈ V)
22 stoweidlem59.9 . . . . . . 7 𝐻 = (𝑗 ∈ (0...𝑁) ↦ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
2322fnmpt 6007 . . . . . 6 (∀𝑗 ∈ (0...𝑁){𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ∈ V → 𝐻 Fn (0...𝑁))
2421, 23syl 17 . . . . 5 (𝜑𝐻 Fn (0...𝑁))
25 fzfi 12754 . . . . 5 (0...𝑁) ∈ Fin
26 fnfi 8223 . . . . 5 ((𝐻 Fn (0...𝑁) ∧ (0...𝑁) ∈ Fin) → 𝐻 ∈ Fin)
2724, 25, 26sylancl 693 . . . 4 (𝜑𝐻 ∈ Fin)
28 rnfi 8234 . . . 4 (𝐻 ∈ Fin → ran 𝐻 ∈ Fin)
2927, 28syl 17 . . 3 (𝜑 → ran 𝐻 ∈ Fin)
30 fnchoice 39008 . . 3 (ran 𝐻 ∈ Fin → ∃( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)))
3129, 30syl 17 . 2 (𝜑 → ∃( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)))
32 simprl 793 . . . . 5 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → Fn ran 𝐻)
33 ovex 6663 . . . . . . . 8 (0...𝑁) ∈ V
3433mptex 6471 . . . . . . 7 (𝑗 ∈ (0...𝑁) ↦ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}) ∈ V
3522, 34eqeltri 2695 . . . . . 6 𝐻 ∈ V
3635rnex 7085 . . . . 5 ran 𝐻 ∈ V
37 fnex 6466 . . . . 5 (( Fn ran 𝐻 ∧ ran 𝐻 ∈ V) → ∈ V)
3832, 36, 37sylancl 693 . . . 4 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ∈ V)
39 coexg 7102 . . . 4 (( ∈ V ∧ 𝐻 ∈ V) → (𝐻) ∈ V)
4038, 35, 39sylancl 693 . . 3 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → (𝐻) ∈ V)
41 dffn3 6041 . . . . . . 7 ( Fn ran 𝐻:ran 𝐻⟶ran )
4232, 41sylib 208 . . . . . 6 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → :ran 𝐻⟶ran )
43 nfv 1841 . . . . . . . . . 10 𝑤𝜑
44 nfv 1841 . . . . . . . . . . 11 𝑤 Fn ran 𝐻
45 nfra1 2938 . . . . . . . . . . 11 𝑤𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)
4644, 45nfan 1826 . . . . . . . . . 10 𝑤( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))
4743, 46nfan 1826 . . . . . . . . 9 𝑤(𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)))
48 simplrr 800 . . . . . . . . . . 11 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))
49 simpr 477 . . . . . . . . . . 11 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → 𝑤 ∈ ran 𝐻)
50 fvelrnb 6230 . . . . . . . . . . . . . . . 16 (𝐻 Fn (0...𝑁) → (𝑤 ∈ ran 𝐻 ↔ ∃𝑎 ∈ (0...𝑁)(𝐻𝑎) = 𝑤))
51 nfv 1841 . . . . . . . . . . . . . . . . 17 𝑎(𝐻𝑗) = 𝑤
52 nfmpt1 4738 . . . . . . . . . . . . . . . . . . . 20 𝑗(𝑗 ∈ (0...𝑁) ↦ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
5322, 52nfcxfr 2760 . . . . . . . . . . . . . . . . . . 19 𝑗𝐻
54 nfcv 2762 . . . . . . . . . . . . . . . . . . 19 𝑗𝑎
5553, 54nffv 6185 . . . . . . . . . . . . . . . . . 18 𝑗(𝐻𝑎)
56 nfcv 2762 . . . . . . . . . . . . . . . . . 18 𝑗𝑤
5755, 56nfeq 2773 . . . . . . . . . . . . . . . . 17 𝑗(𝐻𝑎) = 𝑤
58 fveq2 6178 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑎 → (𝐻𝑗) = (𝐻𝑎))
5958eqeq1d 2622 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑎 → ((𝐻𝑗) = 𝑤 ↔ (𝐻𝑎) = 𝑤))
6051, 57, 59cbvrex 3163 . . . . . . . . . . . . . . . 16 (∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤 ↔ ∃𝑎 ∈ (0...𝑁)(𝐻𝑎) = 𝑤)
6150, 60syl6bbr 278 . . . . . . . . . . . . . . 15 (𝐻 Fn (0...𝑁) → (𝑤 ∈ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤))
6224, 61syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑤 ∈ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤))
6362biimpa 501 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ran 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤)
64 simp3 1061 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑁) ∧ (𝐻𝑗) = 𝑤) → (𝐻𝑗) = 𝑤)
65 simpr 477 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
6620adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ∈ V)
6722fvmpt2 6278 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ (0...𝑁) ∧ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ∈ V) → (𝐻𝑗) = {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
6865, 66, 67syl2anc 692 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐻𝑗) = {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
69 stoweidlem59.6 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
70 nfcv 2762 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡(0...𝑁)
71 nfrab1 3117 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡{𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}
7270, 71nfmpt 4737 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
7369, 72nfcxfr 2760 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡𝐷
74 nfcv 2762 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡𝑗
7573, 74nffv 6185 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝐷𝑗)
76 nfcv 2762 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡𝑇
77 stoweidlem59.7 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
78 nfrab1 3117 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑡{𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)}
7970, 78nfmpt 4737 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
8077, 79nfcxfr 2760 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡𝐵
8180, 74nffv 6185 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡(𝐵𝑗)
8276, 81nfdif 3723 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝑇 ∖ (𝐵𝑗))
83 stoweidlem59.2 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡𝜑
84 nfv 1841 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡 𝑗 ∈ (0...𝑁)
8583, 84nfan 1826 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝜑𝑗 ∈ (0...𝑁))
86 stoweidlem59.3 . . . . . . . . . . . . . . . . . . . . . . 23 𝐾 = (topGen‘ran (,))
87 stoweidlem59.4 . . . . . . . . . . . . . . . . . . . . . . 23 𝑇 = 𝐽
88 stoweidlem59.10 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐽 ∈ Comp)
8988adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → 𝐽 ∈ Comp)
9015adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → 𝐴𝐶)
91 stoweidlem59.12 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
92913adant1r 1317 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
93 stoweidlem59.13 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
94933adant1r 1317 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
95 stoweidlem59.14 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ ℝ) → (𝑡𝑇𝑦) ∈ 𝐴)
9695adantlr 750 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ ℝ) → (𝑡𝑇𝑦) ∈ 𝐴)
97 stoweidlem59.15 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟𝑇𝑡𝑇𝑟𝑡)) → ∃𝑞𝐴 (𝑞𝑟) ≠ (𝑞𝑡))
9897adantlr 750 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑟𝑇𝑡𝑇𝑟𝑡)) → ∃𝑞𝐴 (𝑞𝑟) ≠ (𝑞𝑡))
99 uniexg 6940 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐽 ∈ Comp → 𝐽 ∈ V)
10088, 99syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 𝐽 ∈ V)
10187, 100syl5eqel 2703 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑇 ∈ V)
102101adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇 ∈ V)
103 rabexg 4803 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑇 ∈ V → {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V)
104102, 103syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V)
10577fvmpt2 6278 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗 ∈ (0...𝑁) ∧ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V) → (𝐵𝑗) = {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
10665, 104, 105syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐵𝑗) = {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
107 stoweidlem59.1 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡𝐹
108 eqid 2620 . . . . . . . . . . . . . . . . . . . . . . . . 25 {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} = {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)}
109 elfzelz 12327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
110109zred 11467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
111 3re 11079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3 ∈ ℝ
112 3ne0 11100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3 ≠ 0
113111, 112rereccli 10775 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (1 / 3) ∈ ℝ
114 readdcl 10004 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ) → (𝑗 + (1 / 3)) ∈ ℝ)
115110, 113, 114sylancl 693 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑁) → (𝑗 + (1 / 3)) ∈ ℝ)
116115adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑗 + (1 / 3)) ∈ ℝ)
117 stoweidlem59.17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐸 ∈ ℝ+)
118117rpred 11857 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐸 ∈ ℝ)
119118adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → 𝐸 ∈ ℝ)
120116, 119remulcld 10055 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑗 + (1 / 3)) · 𝐸) ∈ ℝ)
121 stoweidlem59.16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐹𝐶)
122121, 16syl6eleq 2709 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐹 ∈ (𝐽 Cn 𝐾))
123122adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → 𝐹 ∈ (𝐽 Cn 𝐾))
124107, 86, 87, 108, 120, 123rfcnpre3 39012 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ (Clsd‘𝐽))
125106, 124eqeltrd 2699 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐵𝑗) ∈ (Clsd‘𝐽))
126 rabexg 4803 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V)
127102, 126syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V)
12869fvmpt2 6278 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗 ∈ (0...𝑁) ∧ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V) → (𝐷𝑗) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
12965, 127, 128syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐷𝑗) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
130 eqid 2620 . . . . . . . . . . . . . . . . . . . . . . . . 25 {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}
131 resubcl 10330 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ) → (𝑗 − (1 / 3)) ∈ ℝ)
132110, 113, 131sylancl 693 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑁) → (𝑗 − (1 / 3)) ∈ ℝ)
133132adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑗 − (1 / 3)) ∈ ℝ)
134133, 119remulcld 10055 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ)
135107, 86, 87, 130, 134, 123rfcnpre4 39013 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ (Clsd‘𝐽))
136129, 135eqeltrd 2699 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐷𝑗) ∈ (Clsd‘𝐽))
137134adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ)
138120adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ((𝑗 + (1 / 3)) · 𝐸) ∈ ℝ)
13986, 87, 16, 121fcnre 39004 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝐹:𝑇⟶ℝ)
140139ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → 𝐹:𝑇⟶ℝ)
141 ssrab2 3679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ⊆ 𝑇
142106, 141syl6eqss 3647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐵𝑗) ⊆ 𝑇)
143142sselda 3595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → 𝑡𝑇)
144140, 143ffvelrnd 6346 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → (𝐹𝑡) ∈ ℝ)
145113, 131mpan2 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) ∈ ℝ)
146 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ → 𝑗 ∈ ℝ)
147113, 114mpan2 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ → (𝑗 + (1 / 3)) ∈ ℝ)
148 3pos 11099 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 0 < 3
149111, 148recgt0ii 10914 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 0 < (1 / 3)
150113, 149elrpii 11820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (1 / 3) ∈ ℝ+
151 ltsubrp 11851 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ+) → (𝑗 − (1 / 3)) < 𝑗)
152150, 151mpan2 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) < 𝑗)
153 ltaddrp 11852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ+) → 𝑗 < (𝑗 + (1 / 3)))
154150, 153mpan2 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ → 𝑗 < (𝑗 + (1 / 3)))
155145, 146, 147, 152, 154lttrd 10183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
156110, 155syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 ∈ (0...𝑁) → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
157156adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
158117rpregt0d 11863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
159158adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
160 ltmul1 10858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑗 − (1 / 3)) ∈ ℝ ∧ (𝑗 + (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑗 − (1 / 3)) < (𝑗 + (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸)))
161133, 116, 159, 160syl3anc 1324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) < (𝑗 + (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸)))
162157, 161mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸))
163162adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸))
164106eleq2d 2685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑡 ∈ (𝐵𝑗) ↔ 𝑡 ∈ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)}))
165164biimpa 501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → 𝑡 ∈ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
166 rabid 3111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑡 ∈ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ↔ (𝑡𝑇 ∧ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)))
167165, 166sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → (𝑡𝑇 ∧ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)))
168167simprd 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡))
169137, 138, 144, 163, 168ltletrd 10182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) < (𝐹𝑡))
170137, 144ltnled 10169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → (((𝑗 − (1 / 3)) · 𝐸) < (𝐹𝑡) ↔ ¬ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
171169, 170mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ¬ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))
172171intnand 961 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ¬ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
173 rabid 3111 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
174172, 173sylnibr 319 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ¬ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
175129adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → (𝐷𝑗) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
176174, 175neleqtrrd 2721 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ¬ 𝑡 ∈ (𝐷𝑗))
177176ex 450 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑡 ∈ (𝐵𝑗) → ¬ 𝑡 ∈ (𝐷𝑗)))
17885, 177ralrimi 2954 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐵𝑗) ¬ 𝑡 ∈ (𝐷𝑗))
179 disj 4008 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐵𝑗) ∩ (𝐷𝑗)) = ∅ ↔ ∀𝑎 ∈ (𝐵𝑗) ¬ 𝑎 ∈ (𝐷𝑗))
180 nfcv 2762 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑎(𝐵𝑗)
18175nfcri 2756 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑡 𝑎 ∈ (𝐷𝑗)
182181nfn 1782 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡 ¬ 𝑎 ∈ (𝐷𝑗)
183 nfv 1841 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑎 ¬ 𝑡 ∈ (𝐷𝑗)
184 eleq1 2687 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑡 → (𝑎 ∈ (𝐷𝑗) ↔ 𝑡 ∈ (𝐷𝑗)))
185184notbid 308 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = 𝑡 → (¬ 𝑎 ∈ (𝐷𝑗) ↔ ¬ 𝑡 ∈ (𝐷𝑗)))
186180, 81, 182, 183, 185cbvralf 3160 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑎 ∈ (𝐵𝑗) ¬ 𝑎 ∈ (𝐷𝑗) ↔ ∀𝑡 ∈ (𝐵𝑗) ¬ 𝑡 ∈ (𝐷𝑗))
187179, 186bitri 264 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐵𝑗) ∩ (𝐷𝑗)) = ∅ ↔ ∀𝑡 ∈ (𝐵𝑗) ¬ 𝑡 ∈ (𝐷𝑗))
188178, 187sylibr 224 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝐵𝑗) ∩ (𝐷𝑗)) = ∅)
189 eqid 2620 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑇 ∖ (𝐵𝑗)) = (𝑇 ∖ (𝐵𝑗))
190 stoweidlem59.19 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑁 ∈ ℕ)
191190nnrpd 11855 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑁 ∈ ℝ+)
192117, 191rpdivcld 11874 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐸 / 𝑁) ∈ ℝ+)
193192adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐸 / 𝑁) ∈ ℝ+)
194118, 190nndivred 11054 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐸 / 𝑁) ∈ ℝ)
195113a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (1 / 3) ∈ ℝ)
196190nnge1d 11048 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → 1 ≤ 𝑁)
197 1re 10024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 1 ∈ ℝ
198 0lt1 10535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 0 < 1
199197, 198pm3.2i 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (1 ∈ ℝ ∧ 0 < 1)
200199a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (1 ∈ ℝ ∧ 0 < 1))
201190nnred 11020 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑁 ∈ ℝ)
202190nngt0d 11049 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → 0 < 𝑁)
203 lediv2 10898 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((1 ∈ ℝ ∧ 0 < 1) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (1 ≤ 𝑁 ↔ (𝐸 / 𝑁) ≤ (𝐸 / 1)))
204200, 201, 202, 158, 203syl121anc 1329 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (1 ≤ 𝑁 ↔ (𝐸 / 𝑁) ≤ (𝐸 / 1)))
205196, 204mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐸 / 𝑁) ≤ (𝐸 / 1))
206117rpcnd 11859 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐸 ∈ ℂ)
207206div1d 10778 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐸 / 1) = 𝐸)
208205, 207breqtrd 4670 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐸 / 𝑁) ≤ 𝐸)
209 stoweidlem59.18 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐸 < (1 / 3))
210194, 118, 195, 208, 209lelttrd 10180 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐸 / 𝑁) < (1 / 3))
211210adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐸 / 𝑁) < (1 / 3))
21275, 82, 85, 86, 87, 16, 89, 90, 92, 94, 96, 98, 125, 136, 188, 189, 193, 211stoweidlem58 40038 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (0...𝑁)) → ∃𝑥𝐴 (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))
213 df-rex 2915 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑥𝐴 (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)) ↔ ∃𝑥(𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))))
214212, 213sylib 208 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0...𝑁)) → ∃𝑥(𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))))
215 simprl 793 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → 𝑥𝐴)
216 simprr1 1107 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → ∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1))
217 fveq1 6177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 = 𝑥 → (𝑦𝑡) = (𝑥𝑡))
218217breq2d 4656 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = 𝑥 → (0 ≤ (𝑦𝑡) ↔ 0 ≤ (𝑥𝑡)))
219217breq1d 4654 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = 𝑥 → ((𝑦𝑡) ≤ 1 ↔ (𝑥𝑡) ≤ 1))
220218, 219anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = 𝑥 → ((0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1) ↔ (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1)))
221220ralbidv 2983 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑥 → (∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1)))
222221, 1elrab2 3360 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥𝑌 ↔ (𝑥𝐴 ∧ ∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1)))
223215, 216, 222sylanbrc 697 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → 𝑥𝑌)
224 simprr2 1108 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁))
225 simprr3 1109 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))
226224, 225jca 554 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → (∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))
227 nfcv 2762 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦𝑥
228 nfv 1841 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦(∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))
229217breq1d 4654 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = 𝑥 → ((𝑦𝑡) < (𝐸 / 𝑁) ↔ (𝑥𝑡) < (𝐸 / 𝑁)))
230229ralbidv 2983 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑥 → (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁)))
231217breq2d 4656 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = 𝑥 → ((1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ (1 − (𝐸 / 𝑁)) < (𝑥𝑡)))
232231ralbidv 2983 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑥 → (∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))
233230, 232anbi12d 746 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑥 → ((∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡)) ↔ (∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))))
234227, 3, 228, 233elrabf 3354 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ↔ (𝑥𝑌 ∧ (∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))))
235223, 226, 234sylanbrc 697 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → 𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
236235ex 450 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))) → 𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}))
237236eximdv 1844 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0...𝑁)) → (∃𝑥(𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))) → ∃𝑥 𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}))
238214, 237mpd 15 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑁)) → ∃𝑥 𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
239 ne0i 3913 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} → {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ≠ ∅)
240239exlimiv 1856 . . . . . . . . . . . . . . . . . . . 20 (∃𝑥 𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} → {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ≠ ∅)
241238, 240syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ≠ ∅)
24268, 241eqnetrd 2858 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐻𝑗) ≠ ∅)
2432423adant3 1079 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑁) ∧ (𝐻𝑗) = 𝑤) → (𝐻𝑗) ≠ ∅)
24464, 243eqnetrrd 2859 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑁) ∧ (𝐻𝑗) = 𝑤) → 𝑤 ≠ ∅)
2452443exp 1262 . . . . . . . . . . . . . . 15 (𝜑 → (𝑗 ∈ (0...𝑁) → ((𝐻𝑗) = 𝑤𝑤 ≠ ∅)))
246245rexlimdv 3026 . . . . . . . . . . . . . 14 (𝜑 → (∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤𝑤 ≠ ∅))
247246adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ran 𝐻) → (∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤𝑤 ≠ ∅))
24863, 247mpd 15 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ran 𝐻) → 𝑤 ≠ ∅)
249248adantlr 750 . . . . . . . . . . 11 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → 𝑤 ≠ ∅)
250 rsp 2926 . . . . . . . . . . 11 (∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤) → (𝑤 ∈ ran 𝐻 → (𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)))
25148, 49, 249, 250syl3c 66 . . . . . . . . . 10 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → (𝑤) ∈ 𝑤)
252251ex 450 . . . . . . . . 9 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → (𝑤 ∈ ran 𝐻 → (𝑤) ∈ 𝑤))
25347, 252ralrimi 2954 . . . . . . . 8 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ∀𝑤 ∈ ran 𝐻(𝑤) ∈ 𝑤)
254 chfnrn 6314 . . . . . . . 8 (( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤) ∈ 𝑤) → ran ran 𝐻)
25532, 253, 254syl2anc 692 . . . . . . 7 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ran ran 𝐻)
256 nfv 1841 . . . . . . . . . 10 𝑦𝜑
257 nfcv 2762 . . . . . . . . . . . 12 𝑦
258 nfcv 2762 . . . . . . . . . . . . . . 15 𝑦(0...𝑁)
259 nfrab1 3117 . . . . . . . . . . . . . . 15 𝑦{𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}
260258, 259nfmpt 4737 . . . . . . . . . . . . . 14 𝑦(𝑗 ∈ (0...𝑁) ↦ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
26122, 260nfcxfr 2760 . . . . . . . . . . . . 13 𝑦𝐻
262261nfrn 5357 . . . . . . . . . . . 12 𝑦ran 𝐻
263257, 262nffn 5975 . . . . . . . . . . 11 𝑦 Fn ran 𝐻
264 nfv 1841 . . . . . . . . . . . 12 𝑦(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)
265262, 264nfral 2942 . . . . . . . . . . 11 𝑦𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)
266263, 265nfan 1826 . . . . . . . . . 10 𝑦( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))
267256, 266nfan 1826 . . . . . . . . 9 𝑦(𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)))
268262nfuni 4433 . . . . . . . . 9 𝑦 ran 𝐻
269 fnunirn 6496 . . . . . . . . . . . . . . 15 (𝐻 Fn (0...𝑁) → (𝑦 ran 𝐻 ↔ ∃𝑧 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑧)))
270 nfcv 2762 . . . . . . . . . . . . . . . . . 18 𝑗𝑧
27153, 270nffv 6185 . . . . . . . . . . . . . . . . 17 𝑗(𝐻𝑧)
272271nfcri 2756 . . . . . . . . . . . . . . . 16 𝑗 𝑦 ∈ (𝐻𝑧)
273 nfv 1841 . . . . . . . . . . . . . . . 16 𝑧 𝑦 ∈ (𝐻𝑗)
274 fveq2 6178 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑗 → (𝐻𝑧) = (𝐻𝑗))
275274eleq2d 2685 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑗 → (𝑦 ∈ (𝐻𝑧) ↔ 𝑦 ∈ (𝐻𝑗)))
276272, 273, 275cbvrex 3163 . . . . . . . . . . . . . . 15 (∃𝑧 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑧) ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑗))
277269, 276syl6bb 276 . . . . . . . . . . . . . 14 (𝐻 Fn (0...𝑁) → (𝑦 ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑗)))
27824, 277syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑦 ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑗)))
279278biimpa 501 . . . . . . . . . . . 12 ((𝜑𝑦 ran 𝐻) → ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑗))
280 nfv 1841 . . . . . . . . . . . . . 14 𝑗𝜑
28153nfrn 5357 . . . . . . . . . . . . . . . 16 𝑗ran 𝐻
282281nfuni 4433 . . . . . . . . . . . . . . 15 𝑗 ran 𝐻
283282nfcri 2756 . . . . . . . . . . . . . 14 𝑗 𝑦 ran 𝐻
284280, 283nfan 1826 . . . . . . . . . . . . 13 𝑗(𝜑𝑦 ran 𝐻)
285 nfv 1841 . . . . . . . . . . . . 13 𝑗 𝑦𝑌
286 simp1l 1083 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝜑)
287 simp2 1060 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑗 ∈ (0...𝑁))
288 simp3 1061 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑦 ∈ (𝐻𝑗))
28968eleq2d 2685 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑦 ∈ (𝐻𝑗) ↔ 𝑦 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}))
290289biimpa 501 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑦 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
291 rabid 3111 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ↔ (𝑦𝑌 ∧ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))))
292290, 291sylib 208 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → (𝑦𝑌 ∧ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))))
293292simpld 475 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑦𝑌)
294286, 287, 288, 293syl21anc 1323 . . . . . . . . . . . . . 14 (((𝜑𝑦 ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑦𝑌)
2952943exp 1262 . . . . . . . . . . . . 13 ((𝜑𝑦 ran 𝐻) → (𝑗 ∈ (0...𝑁) → (𝑦 ∈ (𝐻𝑗) → 𝑦𝑌)))
296284, 285, 295rexlimd 3022 . . . . . . . . . . . 12 ((𝜑𝑦 ran 𝐻) → (∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑗) → 𝑦𝑌))
297279, 296mpd 15 . . . . . . . . . . 11 ((𝜑𝑦 ran 𝐻) → 𝑦𝑌)
298297adantlr 750 . . . . . . . . . 10 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑦 ran 𝐻) → 𝑦𝑌)
299298ex 450 . . . . . . . . 9 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → (𝑦 ran 𝐻𝑦𝑌))
300267, 268, 3, 299ssrd 3600 . . . . . . . 8 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ran 𝐻𝑌)
301 ssrab2 3679 . . . . . . . . 9 {𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)} ⊆ 𝐴
3021, 301eqsstri 3627 . . . . . . . 8 𝑌𝐴
303300, 302syl6ss 3607 . . . . . . 7 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ran 𝐻𝐴)
304255, 303sstrd 3605 . . . . . 6 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ran 𝐴)
30542, 304fssd 6044 . . . . 5 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → :ran 𝐻𝐴)
306 dffn3 6041 . . . . . . 7 (𝐻 Fn (0...𝑁) ↔ 𝐻:(0...𝑁)⟶ran 𝐻)
30724, 306sylib 208 . . . . . 6 (𝜑𝐻:(0...𝑁)⟶ran 𝐻)
308307adantr 481 . . . . 5 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → 𝐻:(0...𝑁)⟶ran 𝐻)
309 fco 6045 . . . . 5 ((:ran 𝐻𝐴𝐻:(0...𝑁)⟶ran 𝐻) → (𝐻):(0...𝑁)⟶𝐴)
310305, 308, 309syl2anc 692 . . . 4 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → (𝐻):(0...𝑁)⟶𝐴)
311 nfcv 2762 . . . . . . . 8 𝑗
312311, 281nffn 5975 . . . . . . 7 𝑗 Fn ran 𝐻
313 nfv 1841 . . . . . . . 8 𝑗(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)
314281, 313nfral 2942 . . . . . . 7 𝑗𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)
315312, 314nfan 1826 . . . . . 6 𝑗( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))
316280, 315nfan 1826 . . . . 5 𝑗(𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)))
317 simpll 789 . . . . . . . . . 10 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝜑)
318 simpr 477 . . . . . . . . . 10 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
31924ad2antrr 761 . . . . . . . . . . . 12 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝐻 Fn (0...𝑁))
320 fvco2 6260 . . . . . . . . . . . 12 ((𝐻 Fn (0...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → ((𝐻)‘𝑗) = (‘(𝐻𝑗)))
321319, 320sylancom 700 . . . . . . . . . . 11 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝐻)‘𝑗) = (‘(𝐻𝑗)))
322 simplrr 800 . . . . . . . . . . . . 13 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))
323 fnfun 5976 . . . . . . . . . . . . . . . 16 (𝐻 Fn (0...𝑁) → Fun 𝐻)
32424, 323syl 17 . . . . . . . . . . . . . . 15 (𝜑 → Fun 𝐻)
325324ad2antrr 761 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → Fun 𝐻)
326 fndm 5978 . . . . . . . . . . . . . . . . . 18 (𝐻 Fn (0...𝑁) → dom 𝐻 = (0...𝑁))
32724, 326syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → dom 𝐻 = (0...𝑁))
328327adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑁)) → dom 𝐻 = (0...𝑁))
32965, 328eleqtrrd 2702 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑗 ∈ dom 𝐻)
330329adantlr 750 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ dom 𝐻)
331 fvelrn 6338 . . . . . . . . . . . . . 14 ((Fun 𝐻𝑗 ∈ dom 𝐻) → (𝐻𝑗) ∈ ran 𝐻)
332325, 330, 331syl2anc 692 . . . . . . . . . . . . 13 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (𝐻𝑗) ∈ ran 𝐻)
333322, 332jca 554 . . . . . . . . . . . 12 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤) ∧ (𝐻𝑗) ∈ ran 𝐻))
334242adantlr 750 . . . . . . . . . . . 12 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (𝐻𝑗) ≠ ∅)
335 neeq1 2853 . . . . . . . . . . . . . 14 (𝑤 = (𝐻𝑗) → (𝑤 ≠ ∅ ↔ (𝐻𝑗) ≠ ∅))
336 fveq2 6178 . . . . . . . . . . . . . . 15 (𝑤 = (𝐻𝑗) → (𝑤) = (‘(𝐻𝑗)))
337 id 22 . . . . . . . . . . . . . . 15 (𝑤 = (𝐻𝑗) → 𝑤 = (𝐻𝑗))
338336, 337eleq12d 2693 . . . . . . . . . . . . . 14 (𝑤 = (𝐻𝑗) → ((𝑤) ∈ 𝑤 ↔ (‘(𝐻𝑗)) ∈ (𝐻𝑗)))
339335, 338imbi12d 334 . . . . . . . . . . . . 13 (𝑤 = (𝐻𝑗) → ((𝑤 ≠ ∅ → (𝑤) ∈ 𝑤) ↔ ((𝐻𝑗) ≠ ∅ → (‘(𝐻𝑗)) ∈ (𝐻𝑗))))
340339rspccva 3303 . . . . . . . . . . . 12 ((∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤) ∧ (𝐻𝑗) ∈ ran 𝐻) → ((𝐻𝑗) ≠ ∅ → (‘(𝐻𝑗)) ∈ (𝐻𝑗)))
341333, 334, 340sylc 65 . . . . . . . . . . 11 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (‘(𝐻𝑗)) ∈ (𝐻𝑗))
342321, 341eqeltrd 2699 . . . . . . . . . 10 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝐻)‘𝑗) ∈ (𝐻𝑗))
343257, 261nfco 5276 . . . . . . . . . . . . 13 𝑦(𝐻)
344 nfcv 2762 . . . . . . . . . . . . 13 𝑦𝑗
345343, 344nffv 6185 . . . . . . . . . . . 12 𝑦((𝐻)‘𝑗)
346 nfv 1841 . . . . . . . . . . . . . 14 𝑦(𝜑𝑗 ∈ (0...𝑁))
347261, 344nffv 6185 . . . . . . . . . . . . . . 15 𝑦(𝐻𝑗)
348345, 347nfel 2774 . . . . . . . . . . . . . 14 𝑦((𝐻)‘𝑗) ∈ (𝐻𝑗)
349346, 348nfan 1826 . . . . . . . . . . . . 13 𝑦((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗))
350345, 3nfel 2774 . . . . . . . . . . . . 13 𝑦((𝐻)‘𝑗) ∈ 𝑌
351349, 350nfim 1823 . . . . . . . . . . . 12 𝑦(((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ((𝐻)‘𝑗) ∈ 𝑌)
352 eleq1 2687 . . . . . . . . . . . . . 14 (𝑦 = ((𝐻)‘𝑗) → (𝑦 ∈ (𝐻𝑗) ↔ ((𝐻)‘𝑗) ∈ (𝐻𝑗)))
353352anbi2d 739 . . . . . . . . . . . . 13 (𝑦 = ((𝐻)‘𝑗) → (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) ↔ ((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗))))
354 eleq1 2687 . . . . . . . . . . . . 13 (𝑦 = ((𝐻)‘𝑗) → (𝑦𝑌 ↔ ((𝐻)‘𝑗) ∈ 𝑌))
355353, 354imbi12d 334 . . . . . . . . . . . 12 (𝑦 = ((𝐻)‘𝑗) → ((((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑦𝑌) ↔ (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ((𝐻)‘𝑗) ∈ 𝑌)))
356345, 351, 355, 293vtoclgf 3259 . . . . . . . . . . 11 (((𝐻)‘𝑗) ∈ (𝐻𝑗) → (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ((𝐻)‘𝑗) ∈ 𝑌))
357356anabsi7 859 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ((𝐻)‘𝑗) ∈ 𝑌)
358317, 318, 342, 357syl21anc 1323 . . . . . . . . 9 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝐻)‘𝑗) ∈ 𝑌)
3591eleq2i 2691 . . . . . . . . . 10 (((𝐻)‘𝑗) ∈ 𝑌 ↔ ((𝐻)‘𝑗) ∈ {𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)})
360 nfcv 2762 . . . . . . . . . . 11 𝑦𝐴
361 nfcv 2762 . . . . . . . . . . . 12 𝑦𝑇
362 nfcv 2762 . . . . . . . . . . . . . 14 𝑦0
363 nfcv 2762 . . . . . . . . . . . . . 14 𝑦
364 nfcv 2762 . . . . . . . . . . . . . . 15 𝑦𝑡
365345, 364nffv 6185 . . . . . . . . . . . . . 14 𝑦(((𝐻)‘𝑗)‘𝑡)
366362, 363, 365nfbr 4690 . . . . . . . . . . . . 13 𝑦0 ≤ (((𝐻)‘𝑗)‘𝑡)
367 nfcv 2762 . . . . . . . . . . . . . 14 𝑦1
368365, 363, 367nfbr 4690 . . . . . . . . . . . . 13 𝑦(((𝐻)‘𝑗)‘𝑡) ≤ 1
369366, 368nfan 1826 . . . . . . . . . . . 12 𝑦(0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)
370361, 369nfral 2942 . . . . . . . . . . 11 𝑦𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)
371 nfcv 2762 . . . . . . . . . . . . 13 𝑡𝑦
372 nfcv 2762 . . . . . . . . . . . . . . 15 𝑡
373 nfra1 2938 . . . . . . . . . . . . . . . . . . 19 𝑡𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁)
374 nfra1 2938 . . . . . . . . . . . . . . . . . . 19 𝑡𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡)
375373, 374nfan 1826 . . . . . . . . . . . . . . . . . 18 𝑡(∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))
376 nfra1 2938 . . . . . . . . . . . . . . . . . . . 20 𝑡𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)
377 nfcv 2762 . . . . . . . . . . . . . . . . . . . 20 𝑡𝐴
378376, 377nfrab 3118 . . . . . . . . . . . . . . . . . . 19 𝑡{𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)}
3791, 378nfcxfr 2760 . . . . . . . . . . . . . . . . . 18 𝑡𝑌
380375, 379nfrab 3118 . . . . . . . . . . . . . . . . 17 𝑡{𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}
38170, 380nfmpt 4737 . . . . . . . . . . . . . . . 16 𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
38222, 381nfcxfr 2760 . . . . . . . . . . . . . . 15 𝑡𝐻
383372, 382nfco 5276 . . . . . . . . . . . . . 14 𝑡(𝐻)
384383, 74nffv 6185 . . . . . . . . . . . . 13 𝑡((𝐻)‘𝑗)
385371, 384nfeq 2773 . . . . . . . . . . . 12 𝑡 𝑦 = ((𝐻)‘𝑗)
386 fveq1 6177 . . . . . . . . . . . . . 14 (𝑦 = ((𝐻)‘𝑗) → (𝑦𝑡) = (((𝐻)‘𝑗)‘𝑡))
387386breq2d 4656 . . . . . . . . . . . . 13 (𝑦 = ((𝐻)‘𝑗) → (0 ≤ (𝑦𝑡) ↔ 0 ≤ (((𝐻)‘𝑗)‘𝑡)))
388386breq1d 4654 . . . . . . . . . . . . 13 (𝑦 = ((𝐻)‘𝑗) → ((𝑦𝑡) ≤ 1 ↔ (((𝐻)‘𝑗)‘𝑡) ≤ 1))
389387, 388anbi12d 746 . . . . . . . . . . . 12 (𝑦 = ((𝐻)‘𝑗) → ((0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1) ↔ (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
390385, 389ralbid 2980 . . . . . . . . . . 11 (𝑦 = ((𝐻)‘𝑗) → (∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
391345, 360, 370, 390elrabf 3354 . . . . . . . . . 10 (((𝐻)‘𝑗) ∈ {𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)} ↔ (((𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
392359, 391bitri 264 . . . . . . . . 9 (((𝐻)‘𝑗) ∈ 𝑌 ↔ (((𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
393358, 392sylib 208 . . . . . . . 8 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (((𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
394393simprd 479 . . . . . . 7 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1))
395 nfcv 2762 . . . . . . . . . . . 12 𝑦(𝐷𝑗)
396 nfcv 2762 . . . . . . . . . . . . 13 𝑦 <
397 nfcv 2762 . . . . . . . . . . . . 13 𝑦(𝐸 / 𝑁)
398365, 396, 397nfbr 4690 . . . . . . . . . . . 12 𝑦(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)
399395, 398nfral 2942 . . . . . . . . . . 11 𝑦𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)
400349, 399nfim 1823 . . . . . . . . . 10 𝑦(((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))
401386breq1d 4654 . . . . . . . . . . . 12 (𝑦 = ((𝐻)‘𝑗) → ((𝑦𝑡) < (𝐸 / 𝑁) ↔ (((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
402385, 401ralbid 2980 . . . . . . . . . . 11 (𝑦 = ((𝐻)‘𝑗) → (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
403353, 402imbi12d 334 . . . . . . . . . 10 (𝑦 = ((𝐻)‘𝑗) → ((((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁)) ↔ (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))))
404292simprd 479 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡)))
405404simpld 475 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁))
406345, 400, 403, 405vtoclgf 3259 . . . . . . . . 9 (((𝐻)‘𝑗) ∈ (𝐻𝑗) → (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
407406anabsi7 859 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))
408317, 318, 342, 407syl21anc 1323 . . . . . . 7 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))
409 nfcv 2762 . . . . . . . . . . . 12 𝑦(𝐵𝑗)
410 nfcv 2762 . . . . . . . . . . . . 13 𝑦(1 − (𝐸 / 𝑁))
411410, 396, 365nfbr 4690 . . . . . . . . . . . 12 𝑦(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)
412409, 411nfral 2942 . . . . . . . . . . 11 𝑦𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)
413349, 412nfim 1823 . . . . . . . . . 10 𝑦(((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))
414386breq2d 4656 . . . . . . . . . . . 12 (𝑦 = ((𝐻)‘𝑗) → ((1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ (1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
415385, 414ralbid 2980 . . . . . . . . . . 11 (𝑦 = ((𝐻)‘𝑗) → (∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
416353, 415imbi12d 334 . . . . . . . . . 10 (𝑦 = ((𝐻)‘𝑗) → ((((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡)) ↔ (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))))
417404simprd 479 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))
418345, 413, 416, 417vtoclgf 3259 . . . . . . . . 9 (((𝐻)‘𝑗) ∈ (𝐻𝑗) → (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
419418anabsi7 859 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))
420317, 318, 342, 419syl21anc 1323 . . . . . . 7 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))
421394, 408, 4203jca 1240 . . . . . 6 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
422421ex 450 . . . . 5 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → (𝑗 ∈ (0...𝑁) → (∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))))
423316, 422ralrimi 2954 . . . 4 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
424310, 423jca 554 . . 3 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ((𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))))
425 feq1 6013 . . . . 5 (𝑥 = (𝐻) → (𝑥:(0...𝑁)⟶𝐴 ↔ (𝐻):(0...𝑁)⟶𝐴))
426 nfcv 2762 . . . . . . 7 𝑗𝑥
427311, 53nfco 5276 . . . . . . 7 𝑗(𝐻)
428426, 427nfeq 2773 . . . . . 6 𝑗 𝑥 = (𝐻)
429 nfcv 2762 . . . . . . . . 9 𝑡𝑥
430429, 383nfeq 2773 . . . . . . . 8 𝑡 𝑥 = (𝐻)
431 fveq1 6177 . . . . . . . . . . 11 (𝑥 = (𝐻) → (𝑥𝑗) = ((𝐻)‘𝑗))
432431fveq1d 6180 . . . . . . . . . 10 (𝑥 = (𝐻) → ((𝑥𝑗)‘𝑡) = (((𝐻)‘𝑗)‘𝑡))
433432breq2d 4656 . . . . . . . . 9 (𝑥 = (𝐻) → (0 ≤ ((𝑥𝑗)‘𝑡) ↔ 0 ≤ (((𝐻)‘𝑗)‘𝑡)))
434432breq1d 4654 . . . . . . . . 9 (𝑥 = (𝐻) → (((𝑥𝑗)‘𝑡) ≤ 1 ↔ (((𝐻)‘𝑗)‘𝑡) ≤ 1))
435433, 434anbi12d 746 . . . . . . . 8 (𝑥 = (𝐻) → ((0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ↔ (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
436430, 435ralbid 2980 . . . . . . 7 (𝑥 = (𝐻) → (∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
437432breq1d 4654 . . . . . . . 8 (𝑥 = (𝐻) → (((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ (((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
438430, 437ralbid 2980 . . . . . . 7 (𝑥 = (𝐻) → (∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
439432breq2d 4656 . . . . . . . 8 (𝑥 = (𝐻) → ((1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
440430, 439ralbid 2980 . . . . . . 7 (𝑥 = (𝐻) → (∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡) ↔ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
441436, 438, 4403anbi123d 1397 . . . . . 6 (𝑥 = (𝐻) → ((∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡)) ↔ (∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))))
442428, 441ralbid 2980 . . . . 5 (𝑥 = (𝐻) → (∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡)) ↔ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))))
443425, 442anbi12d 746 . . . 4 (𝑥 = (𝐻) → ((𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡))) ↔ ((𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))))
444443spcegv 3289 . . 3 ((𝐻) ∈ V → (((𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))) → ∃𝑥(𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡)))))
44540, 424, 444sylc 65 . 2 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ∃𝑥(𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡))))
44631, 445exlimddv 1861 1 (𝜑 → ∃𝑥(𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036   = wceq 1481  wex 1702  wnf 1706  wcel 1988  wnfc 2749  wne 2791  wral 2909  wrex 2910  {crab 2913  Vcvv 3195  cdif 3564  cin 3566  wss 3567  c0 3907   cuni 4427   class class class wbr 4644  cmpt 4720  dom cdm 5104  ran crn 5105  ccom 5108  Fun wfun 5870   Fn wfn 5871  wf 5872  cfv 5876  (class class class)co 6635  Fincfn 7940  cr 9920  0cc0 9921  1c1 9922   + caddc 9924   · cmul 9926   < clt 10059  cle 10060  cmin 10251   / cdiv 10669  cn 11005  3c3 11056  +crp 11817  (,)cioo 12160  ...cfz 12311  topGenctg 16079  Clsdccld 20801   Cn ccn 21009  Compccmp 21170
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-inf2 8523  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998  ax-pre-sup 9999  ax-mulf 10001
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-fal 1487  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-iin 4514  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-se 5064  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-isom 5885  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-of 6882  df-om 7051  df-1st 7153  df-2nd 7154  df-supp 7281  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-2o 7546  df-oadd 7549  df-er 7727  df-map 7844  df-pm 7845  df-ixp 7894  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-fsupp 8261  df-fi 8302  df-sup 8333  df-inf 8334  df-oi 8400  df-card 8750  df-cda 8975  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-div 10670  df-nn 11006  df-2 11064  df-3 11065  df-4 11066  df-5 11067  df-6 11068  df-7 11069  df-8 11070  df-9 11071  df-n0 11278  df-z 11363  df-dec 11479  df-uz 11673  df-q 11774  df-rp 11818  df-xneg 11931  df-xadd 11932  df-xmul 11933  df-ioo 12164  df-ioc 12165  df-ico 12166  df-icc 12167  df-fz 12312  df-fzo 12450  df-fl 12576  df-seq 12785  df-exp 12844  df-hash 13101  df-cj 13820  df-re 13821  df-im 13822  df-sqrt 13956  df-abs 13957  df-clim 14200  df-rlim 14201  df-sum 14398  df-struct 15840  df-ndx 15841  df-slot 15842  df-base 15844  df-sets 15845  df-ress 15846  df-plusg 15935  df-mulr 15936  df-starv 15937  df-sca 15938  df-vsca 15939  df-ip 15940  df-tset 15941  df-ple 15942  df-ds 15945  df-unif 15946  df-hom 15947  df-cco 15948  df-rest 16064  df-topn 16065  df-0g 16083  df-gsum 16084  df-topgen 16085  df-pt 16086  df-prds 16089  df-xrs 16143  df-qtop 16148  df-imas 16149  df-xps 16151  df-mre 16227  df-mrc 16228  df-acs 16230  df-mgm 17223  df-sgrp 17265  df-mnd 17276  df-submnd 17317  df-mulg 17522  df-cntz 17731  df-cmn 18176  df-psmet 19719  df-xmet 19720  df-met 19721  df-bl 19722  df-mopn 19723  df-cnfld 19728  df-top 20680  df-topon 20697  df-topsp 20718  df-bases 20731  df-cld 20804  df-cn 21012  df-cnp 21013  df-cmp 21171  df-tx 21346  df-hmeo 21539  df-xms 22106  df-ms 22107  df-tms 22108
This theorem is referenced by:  stoweidlem60  40040
  Copyright terms: Public domain W3C validator