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 41912

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 - \epslon / 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 3344	. . . . . . . . . 10 ⊢ Ⅎ𝑦{𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)}
3	1, 2	nfcxfr 2947	. . . . . . . . 9 ⊢ Ⅎ𝑦𝑌
4		nfcv 2949	. . . . . . . . 9 ⊢ Ⅎ𝑧𝑌
5		nfv 1892	. . . . . . . . 9 ⊢ Ⅎ𝑧(∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))
6		nfv 1892	. . . . . . . . 9 ⊢ Ⅎ𝑦(∀𝑡 ∈ (𝐷‘𝑗)(𝑧‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑧‘𝑡))
7		fveq1 6542	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝑦‘𝑡) = (𝑧‘𝑡))
8	7	breq1d 4976	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((𝑦‘𝑡) < (𝐸 / 𝑁) ↔ (𝑧‘𝑡) < (𝐸 / 𝑁)))
9	8	ralbidv 3164	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷‘𝑗)(𝑧‘𝑡) < (𝐸 / 𝑁)))
10	7	breq2d 4978	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (𝑧‘𝑡)))
11	10	ralbidv 3164	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑧‘𝑡)))
12	9, 11	anbi12d 630	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)) ↔ (∀𝑡 ∈ (𝐷‘𝑗)(𝑧‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑧‘𝑡))))
13	3, 4, 5, 6, 12	cbvrab 3433	. . . . . . . 8 ⊢ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} = {𝑧 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑧‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑧‘𝑡))}
14		ovexd 7055	. . . . . . . . . 10 ⊢ (𝜑 → (𝐽 Cn 𝐾) ∈ V)
15		stoweidlem59.11	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
16		stoweidlem59.5	. . . . . . . . . . 11 ⊢ 𝐶 = (𝐽 Cn 𝐾)
17	15, 16	syl6sseq 3942	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ⊆ (𝐽 Cn 𝐾))
18	14, 17	ssexd 5124	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ V)
19	1, 18	rabexd 5132	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ V)
20	13, 19	rabexd 5132	. . . . . . 7 ⊢ (𝜑 → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V)
21	20	ralrimivw 3150	. . . . . 6 ⊢ (𝜑 → ∀𝑗 ∈ (0...𝑁){𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V)
22		stoweidlem59.9	. . . . . . 7 ⊢ 𝐻 = (𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
23	22	fnmpt 6361	. . . . . 6 ⊢ (∀𝑗 ∈ (0...𝑁){𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V → 𝐻 Fn (0...𝑁))
24	21, 23	syl 17	. . . . 5 ⊢ (𝜑 → 𝐻 Fn (0...𝑁))
25		fzfi 13195	. . . . 5 ⊢ (0...𝑁) ∈ Fin
26		fnfi 8647	. . . . 5 ⊢ ((𝐻 Fn (0...𝑁) ∧ (0...𝑁) ∈ Fin) → 𝐻 ∈ Fin)
27	24, 25, 26	sylancl 586	. . . 4 ⊢ (𝜑 → 𝐻 ∈ Fin)
28		rnfi 8658	. . . 4 ⊢ (𝐻 ∈ Fin → ran 𝐻 ∈ Fin)
29	27, 28	syl 17	. . 3 ⊢ (𝜑 → ran 𝐻 ∈ Fin)
30		fnchoice 40850	. . 3 ⊢ (ran 𝐻 ∈ Fin → ∃ℎ(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)))
31	29, 30	syl 17	. 2 ⊢ (𝜑 → ∃ℎ(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)))
32		simprl 767	. . . . 5 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ℎ Fn ran 𝐻)
33		ovex 7053	. . . . . . . 8 ⊢ (0...𝑁) ∈ V
34	33	mptex 6857	. . . . . . 7 ⊢ (𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}) ∈ V
35	22, 34	eqeltri 2879	. . . . . 6 ⊢ 𝐻 ∈ V
36	35	rnex 7478	. . . . 5 ⊢ ran 𝐻 ∈ V
37		fnex 6851	. . . . 5 ⊢ ((ℎ Fn ran 𝐻 ∧ ran 𝐻 ∈ V) → ℎ ∈ V)
38	32, 36, 37	sylancl 586	. . . 4 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ℎ ∈ V)
39		coexg 7495	. . . 4 ⊢ ((ℎ ∈ V ∧ 𝐻 ∈ V) → (ℎ ∘ 𝐻) ∈ V)
40	38, 35, 39	sylancl 586	. . 3 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (ℎ ∘ 𝐻) ∈ V)
41		dffn3 6398	. . . . . . 7 ⊢ (ℎ Fn ran 𝐻 ↔ ℎ:ran 𝐻⟶ran ℎ)
42	32, 41	sylib 219	. . . . . 6 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ℎ:ran 𝐻⟶ran ℎ)
43		nfv 1892	. . . . . . . . . 10 ⊢ Ⅎ𝑤𝜑
44		nfv 1892	. . . . . . . . . . 11 ⊢ Ⅎ𝑤 ℎ Fn ran 𝐻
45		nfra1 3186	. . . . . . . . . . 11 ⊢ Ⅎ𝑤∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)
46	44, 45	nfan 1881	. . . . . . . . . 10 ⊢ Ⅎ𝑤(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))
47	43, 46	nfan 1881	. . . . . . . . 9 ⊢ Ⅎ𝑤(𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)))
48		simplrr 774	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))
49		simpr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → 𝑤 ∈ ran 𝐻)
50		fvelrnb 6599	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 Fn (0...𝑁) → (𝑤 ∈ ran 𝐻 ↔ ∃𝑎 ∈ (0...𝑁)(𝐻‘𝑎) = 𝑤))
51		nfv 1892	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑎(𝐻‘𝑗) = 𝑤
52		nfmpt1 5063	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑗(𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
53	22, 52	nfcxfr 2947	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗𝐻
54		nfcv 2949	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗𝑎
55	53, 54	nffv 6553	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗(𝐻‘𝑎)
56		nfcv 2949	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗𝑤
57	55, 56	nfeq 2960	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑗(𝐻‘𝑎) = 𝑤
58		fveq2 6543	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑎 → (𝐻‘𝑗) = (𝐻‘𝑎))
59	58	eqeq1d 2797	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑎 → ((𝐻‘𝑗) = 𝑤 ↔ (𝐻‘𝑎) = 𝑤))
60	51, 57, 59	cbvrex 3400	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤 ↔ ∃𝑎 ∈ (0...𝑁)(𝐻‘𝑎) = 𝑤)
61	50, 60	syl6bbr 290	. . . . . . . . . . . . . . 15 ⊢ (𝐻 Fn (0...𝑁) → (𝑤 ∈ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤))
62	24, 61	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑤 ∈ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤))
63	62	biimpa 477	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤)
64		simp3 1131	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ (𝐻‘𝑗) = 𝑤) → (𝐻‘𝑗) = 𝑤)
65		simpr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
66	20	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V)
67	22	fvmpt2 6650	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ (0...𝑁) ∧ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V) → (𝐻‘𝑗) = {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
68	65, 66, 67	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐻‘𝑗) = {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
69		stoweidlem59.6	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
70		nfcv 2949	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑡(0...𝑁)
71		nfrab1 3344	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑡{𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}
72	70, 71	nfmpt 5062	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
73	69, 72	nfcxfr 2947	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡𝐷
74		nfcv 2949	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡𝑗
75	73, 74	nffv 6553	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑡(𝐷‘𝑗)
76		nfcv 2949	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡𝑇
77		stoweidlem59.7	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
78		nfrab1 3344	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑡{𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}
79	70, 78	nfmpt 5062	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
80	77, 79	nfcxfr 2947	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑡𝐵
81	80, 74	nffv 6553	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡(𝐵‘𝑗)
82	76, 81	nfdif 4027	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑡(𝑇 ∖ (𝐵‘𝑗))
83		stoweidlem59.2	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡𝜑
84		nfv 1892	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡 𝑗 ∈ (0...𝑁)
85	83, 84	nfan 1881	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑗 ∈ (0...𝑁))
86		stoweidlem59.3	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐾 = (topGen‘ran (,))
87		stoweidlem59.4	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑇 = ∪ 𝐽
88		stoweidlem59.10	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐽 ∈ Comp)
89	88	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝐽 ∈ Comp)
90	15	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝐴 ⊆ 𝐶)
91		stoweidlem59.12	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)
92	91	3adant1r 1170	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)
93		stoweidlem59.13	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)
94	93	3adant1r 1170	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)
95		stoweidlem59.14	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑦) ∈ 𝐴)
96	95	adantlr 711	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑦) ∈ 𝐴)
97		stoweidlem59.15	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡))
98	97	adantlr 711	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡))
99		uniexg 7330	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐽 ∈ Comp → ∪ 𝐽 ∈ V)
100	88, 99	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ∪ 𝐽 ∈ V)
101	87, 100	syl5eqel 2887	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑇 ∈ V)
102	101	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑇 ∈ V)
103		rabexg 5130	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V)
104	102, 103	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V)
105	77	fvmpt2 6650	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑗 ∈ (0...𝑁) ∧ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V) → (𝐵‘𝑗) = {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
106	65, 104, 105	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐵‘𝑗) = {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
107		stoweidlem59.1	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑡𝐹
108		eqid 2795	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} = {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}
109		elfzelz 12763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
110	109	zred 11941	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
111		3re 11570	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 3 ∈ ℝ
112		3ne0 11596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 3 ≠ 0
113	111, 112	rereccli 11258	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (1 / 3) ∈ ℝ
114		readdcl 10471	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ) → (𝑗 + (1 / 3)) ∈ ℝ)
115	110, 113, 114	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + (1 / 3)) ∈ ℝ)
116	115	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑗 + (1 / 3)) ∈ ℝ)
117		stoweidlem59.17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
118	117	rpred 12286	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐸 ∈ ℝ)
119	118	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝐸 ∈ ℝ)
120	116, 119	remulcld 10522	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑗 + (1 / 3)) · 𝐸) ∈ ℝ)
121		stoweidlem59.16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐹 ∈ 𝐶)
122	121, 16	syl6eleq 2893	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))
123	122	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝐹 ∈ (𝐽 Cn 𝐾))
124	107, 86, 87, 108, 120, 123	rfcnpre3 40854	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ (Clsd‘𝐽))
125	106, 124	eqeltrd 2883	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐵‘𝑗) ∈ (Clsd‘𝐽))
126		rabexg 5130	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V)
127	102, 126	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V)
128	69	fvmpt2 6650	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑗 ∈ (0...𝑁) ∧ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V) → (𝐷‘𝑗) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
129	65, 127, 128	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐷‘𝑗) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
130		eqid 2795	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}
131		resubcl 10803	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ) → (𝑗 − (1 / 3)) ∈ ℝ)
132	110, 113, 131	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ (0...𝑁) → (𝑗 − (1 / 3)) ∈ ℝ)
133	132	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑗 − (1 / 3)) ∈ ℝ)
134	133, 119	remulcld 10522	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ)
135	107, 86, 87, 130, 134, 123	rfcnpre4 40855	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ (Clsd‘𝐽))
136	129, 135	eqeltrd 2883	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐷‘𝑗) ∈ (Clsd‘𝐽))
137	134	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ)
138	120	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ((𝑗 + (1 / 3)) · 𝐸) ∈ ℝ)
139	86, 87, 16, 121	fcnre 40846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 𝐹:𝑇⟶ℝ)
140	139	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → 𝐹:𝑇⟶ℝ)
141		ssrab2 3981	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ⊆ 𝑇
142	106, 141	syl6eqss 3946	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐵‘𝑗) ⊆ 𝑇)
143	142	sselda 3893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → 𝑡 ∈ 𝑇)
144	140, 143	ffvelrnd 6722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → (𝐹‘𝑡) ∈ ℝ)
145	113, 131	mpan2 687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) ∈ ℝ)
146		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑗 ∈ ℝ → 𝑗 ∈ ℝ)
147	113, 114	mpan2 687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑗 ∈ ℝ → (𝑗 + (1 / 3)) ∈ ℝ)
148		3pos 11595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ 0 < 3
149	111, 148	recgt0ii 11399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ 0 < (1 / 3)
150	113, 149	elrpii 12247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (1 / 3) ∈ ℝ⁺
151		ltsubrp 12280	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ⁺) → (𝑗 − (1 / 3)) < 𝑗)
152	150, 151	mpan2 687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) < 𝑗)
153		ltaddrp 12281	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ⁺) → 𝑗 < (𝑗 + (1 / 3)))
154	150, 153	mpan2 687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑗 ∈ ℝ → 𝑗 < (𝑗 + (1 / 3)))
155	145, 146, 147, 152, 154	lttrd 10653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
156	110, 155	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑗 ∈ (0...𝑁) → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
157	156	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
158	117	rpregt0d 12292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
159	158	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
160		ltmul1 11343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑗 − (1 / 3)) ∈ ℝ ∧ (𝑗 + (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑗 − (1 / 3)) < (𝑗 + (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸)))
161	133, 116, 159, 160	syl3anc 1364	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) < (𝑗 + (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸)))
162	157, 161	mpbid 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸))
163	162	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸))
164	106	eleq2d 2868	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑡 ∈ (𝐵‘𝑗) ↔ 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}))
165	164	biimpa 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
166		rabid 3337	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑡 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ↔ (𝑡 ∈ 𝑇 ∧ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)))
167	165, 166	sylib 219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → (𝑡 ∈ 𝑇 ∧ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)))
168	167	simprd 496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡))
169	137, 138, 144, 163, 168	ltletrd 10652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) < (𝐹‘𝑡))
170	137, 144	ltnled 10639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → (((𝑗 − (1 / 3)) · 𝐸) < (𝐹‘𝑡) ↔ ¬ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
171	169, 170	mpbid 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ¬ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))
172	171	intnand 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ¬ (𝑡 ∈ 𝑇 ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
173		rabid 3337	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ↔ (𝑡 ∈ 𝑇 ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
174	172, 173	sylnibr 330	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ¬ 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
175	129	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → (𝐷‘𝑗) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
176	174, 175	neleqtrrd 2905	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ¬ 𝑡 ∈ (𝐷‘𝑗))
177	176	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑡 ∈ (𝐵‘𝑗) → ¬ 𝑡 ∈ (𝐷‘𝑗)))
178	85, 177	ralrimi 3183	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐵‘𝑗) ¬ 𝑡 ∈ (𝐷‘𝑗))
179		disj 4317	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐵‘𝑗) ∩ (𝐷‘𝑗)) = ∅ ↔ ∀𝑎 ∈ (𝐵‘𝑗) ¬ 𝑎 ∈ (𝐷‘𝑗))
180		nfcv 2949	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑎(𝐵‘𝑗)
181	75	nfcri 2943	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑡 𝑎 ∈ (𝐷‘𝑗)
182	181	nfn 1838	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑡 ¬ 𝑎 ∈ (𝐷‘𝑗)
183		nfv 1892	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑎 ¬ 𝑡 ∈ (𝐷‘𝑗)
184		eleq1 2870	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = 𝑡 → (𝑎 ∈ (𝐷‘𝑗) ↔ 𝑡 ∈ (𝐷‘𝑗)))
185	184	notbid 319	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑡 → (¬ 𝑎 ∈ (𝐷‘𝑗) ↔ ¬ 𝑡 ∈ (𝐷‘𝑗)))
186	180, 81, 182, 183, 185	cbvralf 3397	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∀𝑎 ∈ (𝐵‘𝑗) ¬ 𝑎 ∈ (𝐷‘𝑗) ↔ ∀𝑡 ∈ (𝐵‘𝑗) ¬ 𝑡 ∈ (𝐷‘𝑗))
187	179, 186	bitri 276	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐵‘𝑗) ∩ (𝐷‘𝑗)) = ∅ ↔ ∀𝑡 ∈ (𝐵‘𝑗) ¬ 𝑡 ∈ (𝐷‘𝑗))
188	178, 187	sylibr 235	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝐵‘𝑗) ∩ (𝐷‘𝑗)) = ∅)
189		eqid 2795	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑇 ∖ (𝐵‘𝑗)) = (𝑇 ∖ (𝐵‘𝑗))
190		stoweidlem59.19	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑁 ∈ ℕ)
191	190	nnrpd 12284	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
192	117, 191	rpdivcld 12303	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℝ⁺)
193	192	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐸 / 𝑁) ∈ ℝ⁺)
194	118, 190	nndivred 11544	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℝ)
195	113	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (1 / 3) ∈ ℝ)
196	190	nnge1d 11538	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 1 ≤ 𝑁)
197		1re 10492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 1 ∈ ℝ
198		0lt1 11015	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 0 < 1
199	197, 198	pm3.2i 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (1 ∈ ℝ ∧ 0 < 1)
200	199	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (1 ∈ ℝ ∧ 0 < 1))
201	190	nnred 11506	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑁 ∈ ℝ)
202	190	nngt0d 11539	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 0 < 𝑁)
203		lediv2 11383	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((1 ∈ ℝ ∧ 0 < 1) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (1 ≤ 𝑁 ↔ (𝐸 / 𝑁) ≤ (𝐸 / 1)))
204	200, 201, 202, 158, 203	syl121anc 1368	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (1 ≤ 𝑁 ↔ (𝐸 / 𝑁) ≤ (𝐸 / 1)))
205	196, 204	mpbid 233	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐸 / 𝑁) ≤ (𝐸 / 1))
206	117	rpcnd 12288	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐸 ∈ ℂ)
207	206	div1d 11261	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐸 / 1) = 𝐸)
208	205, 207	breqtrd 4992	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐸 / 𝑁) ≤ 𝐸)
209		stoweidlem59.18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐸 < (1 / 3))
210	194, 118, 195, 208, 209	lelttrd 10650	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐸 / 𝑁) < (1 / 3))
211	210	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐸 / 𝑁) < (1 / 3))
212	75, 82, 85, 86, 87, 16, 89, 90, 92, 94, 96, 98, 125, 136, 188, 189, 193, 211	stoweidlem58 41911	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))
213		df-rex 3111	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))))
214	212, 213	sylib 219	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ∃𝑥(𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))))
215		simprl 767	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → 𝑥 ∈ 𝐴)
216		simprr1 1214	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1))
217		fveq1 6542	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 = 𝑥 → (𝑦‘𝑡) = (𝑥‘𝑡))
218	217	breq2d 4978	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 = 𝑥 → (0 ≤ (𝑦‘𝑡) ↔ 0 ≤ (𝑥‘𝑡)))
219	217	breq1d 4976	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 = 𝑥 → ((𝑦‘𝑡) ≤ 1 ↔ (𝑥‘𝑡) ≤ 1))
220	218, 219	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = 𝑥 → ((0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ↔ (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1)))
221	220	ralbidv 3164	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑥 → (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1)))
222	221, 1	elrab2 3622	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ 𝑌 ↔ (𝑥 ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1)))
223	215, 216, 222	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → 𝑥 ∈ 𝑌)
224		simprr2 1215	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁))
225		simprr3 1216	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))
226	224, 225	jca 512	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → (∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))
227		nfcv 2949	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑦𝑥
228		nfv 1892	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑦(∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))
229	217	breq1d 4976	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = 𝑥 → ((𝑦‘𝑡) < (𝐸 / 𝑁) ↔ (𝑥‘𝑡) < (𝐸 / 𝑁)))
230	229	ralbidv 3164	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑥 → (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁)))
231	217	breq2d 4978	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = 𝑥 → ((1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))
232	231	ralbidv 3164	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑥 → (∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))
233	230, 232	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑥 → ((∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)) ↔ (∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))))
234	227, 3, 228, 233	elrabf 3615	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ↔ (𝑥 ∈ 𝑌 ∧ (∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))))
235	223, 226, 234	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → 𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
236	235	ex 413	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))) → 𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}))
237	236	eximdv 1895	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (∃𝑥(𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))) → ∃𝑥 𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}))
238	214, 237	mpd 15	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ∃𝑥 𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
239		ne0i 4224	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ≠ ∅)
240	239	exlimiv 1908	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑥 𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ≠ ∅)
241	238, 240	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ≠ ∅)
242	68, 241	eqnetrd 3051	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐻‘𝑗) ≠ ∅)
243	242	3adant3 1125	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ (𝐻‘𝑗) = 𝑤) → (𝐻‘𝑗) ≠ ∅)
244	64, 243	eqnetrrd 3052	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ (𝐻‘𝑗) = 𝑤) → 𝑤 ≠ ∅)
245	244	3exp 1112	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ (0...𝑁) → ((𝐻‘𝑗) = 𝑤 → 𝑤 ≠ ∅)))
246	245	rexlimdv 3246	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤 → 𝑤 ≠ ∅))
247	246	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐻) → (∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤 → 𝑤 ≠ ∅))
248	63, 247	mpd 15	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐻) → 𝑤 ≠ ∅)
249	248	adantlr 711	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → 𝑤 ≠ ∅)
250		rsp 3172	. . . . . . . . . . 11 ⊢ (∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) → (𝑤 ∈ ran 𝐻 → (𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)))
251	48, 49, 249, 250	syl3c 66	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → (ℎ‘𝑤) ∈ 𝑤)
252	251	ex 413	. . . . . . . . 9 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (𝑤 ∈ ran 𝐻 → (ℎ‘𝑤) ∈ 𝑤))
253	47, 252	ralrimi 3183	. . . . . . . 8 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∀𝑤 ∈ ran 𝐻(ℎ‘𝑤) ∈ 𝑤)
254		chfnrn 6689	. . . . . . . 8 ⊢ ((ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(ℎ‘𝑤) ∈ 𝑤) → ran ℎ ⊆ ∪ ran 𝐻)
255	32, 253, 254	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ran ℎ ⊆ ∪ ran 𝐻)
256		nfv 1892	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝜑
257		nfcv 2949	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦ℎ
258		nfcv 2949	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦(0...𝑁)
259		nfrab1 3344	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦{𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}
260	258, 259	nfmpt 5062	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦(𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
261	22, 260	nfcxfr 2947	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦𝐻
262	261	nfrn 5711	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦ran 𝐻
263	257, 262	nffn 6327	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 ℎ Fn ran 𝐻
264		nfv 1892	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)
265	262, 264	nfral 3191	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)
266	263, 265	nfan 1881	. . . . . . . . . 10 ⊢ Ⅎ𝑦(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))
267	256, 266	nfan 1881	. . . . . . . . 9 ⊢ Ⅎ𝑦(𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)))
268	262	nfuni 4755	. . . . . . . . 9 ⊢ Ⅎ𝑦∪ ran 𝐻
269		fnunirn 6882	. . . . . . . . . . . . . . 15 ⊢ (𝐻 Fn (0...𝑁) → (𝑦 ∈ ∪ ran 𝐻 ↔ ∃𝑧 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑧)))
270		nfcv 2949	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗𝑧
271	53, 270	nffv 6553	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑗(𝐻‘𝑧)
272	271	nfcri 2943	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑗 𝑦 ∈ (𝐻‘𝑧)
273		nfv 1892	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧 𝑦 ∈ (𝐻‘𝑗)
274		fveq2 6543	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑗 → (𝐻‘𝑧) = (𝐻‘𝑗))
275	274	eleq2d 2868	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑗 → (𝑦 ∈ (𝐻‘𝑧) ↔ 𝑦 ∈ (𝐻‘𝑗)))
276	272, 273, 275	cbvrex 3400	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑧) ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑗))
277	269, 276	syl6bb 288	. . . . . . . . . . . . . 14 ⊢ (𝐻 Fn (0...𝑁) → (𝑦 ∈ ∪ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑗)))
278	24, 277	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑦 ∈ ∪ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑗)))
279	278	biimpa 477	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) → ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑗))
280		nfv 1892	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗𝜑
281	53	nfrn 5711	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑗ran 𝐻
282	281	nfuni 4755	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑗∪ ran 𝐻
283	282	nfcri 2943	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗 𝑦 ∈ ∪ ran 𝐻
284	280, 283	nfan 1881	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻)
285		nfv 1892	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗 𝑦 ∈ 𝑌
286		simp1l 1190	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝜑)
287		simp2 1130	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑗 ∈ (0...𝑁))
288		simp3 1131	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ (𝐻‘𝑗))
289	68	eleq2d 2868	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑦 ∈ (𝐻‘𝑗) ↔ 𝑦 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}))
290	289	biimpa 477	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
291		rabid 3337	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ↔ (𝑦 ∈ 𝑌 ∧ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))))
292	290, 291	sylib 219	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → (𝑦 ∈ 𝑌 ∧ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))))
293	292	simpld 495	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ 𝑌)
294	286, 287, 288, 293	syl21anc 834	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ 𝑌)
295	294	3exp 1112	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) → (𝑗 ∈ (0...𝑁) → (𝑦 ∈ (𝐻‘𝑗) → 𝑦 ∈ 𝑌)))
296	284, 285, 295	rexlimd 3278	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) → (∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑗) → 𝑦 ∈ 𝑌))
297	279, 296	mpd 15	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) → 𝑦 ∈ 𝑌)
298	297	adantlr 711	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑦 ∈ ∪ ran 𝐻) → 𝑦 ∈ 𝑌)
299	298	ex 413	. . . . . . . . 9 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (𝑦 ∈ ∪ ran 𝐻 → 𝑦 ∈ 𝑌))
300	267, 268, 3, 299	ssrd 3898	. . . . . . . 8 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∪ ran 𝐻 ⊆ 𝑌)
301		ssrab2 3981	. . . . . . . . 9 ⊢ {𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)} ⊆ 𝐴
302	1, 301	eqsstri 3926	. . . . . . . 8 ⊢ 𝑌 ⊆ 𝐴
303	300, 302	syl6ss 3905	. . . . . . 7 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∪ ran 𝐻 ⊆ 𝐴)
304	255, 303	sstrd 3903	. . . . . 6 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ran ℎ ⊆ 𝐴)
305	42, 304	fssd 6401	. . . . 5 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ℎ:ran 𝐻⟶𝐴)
306		dffn3 6398	. . . . . . 7 ⊢ (𝐻 Fn (0...𝑁) ↔ 𝐻:(0...𝑁)⟶ran 𝐻)
307	24, 306	sylib 219	. . . . . 6 ⊢ (𝜑 → 𝐻:(0...𝑁)⟶ran 𝐻)
308	307	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → 𝐻:(0...𝑁)⟶ran 𝐻)
309		fco 6404	. . . . 5 ⊢ ((ℎ:ran 𝐻⟶𝐴 ∧ 𝐻:(0...𝑁)⟶ran 𝐻) → (ℎ ∘ 𝐻):(0...𝑁)⟶𝐴)
310	305, 308, 309	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (ℎ ∘ 𝐻):(0...𝑁)⟶𝐴)
311		nfcv 2949	. . . . . . . 8 ⊢ Ⅎ𝑗ℎ
312	311, 281	nffn 6327	. . . . . . 7 ⊢ Ⅎ𝑗 ℎ Fn ran 𝐻
313		nfv 1892	. . . . . . . 8 ⊢ Ⅎ𝑗(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)
314	281, 313	nfral 3191	. . . . . . 7 ⊢ Ⅎ𝑗∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)
315	312, 314	nfan 1881	. . . . . 6 ⊢ Ⅎ𝑗(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))
316	280, 315	nfan 1881	. . . . 5 ⊢ Ⅎ𝑗(𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)))
317		simpll 763	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝜑)
318		simpr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
319	24	ad2antrr 722	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝐻 Fn (0...𝑁))
320		fvco2 6630	. . . . . . . . . . . 12 ⊢ ((𝐻 Fn (0...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → ((ℎ ∘ 𝐻)‘𝑗) = (ℎ‘(𝐻‘𝑗)))
321	319, 320	sylancom 588	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((ℎ ∘ 𝐻)‘𝑗) = (ℎ‘(𝐻‘𝑗)))
322		simplrr 774	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))
323		fnfun 6328	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 Fn (0...𝑁) → Fun 𝐻)
324	24, 323	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Fun 𝐻)
325	324	ad2antrr 722	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → Fun 𝐻)
326		fndm 6330	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐻 Fn (0...𝑁) → dom 𝐻 = (0...𝑁))
327	24, 326	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom 𝐻 = (0...𝑁))
328	327	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → dom 𝐻 = (0...𝑁))
329	65, 328	eleqtrrd 2886	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ dom 𝐻)
330	329	adantlr 711	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ dom 𝐻)
331		fvelrn 6714	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐻 ∧ 𝑗 ∈ dom 𝐻) → (𝐻‘𝑗) ∈ ran 𝐻)
332	325, 330, 331	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (𝐻‘𝑗) ∈ ran 𝐻)
333	322, 332	jca 512	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) ∧ (𝐻‘𝑗) ∈ ran 𝐻))
334	242	adantlr 711	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (𝐻‘𝑗) ≠ ∅)
335		neeq1 3046	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝐻‘𝑗) → (𝑤 ≠ ∅ ↔ (𝐻‘𝑗) ≠ ∅))
336		fveq2 6543	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝐻‘𝑗) → (ℎ‘𝑤) = (ℎ‘(𝐻‘𝑗)))
337		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝐻‘𝑗) → 𝑤 = (𝐻‘𝑗))
338	336, 337	eleq12d 2877	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝐻‘𝑗) → ((ℎ‘𝑤) ∈ 𝑤 ↔ (ℎ‘(𝐻‘𝑗)) ∈ (𝐻‘𝑗)))
339	335, 338	imbi12d 346	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝐻‘𝑗) → ((𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) ↔ ((𝐻‘𝑗) ≠ ∅ → (ℎ‘(𝐻‘𝑗)) ∈ (𝐻‘𝑗))))
340	339	rspccva 3558	. . . . . . . . . . . 12 ⊢ ((∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) ∧ (𝐻‘𝑗) ∈ ran 𝐻) → ((𝐻‘𝑗) ≠ ∅ → (ℎ‘(𝐻‘𝑗)) ∈ (𝐻‘𝑗)))
341	333, 334, 340	sylc 65	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (ℎ‘(𝐻‘𝑗)) ∈ (𝐻‘𝑗))
342	321, 341	eqeltrd 2883	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗))
343	257, 261	nfco 5627	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(ℎ ∘ 𝐻)
344		nfcv 2949	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦𝑗
345	343, 344	nffv 6553	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦((ℎ ∘ 𝐻)‘𝑗)
346		nfv 1892	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑗 ∈ (0...𝑁))
347	261, 344	nffv 6553	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦(𝐻‘𝑗)
348	345, 347	nfel 2961	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)
349	346, 348	nfan 1881	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗))
350	345, 3	nfel 2961	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌
351	349, 350	nfim 1878	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌)
352		eleq1 2870	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (𝑦 ∈ (𝐻‘𝑗) ↔ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)))
353	352	anbi2d 628	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) ↔ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗))))
354		eleq1 2870	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (𝑦 ∈ 𝑌 ↔ ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌))
355	353, 354	imbi12d 346	. . . . . . . . . . . 12 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ 𝑌) ↔ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌)))
356	345, 351, 355, 293	vtoclgf 3508	. . . . . . . . . . 11 ⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗) → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌))
357	356	anabsi7 667	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌)
358	317, 318, 342, 357	syl21anc 834	. . . . . . . . 9 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌)
359	1	eleq2i 2874	. . . . . . . . . 10 ⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌 ↔ ((ℎ ∘ 𝐻)‘𝑗) ∈ {𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)})
360		nfcv 2949	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝐴
361		nfcv 2949	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦𝑇
362		nfcv 2949	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦0
363		nfcv 2949	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦 ≤
364		nfcv 2949	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦𝑡
365	345, 364	nffv 6553	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦(((ℎ ∘ 𝐻)‘𝑗)‘𝑡)
366	362, 363, 365	nfbr 5013	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)
367		nfcv 2949	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦1
368	365, 363, 367	nfbr 5013	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1
369	366, 368	nfan 1881	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)
370	361, 369	nfral 3191	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)
371		nfcv 2949	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡𝑦
372		nfcv 2949	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡ℎ
373		nfra1 3186	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁)
374		nfra1 3186	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)
375	373, 374	nfan 1881	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡(∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))
376		nfra1 3186	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)
377		nfcv 2949	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡𝐴
378	376, 377	nfrab 3345	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡{𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)}
379	1, 378	nfcxfr 2947	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡𝑌
380	375, 379	nfrab 3345	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡{𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}
381	70, 380	nfmpt 5062	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
382	22, 381	nfcxfr 2947	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡𝐻
383	372, 382	nfco 5627	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡(ℎ ∘ 𝐻)
384	383, 74	nffv 6553	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((ℎ ∘ 𝐻)‘𝑗)
385	371, 384	nfeq 2960	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡 𝑦 = ((ℎ ∘ 𝐻)‘𝑗)
386		fveq1 6542	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (𝑦‘𝑡) = (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))
387	386	breq2d 4978	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (0 ≤ (𝑦‘𝑡) ↔ 0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
388	386	breq1d 4976	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((𝑦‘𝑡) ≤ 1 ↔ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1))
389	387, 388	anbi12d 630	. . . . . . . . . . . 12 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ↔ (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
390	385, 389	ralbid 3195	. . . . . . . . . . 11 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
391	345, 360, 370, 390	elrabf 3615	. . . . . . . . . 10 ⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ {𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)} ↔ (((ℎ ∘ 𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
392	359, 391	bitri 276	. . . . . . . . 9 ⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌 ↔ (((ℎ ∘ 𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
393	358, 392	sylib 219	. . . . . . . 8 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (((ℎ ∘ 𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
394	393	simprd 496	. . . . . . 7 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1))
395		nfcv 2949	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝐷‘𝑗)
396		nfcv 2949	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦 <
397		nfcv 2949	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝐸 / 𝑁)
398	365, 396, 397	nfbr 5013	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)
399	395, 398	nfral 3191	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)
400	349, 399	nfim 1878	. . . . . . . . . 10 ⊢ Ⅎ𝑦(((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))
401	386	breq1d 4976	. . . . . . . . . . . 12 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((𝑦‘𝑡) < (𝐸 / 𝑁) ↔ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
402	385, 401	ralbid 3195	. . . . . . . . . . 11 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
403	353, 402	imbi12d 346	. . . . . . . . . 10 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁)) ↔ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))))
404	292	simprd 496	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)))
405	404	simpld 495	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁))
406	345, 400, 403, 405	vtoclgf 3508	. . . . . . . . 9 ⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗) → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
407	406	anabsi7 667	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))
408	317, 318, 342, 407	syl21anc 834	. . . . . . 7 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))
409		nfcv 2949	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝐵‘𝑗)
410		nfcv 2949	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(1 − (𝐸 / 𝑁))
411	410, 396, 365	nfbr 5013	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)
412	409, 411	nfral 3191	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)
413	349, 412	nfim 1878	. . . . . . . . . 10 ⊢ Ⅎ𝑦(((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))
414	386	breq2d 4978	. . . . . . . . . . . 12 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
415	385, 414	ralbid 3195	. . . . . . . . . . 11 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
416	353, 415	imbi12d 346	. . . . . . . . . 10 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)) ↔ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))))
417	404	simprd 496	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))
418	345, 413, 416, 417	vtoclgf 3508	. . . . . . . . 9 ⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗) → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
419	418	anabsi7 667	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))
420	317, 318, 342, 419	syl21anc 834	. . . . . . 7 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))
421	394, 408, 420	3jca 1121	. . . . . 6 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
422	421	ex 413	. . . . 5 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (𝑗 ∈ (0...𝑁) → (∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))))
423	316, 422	ralrimi 3183	. . . 4 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
424	310, 423	jca 512	. . 3 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ((ℎ ∘ 𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))))
425		feq1 6368	. . . . 5 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (𝑥:(0...𝑁)⟶𝐴 ↔ (ℎ ∘ 𝐻):(0...𝑁)⟶𝐴))
426		nfcv 2949	. . . . . . 7 ⊢ Ⅎ𝑗𝑥
427	311, 53	nfco 5627	. . . . . . 7 ⊢ Ⅎ𝑗(ℎ ∘ 𝐻)
428	426, 427	nfeq 2960	. . . . . 6 ⊢ Ⅎ𝑗 𝑥 = (ℎ ∘ 𝐻)
429		nfcv 2949	. . . . . . . . 9 ⊢ Ⅎ𝑡𝑥
430	429, 383	nfeq 2960	. . . . . . . 8 ⊢ Ⅎ𝑡 𝑥 = (ℎ ∘ 𝐻)
431		fveq1 6542	. . . . . . . . . . 11 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (𝑥‘𝑗) = ((ℎ ∘ 𝐻)‘𝑗))
432	431	fveq1d 6545	. . . . . . . . . 10 ⊢ (𝑥 = (ℎ ∘ 𝐻) → ((𝑥‘𝑗)‘𝑡) = (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))
433	432	breq2d 4978	. . . . . . . . 9 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (0 ≤ ((𝑥‘𝑗)‘𝑡) ↔ 0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
434	432	breq1d 4976	. . . . . . . . 9 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (((𝑥‘𝑗)‘𝑡) ≤ 1 ↔ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1))
435	433, 434	anbi12d 630	. . . . . . . 8 ⊢ (𝑥 = (ℎ ∘ 𝐻) → ((0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ↔ (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
436	430, 435	ralbid 3195	. . . . . . 7 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
437	432	breq1d 4976	. . . . . . . 8 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
438	430, 437	ralbid 3195	. . . . . . 7 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
439	432	breq2d 4978	. . . . . . . 8 ⊢ (𝑥 = (ℎ ∘ 𝐻) → ((1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
440	430, 439	ralbid 3195	. . . . . . 7 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡) ↔ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
441	436, 438, 440	3anbi123d 1428	. . . . . 6 ⊢ (𝑥 = (ℎ ∘ 𝐻) → ((∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))))
442	428, 441	ralbid 3195	. . . . 5 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡)) ↔ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))))
443	425, 442	anbi12d 630	. . . 4 ⊢ (𝑥 = (ℎ ∘ 𝐻) → ((𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡))) ↔ ((ℎ ∘ 𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))))
444	443	spcegv 3540	. . 3 ⊢ ((ℎ ∘ 𝐻) ∈ V → (((ℎ ∘ 𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))) → ∃𝑥(𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡)))))
445	40, 424, 444	sylc 65	. 2 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∃𝑥(𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡))))
446	31, 445	exlimddv 1913	1 ⊢ (𝜑 → ∃𝑥(𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∧ w3a 1080 = wceq 1522 ∃wex 1761 Ⅎwnf 1765 ∈ wcel 2081 Ⅎwnfc 2933 ≠ wne 2984 ∀wral 3105 ∃wrex 3106 {crab 3109 Vcvv 3437 ∖ cdif 3860 ∩ cin 3862 ⊆ wss 3863 ∅c0 4215 ∪ cuni 4749 class class class wbr 4966 ↦ cmpt 5045 dom cdm 5448 ran crn 5449 ∘ ccom 5452 Fun wfun 6224 Fn wfn 6225 ⟶wf 6226 ‘cfv 6230 (class class class)co 7021 Fincfn 8362 ℝcr 10387 0cc0 10388 1c1 10389 + caddc 10391 · cmul 10393 < clt 10526 ≤ cle 10527 − cmin 10722 / cdiv 11150 ℕcn 11491 3c3 11546 ℝ⁺crp 12244 (,)cioo 12593 ...cfz 12747 topGenctg 16545 Clsdccld 21313 Cn ccn 21521 Compccmp 21683

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-rep 5086 ax-sep 5099 ax-nul 5106 ax-pow 5162 ax-pr 5226 ax-un 7324 ax-inf2 8955 ax-cnex 10444 ax-resscn 10445 ax-1cn 10446 ax-icn 10447 ax-addcl 10448 ax-addrcl 10449 ax-mulcl 10450 ax-mulrcl 10451 ax-mulcom 10452 ax-addass 10453 ax-mulass 10454 ax-distr 10455 ax-i2m1 10456 ax-1ne0 10457 ax-1rid 10458 ax-rnegex 10459 ax-rrecex 10460 ax-cnre 10461 ax-pre-lttri 10462 ax-pre-lttrn 10463 ax-pre-ltadd 10464 ax-pre-mulgt0 10465 ax-pre-sup 10466 ax-mulf 10468

This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-fal 1535 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-nel 3091 df-ral 3110 df-rex 3111 df-reu 3112 df-rmo 3113 df-rab 3114 df-v 3439 df-sbc 3710 df-csb 3816 df-dif 3866 df-un 3868 df-in 3870 df-ss 3878 df-pss 3880 df-nul 4216 df-if 4386 df-pw 4459 df-sn 4477 df-pr 4479 df-tp 4481 df-op 4483 df-uni 4750 df-int 4787 df-iun 4831 df-iin 4832 df-br 4967 df-opab 5029 df-mpt 5046 df-tr 5069 df-id 5353 df-eprel 5358 df-po 5367 df-so 5368 df-fr 5407 df-se 5408 df-we 5409 df-xp 5454 df-rel 5455 df-cnv 5456 df-co 5457 df-dm 5458 df-rn 5459 df-res 5460 df-ima 5461 df-pred 6028 df-ord 6074 df-on 6075 df-lim 6076 df-suc 6077 df-iota 6194 df-fun 6232 df-fn 6233 df-f 6234 df-f1 6235 df-fo 6236 df-f1o 6237 df-fv 6238 df-isom 6239 df-riota 6982 df-ov 7024 df-oprab 7025 df-mpo 7026 df-of 7272 df-om 7442 df-1st 7550 df-2nd 7551 df-supp 7687 df-wrecs 7803 df-recs 7865 df-rdg 7903 df-1o 7958 df-2o 7959 df-oadd 7962 df-er 8144 df-map 8263 df-pm 8264 df-ixp 8316 df-en 8363 df-dom 8364 df-sdom 8365 df-fin 8366 df-fsupp 8685 df-fi 8726 df-sup 8757 df-inf 8758 df-oi 8825 df-card 9219 df-pnf 10528 df-mnf 10529 df-xr 10530 df-ltxr 10531 df-le 10532 df-sub 10724 df-neg 10725 df-div 11151 df-nn 11492 df-2 11553 df-3 11554 df-4 11555 df-5 11556 df-6 11557 df-7 11558 df-8 11559 df-9 11560 df-n0 11751 df-z 11835 df-dec 11953 df-uz 12099 df-q 12203 df-rp 12245 df-xneg 12362 df-xadd 12363 df-xmul 12364 df-ioo 12597 df-ioc 12598 df-ico 12599 df-icc 12600 df-fz 12748 df-fzo 12889 df-fl 13017 df-seq 13225 df-exp 13285 df-hash 13546 df-cj 14297 df-re 14298 df-im 14299 df-sqrt 14433 df-abs 14434 df-clim 14684 df-rlim 14685 df-sum 14882 df-struct 16319 df-ndx 16320 df-slot 16321 df-base 16323 df-sets 16324 df-ress 16325 df-plusg 16412 df-mulr 16413 df-starv 16414 df-sca 16415 df-vsca 16416 df-ip 16417 df-tset 16418 df-ple 16419 df-ds 16421 df-unif 16422 df-hom 16423 df-cco 16424 df-rest 16530 df-topn 16531 df-0g 16549 df-gsum 16550 df-topgen 16551 df-pt 16552 df-prds 16555 df-xrs 16609 df-qtop 16614 df-imas 16615 df-xps 16617 df-mre 16691 df-mrc 16692 df-acs 16694 df-mgm 17686 df-sgrp 17728 df-mnd 17739 df-submnd 17780 df-mulg 17987 df-cntz 18193 df-cmn 18640 df-psmet 20224 df-xmet 20225 df-met 20226 df-bl 20227 df-mopn 20228 df-cnfld 20233 df-top 21191 df-topon 21208 df-topsp 21230 df-bases 21243 df-cld 21316 df-cn 21524 df-cnp 21525 df-cmp 21684 df-tx 21859 df-hmeo 22052 df-xms 22618 df-ms 22619 df-tms 22620

This theorem is referenced by: stoweidlem60 41913

W3C validator