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 46074
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 3457 . . . . . . . . . 10 𝑦{𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)}
31, 2nfcxfr 2903 . . . . . . . . 9 𝑦𝑌
4 nfcv 2905 . . . . . . . . 9 𝑧𝑌
5 nfv 1914 . . . . . . . . 9 𝑧(∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))
6 nfv 1914 . . . . . . . . 9 𝑦(∀𝑡 ∈ (𝐷𝑗)(𝑧𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑧𝑡))
7 fveq1 6905 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝑦𝑡) = (𝑧𝑡))
87breq1d 5153 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝑦𝑡) < (𝐸 / 𝑁) ↔ (𝑧𝑡) < (𝐸 / 𝑁)))
98ralbidv 3178 . . . . . . . . . 10 (𝑦 = 𝑧 → (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷𝑗)(𝑧𝑡) < (𝐸 / 𝑁)))
107breq2d 5155 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ (1 − (𝐸 / 𝑁)) < (𝑧𝑡)))
1110ralbidv 3178 . . . . . . . . . 10 (𝑦 = 𝑧 → (∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑧𝑡)))
129, 11anbi12d 632 . . . . . . . . 9 (𝑦 = 𝑧 → ((∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡)) ↔ (∀𝑡 ∈ (𝐷𝑗)(𝑧𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑧𝑡))))
133, 4, 5, 6, 12cbvrabw 3473 . . . . . . . 8 {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} = {𝑧𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑧𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑧𝑡))}
14 ovexd 7466 . . . . . . . . . 10 (𝜑 → (𝐽 Cn 𝐾) ∈ V)
15 stoweidlem59.11 . . . . . . . . . . 11 (𝜑𝐴𝐶)
16 stoweidlem59.5 . . . . . . . . . . 11 𝐶 = (𝐽 Cn 𝐾)
1715, 16sseqtrdi 4024 . . . . . . . . . 10 (𝜑𝐴 ⊆ (𝐽 Cn 𝐾))
1814, 17ssexd 5324 . . . . . . . . 9 (𝜑𝐴 ∈ V)
191, 18rabexd 5340 . . . . . . . 8 (𝜑𝑌 ∈ V)
2013, 19rabexd 5340 . . . . . . 7 (𝜑 → {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ∈ V)
2120ralrimivw 3150 . . . . . 6 (𝜑 → ∀𝑗 ∈ (0...𝑁){𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ∈ V)
22 stoweidlem59.9 . . . . . . 7 𝐻 = (𝑗 ∈ (0...𝑁) ↦ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
2322fnmpt 6708 . . . . . 6 (∀𝑗 ∈ (0...𝑁){𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ∈ V → 𝐻 Fn (0...𝑁))
2421, 23syl 17 . . . . 5 (𝜑𝐻 Fn (0...𝑁))
25 fzfi 14013 . . . . 5 (0...𝑁) ∈ Fin
26 fnfi 9218 . . . . 5 ((𝐻 Fn (0...𝑁) ∧ (0...𝑁) ∈ Fin) → 𝐻 ∈ Fin)
2724, 25, 26sylancl 586 . . . 4 (𝜑𝐻 ∈ Fin)
28 rnfi 9380 . . . 4 (𝐻 ∈ Fin → ran 𝐻 ∈ Fin)
2927, 28syl 17 . . 3 (𝜑 → ran 𝐻 ∈ Fin)
30 fnchoice 45034 . . 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 2837 . . . . . 6 𝐻 ∈ V
3635rnex 7932 . . . . 5 ran 𝐻 ∈ V
37 fnex 7237 . . . . 5 (( Fn ran 𝐻 ∧ ran 𝐻 ∈ V) → ∈ V)
3832, 36, 37sylancl 586 . . . 4 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ∈ V)
39 coexg 7951 . . . 4 (( ∈ V ∧ 𝐻 ∈ V) → (𝐻) ∈ V)
4038, 35, 39sylancl 586 . . 3 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → (𝐻) ∈ V)
41 dffn3 6748 . . . . . . 7 ( Fn ran 𝐻:ran 𝐻⟶ran )
4232, 41sylib 218 . . . . . 6 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → :ran 𝐻⟶ran )
43 nfv 1914 . . . . . . . . . 10 𝑤𝜑
44 nfv 1914 . . . . . . . . . . 11 𝑤 Fn ran 𝐻
45 nfra1 3284 . . . . . . . . . . 11 𝑤𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)
4644, 45nfan 1899 . . . . . . . . . 10 𝑤( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))
4743, 46nfan 1899 . . . . . . . . 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 1914 . . . . . . . . . . . . . . . . 17 𝑎(𝐻𝑗) = 𝑤
52 nfmpt1 5250 . . . . . . . . . . . . . . . . . . . 20 𝑗(𝑗 ∈ (0...𝑁) ↦ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
5322, 52nfcxfr 2903 . . . . . . . . . . . . . . . . . . 19 𝑗𝐻
54 nfcv 2905 . . . . . . . . . . . . . . . . . . 19 𝑗𝑎
5553, 54nffv 6916 . . . . . . . . . . . . . . . . . 18 𝑗(𝐻𝑎)
56 nfcv 2905 . . . . . . . . . . . . . . . . . 18 𝑗𝑤
5755, 56nfeq 2919 . . . . . . . . . . . . . . . . 17 𝑗(𝐻𝑎) = 𝑤
58 fveq2 6906 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑎 → (𝐻𝑗) = (𝐻𝑎))
5958eqeq1d 2739 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑎 → ((𝐻𝑗) = 𝑤 ↔ (𝐻𝑎) = 𝑤))
6051, 57, 59cbvrexw 3307 . . . . . . . . . . . . . . . 16 (∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤 ↔ ∃𝑎 ∈ (0...𝑁)(𝐻𝑎) = 𝑤)
6150, 60bitr4di 289 . . . . . . . . . . . . . . 15 (𝐻 Fn (0...𝑁) → (𝑤 ∈ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤))
6224, 61syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑤 ∈ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤))
6362biimpa 476 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ran 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤)
64 simp3 1139 . . . . . . . . . . . . . . . . 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 2905 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡(0...𝑁)
71 nfrab1 3457 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡{𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}
7270, 71nfmpt 5249 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
7369, 72nfcxfr 2903 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡𝐷
74 nfcv 2905 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡𝑗
7573, 74nffv 6916 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝐷𝑗)
76 nfcv 2905 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡𝑇
77 stoweidlem59.7 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
78 nfrab1 3457 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑡{𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)}
7970, 78nfmpt 5249 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
8077, 79nfcxfr 2903 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡𝐵
8180, 74nffv 6916 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡(𝐵𝑗)
8276, 81nfdif 4129 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝑇 ∖ (𝐵𝑗))
83 stoweidlem59.2 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡𝜑
84 nfv 1914 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡 𝑗 ∈ (0...𝑁)
8583, 84nfan 1899 . . . . . . . . . . . . . . . . . . . . . . 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 1178 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
93 stoweidlem59.13 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
94933adant1r 1178 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
95 stoweidlem59.14 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ ℝ) → (𝑡𝑇𝑦) ∈ 𝐴)
9695adantlr 715 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ ℝ) → (𝑡𝑇𝑦) ∈ 𝐴)
97 stoweidlem59.15 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟𝑇𝑡𝑇𝑟𝑡)) → ∃𝑞𝐴 (𝑞𝑟) ≠ (𝑞𝑡))
9897adantlr 715 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑟𝑇𝑡𝑇𝑟𝑡)) → ∃𝑞𝐴 (𝑞𝑟) ≠ (𝑞𝑡))
9988uniexd 7762 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 𝐽 ∈ V)
10087, 99eqeltrid 2845 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑇 ∈ V)
101100adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇 ∈ V)
102 rabexg 5337 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2737 . . . . . . . . . . . . . . . . . . . . . . . . 25 {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} = {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)}
108 elfzelz 13564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
109108zred 12722 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
110 3re 12346 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3 ∈ ℝ
111 3ne0 12372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3 ≠ 0
112110, 111rereccli 12032 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (1 / 3) ∈ ℝ
113 readdcl 11238 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ) → (𝑗 + (1 / 3)) ∈ ℝ)
114109, 112, 113sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑁) → (𝑗 + (1 / 3)) ∈ ℝ)
115114adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑗 + (1 / 3)) ∈ ℝ)
116 stoweidlem59.17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐸 ∈ ℝ+)
117116rpred 13077 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐸 ∈ ℝ)
118117adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → 𝐸 ∈ ℝ)
119115, 118remulcld 11291 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑗 + (1 / 3)) · 𝐸) ∈ ℝ)
120 stoweidlem59.16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐹𝐶)
121120, 16eleqtrdi 2851 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐹 ∈ (𝐽 Cn 𝐾))
122121adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → 𝐹 ∈ (𝐽 Cn 𝐾))
123106, 86, 87, 107, 119, 122rfcnpre3 45038 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ (Clsd‘𝐽))
124105, 123eqeltrd 2841 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐵𝑗) ∈ (Clsd‘𝐽))
125 rabexg 5337 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2737 . . . . . . . . . . . . . . . . . . . . . . . . 25 {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}
130 resubcl 11573 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ) → (𝑗 − (1 / 3)) ∈ ℝ)
131109, 112, 130sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑁) → (𝑗 − (1 / 3)) ∈ ℝ)
132131adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑗 − (1 / 3)) ∈ ℝ)
133132, 118remulcld 11291 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ)
134106, 86, 87, 129, 133, 122rfcnpre4 45039 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ (Clsd‘𝐽))
135128, 134eqeltrd 2841 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐷𝑗) ∈ (Clsd‘𝐽))
136133adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ)
137119adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ((𝑗 + (1 / 3)) · 𝐸) ∈ ℝ)
13886, 87, 16, 120fcnre 45030 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝐹:𝑇⟶ℝ)
139138ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → 𝐹:𝑇⟶ℝ)
140 ssrab2 4080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ⊆ 𝑇
141105, 140eqsstrdi 4028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐵𝑗) ⊆ 𝑇)
142141sselda 3983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 0 < 3
148110, 147recgt0ii 12174 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 0 < (1 / 3)
149112, 148elrpii 13037 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (1 / 3) ∈ ℝ+
150 ltsubrp 13071 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ+) → (𝑗 − (1 / 3)) < 𝑗)
151149, 150mpan2 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) < 𝑗)
152 ltaddrp 13072 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ+) → 𝑗 < (𝑗 + (1 / 3)))
153149, 152mpan2 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ → 𝑗 < (𝑗 + (1 / 3)))
154144, 145, 146, 151, 153lttrd 11422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
155109, 154syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 ∈ (0...𝑁) → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
156155adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
157116rpregt0d 13083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
158157adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
159 ltmul1 12117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑗 − (1 / 3)) ∈ ℝ ∧ (𝑗 + (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑗 − (1 / 3)) < (𝑗 + (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸)))
160132, 115, 158, 159syl3anc 1373 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑡 ∈ (𝐵𝑗) ↔ 𝑡 ∈ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)}))
164163biimpa 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → 𝑡 ∈ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
165 rabid 3458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑡 ∈ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ↔ (𝑡𝑇 ∧ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)))
166164, 165sylib 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → (𝑡𝑇 ∧ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)))
167166simprd 495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡))
168136, 137, 143, 162, 167ltletrd 11421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) < (𝐹𝑡))
169136, 143ltnled 11408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → (((𝑗 − (1 / 3)) · 𝐸) < (𝐹𝑡) ↔ ¬ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
170168, 169mpbid 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ¬ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))
171170intnand 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ¬ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
172 rabid 3458 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
173171, 172sylnibr 329 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ¬ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
174128adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → (𝐷𝑗) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
175173, 174neleqtrrd 2864 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ¬ 𝑡 ∈ (𝐷𝑗))
176175ex 412 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑡 ∈ (𝐵𝑗) → ¬ 𝑡 ∈ (𝐷𝑗)))
17785, 176ralrimi 3257 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐵𝑗) ¬ 𝑡 ∈ (𝐷𝑗))
178 disj 4450 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐵𝑗) ∩ (𝐷𝑗)) = ∅ ↔ ∀𝑎 ∈ (𝐵𝑗) ¬ 𝑎 ∈ (𝐷𝑗))
179 nfcv 2905 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑎(𝐵𝑗)
18075nfcri 2897 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑡 𝑎 ∈ (𝐷𝑗)
181180nfn 1857 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡 ¬ 𝑎 ∈ (𝐷𝑗)
182 nfv 1914 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑎 ¬ 𝑡 ∈ (𝐷𝑗)
183 eleq1 2829 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑡 → (𝑎 ∈ (𝐷𝑗) ↔ 𝑡 ∈ (𝐷𝑗)))
184183notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = 𝑡 → (¬ 𝑎 ∈ (𝐷𝑗) ↔ ¬ 𝑡 ∈ (𝐷𝑗)))
185179, 81, 181, 182, 184cbvralfw 3304 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑎 ∈ (𝐵𝑗) ¬ 𝑎 ∈ (𝐷𝑗) ↔ ∀𝑡 ∈ (𝐵𝑗) ¬ 𝑡 ∈ (𝐷𝑗))
186178, 185bitri 275 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐵𝑗) ∩ (𝐷𝑗)) = ∅ ↔ ∀𝑡 ∈ (𝐵𝑗) ¬ 𝑡 ∈ (𝐷𝑗))
187177, 186sylibr 234 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝐵𝑗) ∩ (𝐷𝑗)) = ∅)
188 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑇 ∖ (𝐵𝑗)) = (𝑇 ∖ (𝐵𝑗))
189 stoweidlem59.19 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑁 ∈ ℕ)
190189nnrpd 13075 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑁 ∈ ℝ+)
191116, 190rpdivcld 13094 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐸 / 𝑁) ∈ ℝ+)
192191adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐸 / 𝑁) ∈ ℝ+)
193117, 189nndivred 12320 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐸 / 𝑁) ∈ ℝ)
194112a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (1 / 3) ∈ ℝ)
195189nnge1d 12314 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → 1 ≤ 𝑁)
196 1re 11261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 1 ∈ ℝ
197 0lt1 11785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 0 < 1
198196, 197pm3.2i 470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (1 ∈ ℝ ∧ 0 < 1)
199198a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (1 ∈ ℝ ∧ 0 < 1))
200189nnred 12281 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑁 ∈ ℝ)
201189nngt0d 12315 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → 0 < 𝑁)
202 lediv2 12158 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((1 ∈ ℝ ∧ 0 < 1) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (1 ≤ 𝑁 ↔ (𝐸 / 𝑁) ≤ (𝐸 / 1)))
203199, 200, 201, 157, 202syl121anc 1377 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (1 ≤ 𝑁 ↔ (𝐸 / 𝑁) ≤ (𝐸 / 1)))
204195, 203mpbid 232 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐸 / 𝑁) ≤ (𝐸 / 1))
205116rpcnd 13079 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐸 ∈ ℂ)
206205div1d 12035 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐸 / 1) = 𝐸)
207204, 206breqtrd 5169 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐸 / 𝑁) ≤ 𝐸)
208 stoweidlem59.18 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐸 < (1 / 3))
209193, 117, 194, 207, 208lelttrd 11419 . . . . . . . . . . . . . . . . . . . . . . . 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 46073 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (0...𝑁)) → ∃𝑥𝐴 (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))
212 df-rex 3071 . . . . . . . . . . . . . . . . . . . . . 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 1222 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → ∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1))
216 fveq1 6905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 = 𝑥 → (𝑦𝑡) = (𝑥𝑡))
217216breq2d 5155 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = 𝑥 → (0 ≤ (𝑦𝑡) ↔ 0 ≤ (𝑥𝑡)))
218216breq1d 5153 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = 𝑥 → ((𝑦𝑡) ≤ 1 ↔ (𝑥𝑡) ≤ 1))
219217, 218anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = 𝑥 → ((0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1) ↔ (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1)))
220219ralbidv 3178 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑥 → (∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1)))
221220, 1elrab2 3695 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥𝑌 ↔ (𝑥𝐴 ∧ ∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1)))
222214, 215, 221sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → 𝑥𝑌)
223 simprr2 1223 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁))
224 simprr3 1224 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))
225223, 224jca 511 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → (∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))
226 nfcv 2905 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦𝑥
227 nfv 1914 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦(∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))
228216breq1d 5153 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = 𝑥 → ((𝑦𝑡) < (𝐸 / 𝑁) ↔ (𝑥𝑡) < (𝐸 / 𝑁)))
229228ralbidv 3178 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑥 → (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁)))
230216breq2d 5155 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = 𝑥 → ((1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ (1 − (𝐸 / 𝑁)) < (𝑥𝑡)))
231230ralbidv 3178 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑥 → (∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))
232229, 231anbi12d 632 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑥 → ((∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡)) ↔ (∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))))
233226, 3, 227, 232elrabf 3688 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ↔ (𝑥𝑌 ∧ (∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))))
234222, 225, 233sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → 𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
235234ex 412 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))) → 𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}))
236235eximdv 1917 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0...𝑁)) → (∃𝑥(𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))) → ∃𝑥 𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}))
237213, 236mpd 15 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑁)) → ∃𝑥 𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
238 ne0i 4341 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} → {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ≠ ∅)
239238exlimiv 1930 . . . . . . . . . . . . . . . . . . . 20 (∃𝑥 𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} → {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ≠ ∅)
240237, 239syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ≠ ∅)
24168, 240eqnetrd 3008 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐻𝑗) ≠ ∅)
2422413adant3 1133 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑁) ∧ (𝐻𝑗) = 𝑤) → (𝐻𝑗) ≠ ∅)
24364, 242eqnetrrd 3009 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑁) ∧ (𝐻𝑗) = 𝑤) → 𝑤 ≠ ∅)
2442433exp 1120 . . . . . . . . . . . . . . 15 (𝜑 → (𝑗 ∈ (0...𝑁) → ((𝐻𝑗) = 𝑤𝑤 ≠ ∅)))
245244rexlimdv 3153 . . . . . . . . . . . . . 14 (𝜑 → (∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤𝑤 ≠ ∅))
246245adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ran 𝐻) → (∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤𝑤 ≠ ∅))
24763, 246mpd 15 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ran 𝐻) → 𝑤 ≠ ∅)
248247adantlr 715 . . . . . . . . . . 11 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → 𝑤 ≠ ∅)
249 rsp 3247 . . . . . . . . . . 11 (∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤) → (𝑤 ∈ ran 𝐻 → (𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)))
25048, 49, 248, 249syl3c 66 . . . . . . . . . 10 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → (𝑤) ∈ 𝑤)
251250ex 412 . . . . . . . . 9 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → (𝑤 ∈ ran 𝐻 → (𝑤) ∈ 𝑤))
25247, 251ralrimi 3257 . . . . . . . 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 1914 . . . . . . . . . 10 𝑦𝜑
256 nfcv 2905 . . . . . . . . . . . 12 𝑦
257 nfcv 2905 . . . . . . . . . . . . . . 15 𝑦(0...𝑁)
258 nfrab1 3457 . . . . . . . . . . . . . . 15 𝑦{𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}
259257, 258nfmpt 5249 . . . . . . . . . . . . . 14 𝑦(𝑗 ∈ (0...𝑁) ↦ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
26022, 259nfcxfr 2903 . . . . . . . . . . . . 13 𝑦𝐻
261260nfrn 5963 . . . . . . . . . . . 12 𝑦ran 𝐻
262256, 261nffn 6667 . . . . . . . . . . 11 𝑦 Fn ran 𝐻
263 nfv 1914 . . . . . . . . . . . 12 𝑦(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)
264261, 263nfralw 3311 . . . . . . . . . . 11 𝑦𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)
265262, 264nfan 1899 . . . . . . . . . 10 𝑦( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))
266255, 265nfan 1899 . . . . . . . . 9 𝑦(𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)))
267261nfuni 4914 . . . . . . . . 9 𝑦 ran 𝐻
268 fnunirn 7274 . . . . . . . . . . . . . . 15 (𝐻 Fn (0...𝑁) → (𝑦 ran 𝐻 ↔ ∃𝑧 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑧)))
269 nfcv 2905 . . . . . . . . . . . . . . . . . 18 𝑗𝑧
27053, 269nffv 6916 . . . . . . . . . . . . . . . . 17 𝑗(𝐻𝑧)
271270nfcri 2897 . . . . . . . . . . . . . . . 16 𝑗 𝑦 ∈ (𝐻𝑧)
272 nfv 1914 . . . . . . . . . . . . . . . 16 𝑧 𝑦 ∈ (𝐻𝑗)
273 fveq2 6906 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑗 → (𝐻𝑧) = (𝐻𝑗))
274273eleq2d 2827 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑗 → (𝑦 ∈ (𝐻𝑧) ↔ 𝑦 ∈ (𝐻𝑗)))
275271, 272, 274cbvrexw 3307 . . . . . . . . . . . . . . 15 (∃𝑧 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑧) ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑗))
276268, 275bitrdi 287 . . . . . . . . . . . . . 14 (𝐻 Fn (0...𝑁) → (𝑦 ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑗)))
27724, 276syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑦 ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑗)))
278277biimpa 476 . . . . . . . . . . . 12 ((𝜑𝑦 ran 𝐻) → ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑗))
279 nfv 1914 . . . . . . . . . . . . . 14 𝑗𝜑
28053nfrn 5963 . . . . . . . . . . . . . . . 16 𝑗ran 𝐻
281280nfuni 4914 . . . . . . . . . . . . . . 15 𝑗 ran 𝐻
282281nfcri 2897 . . . . . . . . . . . . . 14 𝑗 𝑦 ran 𝐻
283279, 282nfan 1899 . . . . . . . . . . . . 13 𝑗(𝜑𝑦 ran 𝐻)
284 nfv 1914 . . . . . . . . . . . . 13 𝑗 𝑦𝑌
285 simp1l 1198 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝜑)
286 simp2 1138 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑗 ∈ (0...𝑁))
287 simp3 1139 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑦 ∈ (𝐻𝑗))
28868eleq2d 2827 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑦 ∈ (𝐻𝑗) ↔ 𝑦 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}))
289288biimpa 476 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑦 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
290 rabid 3458 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ↔ (𝑦𝑌 ∧ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))))
291289, 290sylib 218 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → (𝑦𝑌 ∧ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))))
292291simpld 494 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑦𝑌)
293285, 286, 287, 292syl21anc 838 . . . . . . . . . . . . . 14 (((𝜑𝑦 ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑦𝑌)
2942933exp 1120 . . . . . . . . . . . . 13 ((𝜑𝑦 ran 𝐻) → (𝑗 ∈ (0...𝑁) → (𝑦 ∈ (𝐻𝑗) → 𝑦𝑌)))
295283, 284, 294rexlimd 3266 . . . . . . . . . . . 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 3988 . . . . . . . 8 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ran 𝐻𝑌)
300 ssrab2 4080 . . . . . . . . 9 {𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)} ⊆ 𝐴
3011, 300eqsstri 4030 . . . . . . . 8 𝑌𝐴
302299, 301sstrdi 3996 . . . . . . 7 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ran 𝐻𝐴)
303254, 302sstrd 3994 . . . . . 6 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ran 𝐴)
30442, 303fssd 6753 . . . . 5 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → :ran 𝐻𝐴)
305 dffn3 6748 . . . . . . 7 (𝐻 Fn (0...𝑁) ↔ 𝐻:(0...𝑁)⟶ran 𝐻)
30624, 305sylib 218 . . . . . 6 (𝜑𝐻:(0...𝑁)⟶ran 𝐻)
307306adantr 480 . . . . 5 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → 𝐻:(0...𝑁)⟶ran 𝐻)
308 fco 6760 . . . . 5 ((:ran 𝐻𝐴𝐻:(0...𝑁)⟶ran 𝐻) → (𝐻):(0...𝑁)⟶𝐴)
309304, 307, 308syl2anc 584 . . . 4 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → (𝐻):(0...𝑁)⟶𝐴)
310 nfcv 2905 . . . . . . . 8 𝑗
311310, 280nffn 6667 . . . . . . 7 𝑗 Fn ran 𝐻
312 nfv 1914 . . . . . . . 8 𝑗(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)
313280, 312nfralw 3311 . . . . . . 7 𝑗𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)
314311, 313nfan 1899 . . . . . 6 𝑗( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))
315279, 314nfan 1899 . . . . 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 6668 . . . . . . . . . . . . . . . 16 (𝐻 Fn (0...𝑁) → Fun 𝐻)
32324, 322syl 17 . . . . . . . . . . . . . . 15 (𝜑 → Fun 𝐻)
324323ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → Fun 𝐻)
32524fndmd 6673 . . . . . . . . . . . . . . . . 17 (𝜑 → dom 𝐻 = (0...𝑁))
326325adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑁)) → dom 𝐻 = (0...𝑁))
32765, 326eleqtrrd 2844 . . . . . . . . . . . . . . 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 3003 . . . . . . . . . . . . . 14 (𝑤 = (𝐻𝑗) → (𝑤 ≠ ∅ ↔ (𝐻𝑗) ≠ ∅))
334 fveq2 6906 . . . . . . . . . . . . . . 15 (𝑤 = (𝐻𝑗) → (𝑤) = (‘(𝐻𝑗)))
335 id 22 . . . . . . . . . . . . . . 15 (𝑤 = (𝐻𝑗) → 𝑤 = (𝐻𝑗))
336334, 335eleq12d 2835 . . . . . . . . . . . . . 14 (𝑤 = (𝐻𝑗) → ((𝑤) ∈ 𝑤 ↔ (‘(𝐻𝑗)) ∈ (𝐻𝑗)))
337333, 336imbi12d 344 . . . . . . . . . . . . 13 (𝑤 = (𝐻𝑗) → ((𝑤 ≠ ∅ → (𝑤) ∈ 𝑤) ↔ ((𝐻𝑗) ≠ ∅ → (‘(𝐻𝑗)) ∈ (𝐻𝑗))))
338337rspccva 3621 . . . . . . . . . . . 12 ((∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤) ∧ (𝐻𝑗) ∈ ran 𝐻) → ((𝐻𝑗) ≠ ∅ → (‘(𝐻𝑗)) ∈ (𝐻𝑗)))
339331, 332, 338sylc 65 . . . . . . . . . . 11 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (‘(𝐻𝑗)) ∈ (𝐻𝑗))
340320, 339eqeltrd 2841 . . . . . . . . . 10 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝐻)‘𝑗) ∈ (𝐻𝑗))
341256, 260nfco 5876 . . . . . . . . . . . . 13 𝑦(𝐻)
342 nfcv 2905 . . . . . . . . . . . . 13 𝑦𝑗
343341, 342nffv 6916 . . . . . . . . . . . 12 𝑦((𝐻)‘𝑗)
344 nfv 1914 . . . . . . . . . . . . . 14 𝑦(𝜑𝑗 ∈ (0...𝑁))
345260, 342nffv 6916 . . . . . . . . . . . . . . 15 𝑦(𝐻𝑗)
346343, 345nfel 2920 . . . . . . . . . . . . . 14 𝑦((𝐻)‘𝑗) ∈ (𝐻𝑗)
347344, 346nfan 1899 . . . . . . . . . . . . 13 𝑦((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗))
348343, 3nfel 2920 . . . . . . . . . . . . 13 𝑦((𝐻)‘𝑗) ∈ 𝑌
349347, 348nfim 1896 . . . . . . . . . . . 12 𝑦(((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ((𝐻)‘𝑗) ∈ 𝑌)
350 eleq1 2829 . . . . . . . . . . . . . 14 (𝑦 = ((𝐻)‘𝑗) → (𝑦 ∈ (𝐻𝑗) ↔ ((𝐻)‘𝑗) ∈ (𝐻𝑗)))
351350anbi2d 630 . . . . . . . . . . . . 13 (𝑦 = ((𝐻)‘𝑗) → (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) ↔ ((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗))))
352 eleq1 2829 . . . . . . . . . . . . 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 2833 . . . . . . . . . 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 6916 . . . . . . . . . . . . . 14 𝑦(((𝐻)‘𝑗)‘𝑡)
364360, 361, 363nfbr 5190 . . . . . . . . . . . . 13 𝑦0 ≤ (((𝐻)‘𝑗)‘𝑡)
365 nfcv 2905 . . . . . . . . . . . . . 14 𝑦1
366363, 361, 365nfbr 5190 . . . . . . . . . . . . 13 𝑦(((𝐻)‘𝑗)‘𝑡) ≤ 1
367364, 366nfan 1899 . . . . . . . . . . . 12 𝑦(0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)
368359, 367nfralw 3311 . . . . . . . . . . 11 𝑦𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)
369 nfcv 2905 . . . . . . . . . . . . 13 𝑡𝑦
370 nfcv 2905 . . . . . . . . . . . . . . 15 𝑡
371 nfra1 3284 . . . . . . . . . . . . . . . . . . 19 𝑡𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁)
372 nfra1 3284 . . . . . . . . . . . . . . . . . . 19 𝑡𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡)
373371, 372nfan 1899 . . . . . . . . . . . . . . . . . 18 𝑡(∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))
374 nfra1 3284 . . . . . . . . . . . . . . . . . . . 20 𝑡𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)
375 nfcv 2905 . . . . . . . . . . . . . . . . . . . 20 𝑡𝐴
376374, 375nfrabw 3475 . . . . . . . . . . . . . . . . . . 19 𝑡{𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)}
3771, 376nfcxfr 2903 . . . . . . . . . . . . . . . . . 18 𝑡𝑌
378373, 377nfrabw 3475 . . . . . . . . . . . . . . . . 17 𝑡{𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}
37970, 378nfmpt 5249 . . . . . . . . . . . . . . . 16 𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
38022, 379nfcxfr 2903 . . . . . . . . . . . . . . 15 𝑡𝐻
381370, 380nfco 5876 . . . . . . . . . . . . . 14 𝑡(𝐻)
382381, 74nffv 6916 . . . . . . . . . . . . 13 𝑡((𝐻)‘𝑗)
383369, 382nfeq 2919 . . . . . . . . . . . 12 𝑡 𝑦 = ((𝐻)‘𝑗)
384 fveq1 6905 . . . . . . . . . . . . . 14 (𝑦 = ((𝐻)‘𝑗) → (𝑦𝑡) = (((𝐻)‘𝑗)‘𝑡))
385384breq2d 5155 . . . . . . . . . . . . 13 (𝑦 = ((𝐻)‘𝑗) → (0 ≤ (𝑦𝑡) ↔ 0 ≤ (((𝐻)‘𝑗)‘𝑡)))
386384breq1d 5153 . . . . . . . . . . . . 13 (𝑦 = ((𝐻)‘𝑗) → ((𝑦𝑡) ≤ 1 ↔ (((𝐻)‘𝑗)‘𝑡) ≤ 1))
387385, 386anbi12d 632 . . . . . . . . . . . 12 (𝑦 = ((𝐻)‘𝑗) → ((0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1) ↔ (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
388383, 387ralbid 3273 . . . . . . . . . . 11 (𝑦 = ((𝐻)‘𝑗) → (∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
389343, 358, 368, 388elrabf 3688 . . . . . . . . . 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 2905 . . . . . . . . . . . 12 𝑦(𝐷𝑗)
394 nfcv 2905 . . . . . . . . . . . . 13 𝑦 <
395 nfcv 2905 . . . . . . . . . . . . 13 𝑦(𝐸 / 𝑁)
396363, 394, 395nfbr 5190 . . . . . . . . . . . 12 𝑦(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)
397393, 396nfralw 3311 . . . . . . . . . . 11 𝑦𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)
398347, 397nfim 1896 . . . . . . . . . 10 𝑦(((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))
399384breq1d 5153 . . . . . . . . . . . 12 (𝑦 = ((𝐻)‘𝑗) → ((𝑦𝑡) < (𝐸 / 𝑁) ↔ (((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
400383, 399ralbid 3273 . . . . . . . . . . 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 2905 . . . . . . . . . . . 12 𝑦(𝐵𝑗)
408 nfcv 2905 . . . . . . . . . . . . 13 𝑦(1 − (𝐸 / 𝑁))
409408, 394, 363nfbr 5190 . . . . . . . . . . . 12 𝑦(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)
410407, 409nfralw 3311 . . . . . . . . . . 11 𝑦𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)
411347, 410nfim 1896 . . . . . . . . . 10 𝑦(((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))
412384breq2d 5155 . . . . . . . . . . . 12 (𝑦 = ((𝐻)‘𝑗) → ((1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ (1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
413383, 412ralbid 3273 . . . . . . . . . . 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 1129 . . . . . 6 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
420419ex 412 . . . . 5 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → (𝑗 ∈ (0...𝑁) → (∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))))
421315, 420ralrimi 3257 . . . 4 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
422309, 421jca 511 . . 3 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ((𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))))
423 feq1 6716 . . . . 5 (𝑥 = (𝐻) → (𝑥:(0...𝑁)⟶𝐴 ↔ (𝐻):(0...𝑁)⟶𝐴))
424 nfcv 2905 . . . . . . 7 𝑗𝑥
425310, 53nfco 5876 . . . . . . 7 𝑗(𝐻)
426424, 425nfeq 2919 . . . . . 6 𝑗 𝑥 = (𝐻)
427 nfcv 2905 . . . . . . . . 9 𝑡𝑥
428427, 381nfeq 2919 . . . . . . . 8 𝑡 𝑥 = (𝐻)
429 fveq1 6905 . . . . . . . . . . 11 (𝑥 = (𝐻) → (𝑥𝑗) = ((𝐻)‘𝑗))
430429fveq1d 6908 . . . . . . . . . 10 (𝑥 = (𝐻) → ((𝑥𝑗)‘𝑡) = (((𝐻)‘𝑗)‘𝑡))
431430breq2d 5155 . . . . . . . . 9 (𝑥 = (𝐻) → (0 ≤ ((𝑥𝑗)‘𝑡) ↔ 0 ≤ (((𝐻)‘𝑗)‘𝑡)))
432430breq1d 5153 . . . . . . . . 9 (𝑥 = (𝐻) → (((𝑥𝑗)‘𝑡) ≤ 1 ↔ (((𝐻)‘𝑗)‘𝑡) ≤ 1))
433431, 432anbi12d 632 . . . . . . . 8 (𝑥 = (𝐻) → ((0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ↔ (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
434428, 433ralbid 3273 . . . . . . 7 (𝑥 = (𝐻) → (∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
435430breq1d 5153 . . . . . . . 8 (𝑥 = (𝐻) → (((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ (((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
436428, 435ralbid 3273 . . . . . . 7 (𝑥 = (𝐻) → (∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
437430breq2d 5155 . . . . . . . 8 (𝑥 = (𝐻) → ((1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
438428, 437ralbid 3273 . . . . . . 7 (𝑥 = (𝐻) → (∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡) ↔ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
439434, 436, 4383anbi123d 1438 . . . . . 6 (𝑥 = (𝐻) → ((∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡)) ↔ (∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))))
440426, 439ralbid 3273 . . . . 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 1935 1 (𝜑 → ∃𝑥(𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wex 1779  wnf 1783  wcel 2108  wnfc 2890  wne 2940  wral 3061  wrex 3070  {crab 3436  Vcvv 3480  cdif 3948  cin 3950  wss 3951  c0 4333   cuni 4907   class class class wbr 5143  cmpt 5225  dom cdm 5685  ran crn 5686  ccom 5689  Fun wfun 6555   Fn wfn 6556  wf 6557  cfv 6561  (class class class)co 7431  Fincfn 8985  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160   < clt 11295  cle 11296  cmin 11492   / cdiv 11920  cn 12266  3c3 12322  +crp 13034  (,)cioo 13387  ...cfz 13547  topGenctg 17482  Clsdccld 23024   Cn ccn 23232  Compccmp 23394
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-er 8745  df-map 8868  df-pm 8869  df-ixp 8938  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-fi 9451  df-sup 9482  df-inf 9483  df-oi 9550  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-z 12614  df-dec 12734  df-uz 12879  df-q 12991  df-rp 13035  df-xneg 13154  df-xadd 13155  df-xmul 13156  df-ioo 13391  df-ioc 13392  df-ico 13393  df-icc 13394  df-fz 13548  df-fzo 13695  df-fl 13832  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-rlim 15525  df-sum 15723  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-rest 17467  df-topn 17468  df-0g 17486  df-gsum 17487  df-topgen 17488  df-pt 17489  df-prds 17492  df-xrs 17547  df-qtop 17552  df-imas 17553  df-xps 17555  df-mre 17629  df-mrc 17630  df-acs 17632  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-submnd 18797  df-mulg 19086  df-cntz 19335  df-cmn 19800  df-psmet 21356  df-xmet 21357  df-met 21358  df-bl 21359  df-mopn 21360  df-cnfld 21365  df-top 22900  df-topon 22917  df-topsp 22939  df-bases 22953  df-cld 23027  df-cn 23235  df-cnp 23236  df-cmp 23395  df-tx 23570  df-hmeo 23763  df-xms 24330  df-ms 24331  df-tms 24332
This theorem is referenced by:  stoweidlem60  46075
  Copyright terms: Public domain W3C validator