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 43986
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 3423 . . . . . . . . . 10 𝑦{𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)}
31, 2nfcxfr 2903 . . . . . . . . 9 𝑦𝑌
4 nfcv 2905 . . . . . . . . 9 𝑧𝑌
5 nfv 1917 . . . . . . . . 9 𝑧(∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))
6 nfv 1917 . . . . . . . . 9 𝑦(∀𝑡 ∈ (𝐷𝑗)(𝑧𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑧𝑡))
7 fveq1 6829 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝑦𝑡) = (𝑧𝑡))
87breq1d 5107 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝑦𝑡) < (𝐸 / 𝑁) ↔ (𝑧𝑡) < (𝐸 / 𝑁)))
98ralbidv 3171 . . . . . . . . . 10 (𝑦 = 𝑧 → (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷𝑗)(𝑧𝑡) < (𝐸 / 𝑁)))
107breq2d 5109 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ (1 − (𝐸 / 𝑁)) < (𝑧𝑡)))
1110ralbidv 3171 . . . . . . . . . 10 (𝑦 = 𝑧 → (∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑧𝑡)))
129, 11anbi12d 632 . . . . . . . . 9 (𝑦 = 𝑧 → ((∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡)) ↔ (∀𝑡 ∈ (𝐷𝑗)(𝑧𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑧𝑡))))
133, 4, 5, 6, 12cbvrabw 3436 . . . . . . . 8 {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} = {𝑧𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑧𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑧𝑡))}
14 ovexd 7377 . . . . . . . . . 10 (𝜑 → (𝐽 Cn 𝐾) ∈ V)
15 stoweidlem59.11 . . . . . . . . . . 11 (𝜑𝐴𝐶)
16 stoweidlem59.5 . . . . . . . . . . 11 𝐶 = (𝐽 Cn 𝐾)
1715, 16sseqtrdi 3986 . . . . . . . . . 10 (𝜑𝐴 ⊆ (𝐽 Cn 𝐾))
1814, 17ssexd 5273 . . . . . . . . 9 (𝜑𝐴 ∈ V)
191, 18rabexd 5282 . . . . . . . 8 (𝜑𝑌 ∈ V)
2013, 19rabexd 5282 . . . . . . 7 (𝜑 → {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ∈ V)
2120ralrimivw 3144 . . . . . 6 (𝜑 → ∀𝑗 ∈ (0...𝑁){𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ∈ V)
22 stoweidlem59.9 . . . . . . 7 𝐻 = (𝑗 ∈ (0...𝑁) ↦ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
2322fnmpt 6629 . . . . . 6 (∀𝑗 ∈ (0...𝑁){𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ∈ V → 𝐻 Fn (0...𝑁))
2421, 23syl 17 . . . . 5 (𝜑𝐻 Fn (0...𝑁))
25 fzfi 13798 . . . . 5 (0...𝑁) ∈ Fin
26 fnfi 9051 . . . . 5 ((𝐻 Fn (0...𝑁) ∧ (0...𝑁) ∈ Fin) → 𝐻 ∈ Fin)
2724, 25, 26sylancl 587 . . . 4 (𝜑𝐻 ∈ Fin)
28 rnfi 9205 . . . 4 (𝐻 ∈ Fin → ran 𝐻 ∈ Fin)
2927, 28syl 17 . . 3 (𝜑 → ran 𝐻 ∈ Fin)
30 fnchoice 42943 . . 3 (ran 𝐻 ∈ Fin → ∃( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)))
3129, 30syl 17 . 2 (𝜑 → ∃( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)))
32 simprl 769 . . . . 5 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → Fn ran 𝐻)
33 ovex 7375 . . . . . . . 8 (0...𝑁) ∈ V
3433mptex 7160 . . . . . . 7 (𝑗 ∈ (0...𝑁) ↦ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}) ∈ V
3522, 34eqeltri 2834 . . . . . 6 𝐻 ∈ V
3635rnex 7832 . . . . 5 ran 𝐻 ∈ V
37 fnex 7154 . . . . 5 (( Fn ran 𝐻 ∧ ran 𝐻 ∈ V) → ∈ V)
3832, 36, 37sylancl 587 . . . 4 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ∈ V)
39 coexg 7849 . . . 4 (( ∈ V ∧ 𝐻 ∈ V) → (𝐻) ∈ V)
4038, 35, 39sylancl 587 . . 3 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → (𝐻) ∈ V)
41 dffn3 6669 . . . . . . 7 ( Fn ran 𝐻:ran 𝐻⟶ran )
4232, 41sylib 217 . . . . . 6 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → :ran 𝐻⟶ran )
43 nfv 1917 . . . . . . . . . 10 𝑤𝜑
44 nfv 1917 . . . . . . . . . . 11 𝑤 Fn ran 𝐻
45 nfra1 3264 . . . . . . . . . . 11 𝑤𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)
4644, 45nfan 1902 . . . . . . . . . 10 𝑤( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))
4743, 46nfan 1902 . . . . . . . . 9 𝑤(𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)))
48 simplrr 776 . . . . . . . . . . 11 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))
49 simpr 486 . . . . . . . . . . 11 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → 𝑤 ∈ ran 𝐻)
50 fvelrnb 6891 . . . . . . . . . . . . . . . 16 (𝐻 Fn (0...𝑁) → (𝑤 ∈ ran 𝐻 ↔ ∃𝑎 ∈ (0...𝑁)(𝐻𝑎) = 𝑤))
51 nfv 1917 . . . . . . . . . . . . . . . . 17 𝑎(𝐻𝑗) = 𝑤
52 nfmpt1 5205 . . . . . . . . . . . . . . . . . . . 20 𝑗(𝑗 ∈ (0...𝑁) ↦ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
5322, 52nfcxfr 2903 . . . . . . . . . . . . . . . . . . 19 𝑗𝐻
54 nfcv 2905 . . . . . . . . . . . . . . . . . . 19 𝑗𝑎
5553, 54nffv 6840 . . . . . . . . . . . . . . . . . 18 𝑗(𝐻𝑎)
56 nfcv 2905 . . . . . . . . . . . . . . . . . 18 𝑗𝑤
5755, 56nfeq 2918 . . . . . . . . . . . . . . . . 17 𝑗(𝐻𝑎) = 𝑤
58 fveq2 6830 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑎 → (𝐻𝑗) = (𝐻𝑎))
5958eqeq1d 2739 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑎 → ((𝐻𝑗) = 𝑤 ↔ (𝐻𝑎) = 𝑤))
6051, 57, 59cbvrexw 3287 . . . . . . . . . . . . . . . 16 (∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤 ↔ ∃𝑎 ∈ (0...𝑁)(𝐻𝑎) = 𝑤)
6150, 60bitr4di 289 . . . . . . . . . . . . . . 15 (𝐻 Fn (0...𝑁) → (𝑤 ∈ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤))
6224, 61syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑤 ∈ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤))
6362biimpa 478 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ran 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤)
64 simp3 1138 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑁) ∧ (𝐻𝑗) = 𝑤) → (𝐻𝑗) = 𝑤)
65 simpr 486 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
6620adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ∈ V)
6722fvmpt2 6947 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ (0...𝑁) ∧ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ∈ V) → (𝐻𝑗) = {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
6865, 66, 67syl2anc 585 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐻𝑗) = {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
69 stoweidlem59.6 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
70 nfcv 2905 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡(0...𝑁)
71 nfrab1 3423 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡{𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}
7270, 71nfmpt 5204 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
7369, 72nfcxfr 2903 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡𝐷
74 nfcv 2905 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡𝑗
7573, 74nffv 6840 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝐷𝑗)
76 nfcv 2905 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡𝑇
77 stoweidlem59.7 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
78 nfrab1 3423 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑡{𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)}
7970, 78nfmpt 5204 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
8077, 79nfcxfr 2903 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡𝐵
8180, 74nffv 6840 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡(𝐵𝑗)
8276, 81nfdif 4077 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝑇 ∖ (𝐵𝑗))
83 stoweidlem59.2 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡𝜑
84 nfv 1917 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡 𝑗 ∈ (0...𝑁)
8583, 84nfan 1902 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝜑𝑗 ∈ (0...𝑁))
86 stoweidlem59.3 . . . . . . . . . . . . . . . . . . . . . . 23 𝐾 = (topGen‘ran (,))
87 stoweidlem59.4 . . . . . . . . . . . . . . . . . . . . . . 23 𝑇 = 𝐽
88 stoweidlem59.10 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐽 ∈ Comp)
8988adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → 𝐽 ∈ Comp)
9015adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → 𝐴𝐶)
91 stoweidlem59.12 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
92913adant1r 1177 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
93 stoweidlem59.13 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
94933adant1r 1177 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
95 stoweidlem59.14 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ ℝ) → (𝑡𝑇𝑦) ∈ 𝐴)
9695adantlr 713 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ ℝ) → (𝑡𝑇𝑦) ∈ 𝐴)
97 stoweidlem59.15 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟𝑇𝑡𝑇𝑟𝑡)) → ∃𝑞𝐴 (𝑞𝑟) ≠ (𝑞𝑡))
9897adantlr 713 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑟𝑇𝑡𝑇𝑟𝑡)) → ∃𝑞𝐴 (𝑞𝑟) ≠ (𝑞𝑡))
9988uniexd 7662 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 𝐽 ∈ V)
10087, 99eqeltrid 2842 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑇 ∈ V)
101100adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇 ∈ V)
102 rabexg 5280 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑇 ∈ V → {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V)
103101, 102syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V)
10477fvmpt2 6947 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗 ∈ (0...𝑁) ∧ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V) → (𝐵𝑗) = {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
10565, 103, 104syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐵𝑗) = {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
106 stoweidlem59.1 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡𝐹
107 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . . 25 {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} = {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)}
108 elfzelz 13362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
109108zred 12532 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
110 3re 12159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3 ∈ ℝ
111 3ne0 12185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3 ≠ 0
112110, 111rereccli 11846 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (1 / 3) ∈ ℝ
113 readdcl 11060 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ) → (𝑗 + (1 / 3)) ∈ ℝ)
114109, 112, 113sylancl 587 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑁) → (𝑗 + (1 / 3)) ∈ ℝ)
115114adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑗 + (1 / 3)) ∈ ℝ)
116 stoweidlem59.17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐸 ∈ ℝ+)
117116rpred 12878 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐸 ∈ ℝ)
118117adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → 𝐸 ∈ ℝ)
119115, 118remulcld 11111 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑗 + (1 / 3)) · 𝐸) ∈ ℝ)
120 stoweidlem59.16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐹𝐶)
121120, 16eleqtrdi 2848 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐹 ∈ (𝐽 Cn 𝐾))
122121adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → 𝐹 ∈ (𝐽 Cn 𝐾))
123106, 86, 87, 107, 119, 122rfcnpre3 42947 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ (Clsd‘𝐽))
124105, 123eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐵𝑗) ∈ (Clsd‘𝐽))
125 rabexg 5280 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V)
126101, 125syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V)
12769fvmpt2 6947 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗 ∈ (0...𝑁) ∧ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V) → (𝐷𝑗) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
12865, 126, 127syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐷𝑗) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
129 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . . . 25 {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}
130 resubcl 11391 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ) → (𝑗 − (1 / 3)) ∈ ℝ)
131109, 112, 130sylancl 587 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑁) → (𝑗 − (1 / 3)) ∈ ℝ)
132131adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑗 − (1 / 3)) ∈ ℝ)
133132, 118remulcld 11111 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ)
134106, 86, 87, 129, 133, 122rfcnpre4 42948 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ (Clsd‘𝐽))
135128, 134eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐷𝑗) ∈ (Clsd‘𝐽))
136133adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ)
137119adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ((𝑗 + (1 / 3)) · 𝐸) ∈ ℝ)
13886, 87, 16, 120fcnre 42939 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝐹:𝑇⟶ℝ)
139138ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → 𝐹:𝑇⟶ℝ)
140 ssrab2 4029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ⊆ 𝑇
141105, 140eqsstrdi 3990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐵𝑗) ⊆ 𝑇)
142141sselda 3936 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → 𝑡𝑇)
143139, 142ffvelcdmd 7023 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → (𝐹𝑡) ∈ ℝ)
144112, 130mpan2 689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) ∈ ℝ)
145 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ → 𝑗 ∈ ℝ)
146112, 113mpan2 689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ → (𝑗 + (1 / 3)) ∈ ℝ)
147 3pos 12184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 0 < 3
148110, 147recgt0ii 11987 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 0 < (1 / 3)
149112, 148elrpii 12839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (1 / 3) ∈ ℝ+
150 ltsubrp 12872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ+) → (𝑗 − (1 / 3)) < 𝑗)
151149, 150mpan2 689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) < 𝑗)
152 ltaddrp 12873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ+) → 𝑗 < (𝑗 + (1 / 3)))
153149, 152mpan2 689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ → 𝑗 < (𝑗 + (1 / 3)))
154144, 145, 146, 151, 153lttrd 11242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
155109, 154syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 ∈ (0...𝑁) → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
156155adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
157116rpregt0d 12884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
158157adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
159 ltmul1 11931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑗 − (1 / 3)) ∈ ℝ ∧ (𝑗 + (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑗 − (1 / 3)) < (𝑗 + (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸)))
160132, 115, 158, 159syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) < (𝑗 + (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸)))
161156, 160mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸))
162161adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸))
163105eleq2d 2823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑡 ∈ (𝐵𝑗) ↔ 𝑡 ∈ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)}))
164163biimpa 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → 𝑡 ∈ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
165 rabid 3424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑡 ∈ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ↔ (𝑡𝑇 ∧ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)))
166164, 165sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → (𝑡𝑇 ∧ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)))
167166simprd 497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡))
168136, 137, 143, 162, 167ltletrd 11241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) < (𝐹𝑡))
169136, 143ltnled 11228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → (((𝑗 − (1 / 3)) · 𝐸) < (𝐹𝑡) ↔ ¬ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
170168, 169mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ¬ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))
171170intnand 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ¬ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
172 rabid 3424 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
173171, 172sylnibr 329 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ¬ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
174128adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → (𝐷𝑗) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
175173, 174neleqtrrd 2860 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ¬ 𝑡 ∈ (𝐷𝑗))
176175ex 414 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑡 ∈ (𝐵𝑗) → ¬ 𝑡 ∈ (𝐷𝑗)))
17785, 176ralrimi 3237 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐵𝑗) ¬ 𝑡 ∈ (𝐷𝑗))
178 disj 4399 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐵𝑗) ∩ (𝐷𝑗)) = ∅ ↔ ∀𝑎 ∈ (𝐵𝑗) ¬ 𝑎 ∈ (𝐷𝑗))
179 nfcv 2905 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑎(𝐵𝑗)
18075nfcri 2892 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑡 𝑎 ∈ (𝐷𝑗)
181180nfn 1860 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡 ¬ 𝑎 ∈ (𝐷𝑗)
182 nfv 1917 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑎 ¬ 𝑡 ∈ (𝐷𝑗)
183 eleq1 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑡 → (𝑎 ∈ (𝐷𝑗) ↔ 𝑡 ∈ (𝐷𝑗)))
184183notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = 𝑡 → (¬ 𝑎 ∈ (𝐷𝑗) ↔ ¬ 𝑡 ∈ (𝐷𝑗)))
185179, 81, 181, 182, 184cbvralfw 3284 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑎 ∈ (𝐵𝑗) ¬ 𝑎 ∈ (𝐷𝑗) ↔ ∀𝑡 ∈ (𝐵𝑗) ¬ 𝑡 ∈ (𝐷𝑗))
186178, 185bitri 275 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐵𝑗) ∩ (𝐷𝑗)) = ∅ ↔ ∀𝑡 ∈ (𝐵𝑗) ¬ 𝑡 ∈ (𝐷𝑗))
187177, 186sylibr 233 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝐵𝑗) ∩ (𝐷𝑗)) = ∅)
188 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑇 ∖ (𝐵𝑗)) = (𝑇 ∖ (𝐵𝑗))
189 stoweidlem59.19 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑁 ∈ ℕ)
190189nnrpd 12876 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑁 ∈ ℝ+)
191116, 190rpdivcld 12895 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐸 / 𝑁) ∈ ℝ+)
192191adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐸 / 𝑁) ∈ ℝ+)
193117, 189nndivred 12133 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐸 / 𝑁) ∈ ℝ)
194112a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (1 / 3) ∈ ℝ)
195189nnge1d 12127 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → 1 ≤ 𝑁)
196 1re 11081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 1 ∈ ℝ
197 0lt1 11603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 0 < 1
198196, 197pm3.2i 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (1 ∈ ℝ ∧ 0 < 1)
199198a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (1 ∈ ℝ ∧ 0 < 1))
200189nnred 12094 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑁 ∈ ℝ)
201189nngt0d 12128 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → 0 < 𝑁)
202 lediv2 11971 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((1 ∈ ℝ ∧ 0 < 1) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (1 ≤ 𝑁 ↔ (𝐸 / 𝑁) ≤ (𝐸 / 1)))
203199, 200, 201, 157, 202syl121anc 1375 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (1 ≤ 𝑁 ↔ (𝐸 / 𝑁) ≤ (𝐸 / 1)))
204195, 203mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐸 / 𝑁) ≤ (𝐸 / 1))
205116rpcnd 12880 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐸 ∈ ℂ)
206205div1d 11849 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐸 / 1) = 𝐸)
207204, 206breqtrd 5123 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐸 / 𝑁) ≤ 𝐸)
208 stoweidlem59.18 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐸 < (1 / 3))
209193, 117, 194, 207, 208lelttrd 11239 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐸 / 𝑁) < (1 / 3))
210209adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐸 / 𝑁) < (1 / 3))
21175, 82, 85, 86, 87, 16, 89, 90, 92, 94, 96, 98, 124, 135, 187, 188, 192, 210stoweidlem58 43985 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (0...𝑁)) → ∃𝑥𝐴 (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))
212 df-rex 3072 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑥𝐴 (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)) ↔ ∃𝑥(𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))))
213211, 212sylib 217 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0...𝑁)) → ∃𝑥(𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))))
214 simprl 769 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → 𝑥𝐴)
215 simprr1 1221 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → ∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1))
216 fveq1 6829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 = 𝑥 → (𝑦𝑡) = (𝑥𝑡))
217216breq2d 5109 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = 𝑥 → (0 ≤ (𝑦𝑡) ↔ 0 ≤ (𝑥𝑡)))
218216breq1d 5107 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = 𝑥 → ((𝑦𝑡) ≤ 1 ↔ (𝑥𝑡) ≤ 1))
219217, 218anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = 𝑥 → ((0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1) ↔ (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1)))
220219ralbidv 3171 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑥 → (∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1)))
221220, 1elrab2 3641 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥𝑌 ↔ (𝑥𝐴 ∧ ∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1)))
222214, 215, 221sylanbrc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → 𝑥𝑌)
223 simprr2 1222 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁))
224 simprr3 1223 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))
225223, 224jca 513 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → (∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))
226 nfcv 2905 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦𝑥
227 nfv 1917 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦(∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))
228216breq1d 5107 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = 𝑥 → ((𝑦𝑡) < (𝐸 / 𝑁) ↔ (𝑥𝑡) < (𝐸 / 𝑁)))
229228ralbidv 3171 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑥 → (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁)))
230216breq2d 5109 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = 𝑥 → ((1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ (1 − (𝐸 / 𝑁)) < (𝑥𝑡)))
231230ralbidv 3171 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑥 → (∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))
232229, 231anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑥 → ((∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡)) ↔ (∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))))
233226, 3, 227, 232elrabf 3634 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ↔ (𝑥𝑌 ∧ (∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))))
234222, 225, 233sylanbrc 584 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → 𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
235234ex 414 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))) → 𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}))
236235eximdv 1920 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0...𝑁)) → (∃𝑥(𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))) → ∃𝑥 𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}))
237213, 236mpd 15 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑁)) → ∃𝑥 𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
238 ne0i 4286 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} → {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ≠ ∅)
239238exlimiv 1933 . . . . . . . . . . . . . . . . . . . 20 (∃𝑥 𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} → {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ≠ ∅)
240237, 239syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ≠ ∅)
24168, 240eqnetrd 3009 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐻𝑗) ≠ ∅)
2422413adant3 1132 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑁) ∧ (𝐻𝑗) = 𝑤) → (𝐻𝑗) ≠ ∅)
24364, 242eqnetrrd 3010 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑁) ∧ (𝐻𝑗) = 𝑤) → 𝑤 ≠ ∅)
2442433exp 1119 . . . . . . . . . . . . . . 15 (𝜑 → (𝑗 ∈ (0...𝑁) → ((𝐻𝑗) = 𝑤𝑤 ≠ ∅)))
245244rexlimdv 3147 . . . . . . . . . . . . . 14 (𝜑 → (∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤𝑤 ≠ ∅))
246245adantr 482 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ran 𝐻) → (∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤𝑤 ≠ ∅))
24763, 246mpd 15 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ran 𝐻) → 𝑤 ≠ ∅)
248247adantlr 713 . . . . . . . . . . 11 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → 𝑤 ≠ ∅)
249 rsp 3227 . . . . . . . . . . 11 (∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤) → (𝑤 ∈ ran 𝐻 → (𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)))
25048, 49, 248, 249syl3c 66 . . . . . . . . . 10 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → (𝑤) ∈ 𝑤)
251250ex 414 . . . . . . . . 9 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → (𝑤 ∈ ran 𝐻 → (𝑤) ∈ 𝑤))
25247, 251ralrimi 3237 . . . . . . . 8 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ∀𝑤 ∈ ran 𝐻(𝑤) ∈ 𝑤)
253 chfnrn 6987 . . . . . . . 8 (( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤) ∈ 𝑤) → ran ran 𝐻)
25432, 252, 253syl2anc 585 . . . . . . 7 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ran ran 𝐻)
255 nfv 1917 . . . . . . . . . 10 𝑦𝜑
256 nfcv 2905 . . . . . . . . . . . 12 𝑦
257 nfcv 2905 . . . . . . . . . . . . . . 15 𝑦(0...𝑁)
258 nfrab1 3423 . . . . . . . . . . . . . . 15 𝑦{𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}
259257, 258nfmpt 5204 . . . . . . . . . . . . . 14 𝑦(𝑗 ∈ (0...𝑁) ↦ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
26022, 259nfcxfr 2903 . . . . . . . . . . . . 13 𝑦𝐻
261260nfrn 5898 . . . . . . . . . . . 12 𝑦ran 𝐻
262256, 261nffn 6589 . . . . . . . . . . 11 𝑦 Fn ran 𝐻
263 nfv 1917 . . . . . . . . . . . 12 𝑦(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)
264261, 263nfralw 3291 . . . . . . . . . . 11 𝑦𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)
265262, 264nfan 1902 . . . . . . . . . 10 𝑦( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))
266255, 265nfan 1902 . . . . . . . . 9 𝑦(𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)))
267261nfuni 4864 . . . . . . . . 9 𝑦 ran 𝐻
268 fnunirn 7188 . . . . . . . . . . . . . . 15 (𝐻 Fn (0...𝑁) → (𝑦 ran 𝐻 ↔ ∃𝑧 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑧)))
269 nfcv 2905 . . . . . . . . . . . . . . . . . 18 𝑗𝑧
27053, 269nffv 6840 . . . . . . . . . . . . . . . . 17 𝑗(𝐻𝑧)
271270nfcri 2892 . . . . . . . . . . . . . . . 16 𝑗 𝑦 ∈ (𝐻𝑧)
272 nfv 1917 . . . . . . . . . . . . . . . 16 𝑧 𝑦 ∈ (𝐻𝑗)
273 fveq2 6830 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑗 → (𝐻𝑧) = (𝐻𝑗))
274273eleq2d 2823 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑗 → (𝑦 ∈ (𝐻𝑧) ↔ 𝑦 ∈ (𝐻𝑗)))
275271, 272, 274cbvrexw 3287 . . . . . . . . . . . . . . 15 (∃𝑧 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑧) ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑗))
276268, 275bitrdi 287 . . . . . . . . . . . . . 14 (𝐻 Fn (0...𝑁) → (𝑦 ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑗)))
27724, 276syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑦 ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑗)))
278277biimpa 478 . . . . . . . . . . . 12 ((𝜑𝑦 ran 𝐻) → ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑗))
279 nfv 1917 . . . . . . . . . . . . . 14 𝑗𝜑
28053nfrn 5898 . . . . . . . . . . . . . . . 16 𝑗ran 𝐻
281280nfuni 4864 . . . . . . . . . . . . . . 15 𝑗 ran 𝐻
282281nfcri 2892 . . . . . . . . . . . . . 14 𝑗 𝑦 ran 𝐻
283279, 282nfan 1902 . . . . . . . . . . . . 13 𝑗(𝜑𝑦 ran 𝐻)
284 nfv 1917 . . . . . . . . . . . . 13 𝑗 𝑦𝑌
285 simp1l 1197 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝜑)
286 simp2 1137 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑗 ∈ (0...𝑁))
287 simp3 1138 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑦 ∈ (𝐻𝑗))
28868eleq2d 2823 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑦 ∈ (𝐻𝑗) ↔ 𝑦 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}))
289288biimpa 478 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑦 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
290 rabid 3424 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ↔ (𝑦𝑌 ∧ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))))
291289, 290sylib 217 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → (𝑦𝑌 ∧ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))))
292291simpld 496 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑦𝑌)
293285, 286, 287, 292syl21anc 836 . . . . . . . . . . . . . 14 (((𝜑𝑦 ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑦𝑌)
2942933exp 1119 . . . . . . . . . . . . 13 ((𝜑𝑦 ran 𝐻) → (𝑗 ∈ (0...𝑁) → (𝑦 ∈ (𝐻𝑗) → 𝑦𝑌)))
295283, 284, 294rexlimd 3246 . . . . . . . . . . . 12 ((𝜑𝑦 ran 𝐻) → (∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑗) → 𝑦𝑌))
296278, 295mpd 15 . . . . . . . . . . 11 ((𝜑𝑦 ran 𝐻) → 𝑦𝑌)
297296adantlr 713 . . . . . . . . . 10 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑦 ran 𝐻) → 𝑦𝑌)
298297ex 414 . . . . . . . . 9 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → (𝑦 ran 𝐻𝑦𝑌))
299266, 267, 3, 298ssrd 3941 . . . . . . . 8 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ran 𝐻𝑌)
300 ssrab2 4029 . . . . . . . . 9 {𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)} ⊆ 𝐴
3011, 300eqsstri 3970 . . . . . . . 8 𝑌𝐴
302299, 301sstrdi 3948 . . . . . . 7 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ran 𝐻𝐴)
303254, 302sstrd 3946 . . . . . 6 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ran 𝐴)
30442, 303fssd 6674 . . . . 5 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → :ran 𝐻𝐴)
305 dffn3 6669 . . . . . . 7 (𝐻 Fn (0...𝑁) ↔ 𝐻:(0...𝑁)⟶ran 𝐻)
30624, 305sylib 217 . . . . . 6 (𝜑𝐻:(0...𝑁)⟶ran 𝐻)
307306adantr 482 . . . . 5 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → 𝐻:(0...𝑁)⟶ran 𝐻)
308 fco 6680 . . . . 5 ((:ran 𝐻𝐴𝐻:(0...𝑁)⟶ran 𝐻) → (𝐻):(0...𝑁)⟶𝐴)
309304, 307, 308syl2anc 585 . . . 4 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → (𝐻):(0...𝑁)⟶𝐴)
310 nfcv 2905 . . . . . . . 8 𝑗
311310, 280nffn 6589 . . . . . . 7 𝑗 Fn ran 𝐻
312 nfv 1917 . . . . . . . 8 𝑗(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)
313280, 312nfralw 3291 . . . . . . 7 𝑗𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)
314311, 313nfan 1902 . . . . . 6 𝑗( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))
315279, 314nfan 1902 . . . . 5 𝑗(𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)))
316 simpll 765 . . . . . . . . . 10 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝜑)
317 simpr 486 . . . . . . . . . 10 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
31824ad2antrr 724 . . . . . . . . . . . 12 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝐻 Fn (0...𝑁))
319 fvco2 6926 . . . . . . . . . . . 12 ((𝐻 Fn (0...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → ((𝐻)‘𝑗) = (‘(𝐻𝑗)))
320318, 319sylancom 589 . . . . . . . . . . 11 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝐻)‘𝑗) = (‘(𝐻𝑗)))
321 simplrr 776 . . . . . . . . . . . . 13 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))
322 fnfun 6590 . . . . . . . . . . . . . . . 16 (𝐻 Fn (0...𝑁) → Fun 𝐻)
32324, 322syl 17 . . . . . . . . . . . . . . 15 (𝜑 → Fun 𝐻)
324323ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → Fun 𝐻)
32524fndmd 6595 . . . . . . . . . . . . . . . . 17 (𝜑 → dom 𝐻 = (0...𝑁))
326325adantr 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑁)) → dom 𝐻 = (0...𝑁))
32765, 326eleqtrrd 2841 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑗 ∈ dom 𝐻)
328327adantlr 713 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ dom 𝐻)
329 fvelrn 7015 . . . . . . . . . . . . . 14 ((Fun 𝐻𝑗 ∈ dom 𝐻) → (𝐻𝑗) ∈ ran 𝐻)
330324, 328, 329syl2anc 585 . . . . . . . . . . . . 13 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (𝐻𝑗) ∈ ran 𝐻)
331321, 330jca 513 . . . . . . . . . . . 12 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤) ∧ (𝐻𝑗) ∈ ran 𝐻))
332241adantlr 713 . . . . . . . . . . . 12 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (𝐻𝑗) ≠ ∅)
333 neeq1 3004 . . . . . . . . . . . . . 14 (𝑤 = (𝐻𝑗) → (𝑤 ≠ ∅ ↔ (𝐻𝑗) ≠ ∅))
334 fveq2 6830 . . . . . . . . . . . . . . 15 (𝑤 = (𝐻𝑗) → (𝑤) = (‘(𝐻𝑗)))
335 id 22 . . . . . . . . . . . . . . 15 (𝑤 = (𝐻𝑗) → 𝑤 = (𝐻𝑗))
336334, 335eleq12d 2832 . . . . . . . . . . . . . 14 (𝑤 = (𝐻𝑗) → ((𝑤) ∈ 𝑤 ↔ (‘(𝐻𝑗)) ∈ (𝐻𝑗)))
337333, 336imbi12d 345 . . . . . . . . . . . . 13 (𝑤 = (𝐻𝑗) → ((𝑤 ≠ ∅ → (𝑤) ∈ 𝑤) ↔ ((𝐻𝑗) ≠ ∅ → (‘(𝐻𝑗)) ∈ (𝐻𝑗))))
338337rspccva 3573 . . . . . . . . . . . 12 ((∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤) ∧ (𝐻𝑗) ∈ ran 𝐻) → ((𝐻𝑗) ≠ ∅ → (‘(𝐻𝑗)) ∈ (𝐻𝑗)))
339331, 332, 338sylc 65 . . . . . . . . . . 11 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (‘(𝐻𝑗)) ∈ (𝐻𝑗))
340320, 339eqeltrd 2838 . . . . . . . . . 10 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝐻)‘𝑗) ∈ (𝐻𝑗))
341256, 260nfco 5812 . . . . . . . . . . . . 13 𝑦(𝐻)
342 nfcv 2905 . . . . . . . . . . . . 13 𝑦𝑗
343341, 342nffv 6840 . . . . . . . . . . . 12 𝑦((𝐻)‘𝑗)
344 nfv 1917 . . . . . . . . . . . . . 14 𝑦(𝜑𝑗 ∈ (0...𝑁))
345260, 342nffv 6840 . . . . . . . . . . . . . . 15 𝑦(𝐻𝑗)
346343, 345nfel 2919 . . . . . . . . . . . . . 14 𝑦((𝐻)‘𝑗) ∈ (𝐻𝑗)
347344, 346nfan 1902 . . . . . . . . . . . . 13 𝑦((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗))
348343, 3nfel 2919 . . . . . . . . . . . . 13 𝑦((𝐻)‘𝑗) ∈ 𝑌
349347, 348nfim 1899 . . . . . . . . . . . 12 𝑦(((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ((𝐻)‘𝑗) ∈ 𝑌)
350 eleq1 2825 . . . . . . . . . . . . . 14 (𝑦 = ((𝐻)‘𝑗) → (𝑦 ∈ (𝐻𝑗) ↔ ((𝐻)‘𝑗) ∈ (𝐻𝑗)))
351350anbi2d 630 . . . . . . . . . . . . 13 (𝑦 = ((𝐻)‘𝑗) → (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) ↔ ((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗))))
352 eleq1 2825 . . . . . . . . . . . . 13 (𝑦 = ((𝐻)‘𝑗) → (𝑦𝑌 ↔ ((𝐻)‘𝑗) ∈ 𝑌))
353351, 352imbi12d 345 . . . . . . . . . . . 12 (𝑦 = ((𝐻)‘𝑗) → ((((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑦𝑌) ↔ (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ((𝐻)‘𝑗) ∈ 𝑌)))
354343, 349, 353, 292vtoclgf 3516 . . . . . . . . . . 11 (((𝐻)‘𝑗) ∈ (𝐻𝑗) → (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ((𝐻)‘𝑗) ∈ 𝑌))
355354anabsi7 669 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ((𝐻)‘𝑗) ∈ 𝑌)
356316, 317, 340, 355syl21anc 836 . . . . . . . . 9 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝐻)‘𝑗) ∈ 𝑌)
3571eleq2i 2829 . . . . . . . . . 10 (((𝐻)‘𝑗) ∈ 𝑌 ↔ ((𝐻)‘𝑗) ∈ {𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)})
358 nfcv 2905 . . . . . . . . . . 11 𝑦𝐴
359 nfcv 2905 . . . . . . . . . . . 12 𝑦𝑇
360 nfcv 2905 . . . . . . . . . . . . . 14 𝑦0
361 nfcv 2905 . . . . . . . . . . . . . 14 𝑦
362 nfcv 2905 . . . . . . . . . . . . . . 15 𝑦𝑡
363343, 362nffv 6840 . . . . . . . . . . . . . 14 𝑦(((𝐻)‘𝑗)‘𝑡)
364360, 361, 363nfbr 5144 . . . . . . . . . . . . 13 𝑦0 ≤ (((𝐻)‘𝑗)‘𝑡)
365 nfcv 2905 . . . . . . . . . . . . . 14 𝑦1
366363, 361, 365nfbr 5144 . . . . . . . . . . . . 13 𝑦(((𝐻)‘𝑗)‘𝑡) ≤ 1
367364, 366nfan 1902 . . . . . . . . . . . 12 𝑦(0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)
368359, 367nfralw 3291 . . . . . . . . . . 11 𝑦𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)
369 nfcv 2905 . . . . . . . . . . . . 13 𝑡𝑦
370 nfcv 2905 . . . . . . . . . . . . . . 15 𝑡
371 nfra1 3264 . . . . . . . . . . . . . . . . . . 19 𝑡𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁)
372 nfra1 3264 . . . . . . . . . . . . . . . . . . 19 𝑡𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡)
373371, 372nfan 1902 . . . . . . . . . . . . . . . . . 18 𝑡(∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))
374 nfra1 3264 . . . . . . . . . . . . . . . . . . . 20 𝑡𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)
375 nfcv 2905 . . . . . . . . . . . . . . . . . . . 20 𝑡𝐴
376374, 375nfrabw 3437 . . . . . . . . . . . . . . . . . . 19 𝑡{𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)}
3771, 376nfcxfr 2903 . . . . . . . . . . . . . . . . . 18 𝑡𝑌
378373, 377nfrabw 3437 . . . . . . . . . . . . . . . . 17 𝑡{𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}
37970, 378nfmpt 5204 . . . . . . . . . . . . . . . 16 𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
38022, 379nfcxfr 2903 . . . . . . . . . . . . . . 15 𝑡𝐻
381370, 380nfco 5812 . . . . . . . . . . . . . 14 𝑡(𝐻)
382381, 74nffv 6840 . . . . . . . . . . . . 13 𝑡((𝐻)‘𝑗)
383369, 382nfeq 2918 . . . . . . . . . . . 12 𝑡 𝑦 = ((𝐻)‘𝑗)
384 fveq1 6829 . . . . . . . . . . . . . 14 (𝑦 = ((𝐻)‘𝑗) → (𝑦𝑡) = (((𝐻)‘𝑗)‘𝑡))
385384breq2d 5109 . . . . . . . . . . . . 13 (𝑦 = ((𝐻)‘𝑗) → (0 ≤ (𝑦𝑡) ↔ 0 ≤ (((𝐻)‘𝑗)‘𝑡)))
386384breq1d 5107 . . . . . . . . . . . . 13 (𝑦 = ((𝐻)‘𝑗) → ((𝑦𝑡) ≤ 1 ↔ (((𝐻)‘𝑗)‘𝑡) ≤ 1))
387385, 386anbi12d 632 . . . . . . . . . . . 12 (𝑦 = ((𝐻)‘𝑗) → ((0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1) ↔ (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
388383, 387ralbid 3253 . . . . . . . . . . 11 (𝑦 = ((𝐻)‘𝑗) → (∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
389343, 358, 368, 388elrabf 3634 . . . . . . . . . 10 (((𝐻)‘𝑗) ∈ {𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)} ↔ (((𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
390357, 389bitri 275 . . . . . . . . 9 (((𝐻)‘𝑗) ∈ 𝑌 ↔ (((𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
391356, 390sylib 217 . . . . . . . 8 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (((𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
392391simprd 497 . . . . . . 7 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1))
393 nfcv 2905 . . . . . . . . . . . 12 𝑦(𝐷𝑗)
394 nfcv 2905 . . . . . . . . . . . . 13 𝑦 <
395 nfcv 2905 . . . . . . . . . . . . 13 𝑦(𝐸 / 𝑁)
396363, 394, 395nfbr 5144 . . . . . . . . . . . 12 𝑦(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)
397393, 396nfralw 3291 . . . . . . . . . . 11 𝑦𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)
398347, 397nfim 1899 . . . . . . . . . 10 𝑦(((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))
399384breq1d 5107 . . . . . . . . . . . 12 (𝑦 = ((𝐻)‘𝑗) → ((𝑦𝑡) < (𝐸 / 𝑁) ↔ (((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
400383, 399ralbid 3253 . . . . . . . . . . 11 (𝑦 = ((𝐻)‘𝑗) → (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
401351, 400imbi12d 345 . . . . . . . . . 10 (𝑦 = ((𝐻)‘𝑗) → ((((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁)) ↔ (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))))
402291simprd 497 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡)))
403402simpld 496 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁))
404343, 398, 401, 403vtoclgf 3516 . . . . . . . . 9 (((𝐻)‘𝑗) ∈ (𝐻𝑗) → (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
405404anabsi7 669 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))
406316, 317, 340, 405syl21anc 836 . . . . . . 7 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))
407 nfcv 2905 . . . . . . . . . . . 12 𝑦(𝐵𝑗)
408 nfcv 2905 . . . . . . . . . . . . 13 𝑦(1 − (𝐸 / 𝑁))
409408, 394, 363nfbr 5144 . . . . . . . . . . . 12 𝑦(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)
410407, 409nfralw 3291 . . . . . . . . . . 11 𝑦𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)
411347, 410nfim 1899 . . . . . . . . . 10 𝑦(((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))
412384breq2d 5109 . . . . . . . . . . . 12 (𝑦 = ((𝐻)‘𝑗) → ((1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ (1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
413383, 412ralbid 3253 . . . . . . . . . . 11 (𝑦 = ((𝐻)‘𝑗) → (∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
414351, 413imbi12d 345 . . . . . . . . . 10 (𝑦 = ((𝐻)‘𝑗) → ((((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡)) ↔ (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))))
415402simprd 497 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))
416343, 411, 414, 415vtoclgf 3516 . . . . . . . . 9 (((𝐻)‘𝑗) ∈ (𝐻𝑗) → (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
417416anabsi7 669 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))
418316, 317, 340, 417syl21anc 836 . . . . . . 7 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))
419392, 406, 4183jca 1128 . . . . . 6 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
420419ex 414 . . . . 5 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → (𝑗 ∈ (0...𝑁) → (∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))))
421315, 420ralrimi 3237 . . . 4 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
422309, 421jca 513 . . 3 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ((𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))))
423 feq1 6637 . . . . 5 (𝑥 = (𝐻) → (𝑥:(0...𝑁)⟶𝐴 ↔ (𝐻):(0...𝑁)⟶𝐴))
424 nfcv 2905 . . . . . . 7 𝑗𝑥
425310, 53nfco 5812 . . . . . . 7 𝑗(𝐻)
426424, 425nfeq 2918 . . . . . 6 𝑗 𝑥 = (𝐻)
427 nfcv 2905 . . . . . . . . 9 𝑡𝑥
428427, 381nfeq 2918 . . . . . . . 8 𝑡 𝑥 = (𝐻)
429 fveq1 6829 . . . . . . . . . . 11 (𝑥 = (𝐻) → (𝑥𝑗) = ((𝐻)‘𝑗))
430429fveq1d 6832 . . . . . . . . . 10 (𝑥 = (𝐻) → ((𝑥𝑗)‘𝑡) = (((𝐻)‘𝑗)‘𝑡))
431430breq2d 5109 . . . . . . . . 9 (𝑥 = (𝐻) → (0 ≤ ((𝑥𝑗)‘𝑡) ↔ 0 ≤ (((𝐻)‘𝑗)‘𝑡)))
432430breq1d 5107 . . . . . . . . 9 (𝑥 = (𝐻) → (((𝑥𝑗)‘𝑡) ≤ 1 ↔ (((𝐻)‘𝑗)‘𝑡) ≤ 1))
433431, 432anbi12d 632 . . . . . . . 8 (𝑥 = (𝐻) → ((0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ↔ (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
434428, 433ralbid 3253 . . . . . . 7 (𝑥 = (𝐻) → (∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
435430breq1d 5107 . . . . . . . 8 (𝑥 = (𝐻) → (((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ (((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
436428, 435ralbid 3253 . . . . . . 7 (𝑥 = (𝐻) → (∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
437430breq2d 5109 . . . . . . . 8 (𝑥 = (𝐻) → ((1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
438428, 437ralbid 3253 . . . . . . 7 (𝑥 = (𝐻) → (∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡) ↔ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
439434, 436, 4383anbi123d 1436 . . . . . 6 (𝑥 = (𝐻) → ((∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡)) ↔ (∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))))
440426, 439ralbid 3253 . . . . 5 (𝑥 = (𝐻) → (∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡)) ↔ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))))
441423, 440anbi12d 632 . . . 4 (𝑥 = (𝐻) → ((𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡))) ↔ ((𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))))
442441spcegv 3549 . . 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 1938 1 (𝜑 → ∃𝑥(𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  w3a 1087   = wceq 1541  wex 1781  wnf 1785  wcel 2106  wnfc 2885  wne 2941  wral 3062  wrex 3071  {crab 3404  Vcvv 3442  cdif 3899  cin 3901  wss 3902  c0 4274   cuni 4857   class class class wbr 5097  cmpt 5180  dom cdm 5625  ran crn 5626  ccom 5629  Fun wfun 6478   Fn wfn 6479  wf 6480  cfv 6484  (class class class)co 7342  Fincfn 8809  cr 10976  0cc0 10977  1c1 10978   + caddc 10980   · cmul 10982   < clt 11115  cle 11116  cmin 11311   / cdiv 11738  cn 12079  3c3 12135  +crp 12836  (,)cioo 13185  ...cfz 13345  topGenctg 17246  Clsdccld 22273   Cn ccn 22481  Compccmp 22643
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5234  ax-sep 5248  ax-nul 5255  ax-pow 5313  ax-pr 5377  ax-un 7655  ax-inf2 9503  ax-cnex 11033  ax-resscn 11034  ax-1cn 11035  ax-icn 11036  ax-addcl 11037  ax-addrcl 11038  ax-mulcl 11039  ax-mulrcl 11040  ax-mulcom 11041  ax-addass 11042  ax-mulass 11043  ax-distr 11044  ax-i2m1 11045  ax-1ne0 11046  ax-1rid 11047  ax-rnegex 11048  ax-rrecex 11049  ax-cnre 11050  ax-pre-lttri 11051  ax-pre-lttrn 11052  ax-pre-ltadd 11053  ax-pre-mulgt0 11054  ax-pre-sup 11055  ax-mulf 11057
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3444  df-sbc 3732  df-csb 3848  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3921  df-nul 4275  df-if 4479  df-pw 4554  df-sn 4579  df-pr 4581  df-tp 4583  df-op 4585  df-uni 4858  df-int 4900  df-iun 4948  df-iin 4949  df-br 5098  df-opab 5160  df-mpt 5181  df-tr 5215  df-id 5523  df-eprel 5529  df-po 5537  df-so 5538  df-fr 5580  df-se 5581  df-we 5582  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6243  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6436  df-fun 6486  df-fn 6487  df-f 6488  df-f1 6489  df-fo 6490  df-f1o 6491  df-fv 6492  df-isom 6493  df-riota 7298  df-ov 7345  df-oprab 7346  df-mpo 7347  df-of 7600  df-om 7786  df-1st 7904  df-2nd 7905  df-supp 8053  df-frecs 8172  df-wrecs 8203  df-recs 8277  df-rdg 8316  df-1o 8372  df-2o 8373  df-er 8574  df-map 8693  df-pm 8694  df-ixp 8762  df-en 8810  df-dom 8811  df-sdom 8812  df-fin 8813  df-fsupp 9232  df-fi 9273  df-sup 9304  df-inf 9305  df-oi 9372  df-card 9801  df-pnf 11117  df-mnf 11118  df-xr 11119  df-ltxr 11120  df-le 11121  df-sub 11313  df-neg 11314  df-div 11739  df-nn 12080  df-2 12142  df-3 12143  df-4 12144  df-5 12145  df-6 12146  df-7 12147  df-8 12148  df-9 12149  df-n0 12340  df-z 12426  df-dec 12544  df-uz 12689  df-q 12795  df-rp 12837  df-xneg 12954  df-xadd 12955  df-xmul 12956  df-ioo 13189  df-ioc 13190  df-ico 13191  df-icc 13192  df-fz 13346  df-fzo 13489  df-fl 13618  df-seq 13828  df-exp 13889  df-hash 14151  df-cj 14910  df-re 14911  df-im 14912  df-sqrt 15046  df-abs 15047  df-clim 15297  df-rlim 15298  df-sum 15498  df-struct 16946  df-sets 16963  df-slot 16981  df-ndx 16993  df-base 17011  df-ress 17040  df-plusg 17073  df-mulr 17074  df-starv 17075  df-sca 17076  df-vsca 17077  df-ip 17078  df-tset 17079  df-ple 17080  df-ds 17082  df-unif 17083  df-hom 17084  df-cco 17085  df-rest 17231  df-topn 17232  df-0g 17250  df-gsum 17251  df-topgen 17252  df-pt 17253  df-prds 17256  df-xrs 17311  df-qtop 17316  df-imas 17317  df-xps 17319  df-mre 17393  df-mrc 17394  df-acs 17396  df-mgm 18424  df-sgrp 18473  df-mnd 18484  df-submnd 18529  df-mulg 18798  df-cntz 19020  df-cmn 19484  df-psmet 20695  df-xmet 20696  df-met 20697  df-bl 20698  df-mopn 20699  df-cnfld 20704  df-top 22149  df-topon 22166  df-topsp 22188  df-bases 22202  df-cld 22276  df-cn 22484  df-cnp 22485  df-cmp 22644  df-tx 22819  df-hmeo 23012  df-xms 23579  df-ms 23580  df-tms 23581
This theorem is referenced by:  stoweidlem60  43987
  Copyright terms: Public domain W3C validator