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 46015
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 3454 . . . . . . . . . 10 𝑦{𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)}
31, 2nfcxfr 2901 . . . . . . . . 9 𝑦𝑌
4 nfcv 2903 . . . . . . . . 9 𝑧𝑌
5 nfv 1912 . . . . . . . . 9 𝑧(∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))
6 nfv 1912 . . . . . . . . 9 𝑦(∀𝑡 ∈ (𝐷𝑗)(𝑧𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑧𝑡))
7 fveq1 6906 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝑦𝑡) = (𝑧𝑡))
87breq1d 5158 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝑦𝑡) < (𝐸 / 𝑁) ↔ (𝑧𝑡) < (𝐸 / 𝑁)))
98ralbidv 3176 . . . . . . . . . 10 (𝑦 = 𝑧 → (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷𝑗)(𝑧𝑡) < (𝐸 / 𝑁)))
107breq2d 5160 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ (1 − (𝐸 / 𝑁)) < (𝑧𝑡)))
1110ralbidv 3176 . . . . . . . . . 10 (𝑦 = 𝑧 → (∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑧𝑡)))
129, 11anbi12d 632 . . . . . . . . 9 (𝑦 = 𝑧 → ((∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡)) ↔ (∀𝑡 ∈ (𝐷𝑗)(𝑧𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑧𝑡))))
133, 4, 5, 6, 12cbvrabw 3471 . . . . . . . 8 {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} = {𝑧𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑧𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑧𝑡))}
14 ovexd 7466 . . . . . . . . . 10 (𝜑 → (𝐽 Cn 𝐾) ∈ V)
15 stoweidlem59.11 . . . . . . . . . . 11 (𝜑𝐴𝐶)
16 stoweidlem59.5 . . . . . . . . . . 11 𝐶 = (𝐽 Cn 𝐾)
1715, 16sseqtrdi 4046 . . . . . . . . . 10 (𝜑𝐴 ⊆ (𝐽 Cn 𝐾))
1814, 17ssexd 5330 . . . . . . . . 9 (𝜑𝐴 ∈ V)
191, 18rabexd 5346 . . . . . . . 8 (𝜑𝑌 ∈ V)
2013, 19rabexd 5346 . . . . . . 7 (𝜑 → {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ∈ V)
2120ralrimivw 3148 . . . . . 6 (𝜑 → ∀𝑗 ∈ (0...𝑁){𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ∈ V)
22 stoweidlem59.9 . . . . . . 7 𝐻 = (𝑗 ∈ (0...𝑁) ↦ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
2322fnmpt 6709 . . . . . 6 (∀𝑗 ∈ (0...𝑁){𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ∈ V → 𝐻 Fn (0...𝑁))
2421, 23syl 17 . . . . 5 (𝜑𝐻 Fn (0...𝑁))
25 fzfi 14010 . . . . 5 (0...𝑁) ∈ Fin
26 fnfi 9216 . . . . 5 ((𝐻 Fn (0...𝑁) ∧ (0...𝑁) ∈ Fin) → 𝐻 ∈ Fin)
2724, 25, 26sylancl 586 . . . 4 (𝜑𝐻 ∈ Fin)
28 rnfi 9378 . . . 4 (𝐻 ∈ Fin → ran 𝐻 ∈ Fin)
2927, 28syl 17 . . 3 (𝜑 → ran 𝐻 ∈ Fin)
30 fnchoice 44967 . . 3 (ran 𝐻 ∈ Fin → ∃( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)))
3129, 30syl 17 . 2 (𝜑 → ∃( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)))
32 simprl 771 . . . . 5 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → Fn ran 𝐻)
33 ovex 7464 . . . . . . . 8 (0...𝑁) ∈ V
3433mptex 7243 . . . . . . 7 (𝑗 ∈ (0...𝑁) ↦ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}) ∈ V
3522, 34eqeltri 2835 . . . . . 6 𝐻 ∈ V
3635rnex 7933 . . . . 5 ran 𝐻 ∈ V
37 fnex 7237 . . . . 5 (( Fn ran 𝐻 ∧ ran 𝐻 ∈ V) → ∈ V)
3832, 36, 37sylancl 586 . . . 4 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ∈ V)
39 coexg 7952 . . . 4 (( ∈ V ∧ 𝐻 ∈ V) → (𝐻) ∈ V)
4038, 35, 39sylancl 586 . . 3 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → (𝐻) ∈ V)
41 dffn3 6749 . . . . . . 7 ( Fn ran 𝐻:ran 𝐻⟶ran )
4232, 41sylib 218 . . . . . 6 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → :ran 𝐻⟶ran )
43 nfv 1912 . . . . . . . . . 10 𝑤𝜑
44 nfv 1912 . . . . . . . . . . 11 𝑤 Fn ran 𝐻
45 nfra1 3282 . . . . . . . . . . 11 𝑤𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)
4644, 45nfan 1897 . . . . . . . . . 10 𝑤( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))
4743, 46nfan 1897 . . . . . . . . 9 𝑤(𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)))
48 simplrr 778 . . . . . . . . . . 11 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))
49 simpr 484 . . . . . . . . . . 11 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → 𝑤 ∈ ran 𝐻)
50 fvelrnb 6969 . . . . . . . . . . . . . . . 16 (𝐻 Fn (0...𝑁) → (𝑤 ∈ ran 𝐻 ↔ ∃𝑎 ∈ (0...𝑁)(𝐻𝑎) = 𝑤))
51 nfv 1912 . . . . . . . . . . . . . . . . 17 𝑎(𝐻𝑗) = 𝑤
52 nfmpt1 5256 . . . . . . . . . . . . . . . . . . . 20 𝑗(𝑗 ∈ (0...𝑁) ↦ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
5322, 52nfcxfr 2901 . . . . . . . . . . . . . . . . . . 19 𝑗𝐻
54 nfcv 2903 . . . . . . . . . . . . . . . . . . 19 𝑗𝑎
5553, 54nffv 6917 . . . . . . . . . . . . . . . . . 18 𝑗(𝐻𝑎)
56 nfcv 2903 . . . . . . . . . . . . . . . . . 18 𝑗𝑤
5755, 56nfeq 2917 . . . . . . . . . . . . . . . . 17 𝑗(𝐻𝑎) = 𝑤
58 fveq2 6907 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑎 → (𝐻𝑗) = (𝐻𝑎))
5958eqeq1d 2737 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑎 → ((𝐻𝑗) = 𝑤 ↔ (𝐻𝑎) = 𝑤))
6051, 57, 59cbvrexw 3305 . . . . . . . . . . . . . . . 16 (∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤 ↔ ∃𝑎 ∈ (0...𝑁)(𝐻𝑎) = 𝑤)
6150, 60bitr4di 289 . . . . . . . . . . . . . . 15 (𝐻 Fn (0...𝑁) → (𝑤 ∈ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤))
6224, 61syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑤 ∈ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤))
6362biimpa 476 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ran 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤)
64 simp3 1137 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑁) ∧ (𝐻𝑗) = 𝑤) → (𝐻𝑗) = 𝑤)
65 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
6620adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ∈ V)
6722fvmpt2 7027 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ (0...𝑁) ∧ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ∈ V) → (𝐻𝑗) = {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
6865, 66, 67syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐻𝑗) = {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
69 stoweidlem59.6 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
70 nfcv 2903 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡(0...𝑁)
71 nfrab1 3454 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡{𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}
7270, 71nfmpt 5255 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
7369, 72nfcxfr 2901 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡𝐷
74 nfcv 2903 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡𝑗
7573, 74nffv 6917 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝐷𝑗)
76 nfcv 2903 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡𝑇
77 stoweidlem59.7 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
78 nfrab1 3454 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑡{𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)}
7970, 78nfmpt 5255 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
8077, 79nfcxfr 2901 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡𝐵
8180, 74nffv 6917 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡(𝐵𝑗)
8276, 81nfdif 4139 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝑇 ∖ (𝐵𝑗))
83 stoweidlem59.2 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡𝜑
84 nfv 1912 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡 𝑗 ∈ (0...𝑁)
8583, 84nfan 1897 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝜑𝑗 ∈ (0...𝑁))
86 stoweidlem59.3 . . . . . . . . . . . . . . . . . . . . . . 23 𝐾 = (topGen‘ran (,))
87 stoweidlem59.4 . . . . . . . . . . . . . . . . . . . . . . 23 𝑇 = 𝐽
88 stoweidlem59.10 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐽 ∈ Comp)
8988adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → 𝐽 ∈ Comp)
9015adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → 𝐴𝐶)
91 stoweidlem59.12 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
92913adant1r 1176 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
93 stoweidlem59.13 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
94933adant1r 1176 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
95 stoweidlem59.14 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ ℝ) → (𝑡𝑇𝑦) ∈ 𝐴)
9695adantlr 715 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ ℝ) → (𝑡𝑇𝑦) ∈ 𝐴)
97 stoweidlem59.15 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟𝑇𝑡𝑇𝑟𝑡)) → ∃𝑞𝐴 (𝑞𝑟) ≠ (𝑞𝑡))
9897adantlr 715 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑟𝑇𝑡𝑇𝑟𝑡)) → ∃𝑞𝐴 (𝑞𝑟) ≠ (𝑞𝑡))
9988uniexd 7761 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 𝐽 ∈ V)
10087, 99eqeltrid 2843 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑇 ∈ V)
101100adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇 ∈ V)
102 rabexg 5343 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑇 ∈ V → {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V)
103101, 102syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V)
10477fvmpt2 7027 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗 ∈ (0...𝑁) ∧ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V) → (𝐵𝑗) = {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
10565, 103, 104syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐵𝑗) = {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
106 stoweidlem59.1 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡𝐹
107 eqid 2735 . . . . . . . . . . . . . . . . . . . . . . . . 25 {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} = {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)}
108 elfzelz 13561 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
109108zred 12720 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
110 3re 12344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3 ∈ ℝ
111 3ne0 12370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3 ≠ 0
112110, 111rereccli 12030 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (1 / 3) ∈ ℝ
113 readdcl 11236 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ) → (𝑗 + (1 / 3)) ∈ ℝ)
114109, 112, 113sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑁) → (𝑗 + (1 / 3)) ∈ ℝ)
115114adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑗 + (1 / 3)) ∈ ℝ)
116 stoweidlem59.17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐸 ∈ ℝ+)
117116rpred 13075 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐸 ∈ ℝ)
118117adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → 𝐸 ∈ ℝ)
119115, 118remulcld 11289 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑗 + (1 / 3)) · 𝐸) ∈ ℝ)
120 stoweidlem59.16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐹𝐶)
121120, 16eleqtrdi 2849 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐹 ∈ (𝐽 Cn 𝐾))
122121adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → 𝐹 ∈ (𝐽 Cn 𝐾))
123106, 86, 87, 107, 119, 122rfcnpre3 44971 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ (Clsd‘𝐽))
124105, 123eqeltrd 2839 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐵𝑗) ∈ (Clsd‘𝐽))
125 rabexg 5343 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V)
126101, 125syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V)
12769fvmpt2 7027 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗 ∈ (0...𝑁) ∧ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V) → (𝐷𝑗) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
12865, 126, 127syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐷𝑗) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
129 eqid 2735 . . . . . . . . . . . . . . . . . . . . . . . . 25 {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}
130 resubcl 11571 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ) → (𝑗 − (1 / 3)) ∈ ℝ)
131109, 112, 130sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑁) → (𝑗 − (1 / 3)) ∈ ℝ)
132131adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑗 − (1 / 3)) ∈ ℝ)
133132, 118remulcld 11289 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ)
134106, 86, 87, 129, 133, 122rfcnpre4 44972 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ (Clsd‘𝐽))
135128, 134eqeltrd 2839 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐷𝑗) ∈ (Clsd‘𝐽))
136133adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ)
137119adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ((𝑗 + (1 / 3)) · 𝐸) ∈ ℝ)
13886, 87, 16, 120fcnre 44963 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝐹:𝑇⟶ℝ)
139138ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → 𝐹:𝑇⟶ℝ)
140 ssrab2 4090 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ⊆ 𝑇
141105, 140eqsstrdi 4050 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐵𝑗) ⊆ 𝑇)
142141sselda 3995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → 𝑡𝑇)
143139, 142ffvelcdmd 7105 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → (𝐹𝑡) ∈ ℝ)
144112, 130mpan2 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) ∈ ℝ)
145 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ → 𝑗 ∈ ℝ)
146112, 113mpan2 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ → (𝑗 + (1 / 3)) ∈ ℝ)
147 3pos 12369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 0 < 3
148110, 147recgt0ii 12172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 0 < (1 / 3)
149112, 148elrpii 13035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (1 / 3) ∈ ℝ+
150 ltsubrp 13069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ+) → (𝑗 − (1 / 3)) < 𝑗)
151149, 150mpan2 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) < 𝑗)
152 ltaddrp 13070 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ+) → 𝑗 < (𝑗 + (1 / 3)))
153149, 152mpan2 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ → 𝑗 < (𝑗 + (1 / 3)))
154144, 145, 146, 151, 153lttrd 11420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
155109, 154syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 ∈ (0...𝑁) → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
156155adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
157116rpregt0d 13081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
158157adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
159 ltmul1 12115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑗 − (1 / 3)) ∈ ℝ ∧ (𝑗 + (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑗 − (1 / 3)) < (𝑗 + (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸)))
160132, 115, 158, 159syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) < (𝑗 + (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸)))
161156, 160mpbid 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸))
162161adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸))
163105eleq2d 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑡 ∈ (𝐵𝑗) ↔ 𝑡 ∈ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)}))
164163biimpa 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → 𝑡 ∈ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
165 rabid 3455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑡 ∈ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ↔ (𝑡𝑇 ∧ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)))
166164, 165sylib 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → (𝑡𝑇 ∧ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)))
167166simprd 495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡))
168136, 137, 143, 162, 167ltletrd 11419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) < (𝐹𝑡))
169136, 143ltnled 11406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → (((𝑗 − (1 / 3)) · 𝐸) < (𝐹𝑡) ↔ ¬ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
170168, 169mpbid 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ¬ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))
171170intnand 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ¬ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
172 rabid 3455 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
173171, 172sylnibr 329 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ¬ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
174128adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → (𝐷𝑗) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
175173, 174neleqtrrd 2862 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ¬ 𝑡 ∈ (𝐷𝑗))
176175ex 412 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑡 ∈ (𝐵𝑗) → ¬ 𝑡 ∈ (𝐷𝑗)))
17785, 176ralrimi 3255 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐵𝑗) ¬ 𝑡 ∈ (𝐷𝑗))
178 disj 4456 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐵𝑗) ∩ (𝐷𝑗)) = ∅ ↔ ∀𝑎 ∈ (𝐵𝑗) ¬ 𝑎 ∈ (𝐷𝑗))
179 nfcv 2903 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑎(𝐵𝑗)
18075nfcri 2895 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑡 𝑎 ∈ (𝐷𝑗)
181180nfn 1855 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡 ¬ 𝑎 ∈ (𝐷𝑗)
182 nfv 1912 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑎 ¬ 𝑡 ∈ (𝐷𝑗)
183 eleq1 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑡 → (𝑎 ∈ (𝐷𝑗) ↔ 𝑡 ∈ (𝐷𝑗)))
184183notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = 𝑡 → (¬ 𝑎 ∈ (𝐷𝑗) ↔ ¬ 𝑡 ∈ (𝐷𝑗)))
185179, 81, 181, 182, 184cbvralfw 3302 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑎 ∈ (𝐵𝑗) ¬ 𝑎 ∈ (𝐷𝑗) ↔ ∀𝑡 ∈ (𝐵𝑗) ¬ 𝑡 ∈ (𝐷𝑗))
186178, 185bitri 275 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐵𝑗) ∩ (𝐷𝑗)) = ∅ ↔ ∀𝑡 ∈ (𝐵𝑗) ¬ 𝑡 ∈ (𝐷𝑗))
187177, 186sylibr 234 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝐵𝑗) ∩ (𝐷𝑗)) = ∅)
188 eqid 2735 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑇 ∖ (𝐵𝑗)) = (𝑇 ∖ (𝐵𝑗))
189 stoweidlem59.19 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑁 ∈ ℕ)
190189nnrpd 13073 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑁 ∈ ℝ+)
191116, 190rpdivcld 13092 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐸 / 𝑁) ∈ ℝ+)
192191adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐸 / 𝑁) ∈ ℝ+)
193117, 189nndivred 12318 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐸 / 𝑁) ∈ ℝ)
194112a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (1 / 3) ∈ ℝ)
195189nnge1d 12312 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → 1 ≤ 𝑁)
196 1re 11259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 1 ∈ ℝ
197 0lt1 11783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 0 < 1
198196, 197pm3.2i 470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (1 ∈ ℝ ∧ 0 < 1)
199198a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (1 ∈ ℝ ∧ 0 < 1))
200189nnred 12279 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑁 ∈ ℝ)
201189nngt0d 12313 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → 0 < 𝑁)
202 lediv2 12156 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((1 ∈ ℝ ∧ 0 < 1) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (1 ≤ 𝑁 ↔ (𝐸 / 𝑁) ≤ (𝐸 / 1)))
203199, 200, 201, 157, 202syl121anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (1 ≤ 𝑁 ↔ (𝐸 / 𝑁) ≤ (𝐸 / 1)))
204195, 203mpbid 232 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐸 / 𝑁) ≤ (𝐸 / 1))
205116rpcnd 13077 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐸 ∈ ℂ)
206205div1d 12033 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐸 / 1) = 𝐸)
207204, 206breqtrd 5174 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐸 / 𝑁) ≤ 𝐸)
208 stoweidlem59.18 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐸 < (1 / 3))
209193, 117, 194, 207, 208lelttrd 11417 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐸 / 𝑁) < (1 / 3))
210209adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐸 / 𝑁) < (1 / 3))
21175, 82, 85, 86, 87, 16, 89, 90, 92, 94, 96, 98, 124, 135, 187, 188, 192, 210stoweidlem58 46014 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (0...𝑁)) → ∃𝑥𝐴 (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))
212 df-rex 3069 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑥𝐴 (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)) ↔ ∃𝑥(𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))))
213211, 212sylib 218 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0...𝑁)) → ∃𝑥(𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))))
214 simprl 771 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → 𝑥𝐴)
215 simprr1 1220 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → ∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1))
216 fveq1 6906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 = 𝑥 → (𝑦𝑡) = (𝑥𝑡))
217216breq2d 5160 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = 𝑥 → (0 ≤ (𝑦𝑡) ↔ 0 ≤ (𝑥𝑡)))
218216breq1d 5158 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = 𝑥 → ((𝑦𝑡) ≤ 1 ↔ (𝑥𝑡) ≤ 1))
219217, 218anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = 𝑥 → ((0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1) ↔ (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1)))
220219ralbidv 3176 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑥 → (∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1)))
221220, 1elrab2 3698 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥𝑌 ↔ (𝑥𝐴 ∧ ∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1)))
222214, 215, 221sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → 𝑥𝑌)
223 simprr2 1221 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁))
224 simprr3 1222 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))
225223, 224jca 511 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → (∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))
226 nfcv 2903 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦𝑥
227 nfv 1912 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦(∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))
228216breq1d 5158 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = 𝑥 → ((𝑦𝑡) < (𝐸 / 𝑁) ↔ (𝑥𝑡) < (𝐸 / 𝑁)))
229228ralbidv 3176 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑥 → (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁)))
230216breq2d 5160 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = 𝑥 → ((1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ (1 − (𝐸 / 𝑁)) < (𝑥𝑡)))
231230ralbidv 3176 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑥 → (∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))
232229, 231anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑥 → ((∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡)) ↔ (∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))))
233226, 3, 227, 232elrabf 3691 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ↔ (𝑥𝑌 ∧ (∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))))
234222, 225, 233sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → 𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
235234ex 412 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))) → 𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}))
236235eximdv 1915 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0...𝑁)) → (∃𝑥(𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))) → ∃𝑥 𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}))
237213, 236mpd 15 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑁)) → ∃𝑥 𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
238 ne0i 4347 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} → {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ≠ ∅)
239238exlimiv 1928 . . . . . . . . . . . . . . . . . . . 20 (∃𝑥 𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} → {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ≠ ∅)
240237, 239syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ≠ ∅)
24168, 240eqnetrd 3006 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐻𝑗) ≠ ∅)
2422413adant3 1131 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑁) ∧ (𝐻𝑗) = 𝑤) → (𝐻𝑗) ≠ ∅)
24364, 242eqnetrrd 3007 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑁) ∧ (𝐻𝑗) = 𝑤) → 𝑤 ≠ ∅)
2442433exp 1118 . . . . . . . . . . . . . . 15 (𝜑 → (𝑗 ∈ (0...𝑁) → ((𝐻𝑗) = 𝑤𝑤 ≠ ∅)))
245244rexlimdv 3151 . . . . . . . . . . . . . 14 (𝜑 → (∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤𝑤 ≠ ∅))
246245adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ran 𝐻) → (∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤𝑤 ≠ ∅))
24763, 246mpd 15 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ran 𝐻) → 𝑤 ≠ ∅)
248247adantlr 715 . . . . . . . . . . 11 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → 𝑤 ≠ ∅)
249 rsp 3245 . . . . . . . . . . 11 (∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤) → (𝑤 ∈ ran 𝐻 → (𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)))
25048, 49, 248, 249syl3c 66 . . . . . . . . . 10 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → (𝑤) ∈ 𝑤)
251250ex 412 . . . . . . . . 9 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → (𝑤 ∈ ran 𝐻 → (𝑤) ∈ 𝑤))
25247, 251ralrimi 3255 . . . . . . . 8 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ∀𝑤 ∈ ran 𝐻(𝑤) ∈ 𝑤)
253 chfnrn 7069 . . . . . . . 8 (( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤) ∈ 𝑤) → ran ran 𝐻)
25432, 252, 253syl2anc 584 . . . . . . 7 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ran ran 𝐻)
255 nfv 1912 . . . . . . . . . 10 𝑦𝜑
256 nfcv 2903 . . . . . . . . . . . 12 𝑦
257 nfcv 2903 . . . . . . . . . . . . . . 15 𝑦(0...𝑁)
258 nfrab1 3454 . . . . . . . . . . . . . . 15 𝑦{𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}
259257, 258nfmpt 5255 . . . . . . . . . . . . . 14 𝑦(𝑗 ∈ (0...𝑁) ↦ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
26022, 259nfcxfr 2901 . . . . . . . . . . . . 13 𝑦𝐻
261260nfrn 5966 . . . . . . . . . . . 12 𝑦ran 𝐻
262256, 261nffn 6668 . . . . . . . . . . 11 𝑦 Fn ran 𝐻
263 nfv 1912 . . . . . . . . . . . 12 𝑦(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)
264261, 263nfralw 3309 . . . . . . . . . . 11 𝑦𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)
265262, 264nfan 1897 . . . . . . . . . 10 𝑦( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))
266255, 265nfan 1897 . . . . . . . . 9 𝑦(𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)))
267261nfuni 4919 . . . . . . . . 9 𝑦 ran 𝐻
268 fnunirn 7274 . . . . . . . . . . . . . . 15 (𝐻 Fn (0...𝑁) → (𝑦 ran 𝐻 ↔ ∃𝑧 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑧)))
269 nfcv 2903 . . . . . . . . . . . . . . . . . 18 𝑗𝑧
27053, 269nffv 6917 . . . . . . . . . . . . . . . . 17 𝑗(𝐻𝑧)
271270nfcri 2895 . . . . . . . . . . . . . . . 16 𝑗 𝑦 ∈ (𝐻𝑧)
272 nfv 1912 . . . . . . . . . . . . . . . 16 𝑧 𝑦 ∈ (𝐻𝑗)
273 fveq2 6907 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑗 → (𝐻𝑧) = (𝐻𝑗))
274273eleq2d 2825 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑗 → (𝑦 ∈ (𝐻𝑧) ↔ 𝑦 ∈ (𝐻𝑗)))
275271, 272, 274cbvrexw 3305 . . . . . . . . . . . . . . 15 (∃𝑧 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑧) ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑗))
276268, 275bitrdi 287 . . . . . . . . . . . . . 14 (𝐻 Fn (0...𝑁) → (𝑦 ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑗)))
27724, 276syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑦 ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑗)))
278277biimpa 476 . . . . . . . . . . . 12 ((𝜑𝑦 ran 𝐻) → ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑗))
279 nfv 1912 . . . . . . . . . . . . . 14 𝑗𝜑
28053nfrn 5966 . . . . . . . . . . . . . . . 16 𝑗ran 𝐻
281280nfuni 4919 . . . . . . . . . . . . . . 15 𝑗 ran 𝐻
282281nfcri 2895 . . . . . . . . . . . . . 14 𝑗 𝑦 ran 𝐻
283279, 282nfan 1897 . . . . . . . . . . . . 13 𝑗(𝜑𝑦 ran 𝐻)
284 nfv 1912 . . . . . . . . . . . . 13 𝑗 𝑦𝑌
285 simp1l 1196 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝜑)
286 simp2 1136 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑗 ∈ (0...𝑁))
287 simp3 1137 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑦 ∈ (𝐻𝑗))
28868eleq2d 2825 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑦 ∈ (𝐻𝑗) ↔ 𝑦 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}))
289288biimpa 476 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑦 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
290 rabid 3455 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ↔ (𝑦𝑌 ∧ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))))
291289, 290sylib 218 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → (𝑦𝑌 ∧ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))))
292291simpld 494 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑦𝑌)
293285, 286, 287, 292syl21anc 838 . . . . . . . . . . . . . 14 (((𝜑𝑦 ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑦𝑌)
2942933exp 1118 . . . . . . . . . . . . 13 ((𝜑𝑦 ran 𝐻) → (𝑗 ∈ (0...𝑁) → (𝑦 ∈ (𝐻𝑗) → 𝑦𝑌)))
295283, 284, 294rexlimd 3264 . . . . . . . . . . . 12 ((𝜑𝑦 ran 𝐻) → (∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑗) → 𝑦𝑌))
296278, 295mpd 15 . . . . . . . . . . 11 ((𝜑𝑦 ran 𝐻) → 𝑦𝑌)
297296adantlr 715 . . . . . . . . . 10 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑦 ran 𝐻) → 𝑦𝑌)
298297ex 412 . . . . . . . . 9 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → (𝑦 ran 𝐻𝑦𝑌))
299266, 267, 3, 298ssrd 4000 . . . . . . . 8 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ran 𝐻𝑌)
300 ssrab2 4090 . . . . . . . . 9 {𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)} ⊆ 𝐴
3011, 300eqsstri 4030 . . . . . . . 8 𝑌𝐴
302299, 301sstrdi 4008 . . . . . . 7 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ran 𝐻𝐴)
303254, 302sstrd 4006 . . . . . 6 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ran 𝐴)
30442, 303fssd 6754 . . . . 5 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → :ran 𝐻𝐴)
305 dffn3 6749 . . . . . . 7 (𝐻 Fn (0...𝑁) ↔ 𝐻:(0...𝑁)⟶ran 𝐻)
30624, 305sylib 218 . . . . . 6 (𝜑𝐻:(0...𝑁)⟶ran 𝐻)
307306adantr 480 . . . . 5 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → 𝐻:(0...𝑁)⟶ran 𝐻)
308 fco 6761 . . . . 5 ((:ran 𝐻𝐴𝐻:(0...𝑁)⟶ran 𝐻) → (𝐻):(0...𝑁)⟶𝐴)
309304, 307, 308syl2anc 584 . . . 4 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → (𝐻):(0...𝑁)⟶𝐴)
310 nfcv 2903 . . . . . . . 8 𝑗
311310, 280nffn 6668 . . . . . . 7 𝑗 Fn ran 𝐻
312 nfv 1912 . . . . . . . 8 𝑗(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)
313280, 312nfralw 3309 . . . . . . 7 𝑗𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)
314311, 313nfan 1897 . . . . . 6 𝑗( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))
315279, 314nfan 1897 . . . . 5 𝑗(𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)))
316 simpll 767 . . . . . . . . . 10 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝜑)
317 simpr 484 . . . . . . . . . 10 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
31824ad2antrr 726 . . . . . . . . . . . 12 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝐻 Fn (0...𝑁))
319 fvco2 7006 . . . . . . . . . . . 12 ((𝐻 Fn (0...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → ((𝐻)‘𝑗) = (‘(𝐻𝑗)))
320318, 319sylancom 588 . . . . . . . . . . 11 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝐻)‘𝑗) = (‘(𝐻𝑗)))
321 simplrr 778 . . . . . . . . . . . . 13 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))
322 fnfun 6669 . . . . . . . . . . . . . . . 16 (𝐻 Fn (0...𝑁) → Fun 𝐻)
32324, 322syl 17 . . . . . . . . . . . . . . 15 (𝜑 → Fun 𝐻)
324323ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → Fun 𝐻)
32524fndmd 6674 . . . . . . . . . . . . . . . . 17 (𝜑 → dom 𝐻 = (0...𝑁))
326325adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑁)) → dom 𝐻 = (0...𝑁))
32765, 326eleqtrrd 2842 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑗 ∈ dom 𝐻)
328327adantlr 715 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ dom 𝐻)
329 fvelrn 7096 . . . . . . . . . . . . . 14 ((Fun 𝐻𝑗 ∈ dom 𝐻) → (𝐻𝑗) ∈ ran 𝐻)
330324, 328, 329syl2anc 584 . . . . . . . . . . . . 13 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (𝐻𝑗) ∈ ran 𝐻)
331321, 330jca 511 . . . . . . . . . . . 12 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤) ∧ (𝐻𝑗) ∈ ran 𝐻))
332241adantlr 715 . . . . . . . . . . . 12 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (𝐻𝑗) ≠ ∅)
333 neeq1 3001 . . . . . . . . . . . . . 14 (𝑤 = (𝐻𝑗) → (𝑤 ≠ ∅ ↔ (𝐻𝑗) ≠ ∅))
334 fveq2 6907 . . . . . . . . . . . . . . 15 (𝑤 = (𝐻𝑗) → (𝑤) = (‘(𝐻𝑗)))
335 id 22 . . . . . . . . . . . . . . 15 (𝑤 = (𝐻𝑗) → 𝑤 = (𝐻𝑗))
336334, 335eleq12d 2833 . . . . . . . . . . . . . 14 (𝑤 = (𝐻𝑗) → ((𝑤) ∈ 𝑤 ↔ (‘(𝐻𝑗)) ∈ (𝐻𝑗)))
337333, 336imbi12d 344 . . . . . . . . . . . . 13 (𝑤 = (𝐻𝑗) → ((𝑤 ≠ ∅ → (𝑤) ∈ 𝑤) ↔ ((𝐻𝑗) ≠ ∅ → (‘(𝐻𝑗)) ∈ (𝐻𝑗))))
338337rspccva 3621 . . . . . . . . . . . 12 ((∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤) ∧ (𝐻𝑗) ∈ ran 𝐻) → ((𝐻𝑗) ≠ ∅ → (‘(𝐻𝑗)) ∈ (𝐻𝑗)))
339331, 332, 338sylc 65 . . . . . . . . . . 11 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (‘(𝐻𝑗)) ∈ (𝐻𝑗))
340320, 339eqeltrd 2839 . . . . . . . . . 10 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝐻)‘𝑗) ∈ (𝐻𝑗))
341256, 260nfco 5879 . . . . . . . . . . . . 13 𝑦(𝐻)
342 nfcv 2903 . . . . . . . . . . . . 13 𝑦𝑗
343341, 342nffv 6917 . . . . . . . . . . . 12 𝑦((𝐻)‘𝑗)
344 nfv 1912 . . . . . . . . . . . . . 14 𝑦(𝜑𝑗 ∈ (0...𝑁))
345260, 342nffv 6917 . . . . . . . . . . . . . . 15 𝑦(𝐻𝑗)
346343, 345nfel 2918 . . . . . . . . . . . . . 14 𝑦((𝐻)‘𝑗) ∈ (𝐻𝑗)
347344, 346nfan 1897 . . . . . . . . . . . . 13 𝑦((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗))
348343, 3nfel 2918 . . . . . . . . . . . . 13 𝑦((𝐻)‘𝑗) ∈ 𝑌
349347, 348nfim 1894 . . . . . . . . . . . 12 𝑦(((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ((𝐻)‘𝑗) ∈ 𝑌)
350 eleq1 2827 . . . . . . . . . . . . . 14 (𝑦 = ((𝐻)‘𝑗) → (𝑦 ∈ (𝐻𝑗) ↔ ((𝐻)‘𝑗) ∈ (𝐻𝑗)))
351350anbi2d 630 . . . . . . . . . . . . 13 (𝑦 = ((𝐻)‘𝑗) → (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) ↔ ((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗))))
352 eleq1 2827 . . . . . . . . . . . . 13 (𝑦 = ((𝐻)‘𝑗) → (𝑦𝑌 ↔ ((𝐻)‘𝑗) ∈ 𝑌))
353351, 352imbi12d 344 . . . . . . . . . . . 12 (𝑦 = ((𝐻)‘𝑗) → ((((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑦𝑌) ↔ (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ((𝐻)‘𝑗) ∈ 𝑌)))
354343, 349, 353, 292vtoclgf 3569 . . . . . . . . . . 11 (((𝐻)‘𝑗) ∈ (𝐻𝑗) → (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ((𝐻)‘𝑗) ∈ 𝑌))
355354anabsi7 671 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ((𝐻)‘𝑗) ∈ 𝑌)
356316, 317, 340, 355syl21anc 838 . . . . . . . . 9 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝐻)‘𝑗) ∈ 𝑌)
3571eleq2i 2831 . . . . . . . . . 10 (((𝐻)‘𝑗) ∈ 𝑌 ↔ ((𝐻)‘𝑗) ∈ {𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)})
358 nfcv 2903 . . . . . . . . . . 11 𝑦𝐴
359 nfcv 2903 . . . . . . . . . . . 12 𝑦𝑇
360 nfcv 2903 . . . . . . . . . . . . . 14 𝑦0
361 nfcv 2903 . . . . . . . . . . . . . 14 𝑦
362 nfcv 2903 . . . . . . . . . . . . . . 15 𝑦𝑡
363343, 362nffv 6917 . . . . . . . . . . . . . 14 𝑦(((𝐻)‘𝑗)‘𝑡)
364360, 361, 363nfbr 5195 . . . . . . . . . . . . 13 𝑦0 ≤ (((𝐻)‘𝑗)‘𝑡)
365 nfcv 2903 . . . . . . . . . . . . . 14 𝑦1
366363, 361, 365nfbr 5195 . . . . . . . . . . . . 13 𝑦(((𝐻)‘𝑗)‘𝑡) ≤ 1
367364, 366nfan 1897 . . . . . . . . . . . 12 𝑦(0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)
368359, 367nfralw 3309 . . . . . . . . . . 11 𝑦𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)
369 nfcv 2903 . . . . . . . . . . . . 13 𝑡𝑦
370 nfcv 2903 . . . . . . . . . . . . . . 15 𝑡
371 nfra1 3282 . . . . . . . . . . . . . . . . . . 19 𝑡𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁)
372 nfra1 3282 . . . . . . . . . . . . . . . . . . 19 𝑡𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡)
373371, 372nfan 1897 . . . . . . . . . . . . . . . . . 18 𝑡(∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))
374 nfra1 3282 . . . . . . . . . . . . . . . . . . . 20 𝑡𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)
375 nfcv 2903 . . . . . . . . . . . . . . . . . . . 20 𝑡𝐴
376374, 375nfrabw 3473 . . . . . . . . . . . . . . . . . . 19 𝑡{𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)}
3771, 376nfcxfr 2901 . . . . . . . . . . . . . . . . . 18 𝑡𝑌
378373, 377nfrabw 3473 . . . . . . . . . . . . . . . . 17 𝑡{𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}
37970, 378nfmpt 5255 . . . . . . . . . . . . . . . 16 𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
38022, 379nfcxfr 2901 . . . . . . . . . . . . . . 15 𝑡𝐻
381370, 380nfco 5879 . . . . . . . . . . . . . 14 𝑡(𝐻)
382381, 74nffv 6917 . . . . . . . . . . . . 13 𝑡((𝐻)‘𝑗)
383369, 382nfeq 2917 . . . . . . . . . . . 12 𝑡 𝑦 = ((𝐻)‘𝑗)
384 fveq1 6906 . . . . . . . . . . . . . 14 (𝑦 = ((𝐻)‘𝑗) → (𝑦𝑡) = (((𝐻)‘𝑗)‘𝑡))
385384breq2d 5160 . . . . . . . . . . . . 13 (𝑦 = ((𝐻)‘𝑗) → (0 ≤ (𝑦𝑡) ↔ 0 ≤ (((𝐻)‘𝑗)‘𝑡)))
386384breq1d 5158 . . . . . . . . . . . . 13 (𝑦 = ((𝐻)‘𝑗) → ((𝑦𝑡) ≤ 1 ↔ (((𝐻)‘𝑗)‘𝑡) ≤ 1))
387385, 386anbi12d 632 . . . . . . . . . . . 12 (𝑦 = ((𝐻)‘𝑗) → ((0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1) ↔ (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
388383, 387ralbid 3271 . . . . . . . . . . 11 (𝑦 = ((𝐻)‘𝑗) → (∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
389343, 358, 368, 388elrabf 3691 . . . . . . . . . 10 (((𝐻)‘𝑗) ∈ {𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)} ↔ (((𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
390357, 389bitri 275 . . . . . . . . 9 (((𝐻)‘𝑗) ∈ 𝑌 ↔ (((𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
391356, 390sylib 218 . . . . . . . 8 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (((𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
392391simprd 495 . . . . . . 7 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1))
393 nfcv 2903 . . . . . . . . . . . 12 𝑦(𝐷𝑗)
394 nfcv 2903 . . . . . . . . . . . . 13 𝑦 <
395 nfcv 2903 . . . . . . . . . . . . 13 𝑦(𝐸 / 𝑁)
396363, 394, 395nfbr 5195 . . . . . . . . . . . 12 𝑦(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)
397393, 396nfralw 3309 . . . . . . . . . . 11 𝑦𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)
398347, 397nfim 1894 . . . . . . . . . 10 𝑦(((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))
399384breq1d 5158 . . . . . . . . . . . 12 (𝑦 = ((𝐻)‘𝑗) → ((𝑦𝑡) < (𝐸 / 𝑁) ↔ (((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
400383, 399ralbid 3271 . . . . . . . . . . 11 (𝑦 = ((𝐻)‘𝑗) → (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
401351, 400imbi12d 344 . . . . . . . . . 10 (𝑦 = ((𝐻)‘𝑗) → ((((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁)) ↔ (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))))
402291simprd 495 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡)))
403402simpld 494 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁))
404343, 398, 401, 403vtoclgf 3569 . . . . . . . . 9 (((𝐻)‘𝑗) ∈ (𝐻𝑗) → (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
405404anabsi7 671 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))
406316, 317, 340, 405syl21anc 838 . . . . . . 7 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))
407 nfcv 2903 . . . . . . . . . . . 12 𝑦(𝐵𝑗)
408 nfcv 2903 . . . . . . . . . . . . 13 𝑦(1 − (𝐸 / 𝑁))
409408, 394, 363nfbr 5195 . . . . . . . . . . . 12 𝑦(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)
410407, 409nfralw 3309 . . . . . . . . . . 11 𝑦𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)
411347, 410nfim 1894 . . . . . . . . . 10 𝑦(((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))
412384breq2d 5160 . . . . . . . . . . . 12 (𝑦 = ((𝐻)‘𝑗) → ((1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ (1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
413383, 412ralbid 3271 . . . . . . . . . . 11 (𝑦 = ((𝐻)‘𝑗) → (∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
414351, 413imbi12d 344 . . . . . . . . . 10 (𝑦 = ((𝐻)‘𝑗) → ((((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡)) ↔ (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))))
415402simprd 495 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))
416343, 411, 414, 415vtoclgf 3569 . . . . . . . . 9 (((𝐻)‘𝑗) ∈ (𝐻𝑗) → (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
417416anabsi7 671 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))
418316, 317, 340, 417syl21anc 838 . . . . . . 7 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))
419392, 406, 4183jca 1127 . . . . . 6 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
420419ex 412 . . . . 5 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → (𝑗 ∈ (0...𝑁) → (∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))))
421315, 420ralrimi 3255 . . . 4 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
422309, 421jca 511 . . 3 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ((𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))))
423 feq1 6717 . . . . 5 (𝑥 = (𝐻) → (𝑥:(0...𝑁)⟶𝐴 ↔ (𝐻):(0...𝑁)⟶𝐴))
424 nfcv 2903 . . . . . . 7 𝑗𝑥
425310, 53nfco 5879 . . . . . . 7 𝑗(𝐻)
426424, 425nfeq 2917 . . . . . 6 𝑗 𝑥 = (𝐻)
427 nfcv 2903 . . . . . . . . 9 𝑡𝑥
428427, 381nfeq 2917 . . . . . . . 8 𝑡 𝑥 = (𝐻)
429 fveq1 6906 . . . . . . . . . . 11 (𝑥 = (𝐻) → (𝑥𝑗) = ((𝐻)‘𝑗))
430429fveq1d 6909 . . . . . . . . . 10 (𝑥 = (𝐻) → ((𝑥𝑗)‘𝑡) = (((𝐻)‘𝑗)‘𝑡))
431430breq2d 5160 . . . . . . . . 9 (𝑥 = (𝐻) → (0 ≤ ((𝑥𝑗)‘𝑡) ↔ 0 ≤ (((𝐻)‘𝑗)‘𝑡)))
432430breq1d 5158 . . . . . . . . 9 (𝑥 = (𝐻) → (((𝑥𝑗)‘𝑡) ≤ 1 ↔ (((𝐻)‘𝑗)‘𝑡) ≤ 1))
433431, 432anbi12d 632 . . . . . . . 8 (𝑥 = (𝐻) → ((0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ↔ (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
434428, 433ralbid 3271 . . . . . . 7 (𝑥 = (𝐻) → (∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
435430breq1d 5158 . . . . . . . 8 (𝑥 = (𝐻) → (((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ (((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
436428, 435ralbid 3271 . . . . . . 7 (𝑥 = (𝐻) → (∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
437430breq2d 5160 . . . . . . . 8 (𝑥 = (𝐻) → ((1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
438428, 437ralbid 3271 . . . . . . 7 (𝑥 = (𝐻) → (∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡) ↔ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
439434, 436, 4383anbi123d 1435 . . . . . 6 (𝑥 = (𝐻) → ((∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡)) ↔ (∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))))
440426, 439ralbid 3271 . . . . 5 (𝑥 = (𝐻) → (∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡)) ↔ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))))
441423, 440anbi12d 632 . . . 4 (𝑥 = (𝐻) → ((𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡))) ↔ ((𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))))
442441spcegv 3597 . . 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 1933 1 (𝜑 → ∃𝑥(𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1537  wex 1776  wnf 1780  wcel 2106  wnfc 2888  wne 2938  wral 3059  wrex 3068  {crab 3433  Vcvv 3478  cdif 3960  cin 3962  wss 3963  c0 4339   cuni 4912   class class class wbr 5148  cmpt 5231  dom cdm 5689  ran crn 5690  ccom 5693  Fun wfun 6557   Fn wfn 6558  wf 6559  cfv 6563  (class class class)co 7431  Fincfn 8984  cr 11152  0cc0 11153  1c1 11154   + caddc 11156   · cmul 11158   < clt 11293  cle 11294  cmin 11490   / cdiv 11918  cn 12264  3c3 12320  +crp 13032  (,)cioo 13384  ...cfz 13544  topGenctg 17484  Clsdccld 23040   Cn ccn 23248  Compccmp 23410
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-inf2 9679  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230  ax-pre-sup 11231
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-isom 6572  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8013  df-2nd 8014  df-supp 8185  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-2o 8506  df-er 8744  df-map 8867  df-pm 8868  df-ixp 8937  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-fsupp 9400  df-fi 9449  df-sup 9480  df-inf 9481  df-oi 9548  df-card 9977  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919  df-nn 12265  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334  df-n0 12525  df-z 12612  df-dec 12732  df-uz 12877  df-q 12989  df-rp 13033  df-xneg 13152  df-xadd 13153  df-xmul 13154  df-ioo 13388  df-ioc 13389  df-ico 13390  df-icc 13391  df-fz 13545  df-fzo 13692  df-fl 13829  df-seq 14040  df-exp 14100  df-hash 14367  df-cj 15135  df-re 15136  df-im 15137  df-sqrt 15271  df-abs 15272  df-clim 15521  df-rlim 15522  df-sum 15720  df-struct 17181  df-sets 17198  df-slot 17216  df-ndx 17228  df-base 17246  df-ress 17275  df-plusg 17311  df-mulr 17312  df-starv 17313  df-sca 17314  df-vsca 17315  df-ip 17316  df-tset 17317  df-ple 17318  df-ds 17320  df-unif 17321  df-hom 17322  df-cco 17323  df-rest 17469  df-topn 17470  df-0g 17488  df-gsum 17489  df-topgen 17490  df-pt 17491  df-prds 17494  df-xrs 17549  df-qtop 17554  df-imas 17555  df-xps 17557  df-mre 17631  df-mrc 17632  df-acs 17634  df-mgm 18666  df-sgrp 18745  df-mnd 18761  df-submnd 18810  df-mulg 19099  df-cntz 19348  df-cmn 19815  df-psmet 21374  df-xmet 21375  df-met 21376  df-bl 21377  df-mopn 21378  df-cnfld 21383  df-top 22916  df-topon 22933  df-topsp 22955  df-bases 22969  df-cld 23043  df-cn 23251  df-cnp 23252  df-cmp 23411  df-tx 23586  df-hmeo 23779  df-xms 24346  df-ms 24347  df-tms 24348
This theorem is referenced by:  stoweidlem60  46016
  Copyright terms: Public domain W3C validator