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 46890

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 3431	. . . . . . . . . 10 ⊢ Ⅎ𝑦{𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)}
3	1, 2	nfcxfr 2920	. . . . . . . . 9 ⊢ Ⅎ𝑦𝑌
4		nfcv 2922	. . . . . . . . 9 ⊢ Ⅎ𝑧𝑌
5		nfv 1947	. . . . . . . . 9 ⊢ Ⅎ𝑧(∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))
6		nfv 1947	. . . . . . . . 9 ⊢ Ⅎ𝑦(∀𝑡 ∈ (𝐷‘𝑗)(𝑧‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑧‘𝑡))
7		fveq1 6878	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝑦‘𝑡) = (𝑧‘𝑡))
8	7	breq1d 5113	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((𝑦‘𝑡) < (𝐸 / 𝑁) ↔ (𝑧‘𝑡) < (𝐸 / 𝑁)))
9	8	ralbidv 3185	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷‘𝑗)(𝑧‘𝑡) < (𝐸 / 𝑁)))
10	7	breq2d 5115	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (𝑧‘𝑡)))
11	10	ralbidv 3185	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑧‘𝑡)))
12	9, 11	anbi12d 644	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)) ↔ (∀𝑡 ∈ (𝐷‘𝑗)(𝑧‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑧‘𝑡))))
13	3, 4, 5, 6, 12	cbvrabw 3446	. . . . . . . 8 ⊢ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} = {𝑧 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑧‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑧‘𝑡))}
14		ovexd 7449	. . . . . . . . . 10 ⊢ (𝜑 → (𝐽 Cn 𝐾) ∈ V)
15		stoweidlem59.11	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
16		stoweidlem59.5	. . . . . . . . . . 11 ⊢ 𝐶 = (𝐽 Cn 𝐾)
17	15, 16	sseqtrdi 3971	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ⊆ (𝐽 Cn 𝐾))
18	14, 17	ssexd 5289	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ V)
19	1, 18	rabexd 5304	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ V)
20	13, 19	rabexd 5304	. . . . . . 7 ⊢ (𝜑 → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V)
21	20	ralrimivw 3158	. . . . . 6 ⊢ (𝜑 → ∀𝑗 ∈ (0...𝑁){𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V)
22		stoweidlem59.9	. . . . . . 7 ⊢ 𝐻 = (𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
23	22	fnmpt 6673	. . . . . 6 ⊢ (∀𝑗 ∈ (0...𝑁){𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V → 𝐻 Fn (0...𝑁))
24	21, 23	syl 18	. . . . 5 ⊢ (𝜑 → 𝐻 Fn (0...𝑁))
25		fzfi 14039	. . . . 5 ⊢ (0...𝑁) ∈ Fin
26		fnfi 9175	. . . . 5 ⊢ ((𝐻 Fn (0...𝑁) ∧ (0...𝑁) ∈ Fin) → 𝐻 ∈ Fin)
27	24, 25, 26	sylancl 598	. . . 4 ⊢ (𝜑 → 𝐻 ∈ Fin)
28		rnfi 9310	. . . 4 ⊢ (𝐻 ∈ Fin → ran 𝐻 ∈ Fin)
29	27, 28	syl 18	. . 3 ⊢ (𝜑 → ran 𝐻 ∈ Fin)
30		fnchoice 45866	. . 3 ⊢ (ran 𝐻 ∈ Fin → ∃ℎ(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)))
31	29, 30	syl 18	. 2 ⊢ (𝜑 → ∃ℎ(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)))
32		simprl 783	. . . . 5 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ℎ Fn ran 𝐻)
33		ovex 7447	. . . . . . . 8 ⊢ (0...𝑁) ∈ V
34	33	mptex 7223	. . . . . . 7 ⊢ (𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}) ∈ V
35	22, 34	eqeltri 2856	. . . . . 6 ⊢ 𝐻 ∈ V
36	35	rnex 7908	. . . . 5 ⊢ ran 𝐻 ∈ V
37		fnex 7217	. . . . 5 ⊢ ((ℎ Fn ran 𝐻 ∧ ran 𝐻 ∈ V) → ℎ ∈ V)
38	32, 36, 37	sylancl 598	. . . 4 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ℎ ∈ V)
39		coexg 7927	. . . 4 ⊢ ((ℎ ∈ V ∧ 𝐻 ∈ V) → (ℎ ∘ 𝐻) ∈ V)
40	38, 35, 39	sylancl 598	. . 3 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (ℎ ∘ 𝐻) ∈ V)
41		dffn3 6716	. . . . . . 7 ⊢ (ℎ Fn ran 𝐻 ↔ ℎ:ran 𝐻⟶ran ℎ)
42	32, 41	sylib 221	. . . . . 6 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ℎ:ran 𝐻⟶ran ℎ)
43		nfv 1947	. . . . . . . . . 10 ⊢ Ⅎ𝑤𝜑
44		nfv 1947	. . . . . . . . . . 11 ⊢ Ⅎ𝑤 ℎ Fn ran 𝐻
45		nfra1 3286	. . . . . . . . . . 11 ⊢ Ⅎ𝑤∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)
46	44, 45	nfan 1932	. . . . . . . . . 10 ⊢ Ⅎ𝑤(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))
47	43, 46	nfan 1932	. . . . . . . . 9 ⊢ Ⅎ𝑤(𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)))
48		simplrr 790	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))
49		simpr 490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → 𝑤 ∈ ran 𝐻)
50		fvelrnb 6939	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 Fn (0...𝑁) → (𝑤 ∈ ran 𝐻 ↔ ∃𝑎 ∈ (0...𝑁)(𝐻‘𝑎) = 𝑤))
51		nfv 1947	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑎(𝐻‘𝑗) = 𝑤
52		nfmpt1 5204	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑗(𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
53	22, 52	nfcxfr 2920	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗𝐻
54		nfcv 2922	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗𝑎
55	53, 54	nffv 6889	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗(𝐻‘𝑎)
56		nfcv 2922	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗𝑤
57	55, 56	nfeq 2935	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑗(𝐻‘𝑎) = 𝑤
58		fveq2 6879	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑎 → (𝐻‘𝑗) = (𝐻‘𝑎))
59	58	eqeq1d 2762	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑎 → ((𝐻‘𝑗) = 𝑤 ↔ (𝐻‘𝑎) = 𝑤))
60	51, 57, 59	cbvrexw 3305	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤 ↔ ∃𝑎 ∈ (0...𝑁)(𝐻‘𝑎) = 𝑤)
61	50, 60	bitr4di 292	. . . . . . . . . . . . . . 15 ⊢ (𝐻 Fn (0...𝑁) → (𝑤 ∈ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤))
62	24, 61	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑤 ∈ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤))
63	62	biimpa 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤)
64		simp3 1156	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ (𝐻‘𝑗) = 𝑤) → (𝐻‘𝑗) = 𝑤)
65		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
66	20	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V)
67	22	fvmpt2 6999	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ (0...𝑁) ∧ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V) → (𝐻‘𝑗) = {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
68	65, 66, 67	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐻‘𝑗) = {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
69		stoweidlem59.6	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
70		nfcv 2922	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑡(0...𝑁)
71		nfrab1 3431	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑡{𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}
72	70, 71	nfmpt 5203	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
73	69, 72	nfcxfr 2920	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡𝐷
74		nfcv 2922	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡𝑗
75	73, 74	nffv 6889	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑡(𝐷‘𝑗)
76		nfcv 2922	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡𝑇
77		stoweidlem59.7	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
78		nfrab1 3431	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑡{𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}
79	70, 78	nfmpt 5203	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
80	77, 79	nfcxfr 2920	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑡𝐵
81	80, 74	nffv 6889	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡(𝐵‘𝑗)
82	76, 81	nfdif 4077	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑡(𝑇 ∖ (𝐵‘𝑗))
83		stoweidlem59.2	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡𝜑
84		nfv 1947	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑡 𝑗 ∈ (0...𝑁)
85	83, 84	nfan 1932	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑡(𝜑 ∧ 𝑗 ∈ (0...𝑁))
86		stoweidlem59.3	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐾 = (topGen‘ran (,))
87		stoweidlem59.4	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑇 = ∪ 𝐽
88		stoweidlem59.10	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐽 ∈ Comp)
89	88	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝐽 ∈ Comp)
90	15	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝐴 ⊆ 𝐶)
91		stoweidlem59.12	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)
92	91	3adant1r 1196	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)
93		stoweidlem59.13	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)
94	93	3adant1r 1196	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)
95		stoweidlem59.14	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑦) ∈ 𝐴)
96	95	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑦) ∈ 𝐴)
97		stoweidlem59.15	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡))
98	97	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡)) → ∃𝑞 ∈ 𝐴 (𝑞‘𝑟) ≠ (𝑞‘𝑡))
99	88	uniexd 7745	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → ∪ 𝐽 ∈ V)
100	87, 99	eqeltrid 2864	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑇 ∈ V)
101	100	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑇 ∈ V)
102		rabexg 5302	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V)
103	101, 102	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V)
104	77	fvmpt2 6999	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑗 ∈ (0...𝑁) ∧ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V) → (𝐵‘𝑗) = {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
105	65, 103, 104	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐵‘𝑗) = {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
106		stoweidlem59.1	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑡𝐹
107		eqid 2760	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} = {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}
108		elfzelz 13581	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
109	108	zred 12728	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
110		3re 12348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 3 ∈ ℝ
111		3ne0 12377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 3 ≠ 0
112	110, 111	rereccli 12007	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (1 / 3) ∈ ℝ
113		readdcl 11210	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ) → (𝑗 + (1 / 3)) ∈ ℝ)
114	109, 112, 113	sylancl 598	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + (1 / 3)) ∈ ℝ)
115	114	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑗 + (1 / 3)) ∈ ℝ)
116		stoweidlem59.17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐸 ∈ ℝ⁺)
117	116	rpred 13089	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐸 ∈ ℝ)
118	117	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝐸 ∈ ℝ)
119	115, 118	remulcld 11266	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑗 + (1 / 3)) · 𝐸) ∈ ℝ)
120		stoweidlem59.16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐹 ∈ 𝐶)
121	120, 16	eleqtrdi 2870	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))
122	121	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝐹 ∈ (𝐽 Cn 𝐾))
123	106, 86, 87, 107, 119, 122	rfcnpre3 45870	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ (Clsd‘𝐽))
124	105, 123	eqeltrd 2860	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐵‘𝑗) ∈ (Clsd‘𝐽))
125		rabexg 5302	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V)
126	101, 125	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V)
127	69	fvmpt2 6999	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑗 ∈ (0...𝑁) ∧ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V) → (𝐷‘𝑗) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
128	65, 126, 127	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐷‘𝑗) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
129		eqid 2760	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}
130		resubcl 11549	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ) → (𝑗 − (1 / 3)) ∈ ℝ)
131	109, 112, 130	sylancl 598	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ (0...𝑁) → (𝑗 − (1 / 3)) ∈ ℝ)
132	131	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑗 − (1 / 3)) ∈ ℝ)
133	132, 118	remulcld 11266	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ)
134	106, 86, 87, 129, 133, 122	rfcnpre4 45871	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ (Clsd‘𝐽))
135	128, 134	eqeltrd 2860	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐷‘𝑗) ∈ (Clsd‘𝐽))
136	133	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ)
137	119	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ((𝑗 + (1 / 3)) · 𝐸) ∈ ℝ)
138	86, 87, 16, 120	fcnre 45862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝜑 → 𝐹:𝑇⟶ℝ)
139	138	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → 𝐹:𝑇⟶ℝ)
140		ssrab2 4028	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ⊆ 𝑇
141	105, 140	eqsstrdi 3975	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐵‘𝑗) ⊆ 𝑇)
142	141	sselda 3931	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → 𝑡 ∈ 𝑇)
143	139, 142	ffvelcdmd 7079	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → (𝐹‘𝑡) ∈ ℝ)
144	112, 130	mpan2 704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) ∈ ℝ)
145		id 23	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑗 ∈ ℝ → 𝑗 ∈ ℝ)
146	112, 113	mpan2 704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑗 ∈ ℝ → (𝑗 + (1 / 3)) ∈ ℝ)
147		3pos 12376	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ 0 < 3
148	110, 147	recgt0ii 12148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ 0 < (1 / 3)
149	112, 148	elrpii 13048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (1 / 3) ∈ ℝ⁺
150		ltsubrp 13083	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ⁺) → (𝑗 − (1 / 3)) < 𝑗)
151	149, 150	mpan2 704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) < 𝑗)
152		ltaddrp 13084	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑗 ∈ ℝ ∧ (1 / 3) ∈ ℝ⁺) → 𝑗 < (𝑗 + (1 / 3)))
153	149, 152	mpan2 704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑗 ∈ ℝ → 𝑗 < (𝑗 + (1 / 3)))
154	144, 145, 146, 151, 153	lttrd 11398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
155	109, 154	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑗 ∈ (0...𝑁) → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
156	155	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑗 − (1 / 3)) < (𝑗 + (1 / 3)))
157	116	rpregt0d 13095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
158	157	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
159		ltmul1 12092	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑗 − (1 / 3)) ∈ ℝ ∧ (𝑗 + (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑗 − (1 / 3)) < (𝑗 + (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸)))
160	132, 115, 158, 159	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) < (𝑗 + (1 / 3)) ↔ ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸)))
161	156, 160	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸))
162	161	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸))
163	105	eleq2d 2846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑡 ∈ (𝐵‘𝑗) ↔ 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}))
164	163	biimpa 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})
165		rabid 3432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑡 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ↔ (𝑡 ∈ 𝑇 ∧ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)))
166	164, 165	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → (𝑡 ∈ 𝑇 ∧ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)))
167	166	simprd 501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡))
168	136, 137, 143, 162, 167	ltletrd 11397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) < (𝐹‘𝑡))
169	136, 143	ltnled 11384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → (((𝑗 − (1 / 3)) · 𝐸) < (𝐹‘𝑡) ↔ ¬ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
170	168, 169	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ¬ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸))
171	170	intnand 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ¬ (𝑡 ∈ 𝑇 ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
172		rabid 3432	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ↔ (𝑡 ∈ 𝑇 ∧ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)))
173	171, 172	sylnibr 332	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ¬ 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
174	128	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → (𝐷‘𝑗) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
175	173, 174	neleqtrrd 2883	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ¬ 𝑡 ∈ (𝐷‘𝑗))
176	175	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑡 ∈ (𝐵‘𝑗) → ¬ 𝑡 ∈ (𝐷‘𝑗)))
177	85, 176	ralrimi 3260	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐵‘𝑗) ¬ 𝑡 ∈ (𝐷‘𝑗))
178		disj 4403	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐵‘𝑗) ∩ (𝐷‘𝑗)) = ∅ ↔ ∀𝑎 ∈ (𝐵‘𝑗) ¬ 𝑎 ∈ (𝐷‘𝑗))
179		nfcv 2922	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑎(𝐵‘𝑗)
180	75	nfcri 2914	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑡 𝑎 ∈ (𝐷‘𝑗)
181	180	nfn 1890	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑡 ¬ 𝑎 ∈ (𝐷‘𝑗)
182		nfv 1947	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑎 ¬ 𝑡 ∈ (𝐷‘𝑗)
183		eleq1 2848	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = 𝑡 → (𝑎 ∈ (𝐷‘𝑗) ↔ 𝑡 ∈ (𝐷‘𝑗)))
184	183	notbid 321	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑡 → (¬ 𝑎 ∈ (𝐷‘𝑗) ↔ ¬ 𝑡 ∈ (𝐷‘𝑗)))
185	179, 81, 181, 182, 184	cbvralfw 3302	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∀𝑎 ∈ (𝐵‘𝑗) ¬ 𝑎 ∈ (𝐷‘𝑗) ↔ ∀𝑡 ∈ (𝐵‘𝑗) ¬ 𝑡 ∈ (𝐷‘𝑗))
186	178, 185	bitri 278	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐵‘𝑗) ∩ (𝐷‘𝑗)) = ∅ ↔ ∀𝑡 ∈ (𝐵‘𝑗) ¬ 𝑡 ∈ (𝐷‘𝑗))
187	177, 186	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝐵‘𝑗) ∩ (𝐷‘𝑗)) = ∅)
188		eqid 2760	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑇 ∖ (𝐵‘𝑗)) = (𝑇 ∖ (𝐵‘𝑗))
189		stoweidlem59.19	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑁 ∈ ℕ)
190	189	nnrpd 13087	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
191	116, 190	rpdivcld 13106	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℝ⁺)
192	191	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐸 / 𝑁) ∈ ℝ⁺)
193	117, 189	nndivred 12317	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℝ)
194	112	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (1 / 3) ∈ ℝ)
195	189	nnge1d 12311	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 1 ≤ 𝑁)
196		1re 11235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 1 ∈ ℝ
197		0lt1 11763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ 0 < 1
198	196, 197	pm3.2i 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (1 ∈ ℝ ∧ 0 < 1)
199	198	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (1 ∈ ℝ ∧ 0 < 1))
200	189	nnred 12275	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝑁 ∈ ℝ)
201	189	nngt0d 12312	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 0 < 𝑁)
202		lediv2 12132	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((1 ∈ ℝ ∧ 0 < 1) ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (1 ≤ 𝑁 ↔ (𝐸 / 𝑁) ≤ (𝐸 / 1)))
203	199, 200, 201, 157, 202	syl121anc 1402	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (1 ≤ 𝑁 ↔ (𝐸 / 𝑁) ≤ (𝐸 / 1)))
204	195, 203	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐸 / 𝑁) ≤ (𝐸 / 1))
205	116	rpcnd 13091	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐸 ∈ ℂ)
206	205	div1d 12010	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐸 / 1) = 𝐸)
207	204, 206	breqtrd 5131	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐸 / 𝑁) ≤ 𝐸)
208		stoweidlem59.18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐸 < (1 / 3))
209	193, 117, 194, 207, 208	lelttrd 11395	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝐸 / 𝑁) < (1 / 3))
210	209	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐸 / 𝑁) < (1 / 3))
211	75, 82, 85, 86, 87, 16, 89, 90, 92, 94, 96, 98, 124, 135, 187, 188, 192, 210	stoweidlem58 46889	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))
212		df-rex 3087	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))))
213	211, 212	sylib 221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ∃𝑥(𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))))
214		simprl 783	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → 𝑥 ∈ 𝐴)
215		simprr1 1240	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1))
216		fveq1 6878	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 = 𝑥 → (𝑦‘𝑡) = (𝑥‘𝑡))
217	216	breq2d 5115	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 = 𝑥 → (0 ≤ (𝑦‘𝑡) ↔ 0 ≤ (𝑥‘𝑡)))
218	216	breq1d 5113	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 = 𝑥 → ((𝑦‘𝑡) ≤ 1 ↔ (𝑥‘𝑡) ≤ 1))
219	217, 218	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = 𝑥 → ((0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ↔ (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1)))
220	219	ralbidv 3185	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑥 → (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1)))
221	220, 1	elrab2 3649	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ 𝑌 ↔ (𝑥 ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1)))
222	214, 215, 221	sylanbrc 595	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → 𝑥 ∈ 𝑌)
223		simprr2 1241	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁))
224		simprr3 1242	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))
225	223, 224	jca 521	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → (∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))
226		nfcv 2922	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑦𝑥
227		nfv 1947	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑦(∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))
228	216	breq1d 5113	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = 𝑥 → ((𝑦‘𝑡) < (𝐸 / 𝑁) ↔ (𝑥‘𝑡) < (𝐸 / 𝑁)))
229	228	ralbidv 3185	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑥 → (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁)))
230	216	breq2d 5115	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = 𝑥 → ((1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))
231	230	ralbidv 3185	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑥 → (∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))
232	229, 231	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑥 → ((∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)) ↔ (∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))))
233	226, 3, 227, 232	elrabf 3642	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ↔ (𝑥 ∈ 𝑌 ∧ (∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))))
234	222, 225, 233	sylanbrc 595	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → 𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
235	234	ex 418	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))) → 𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}))
236	235	eximdv 1950	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (∃𝑥(𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))) → ∃𝑥 𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}))
237	213, 236	mpd 16	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ∃𝑥 𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
238		ne0i 4287	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ≠ ∅)
239	238	exlimiv 1963	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑥 𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ≠ ∅)
240	237, 239	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ≠ ∅)
241	68, 240	eqnetrd 3022	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐻‘𝑗) ≠ ∅)
242	241	3adant3 1150	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ (𝐻‘𝑗) = 𝑤) → (𝐻‘𝑗) ≠ ∅)
243	64, 242	eqnetrrd 3023	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ (𝐻‘𝑗) = 𝑤) → 𝑤 ≠ ∅)
244	243	3exp 1137	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑗 ∈ (0...𝑁) → ((𝐻‘𝑗) = 𝑤 → 𝑤 ≠ ∅)))
245	244	rexlimdv 3161	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤 → 𝑤 ≠ ∅))
246	245	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐻) → (∃𝑗 ∈ (0...𝑁)(𝐻‘𝑗) = 𝑤 → 𝑤 ≠ ∅))
247	63, 246	mpd 16	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐻) → 𝑤 ≠ ∅)
248	247	adantlr 728	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → 𝑤 ≠ ∅)
249		rsp 3250	. . . . . . . . . . 11 ⊢ (∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) → (𝑤 ∈ ran 𝐻 → (𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)))
250	48, 49, 248, 249	syl3c 67	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → (ℎ‘𝑤) ∈ 𝑤)
251	250	ex 418	. . . . . . . . 9 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (𝑤 ∈ ran 𝐻 → (ℎ‘𝑤) ∈ 𝑤))
252	47, 251	ralrimi 3260	. . . . . . . 8 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∀𝑤 ∈ ran 𝐻(ℎ‘𝑤) ∈ 𝑤)
253		chfnrn 7042	. . . . . . . 8 ⊢ ((ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(ℎ‘𝑤) ∈ 𝑤) → ran ℎ ⊆ ∪ ran 𝐻)
254	32, 252, 253	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ran ℎ ⊆ ∪ ran 𝐻)
255		nfv 1947	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝜑
256		nfcv 2922	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦ℎ
257		nfcv 2922	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦(0...𝑁)
258		nfrab1 3431	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦{𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}
259	257, 258	nfmpt 5203	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦(𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
260	22, 259	nfcxfr 2920	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦𝐻
261	260	nfrn 5936	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦ran 𝐻
262	256, 261	nffn 6632	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 ℎ Fn ran 𝐻
263		nfv 1947	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)
264	261, 263	nfralw 3309	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)
265	262, 264	nfan 1932	. . . . . . . . . 10 ⊢ Ⅎ𝑦(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))
266	255, 265	nfan 1932	. . . . . . . . 9 ⊢ Ⅎ𝑦(𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)))
267	261	nfuni 4874	. . . . . . . . 9 ⊢ Ⅎ𝑦∪ ran 𝐻
268		fnunirn 7251	. . . . . . . . . . . . . . 15 ⊢ (𝐻 Fn (0...𝑁) → (𝑦 ∈ ∪ ran 𝐻 ↔ ∃𝑧 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑧)))
269		nfcv 2922	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗𝑧
270	53, 269	nffv 6889	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑗(𝐻‘𝑧)
271	270	nfcri 2914	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑗 𝑦 ∈ (𝐻‘𝑧)
272		nfv 1947	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧 𝑦 ∈ (𝐻‘𝑗)
273		fveq2 6879	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑗 → (𝐻‘𝑧) = (𝐻‘𝑗))
274	273	eleq2d 2846	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑗 → (𝑦 ∈ (𝐻‘𝑧) ↔ 𝑦 ∈ (𝐻‘𝑗)))
275	271, 272, 274	cbvrexw 3305	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑧) ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑗))
276	268, 275	bitrdi 290	. . . . . . . . . . . . . 14 ⊢ (𝐻 Fn (0...𝑁) → (𝑦 ∈ ∪ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑗)))
277	24, 276	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑦 ∈ ∪ ran 𝐻 ↔ ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑗)))
278	277	biimpa 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) → ∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑗))
279		nfv 1947	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗𝜑
280	53	nfrn 5936	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑗ran 𝐻
281	280	nfuni 4874	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑗∪ ran 𝐻
282	281	nfcri 2914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗 𝑦 ∈ ∪ ran 𝐻
283	279, 282	nfan 1932	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻)
284		nfv 1947	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗 𝑦 ∈ 𝑌
285		simp1l 1216	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝜑)
286		simp2 1155	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑗 ∈ (0...𝑁))
287		simp3 1156	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ (𝐻‘𝑗))
288	68	eleq2d 2846	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑦 ∈ (𝐻‘𝑗) ↔ 𝑦 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}))
289	288	biimpa 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
290		rabid 3432	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ↔ (𝑦 ∈ 𝑌 ∧ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))))
291	289, 290	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → (𝑦 ∈ 𝑌 ∧ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))))
292	291	simpld 500	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ 𝑌)
293	285, 286, 287, 292	syl21anc 851	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ 𝑌)
294	293	3exp 1137	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) → (𝑗 ∈ (0...𝑁) → (𝑦 ∈ (𝐻‘𝑗) → 𝑦 ∈ 𝑌)))
295	283, 284, 294	rexlimd 3269	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) → (∃𝑗 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑗) → 𝑦 ∈ 𝑌))
296	278, 295	mpd 16	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻) → 𝑦 ∈ 𝑌)
297	296	adantlr 728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑦 ∈ ∪ ran 𝐻) → 𝑦 ∈ 𝑌)
298	297	ex 418	. . . . . . . . 9 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (𝑦 ∈ ∪ ran 𝐻 → 𝑦 ∈ 𝑌))
299	266, 267, 3, 298	ssrd 3936	. . . . . . . 8 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∪ ran 𝐻 ⊆ 𝑌)
300		ssrab2 4028	. . . . . . . . 9 ⊢ {𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)} ⊆ 𝐴
301	1, 300	eqsstri 3977	. . . . . . . 8 ⊢ 𝑌 ⊆ 𝐴
302	299, 301	sstrdi 3943	. . . . . . 7 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∪ ran 𝐻 ⊆ 𝐴)
303	254, 302	sstrd 3941	. . . . . 6 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ran ℎ ⊆ 𝐴)
304	42, 303	fssd 6721	. . . . 5 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ℎ:ran 𝐻⟶𝐴)
305		dffn3 6716	. . . . . . 7 ⊢ (𝐻 Fn (0...𝑁) ↔ 𝐻:(0...𝑁)⟶ran 𝐻)
306	24, 305	sylib 221	. . . . . 6 ⊢ (𝜑 → 𝐻:(0...𝑁)⟶ran 𝐻)
307	306	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → 𝐻:(0...𝑁)⟶ran 𝐻)
308		fco 6728	. . . . 5 ⊢ ((ℎ:ran 𝐻⟶𝐴 ∧ 𝐻:(0...𝑁)⟶ran 𝐻) → (ℎ ∘ 𝐻):(0...𝑁)⟶𝐴)
309	304, 307, 308	syl2anc 596	. . . 4 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (ℎ ∘ 𝐻):(0...𝑁)⟶𝐴)
310		nfcv 2922	. . . . . . . 8 ⊢ Ⅎ𝑗ℎ
311	310, 280	nffn 6632	. . . . . . 7 ⊢ Ⅎ𝑗 ℎ Fn ran 𝐻
312		nfv 1947	. . . . . . . 8 ⊢ Ⅎ𝑗(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)
313	280, 312	nfralw 3309	. . . . . . 7 ⊢ Ⅎ𝑗∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)
314	311, 313	nfan 1932	. . . . . 6 ⊢ Ⅎ𝑗(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))
315	279, 314	nfan 1932	. . . . 5 ⊢ Ⅎ𝑗(𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)))
316		simpll 779	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝜑)
317		simpr 490	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁))
318	24	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝐻 Fn (0...𝑁))
319		fvco2 6976	. . . . . . . . . . . 12 ⊢ ((𝐻 Fn (0...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → ((ℎ ∘ 𝐻)‘𝑗) = (ℎ‘(𝐻‘𝑗)))
320	318, 319	sylancom 600	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((ℎ ∘ 𝐻)‘𝑗) = (ℎ‘(𝐻‘𝑗)))
321		simplrr 790	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))
322		fnfun 6633	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 Fn (0...𝑁) → Fun 𝐻)
323	24, 322	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Fun 𝐻)
324	323	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → Fun 𝐻)
325	24	fndmd 6638	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom 𝐻 = (0...𝑁))
326	325	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → dom 𝐻 = (0...𝑁))
327	65, 326	eleqtrrd 2863	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ dom 𝐻)
328	327	adantlr 728	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ dom 𝐻)
329		fvelrn 7070	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐻 ∧ 𝑗 ∈ dom 𝐻) → (𝐻‘𝑗) ∈ ran 𝐻)
330	324, 328, 329	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (𝐻‘𝑗) ∈ ran 𝐻)
331	321, 330	jca 521	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) ∧ (𝐻‘𝑗) ∈ ran 𝐻))
332	241	adantlr 728	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (𝐻‘𝑗) ≠ ∅)
333		neeq1 3017	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝐻‘𝑗) → (𝑤 ≠ ∅ ↔ (𝐻‘𝑗) ≠ ∅))
334		fveq2 6879	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝐻‘𝑗) → (ℎ‘𝑤) = (ℎ‘(𝐻‘𝑗)))
335		id 23	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = (𝐻‘𝑗) → 𝑤 = (𝐻‘𝑗))
336	334, 335	eleq12d 2854	. . . . . . . . . . . . . 14 ⊢ (𝑤 = (𝐻‘𝑗) → ((ℎ‘𝑤) ∈ 𝑤 ↔ (ℎ‘(𝐻‘𝑗)) ∈ (𝐻‘𝑗)))
337	333, 336	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑤 = (𝐻‘𝑗) → ((𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) ↔ ((𝐻‘𝑗) ≠ ∅ → (ℎ‘(𝐻‘𝑗)) ∈ (𝐻‘𝑗))))
338	337	rspccva 3575	. . . . . . . . . . . 12 ⊢ ((∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) ∧ (𝐻‘𝑗) ∈ ran 𝐻) → ((𝐻‘𝑗) ≠ ∅ → (ℎ‘(𝐻‘𝑗)) ∈ (𝐻‘𝑗)))
339	331, 332, 338	sylc 66	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (ℎ‘(𝐻‘𝑗)) ∈ (𝐻‘𝑗))
340	320, 339	eqeltrd 2860	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗))
341	256, 260	nfco 5845	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(ℎ ∘ 𝐻)
342		nfcv 2922	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦𝑗
343	341, 342	nffv 6889	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦((ℎ ∘ 𝐻)‘𝑗)
344		nfv 1947	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑗 ∈ (0...𝑁))
345	260, 342	nffv 6889	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦(𝐻‘𝑗)
346	343, 345	nfel 2936	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)
347	344, 346	nfan 1932	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗))
348	343, 3	nfel 2936	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌
349	347, 348	nfim 1929	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌)
350		eleq1 2848	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (𝑦 ∈ (𝐻‘𝑗) ↔ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)))
351	350	anbi2d 642	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) ↔ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗))))
352		eleq1 2848	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (𝑦 ∈ 𝑌 ↔ ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌))
353	351, 352	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ 𝑌) ↔ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌)))
354	343, 349, 353, 292	vtoclgf 3529	. . . . . . . . . . 11 ⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗) → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌))
355	354	anabsi7 684	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌)
356	316, 317, 340, 355	syl21anc 851	. . . . . . . . 9 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌)
357	1	eleq2i 2852	. . . . . . . . . 10 ⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌 ↔ ((ℎ ∘ 𝐻)‘𝑗) ∈ {𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)})
358		nfcv 2922	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝐴
359		nfcv 2922	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦𝑇
360		nfcv 2922	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦0
361		nfcv 2922	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦 ≤
362		nfcv 2922	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦𝑡
363	343, 362	nffv 6889	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦(((ℎ ∘ 𝐻)‘𝑗)‘𝑡)
364	360, 361, 363	nfbr 5152	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)
365		nfcv 2922	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦1
366	363, 361, 365	nfbr 5152	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1
367	364, 366	nfan 1932	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)
368	359, 367	nfralw 3309	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)
369		nfcv 2922	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡𝑦
370		nfcv 2922	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡ℎ
371		nfra1 3286	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁)
372		nfra1 3286	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)
373	371, 372	nfan 1932	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡(∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))
374		nfra1 3286	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)
375		nfcv 2922	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑡𝐴
376	374, 375	nfrabw 3447	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡{𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)}
377	1, 376	nfcxfr 2920	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡𝑌
378	373, 377	nfrabw 3447	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡{𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}
379	70, 378	nfmpt 5203	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})
380	22, 379	nfcxfr 2920	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑡𝐻
381	370, 380	nfco 5845	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑡(ℎ ∘ 𝐻)
382	381, 74	nffv 6889	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑡((ℎ ∘ 𝐻)‘𝑗)
383	369, 382	nfeq 2935	. . . . . . . . . . . 12 ⊢ Ⅎ𝑡 𝑦 = ((ℎ ∘ 𝐻)‘𝑗)
384		fveq1 6878	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (𝑦‘𝑡) = (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))
385	384	breq2d 5115	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (0 ≤ (𝑦‘𝑡) ↔ 0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
386	384	breq1d 5113	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((𝑦‘𝑡) ≤ 1 ↔ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1))
387	385, 386	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ↔ (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
388	383, 387	ralbid 3275	. . . . . . . . . . 11 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
389	343, 358, 368, 388	elrabf 3642	. . . . . . . . . 10 ⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ {𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)} ↔ (((ℎ ∘ 𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
390	357, 389	bitri 278	. . . . . . . . 9 ⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌 ↔ (((ℎ ∘ 𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
391	356, 390	sylib 221	. . . . . . . 8 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (((ℎ ∘ 𝐻)‘𝑗) ∈ 𝐴 ∧ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
392	391	simprd 501	. . . . . . 7 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1))
393		nfcv 2922	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝐷‘𝑗)
394		nfcv 2922	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦 <
395		nfcv 2922	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝐸 / 𝑁)
396	363, 394, 395	nfbr 5152	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)
397	393, 396	nfralw 3309	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)
398	347, 397	nfim 1929	. . . . . . . . . 10 ⊢ Ⅎ𝑦(((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))
399	384	breq1d 5113	. . . . . . . . . . . 12 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((𝑦‘𝑡) < (𝐸 / 𝑁) ↔ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
400	383, 399	ralbid 3275	. . . . . . . . . . 11 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
401	351, 400	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁)) ↔ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))))
402	291	simprd 501	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)))
403	402	simpld 500	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁))
404	343, 398, 401, 403	vtoclgf 3529	. . . . . . . . 9 ⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗) → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
405	404	anabsi7 684	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))
406	316, 317, 340, 405	syl21anc 851	. . . . . . 7 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))
407		nfcv 2922	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(𝐵‘𝑗)
408		nfcv 2922	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(1 − (𝐸 / 𝑁))
409	408, 394, 363	nfbr 5152	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)
410	407, 409	nfralw 3309	. . . . . . . . . . 11 ⊢ Ⅎ𝑦∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)
411	347, 410	nfim 1929	. . . . . . . . . 10 ⊢ Ⅎ𝑦(((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))
412	384	breq2d 5115	. . . . . . . . . . . 12 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
413	383, 412	ralbid 3275	. . . . . . . . . . 11 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
414	351, 413	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)) ↔ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))))
415	402	simprd 501	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))
416	343, 411, 414, 415	vtoclgf 3529	. . . . . . . . 9 ⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗) → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
417	416	anabsi7 684	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))
418	316, 317, 340, 417	syl21anc 851	. . . . . . 7 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))
419	392, 406, 418	3jca 1146	. . . . . 6 ⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
420	419	ex 418	. . . . 5 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (𝑗 ∈ (0...𝑁) → (∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))))
421	315, 420	ralrimi 3260	. . . 4 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
422	309, 421	jca 521	. . 3 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ((ℎ ∘ 𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))))
423		feq1 6681	. . . . 5 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (𝑥:(0...𝑁)⟶𝐴 ↔ (ℎ ∘ 𝐻):(0...𝑁)⟶𝐴))
424		nfcv 2922	. . . . . . 7 ⊢ Ⅎ𝑗𝑥
425	310, 53	nfco 5845	. . . . . . 7 ⊢ Ⅎ𝑗(ℎ ∘ 𝐻)
426	424, 425	nfeq 2935	. . . . . 6 ⊢ Ⅎ𝑗 𝑥 = (ℎ ∘ 𝐻)
427		nfcv 2922	. . . . . . . . 9 ⊢ Ⅎ𝑡𝑥
428	427, 381	nfeq 2935	. . . . . . . 8 ⊢ Ⅎ𝑡 𝑥 = (ℎ ∘ 𝐻)
429		fveq1 6878	. . . . . . . . . . 11 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (𝑥‘𝑗) = ((ℎ ∘ 𝐻)‘𝑗))
430	429	fveq1d 6881	. . . . . . . . . 10 ⊢ (𝑥 = (ℎ ∘ 𝐻) → ((𝑥‘𝑗)‘𝑡) = (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))
431	430	breq2d 5115	. . . . . . . . 9 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (0 ≤ ((𝑥‘𝑗)‘𝑡) ↔ 0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
432	430	breq1d 5113	. . . . . . . . 9 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (((𝑥‘𝑗)‘𝑡) ≤ 1 ↔ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1))
433	431, 432	anbi12d 644	. . . . . . . 8 ⊢ (𝑥 = (ℎ ∘ 𝐻) → ((0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ↔ (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
434	428, 433	ralbid 3275	. . . . . . 7 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)))
435	430	breq1d 5113	. . . . . . . 8 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
436	428, 435	ralbid 3275	. . . . . . 7 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)))
437	430	breq2d 5115	. . . . . . . 8 ⊢ (𝑥 = (ℎ ∘ 𝐻) → ((1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
438	428, 437	ralbid 3275	. . . . . . 7 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡) ↔ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))
439	434, 436, 438	3anbi123d 1464	. . . . . 6 ⊢ (𝑥 = (ℎ ∘ 𝐻) → ((∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))))
440	426, 439	ralbid 3275	. . . . 5 ⊢ (𝑥 = (ℎ ∘ 𝐻) → (∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡)) ↔ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))))
441	423, 440	anbi12d 644	. . . 4 ⊢ (𝑥 = (ℎ ∘ 𝐻) → ((𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡))) ↔ ((ℎ ∘ 𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))))
442	441	spcegv 3551	. . 3 ⊢ ((ℎ ∘ 𝐻) ∈ V → (((ℎ ∘ 𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))) → ∃𝑥(𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡)))))
443	40, 422, 442	sylc 66	. 2 ⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∃𝑥(𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡))))
444	31, 443	exlimddv 1968	1 ⊢ (𝜑 → ∃𝑥(𝑥:(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∃wex 1812 Ⅎwnf 1816 ∈ wcel 2145 Ⅎwnfc 2907 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 {crab 3412 Vcvv 3450 ∖ cdif 3896 ∩ cin 3898 ⊆ wss 3899 ∅c0 4279 ∪ cuni 4867 class class class wbr 5103 ↦ cmpt 5186 dom cdm 5655 ran crn 5656 ∘ ccom 5659 Fun wfun 6527 Fn wfn 6528 ⟶wf 6529 ‘cfv 6533 (class class class)co 7414 Fincfn 8955 ℝcr 11126 0cc0 11127 1c1 11128 + caddc 11130 · cmul 11132 < clt 11270 ≤ cle 11271 − cmin 11468 / cdiv 11898 ℕcn 12260 3c3 12323 ℝ⁺crp 13045 (,)cioo 13401 ...cfz 13564 topGenctg 17525 Clsdccld 23244 Cn ccn 23452 Compccmp 23614

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7737 ax-inf2 9623 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204 ax-pre-sup 11205

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-isom 6542 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-of 7679 df-om 7864 df-1st 7987 df-2nd 7988 df-supp 8160 df-frecs 8281 df-wrecs 8312 df-recs 8361 df-rdg 8400 df-1o 8458 df-2o 8459 df-er 8699 df-map 8831 df-pm 8832 df-ixp 8908 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-fsupp 9335 df-fi 9384 df-sup 9415 df-inf 9416 df-oi 9485 df-card 9947 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-div 11899 df-nn 12261 df-2 12330 df-3 12331 df-4 12332 df-5 12333 df-6 12334 df-7 12335 df-8 12336 df-9 12337 df-n0 12532 df-z 12619 df-dec 12740 df-uz 12891 df-q 13001 df-rp 13046 df-xneg 13166 df-xadd 13167 df-xmul 13168 df-ioo 13405 df-ioc 13406 df-ico 13407 df-icc 13408 df-fz 13565 df-fzo 13713 df-fl 13856 df-seq 14069 df-exp 14129 df-hash 14398 df-cj 15189 df-re 15190 df-im 15191 df-sqrt 15325 df-abs 15326 df-clim 15578 df-rlim 15579 df-sum 15777 df-struct 17242 df-sets 17259 df-slot 17277 df-ndx 17289 df-base 17305 df-ress 17326 df-plusg 17358 df-mulr 17359 df-starv 17360 df-sca 17361 df-vsca 17362 df-ip 17363 df-tset 17364 df-ple 17365 df-ds 17367 df-unif 17368 df-hom 17369 df-cco 17370 df-rest 17510 df-topn 17511 df-0g 17529 df-gsum 17530 df-topgen 17531 df-pt 17532 df-prds 17535 df-xrs 17591 df-qtop 17596 df-imas 17597 df-xps 17599 df-mre 17673 df-mrc 17674 df-acs 17676 df-mgm 18733 df-sgrp 18824 df-mnd 18840 df-submnd 18895 df-mulg 19194 df-cntz 19447 df-cmn 19912 df-psmet 21580 df-xmet 21581 df-met 21582 df-bl 21583 df-mopn 21584 df-cnfld 21589 df-top 23122 df-topon 23139 df-topsp 23161 df-bases 23174 df-cld 23247 df-cn 23455 df-cnp 23456 df-cmp 23615 df-tx 23791 df-hmeo 23984 df-xms 24549 df-ms 24550 df-tms 24551

This theorem is used by: stoweidlem60 46891

W3C validator