| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | stoweidlem59.8 | . . . . . . . . . 10
⊢ 𝑌 = {𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)} | 
| 2 |  | nfrab1 3457 | . . . . . . . . . 10
⊢
Ⅎ𝑦{𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)} | 
| 3 | 1, 2 | nfcxfr 2903 | . . . . . . . . 9
⊢
Ⅎ𝑦𝑌 | 
| 4 |  | nfcv 2905 | . . . . . . . . 9
⊢
Ⅎ𝑧𝑌 | 
| 5 |  | nfv 1914 | . . . . . . . . 9
⊢
Ⅎ𝑧(∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)) | 
| 6 |  | nfv 1914 | . . . . . . . . 9
⊢
Ⅎ𝑦(∀𝑡 ∈ (𝐷‘𝑗)(𝑧‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑧‘𝑡)) | 
| 7 |  | fveq1 6905 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → (𝑦‘𝑡) = (𝑧‘𝑡)) | 
| 8 | 7 | breq1d 5153 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → ((𝑦‘𝑡) < (𝐸 / 𝑁) ↔ (𝑧‘𝑡) < (𝐸 / 𝑁))) | 
| 9 | 8 | ralbidv 3178 | . . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷‘𝑗)(𝑧‘𝑡) < (𝐸 / 𝑁))) | 
| 10 | 7 | breq2d 5155 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → ((1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (𝑧‘𝑡))) | 
| 11 | 10 | ralbidv 3178 | . . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑧‘𝑡))) | 
| 12 | 9, 11 | anbi12d 632 | . . . . . . . . 9
⊢ (𝑦 = 𝑧 → ((∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)) ↔ (∀𝑡 ∈ (𝐷‘𝑗)(𝑧‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑧‘𝑡)))) | 
| 13 | 3, 4, 5, 6, 12 | cbvrabw 3473 | . . . . . . . 8
⊢ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} = {𝑧 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑧‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑧‘𝑡))} | 
| 14 |  | ovexd 7466 | . . . . . . . . . 10
⊢ (𝜑 → (𝐽 Cn 𝐾) ∈ V) | 
| 15 |  | stoweidlem59.11 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ⊆ 𝐶) | 
| 16 |  | stoweidlem59.5 | . . . . . . . . . . 11
⊢ 𝐶 = (𝐽 Cn 𝐾) | 
| 17 | 15, 16 | sseqtrdi 4024 | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ⊆ (𝐽 Cn 𝐾)) | 
| 18 | 14, 17 | ssexd 5324 | . . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ V) | 
| 19 | 1, 18 | rabexd 5340 | . . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ V) | 
| 20 | 13, 19 | rabexd 5340 | . . . . . . 7
⊢ (𝜑 → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V) | 
| 21 | 20 | ralrimivw 3150 | . . . . . 6
⊢ (𝜑 → ∀𝑗 ∈ (0...𝑁){𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V) | 
| 22 |  | stoweidlem59.9 | . . . . . . 7
⊢ 𝐻 = (𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}) | 
| 23 | 22 | fnmpt 6708 | . . . . . 6
⊢
(∀𝑗 ∈
(0...𝑁){𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V → 𝐻 Fn (0...𝑁)) | 
| 24 | 21, 23 | syl 17 | . . . . 5
⊢ (𝜑 → 𝐻 Fn (0...𝑁)) | 
| 25 |  | fzfi 14013 | . . . . 5
⊢
(0...𝑁) ∈
Fin | 
| 26 |  | fnfi 9218 | . . . . 5
⊢ ((𝐻 Fn (0...𝑁) ∧ (0...𝑁) ∈ Fin) → 𝐻 ∈ Fin) | 
| 27 | 24, 25, 26 | sylancl 586 | . . . 4
⊢ (𝜑 → 𝐻 ∈ Fin) | 
| 28 |  | rnfi 9380 | . . . 4
⊢ (𝐻 ∈ Fin → ran 𝐻 ∈ Fin) | 
| 29 | 27, 28 | syl 17 | . . 3
⊢ (𝜑 → ran 𝐻 ∈ Fin) | 
| 30 |  | fnchoice 45034 | . . 3
⊢ (ran
𝐻 ∈ Fin →
∃ℎ(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) | 
| 31 | 29, 30 | syl 17 | . 2
⊢ (𝜑 → ∃ℎ(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) | 
| 32 |  | simprl 771 | . . . . 5
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ℎ Fn ran 𝐻) | 
| 33 |  | ovex 7464 | . . . . . . . 8
⊢
(0...𝑁) ∈
V | 
| 34 | 33 | mptex 7243 | . . . . . . 7
⊢ (𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}) ∈ V | 
| 35 | 22, 34 | eqeltri 2837 | . . . . . 6
⊢ 𝐻 ∈ V | 
| 36 | 35 | rnex 7932 | . . . . 5
⊢ ran 𝐻 ∈ V | 
| 37 |  | fnex 7237 | . . . . 5
⊢ ((ℎ Fn ran 𝐻 ∧ ran 𝐻 ∈ V) → ℎ ∈ V) | 
| 38 | 32, 36, 37 | sylancl 586 | . . . 4
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ℎ ∈ V) | 
| 39 |  | coexg 7951 | . . . 4
⊢ ((ℎ ∈ V ∧ 𝐻 ∈ V) → (ℎ ∘ 𝐻) ∈ V) | 
| 40 | 38, 35, 39 | sylancl 586 | . . 3
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (ℎ ∘ 𝐻) ∈ V) | 
| 41 |  | dffn3 6748 | . . . . . . 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 3284 | . . . . . . . . . . 11
⊢
Ⅎ𝑤∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) | 
| 46 | 44, 45 | nfan 1899 | . . . . . . . . . 10
⊢
Ⅎ𝑤(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)) | 
| 47 | 43, 46 | nfan 1899 | . . . . . . . . 9
⊢
Ⅎ𝑤(𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) | 
| 48 |  | simplrr 778 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)) | 
| 49 |  | simpr 484 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑤 ∈ ran 𝐻) → 𝑤 ∈ ran 𝐻) | 
| 50 |  | fvelrnb 6969 | . . . . . . . . . . . . . . . 16
⊢ (𝐻 Fn (0...𝑁) → (𝑤 ∈ ran 𝐻 ↔ ∃𝑎 ∈ (0...𝑁)(𝐻‘𝑎) = 𝑤)) | 
| 51 |  | nfv 1914 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑎(𝐻‘𝑗) = 𝑤 | 
| 52 |  | nfmpt1 5250 | . . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑗(𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}) | 
| 53 | 22, 52 | nfcxfr 2903 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑗𝐻 | 
| 54 |  | nfcv 2905 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑗𝑎 | 
| 55 | 53, 54 | nffv 6916 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑗(𝐻‘𝑎) | 
| 56 |  | nfcv 2905 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑗𝑤 | 
| 57 | 55, 56 | nfeq 2919 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑗(𝐻‘𝑎) = 𝑤 | 
| 58 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑎 → (𝐻‘𝑗) = (𝐻‘𝑎)) | 
| 59 | 58 | eqeq1d 2739 | . . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑎 → ((𝐻‘𝑗) = 𝑤 ↔ (𝐻‘𝑎) = 𝑤)) | 
| 60 | 51, 57, 59 | cbvrexw 3307 | . . . . . . . . . . . . . . . 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 1139 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ (𝐻‘𝑗) = 𝑤) → (𝐻‘𝑗) = 𝑤) | 
| 65 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ (0...𝑁)) | 
| 66 | 20 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V) | 
| 67 | 22 | fvmpt2 7027 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ (0...𝑁) ∧ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ∈ V) → (𝐻‘𝑗) = {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}) | 
| 68 | 65, 66, 67 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐻‘𝑗) = {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}) | 
| 69 |  | stoweidlem59.6 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) | 
| 70 |  | nfcv 2905 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑡(0...𝑁) | 
| 71 |  | nfrab1 3457 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑡{𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} | 
| 72 | 70, 71 | nfmpt 5249 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) | 
| 73 | 69, 72 | nfcxfr 2903 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑡𝐷 | 
| 74 |  | nfcv 2905 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑡𝑗 | 
| 75 | 73, 74 | nffv 6916 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑡(𝐷‘𝑗) | 
| 76 |  | nfcv 2905 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑡𝑇 | 
| 77 |  | stoweidlem59.7 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) | 
| 78 |  | nfrab1 3457 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
Ⅎ𝑡{𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} | 
| 79 | 70, 78 | nfmpt 5249 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) | 
| 80 | 77, 79 | nfcxfr 2903 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑡𝐵 | 
| 81 | 80, 74 | nffv 6916 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑡(𝐵‘𝑗) | 
| 82 | 76, 81 | nfdif 4129 | . . . . . . . . . . . . . . . . . . . . . . 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 7762 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → ∪ 𝐽
∈ V) | 
| 100 | 87, 99 | eqeltrid 2845 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝑇 ∈ V) | 
| 101 | 100 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑇 ∈ V) | 
| 102 |  | rabexg 5337 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V) | 
| 103 | 101, 102 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V) | 
| 104 | 77 | fvmpt2 7027 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑗 ∈ (0...𝑁) ∧ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ V) → (𝐵‘𝑗) = {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) | 
| 105 | 65, 103, 104 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐵‘𝑗) = {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) | 
| 106 |  | stoweidlem59.1 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑡𝐹 | 
| 107 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} = {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} | 
| 108 |  | elfzelz 13564 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ) | 
| 109 | 108 | zred 12722 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ) | 
| 110 |  | 3re 12346 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 3 ∈
ℝ | 
| 111 |  | 3ne0 12372 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 3 ≠
0 | 
| 112 | 110, 111 | rereccli 12032 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (1 / 3)
∈ ℝ | 
| 113 |  | readdcl 11238 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13077 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝐸 ∈ ℝ) | 
| 118 | 117 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝐸 ∈ ℝ) | 
| 119 | 115, 118 | remulcld 11291 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑗 + (1 / 3)) · 𝐸) ∈ ℝ) | 
| 120 |  | stoweidlem59.16 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝐹 ∈ 𝐶) | 
| 121 | 120, 16 | eleqtrdi 2851 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) | 
| 122 | 121 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝐹 ∈ (𝐽 Cn 𝐾)) | 
| 123 | 106, 86, 87, 107, 119, 122 | rfcnpre3 45038 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ∈ (Clsd‘𝐽)) | 
| 124 | 105, 123 | eqeltrd 2841 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐵‘𝑗) ∈ (Clsd‘𝐽)) | 
| 125 |  | rabexg 5337 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑇 ∈ V → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V) | 
| 126 | 101, 125 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V) | 
| 127 | 69 | fvmpt2 7027 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑗 ∈ (0...𝑁) ∧ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ V) → (𝐷‘𝑗) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) | 
| 128 | 65, 126, 127 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐷‘𝑗) = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)}) | 
| 129 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} | 
| 130 |  | resubcl 11573 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11291 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ) | 
| 134 | 106, 86, 87, 129, 133, 122 | rfcnpre4 45039 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑡 ∈ 𝑇 ∣ (𝐹‘𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} ∈ (Clsd‘𝐽)) | 
| 135 | 128, 134 | eqeltrd 2841 | . . . . . . . . . . . . . . . . . . . . . . 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 45030 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → 𝐹:𝑇⟶ℝ) | 
| 139 | 138 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → 𝐹:𝑇⟶ℝ) | 
| 140 |  | ssrab2 4080 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)} ⊆ 𝑇 | 
| 141 | 105, 140 | eqsstrdi 4028 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐵‘𝑗) ⊆ 𝑇) | 
| 142 | 141 | sselda 3983 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → 𝑡 ∈ 𝑇) | 
| 143 | 139, 142 | ffvelcdmd 7105 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → (𝐹‘𝑡) ∈ ℝ) | 
| 144 | 112, 130 | mpan2 691 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) ∈
ℝ) | 
| 145 |  | id 22 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑗 ∈ ℝ → 𝑗 ∈
ℝ) | 
| 146 | 112, 113 | mpan2 691 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑗 ∈ ℝ → (𝑗 + (1 / 3)) ∈
ℝ) | 
| 147 |  | 3pos 12371 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ 0 <
3 | 
| 148 | 110, 147 | recgt0ii 12174 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ 0 < (1
/ 3) | 
| 149 | 112, 148 | elrpii 13037 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (1 / 3)
∈ ℝ+ | 
| 150 |  | ltsubrp 13071 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑗 ∈ ℝ ∧ (1 / 3)
∈ ℝ+) → (𝑗 − (1 / 3)) < 𝑗) | 
| 151 | 149, 150 | mpan2 691 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑗 ∈ ℝ → (𝑗 − (1 / 3)) < 𝑗) | 
| 152 |  | ltaddrp 13072 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑗 ∈ ℝ ∧ (1 / 3)
∈ ℝ+) → 𝑗 < (𝑗 + (1 / 3))) | 
| 153 | 149, 152 | mpan2 691 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑗 ∈ ℝ → 𝑗 < (𝑗 + (1 / 3))) | 
| 154 | 144, 145,
146, 151, 153 | lttrd 11422 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 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 13083 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸)) | 
| 158 | 157 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸)) | 
| 159 |  | ltmul1 12117 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 2827 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑡 ∈ (𝐵‘𝑗) ↔ 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)})) | 
| 164 | 163 | biimpa 476 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → 𝑡 ∈ {𝑡 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹‘𝑡)}) | 
| 165 |  | rabid 3458 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 11421 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ((𝑗 − (1 / 3)) · 𝐸) < (𝐹‘𝑡)) | 
| 169 | 136, 143 | ltnled 11408 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 3458 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2864 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑡 ∈ (𝐵‘𝑗)) → ¬ 𝑡 ∈ (𝐷‘𝑗)) | 
| 176 | 175 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑡 ∈ (𝐵‘𝑗) → ¬ 𝑡 ∈ (𝐷‘𝑗))) | 
| 177 | 85, 176 | ralrimi 3257 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐵‘𝑗) ¬ 𝑡 ∈ (𝐷‘𝑗)) | 
| 178 |  | disj 4450 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐵‘𝑗) ∩ (𝐷‘𝑗)) = ∅ ↔ ∀𝑎 ∈ (𝐵‘𝑗) ¬ 𝑎 ∈ (𝐷‘𝑗)) | 
| 179 |  | nfcv 2905 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑎(𝐵‘𝑗) | 
| 180 | 75 | nfcri 2897 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
Ⅎ𝑡 𝑎 ∈ (𝐷‘𝑗) | 
| 181 | 180 | nfn 1857 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑡 ¬ 𝑎 ∈ (𝐷‘𝑗) | 
| 182 |  | nfv 1914 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑎 ¬ 𝑡 ∈ (𝐷‘𝑗) | 
| 183 |  | eleq1 2829 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑎 = 𝑡 → (𝑎 ∈ (𝐷‘𝑗) ↔ 𝑡 ∈ (𝐷‘𝑗))) | 
| 184 | 183 | notbid 318 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 = 𝑡 → (¬ 𝑎 ∈ (𝐷‘𝑗) ↔ ¬ 𝑡 ∈ (𝐷‘𝑗))) | 
| 185 | 179, 81, 181, 182, 184 | cbvralfw 3304 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∀𝑎 ∈
(𝐵‘𝑗) ¬ 𝑎 ∈ (𝐷‘𝑗) ↔ ∀𝑡 ∈ (𝐵‘𝑗) ¬ 𝑡 ∈ (𝐷‘𝑗)) | 
| 186 | 178, 185 | bitri 275 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐵‘𝑗) ∩ (𝐷‘𝑗)) = ∅ ↔ ∀𝑡 ∈ (𝐵‘𝑗) ¬ 𝑡 ∈ (𝐷‘𝑗)) | 
| 187 | 177, 186 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝐵‘𝑗) ∩ (𝐷‘𝑗)) = ∅) | 
| 188 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑇 ∖ (𝐵‘𝑗)) = (𝑇 ∖ (𝐵‘𝑗)) | 
| 189 |  | stoweidlem59.19 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 190 | 189 | nnrpd 13075 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑁 ∈
ℝ+) | 
| 191 | 116, 190 | rpdivcld 13094 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝐸 / 𝑁) ∈
ℝ+) | 
| 192 | 191 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐸 / 𝑁) ∈
ℝ+) | 
| 193 | 117, 189 | nndivred 12320 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℝ) | 
| 194 | 112 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (1 / 3) ∈
ℝ) | 
| 195 | 189 | nnge1d 12314 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 1 ≤ 𝑁) | 
| 196 |  | 1re 11261 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 1 ∈
ℝ | 
| 197 |  | 0lt1 11785 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ 0 <
1 | 
| 198 | 196, 197 | pm3.2i 470 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (1 ∈
ℝ ∧ 0 < 1) | 
| 199 | 198 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (1 ∈ ℝ ∧ 0
< 1)) | 
| 200 | 189 | nnred 12281 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 201 | 189 | nngt0d 12315 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 0 < 𝑁) | 
| 202 |  | lediv2 12158 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13079 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝐸 ∈ ℂ) | 
| 206 | 205 | div1d 12035 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐸 / 1) = 𝐸) | 
| 207 | 204, 206 | breqtrd 5169 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝐸 / 𝑁) ≤ 𝐸) | 
| 208 |  | stoweidlem59.18 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝐸 < (1 / 3)) | 
| 209 | 193, 117,
194, 207, 208 | lelttrd 11419 | . . . . . . . . . . . . . . . . . . . . . . . 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 46073 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))) | 
| 212 |  | df-rex 3071 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(∃𝑥 ∈
𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) | 
| 213 | 211, 212 | sylib 218 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ∃𝑥(𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) | 
| 214 |  | simprl 771 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → 𝑥 ∈ 𝐴) | 
| 215 |  | simprr1 1222 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑥 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1)) | 
| 216 |  | fveq1 6905 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 = 𝑥 → (𝑦‘𝑡) = (𝑥‘𝑡)) | 
| 217 | 216 | breq2d 5155 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 = 𝑥 → (0 ≤ (𝑦‘𝑡) ↔ 0 ≤ (𝑥‘𝑡))) | 
| 218 | 216 | breq1d 5153 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 = 𝑥 → ((𝑦‘𝑡) ≤ 1 ↔ (𝑥‘𝑡) ≤ 1)) | 
| 219 | 217, 218 | anbi12d 632 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 = 𝑥 → ((0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ↔ (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1))) | 
| 220 | 219 | ralbidv 3178 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = 𝑥 → (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1))) | 
| 221 | 220, 1 | elrab2 3695 | . . . . . . . . . . . . . . . . . . . . . . . . 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 2905 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑦𝑥 | 
| 227 |  | nfv 1914 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑦(∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)) | 
| 228 | 216 | breq1d 5153 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 = 𝑥 → ((𝑦‘𝑡) < (𝐸 / 𝑁) ↔ (𝑥‘𝑡) < (𝐸 / 𝑁))) | 
| 229 | 228 | ralbidv 3178 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = 𝑥 → (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁))) | 
| 230 | 216 | breq2d 5155 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 = 𝑥 → ((1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))) | 
| 231 | 230 | ralbidv 3178 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = 𝑥 → (∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡))) | 
| 232 | 229, 231 | anbi12d 632 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = 𝑥 → ((∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)) ↔ (∀𝑡 ∈ (𝐷‘𝑗)(𝑥‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑥‘𝑡)))) | 
| 233 | 226, 3, 227, 232 | elrabf 3688 | . . . . . . . . . . . . . . . . . . . . . . . 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 4341 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ≠ ∅) | 
| 239 | 238 | exlimiv 1930 | . . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑥 𝑥 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ≠ ∅) | 
| 240 | 237, 239 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ≠ ∅) | 
| 241 | 68, 240 | eqnetrd 3008 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐻‘𝑗) ≠ ∅) | 
| 242 | 241 | 3adant3 1133 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ (𝐻‘𝑗) = 𝑤) → (𝐻‘𝑗) ≠ ∅) | 
| 243 | 64, 242 | eqnetrrd 3009 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁) ∧ (𝐻‘𝑗) = 𝑤) → 𝑤 ≠ ∅) | 
| 244 | 243 | 3exp 1120 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑗 ∈ (0...𝑁) → ((𝐻‘𝑗) = 𝑤 → 𝑤 ≠ ∅))) | 
| 245 | 244 | rexlimdv 3153 | . . . . . . . . . . . . . 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 3247 | . . . . . . . . . . 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 3257 | . . . . . . . 8
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∀𝑤 ∈ ran 𝐻(ℎ‘𝑤) ∈ 𝑤) | 
| 253 |  | chfnrn 7069 | . . . . . . . 8
⊢ ((ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(ℎ‘𝑤) ∈ 𝑤) → ran ℎ ⊆ ∪ ran
𝐻) | 
| 254 | 32, 252, 253 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ran ℎ ⊆ ∪ ran
𝐻) | 
| 255 |  | nfv 1914 | . . . . . . . . . 10
⊢
Ⅎ𝑦𝜑 | 
| 256 |  | nfcv 2905 | . . . . . . . . . . . 12
⊢
Ⅎ𝑦ℎ | 
| 257 |  | nfcv 2905 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦(0...𝑁) | 
| 258 |  | nfrab1 3457 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦{𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} | 
| 259 | 257, 258 | nfmpt 5249 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑦(𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}) | 
| 260 | 22, 259 | nfcxfr 2903 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑦𝐻 | 
| 261 | 260 | nfrn 5963 | . . . . . . . . . . . 12
⊢
Ⅎ𝑦ran
𝐻 | 
| 262 | 256, 261 | nffn 6667 | . . . . . . . . . . 11
⊢
Ⅎ𝑦 ℎ Fn ran 𝐻 | 
| 263 |  | nfv 1914 | . . . . . . . . . . . 12
⊢
Ⅎ𝑦(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) | 
| 264 | 261, 263 | nfralw 3311 | . . . . . . . . . . 11
⊢
Ⅎ𝑦∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) | 
| 265 | 262, 264 | nfan 1899 | . . . . . . . . . 10
⊢
Ⅎ𝑦(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)) | 
| 266 | 255, 265 | nfan 1899 | . . . . . . . . 9
⊢
Ⅎ𝑦(𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) | 
| 267 | 261 | nfuni 4914 | . . . . . . . . 9
⊢
Ⅎ𝑦∪ ran 𝐻 | 
| 268 |  | fnunirn 7274 | . . . . . . . . . . . . . . 15
⊢ (𝐻 Fn (0...𝑁) → (𝑦 ∈ ∪ ran
𝐻 ↔ ∃𝑧 ∈ (0...𝑁)𝑦 ∈ (𝐻‘𝑧))) | 
| 269 |  | nfcv 2905 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑗𝑧 | 
| 270 | 53, 269 | nffv 6916 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑗(𝐻‘𝑧) | 
| 271 | 270 | nfcri 2897 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑗 𝑦 ∈ (𝐻‘𝑧) | 
| 272 |  | nfv 1914 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑧 𝑦 ∈ (𝐻‘𝑗) | 
| 273 |  | fveq2 6906 | . . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑗 → (𝐻‘𝑧) = (𝐻‘𝑗)) | 
| 274 | 273 | eleq2d 2827 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑗 → (𝑦 ∈ (𝐻‘𝑧) ↔ 𝑦 ∈ (𝐻‘𝑗))) | 
| 275 | 271, 272,
274 | cbvrexw 3307 | . . . . . . . . . . . . . . 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 5963 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑗ran
𝐻 | 
| 281 | 280 | nfuni 4914 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑗∪ ran 𝐻 | 
| 282 | 281 | nfcri 2897 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑗 𝑦 ∈ ∪ ran 𝐻 | 
| 283 | 279, 282 | nfan 1899 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑗(𝜑 ∧ 𝑦 ∈ ∪ ran
𝐻) | 
| 284 |  | nfv 1914 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑗 𝑦 ∈ 𝑌 | 
| 285 |  | simp1l 1198 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ∪ ran
𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝜑) | 
| 286 |  | simp2 1138 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ∪ ran
𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑗 ∈ (0...𝑁)) | 
| 287 |  | simp3 1139 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ∪ ran
𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ (𝐻‘𝑗)) | 
| 288 | 68 | eleq2d 2827 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑦 ∈ (𝐻‘𝑗) ↔ 𝑦 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))})) | 
| 289 | 288 | biimpa 476 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}) | 
| 290 |  | rabid 3458 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} ↔ (𝑦 ∈ 𝑌 ∧ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)))) | 
| 291 | 289, 290 | sylib 218 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → (𝑦 ∈ 𝑌 ∧ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)))) | 
| 292 | 291 | simpld 494 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ 𝑌) | 
| 293 | 285, 286,
287, 292 | syl21anc 838 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ∪ ran
𝐻) ∧ 𝑗 ∈ (0...𝑁) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ 𝑌) | 
| 294 | 293 | 3exp 1120 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ∪ ran
𝐻) → (𝑗 ∈ (0...𝑁) → (𝑦 ∈ (𝐻‘𝑗) → 𝑦 ∈ 𝑌))) | 
| 295 | 283, 284,
294 | rexlimd 3266 | . . . . . . . . . . . 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 3988 | . . . . . . . 8
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∪ ran
𝐻 ⊆ 𝑌) | 
| 300 |  | ssrab2 4080 | . . . . . . . . 9
⊢ {𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)} ⊆ 𝐴 | 
| 301 | 1, 300 | eqsstri 4030 | . . . . . . . 8
⊢ 𝑌 ⊆ 𝐴 | 
| 302 | 299, 301 | sstrdi 3996 | . . . . . . 7
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∪ ran
𝐻 ⊆ 𝐴) | 
| 303 | 254, 302 | sstrd 3994 | . . . . . 6
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ran ℎ ⊆ 𝐴) | 
| 304 | 42, 303 | fssd 6753 | . . . . 5
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ℎ:ran 𝐻⟶𝐴) | 
| 305 |  | dffn3 6748 | . . . . . . 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 6760 | . . . . 5
⊢ ((ℎ:ran 𝐻⟶𝐴 ∧ 𝐻:(0...𝑁)⟶ran 𝐻) → (ℎ ∘ 𝐻):(0...𝑁)⟶𝐴) | 
| 309 | 304, 307,
308 | syl2anc 584 | . . . 4
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (ℎ ∘ 𝐻):(0...𝑁)⟶𝐴) | 
| 310 |  | nfcv 2905 | . . . . . . . 8
⊢
Ⅎ𝑗ℎ | 
| 311 | 310, 280 | nffn 6667 | . . . . . . 7
⊢
Ⅎ𝑗 ℎ Fn ran 𝐻 | 
| 312 |  | nfv 1914 | . . . . . . . 8
⊢
Ⅎ𝑗(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) | 
| 313 | 280, 312 | nfralw 3311 | . . . . . . 7
⊢
Ⅎ𝑗∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) | 
| 314 | 311, 313 | nfan 1899 | . . . . . 6
⊢
Ⅎ𝑗(ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)) | 
| 315 | 279, 314 | nfan 1899 | . . . . 5
⊢
Ⅎ𝑗(𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) | 
| 316 |  | simpll 767 | . . . . . . . . . 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 7006 | . . . . . . . . . . . 12
⊢ ((𝐻 Fn (0...𝑁) ∧ 𝑗 ∈ (0...𝑁)) → ((ℎ ∘ 𝐻)‘𝑗) = (ℎ‘(𝐻‘𝑗))) | 
| 320 | 318, 319 | sylancom 588 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((ℎ ∘ 𝐻)‘𝑗) = (ℎ‘(𝐻‘𝑗))) | 
| 321 |  | simplrr 778 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤)) | 
| 322 |  | fnfun 6668 | . . . . . . . . . . . . . . . 16
⊢ (𝐻 Fn (0...𝑁) → Fun 𝐻) | 
| 323 | 24, 322 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → Fun 𝐻) | 
| 324 | 323 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → Fun 𝐻) | 
| 325 | 24 | fndmd 6673 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom 𝐻 = (0...𝑁)) | 
| 326 | 325 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → dom 𝐻 = (0...𝑁)) | 
| 327 | 65, 326 | eleqtrrd 2844 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ dom 𝐻) | 
| 328 | 327 | adantlr 715 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ dom 𝐻) | 
| 329 |  | fvelrn 7096 | . . . . . . . . . . . . . 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 3003 | . . . . . . . . . . . . . 14
⊢ (𝑤 = (𝐻‘𝑗) → (𝑤 ≠ ∅ ↔ (𝐻‘𝑗) ≠ ∅)) | 
| 334 |  | fveq2 6906 | . . . . . . . . . . . . . . 15
⊢ (𝑤 = (𝐻‘𝑗) → (ℎ‘𝑤) = (ℎ‘(𝐻‘𝑗))) | 
| 335 |  | id 22 | . . . . . . . . . . . . . . 15
⊢ (𝑤 = (𝐻‘𝑗) → 𝑤 = (𝐻‘𝑗)) | 
| 336 | 334, 335 | eleq12d 2835 | . . . . . . . . . . . . . 14
⊢ (𝑤 = (𝐻‘𝑗) → ((ℎ‘𝑤) ∈ 𝑤 ↔ (ℎ‘(𝐻‘𝑗)) ∈ (𝐻‘𝑗))) | 
| 337 | 333, 336 | imbi12d 344 | . . . . . . . . . . . . 13
⊢ (𝑤 = (𝐻‘𝑗) → ((𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) ↔ ((𝐻‘𝑗) ≠ ∅ → (ℎ‘(𝐻‘𝑗)) ∈ (𝐻‘𝑗)))) | 
| 338 | 337 | rspccva 3621 | . . . . . . . . . . . 12
⊢
((∀𝑤 ∈
ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤) ∧ (𝐻‘𝑗) ∈ ran 𝐻) → ((𝐻‘𝑗) ≠ ∅ → (ℎ‘(𝐻‘𝑗)) ∈ (𝐻‘𝑗))) | 
| 339 | 331, 332,
338 | sylc 65 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (ℎ‘(𝐻‘𝑗)) ∈ (𝐻‘𝑗)) | 
| 340 | 320, 339 | eqeltrd 2841 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) | 
| 341 | 256, 260 | nfco 5876 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑦(ℎ ∘ 𝐻) | 
| 342 |  | nfcv 2905 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑦𝑗 | 
| 343 | 341, 342 | nffv 6916 | . . . . . . . . . . . 12
⊢
Ⅎ𝑦((ℎ ∘ 𝐻)‘𝑗) | 
| 344 |  | nfv 1914 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑦(𝜑 ∧ 𝑗 ∈ (0...𝑁)) | 
| 345 | 260, 342 | nffv 6916 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦(𝐻‘𝑗) | 
| 346 | 343, 345 | nfel 2920 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑦((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗) | 
| 347 | 344, 346 | nfan 1899 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑦((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) | 
| 348 | 343, 3 | nfel 2920 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑦((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌 | 
| 349 | 347, 348 | nfim 1896 | . . . . . . . . . . . 12
⊢
Ⅎ𝑦(((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌) | 
| 350 |  | eleq1 2829 | . . . . . . . . . . . . . 14
⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (𝑦 ∈ (𝐻‘𝑗) ↔ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗))) | 
| 351 | 350 | anbi2d 630 | . . . . . . . . . . . . 13
⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) ↔ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)))) | 
| 352 |  | eleq1 2829 | . . . . . . . . . . . . 13
⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (𝑦 ∈ 𝑌 ↔ ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌)) | 
| 353 | 351, 352 | imbi12d 344 | . . . . . . . . . . . 12
⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑦 ∈ (𝐻‘𝑗)) → 𝑦 ∈ 𝑌) ↔ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌))) | 
| 354 | 343, 349,
353, 292 | vtoclgf 3569 | . . . . . . . . . . 11
⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗) → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌)) | 
| 355 | 354 | anabsi7 671 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌) | 
| 356 | 316, 317,
340, 355 | syl21anc 838 | . . . . . . . . 9
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌) | 
| 357 | 1 | eleq2i 2833 | . . . . . . . . . 10
⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ 𝑌 ↔ ((ℎ ∘ 𝐻)‘𝑗) ∈ {𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)}) | 
| 358 |  | nfcv 2905 | . . . . . . . . . . 11
⊢
Ⅎ𝑦𝐴 | 
| 359 |  | nfcv 2905 | . . . . . . . . . . . 12
⊢
Ⅎ𝑦𝑇 | 
| 360 |  | nfcv 2905 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑦0 | 
| 361 |  | nfcv 2905 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑦
≤ | 
| 362 |  | nfcv 2905 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦𝑡 | 
| 363 | 343, 362 | nffv 6916 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑦(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) | 
| 364 | 360, 361,
363 | nfbr 5190 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑦0 ≤
(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) | 
| 365 |  | nfcv 2905 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑦1 | 
| 366 | 363, 361,
365 | nfbr 5190 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑦(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1 | 
| 367 | 364, 366 | nfan 1899 | . . . . . . . . . . . 12
⊢
Ⅎ𝑦(0 ≤
(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) | 
| 368 | 359, 367 | nfralw 3311 | . . . . . . . . . . 11
⊢
Ⅎ𝑦∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) | 
| 369 |  | nfcv 2905 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑡𝑦 | 
| 370 |  | nfcv 2905 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑡ℎ | 
| 371 |  | nfra1 3284 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑡∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) | 
| 372 |  | nfra1 3284 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑡∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) | 
| 373 | 371, 372 | nfan 1899 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡(∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡)) | 
| 374 |  | nfra1 3284 | . . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑡∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) | 
| 375 |  | nfcv 2905 | . . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑡𝐴 | 
| 376 | 374, 375 | nfrabw 3475 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑡{𝑦 ∈ 𝐴 ∣ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)} | 
| 377 | 1, 376 | nfcxfr 2903 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑡𝑌 | 
| 378 | 373, 377 | nfrabw 3475 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑡{𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))} | 
| 379 | 70, 378 | nfmpt 5249 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑦 ∈ 𝑌 ∣ (∀𝑡 ∈ (𝐷‘𝑗)(𝑦‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (𝑦‘𝑡))}) | 
| 380 | 22, 379 | nfcxfr 2903 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑡𝐻 | 
| 381 | 370, 380 | nfco 5876 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑡(ℎ ∘ 𝐻) | 
| 382 | 381, 74 | nffv 6916 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑡((ℎ ∘ 𝐻)‘𝑗) | 
| 383 | 369, 382 | nfeq 2919 | . . . . . . . . . . . 12
⊢
Ⅎ𝑡 𝑦 = ((ℎ ∘ 𝐻)‘𝑗) | 
| 384 |  | fveq1 6905 | . . . . . . . . . . . . . 14
⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (𝑦‘𝑡) = (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)) | 
| 385 | 384 | breq2d 5155 | . . . . . . . . . . . . 13
⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (0 ≤ (𝑦‘𝑡) ↔ 0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))) | 
| 386 | 384 | breq1d 5153 | . . . . . . . . . . . . 13
⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((𝑦‘𝑡) ≤ 1 ↔ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)) | 
| 387 | 385, 386 | anbi12d 632 | . . . . . . . . . . . 12
⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ↔ (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1))) | 
| 388 | 383, 387 | ralbid 3273 | . . . . . . . . . . 11
⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1))) | 
| 389 | 343, 358,
368, 388 | elrabf 3688 | . . . . . . . . . 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 2905 | . . . . . . . . . . . 12
⊢
Ⅎ𝑦(𝐷‘𝑗) | 
| 394 |  | nfcv 2905 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑦
< | 
| 395 |  | nfcv 2905 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑦(𝐸 / 𝑁) | 
| 396 | 363, 394,
395 | nfbr 5190 | . . . . . . . . . . . 12
⊢
Ⅎ𝑦(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) | 
| 397 | 393, 396 | nfralw 3311 | . . . . . . . . . . 11
⊢
Ⅎ𝑦∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) | 
| 398 | 347, 397 | nfim 1896 | . . . . . . . . . 10
⊢
Ⅎ𝑦(((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)) | 
| 399 | 384 | breq1d 5153 | . . . . . . . . . . . 12
⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((𝑦‘𝑡) < (𝐸 / 𝑁) ↔ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))) | 
| 400 | 383, 399 | ralbid 3273 | . . . . . . . . . . 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 3569 | . . . . . . . . 9
⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗) → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))) | 
| 405 | 404 | anabsi7 671 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)) | 
| 406 | 316, 317,
340, 405 | syl21anc 838 | . . . . . . 7
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁)) | 
| 407 |  | nfcv 2905 | . . . . . . . . . . . 12
⊢
Ⅎ𝑦(𝐵‘𝑗) | 
| 408 |  | nfcv 2905 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑦(1
− (𝐸 / 𝑁)) | 
| 409 | 408, 394,
363 | nfbr 5190 | . . . . . . . . . . . 12
⊢
Ⅎ𝑦(1 −
(𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) | 
| 410 | 407, 409 | nfralw 3311 | . . . . . . . . . . 11
⊢
Ⅎ𝑦∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) | 
| 411 | 347, 410 | nfim 1896 | . . . . . . . . . 10
⊢
Ⅎ𝑦(((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)) | 
| 412 | 384 | breq2d 5155 | . . . . . . . . . . . 12
⊢ (𝑦 = ((ℎ ∘ 𝐻)‘𝑗) → ((1 − (𝐸 / 𝑁)) < (𝑦‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))) | 
| 413 | 383, 412 | ralbid 3273 | . . . . . . . . . . 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 3569 | . . . . . . . . 9
⊢ (((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗) → (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))) | 
| 417 | 416 | anabsi7 671 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((ℎ ∘ 𝐻)‘𝑗) ∈ (𝐻‘𝑗)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)) | 
| 418 | 316, 317,
340, 417 | syl21anc 838 | . . . . . . 7
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)) | 
| 419 | 392, 406,
418 | 3jca 1129 | . . . . . 6
⊢ (((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) ∧ 𝑗 ∈ (0...𝑁)) → (∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))) | 
| 420 | 419 | ex 412 | . . . . 5
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → (𝑗 ∈ (0...𝑁) → (∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))) | 
| 421 | 315, 420 | ralrimi 3257 | . . . 4
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))) | 
| 422 | 309, 421 | jca 511 | . . 3
⊢ ((𝜑 ∧ (ℎ Fn ran 𝐻 ∧ ∀𝑤 ∈ ran 𝐻(𝑤 ≠ ∅ → (ℎ‘𝑤) ∈ 𝑤))) → ((ℎ ∘ 𝐻):(0...𝑁)⟶𝐴 ∧ ∀𝑗 ∈ (0...𝑁)(∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))) | 
| 423 |  | feq1 6716 | . . . . 5
⊢ (𝑥 = (ℎ ∘ 𝐻) → (𝑥:(0...𝑁)⟶𝐴 ↔ (ℎ ∘ 𝐻):(0...𝑁)⟶𝐴)) | 
| 424 |  | nfcv 2905 | . . . . . . 7
⊢
Ⅎ𝑗𝑥 | 
| 425 | 310, 53 | nfco 5876 | . . . . . . 7
⊢
Ⅎ𝑗(ℎ ∘ 𝐻) | 
| 426 | 424, 425 | nfeq 2919 | . . . . . 6
⊢
Ⅎ𝑗 𝑥 = (ℎ ∘ 𝐻) | 
| 427 |  | nfcv 2905 | . . . . . . . . 9
⊢
Ⅎ𝑡𝑥 | 
| 428 | 427, 381 | nfeq 2919 | . . . . . . . 8
⊢
Ⅎ𝑡 𝑥 = (ℎ ∘ 𝐻) | 
| 429 |  | fveq1 6905 | . . . . . . . . . . 11
⊢ (𝑥 = (ℎ ∘ 𝐻) → (𝑥‘𝑗) = ((ℎ ∘ 𝐻)‘𝑗)) | 
| 430 | 429 | fveq1d 6908 | . . . . . . . . . 10
⊢ (𝑥 = (ℎ ∘ 𝐻) → ((𝑥‘𝑗)‘𝑡) = (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)) | 
| 431 | 430 | breq2d 5155 | . . . . . . . . 9
⊢ (𝑥 = (ℎ ∘ 𝐻) → (0 ≤ ((𝑥‘𝑗)‘𝑡) ↔ 0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))) | 
| 432 | 430 | breq1d 5153 | . . . . . . . . 9
⊢ (𝑥 = (ℎ ∘ 𝐻) → (((𝑥‘𝑗)‘𝑡) ≤ 1 ↔ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1)) | 
| 433 | 431, 432 | anbi12d 632 | . . . . . . . 8
⊢ (𝑥 = (ℎ ∘ 𝐻) → ((0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ↔ (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1))) | 
| 434 | 428, 433 | ralbid 3273 | . . . . . . 7
⊢ (𝑥 = (ℎ ∘ 𝐻) → (∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1))) | 
| 435 | 430 | breq1d 5153 | . . . . . . . 8
⊢ (𝑥 = (ℎ ∘ 𝐻) → (((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))) | 
| 436 | 428, 435 | ralbid 3273 | . . . . . . 7
⊢ (𝑥 = (ℎ ∘ 𝐻) → (∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ↔ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁))) | 
| 437 | 430 | breq2d 5155 | . . . . . . . 8
⊢ (𝑥 = (ℎ ∘ 𝐻) → ((1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))) | 
| 438 | 428, 437 | ralbid 3273 | . . . . . . 7
⊢ (𝑥 = (ℎ ∘ 𝐻) → (∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡) ↔ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡))) | 
| 439 | 434, 436,
438 | 3anbi123d 1438 | . . . . . 6
⊢ (𝑥 = (ℎ ∘ 𝐻) → ((∀𝑡 ∈ 𝑇 (0 ≤ ((𝑥‘𝑗)‘𝑡) ∧ ((𝑥‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)((𝑥‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ∧ (((ℎ ∘ 𝐻)‘𝑗)‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ (𝐷‘𝑗)(((ℎ ∘ 𝐻)‘𝑗)‘𝑡) < (𝐸 / 𝑁) ∧ ∀𝑡 ∈ (𝐵‘𝑗)(1 − (𝐸 / 𝑁)) < (((ℎ ∘ 𝐻)‘𝑗)‘𝑡)))) | 
| 440 | 426, 439 | ralbid 3273 | . . . . 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 3597 | . . 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 − (𝐸 / 𝑁)) < ((𝑥‘𝑗)‘𝑡)))) |