stoweidlem59 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > stoweidlem59		Structured version Visualization version GIF version

Theorem stoweidlem59 42343

Description: This lemma proves that there exists a function 𝑥 as in the proof in [BrosowskiDeutsh] p. 91, after Lemma 2: x_j is in the subalgebra, 0 <= x_j <= 1, x_j < ε / n on A_j (meaning A in the paper), x_j > 1 - \epsilon / n on B_j. 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.

Step	Hyp	Ref	Expression
1		stoweidlem59.8	. . . . . . . . . 10 ⊢ 𝑌 = {𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)}
2		nfrab1 3384	. . . . . . . . . 10 ⊢ Ⅎ𝑦{𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)}
3	1, 2	nfcxfr 2975	. . . . . . . . 9 ⊢ Ⅎ𝑦𝑌
4		nfcv 2977	. . . . . . . . 9 ⊢ Ⅎ𝑧𝑌
5		nfv 1911	. . . . . . . . 9 ⊢ Ⅎ𝑧(∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))
6		nfv 1911	. . . . . . . . 9 ⊢ Ⅎ𝑦(∀𝑡 ∈ (𝐷‘𝑗)(𝑧‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑧‘𝑡))
7		fveq1 6668	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝑦‘𝑡) = (𝑧‘𝑡))
8	7	breq1d 5075	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((𝑦‘𝑡) < (𝐸 / 𝑁) ↔ (𝑧‘𝑡) < (𝐸 / 𝑁)))
9	8	ralbidv 3197	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷‘𝑗)(𝑧‘𝑡) < (𝐸 / 𝑁)))
10	7	breq2d 5077	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (𝑧‘𝑡)))
11	10	ralbidv 3197	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑧‘𝑡)))
12	9, 11	anbi12d 632	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)) ↔ (∀𝑡 ∈ (𝐷‘𝑗)(𝑧‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑧‘𝑡))))
13	3, 4, 5, 6, 12	cbvrabw 3489	. . . . . . . 8 ⊢ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} = {𝑧 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑧‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑧‘𝑡))}
14		ovexd 7190	. . . . . . . . . 10 ⊢ (𝜑 → (𝐽 Cn 𝐾) ∈ V)
15		stoweidlem59.11	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
16		stoweidlem59.5	. . . . . . . . . . 11 ⊢ 𝐶 = (𝐽 Cn 𝐾)
17	15, 16	sseqtrdi 4016	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ⊆ (𝐽 Cn 𝐾))
18	14, 17	ssexd 5227	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ V)
19	1, 18	rabexd 5235	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ V)
20	13, 19	rabexd 5235	. . . . . . 7 ⊢ (𝜑 → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V)
21	20	ralrimivw 3183	. . . . . 6 ⊢ (𝜑 → ∀𝑗 ∈ (0...𝑁){𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V)
22		stoweidlem59.9	. . . . . . 7 ⊢ 𝐻 = (𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
23	22	fnmpt 6487	. . . . . 6 ⊢ (∀𝑗 ∈ (0...𝑁){𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V → 𝐻 Fn (0...𝑁))
24	21, 23	syl 17	. . . . 5 ⊢ (𝜑 → 𝐻 Fn (0...𝑁))
25		fzfi 13339	. . . . 5 ⊢ (0...𝑁) ∈ Fin
26		fnfi 8795	. . . . 5 ⊢ ((𝐻 Fn (0...𝑁) ∧ (0...𝑁) ∈ Fin) → 𝐻 ∈ Fin)
27	24, 25, 26	sylancl 588	. . . 4 ⊢ (𝜑 → 𝐻 ∈ Fin)
28		rnfi 8806	. . . 4 ⊢ (𝐻 ∈ Fin → ran 𝐻 ∈ Fin)
29	27, 28	syl 17	. . 3 ⊢ (𝜑 → ran 𝐻 ∈ Fin)
30		fnchoice 41284	. . 3 ⊢ (ran 𝐻 ∈ Fin → ∃ℎ(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)))
31	29, 30	syl 17	. 2 ⊢ (𝜑 → ∃ℎ(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)))
32		simprl 769	. . . . 5 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ℎ Fn ran 𝐻)
33		ovex 7188	. . . . . . . 8 ⊢ (0...𝑁) ∈ V
34	33	mptex 6985	. . . . . . 7 ⊢ (𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}) ∈ V
35	22, 34	eqeltri 2909	. . . . . 6 ⊢ 𝐻 ∈ V
36	35	rnex 7616	. . . . 5 ⊢ ran 𝐻 ∈ V
37		fnex 6979	. . . . 5 ⊢ ((ℎ Fn ran 𝐻 ∧ ran 𝐻 ∈ V) → ℎ ∈ V)
38	32, 36, 37	sylancl 588	. . . 4 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ℎ ∈ V)
39		coexg 7633	. . . 4 ⊢ ((ℎ ∈ V ∧ 𝐻 ∈ V) → (ℎ ∘ 𝐻) ∈ V)
40	38, 35, 39	sylancl 588	. . 3 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (ℎ ∘ 𝐻) ∈ V)
41		dffn3 6524	. . . . . . 7 ⊢ (ℎ Fn ran 𝐻 ↔ ℎ:ran 𝐻⟶ran ℎ)
42	32, 41	sylib 220	. . . . . 6 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ℎ:ran 𝐻⟶ran ℎ)
43		nfv 1911	. . . . . . . . . 10 ⊢ Ⅎ𝑤𝜑
44		nfv 1911	. . . . . . . . . . 11 ⊢ Ⅎ𝑤 ℎ Fn ran 𝐻
45		nfra1 3219	. . . . . . . . . . 11 ⊢ Ⅎ𝑤∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)
46	44, 45	nfan 1896	. . . . . . . . . 10 ⊢ Ⅎ𝑤(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))
47	43, 46	nfan 1896	. . . . . . . . 9 ⊢ Ⅎ𝑤(𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)))
48		simplrr 776	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))
49		simpr 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → 𝑤 ∈ ran 𝐻)
50		fvelrnb 6725	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 Fn (0...𝑁) → (𝑤 ∈ ran 𝐻 ↔ ∃𝑎 ∈ (0...𝑁)(𝐻‘𝑎) = 𝑤))
51		nfv 1911	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑎(𝐻‘𝑗) = 𝑤
52		nfmpt1 5163	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑗(𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
53	22, 52	nfcxfr 2975	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗𝐻
54		nfcv 2977	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗𝑎
55	53, 54	nffv 6679	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗(𝐻‘𝑎)
56		nfcv 2977	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗𝑤
57	55, 56	nfeq 2991	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑗(𝐻‘𝑎) = 𝑤
58		fveq2 6669	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑎 → (𝐻‘𝑗) = (𝐻‘𝑎))
59	58	eqeq1d 2823	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑎 → ((𝐻‘𝑗) = 𝑤 ↔ (𝐻‘𝑎) = 𝑤))
60	51, 57, 59	cbvrexw 3442	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤 ↔ ∃𝑎 ∈ (0...𝑁)(𝐻‘𝑎) = 𝑤)
61	50, 60	syl6bbr 291	. . . . . . . . . . . . . . 15 ⊢ (𝐻 Fn (0...𝑁) → (𝑤 ∈ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤))
62	24, 61	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑤 ∈ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤))
63	62	biimpa 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤)
64		simp3 1134	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ (𝐻‘𝑗) = 𝑤) → (𝐻‘𝑗) = 𝑤)
65		simpr 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
66	20	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V)
67	22	fvmpt2 6778	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ (0...𝑁) ∧ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V) → (𝐻‘𝑗) = {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
68	65, 66, 67	syl2anc 586	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐻‘𝑗) = {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
69		stoweidlem59.6	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
70		nfcv 2977	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑡(0...𝑁)
71		nfrab1 3384	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑡{𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}
72	70, 71	nfmpt 5162	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
73	69, 72	nfcxfr 2975	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡𝐷
74		nfcv 2977	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡𝑗
75	73, 74	nffv 6679	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑡(𝐷‘𝑗)
76		nfcv 2977	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡𝑇
77		stoweidlem59.7	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
78		nfrab1 3384	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑡{𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}
79	70, 78	nfmpt 5162	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
80	77, 79	nfcxfr 2975	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑡𝐵
81	80, 74	nffv 6679	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡(𝐵‘𝑗)
82	76, 81	nfdif 4101	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑡(𝑇 ∖ (𝐵‘𝑗))
83		stoweidlem59.2	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡𝜑
84		nfv 1911	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡 𝑗 ∈ (0...𝑁)
85	83, 84	nfan 1896	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑗 ∈ (0...𝑁))
86		stoweidlem59.3	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐾 = (topGen‘ran (,))
87		stoweidlem59.4	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑇 = ∪ 𝐽
88		stoweidlem59.10	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐽 ∈ Comp)
89	88	adantr 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝐽 ∈ Comp)
90	15	adantr 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝐴 ⊆ 𝐶)
91		stoweidlem59.12	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)
92	91	3adant1r 1173	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)
93		stoweidlem59.13	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)
94	93	3adant1r 1173	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)
95		stoweidlem59.14	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑦) ∈ 𝐴)
96	95	adantlr 713	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑦) ∈ 𝐴)
97		stoweidlem59.15	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡))
98	97	adantlr 713	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡))
99	88	uniexd 7467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ∪ 𝐽 ∈ V)
100	87, 99	eqeltrid 2917	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑇 ∈ V)
101	100	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑇 ∈ V)
102		rabexg 5233	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V)
103	101, 102	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V)
104	77	fvmpt2 6778	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑗 ∈ (0...𝑁) ∧ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V) → (𝐵‘𝑗) = {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
105	65, 103, 104	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐵‘𝑗) = {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
106		stoweidlem59.1	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑡𝐹
107		eqid 2821	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} = {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}
108		elfzelz 12907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
109	108	zred 12086	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
110		3re 11716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 3 ∈ ℝ
111		3ne0 11742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 3 ≠ 0
112	110, 111	rereccli 11404	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (1 / 3) ∈ ℝ
113		readdcl 10619	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ) → (𝑗 + (1 / 3)) ∈ ℝ)
114	109, 112, 113	sylancl 588	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + (1 / 3)) ∈ ℝ)
115	114	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑗 + (1 / 3)) ∈ ℝ)
116		stoweidlem59.17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
117	116	rpred 12430	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐸 ∈ ℝ)
118	117	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝐸 ∈ ℝ)
119	115, 118	remulcld 10670	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑗 + (1 / 3)) · 𝐸) ∈ ℝ)
120		stoweidlem59.16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐹 ∈ 𝐶)
121	120, 16	eleqtrdi 2923	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))
122	121	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝐹 ∈ (𝐽 Cn 𝐾))
123	106, 86, 87, 107, 119, 122	rfcnpre3 41288	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ (Clsd‘𝐽))
124	105, 123	eqeltrd 2913	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐵‘𝑗) ∈ (Clsd‘𝐽))
125		rabexg 5233	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V)
126	101, 125	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V)
127	69	fvmpt2 6778	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑗 ∈ (0...𝑁) ∧ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V) → (𝐷‘𝑗) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
128	65, 126, 127	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐷‘𝑗) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
129		eqid 2821	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}
130		resubcl 10949	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ) → (𝑗 − (1 / 3)) ∈ ℝ)
131	109, 112, 130	sylancl 588	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ (0...𝑁) → (𝑗 − (1 / 3)) ∈ ℝ)
132	131	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑗 − (1 / 3)) ∈ ℝ)
133	132, 118	remulcld 10670	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ)
134	106, 86, 87, 129, 133, 122	rfcnpre4 41289	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ (Clsd‘𝐽))
135	128, 134	eqeltrd 2913	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐷‘𝑗) ∈ (Clsd‘𝐽))
136	133	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ)
137	119	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ((𝑗 + (1 / 3)) · 𝐸) ∈ ℝ)
138	86, 87, 16, 120	fcnre 41280	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 𝐹:𝑇⟶ℝ)
139	138	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → 𝐹:𝑇⟶ℝ)
140		ssrab2 4055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ⊆ 𝑇
141	105, 140	eqsstrdi 4020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐵‘𝑗) ⊆ 𝑇)
142	141	sselda 3966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → 𝑡 ∈ 𝑇)
143	139, 142	ffvelrnd 6851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → (𝐹‘𝑡) ∈ ℝ)
144	112, 130	mpan2 689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) ∈ ℝ)
145		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑗 ∈ ℝ → 𝑗 ∈ ℝ)
146	112, 113	mpan2 689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑗 ∈ ℝ → (𝑗 + (1 / 3)) ∈ ℝ)
147		3pos 11741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ 0 < 3
148	110, 147	recgt0ii 11545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ 0 < (1 / 3)
149	112, 148	elrpii 12391	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (1 / 3) ∈ ℝ⁺
150		ltsubrp 12424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ⁺) → (𝑗 − (1 / 3)) < 𝑗)
151	149, 150	mpan2 689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) < 𝑗)
152		ltaddrp 12425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ⁺) → 𝑗 < (𝑗 + (1 / 3)))
153	149, 152	mpan2 689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑗 ∈ ℝ → 𝑗 < (𝑗 + (1 / 3)))
154	144, 145, 146, 151, 153	lttrd 10800	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
155	109, 154	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑗 ∈ (0...𝑁) → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
156	155	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
157	116	rpregt0d 12436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
158	157	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
159		ltmul1 11489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑗 − (1 / 3)) ∈ ℝ ∧ (𝑗 + (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑗 − (1 / 3)) < (𝑗 + (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸)))
160	132, 115, 158, 159	syl3anc 1367	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) < (𝑗 + (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸)))
161	156, 160	mpbid 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸))
162	161	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸))
163	105	eleq2d 2898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑡 ∈ (𝐵‘𝑗) ↔ 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}))
164	163	biimpa 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
165		rabid 3378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑡 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ↔ (𝑡 ∈ 𝑇 ∧ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)))
166	164, 165	sylib 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → (𝑡 ∈ 𝑇 ∧ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)))
167	166	simprd 498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡))
168	136, 137, 143, 162, 167	ltletrd 10799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) < (𝐹‘𝑡))
169	136, 143	ltnled 10786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → (((𝑗 − (1 / 3)) · 𝐸) < (𝐹‘𝑡) ↔ ¬ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
170	168, 169	mpbid 234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ¬ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))
171	170	intnand 491	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ¬ (𝑡 ∈ 𝑇 ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
172		rabid 3378	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ↔ (𝑡 ∈ 𝑇 ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
173	171, 172	sylnibr 331	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ¬ 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
174	128	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → (𝐷‘𝑗) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
175	173, 174	neleqtrrd 2935	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ¬ 𝑡 ∈ (𝐷‘𝑗))
176	175	ex 415	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑡 ∈ (𝐵‘𝑗) → ¬ 𝑡 ∈ (𝐷‘𝑗)))
177	85, 176	ralrimi 3216	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐵‘𝑗) ¬ 𝑡 ∈ (𝐷‘𝑗))
178		disj 4398	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐵‘𝑗) ∩ (𝐷‘𝑗)) = ∅ ↔ ∀𝑎 ∈ (𝐵‘𝑗) ¬ 𝑎 ∈ (𝐷‘𝑗))
179		nfcv 2977	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑎(𝐵‘𝑗)
180	75	nfcri 2971	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑡 𝑎 ∈ (𝐷‘𝑗)
181	180	nfn 1853	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑡 ¬ 𝑎 ∈ (𝐷‘𝑗)
182		nfv 1911	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑎 ¬ 𝑡 ∈ (𝐷‘𝑗)
183		eleq1 2900	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = 𝑡 → (𝑎 ∈ (𝐷‘𝑗) ↔ 𝑡 ∈ (𝐷‘𝑗)))
184	183	notbid 320	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑡 → (¬ 𝑎 ∈ (𝐷‘𝑗) ↔ ¬ 𝑡 ∈ (𝐷‘𝑗)))
185	179, 81, 181, 182, 184	cbvralfw 3437	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∀𝑎 ∈ (𝐵‘𝑗) ¬ 𝑎 ∈ (𝐷‘𝑗) ↔ ∀𝑡 ∈ (𝐵‘𝑗) ¬ 𝑡 ∈ (𝐷‘𝑗))
186	178, 185	bitri 277	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐵‘𝑗) ∩ (𝐷‘𝑗)) = ∅ ↔ ∀𝑡 ∈ (𝐵‘𝑗) ¬ 𝑡 ∈ (𝐷‘𝑗))
187	177, 186	sylibr 236	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝐵‘𝑗) ∩ (𝐷‘𝑗)) = ∅)
188		eqid 2821	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑇 ∖ (𝐵‘𝑗)) = (𝑇 ∖ (𝐵‘𝑗))
189		stoweidlem59.19	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑁 ∈ ℕ)
190	189	nnrpd 12428	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
191	116, 190	rpdivcld 12447	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℝ⁺)
192	191	adantr 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐸 / 𝑁) ∈ ℝ⁺)
193	117, 189	nndivred 11690	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℝ)
194	112	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (1 / 3) ∈ ℝ)
195	189	nnge1d 11684	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 1 ≤ 𝑁)
196		1re 10640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 1 ∈ ℝ
197		0lt1 11161	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 0 < 1
198	196, 197	pm3.2i 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (1 ∈ ℝ ∧ 0 < 1)
199	198	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (1 ∈ ℝ ∧ 0 < 1))
200	189	nnred 11652	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑁 ∈ ℝ)
201	189	nngt0d 11685	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 0 < 𝑁)
202		lediv2 11529	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((1 ∈ ℝ ∧ 0 < 1) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (1 ≤ 𝑁 ↔ (𝐸 / 𝑁) ≤ (𝐸 / 1)))
203	199, 200, 201, 157, 202	syl121anc 1371	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (1 ≤ 𝑁 ↔ (𝐸 / 𝑁) ≤ (𝐸 / 1)))
204	195, 203	mpbid 234	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐸 / 𝑁) ≤ (𝐸 / 1))
205	116	rpcnd 12432	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐸 ∈ ℂ)
206	205	div1d 11407	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐸 / 1) = 𝐸)
207	204, 206	breqtrd 5091	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐸 / 𝑁) ≤ 𝐸)
208		stoweidlem59.18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐸 < (1 / 3))
209	193, 117, 194, 207, 208	lelttrd 10797	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐸 / 𝑁) < (1 / 3))
210	209	adantr 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐸 / 𝑁) < (1 / 3))
211	75, 82, 85, 86, 87, 16, 89, 90, 92, 94, 96, 98, 124, 135, 187, 188, 192, 210	stoweidlem58 42342	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))
212		df-rex 3144	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))))
213	211, 212	sylib 220	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ∃𝑥(𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))))
214		simprl 769	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → 𝑥 ∈ 𝐴)
215		simprr1 1217	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1))
216		fveq1 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 = 𝑥 → (𝑦‘𝑡) = (𝑥‘𝑡))
217	216	breq2d 5077	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 = 𝑥 → (0 ≤ (𝑦‘𝑡) ↔ 0 ≤ (𝑥‘𝑡)))
218	216	breq1d 5075	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 = 𝑥 → ((𝑦‘𝑡) ≤ 1 ↔ (𝑥‘𝑡) ≤ 1))
219	217, 218	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = 𝑥 → ((0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ↔ (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1)))
220	219	ralbidv 3197	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑥 → (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1)))
221	220, 1	elrab2 3682	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ 𝑌 ↔ (𝑥 ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1)))
222	214, 215, 221	sylanbrc 585	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → 𝑥 ∈ 𝑌)
223		simprr2 1218	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁))
224		simprr3 1219	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))
225	223, 224	jca 514	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → (∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))
226		nfcv 2977	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑦𝑥
227		nfv 1911	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑦(∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))
228	216	breq1d 5075	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = 𝑥 → ((𝑦‘𝑡) < (𝐸 / 𝑁) ↔ (𝑥‘𝑡) < (𝐸 / 𝑁)))
229	228	ralbidv 3197	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑥 → (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁)))
230	216	breq2d 5077	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = 𝑥 → ((1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))
231	230	ralbidv 3197	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑥 → (∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))
232	229, 231	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑥 → ((∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)) ↔ (∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))))
233	226, 3, 227, 232	elrabf 3675	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ↔ (𝑥 ∈ 𝑌 ∧ (∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))))
234	222, 225, 233	sylanbrc 585	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → 𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
235	234	ex 415	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))) → 𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}))
236	235	eximdv 1914	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (∃𝑥(𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))) → ∃𝑥 𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}))
237	213, 236	mpd 15	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ∃𝑥 𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
238		ne0i 4299	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ≠ ∅)
239	238	exlimiv 1927	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑥 𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ≠ ∅)
240	237, 239	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ≠ ∅)
241	68, 240	eqnetrd 3083	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐻‘𝑗) ≠ ∅)
242	241	3adant3 1128	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ (𝐻‘𝑗) = 𝑤) → (𝐻‘𝑗) ≠ ∅)
243	64, 242	eqnetrrd 3084	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ (𝐻‘𝑗) = 𝑤) → 𝑤 ≠ ∅)
244	243	3exp 1115	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ (0...𝑁) → ((𝐻‘𝑗) = 𝑤 → 𝑤 ≠ ∅)))
245	244	rexlimdv 3283	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤 → 𝑤 ≠ ∅))
246	245	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐻) → (∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤 → 𝑤 ≠ ∅))
247	63, 246	mpd 15	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐻) → 𝑤 ≠ ∅)
248	247	adantlr 713	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → 𝑤 ≠ ∅)
249		rsp 3205	. . . . . . . . . . 11 ⊢ (∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) → (𝑤 ∈ ran 𝐻 → (𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)))
250	48, 49, 248, 249	syl3c 66	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → (ℎ‘𝑤) ∈ 𝑤)
251	250	ex 415	. . . . . . . . 9 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (𝑤 ∈ ran 𝐻 → (ℎ‘𝑤) ∈ 𝑤))
252	47, 251	ralrimi 3216	. . . . . . . 8 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∀𝑤 ∈ ran 𝐻(ℎ‘𝑤) ∈ 𝑤)
253		chfnrn 6818	. . . . . . . 8 ⊢ ((ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(ℎ‘𝑤) ∈ 𝑤) → ran ℎ ⊆ ∪ ran 𝐻)
254	32, 252, 253	syl2anc 586	. . . . . . 7 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ran ℎ ⊆ ∪ ran 𝐻)
255		nfv 1911	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝜑
256		nfcv 2977	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦ℎ
257		nfcv 2977	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦(0...𝑁)
258		nfrab1 3384	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦{𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}
259	257, 258	nfmpt 5162	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦(𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
260	22, 259	nfcxfr 2975	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦𝐻
261	260	nfrn 5823	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦ran 𝐻
262	256, 261	nffn 6451	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 ℎ Fn ran 𝐻
263		nfv 1911	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)
264	261, 263	nfralw 3225	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)
265	262, 264	nfan 1896	. . . . . . . . . 10 ⊢ Ⅎ𝑦(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))
266	255, 265	nfan 1896	. . . . . . . . 9 ⊢ Ⅎ𝑦(𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)))
267	261	nfuni 4844	. . . . . . . . 9 ⊢ Ⅎ𝑦∪ ran 𝐻
268		fnunirn 7011	. . . . . . . . . . . . . . 15 ⊢ (𝐻 Fn (0...𝑁) → (𝑦 ∈ ∪ ran 𝐻 ↔ ∃𝑧 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑧)))
269		nfcv 2977	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗𝑧
270	53, 269	nffv 6679	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑗(𝐻‘𝑧)
271	270	nfcri 2971	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑗 𝑦 ∈ (𝐻‘𝑧)
272		nfv 1911	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧 𝑦 ∈ (𝐻‘𝑗)
273		fveq2 6669	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑗 → (𝐻‘𝑧) = (𝐻‘𝑗))
274	273	eleq2d 2898	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑗 → (𝑦 ∈ (𝐻‘𝑧) ↔ 𝑦 ∈ (𝐻‘𝑗)))
275	271, 272, 274	cbvrexw 3442	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑧) ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑗))
276	268, 275	syl6bb 289	. . . . . . . . . . . . . 14 ⊢ (𝐻 Fn (0...𝑁) → (𝑦 ∈ ∪ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑗)))
277	24, 276	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑦 ∈ ∪ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑗)))
278	277	biimpa 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) → ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑗))
279		nfv 1911	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗𝜑
280	53	nfrn 5823	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑗ran 𝐻
281	280	nfuni 4844	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑗∪ ran 𝐻
282	281	nfcri 2971	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗 𝑦 ∈ ∪ ran 𝐻
283	279, 282	nfan 1896	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻)
284		nfv 1911	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗 𝑦 ∈ 𝑌
285		simp1l 1193	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝜑)
286		simp2 1133	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑗 ∈ (0...𝑁))
287		simp3 1134	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ (𝐻‘𝑗))
288	68	eleq2d 2898	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑦 ∈ (𝐻‘𝑗) ↔ 𝑦 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}))
289	288	biimpa 479	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
290		rabid 3378	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ↔ (𝑦 ∈ 𝑌 ∧ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))))
291	289, 290	sylib 220	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → (𝑦 ∈ 𝑌 ∧ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))))
292	291	simpld 497	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ 𝑌)
293	285, 286, 287, 292	syl21anc 835	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ 𝑌)
294	293	3exp 1115	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) → (𝑗 ∈ (0...𝑁) → (𝑦 ∈ (𝐻‘𝑗) → 𝑦 ∈ 𝑌)))
295	283, 284, 294	rexlimd 3317	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) → (∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑗) → 𝑦 ∈ 𝑌))
296	278, 295	mpd 15	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) → 𝑦 ∈ 𝑌)
297	296	adantlr 713	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑦 ∈ ∪ ran 𝐻) → 𝑦 ∈ 𝑌)
298	297	ex 415	. . . . . . . . 9 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (𝑦 ∈ ∪ ran 𝐻 → 𝑦 ∈ 𝑌))
299	266, 267, 3, 298	ssrd 3971	. . . . . . . 8 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∪ ran 𝐻 ⊆ 𝑌)
300		ssrab2 4055	. . . . . . . . 9 ⊢ {𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)} ⊆ 𝐴
301	1, 300	eqsstri 4000	. . . . . . . 8 ⊢ 𝑌 ⊆ 𝐴
302	299, 301	sstrdi 3978	. . . . . . 7 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∪ ran 𝐻 ⊆ 𝐴)
303	254, 302	sstrd 3976	. . . . . 6 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ran ℎ ⊆ 𝐴)
304	42, 303	fssd 6527	. . . . 5 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ℎ:ran 𝐻⟶𝐴)
305		dffn3 6524	. . . . . . 7 ⊢ (𝐻 Fn (0...𝑁) ↔ 𝐻:(0...𝑁)⟶ran 𝐻)
306	24, 305	sylib 220	. . . . . 6 ⊢ (𝜑 → 𝐻:(0...𝑁)⟶ran 𝐻)
307	306	adantr 483	. . . . 5 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → 𝐻:(0...𝑁)⟶ran 𝐻)
308		fco 6530	. . . . 5 ⊢ ((ℎ:ran 𝐻⟶𝐴 ∧ 𝐻:(0...𝑁)⟶ran 𝐻) → (ℎ ∘ 𝐻):(0...𝑁)⟶𝐴)
309	304, 307, 308	syl2anc 586	. . . 4 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (ℎ ∘ 𝐻):(0...𝑁)⟶𝐴)
310		nfcv 2977	. . . . . . . 8 ⊢ Ⅎ𝑗ℎ
311	310, 280	nffn 6451	. . . . . . 7 ⊢ Ⅎ𝑗 ℎ Fn ran 𝐻
312		nfv 1911	. . . . . . . 8 ⊢ Ⅎ𝑗(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)
313	280, 312	nfralw 3225	. . . . . . 7 ⊢ Ⅎ𝑗∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)
314	311, 313	nfan 1896	. . . . . 6 ⊢ Ⅎ𝑗(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))
315	279, 314	nfan 1896	. . . . 5 ⊢ Ⅎ𝑗(𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)))
316		simpll 765	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝜑)
317		simpr 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
318	24	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝐻 Fn (0...𝑁))
319		fvco2 6757	. . . . . . . . . . . 12 ⊢ ((𝐻 Fn (0...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → ((ℎ ∘ 𝐻)‘𝑗) = (ℎ‘(𝐻‘𝑗)))
320	318, 319	sylancom 590	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((ℎ ∘ 𝐻)‘𝑗) = (ℎ‘(𝐻‘𝑗)))
321		simplrr 776	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))
322		fnfun 6452	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 Fn (0...𝑁) → Fun 𝐻)
323	24, 322	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Fun 𝐻)
324	323	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → Fun 𝐻)
325		fndm 6454	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐻 Fn (0...𝑁) → dom 𝐻 = (0...𝑁))
326	24, 325	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom 𝐻 = (0...𝑁))
327	326	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → dom 𝐻 = (0...𝑁))
328	65, 327	eleqtrrd 2916	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ dom 𝐻)
329	328	adantlr 713	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ dom 𝐻)
330		fvelrn 6843	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐻 ∧ 𝑗 ∈ dom 𝐻) → (𝐻‘𝑗) ∈ ran 𝐻)
331	324, 329, 330	syl2anc 586	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (𝐻‘𝑗) ∈ ran 𝐻)
332	321, 331	jca 514	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) ∧ (𝐻‘𝑗) ∈ ran 𝐻))
333	241	adantlr 713	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (𝐻‘𝑗) ≠ ∅)
334		neeq1 3078	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝐻‘𝑗) → (𝑤 ≠ ∅ ↔ (𝐻‘𝑗) ≠ ∅))
335		fveq2 6669	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝐻‘𝑗) → (ℎ‘𝑤) = (ℎ‘(𝐻‘𝑗)))
336		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝐻‘𝑗) → 𝑤 = (𝐻‘𝑗))
337	335, 336	eleq12d 2907	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝐻‘𝑗) → ((ℎ‘𝑤) ∈ 𝑤 ↔ (ℎ‘(𝐻‘𝑗)) ∈ (𝐻‘𝑗)))
338	334, 337	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝐻‘𝑗) → ((𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) ↔ ((𝐻‘𝑗) ≠ ∅ → (ℎ‘(𝐻‘𝑗)) ∈ (𝐻‘𝑗))))
339	338	rspccva 3621	. . . . . . . . . . . 12 ⊢ ((∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) ∧ (𝐻‘𝑗) ∈ ran 𝐻) → ((𝐻‘𝑗) ≠ ∅ → (ℎ‘(𝐻‘𝑗)) ∈ (𝐻‘𝑗)))
340	332, 333, 339	sylc 65	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (ℎ‘(𝐻‘𝑗)) ∈ (𝐻‘𝑗))
341	320, 340	eqeltrd 2913	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗))
342	256, 260	nfco 5735	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(ℎ ∘ 𝐻)
343		nfcv 2977	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦𝑗
344	342, 343	nffv 6679	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦((ℎ ∘ 𝐻)‘𝑗)
345		nfv 1911	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑗 ∈ (0...𝑁))
346	260, 343	nffv 6679	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦(𝐻‘𝑗)
347	344, 346	nfel 2992	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)
348	345, 347	nfan 1896	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗))
349	344, 3	nfel 2992	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌
350	348, 349	nfim 1893	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌)
351		eleq1 2900	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (𝑦 ∈ (𝐻‘𝑗) ↔ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)))
352	351	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) ↔ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗))))
353		eleq1 2900	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (𝑦 ∈ 𝑌 ↔ ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌))
354	352, 353	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ 𝑌) ↔ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌)))
355	344, 350, 354, 292	vtoclgf 3565	. . . . . . . . . . 11 ⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗) → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌))
356	355	anabsi7 669	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌)
357	316, 317, 341, 356	syl21anc 835	. . . . . . . . 9 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌)
358	1	eleq2i 2904	. . . . . . . . . 10 ⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌 ↔ ((ℎ ∘ 𝐻)‘𝑗) ∈ {𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)})
359		nfcv 2977	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝐴
360		nfcv 2977	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦𝑇
361		nfcv 2977	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦0
362		nfcv 2977	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦 ≤
363		nfcv 2977	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦𝑡
364	344, 363	nffv 6679	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦(((ℎ ∘ 𝐻)‘𝑗)‘𝑡)
365	361, 362, 364	nfbr 5112	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)
366		nfcv 2977	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦1
367	364, 362, 366	nfbr 5112	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1
368	365, 367	nfan 1896	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)
369	360, 368	nfralw 3225	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)
370		nfcv 2977	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡𝑦
371		nfcv 2977	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡ℎ
372		nfra1 3219	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁)
373		nfra1 3219	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)
374	372, 373	nfan 1896	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡(∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))
375		nfra1 3219	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)
376		nfcv 2977	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡𝐴
377	375, 376	nfrabw 3385	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡{𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)}
378	1, 377	nfcxfr 2975	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡𝑌
379	374, 378	nfrabw 3385	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡{𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}
380	70, 379	nfmpt 5162	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
381	22, 380	nfcxfr 2975	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡𝐻
382	371, 381	nfco 5735	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡(ℎ ∘ 𝐻)
383	382, 74	nffv 6679	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((ℎ ∘ 𝐻)‘𝑗)
384	370, 383	nfeq 2991	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡 𝑦 = ((ℎ ∘ 𝐻)‘𝑗)
385		fveq1 6668	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (𝑦‘𝑡) = (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))
386	385	breq2d 5077	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (0 ≤ (𝑦‘𝑡) ↔ 0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
387	385	breq1d 5075	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((𝑦‘𝑡) ≤ 1 ↔ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1))
388	386, 387	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ↔ (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
389	384, 388	ralbid 3231	. . . . . . . . . . 11 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
390	344, 359, 369, 389	elrabf 3675	. . . . . . . . . 10 ⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ {𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)} ↔ (((ℎ ∘ 𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
391	358, 390	bitri 277	. . . . . . . . 9 ⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌 ↔ (((ℎ ∘ 𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
392	357, 391	sylib 220	. . . . . . . 8 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (((ℎ ∘ 𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
393	392	simprd 498	. . . . . . 7 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1))
394		nfcv 2977	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝐷‘𝑗)
395		nfcv 2977	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦 <
396		nfcv 2977	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝐸 / 𝑁)
397	364, 395, 396	nfbr 5112	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)
398	394, 397	nfralw 3225	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)
399	348, 398	nfim 1893	. . . . . . . . . 10 ⊢ Ⅎ𝑦(((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))
400	385	breq1d 5075	. . . . . . . . . . . 12 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((𝑦‘𝑡) < (𝐸 / 𝑁) ↔ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
401	384, 400	ralbid 3231	. . . . . . . . . . 11 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
402	352, 401	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁)) ↔ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))))
403	291	simprd 498	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)))
404	403	simpld 497	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁))
405	344, 399, 402, 404	vtoclgf 3565	. . . . . . . . 9 ⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗) → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
406	405	anabsi7 669	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))
407	316, 317, 341, 406	syl21anc 835	. . . . . . 7 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))
408		nfcv 2977	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝐵‘𝑗)
409		nfcv 2977	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(1 − (𝐸 / 𝑁))
410	409, 395, 364	nfbr 5112	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)
411	408, 410	nfralw 3225	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)
412	348, 411	nfim 1893	. . . . . . . . . 10 ⊢ Ⅎ𝑦(((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))
413	385	breq2d 5077	. . . . . . . . . . . 12 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
414	384, 413	ralbid 3231	. . . . . . . . . . 11 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
415	352, 414	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)) ↔ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))))
416	403	simprd 498	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))
417	344, 412, 415, 416	vtoclgf 3565	. . . . . . . . 9 ⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗) → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
418	417	anabsi7 669	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))
419	316, 317, 341, 418	syl21anc 835	. . . . . . 7 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))
420	393, 407, 419	3jca 1124	. . . . . 6 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
421	420	ex 415	. . . . 5 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (𝑗 ∈ (0...𝑁) → (∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))))
422	315, 421	ralrimi 3216	. . . 4 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
423	309, 422	jca 514	. . 3 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ((ℎ ∘ 𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))))
424		feq1 6494	. . . . 5 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (𝑥:(0...𝑁)⟶𝐴 ↔ (ℎ ∘ 𝐻):(0...𝑁)⟶𝐴))
425		nfcv 2977	. . . . . . 7 ⊢ Ⅎ𝑗𝑥
426	310, 53	nfco 5735	. . . . . . 7 ⊢ Ⅎ𝑗(ℎ ∘ 𝐻)
427	425, 426	nfeq 2991	. . . . . 6 ⊢ Ⅎ𝑗 𝑥 = (ℎ ∘ 𝐻)
428		nfcv 2977	. . . . . . . . 9 ⊢ Ⅎ𝑡𝑥
429	428, 382	nfeq 2991	. . . . . . . 8 ⊢ Ⅎ𝑡 𝑥 = (ℎ ∘ 𝐻)
430		fveq1 6668	. . . . . . . . . . 11 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (𝑥‘𝑗) = ((ℎ ∘ 𝐻)‘𝑗))
431	430	fveq1d 6671	. . . . . . . . . 10 ⊢ (𝑥 = (ℎ ∘ 𝐻) → ((𝑥‘𝑗)‘𝑡) = (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))
432	431	breq2d 5077	. . . . . . . . 9 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (0 ≤ ((𝑥‘𝑗)‘𝑡) ↔ 0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
433	431	breq1d 5075	. . . . . . . . 9 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (((𝑥‘𝑗)‘𝑡) ≤ 1 ↔ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1))
434	432, 433	anbi12d 632	. . . . . . . 8 ⊢ (𝑥 = (ℎ ∘ 𝐻) → ((0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ↔ (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
435	429, 434	ralbid 3231	. . . . . . 7 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
436	431	breq1d 5075	. . . . . . . 8 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
437	429, 436	ralbid 3231	. . . . . . 7 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
438	431	breq2d 5077	. . . . . . . 8 ⊢ (𝑥 = (ℎ ∘ 𝐻) → ((1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
439	429, 438	ralbid 3231	. . . . . . 7 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡) ↔ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
440	435, 437, 439	3anbi123d 1432	. . . . . 6 ⊢ (𝑥 = (ℎ ∘ 𝐻) → ((∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))))
441	427, 440	ralbid 3231	. . . . 5 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡)) ↔ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))))
442	424, 441	anbi12d 632	. . . 4 ⊢ (𝑥 = (ℎ ∘ 𝐻) → ((𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡))) ↔ ((ℎ ∘ 𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))))
443	442	spcegv 3596	. . 3 ⊢ ((ℎ ∘ 𝐻) ∈ V → (((ℎ ∘ 𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))) → ∃𝑥(𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡)))))
444	40, 423, 443	sylc 65	. 2 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∃𝑥(𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡))))
445	31, 444	exlimddv 1932	1 ⊢ (𝜑 → ∃𝑥(𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1533 ∃wex 1776 Ⅎwnf 1780 ∈ wcel 2110 Ⅎwnfc 2961 ≠ wne 3016 ∀wral 3138 ∃wrex 3139 {crab 3142 Vcvv 3494 ∖ cdif 3932 ∩ cin 3934 ⊆ wss 3935 ∅c0 4290 ∪ cuni 4837 class class class wbr 5065 ↦ cmpt 5145 dom cdm 5554 ran crn 5555 ∘ ccom 5558 Fun wfun 6348 Fn wfn 6349 ⟶wf 6350 ‘cfv 6354 (class class class)co 7155 Fincfn 8508 ℝcr 10535 0cc0 10536 1c1 10537 + caddc 10539 · cmul 10541 < clt 10674 ≤ cle 10675 − cmin 10869 / cdiv 11296 ℕcn 11637 3c3 11692 ℝ⁺crp 12388 (,)cioo 12737 ...cfz 12891 topGenctg 16710 Clsdccld 21623 Cn ccn 21831 Compccmp 21993

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-rep 5189 ax-sep 5202 ax-nul 5209 ax-pow 5265 ax-pr 5329 ax-un 7460 ax-inf2 9103 ax-cnex 10592 ax-resscn 10593 ax-1cn 10594 ax-icn 10595 ax-addcl 10596 ax-addrcl 10597 ax-mulcl 10598 ax-mulrcl 10599 ax-mulcom 10600 ax-addass 10601 ax-mulass 10602 ax-distr 10603 ax-i2m1 10604 ax-1ne0 10605 ax-1rid 10606 ax-rnegex 10607 ax-rrecex 10608 ax-cnre 10609 ax-pre-lttri 10610 ax-pre-lttrn 10611 ax-pre-ltadd 10612 ax-pre-mulgt0 10613 ax-pre-sup 10614 ax-mulf 10616

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-fal 1546 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4567 df-pr 4569 df-tp 4571 df-op 4573 df-uni 4838 df-int 4876 df-iun 4920 df-iin 4921 df-br 5066 df-opab 5128 df-mpt 5146 df-tr 5172 df-id 5459 df-eprel 5464 df-po 5473 df-so 5474 df-fr 5513 df-se 5514 df-we 5515 df-xp 5560 df-rel 5561 df-cnv 5562 df-co 5563 df-dm 5564 df-rn 5565 df-res 5566 df-ima 5567 df-pred 6147 df-ord 6193 df-on 6194 df-lim 6195 df-suc 6196 df-iota 6313 df-fun 6356 df-fn 6357 df-f 6358 df-f1 6359 df-fo 6360 df-f1o 6361 df-fv 6362 df-isom 6363 df-riota 7113 df-ov 7158 df-oprab 7159 df-mpo 7160 df-of 7408 df-om 7580 df-1st 7688 df-2nd 7689 df-supp 7830 df-wrecs 7946 df-recs 8007 df-rdg 8045 df-1o 8101 df-2o 8102 df-oadd 8105 df-er 8288 df-map 8407 df-pm 8408 df-ixp 8461 df-en 8509 df-dom 8510 df-sdom 8511 df-fin 8512 df-fsupp 8833 df-fi 8874 df-sup 8905 df-inf 8906 df-oi 8973 df-card 9367 df-pnf 10676 df-mnf 10677 df-xr 10678 df-ltxr 10679 df-le 10680 df-sub 10871 df-neg 10872 df-div 11297 df-nn 11638 df-2 11699 df-3 11700 df-4 11701 df-5 11702 df-6 11703 df-7 11704 df-8 11705 df-9 11706 df-n0 11897 df-z 11981 df-dec 12098 df-uz 12243 df-q 12348 df-rp 12389 df-xneg 12506 df-xadd 12507 df-xmul 12508 df-ioo 12741 df-ioc 12742 df-ico 12743 df-icc 12744 df-fz 12892 df-fzo 13033 df-fl 13161 df-seq 13369 df-exp 13429 df-hash 13690 df-cj 14457 df-re 14458 df-im 14459 df-sqrt 14593 df-abs 14594 df-clim 14844 df-rlim 14845 df-sum 15042 df-struct 16484 df-ndx 16485 df-slot 16486 df-base 16488 df-sets 16489 df-ress 16490 df-plusg 16577 df-mulr 16578 df-starv 16579 df-sca 16580 df-vsca 16581 df-ip 16582 df-tset 16583 df-ple 16584 df-ds 16586 df-unif 16587 df-hom 16588 df-cco 16589 df-rest 16695 df-topn 16696 df-0g 16714 df-gsum 16715 df-topgen 16716 df-pt 16717 df-prds 16720 df-xrs 16774 df-qtop 16779 df-imas 16780 df-xps 16782 df-mre 16856 df-mrc 16857 df-acs 16859 df-mgm 17851 df-sgrp 17900 df-mnd 17911 df-submnd 17956 df-mulg 18224 df-cntz 18446 df-cmn 18907 df-psmet 20536 df-xmet 20537 df-met 20538 df-bl 20539 df-mopn 20540 df-cnfld 20545 df-top 21501 df-topon 21518 df-topsp 21540 df-bases 21553 df-cld 21626 df-cn 21834 df-cnp 21835 df-cmp 21994 df-tx 22169 df-hmeo 22362 df-xms 22929 df-ms 22930 df-tms 22931

This theorem is referenced by: stoweidlem60 42344

W3C validator