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 40772
Description: This lemma proves that there exists a function 𝑥 as in the proof in [BrosowskiDeutsh] p. 91, after Lemma 2: xj is in the subalgebra, 0 <= xj <= 1, xj < ε / n on Aj (meaning A in the paper), xj > 1 - \epslon / n on Bj. Here 𝐷 is used to represent A in the paper (because A is used for the subalgebra of functions), 𝐸 is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem59.1 𝑡𝐹
stoweidlem59.2 𝑡𝜑
stoweidlem59.3 𝐾 = (topGen‘ran (,))
stoweidlem59.4 𝑇 = 𝐽
stoweidlem59.5 𝐶 = (𝐽 Cn 𝐾)
stoweidlem59.6 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
stoweidlem59.7 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
stoweidlem59.8 𝑌 = {𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)}
stoweidlem59.9 𝐻 = (𝑗 ∈ (0...𝑁) ↦ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
stoweidlem59.10 (𝜑𝐽 ∈ Comp)
stoweidlem59.11 (𝜑𝐴𝐶)
stoweidlem59.12 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
stoweidlem59.13 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
stoweidlem59.14 ((𝜑𝑦 ∈ ℝ) → (𝑡𝑇𝑦) ∈ 𝐴)
stoweidlem59.15 ((𝜑 ∧ (𝑟𝑇𝑡𝑇𝑟𝑡)) → ∃𝑞𝐴 (𝑞𝑟) ≠ (𝑞𝑡))
stoweidlem59.16 (𝜑𝐹𝐶)
stoweidlem59.17 (𝜑𝐸 ∈ ℝ+)
stoweidlem59.18 (𝜑𝐸 < (1 / 3))
stoweidlem59.19 (𝜑𝑁 ∈ ℕ)
Assertion
Ref Expression
stoweidlem59 (𝜑 → ∃𝑥(𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡))))
Distinct variable groups:   𝑡,𝑗,𝑦   𝑦,𝐵   𝑦,𝐷   𝑗,𝑁,𝑡,𝑦   𝑗,𝑌   𝑓,𝑔,𝑗,𝑞,𝑟,𝑡,𝑁   𝑥,𝑓,𝑔,𝑗,𝑡,𝑁   𝑦,𝑓,𝑞,𝑟,𝐴   𝐴,𝑔,𝑞,𝑟,𝑡   𝐵,𝑓,𝑔,𝑞,𝑟   𝐷,𝑓,𝑔,𝑞,𝑟   𝑓,𝐸,𝑔,𝑟,𝑡   𝑓,𝐽,𝑔,𝑟,𝑡   𝑇,𝑓,𝑔,𝑞,𝑟,𝑡   𝜑,𝑓,𝑔,𝑗,𝑞,𝑟   𝑥,𝑦,𝐴   𝑥,𝐵   𝑥,𝐷   𝑥,𝐸,𝑦   𝑥,𝑇,𝑦   𝜑,𝑦   𝑡,𝐾   𝑥,𝐻   𝑥,𝑌   𝜑,𝑥
Allowed substitution hints:   𝜑(𝑡)   𝐴(𝑗)   𝐵(𝑡,𝑗)   𝐶(𝑥,𝑦,𝑡,𝑓,𝑔,𝑗,𝑟,𝑞)   𝐷(𝑡,𝑗)   𝑇(𝑗)   𝐸(𝑗,𝑞)   𝐹(𝑥,𝑦,𝑡,𝑓,𝑔,𝑗,𝑟,𝑞)   𝐻(𝑦,𝑡,𝑓,𝑔,𝑗,𝑟,𝑞)   𝐽(𝑥,𝑦,𝑗,𝑞)   𝐾(𝑥,𝑦,𝑓,𝑔,𝑗,𝑟,𝑞)   𝑌(𝑦,𝑡,𝑓,𝑔,𝑟,𝑞)

Proof of Theorem stoweidlem59
Dummy variables 𝑎 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 stoweidlem59.8 . . . . . . . . . 10 𝑌 = {𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)}
2 nfrab1 3322 . . . . . . . . . 10 𝑦{𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)}
31, 2nfcxfr 2957 . . . . . . . . 9 𝑦𝑌
4 nfcv 2959 . . . . . . . . 9 𝑧𝑌
5 nfv 2005 . . . . . . . . 9 𝑧(∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))
6 nfv 2005 . . . . . . . . 9 𝑦(∀𝑡 ∈ (𝐷𝑗)(𝑧𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑧𝑡))
7 fveq1 6416 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝑦𝑡) = (𝑧𝑡))
87breq1d 4865 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝑦𝑡) < (𝐸 / 𝑁) ↔ (𝑧𝑡) < (𝐸 / 𝑁)))
98ralbidv 3185 . . . . . . . . . 10 (𝑦 = 𝑧 → (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷𝑗)(𝑧𝑡) < (𝐸 / 𝑁)))
107breq2d 4867 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ (1 − (𝐸 / 𝑁)) < (𝑧𝑡)))
1110ralbidv 3185 . . . . . . . . . 10 (𝑦 = 𝑧 → (∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑧𝑡)))
129, 11anbi12d 618 . . . . . . . . 9 (𝑦 = 𝑧 → ((∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡)) ↔ (∀𝑡 ∈ (𝐷𝑗)(𝑧𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑧𝑡))))
133, 4, 5, 6, 12cbvrab 3399 . . . . . . . 8 {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} = {𝑧𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑧𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑧𝑡))}
14 ovexd 6917 . . . . . . . . . 10 (𝜑 → (𝐽 Cn 𝐾) ∈ V)
15 stoweidlem59.11 . . . . . . . . . . 11 (𝜑𝐴𝐶)
16 stoweidlem59.5 . . . . . . . . . . 11 𝐶 = (𝐽 Cn 𝐾)
1715, 16syl6sseq 3859 . . . . . . . . . 10 (𝜑𝐴 ⊆ (𝐽 Cn 𝐾))
1814, 17ssexd 5013 . . . . . . . . 9 (𝜑𝐴 ∈ V)
191, 18rabexd 5021 . . . . . . . 8 (𝜑𝑌 ∈ V)
2013, 19rabexd 5021 . . . . . . 7 (𝜑 → {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ∈ V)
2120ralrimivw 3166 . . . . . 6 (𝜑 → ∀𝑗 ∈ (0...𝑁){𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ∈ V)
22 stoweidlem59.9 . . . . . . 7 𝐻 = (𝑗 ∈ (0...𝑁) ↦ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
2322fnmpt 6240 . . . . . 6 (∀𝑗 ∈ (0...𝑁){𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ∈ V → 𝐻 Fn (0...𝑁))
2421, 23syl 17 . . . . 5 (𝜑𝐻 Fn (0...𝑁))
25 fzfi 13014 . . . . 5 (0...𝑁) ∈ Fin
26 fnfi 8486 . . . . 5 ((𝐻 Fn (0...𝑁) ∧ (0...𝑁) ∈ Fin) → 𝐻 ∈ Fin)
2724, 25, 26sylancl 576 . . . 4 (𝜑𝐻 ∈ Fin)
28 rnfi 8497 . . . 4 (𝐻 ∈ Fin → ran 𝐻 ∈ Fin)
2927, 28syl 17 . . 3 (𝜑 → ran 𝐻 ∈ Fin)
30 fnchoice 39699 . . 3 (ran 𝐻 ∈ Fin → ∃( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)))
3129, 30syl 17 . 2 (𝜑 → ∃( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)))
32 simprl 778 . . . . 5 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → Fn ran 𝐻)
33 ovex 6915 . . . . . . . 8 (0...𝑁) ∈ V
3433mptex 6720 . . . . . . 7 (𝑗 ∈ (0...𝑁) ↦ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}) ∈ V
3522, 34eqeltri 2892 . . . . . 6 𝐻 ∈ V
3635rnex 7339 . . . . 5 ran 𝐻 ∈ V
37 fnex 6715 . . . . 5 (( Fn ran 𝐻 ∧ ran 𝐻 ∈ V) → ∈ V)
3832, 36, 37sylancl 576 . . . 4 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ∈ V)
39 coexg 7356 . . . 4 (( ∈ V ∧ 𝐻 ∈ V) → (𝐻) ∈ V)
4038, 35, 39sylancl 576 . . 3 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → (𝐻) ∈ V)
41 dffn3 6276 . . . . . . 7 ( Fn ran 𝐻:ran 𝐻⟶ran )
4232, 41sylib 209 . . . . . 6 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → :ran 𝐻⟶ran )
43 nfv 2005 . . . . . . . . . 10 𝑤𝜑
44 nfv 2005 . . . . . . . . . . 11 𝑤 Fn ran 𝐻
45 nfra1 3140 . . . . . . . . . . 11 𝑤𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)
4644, 45nfan 1990 . . . . . . . . . 10 𝑤( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))
4743, 46nfan 1990 . . . . . . . . 9 𝑤(𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)))
48 simplrr 787 . . . . . . . . . . 11 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))
49 simpr 473 . . . . . . . . . . 11 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → 𝑤 ∈ ran 𝐻)
50 fvelrnb 6473 . . . . . . . . . . . . . . . 16 (𝐻 Fn (0...𝑁) → (𝑤 ∈ ran 𝐻 ↔ ∃𝑎 ∈ (0...𝑁)(𝐻𝑎) = 𝑤))
51 nfv 2005 . . . . . . . . . . . . . . . . 17 𝑎(𝐻𝑗) = 𝑤
52 nfmpt1 4952 . . . . . . . . . . . . . . . . . . . 20 𝑗(𝑗 ∈ (0...𝑁) ↦ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
5322, 52nfcxfr 2957 . . . . . . . . . . . . . . . . . . 19 𝑗𝐻
54 nfcv 2959 . . . . . . . . . . . . . . . . . . 19 𝑗𝑎
5553, 54nffv 6427 . . . . . . . . . . . . . . . . . 18 𝑗(𝐻𝑎)
56 nfcv 2959 . . . . . . . . . . . . . . . . . 18 𝑗𝑤
5755, 56nfeq 2971 . . . . . . . . . . . . . . . . 17 𝑗(𝐻𝑎) = 𝑤
58 fveq2 6417 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑎 → (𝐻𝑗) = (𝐻𝑎))
5958eqeq1d 2819 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑎 → ((𝐻𝑗) = 𝑤 ↔ (𝐻𝑎) = 𝑤))
6051, 57, 59cbvrex 3368 . . . . . . . . . . . . . . . 16 (∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤 ↔ ∃𝑎 ∈ (0...𝑁)(𝐻𝑎) = 𝑤)
6150, 60syl6bbr 280 . . . . . . . . . . . . . . 15 (𝐻 Fn (0...𝑁) → (𝑤 ∈ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤))
6224, 61syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑤 ∈ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤))
6362biimpa 464 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ran 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤)
64 simp3 1161 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑁) ∧ (𝐻𝑗) = 𝑤) → (𝐻𝑗) = 𝑤)
65 simpr 473 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
6620adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ∈ V)
6722fvmpt2 6521 . . . . . . . . . . . . . . . . . . . 20 ((𝑗 ∈ (0...𝑁) ∧ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ∈ V) → (𝐻𝑗) = {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
6865, 66, 67syl2anc 575 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐻𝑗) = {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
69 stoweidlem59.6 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
70 nfcv 2959 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡(0...𝑁)
71 nfrab1 3322 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡{𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}
7270, 71nfmpt 4951 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
7369, 72nfcxfr 2957 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡𝐷
74 nfcv 2959 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡𝑗
7573, 74nffv 6427 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝐷𝑗)
76 nfcv 2959 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡𝑇
77 stoweidlem59.7 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
78 nfrab1 3322 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑡{𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)}
7970, 78nfmpt 4951 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
8077, 79nfcxfr 2957 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡𝐵
8180, 74nffv 6427 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡(𝐵𝑗)
8276, 81nfdif 3941 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝑇 ∖ (𝐵𝑗))
83 stoweidlem59.2 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡𝜑
84 nfv 2005 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡 𝑗 ∈ (0...𝑁)
8583, 84nfan 1990 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝜑𝑗 ∈ (0...𝑁))
86 stoweidlem59.3 . . . . . . . . . . . . . . . . . . . . . . 23 𝐾 = (topGen‘ran (,))
87 stoweidlem59.4 . . . . . . . . . . . . . . . . . . . . . . 23 𝑇 = 𝐽
88 stoweidlem59.10 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐽 ∈ Comp)
8988adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → 𝐽 ∈ Comp)
9015adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → 𝐴𝐶)
91 stoweidlem59.12 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
92913adant1r 1216 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) + (𝑔𝑡))) ∈ 𝐴)
93 stoweidlem59.13 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
94933adant1r 1216 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑓𝐴𝑔𝐴) → (𝑡𝑇 ↦ ((𝑓𝑡) · (𝑔𝑡))) ∈ 𝐴)
95 stoweidlem59.14 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑦 ∈ ℝ) → (𝑡𝑇𝑦) ∈ 𝐴)
9695adantlr 697 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ ℝ) → (𝑡𝑇𝑦) ∈ 𝐴)
97 stoweidlem59.15 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑟𝑇𝑡𝑇𝑟𝑡)) → ∃𝑞𝐴 (𝑞𝑟) ≠ (𝑞𝑡))
9897adantlr 697 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑟𝑇𝑡𝑇𝑟𝑡)) → ∃𝑞𝐴 (𝑞𝑟) ≠ (𝑞𝑡))
99 uniexg 7194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐽 ∈ Comp → 𝐽 ∈ V)
10088, 99syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 𝐽 ∈ V)
10187, 100syl5eqel 2900 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑇 ∈ V)
102101adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑇 ∈ V)
103 rabexg 5019 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑇 ∈ V → {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V)
104102, 103syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V)
10577fvmpt2 6521 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗 ∈ (0...𝑁) ∧ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V) → (𝐵𝑗) = {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
10665, 104, 105syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐵𝑗) = {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
107 stoweidlem59.1 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑡𝐹
108 eqid 2817 . . . . . . . . . . . . . . . . . . . . . . . . 25 {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} = {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)}
109 elfzelz 12584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
110109zred 11767 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
111 3re 11392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3 ∈ ℝ
112 3ne0 11425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3 ≠ 0
113111, 112rereccli 11084 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (1 / 3) ∈ ℝ
114 readdcl 10313 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ) → (𝑗 + (1 / 3)) ∈ ℝ)
115110, 113, 114sylancl 576 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑁) → (𝑗 + (1 / 3)) ∈ ℝ)
116115adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑗 + (1 / 3)) ∈ ℝ)
117 stoweidlem59.17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐸 ∈ ℝ+)
118117rpred 12105 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐸 ∈ ℝ)
119118adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → 𝐸 ∈ ℝ)
120116, 119remulcld 10364 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑗 + (1 / 3)) · 𝐸) ∈ ℝ)
121 stoweidlem59.16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐹𝐶)
122121, 16syl6eleq 2906 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐹 ∈ (𝐽 Cn 𝐾))
123122adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → 𝐹 ∈ (𝐽 Cn 𝐾))
124107, 86, 87, 108, 120, 123rfcnpre3 39703 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ (Clsd‘𝐽))
125106, 124eqeltrd 2896 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐵𝑗) ∈ (Clsd‘𝐽))
126 rabexg 5019 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V)
127102, 126syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V)
12869fvmpt2 6521 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑗 ∈ (0...𝑁) ∧ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V) → (𝐷𝑗) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
12965, 127, 128syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐷𝑗) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
130 eqid 2817 . . . . . . . . . . . . . . . . . . . . . . . . 25 {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}
131 resubcl 10639 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ) → (𝑗 − (1 / 3)) ∈ ℝ)
132110, 113, 131sylancl 576 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 ∈ (0...𝑁) → (𝑗 − (1 / 3)) ∈ ℝ)
133132adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑗 − (1 / 3)) ∈ ℝ)
134133, 119remulcld 10364 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ)
135107, 86, 87, 130, 134, 123rfcnpre4 39704 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ (Clsd‘𝐽))
136129, 135eqeltrd 2896 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐷𝑗) ∈ (Clsd‘𝐽))
137134adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ)
138120adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ((𝑗 + (1 / 3)) · 𝐸) ∈ ℝ)
13986, 87, 16, 121fcnre 39695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝜑𝐹:𝑇⟶ℝ)
140139ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → 𝐹:𝑇⟶ℝ)
141 ssrab2 3895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ⊆ 𝑇
142106, 141syl6eqss 3863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐵𝑗) ⊆ 𝑇)
143142sselda 3809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → 𝑡𝑇)
144140, 143ffvelrnd 6591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → (𝐹𝑡) ∈ ℝ)
145113, 131mpan2 674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) ∈ ℝ)
146 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ → 𝑗 ∈ ℝ)
147113, 114mpan2 674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ → (𝑗 + (1 / 3)) ∈ ℝ)
148 3pos 11424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 0 < 3
149111, 148recgt0ii 11223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 0 < (1 / 3)
150113, 149elrpii 12068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (1 / 3) ∈ ℝ+
151 ltsubrp 12099 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ+) → (𝑗 − (1 / 3)) < 𝑗)
152150, 151mpan2 674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) < 𝑗)
153 ltaddrp 12100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ+) → 𝑗 < (𝑗 + (1 / 3)))
154150, 153mpan2 674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 ∈ ℝ → 𝑗 < (𝑗 + (1 / 3)))
155145, 146, 147, 152, 154lttrd 10492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
156110, 155syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑗 ∈ (0...𝑁) → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
157156adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
158117rpregt0d 12111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
159158adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
160 ltmul1 11167 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑗 − (1 / 3)) ∈ ℝ ∧ (𝑗 + (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑗 − (1 / 3)) < (𝑗 + (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸)))
161133, 116, 159, 160syl3anc 1483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) < (𝑗 + (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸)))
162157, 161mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸))
163162adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸))
164106eleq2d 2882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑡 ∈ (𝐵𝑗) ↔ 𝑡 ∈ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)}))
165164biimpa 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → 𝑡 ∈ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
166 rabid 3315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑡 ∈ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ↔ (𝑡𝑇 ∧ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)))
167165, 166sylib 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → (𝑡𝑇 ∧ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)))
168167simprd 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡))
169137, 138, 144, 163, 168ltletrd 10491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) < (𝐹𝑡))
170137, 144ltnled 10478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → (((𝑗 − (1 / 3)) · 𝐸) < (𝐹𝑡) ↔ ¬ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
171169, 170mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ¬ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))
172171intnand 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ¬ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
173 rabid 3315 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ↔ (𝑡𝑇 ∧ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
174172, 173sylnibr 320 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ¬ 𝑡 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
175129adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → (𝐷𝑗) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
176174, 175neleqtrrd 2918 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵𝑗)) → ¬ 𝑡 ∈ (𝐷𝑗))
177176ex 399 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑡 ∈ (𝐵𝑗) → ¬ 𝑡 ∈ (𝐷𝑗)))
17885, 177ralrimi 3156 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐵𝑗) ¬ 𝑡 ∈ (𝐷𝑗))
179 disj 4225 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐵𝑗) ∩ (𝐷𝑗)) = ∅ ↔ ∀𝑎 ∈ (𝐵𝑗) ¬ 𝑎 ∈ (𝐷𝑗))
180 nfcv 2959 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑎(𝐵𝑗)
18175nfcri 2953 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑡 𝑎 ∈ (𝐷𝑗)
182181nfn 1944 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑡 ¬ 𝑎 ∈ (𝐷𝑗)
183 nfv 2005 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑎 ¬ 𝑡 ∈ (𝐷𝑗)
184 eleq1 2884 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = 𝑡 → (𝑎 ∈ (𝐷𝑗) ↔ 𝑡 ∈ (𝐷𝑗)))
185184notbid 309 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = 𝑡 → (¬ 𝑎 ∈ (𝐷𝑗) ↔ ¬ 𝑡 ∈ (𝐷𝑗)))
186180, 81, 182, 183, 185cbvralf 3365 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∀𝑎 ∈ (𝐵𝑗) ¬ 𝑎 ∈ (𝐷𝑗) ↔ ∀𝑡 ∈ (𝐵𝑗) ¬ 𝑡 ∈ (𝐷𝑗))
187179, 186bitri 266 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐵𝑗) ∩ (𝐷𝑗)) = ∅ ↔ ∀𝑡 ∈ (𝐵𝑗) ¬ 𝑡 ∈ (𝐷𝑗))
188178, 187sylibr 225 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝐵𝑗) ∩ (𝐷𝑗)) = ∅)
189 eqid 2817 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑇 ∖ (𝐵𝑗)) = (𝑇 ∖ (𝐵𝑗))
190 stoweidlem59.19 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝑁 ∈ ℕ)
191190nnrpd 12103 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑁 ∈ ℝ+)
192117, 191rpdivcld 12122 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐸 / 𝑁) ∈ ℝ+)
193192adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐸 / 𝑁) ∈ ℝ+)
194118, 190nndivred 11366 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐸 / 𝑁) ∈ ℝ)
195113a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (1 / 3) ∈ ℝ)
196190nnge1d 11360 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → 1 ≤ 𝑁)
197 1re 10334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 1 ∈ ℝ
198 0lt1 10844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 0 < 1
199197, 198pm3.2i 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (1 ∈ ℝ ∧ 0 < 1)
200199a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (1 ∈ ℝ ∧ 0 < 1))
201190nnred 11331 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑁 ∈ ℝ)
202190nngt0d 11361 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → 0 < 𝑁)
203 lediv2 11207 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((1 ∈ ℝ ∧ 0 < 1) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (1 ≤ 𝑁 ↔ (𝐸 / 𝑁) ≤ (𝐸 / 1)))
204200, 201, 202, 158, 203syl121anc 1487 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (1 ≤ 𝑁 ↔ (𝐸 / 𝑁) ≤ (𝐸 / 1)))
205196, 204mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐸 / 𝑁) ≤ (𝐸 / 1))
206117rpcnd 12107 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐸 ∈ ℂ)
207206div1d 11087 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐸 / 1) = 𝐸)
208205, 207breqtrd 4881 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐸 / 𝑁) ≤ 𝐸)
209 stoweidlem59.18 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐸 < (1 / 3))
210194, 118, 195, 208, 209lelttrd 10489 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐸 / 𝑁) < (1 / 3))
211210adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐸 / 𝑁) < (1 / 3))
21275, 82, 85, 86, 87, 16, 89, 90, 92, 94, 96, 98, 125, 136, 188, 189, 193, 211stoweidlem58 40771 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (0...𝑁)) → ∃𝑥𝐴 (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))
213 df-rex 3113 . . . . . . . . . . . . . . . . . . . . . 22 (∃𝑥𝐴 (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)) ↔ ∃𝑥(𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))))
214212, 213sylib 209 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0...𝑁)) → ∃𝑥(𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))))
215 simprl 778 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → 𝑥𝐴)
216 simprr1 1280 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → ∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1))
217 fveq1 6416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 = 𝑥 → (𝑦𝑡) = (𝑥𝑡))
218217breq2d 4867 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = 𝑥 → (0 ≤ (𝑦𝑡) ↔ 0 ≤ (𝑥𝑡)))
219217breq1d 4865 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = 𝑥 → ((𝑦𝑡) ≤ 1 ↔ (𝑥𝑡) ≤ 1))
220218, 219anbi12d 618 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = 𝑥 → ((0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1) ↔ (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1)))
221220ralbidv 3185 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑥 → (∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1)))
222221, 1elrab2 3573 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥𝑌 ↔ (𝑥𝐴 ∧ ∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1)))
223215, 216, 222sylanbrc 574 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → 𝑥𝑌)
224 simprr2 1282 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁))
225 simprr3 1284 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))
226224, 225jca 503 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → (∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))
227 nfcv 2959 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦𝑥
228 nfv 2005 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦(∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))
229217breq1d 4865 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = 𝑥 → ((𝑦𝑡) < (𝐸 / 𝑁) ↔ (𝑥𝑡) < (𝐸 / 𝑁)))
230229ralbidv 3185 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑥 → (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁)))
231217breq2d 4867 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = 𝑥 → ((1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ (1 − (𝐸 / 𝑁)) < (𝑥𝑡)))
232231ralbidv 3185 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑥 → (∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))
233230, 232anbi12d 618 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑥 → ((∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡)) ↔ (∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))))
234227, 3, 228, 233elrabf 3566 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ↔ (𝑥𝑌 ∧ (∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))))
235223, 226, 234sylanbrc 574 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡)))) → 𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
236235ex 399 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑗 ∈ (0...𝑁)) → ((𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))) → 𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}))
237236eximdv 2008 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑗 ∈ (0...𝑁)) → (∃𝑥(𝑥𝐴 ∧ (∀𝑡𝑇 (0 ≤ (𝑥𝑡) ∧ (𝑥𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(𝑥𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑥𝑡))) → ∃𝑥 𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}))
238214, 237mpd 15 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑗 ∈ (0...𝑁)) → ∃𝑥 𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
239 ne0i 4133 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} → {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ≠ ∅)
240239exlimiv 2021 . . . . . . . . . . . . . . . . . . . 20 (∃𝑥 𝑥 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} → {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ≠ ∅)
241238, 240syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑗 ∈ (0...𝑁)) → {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ≠ ∅)
24268, 241eqnetrd 3056 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0...𝑁)) → (𝐻𝑗) ≠ ∅)
2432423adant3 1155 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...𝑁) ∧ (𝐻𝑗) = 𝑤) → (𝐻𝑗) ≠ ∅)
24464, 243eqnetrrd 3057 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑁) ∧ (𝐻𝑗) = 𝑤) → 𝑤 ≠ ∅)
2452443exp 1141 . . . . . . . . . . . . . . 15 (𝜑 → (𝑗 ∈ (0...𝑁) → ((𝐻𝑗) = 𝑤𝑤 ≠ ∅)))
246245rexlimdv 3229 . . . . . . . . . . . . . 14 (𝜑 → (∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤𝑤 ≠ ∅))
247246adantr 468 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ran 𝐻) → (∃𝑗 ∈ (0...𝑁)(𝐻𝑗) = 𝑤𝑤 ≠ ∅))
24863, 247mpd 15 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ran 𝐻) → 𝑤 ≠ ∅)
249248adantlr 697 . . . . . . . . . . 11 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → 𝑤 ≠ ∅)
250 rsp 3128 . . . . . . . . . . 11 (∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤) → (𝑤 ∈ ran 𝐻 → (𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)))
25148, 49, 249, 250syl3c 66 . . . . . . . . . 10 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → (𝑤) ∈ 𝑤)
252251ex 399 . . . . . . . . 9 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → (𝑤 ∈ ran 𝐻 → (𝑤) ∈ 𝑤))
25347, 252ralrimi 3156 . . . . . . . 8 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ∀𝑤 ∈ ran 𝐻(𝑤) ∈ 𝑤)
254 chfnrn 6559 . . . . . . . 8 (( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤) ∈ 𝑤) → ran ran 𝐻)
25532, 253, 254syl2anc 575 . . . . . . 7 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ran ran 𝐻)
256 nfv 2005 . . . . . . . . . 10 𝑦𝜑
257 nfcv 2959 . . . . . . . . . . . 12 𝑦
258 nfcv 2959 . . . . . . . . . . . . . . 15 𝑦(0...𝑁)
259 nfrab1 3322 . . . . . . . . . . . . . . 15 𝑦{𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}
260258, 259nfmpt 4951 . . . . . . . . . . . . . 14 𝑦(𝑗 ∈ (0...𝑁) ↦ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
26122, 260nfcxfr 2957 . . . . . . . . . . . . 13 𝑦𝐻
262261nfrn 5582 . . . . . . . . . . . 12 𝑦ran 𝐻
263257, 262nffn 6207 . . . . . . . . . . 11 𝑦 Fn ran 𝐻
264 nfv 2005 . . . . . . . . . . . 12 𝑦(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)
265262, 264nfral 3144 . . . . . . . . . . 11 𝑦𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)
266263, 265nfan 1990 . . . . . . . . . 10 𝑦( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))
267256, 266nfan 1990 . . . . . . . . 9 𝑦(𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)))
268262nfuni 4647 . . . . . . . . 9 𝑦 ran 𝐻
269 fnunirn 6744 . . . . . . . . . . . . . . 15 (𝐻 Fn (0...𝑁) → (𝑦 ran 𝐻 ↔ ∃𝑧 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑧)))
270 nfcv 2959 . . . . . . . . . . . . . . . . . 18 𝑗𝑧
27153, 270nffv 6427 . . . . . . . . . . . . . . . . 17 𝑗(𝐻𝑧)
272271nfcri 2953 . . . . . . . . . . . . . . . 16 𝑗 𝑦 ∈ (𝐻𝑧)
273 nfv 2005 . . . . . . . . . . . . . . . 16 𝑧 𝑦 ∈ (𝐻𝑗)
274 fveq2 6417 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑗 → (𝐻𝑧) = (𝐻𝑗))
275274eleq2d 2882 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑗 → (𝑦 ∈ (𝐻𝑧) ↔ 𝑦 ∈ (𝐻𝑗)))
276272, 273, 275cbvrex 3368 . . . . . . . . . . . . . . 15 (∃𝑧 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑧) ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑗))
277269, 276syl6bb 278 . . . . . . . . . . . . . 14 (𝐻 Fn (0...𝑁) → (𝑦 ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑗)))
27824, 277syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑦 ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑗)))
279278biimpa 464 . . . . . . . . . . . 12 ((𝜑𝑦 ran 𝐻) → ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑗))
280 nfv 2005 . . . . . . . . . . . . . 14 𝑗𝜑
28153nfrn 5582 . . . . . . . . . . . . . . . 16 𝑗ran 𝐻
282281nfuni 4647 . . . . . . . . . . . . . . 15 𝑗 ran 𝐻
283282nfcri 2953 . . . . . . . . . . . . . 14 𝑗 𝑦 ran 𝐻
284280, 283nfan 1990 . . . . . . . . . . . . 13 𝑗(𝜑𝑦 ran 𝐻)
285 nfv 2005 . . . . . . . . . . . . 13 𝑗 𝑦𝑌
286 simp1l 1247 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝜑)
287 simp2 1160 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑗 ∈ (0...𝑁))
288 simp3 1161 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑦 ∈ (𝐻𝑗))
28968eleq2d 2882 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑦 ∈ (𝐻𝑗) ↔ 𝑦 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}))
290289biimpa 464 . . . . . . . . . . . . . . . . 17 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑦 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
291 rabid 3315 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))} ↔ (𝑦𝑌 ∧ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))))
292290, 291sylib 209 . . . . . . . . . . . . . . . 16 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → (𝑦𝑌 ∧ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))))
293292simpld 484 . . . . . . . . . . . . . . 15 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑦𝑌)
294286, 287, 288, 293syl21anc 857 . . . . . . . . . . . . . 14 (((𝜑𝑦 ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑦𝑌)
2952943exp 1141 . . . . . . . . . . . . 13 ((𝜑𝑦 ran 𝐻) → (𝑗 ∈ (0...𝑁) → (𝑦 ∈ (𝐻𝑗) → 𝑦𝑌)))
296284, 285, 295rexlimd 3225 . . . . . . . . . . . 12 ((𝜑𝑦 ran 𝐻) → (∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻𝑗) → 𝑦𝑌))
297279, 296mpd 15 . . . . . . . . . . 11 ((𝜑𝑦 ran 𝐻) → 𝑦𝑌)
298297adantlr 697 . . . . . . . . . 10 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑦 ran 𝐻) → 𝑦𝑌)
299298ex 399 . . . . . . . . 9 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → (𝑦 ran 𝐻𝑦𝑌))
300267, 268, 3, 299ssrd 3814 . . . . . . . 8 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ran 𝐻𝑌)
301 ssrab2 3895 . . . . . . . . 9 {𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)} ⊆ 𝐴
3021, 301eqsstri 3843 . . . . . . . 8 𝑌𝐴
303300, 302syl6ss 3821 . . . . . . 7 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ran 𝐻𝐴)
304255, 303sstrd 3819 . . . . . 6 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ran 𝐴)
30542, 304fssd 6279 . . . . 5 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → :ran 𝐻𝐴)
306 dffn3 6276 . . . . . . 7 (𝐻 Fn (0...𝑁) ↔ 𝐻:(0...𝑁)⟶ran 𝐻)
30724, 306sylib 209 . . . . . 6 (𝜑𝐻:(0...𝑁)⟶ran 𝐻)
308307adantr 468 . . . . 5 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → 𝐻:(0...𝑁)⟶ran 𝐻)
309 fco 6282 . . . . 5 ((:ran 𝐻𝐴𝐻:(0...𝑁)⟶ran 𝐻) → (𝐻):(0...𝑁)⟶𝐴)
310305, 308, 309syl2anc 575 . . . 4 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → (𝐻):(0...𝑁)⟶𝐴)
311 nfcv 2959 . . . . . . . 8 𝑗
312311, 281nffn 6207 . . . . . . 7 𝑗 Fn ran 𝐻
313 nfv 2005 . . . . . . . 8 𝑗(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)
314281, 313nfral 3144 . . . . . . 7 𝑗𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)
315312, 314nfan 1990 . . . . . 6 𝑗( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))
316280, 315nfan 1990 . . . . 5 𝑗(𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤)))
317 simpll 774 . . . . . . . . . 10 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝜑)
318 simpr 473 . . . . . . . . . 10 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
31924ad2antrr 708 . . . . . . . . . . . 12 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝐻 Fn (0...𝑁))
320 fvco2 6503 . . . . . . . . . . . 12 ((𝐻 Fn (0...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → ((𝐻)‘𝑗) = (‘(𝐻𝑗)))
321319, 320sylancom 578 . . . . . . . . . . 11 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝐻)‘𝑗) = (‘(𝐻𝑗)))
322 simplrr 787 . . . . . . . . . . . . 13 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))
323 fnfun 6208 . . . . . . . . . . . . . . . 16 (𝐻 Fn (0...𝑁) → Fun 𝐻)
32424, 323syl 17 . . . . . . . . . . . . . . 15 (𝜑 → Fun 𝐻)
325324ad2antrr 708 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → Fun 𝐻)
326 fndm 6210 . . . . . . . . . . . . . . . . . 18 (𝐻 Fn (0...𝑁) → dom 𝐻 = (0...𝑁))
32724, 326syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → dom 𝐻 = (0...𝑁))
328327adantr 468 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...𝑁)) → dom 𝐻 = (0...𝑁))
32965, 328eleqtrrd 2899 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...𝑁)) → 𝑗 ∈ dom 𝐻)
330329adantlr 697 . . . . . . . . . . . . . 14 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ dom 𝐻)
331 fvelrn 6583 . . . . . . . . . . . . . 14 ((Fun 𝐻𝑗 ∈ dom 𝐻) → (𝐻𝑗) ∈ ran 𝐻)
332325, 330, 331syl2anc 575 . . . . . . . . . . . . 13 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (𝐻𝑗) ∈ ran 𝐻)
333322, 332jca 503 . . . . . . . . . . . 12 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤) ∧ (𝐻𝑗) ∈ ran 𝐻))
334242adantlr 697 . . . . . . . . . . . 12 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (𝐻𝑗) ≠ ∅)
335 neeq1 3051 . . . . . . . . . . . . . 14 (𝑤 = (𝐻𝑗) → (𝑤 ≠ ∅ ↔ (𝐻𝑗) ≠ ∅))
336 fveq2 6417 . . . . . . . . . . . . . . 15 (𝑤 = (𝐻𝑗) → (𝑤) = (‘(𝐻𝑗)))
337 id 22 . . . . . . . . . . . . . . 15 (𝑤 = (𝐻𝑗) → 𝑤 = (𝐻𝑗))
338336, 337eleq12d 2890 . . . . . . . . . . . . . 14 (𝑤 = (𝐻𝑗) → ((𝑤) ∈ 𝑤 ↔ (‘(𝐻𝑗)) ∈ (𝐻𝑗)))
339335, 338imbi12d 335 . . . . . . . . . . . . 13 (𝑤 = (𝐻𝑗) → ((𝑤 ≠ ∅ → (𝑤) ∈ 𝑤) ↔ ((𝐻𝑗) ≠ ∅ → (‘(𝐻𝑗)) ∈ (𝐻𝑗))))
340339rspccva 3512 . . . . . . . . . . . 12 ((∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤) ∧ (𝐻𝑗) ∈ ran 𝐻) → ((𝐻𝑗) ≠ ∅ → (‘(𝐻𝑗)) ∈ (𝐻𝑗)))
341333, 334, 340sylc 65 . . . . . . . . . . 11 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (‘(𝐻𝑗)) ∈ (𝐻𝑗))
342321, 341eqeltrd 2896 . . . . . . . . . 10 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝐻)‘𝑗) ∈ (𝐻𝑗))
343257, 261nfco 5502 . . . . . . . . . . . . 13 𝑦(𝐻)
344 nfcv 2959 . . . . . . . . . . . . 13 𝑦𝑗
345343, 344nffv 6427 . . . . . . . . . . . 12 𝑦((𝐻)‘𝑗)
346 nfv 2005 . . . . . . . . . . . . . 14 𝑦(𝜑𝑗 ∈ (0...𝑁))
347261, 344nffv 6427 . . . . . . . . . . . . . . 15 𝑦(𝐻𝑗)
348345, 347nfel 2972 . . . . . . . . . . . . . 14 𝑦((𝐻)‘𝑗) ∈ (𝐻𝑗)
349346, 348nfan 1990 . . . . . . . . . . . . 13 𝑦((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗))
350345, 3nfel 2972 . . . . . . . . . . . . 13 𝑦((𝐻)‘𝑗) ∈ 𝑌
351349, 350nfim 1987 . . . . . . . . . . . 12 𝑦(((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ((𝐻)‘𝑗) ∈ 𝑌)
352 eleq1 2884 . . . . . . . . . . . . . 14 (𝑦 = ((𝐻)‘𝑗) → (𝑦 ∈ (𝐻𝑗) ↔ ((𝐻)‘𝑗) ∈ (𝐻𝑗)))
353352anbi2d 616 . . . . . . . . . . . . 13 (𝑦 = ((𝐻)‘𝑗) → (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) ↔ ((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗))))
354 eleq1 2884 . . . . . . . . . . . . 13 (𝑦 = ((𝐻)‘𝑗) → (𝑦𝑌 ↔ ((𝐻)‘𝑗) ∈ 𝑌))
355353, 354imbi12d 335 . . . . . . . . . . . 12 (𝑦 = ((𝐻)‘𝑗) → ((((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → 𝑦𝑌) ↔ (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ((𝐻)‘𝑗) ∈ 𝑌)))
356345, 351, 355, 293vtoclgf 3468 . . . . . . . . . . 11 (((𝐻)‘𝑗) ∈ (𝐻𝑗) → (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ((𝐻)‘𝑗) ∈ 𝑌))
357356anabsi7 653 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ((𝐻)‘𝑗) ∈ 𝑌)
358317, 318, 342, 357syl21anc 857 . . . . . . . . 9 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((𝐻)‘𝑗) ∈ 𝑌)
3591eleq2i 2888 . . . . . . . . . 10 (((𝐻)‘𝑗) ∈ 𝑌 ↔ ((𝐻)‘𝑗) ∈ {𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)})
360 nfcv 2959 . . . . . . . . . . 11 𝑦𝐴
361 nfcv 2959 . . . . . . . . . . . 12 𝑦𝑇
362 nfcv 2959 . . . . . . . . . . . . . 14 𝑦0
363 nfcv 2959 . . . . . . . . . . . . . 14 𝑦
364 nfcv 2959 . . . . . . . . . . . . . . 15 𝑦𝑡
365345, 364nffv 6427 . . . . . . . . . . . . . 14 𝑦(((𝐻)‘𝑗)‘𝑡)
366362, 363, 365nfbr 4902 . . . . . . . . . . . . 13 𝑦0 ≤ (((𝐻)‘𝑗)‘𝑡)
367 nfcv 2959 . . . . . . . . . . . . . 14 𝑦1
368365, 363, 367nfbr 4902 . . . . . . . . . . . . 13 𝑦(((𝐻)‘𝑗)‘𝑡) ≤ 1
369366, 368nfan 1990 . . . . . . . . . . . 12 𝑦(0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)
370361, 369nfral 3144 . . . . . . . . . . 11 𝑦𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)
371 nfcv 2959 . . . . . . . . . . . . 13 𝑡𝑦
372 nfcv 2959 . . . . . . . . . . . . . . 15 𝑡
373 nfra1 3140 . . . . . . . . . . . . . . . . . . 19 𝑡𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁)
374 nfra1 3140 . . . . . . . . . . . . . . . . . . 19 𝑡𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡)
375373, 374nfan 1990 . . . . . . . . . . . . . . . . . 18 𝑡(∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))
376 nfra1 3140 . . . . . . . . . . . . . . . . . . . 20 𝑡𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)
377 nfcv 2959 . . . . . . . . . . . . . . . . . . . 20 𝑡𝐴
378376, 377nfrab 3323 . . . . . . . . . . . . . . . . . . 19 𝑡{𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)}
3791, 378nfcxfr 2957 . . . . . . . . . . . . . . . . . 18 𝑡𝑌
380375, 379nfrab 3323 . . . . . . . . . . . . . . . . 17 𝑡{𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))}
38170, 380nfmpt 4951 . . . . . . . . . . . . . . . 16 𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑦𝑌 ∣ (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))})
38222, 381nfcxfr 2957 . . . . . . . . . . . . . . 15 𝑡𝐻
383372, 382nfco 5502 . . . . . . . . . . . . . 14 𝑡(𝐻)
384383, 74nffv 6427 . . . . . . . . . . . . 13 𝑡((𝐻)‘𝑗)
385371, 384nfeq 2971 . . . . . . . . . . . 12 𝑡 𝑦 = ((𝐻)‘𝑗)
386 fveq1 6416 . . . . . . . . . . . . . 14 (𝑦 = ((𝐻)‘𝑗) → (𝑦𝑡) = (((𝐻)‘𝑗)‘𝑡))
387386breq2d 4867 . . . . . . . . . . . . 13 (𝑦 = ((𝐻)‘𝑗) → (0 ≤ (𝑦𝑡) ↔ 0 ≤ (((𝐻)‘𝑗)‘𝑡)))
388386breq1d 4865 . . . . . . . . . . . . 13 (𝑦 = ((𝐻)‘𝑗) → ((𝑦𝑡) ≤ 1 ↔ (((𝐻)‘𝑗)‘𝑡) ≤ 1))
389387, 388anbi12d 618 . . . . . . . . . . . 12 (𝑦 = ((𝐻)‘𝑗) → ((0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1) ↔ (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
390385, 389ralbid 3182 . . . . . . . . . . 11 (𝑦 = ((𝐻)‘𝑗) → (∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
391345, 360, 370, 390elrabf 3566 . . . . . . . . . 10 (((𝐻)‘𝑗) ∈ {𝑦𝐴 ∣ ∀𝑡𝑇 (0 ≤ (𝑦𝑡) ∧ (𝑦𝑡) ≤ 1)} ↔ (((𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
392359, 391bitri 266 . . . . . . . . 9 (((𝐻)‘𝑗) ∈ 𝑌 ↔ (((𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
393358, 392sylib 209 . . . . . . . 8 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (((𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
394393simprd 485 . . . . . . 7 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1))
395 nfcv 2959 . . . . . . . . . . . 12 𝑦(𝐷𝑗)
396 nfcv 2959 . . . . . . . . . . . . 13 𝑦 <
397 nfcv 2959 . . . . . . . . . . . . 13 𝑦(𝐸 / 𝑁)
398365, 396, 397nfbr 4902 . . . . . . . . . . . 12 𝑦(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)
399395, 398nfral 3144 . . . . . . . . . . 11 𝑦𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)
400349, 399nfim 1987 . . . . . . . . . 10 𝑦(((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))
401386breq1d 4865 . . . . . . . . . . . 12 (𝑦 = ((𝐻)‘𝑗) → ((𝑦𝑡) < (𝐸 / 𝑁) ↔ (((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
402385, 401ralbid 3182 . . . . . . . . . . 11 (𝑦 = ((𝐻)‘𝑗) → (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
403353, 402imbi12d 335 . . . . . . . . . 10 (𝑦 = ((𝐻)‘𝑗) → ((((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁)) ↔ (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))))
404292simprd 485 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → (∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡)))
405404simpld 484 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐷𝑗)(𝑦𝑡) < (𝐸 / 𝑁))
406345, 400, 403, 405vtoclgf 3468 . . . . . . . . 9 (((𝐻)‘𝑗) ∈ (𝐻𝑗) → (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
407406anabsi7 653 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))
408317, 318, 342, 407syl21anc 857 . . . . . . 7 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))
409 nfcv 2959 . . . . . . . . . . . 12 𝑦(𝐵𝑗)
410 nfcv 2959 . . . . . . . . . . . . 13 𝑦(1 − (𝐸 / 𝑁))
411410, 396, 365nfbr 4902 . . . . . . . . . . . 12 𝑦(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)
412409, 411nfral 3144 . . . . . . . . . . 11 𝑦𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)
413349, 412nfim 1987 . . . . . . . . . 10 𝑦(((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))
414386breq2d 4867 . . . . . . . . . . . 12 (𝑦 = ((𝐻)‘𝑗) → ((1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ (1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
415385, 414ralbid 3182 . . . . . . . . . . 11 (𝑦 = ((𝐻)‘𝑗) → (∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡) ↔ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
416353, 415imbi12d 335 . . . . . . . . . 10 (𝑦 = ((𝐻)‘𝑗) → ((((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡)) ↔ (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))))
417404simprd 485 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (𝑦𝑡))
418345, 413, 416, 417vtoclgf 3468 . . . . . . . . 9 (((𝐻)‘𝑗) ∈ (𝐻𝑗) → (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
419418anabsi7 653 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝐻)‘𝑗) ∈ (𝐻𝑗)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))
420317, 318, 342, 419syl21anc 857 . . . . . . 7 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))
421394, 408, 4203jca 1151 . . . . . 6 (((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
422421ex 399 . . . . 5 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → (𝑗 ∈ (0...𝑁) → (∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))))
423316, 422ralrimi 3156 . . . 4 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
424310, 423jca 503 . . 3 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ((𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))))
425 feq1 6246 . . . . 5 (𝑥 = (𝐻) → (𝑥:(0...𝑁)⟶𝐴 ↔ (𝐻):(0...𝑁)⟶𝐴))
426 nfcv 2959 . . . . . . 7 𝑗𝑥
427311, 53nfco 5502 . . . . . . 7 𝑗(𝐻)
428426, 427nfeq 2971 . . . . . 6 𝑗 𝑥 = (𝐻)
429 nfcv 2959 . . . . . . . . 9 𝑡𝑥
430429, 383nfeq 2971 . . . . . . . 8 𝑡 𝑥 = (𝐻)
431 fveq1 6416 . . . . . . . . . . 11 (𝑥 = (𝐻) → (𝑥𝑗) = ((𝐻)‘𝑗))
432431fveq1d 6419 . . . . . . . . . 10 (𝑥 = (𝐻) → ((𝑥𝑗)‘𝑡) = (((𝐻)‘𝑗)‘𝑡))
433432breq2d 4867 . . . . . . . . 9 (𝑥 = (𝐻) → (0 ≤ ((𝑥𝑗)‘𝑡) ↔ 0 ≤ (((𝐻)‘𝑗)‘𝑡)))
434432breq1d 4865 . . . . . . . . 9 (𝑥 = (𝐻) → (((𝑥𝑗)‘𝑡) ≤ 1 ↔ (((𝐻)‘𝑗)‘𝑡) ≤ 1))
435433, 434anbi12d 618 . . . . . . . 8 (𝑥 = (𝐻) → ((0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ↔ (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
436430, 435ralbid 3182 . . . . . . 7 (𝑥 = (𝐻) → (∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ↔ ∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1)))
437432breq1d 4865 . . . . . . . 8 (𝑥 = (𝐻) → (((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ (((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
438430, 437ralbid 3182 . . . . . . 7 (𝑥 = (𝐻) → (∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
439432breq2d 4867 . . . . . . . 8 (𝑥 = (𝐻) → ((1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
440430, 439ralbid 3182 . . . . . . 7 (𝑥 = (𝐻) → (∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡) ↔ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))
441436, 438, 4403anbi123d 1553 . . . . . 6 (𝑥 = (𝐻) → ((∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡)) ↔ (∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))))
442428, 441ralbid 3182 . . . . 5 (𝑥 = (𝐻) → (∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡)) ↔ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))))
443425, 442anbi12d 618 . . . 4 (𝑥 = (𝐻) → ((𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡))) ↔ ((𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡)))))
444443spcegv 3498 . . 3 ((𝐻) ∈ V → (((𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ (((𝐻)‘𝑗)‘𝑡) ∧ (((𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)(((𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < (((𝐻)‘𝑗)‘𝑡))) → ∃𝑥(𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡)))))
44540, 424, 444sylc 65 . 2 ((𝜑 ∧ ( Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (𝑤) ∈ 𝑤))) → ∃𝑥(𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡))))
44631, 445exlimddv 2026 1 (𝜑 → ∃𝑥(𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡𝑇 (0 ≤ ((𝑥𝑗)‘𝑡) ∧ ((𝑥𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷𝑗)((𝑥𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥𝑗)‘𝑡))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wex 1859  wnf 1863  wcel 2157  wnfc 2946  wne 2989  wral 3107  wrex 3108  {crab 3111  Vcvv 3402  cdif 3777  cin 3779  wss 3780  c0 4127   cuni 4641   class class class wbr 4855  cmpt 4934  dom cdm 5324  ran crn 5325  ccom 5328  Fun wfun 6104   Fn wfn 6105  wf 6106  cfv 6110  (class class class)co 6883  Fincfn 8201  cr 10229  0cc0 10230  1c1 10231   + caddc 10233   · cmul 10235   < clt 10368  cle 10369  cmin 10560   / cdiv 10978  cn 11314  3c3 11368  +crp 12065  (,)cioo 12412  ...cfz 12568  topGenctg 16322  Clsdccld 21054   Cn ccn 21262  Compccmp 21423
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4977  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7188  ax-inf2 8794  ax-cnex 10286  ax-resscn 10287  ax-1cn 10288  ax-icn 10289  ax-addcl 10290  ax-addrcl 10291  ax-mulcl 10292  ax-mulrcl 10293  ax-mulcom 10294  ax-addass 10295  ax-mulass 10296  ax-distr 10297  ax-i2m1 10298  ax-1ne0 10299  ax-1rid 10300  ax-rnegex 10301  ax-rrecex 10302  ax-cnre 10303  ax-pre-lttri 10304  ax-pre-lttrn 10305  ax-pre-ltadd 10306  ax-pre-mulgt0 10307  ax-pre-sup 10308  ax-mulf 10310
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-int 4681  df-iun 4725  df-iin 4726  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5232  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-se 5284  df-we 5285  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5906  df-ord 5952  df-on 5953  df-lim 5954  df-suc 5955  df-iota 6073  df-fun 6112  df-fn 6113  df-f 6114  df-f1 6115  df-fo 6116  df-f1o 6117  df-fv 6118  df-isom 6119  df-riota 6844  df-ov 6886  df-oprab 6887  df-mpt2 6888  df-of 7136  df-om 7305  df-1st 7407  df-2nd 7408  df-supp 7539  df-wrecs 7651  df-recs 7713  df-rdg 7751  df-1o 7805  df-2o 7806  df-oadd 7809  df-er 7988  df-map 8103  df-pm 8104  df-ixp 8155  df-en 8202  df-dom 8203  df-sdom 8204  df-fin 8205  df-fsupp 8524  df-fi 8565  df-sup 8596  df-inf 8597  df-oi 8663  df-card 9057  df-cda 9284  df-pnf 10370  df-mnf 10371  df-xr 10372  df-ltxr 10373  df-le 10374  df-sub 10562  df-neg 10563  df-div 10979  df-nn 11315  df-2 11375  df-3 11376  df-4 11377  df-5 11378  df-6 11379  df-7 11380  df-8 11381  df-9 11382  df-n0 11579  df-z 11663  df-dec 11779  df-uz 11924  df-q 12027  df-rp 12066  df-xneg 12181  df-xadd 12182  df-xmul 12183  df-ioo 12416  df-ioc 12417  df-ico 12418  df-icc 12419  df-fz 12569  df-fzo 12709  df-fl 12836  df-seq 13044  df-exp 13103  df-hash 13357  df-cj 14081  df-re 14082  df-im 14083  df-sqrt 14217  df-abs 14218  df-clim 14461  df-rlim 14462  df-sum 14659  df-struct 16089  df-ndx 16090  df-slot 16091  df-base 16093  df-sets 16094  df-ress 16095  df-plusg 16185  df-mulr 16186  df-starv 16187  df-sca 16188  df-vsca 16189  df-ip 16190  df-tset 16191  df-ple 16192  df-ds 16194  df-unif 16195  df-hom 16196  df-cco 16197  df-rest 16307  df-topn 16308  df-0g 16326  df-gsum 16327  df-topgen 16328  df-pt 16329  df-prds 16332  df-xrs 16386  df-qtop 16391  df-imas 16392  df-xps 16394  df-mre 16470  df-mrc 16471  df-acs 16473  df-mgm 17466  df-sgrp 17508  df-mnd 17519  df-submnd 17560  df-mulg 17765  df-cntz 17970  df-cmn 18415  df-psmet 19965  df-xmet 19966  df-met 19967  df-bl 19968  df-mopn 19969  df-cnfld 19974  df-top 20932  df-topon 20949  df-topsp 20971  df-bases 20984  df-cld 21057  df-cn 21265  df-cnp 21266  df-cmp 21424  df-tx 21599  df-hmeo 21792  df-xms 22358  df-ms 22359  df-tms 22360
This theorem is referenced by:  stoweidlem60  40773
  Copyright terms: Public domain W3C validator