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 46057

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 3426	. . . . . . . . . 10 ⊢ Ⅎ𝑦{𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)}
3	1, 2	nfcxfr 2889	. . . . . . . . 9 ⊢ Ⅎ𝑦𝑌
4		nfcv 2891	. . . . . . . . 9 ⊢ Ⅎ𝑧𝑌
5		nfv 1914	. . . . . . . . 9 ⊢ Ⅎ𝑧(∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))
6		nfv 1914	. . . . . . . . 9 ⊢ Ⅎ𝑦(∀𝑡 ∈ (𝐷‘𝑗)(𝑧‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑧‘𝑡))
7		fveq1 6857	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝑦‘𝑡) = (𝑧‘𝑡))
8	7	breq1d 5117	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((𝑦‘𝑡) < (𝐸 / 𝑁) ↔ (𝑧‘𝑡) < (𝐸 / 𝑁)))
9	8	ralbidv 3156	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷‘𝑗)(𝑧‘𝑡) < (𝐸 / 𝑁)))
10	7	breq2d 5119	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (𝑧‘𝑡)))
11	10	ralbidv 3156	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑧‘𝑡)))
12	9, 11	anbi12d 632	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)) ↔ (∀𝑡 ∈ (𝐷‘𝑗)(𝑧‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑧‘𝑡))))
13	3, 4, 5, 6, 12	cbvrabw 3441	. . . . . . . 8 ⊢ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} = {𝑧 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑧‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑧‘𝑡))}
14		ovexd 7422	. . . . . . . . . 10 ⊢ (𝜑 → (𝐽 Cn 𝐾) ∈ V)
15		stoweidlem59.11	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
16		stoweidlem59.5	. . . . . . . . . . 11 ⊢ 𝐶 = (𝐽 Cn 𝐾)
17	15, 16	sseqtrdi 3987	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ⊆ (𝐽 Cn 𝐾))
18	14, 17	ssexd 5279	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ V)
19	1, 18	rabexd 5295	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ V)
20	13, 19	rabexd 5295	. . . . . . 7 ⊢ (𝜑 → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V)
21	20	ralrimivw 3129	. . . . . 6 ⊢ (𝜑 → ∀𝑗 ∈ (0...𝑁){𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V)
22		stoweidlem59.9	. . . . . . 7 ⊢ 𝐻 = (𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
23	22	fnmpt 6658	. . . . . 6 ⊢ (∀𝑗 ∈ (0...𝑁){𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V → 𝐻 Fn (0...𝑁))
24	21, 23	syl 17	. . . . 5 ⊢ (𝜑 → 𝐻 Fn (0...𝑁))
25		fzfi 13937	. . . . 5 ⊢ (0...𝑁) ∈ Fin
26		fnfi 9142	. . . . 5 ⊢ ((𝐻 Fn (0...𝑁) ∧ (0...𝑁) ∈ Fin) → 𝐻 ∈ Fin)
27	24, 25, 26	sylancl 586	. . . 4 ⊢ (𝜑 → 𝐻 ∈ Fin)
28		rnfi 9291	. . . 4 ⊢ (𝐻 ∈ Fin → ran 𝐻 ∈ Fin)
29	27, 28	syl 17	. . 3 ⊢ (𝜑 → ran 𝐻 ∈ Fin)
30		fnchoice 45023	. . 3 ⊢ (ran 𝐻 ∈ Fin → ∃ℎ(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)))
31	29, 30	syl 17	. 2 ⊢ (𝜑 → ∃ℎ(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)))
32		simprl 770	. . . . 5 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ℎ Fn ran 𝐻)
33		ovex 7420	. . . . . . . 8 ⊢ (0...𝑁) ∈ V
34	33	mptex 7197	. . . . . . 7 ⊢ (𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}) ∈ V
35	22, 34	eqeltri 2824	. . . . . 6 ⊢ 𝐻 ∈ V
36	35	rnex 7886	. . . . 5 ⊢ ran 𝐻 ∈ V
37		fnex 7191	. . . . 5 ⊢ ((ℎ Fn ran 𝐻 ∧ ran 𝐻 ∈ V) → ℎ ∈ V)
38	32, 36, 37	sylancl 586	. . . 4 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ℎ ∈ V)
39		coexg 7905	. . . 4 ⊢ ((ℎ ∈ V ∧ 𝐻 ∈ V) → (ℎ ∘ 𝐻) ∈ V)
40	38, 35, 39	sylancl 586	. . 3 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (ℎ ∘ 𝐻) ∈ V)
41		dffn3 6700	. . . . . . 7 ⊢ (ℎ Fn ran 𝐻 ↔ ℎ:ran 𝐻⟶ran ℎ)
42	32, 41	sylib 218	. . . . . 6 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ℎ:ran 𝐻⟶ran ℎ)
43		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑤𝜑
44		nfv 1914	. . . . . . . . . . 11 ⊢ Ⅎ𝑤 ℎ Fn ran 𝐻
45		nfra1 3261	. . . . . . . . . . 11 ⊢ Ⅎ𝑤∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)
46	44, 45	nfan 1899	. . . . . . . . . 10 ⊢ Ⅎ𝑤(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))
47	43, 46	nfan 1899	. . . . . . . . 9 ⊢ Ⅎ𝑤(𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)))
48		simplrr 777	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))
49		simpr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → 𝑤 ∈ ran 𝐻)
50		fvelrnb 6921	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 Fn (0...𝑁) → (𝑤 ∈ ran 𝐻 ↔ ∃𝑎 ∈ (0...𝑁)(𝐻‘𝑎) = 𝑤))
51		nfv 1914	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑎(𝐻‘𝑗) = 𝑤
52		nfmpt1 5206	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑗(𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
53	22, 52	nfcxfr 2889	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗𝐻
54		nfcv 2891	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗𝑎
55	53, 54	nffv 6868	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗(𝐻‘𝑎)
56		nfcv 2891	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗𝑤
57	55, 56	nfeq 2905	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑗(𝐻‘𝑎) = 𝑤
58		fveq2 6858	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑎 → (𝐻‘𝑗) = (𝐻‘𝑎))
59	58	eqeq1d 2731	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑎 → ((𝐻‘𝑗) = 𝑤 ↔ (𝐻‘𝑎) = 𝑤))
60	51, 57, 59	cbvrexw 3281	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤 ↔ ∃𝑎 ∈ (0...𝑁)(𝐻‘𝑎) = 𝑤)
61	50, 60	bitr4di 289	. . . . . . . . . . . . . . 15 ⊢ (𝐻 Fn (0...𝑁) → (𝑤 ∈ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤))
62	24, 61	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑤 ∈ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤))
63	62	biimpa 476	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤)
64		simp3 1138	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ (𝐻‘𝑗) = 𝑤) → (𝐻‘𝑗) = 𝑤)
65		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
66	20	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V)
67	22	fvmpt2 6979	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ (0...𝑁) ∧ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V) → (𝐻‘𝑗) = {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
68	65, 66, 67	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐻‘𝑗) = {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
69		stoweidlem59.6	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
70		nfcv 2891	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑡(0...𝑁)
71		nfrab1 3426	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑡{𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}
72	70, 71	nfmpt 5205	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
73	69, 72	nfcxfr 2889	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡𝐷
74		nfcv 2891	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡𝑗
75	73, 74	nffv 6868	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑡(𝐷‘𝑗)
76		nfcv 2891	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡𝑇
77		stoweidlem59.7	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
78		nfrab1 3426	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑡{𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}
79	70, 78	nfmpt 5205	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
80	77, 79	nfcxfr 2889	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑡𝐵
81	80, 74	nffv 6868	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡(𝐵‘𝑗)
82	76, 81	nfdif 4092	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑡(𝑇 ∖ (𝐵‘𝑗))
83		stoweidlem59.2	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡𝜑
84		nfv 1914	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡 𝑗 ∈ (0...𝑁)
85	83, 84	nfan 1899	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑗 ∈ (0...𝑁))
86		stoweidlem59.3	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐾 = (topGen‘ran (,))
87		stoweidlem59.4	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑇 = ∪ 𝐽
88		stoweidlem59.10	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐽 ∈ Comp)
89	88	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝐽 ∈ Comp)
90	15	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝐴 ⊆ 𝐶)
91		stoweidlem59.12	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)
92	91	3adant1r 1178	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)
93		stoweidlem59.13	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)
94	93	3adant1r 1178	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)
95		stoweidlem59.14	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑦) ∈ 𝐴)
96	95	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑦) ∈ 𝐴)
97		stoweidlem59.15	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡))
98	97	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡))
99	88	uniexd 7718	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ∪ 𝐽 ∈ V)
100	87, 99	eqeltrid 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑇 ∈ V)
101	100	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑇 ∈ V)
102		rabexg 5292	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V)
103	101, 102	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V)
104	77	fvmpt2 6979	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑗 ∈ (0...𝑁) ∧ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V) → (𝐵‘𝑗) = {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
105	65, 103, 104	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐵‘𝑗) = {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
106		stoweidlem59.1	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑡𝐹
107		eqid 2729	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} = {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}
108		elfzelz 13485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
109	108	zred 12638	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
110		3re 12266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 3 ∈ ℝ
111		3ne0 12292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 3 ≠ 0
112	110, 111	rereccli 11947	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (1 / 3) ∈ ℝ
113		readdcl 11151	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ) → (𝑗 + (1 / 3)) ∈ ℝ)
114	109, 112, 113	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + (1 / 3)) ∈ ℝ)
115	114	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑗 + (1 / 3)) ∈ ℝ)
116		stoweidlem59.17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
117	116	rpred 12995	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐸 ∈ ℝ)
118	117	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝐸 ∈ ℝ)
119	115, 118	remulcld 11204	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑗 + (1 / 3)) · 𝐸) ∈ ℝ)
120		stoweidlem59.16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐹 ∈ 𝐶)
121	120, 16	eleqtrdi 2838	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))
122	121	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝐹 ∈ (𝐽 Cn 𝐾))
123	106, 86, 87, 107, 119, 122	rfcnpre3 45027	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ (Clsd‘𝐽))
124	105, 123	eqeltrd 2828	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐵‘𝑗) ∈ (Clsd‘𝐽))
125		rabexg 5292	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V)
126	101, 125	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V)
127	69	fvmpt2 6979	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑗 ∈ (0...𝑁) ∧ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V) → (𝐷‘𝑗) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
128	65, 126, 127	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐷‘𝑗) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
129		eqid 2729	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}
130		resubcl 11486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ) → (𝑗 − (1 / 3)) ∈ ℝ)
131	109, 112, 130	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ (0...𝑁) → (𝑗 − (1 / 3)) ∈ ℝ)
132	131	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑗 − (1 / 3)) ∈ ℝ)
133	132, 118	remulcld 11204	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ)
134	106, 86, 87, 129, 133, 122	rfcnpre4 45028	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ (Clsd‘𝐽))
135	128, 134	eqeltrd 2828	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐷‘𝑗) ∈ (Clsd‘𝐽))
136	133	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ)
137	119	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ((𝑗 + (1 / 3)) · 𝐸) ∈ ℝ)
138	86, 87, 16, 120	fcnre 45019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 𝐹:𝑇⟶ℝ)
139	138	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → 𝐹:𝑇⟶ℝ)
140		ssrab2 4043	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ⊆ 𝑇
141	105, 140	eqsstrdi 3991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐵‘𝑗) ⊆ 𝑇)
142	141	sselda 3946	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → 𝑡 ∈ 𝑇)
143	139, 142	ffvelcdmd 7057	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → (𝐹‘𝑡) ∈ ℝ)
144	112, 130	mpan2 691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) ∈ ℝ)
145		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑗 ∈ ℝ → 𝑗 ∈ ℝ)
146	112, 113	mpan2 691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑗 ∈ ℝ → (𝑗 + (1 / 3)) ∈ ℝ)
147		3pos 12291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ 0 < 3
148	110, 147	recgt0ii 12089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ 0 < (1 / 3)
149	112, 148	elrpii 12954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (1 / 3) ∈ ℝ⁺
150		ltsubrp 12989	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ⁺) → (𝑗 − (1 / 3)) < 𝑗)
151	149, 150	mpan2 691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) < 𝑗)
152		ltaddrp 12990	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ⁺) → 𝑗 < (𝑗 + (1 / 3)))
153	149, 152	mpan2 691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑗 ∈ ℝ → 𝑗 < (𝑗 + (1 / 3)))
154	144, 145, 146, 151, 153	lttrd 11335	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
155	109, 154	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑗 ∈ (0...𝑁) → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
156	155	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
157	116	rpregt0d 13001	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
158	157	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
159		ltmul1 12032	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑗 − (1 / 3)) ∈ ℝ ∧ (𝑗 + (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑗 − (1 / 3)) < (𝑗 + (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸)))
160	132, 115, 158, 159	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) < (𝑗 + (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸)))
161	156, 160	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸))
162	161	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸))
163	105	eleq2d 2814	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑡 ∈ (𝐵‘𝑗) ↔ 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}))
164	163	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
165		rabid 3427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑡 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ↔ (𝑡 ∈ 𝑇 ∧ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)))
166	164, 165	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → (𝑡 ∈ 𝑇 ∧ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)))
167	166	simprd 495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡))
168	136, 137, 143, 162, 167	ltletrd 11334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) < (𝐹‘𝑡))
169	136, 143	ltnled 11321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → (((𝑗 − (1 / 3)) · 𝐸) < (𝐹‘𝑡) ↔ ¬ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
170	168, 169	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ¬ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))
171	170	intnand 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ¬ (𝑡 ∈ 𝑇 ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
172		rabid 3427	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ↔ (𝑡 ∈ 𝑇 ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
173	171, 172	sylnibr 329	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ¬ 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
174	128	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → (𝐷‘𝑗) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
175	173, 174	neleqtrrd 2851	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ¬ 𝑡 ∈ (𝐷‘𝑗))
176	175	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑡 ∈ (𝐵‘𝑗) → ¬ 𝑡 ∈ (𝐷‘𝑗)))
177	85, 176	ralrimi 3235	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐵‘𝑗) ¬ 𝑡 ∈ (𝐷‘𝑗))
178		disj 4413	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐵‘𝑗) ∩ (𝐷‘𝑗)) = ∅ ↔ ∀𝑎 ∈ (𝐵‘𝑗) ¬ 𝑎 ∈ (𝐷‘𝑗))
179		nfcv 2891	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑎(𝐵‘𝑗)
180	75	nfcri 2883	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑡 𝑎 ∈ (𝐷‘𝑗)
181	180	nfn 1857	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑡 ¬ 𝑎 ∈ (𝐷‘𝑗)
182		nfv 1914	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑎 ¬ 𝑡 ∈ (𝐷‘𝑗)
183		eleq1 2816	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = 𝑡 → (𝑎 ∈ (𝐷‘𝑗) ↔ 𝑡 ∈ (𝐷‘𝑗)))
184	183	notbid 318	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑡 → (¬ 𝑎 ∈ (𝐷‘𝑗) ↔ ¬ 𝑡 ∈ (𝐷‘𝑗)))
185	179, 81, 181, 182, 184	cbvralfw 3278	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∀𝑎 ∈ (𝐵‘𝑗) ¬ 𝑎 ∈ (𝐷‘𝑗) ↔ ∀𝑡 ∈ (𝐵‘𝑗) ¬ 𝑡 ∈ (𝐷‘𝑗))
186	178, 185	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐵‘𝑗) ∩ (𝐷‘𝑗)) = ∅ ↔ ∀𝑡 ∈ (𝐵‘𝑗) ¬ 𝑡 ∈ (𝐷‘𝑗))
187	177, 186	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝐵‘𝑗) ∩ (𝐷‘𝑗)) = ∅)
188		eqid 2729	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑇 ∖ (𝐵‘𝑗)) = (𝑇 ∖ (𝐵‘𝑗))
189		stoweidlem59.19	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑁 ∈ ℕ)
190	189	nnrpd 12993	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
191	116, 190	rpdivcld 13012	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℝ⁺)
192	191	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐸 / 𝑁) ∈ ℝ⁺)
193	117, 189	nndivred 12240	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℝ)
194	112	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (1 / 3) ∈ ℝ)
195	189	nnge1d 12234	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 1 ≤ 𝑁)
196		1re 11174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 1 ∈ ℝ
197		0lt1 11700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 0 < 1
198	196, 197	pm3.2i 470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (1 ∈ ℝ ∧ 0 < 1)
199	198	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (1 ∈ ℝ ∧ 0 < 1))
200	189	nnred 12201	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑁 ∈ ℝ)
201	189	nngt0d 12235	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 0 < 𝑁)
202		lediv2 12073	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((1 ∈ ℝ ∧ 0 < 1) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (1 ≤ 𝑁 ↔ (𝐸 / 𝑁) ≤ (𝐸 / 1)))
203	199, 200, 201, 157, 202	syl121anc 1377	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (1 ≤ 𝑁 ↔ (𝐸 / 𝑁) ≤ (𝐸 / 1)))
204	195, 203	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐸 / 𝑁) ≤ (𝐸 / 1))
205	116	rpcnd 12997	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐸 ∈ ℂ)
206	205	div1d 11950	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐸 / 1) = 𝐸)
207	204, 206	breqtrd 5133	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐸 / 𝑁) ≤ 𝐸)
208		stoweidlem59.18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐸 < (1 / 3))
209	193, 117, 194, 207, 208	lelttrd 11332	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐸 / 𝑁) < (1 / 3))
210	209	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐸 / 𝑁) < (1 / 3))
211	75, 82, 85, 86, 87, 16, 89, 90, 92, 94, 96, 98, 124, 135, 187, 188, 192, 210	stoweidlem58 46056	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))
212		df-rex 3054	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))))
213	211, 212	sylib 218	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ∃𝑥(𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))))
214		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → 𝑥 ∈ 𝐴)
215		simprr1 1222	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1))
216		fveq1 6857	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 = 𝑥 → (𝑦‘𝑡) = (𝑥‘𝑡))
217	216	breq2d 5119	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 = 𝑥 → (0 ≤ (𝑦‘𝑡) ↔ 0 ≤ (𝑥‘𝑡)))
218	216	breq1d 5117	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 = 𝑥 → ((𝑦‘𝑡) ≤ 1 ↔ (𝑥‘𝑡) ≤ 1))
219	217, 218	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = 𝑥 → ((0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ↔ (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1)))
220	219	ralbidv 3156	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑥 → (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1)))
221	220, 1	elrab2 3662	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ 𝑌 ↔ (𝑥 ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1)))
222	214, 215, 221	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → 𝑥 ∈ 𝑌)
223		simprr2 1223	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁))
224		simprr3 1224	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))
225	223, 224	jca 511	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → (∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))
226		nfcv 2891	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑦𝑥
227		nfv 1914	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑦(∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))
228	216	breq1d 5117	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = 𝑥 → ((𝑦‘𝑡) < (𝐸 / 𝑁) ↔ (𝑥‘𝑡) < (𝐸 / 𝑁)))
229	228	ralbidv 3156	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑥 → (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁)))
230	216	breq2d 5119	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = 𝑥 → ((1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))
231	230	ralbidv 3156	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑥 → (∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))
232	229, 231	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑥 → ((∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)) ↔ (∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))))
233	226, 3, 227, 232	elrabf 3655	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ↔ (𝑥 ∈ 𝑌 ∧ (∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))))
234	222, 225, 233	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → 𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
235	234	ex 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))) → 𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}))
236	235	eximdv 1917	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (∃𝑥(𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))) → ∃𝑥 𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}))
237	213, 236	mpd 15	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ∃𝑥 𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
238		ne0i 4304	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ≠ ∅)
239	238	exlimiv 1930	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑥 𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ≠ ∅)
240	237, 239	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ≠ ∅)
241	68, 240	eqnetrd 2992	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐻‘𝑗) ≠ ∅)
242	241	3adant3 1132	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ (𝐻‘𝑗) = 𝑤) → (𝐻‘𝑗) ≠ ∅)
243	64, 242	eqnetrrd 2993	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ (𝐻‘𝑗) = 𝑤) → 𝑤 ≠ ∅)
244	243	3exp 1119	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ (0...𝑁) → ((𝐻‘𝑗) = 𝑤 → 𝑤 ≠ ∅)))
245	244	rexlimdv 3132	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤 → 𝑤 ≠ ∅))
246	245	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐻) → (∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤 → 𝑤 ≠ ∅))
247	63, 246	mpd 15	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐻) → 𝑤 ≠ ∅)
248	247	adantlr 715	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → 𝑤 ≠ ∅)
249		rsp 3225	. . . . . . . . . . 11 ⊢ (∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) → (𝑤 ∈ ran 𝐻 → (𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)))
250	48, 49, 248, 249	syl3c 66	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → (ℎ‘𝑤) ∈ 𝑤)
251	250	ex 412	. . . . . . . . 9 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (𝑤 ∈ ran 𝐻 → (ℎ‘𝑤) ∈ 𝑤))
252	47, 251	ralrimi 3235	. . . . . . . 8 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∀𝑤 ∈ ran 𝐻(ℎ‘𝑤) ∈ 𝑤)
253		chfnrn 7021	. . . . . . . 8 ⊢ ((ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(ℎ‘𝑤) ∈ 𝑤) → ran ℎ ⊆ ∪ ran 𝐻)
254	32, 252, 253	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ran ℎ ⊆ ∪ ran 𝐻)
255		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝜑
256		nfcv 2891	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦ℎ
257		nfcv 2891	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦(0...𝑁)
258		nfrab1 3426	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦{𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}
259	257, 258	nfmpt 5205	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦(𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
260	22, 259	nfcxfr 2889	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦𝐻
261	260	nfrn 5916	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦ran 𝐻
262	256, 261	nffn 6617	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 ℎ Fn ran 𝐻
263		nfv 1914	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)
264	261, 263	nfralw 3285	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)
265	262, 264	nfan 1899	. . . . . . . . . 10 ⊢ Ⅎ𝑦(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))
266	255, 265	nfan 1899	. . . . . . . . 9 ⊢ Ⅎ𝑦(𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)))
267	261	nfuni 4878	. . . . . . . . 9 ⊢ Ⅎ𝑦∪ ran 𝐻
268		fnunirn 7228	. . . . . . . . . . . . . . 15 ⊢ (𝐻 Fn (0...𝑁) → (𝑦 ∈ ∪ ran 𝐻 ↔ ∃𝑧 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑧)))
269		nfcv 2891	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗𝑧
270	53, 269	nffv 6868	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑗(𝐻‘𝑧)
271	270	nfcri 2883	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑗 𝑦 ∈ (𝐻‘𝑧)
272		nfv 1914	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧 𝑦 ∈ (𝐻‘𝑗)
273		fveq2 6858	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑗 → (𝐻‘𝑧) = (𝐻‘𝑗))
274	273	eleq2d 2814	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑗 → (𝑦 ∈ (𝐻‘𝑧) ↔ 𝑦 ∈ (𝐻‘𝑗)))
275	271, 272, 274	cbvrexw 3281	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑧) ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑗))
276	268, 275	bitrdi 287	. . . . . . . . . . . . . 14 ⊢ (𝐻 Fn (0...𝑁) → (𝑦 ∈ ∪ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑗)))
277	24, 276	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑦 ∈ ∪ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑗)))
278	277	biimpa 476	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) → ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑗))
279		nfv 1914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗𝜑
280	53	nfrn 5916	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑗ran 𝐻
281	280	nfuni 4878	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑗∪ ran 𝐻
282	281	nfcri 2883	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗 𝑦 ∈ ∪ ran 𝐻
283	279, 282	nfan 1899	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻)
284		nfv 1914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗 𝑦 ∈ 𝑌
285		simp1l 1198	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝜑)
286		simp2 1137	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑗 ∈ (0...𝑁))
287		simp3 1138	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ (𝐻‘𝑗))
288	68	eleq2d 2814	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑦 ∈ (𝐻‘𝑗) ↔ 𝑦 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}))
289	288	biimpa 476	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
290		rabid 3427	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ↔ (𝑦 ∈ 𝑌 ∧ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))))
291	289, 290	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → (𝑦 ∈ 𝑌 ∧ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))))
292	291	simpld 494	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ 𝑌)
293	285, 286, 287, 292	syl21anc 837	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ 𝑌)
294	293	3exp 1119	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) → (𝑗 ∈ (0...𝑁) → (𝑦 ∈ (𝐻‘𝑗) → 𝑦 ∈ 𝑌)))
295	283, 284, 294	rexlimd 3244	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) → (∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑗) → 𝑦 ∈ 𝑌))
296	278, 295	mpd 15	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) → 𝑦 ∈ 𝑌)
297	296	adantlr 715	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑦 ∈ ∪ ran 𝐻) → 𝑦 ∈ 𝑌)
298	297	ex 412	. . . . . . . . 9 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (𝑦 ∈ ∪ ran 𝐻 → 𝑦 ∈ 𝑌))
299	266, 267, 3, 298	ssrd 3951	. . . . . . . 8 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∪ ran 𝐻 ⊆ 𝑌)
300		ssrab2 4043	. . . . . . . . 9 ⊢ {𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)} ⊆ 𝐴
301	1, 300	eqsstri 3993	. . . . . . . 8 ⊢ 𝑌 ⊆ 𝐴
302	299, 301	sstrdi 3959	. . . . . . 7 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∪ ran 𝐻 ⊆ 𝐴)
303	254, 302	sstrd 3957	. . . . . 6 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ran ℎ ⊆ 𝐴)
304	42, 303	fssd 6705	. . . . 5 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ℎ:ran 𝐻⟶𝐴)
305		dffn3 6700	. . . . . . 7 ⊢ (𝐻 Fn (0...𝑁) ↔ 𝐻:(0...𝑁)⟶ran 𝐻)
306	24, 305	sylib 218	. . . . . 6 ⊢ (𝜑 → 𝐻:(0...𝑁)⟶ran 𝐻)
307	306	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → 𝐻:(0...𝑁)⟶ran 𝐻)
308		fco 6712	. . . . 5 ⊢ ((ℎ:ran 𝐻⟶𝐴 ∧ 𝐻:(0...𝑁)⟶ran 𝐻) → (ℎ ∘ 𝐻):(0...𝑁)⟶𝐴)
309	304, 307, 308	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (ℎ ∘ 𝐻):(0...𝑁)⟶𝐴)
310		nfcv 2891	. . . . . . . 8 ⊢ Ⅎ𝑗ℎ
311	310, 280	nffn 6617	. . . . . . 7 ⊢ Ⅎ𝑗 ℎ Fn ran 𝐻
312		nfv 1914	. . . . . . . 8 ⊢ Ⅎ𝑗(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)
313	280, 312	nfralw 3285	. . . . . . 7 ⊢ Ⅎ𝑗∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)
314	311, 313	nfan 1899	. . . . . 6 ⊢ Ⅎ𝑗(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))
315	279, 314	nfan 1899	. . . . 5 ⊢ Ⅎ𝑗(𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)))
316		simpll 766	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝜑)
317		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
318	24	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝐻 Fn (0...𝑁))
319		fvco2 6958	. . . . . . . . . . . 12 ⊢ ((𝐻 Fn (0...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → ((ℎ ∘ 𝐻)‘𝑗) = (ℎ‘(𝐻‘𝑗)))
320	318, 319	sylancom 588	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((ℎ ∘ 𝐻)‘𝑗) = (ℎ‘(𝐻‘𝑗)))
321		simplrr 777	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))
322		fnfun 6618	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 Fn (0...𝑁) → Fun 𝐻)
323	24, 322	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Fun 𝐻)
324	323	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → Fun 𝐻)
325	24	fndmd 6623	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom 𝐻 = (0...𝑁))
326	325	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → dom 𝐻 = (0...𝑁))
327	65, 326	eleqtrrd 2831	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ dom 𝐻)
328	327	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ dom 𝐻)
329		fvelrn 7048	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐻 ∧ 𝑗 ∈ dom 𝐻) → (𝐻‘𝑗) ∈ ran 𝐻)
330	324, 328, 329	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (𝐻‘𝑗) ∈ ran 𝐻)
331	321, 330	jca 511	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) ∧ (𝐻‘𝑗) ∈ ran 𝐻))
332	241	adantlr 715	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (𝐻‘𝑗) ≠ ∅)
333		neeq1 2987	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝐻‘𝑗) → (𝑤 ≠ ∅ ↔ (𝐻‘𝑗) ≠ ∅))
334		fveq2 6858	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝐻‘𝑗) → (ℎ‘𝑤) = (ℎ‘(𝐻‘𝑗)))
335		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝐻‘𝑗) → 𝑤 = (𝐻‘𝑗))
336	334, 335	eleq12d 2822	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝐻‘𝑗) → ((ℎ‘𝑤) ∈ 𝑤 ↔ (ℎ‘(𝐻‘𝑗)) ∈ (𝐻‘𝑗)))
337	333, 336	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝐻‘𝑗) → ((𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) ↔ ((𝐻‘𝑗) ≠ ∅ → (ℎ‘(𝐻‘𝑗)) ∈ (𝐻‘𝑗))))
338	337	rspccva 3587	. . . . . . . . . . . 12 ⊢ ((∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) ∧ (𝐻‘𝑗) ∈ ran 𝐻) → ((𝐻‘𝑗) ≠ ∅ → (ℎ‘(𝐻‘𝑗)) ∈ (𝐻‘𝑗)))
339	331, 332, 338	sylc 65	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (ℎ‘(𝐻‘𝑗)) ∈ (𝐻‘𝑗))
340	320, 339	eqeltrd 2828	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗))
341	256, 260	nfco 5829	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(ℎ ∘ 𝐻)
342		nfcv 2891	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦𝑗
343	341, 342	nffv 6868	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦((ℎ ∘ 𝐻)‘𝑗)
344		nfv 1914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑗 ∈ (0...𝑁))
345	260, 342	nffv 6868	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦(𝐻‘𝑗)
346	343, 345	nfel 2906	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)
347	344, 346	nfan 1899	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗))
348	343, 3	nfel 2906	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌
349	347, 348	nfim 1896	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌)
350		eleq1 2816	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (𝑦 ∈ (𝐻‘𝑗) ↔ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)))
351	350	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) ↔ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗))))
352		eleq1 2816	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (𝑦 ∈ 𝑌 ↔ ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌))
353	351, 352	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ 𝑌) ↔ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌)))
354	343, 349, 353, 292	vtoclgf 3535	. . . . . . . . . . 11 ⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗) → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌))
355	354	anabsi7 671	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌)
356	316, 317, 340, 355	syl21anc 837	. . . . . . . . 9 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌)
357	1	eleq2i 2820	. . . . . . . . . 10 ⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌 ↔ ((ℎ ∘ 𝐻)‘𝑗) ∈ {𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)})
358		nfcv 2891	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝐴
359		nfcv 2891	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦𝑇
360		nfcv 2891	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦0
361		nfcv 2891	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦 ≤
362		nfcv 2891	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦𝑡
363	343, 362	nffv 6868	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦(((ℎ ∘ 𝐻)‘𝑗)‘𝑡)
364	360, 361, 363	nfbr 5154	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)
365		nfcv 2891	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦1
366	363, 361, 365	nfbr 5154	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1
367	364, 366	nfan 1899	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)
368	359, 367	nfralw 3285	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)
369		nfcv 2891	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡𝑦
370		nfcv 2891	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡ℎ
371		nfra1 3261	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁)
372		nfra1 3261	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)
373	371, 372	nfan 1899	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡(∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))
374		nfra1 3261	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)
375		nfcv 2891	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡𝐴
376	374, 375	nfrabw 3443	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡{𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)}
377	1, 376	nfcxfr 2889	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡𝑌
378	373, 377	nfrabw 3443	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡{𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}
379	70, 378	nfmpt 5205	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
380	22, 379	nfcxfr 2889	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡𝐻
381	370, 380	nfco 5829	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡(ℎ ∘ 𝐻)
382	381, 74	nffv 6868	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((ℎ ∘ 𝐻)‘𝑗)
383	369, 382	nfeq 2905	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡 𝑦 = ((ℎ ∘ 𝐻)‘𝑗)
384		fveq1 6857	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (𝑦‘𝑡) = (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))
385	384	breq2d 5119	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (0 ≤ (𝑦‘𝑡) ↔ 0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
386	384	breq1d 5117	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((𝑦‘𝑡) ≤ 1 ↔ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1))
387	385, 386	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ↔ (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
388	383, 387	ralbid 3250	. . . . . . . . . . 11 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
389	343, 358, 368, 388	elrabf 3655	. . . . . . . . . 10 ⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ {𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)} ↔ (((ℎ ∘ 𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
390	357, 389	bitri 275	. . . . . . . . 9 ⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌 ↔ (((ℎ ∘ 𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
391	356, 390	sylib 218	. . . . . . . 8 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (((ℎ ∘ 𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
392	391	simprd 495	. . . . . . 7 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1))
393		nfcv 2891	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝐷‘𝑗)
394		nfcv 2891	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦 <
395		nfcv 2891	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝐸 / 𝑁)
396	363, 394, 395	nfbr 5154	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)
397	393, 396	nfralw 3285	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)
398	347, 397	nfim 1896	. . . . . . . . . 10 ⊢ Ⅎ𝑦(((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))
399	384	breq1d 5117	. . . . . . . . . . . 12 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((𝑦‘𝑡) < (𝐸 / 𝑁) ↔ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
400	383, 399	ralbid 3250	. . . . . . . . . . 11 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
401	351, 400	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁)) ↔ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))))
402	291	simprd 495	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)))
403	402	simpld 494	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁))
404	343, 398, 401, 403	vtoclgf 3535	. . . . . . . . 9 ⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗) → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
405	404	anabsi7 671	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))
406	316, 317, 340, 405	syl21anc 837	. . . . . . 7 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))
407		nfcv 2891	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝐵‘𝑗)
408		nfcv 2891	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(1 − (𝐸 / 𝑁))
409	408, 394, 363	nfbr 5154	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)
410	407, 409	nfralw 3285	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)
411	347, 410	nfim 1896	. . . . . . . . . 10 ⊢ Ⅎ𝑦(((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))
412	384	breq2d 5119	. . . . . . . . . . . 12 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
413	383, 412	ralbid 3250	. . . . . . . . . . 11 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
414	351, 413	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)) ↔ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))))
415	402	simprd 495	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))
416	343, 411, 414, 415	vtoclgf 3535	. . . . . . . . 9 ⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗) → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
417	416	anabsi7 671	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))
418	316, 317, 340, 417	syl21anc 837	. . . . . . 7 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))
419	392, 406, 418	3jca 1128	. . . . . 6 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
420	419	ex 412	. . . . 5 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (𝑗 ∈ (0...𝑁) → (∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))))
421	315, 420	ralrimi 3235	. . . 4 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
422	309, 421	jca 511	. . 3 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ((ℎ ∘ 𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))))
423		feq1 6666	. . . . 5 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (𝑥:(0...𝑁)⟶𝐴 ↔ (ℎ ∘ 𝐻):(0...𝑁)⟶𝐴))
424		nfcv 2891	. . . . . . 7 ⊢ Ⅎ𝑗𝑥
425	310, 53	nfco 5829	. . . . . . 7 ⊢ Ⅎ𝑗(ℎ ∘ 𝐻)
426	424, 425	nfeq 2905	. . . . . 6 ⊢ Ⅎ𝑗 𝑥 = (ℎ ∘ 𝐻)
427		nfcv 2891	. . . . . . . . 9 ⊢ Ⅎ𝑡𝑥
428	427, 381	nfeq 2905	. . . . . . . 8 ⊢ Ⅎ𝑡 𝑥 = (ℎ ∘ 𝐻)
429		fveq1 6857	. . . . . . . . . . 11 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (𝑥‘𝑗) = ((ℎ ∘ 𝐻)‘𝑗))
430	429	fveq1d 6860	. . . . . . . . . 10 ⊢ (𝑥 = (ℎ ∘ 𝐻) → ((𝑥‘𝑗)‘𝑡) = (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))
431	430	breq2d 5119	. . . . . . . . 9 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (0 ≤ ((𝑥‘𝑗)‘𝑡) ↔ 0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
432	430	breq1d 5117	. . . . . . . . 9 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (((𝑥‘𝑗)‘𝑡) ≤ 1 ↔ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1))
433	431, 432	anbi12d 632	. . . . . . . 8 ⊢ (𝑥 = (ℎ ∘ 𝐻) → ((0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ↔ (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
434	428, 433	ralbid 3250	. . . . . . 7 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
435	430	breq1d 5117	. . . . . . . 8 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
436	428, 435	ralbid 3250	. . . . . . 7 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
437	430	breq2d 5119	. . . . . . . 8 ⊢ (𝑥 = (ℎ ∘ 𝐻) → ((1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
438	428, 437	ralbid 3250	. . . . . . 7 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡) ↔ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
439	434, 436, 438	3anbi123d 1438	. . . . . 6 ⊢ (𝑥 = (ℎ ∘ 𝐻) → ((∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))))
440	426, 439	ralbid 3250	. . . . 5 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡)) ↔ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))))
441	423, 440	anbi12d 632	. . . 4 ⊢ (𝑥 = (ℎ ∘ 𝐻) → ((𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡))) ↔ ((ℎ ∘ 𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))))
442	441	spcegv 3563	. . 3 ⊢ ((ℎ ∘ 𝐻) ∈ V → (((ℎ ∘ 𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))) → ∃𝑥(𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡)))))
443	40, 422, 442	sylc 65	. 2 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∃𝑥(𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡))))
444	31, 443	exlimddv 1935	1 ⊢ (𝜑 → ∃𝑥(𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∃wex 1779 Ⅎwnf 1783 ∈ wcel 2109 Ⅎwnfc 2876 ≠ wne 2925 ∀wral 3044 ∃wrex 3053 {crab 3405 Vcvv 3447 ∖ cdif 3911 ∩ cin 3913 ⊆ wss 3914 ∅c0 4296 ∪ cuni 4871 class class class wbr 5107 ↦ cmpt 5188 dom cdm 5638 ran crn 5639 ∘ ccom 5642 Fun wfun 6505 Fn wfn 6506 ⟶wf 6507 ‘cfv 6511 (class class class)co 7387 Fincfn 8918 ℝcr 11067 0cc0 11068 1c1 11069 + caddc 11071 · cmul 11073 < clt 11208 ≤ cle 11209 − cmin 11405 / cdiv 11835 ℕcn 12186 3c3 12242 ℝ⁺crp 12951 (,)cioo 13306 ...cfz 13468 topGenctg 17400 Clsdccld 22903 Cn ccn 23111 Compccmp 23273

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-inf2 9594 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145 ax-pre-sup 11146

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4872 df-int 4911 df-iun 4957 df-iin 4958 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-se 5592 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-isom 6520 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-of 7653 df-om 7843 df-1st 7968 df-2nd 7969 df-supp 8140 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-1o 8434 df-2o 8435 df-er 8671 df-map 8801 df-pm 8802 df-ixp 8871 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-fsupp 9313 df-fi 9362 df-sup 9393 df-inf 9394 df-oi 9463 df-card 9892 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-div 11836 df-nn 12187 df-2 12249 df-3 12250 df-4 12251 df-5 12252 df-6 12253 df-7 12254 df-8 12255 df-9 12256 df-n0 12443 df-z 12530 df-dec 12650 df-uz 12794 df-q 12908 df-rp 12952 df-xneg 13072 df-xadd 13073 df-xmul 13074 df-ioo 13310 df-ioc 13311 df-ico 13312 df-icc 13313 df-fz 13469 df-fzo 13616 df-fl 13754 df-seq 13967 df-exp 14027 df-hash 14296 df-cj 15065 df-re 15066 df-im 15067 df-sqrt 15201 df-abs 15202 df-clim 15454 df-rlim 15455 df-sum 15653 df-struct 17117 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-mulr 17234 df-starv 17235 df-sca 17236 df-vsca 17237 df-ip 17238 df-tset 17239 df-ple 17240 df-ds 17242 df-unif 17243 df-hom 17244 df-cco 17245 df-rest 17385 df-topn 17386 df-0g 17404 df-gsum 17405 df-topgen 17406 df-pt 17407 df-prds 17410 df-xrs 17465 df-qtop 17470 df-imas 17471 df-xps 17473 df-mre 17547 df-mrc 17548 df-acs 17550 df-mgm 18567 df-sgrp 18646 df-mnd 18662 df-submnd 18711 df-mulg 19000 df-cntz 19249 df-cmn 19712 df-psmet 21256 df-xmet 21257 df-met 21258 df-bl 21259 df-mopn 21260 df-cnfld 21265 df-top 22781 df-topon 22798 df-topsp 22820 df-bases 22833 df-cld 22906 df-cn 23114 df-cnp 23115 df-cmp 23274 df-tx 23449 df-hmeo 23642 df-xms 24208 df-ms 24209 df-tms 24210

This theorem is referenced by: stoweidlem60 46058

W3C validator