Metamath Proof Explorer

Theorem stoweidlem59

Description: This lemma proves that there exists a function x 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 D is used to represent A in the paper (because A is used for the subalgebra of functions), E is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses 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 stoweidlem59 ( 𝜑 → ∃ 𝑥 ( 𝑥 : ( 0 ... 𝑁 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑁 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem59.1 ⊢ Ⅎ 𝑡 𝐹
2 stoweidlem59.2 ⊢ Ⅎ 𝑡 𝜑
3 stoweidlem59.3 ⊢ 𝐾 = ( topGen ‘ ran (,) )
4 stoweidlem59.4 ⊢ 𝑇 = ∪ 𝐽
5 stoweidlem59.5 ⊢ 𝐶 = ( 𝐽 Cn 𝐾 )
6 stoweidlem59.6 ⊢ 𝐷 = ( 𝑗 ∈ ( 0 ... 𝑁 ) ↦ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } )
7 stoweidlem59.7 ⊢ 𝐵 = ( 𝑗 ∈ ( 0 ... 𝑁 ) ↦ { 𝑡 ∈ 𝑇 ∣ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } )
8 stoweidlem59.8 ⊢ 𝑌 = { 𝑦 ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) }
9 stoweidlem59.9 ⊢ 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑁 ) ↦ { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) } )
10 stoweidlem59.10 ⊢ ( 𝜑 → 𝐽 ∈ Comp )
11 stoweidlem59.11 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
12 stoweidlem59.12 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
13 stoweidlem59.13 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
14 stoweidlem59.14 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑦 ) ∈ 𝐴 )
15 stoweidlem59.15 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
16 stoweidlem59.16 ⊢ ( 𝜑 → 𝐹 ∈ 𝐶 )
17 stoweidlem59.17 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
18 stoweidlem59.18 ⊢ ( 𝜑 → 𝐸 < ( 1 / 3 ) )
19 stoweidlem59.19 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
20 nfrab1 ⊢ Ⅎ 𝑦 { 𝑦 ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) }
21 8 20 nfcxfr ⊢ Ⅎ 𝑦 𝑌
22 nfcv ⊢ Ⅎ 𝑧 𝑌
23 nfv ⊢ Ⅎ 𝑧 ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) )
24 nfv ⊢ Ⅎ 𝑦 ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑧 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑧 ‘ 𝑡 ) )
25 fveq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ‘ 𝑡 ) = ( 𝑧 ‘ 𝑡 ) )
26 25 breq1d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ↔ ( 𝑧 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ) )
27 26 ralbidv ⊢ ( 𝑦 = 𝑧 → ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ↔ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑧 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ) )
28 25 breq2d ⊢ ( 𝑦 = 𝑧 → ( ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ↔ ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑧 ‘ 𝑡 ) ) )
29 28 ralbidv ⊢ ( 𝑦 = 𝑧 → ( ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ↔ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑧 ‘ 𝑡 ) ) )
30 27 29 anbi12d ⊢ ( 𝑦 = 𝑧 → ( ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) ↔ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑧 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑧 ‘ 𝑡 ) ) ) )
31 21 22 23 24 30 cbvrabw ⊢ { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) } = { 𝑧 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑧 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑧 ‘ 𝑡 ) ) }
32 ovexd ⊢ ( 𝜑 → ( 𝐽 Cn 𝐾 ) ∈ V )
33 11 5 sseqtrdi ⊢ ( 𝜑 → 𝐴 ⊆ ( 𝐽 Cn 𝐾 ) )
34 32 33 ssexd ⊢ ( 𝜑 → 𝐴 ∈ V )
35 8 34 rabexd ⊢ ( 𝜑 → 𝑌 ∈ V )
36 31 35 rabexd ⊢ ( 𝜑 → { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) } ∈ V )
37 36 ralrimivw ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( 0 ... 𝑁 ) { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) } ∈ V )
38 9 fnmpt ⊢ ( ∀ 𝑗 ∈ ( 0 ... 𝑁 ) { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) } ∈ V → 𝐻 Fn ( 0 ... 𝑁 ) )
39 37 38 syl ⊢ ( 𝜑 → 𝐻 Fn ( 0 ... 𝑁 ) )
40 fzfi ⊢ ( 0 ... 𝑁 ) ∈ Fin
41 fnfi ⊢ ( ( 𝐻 Fn ( 0 ... 𝑁 ) ∧ ( 0 ... 𝑁 ) ∈ Fin ) → 𝐻 ∈ Fin )
42 39 40 41 sylancl ⊢ ( 𝜑 → 𝐻 ∈ Fin )
43 rnfi ⊢ ( 𝐻 ∈ Fin → ran 𝐻 ∈ Fin )
44 42 43 syl ⊢ ( 𝜑 → ran 𝐻 ∈ Fin )
45 fnchoice ⊢ ( ran 𝐻 ∈ Fin → ∃ ℎ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) )
46 44 45 syl ⊢ ( 𝜑 → ∃ ℎ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) )
47 simprl ⊢ ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) → ℎ Fn ran 𝐻 )
48 ovex ⊢ ( 0 ... 𝑁 ) ∈ V
49 48 mptex ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) ↦ { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) } ) ∈ V
50 9 49 eqeltri ⊢ 𝐻 ∈ V
51 50 rnex ⊢ ran 𝐻 ∈ V
52 fnex ⊢ ( ( ℎ Fn ran 𝐻 ∧ ran 𝐻 ∈ V ) → ℎ ∈ V )
53 47 51 52 sylancl ⊢ ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) → ℎ ∈ V )
54 coexg ⊢ ( ( ℎ ∈ V ∧ 𝐻 ∈ V ) → ( ℎ ∘ 𝐻 ) ∈ V )
55 53 50 54 sylancl ⊢ ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) → ( ℎ ∘ 𝐻 ) ∈ V )
56 dffn3 ⊢ ( ℎ Fn ran 𝐻 ↔ ℎ : ran 𝐻 ⟶ ran ℎ )
57 47 56 sylib ⊢ ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) → ℎ : ran 𝐻 ⟶ ran ℎ )
58 nfv ⊢ Ⅎ 𝑤 𝜑
59 nfv ⊢ Ⅎ 𝑤 ℎ Fn ran 𝐻
60 nfra1 ⊢ Ⅎ 𝑤 ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 )
61 59 60 nfan ⊢ Ⅎ 𝑤 ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) )
62 58 61 nfan ⊢ Ⅎ 𝑤 ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) )
63 simplrr ⊢ ( ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) ∧ 𝑤 ∈ ran 𝐻 ) → ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) )
64 simpr ⊢ ( ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) ∧ 𝑤 ∈ ran 𝐻 ) → 𝑤 ∈ ran 𝐻 )
65 fvelrnb ⊢ ( 𝐻 Fn ( 0 ... 𝑁 ) → ( 𝑤 ∈ ran 𝐻 ↔ ∃ 𝑎 ∈ ( 0 ... 𝑁 ) ( 𝐻 ‘ 𝑎 ) = 𝑤 ) )
66 nfv ⊢ Ⅎ 𝑎 ( 𝐻 ‘ 𝑗 ) = 𝑤
67 nfmpt1 ⊢ Ⅎ 𝑗 ( 𝑗 ∈ ( 0 ... 𝑁 ) ↦ { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) } )
68 9 67 nfcxfr ⊢ Ⅎ 𝑗 𝐻
69 nfcv ⊢ Ⅎ 𝑗 𝑎
70 68 69 nffv ⊢ Ⅎ 𝑗 ( 𝐻 ‘ 𝑎 )
71 nfcv ⊢ Ⅎ 𝑗 𝑤
72 70 71 nfeq ⊢ Ⅎ 𝑗 ( 𝐻 ‘ 𝑎 ) = 𝑤
73 fveq2 ⊢ ( 𝑗 = 𝑎 → ( 𝐻 ‘ 𝑗 ) = ( 𝐻 ‘ 𝑎 ) )
74 73 eqeq1d ⊢ ( 𝑗 = 𝑎 → ( ( 𝐻 ‘ 𝑗 ) = 𝑤 ↔ ( 𝐻 ‘ 𝑎 ) = 𝑤 ) )
75 66 72 74 cbvrexw ⊢ ( ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝐻 ‘ 𝑗 ) = 𝑤 ↔ ∃ 𝑎 ∈ ( 0 ... 𝑁 ) ( 𝐻 ‘ 𝑎 ) = 𝑤 )
76 65 75 bitr4di ⊢ ( 𝐻 Fn ( 0 ... 𝑁 ) → ( 𝑤 ∈ ran 𝐻 ↔ ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝐻 ‘ 𝑗 ) = 𝑤 ) )
77 39 76 syl ⊢ ( 𝜑 → ( 𝑤 ∈ ran 𝐻 ↔ ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝐻 ‘ 𝑗 ) = 𝑤 ) )
78 77 biimpa ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐻 ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝐻 ‘ 𝑗 ) = 𝑤 )
79 simp3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ ( 𝐻 ‘ 𝑗 ) = 𝑤 ) → ( 𝐻 ‘ 𝑗 ) = 𝑤 )
80 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
81 36 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) } ∈ V )
82 9 fvmpt2 ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) } ∈ V ) → ( 𝐻 ‘ 𝑗 ) = { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) } )
83 80 81 82 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝐻 ‘ 𝑗 ) = { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) } )
84 nfcv ⊢ Ⅎ 𝑡 ( 0 ... 𝑁 )
85 nfrab1 ⊢ Ⅎ 𝑡 { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) }
86 84 85 nfmpt ⊢ Ⅎ 𝑡 ( 𝑗 ∈ ( 0 ... 𝑁 ) ↦ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } )
87 6 86 nfcxfr ⊢ Ⅎ 𝑡 𝐷
88 nfcv ⊢ Ⅎ 𝑡 𝑗
89 87 88 nffv ⊢ Ⅎ 𝑡 ( 𝐷 ‘ 𝑗 )
90 nfcv ⊢ Ⅎ 𝑡 𝑇
91 nfrab1 ⊢ Ⅎ 𝑡 { 𝑡 ∈ 𝑇 ∣ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) }
92 84 91 nfmpt ⊢ Ⅎ 𝑡 ( 𝑗 ∈ ( 0 ... 𝑁 ) ↦ { 𝑡 ∈ 𝑇 ∣ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } )
93 7 92 nfcxfr ⊢ Ⅎ 𝑡 𝐵
94 93 88 nffv ⊢ Ⅎ 𝑡 ( 𝐵 ‘ 𝑗 )
95 90 94 nfdif ⊢ Ⅎ 𝑡 ( 𝑇 ∖ ( 𝐵 ‘ 𝑗 ) )
96 nfv ⊢ Ⅎ 𝑡 𝑗 ∈ ( 0 ... 𝑁 )
97 2 96 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) )
98 10 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝐽 ∈ Comp )
99 11 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝐴 ⊆ 𝐶 )
100 12 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
101 13 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
102 14 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑦 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑦 ) ∈ 𝐴 )
103 15 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
104 10 uniexd ⊢ ( 𝜑 → ∪ 𝐽 ∈ V )
105 4 104 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ V )
106 105 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑇 ∈ V )
107 rabexg ⊢ ( 𝑇 ∈ V → { 𝑡 ∈ 𝑇 ∣ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } ∈ V )
108 106 107 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → { 𝑡 ∈ 𝑇 ∣ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } ∈ V )
109 7 fvmpt2 ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ { 𝑡 ∈ 𝑇 ∣ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } ∈ V ) → ( 𝐵 ‘ 𝑗 ) = { 𝑡 ∈ 𝑇 ∣ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } )
110 80 108 109 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑗 ) = { 𝑡 ∈ 𝑇 ∣ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } )
111 eqid ⊢ { 𝑡 ∈ 𝑇 ∣ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } = { 𝑡 ∈ 𝑇 ∣ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) }
112 elfzelz ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 ∈ ℤ )
113 112 zred ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 ∈ ℝ )
114 3re ⊢ 3 ∈ ℝ
115 3ne0 ⊢ 3 ≠ 0
116 114 115 rereccli ⊢ ( 1 / 3 ) ∈ ℝ
117 readdcl ⊢ ( ( 𝑗 ∈ ℝ ∧ ( 1 / 3 ) ∈ ℝ ) → ( 𝑗 + ( 1 / 3 ) ) ∈ ℝ )
118 113 116 117 sylancl ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑗 + ( 1 / 3 ) ) ∈ ℝ )
119 118 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑗 + ( 1 / 3 ) ) ∈ ℝ )
120 17 rpred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
121 120 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝐸 ∈ ℝ )
122 119 121 remulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∈ ℝ )
123 16 5 eleqtrdi ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
124 123 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
125 1 3 4 111 122 124 rfcnpre3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → { 𝑡 ∈ 𝑇 ∣ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } ∈ ( Clsd ‘ 𝐽 ) )
126 110 125 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑗 ) ∈ ( Clsd ‘ 𝐽 ) )
127 rabexg ⊢ ( 𝑇 ∈ V → { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } ∈ V )
128 106 127 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } ∈ V )
129 6 fvmpt2 ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } ∈ V ) → ( 𝐷 ‘ 𝑗 ) = { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } )
130 80 128 129 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝐷 ‘ 𝑗 ) = { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } )
131 eqid ⊢ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } = { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) }
132 resubcl ⊢ ( ( 𝑗 ∈ ℝ ∧ ( 1 / 3 ) ∈ ℝ ) → ( 𝑗 − ( 1 / 3 ) ) ∈ ℝ )
133 113 116 132 sylancl ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑗 − ( 1 / 3 ) ) ∈ ℝ )
134 133 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑗 − ( 1 / 3 ) ) ∈ ℝ )
135 134 121 remulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ∈ ℝ )
136 1 3 4 131 135 124 rfcnpre4 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } ∈ ( Clsd ‘ 𝐽 ) )
137 130 136 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝐷 ‘ 𝑗 ) ∈ ( Clsd ‘ 𝐽 ) )
138 135 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ) → ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ∈ ℝ )
139 122 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ) → ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∈ ℝ )
140 3 4 5 16 fcnre ⊢ ( 𝜑 → 𝐹 : 𝑇 ⟶ ℝ )
141 140 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ) → 𝐹 : 𝑇 ⟶ ℝ )
142 ssrab2 ⊢ { 𝑡 ∈ 𝑇 ∣ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } ⊆ 𝑇
143 110 142 eqsstrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑗 ) ⊆ 𝑇 )
144 143 sselda ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ) → 𝑡 ∈ 𝑇 )
145 141 144 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℝ )
146 116 132 mpan2 ⊢ ( 𝑗 ∈ ℝ → ( 𝑗 − ( 1 / 3 ) ) ∈ ℝ )
147 id ⊢ ( 𝑗 ∈ ℝ → 𝑗 ∈ ℝ )
148 116 117 mpan2 ⊢ ( 𝑗 ∈ ℝ → ( 𝑗 + ( 1 / 3 ) ) ∈ ℝ )
149 3pos ⊢ 0 < 3
150 114 149 recgt0ii ⊢ 0 < ( 1 / 3 )
151 116 150 elrpii ⊢ ( 1 / 3 ) ∈ ℝ+
152 ltsubrp ⊢ ( ( 𝑗 ∈ ℝ ∧ ( 1 / 3 ) ∈ ℝ+ ) → ( 𝑗 − ( 1 / 3 ) ) < 𝑗 )
153 151 152 mpan2 ⊢ ( 𝑗 ∈ ℝ → ( 𝑗 − ( 1 / 3 ) ) < 𝑗 )
154 ltaddrp ⊢ ( ( 𝑗 ∈ ℝ ∧ ( 1 / 3 ) ∈ ℝ+ ) → 𝑗 < ( 𝑗 + ( 1 / 3 ) ) )
155 151 154 mpan2 ⊢ ( 𝑗 ∈ ℝ → 𝑗 < ( 𝑗 + ( 1 / 3 ) ) )
156 146 147 148 153 155 lttrd ⊢ ( 𝑗 ∈ ℝ → ( 𝑗 − ( 1 / 3 ) ) < ( 𝑗 + ( 1 / 3 ) ) )
157 113 156 syl ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑗 − ( 1 / 3 ) ) < ( 𝑗 + ( 1 / 3 ) ) )
158 157 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑗 − ( 1 / 3 ) ) < ( 𝑗 + ( 1 / 3 ) ) )
159 17 rpregt0d ⊢ ( 𝜑 → ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) )
160 159 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) )
161 ltmul1 ⊢ ( ( ( 𝑗 − ( 1 / 3 ) ) ∈ ℝ ∧ ( 𝑗 + ( 1 / 3 ) ) ∈ ℝ ∧ ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) ) → ( ( 𝑗 − ( 1 / 3 ) ) < ( 𝑗 + ( 1 / 3 ) ) ↔ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ) )
162 134 119 160 161 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑗 − ( 1 / 3 ) ) < ( 𝑗 + ( 1 / 3 ) ) ↔ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ) )
163 158 162 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) )
164 163 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ) → ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) )
165 110 eleq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ↔ 𝑡 ∈ { 𝑡 ∈ 𝑇 ∣ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } ) )
166 165 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ) → 𝑡 ∈ { 𝑡 ∈ 𝑇 ∣ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } )
167 rabid ⊢ ( 𝑡 ∈ { 𝑡 ∈ 𝑇 ∣ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } ↔ ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) ) )
168 166 167 sylib ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ) → ( 𝑡 ∈ 𝑇 ∧ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) ) )
169 168 simprd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ) → ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) )
170 138 139 145 164 169 ltletrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ) → ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) )
171 138 145 ltnled ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ) → ( ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑡 ) ↔ ¬ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) )
172 170 171 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ) → ¬ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) )
173 172 intnand ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ) → ¬ ( 𝑡 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) )
174 rabid ⊢ ( 𝑡 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } ↔ ( 𝑡 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ) )
175 173 174 sylnibr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ) → ¬ 𝑡 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } )
176 130 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ) → ( 𝐷 ‘ 𝑗 ) = { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } )
177 175 176 neleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ) → ¬ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) )
178 177 ex ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) → ¬ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) )
179 97 178 ralrimi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ¬ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) )
180 disj ⊢ ( ( ( 𝐵 ‘ 𝑗 ) ∩ ( 𝐷 ‘ 𝑗 ) ) = ∅ ↔ ∀ 𝑎 ∈ ( 𝐵 ‘ 𝑗 ) ¬ 𝑎 ∈ ( 𝐷 ‘ 𝑗 ) )
181 nfcv ⊢ Ⅎ 𝑎 ( 𝐵 ‘ 𝑗 )
182 89 nfcri ⊢ Ⅎ 𝑡 𝑎 ∈ ( 𝐷 ‘ 𝑗 )
183 182 nfn ⊢ Ⅎ 𝑡 ¬ 𝑎 ∈ ( 𝐷 ‘ 𝑗 )
184 nfv ⊢ Ⅎ 𝑎 ¬ 𝑡 ∈ ( 𝐷 ‘ 𝑗 )
185 eleq1 ⊢ ( 𝑎 = 𝑡 → ( 𝑎 ∈ ( 𝐷 ‘ 𝑗 ) ↔ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) )
186 185 notbid ⊢ ( 𝑎 = 𝑡 → ( ¬ 𝑎 ∈ ( 𝐷 ‘ 𝑗 ) ↔ ¬ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ) )
187 181 94 183 184 186 cbvralfw ⊢ ( ∀ 𝑎 ∈ ( 𝐵 ‘ 𝑗 ) ¬ 𝑎 ∈ ( 𝐷 ‘ 𝑗 ) ↔ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ¬ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) )
188 180 187 bitri ⊢ ( ( ( 𝐵 ‘ 𝑗 ) ∩ ( 𝐷 ‘ 𝑗 ) ) = ∅ ↔ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ¬ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) )
189 179 188 sylibr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐵 ‘ 𝑗 ) ∩ ( 𝐷 ‘ 𝑗 ) ) = ∅ )
190 eqid ⊢ ( 𝑇 ∖ ( 𝐵 ‘ 𝑗 ) ) = ( 𝑇 ∖ ( 𝐵 ‘ 𝑗 ) )
191 19 nnrpd ⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
192 17 191 rpdivcld ⊢ ( 𝜑 → ( 𝐸 / 𝑁 ) ∈ ℝ+ )
193 192 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝐸 / 𝑁 ) ∈ ℝ+ )
194 120 19 nndivred ⊢ ( 𝜑 → ( 𝐸 / 𝑁 ) ∈ ℝ )
195 116 a1i ⊢ ( 𝜑 → ( 1 / 3 ) ∈ ℝ )
196 19 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝑁 )
197 1re ⊢ 1 ∈ ℝ
198 0lt1 ⊢ 0 < 1
199 197 198 pm3.2i ⊢ ( 1 ∈ ℝ ∧ 0 < 1 )
200 199 a1i ⊢ ( 𝜑 → ( 1 ∈ ℝ ∧ 0 < 1 ) )
201 19 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
202 19 nngt0d ⊢ ( 𝜑 → 0 < 𝑁 )
203 lediv2 ⊢ ( ( ( 1 ∈ ℝ ∧ 0 < 1 ) ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ∧ ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) ) → ( 1 ≤ 𝑁 ↔ ( 𝐸 / 𝑁 ) ≤ ( 𝐸 / 1 ) ) )
204 200 201 202 159 203 syl121anc ⊢ ( 𝜑 → ( 1 ≤ 𝑁 ↔ ( 𝐸 / 𝑁 ) ≤ ( 𝐸 / 1 ) ) )
205 196 204 mpbid ⊢ ( 𝜑 → ( 𝐸 / 𝑁 ) ≤ ( 𝐸 / 1 ) )
206 17 rpcnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
207 206 div1d ⊢ ( 𝜑 → ( 𝐸 / 1 ) = 𝐸 )
208 205 207 breqtrd ⊢ ( 𝜑 → ( 𝐸 / 𝑁 ) ≤ 𝐸 )
209 194 120 195 208 18 lelttrd ⊢ ( 𝜑 → ( 𝐸 / 𝑁 ) < ( 1 / 3 ) )
210 209 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝐸 / 𝑁 ) < ( 1 / 3 ) )
211 89 95 97 3 4 5 98 99 100 101 102 103 126 137 189 190 193 210 stoweidlem58 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑥 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑥 ‘ 𝑡 ) ) )
212 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑥 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑥 ‘ 𝑡 ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑥 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑥 ‘ 𝑡 ) ) ) )
213 211 212 sylib ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑥 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑥 ‘ 𝑡 ) ) ) )
214 simprl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑥 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑥 ‘ 𝑡 ) ) ) ) → 𝑥 ∈ 𝐴 )
215 simprr1 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑥 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑥 ‘ 𝑡 ) ) ) ) → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) )
216 fveq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ‘ 𝑡 ) = ( 𝑥 ‘ 𝑡 ) )
217 216 breq2d ⊢ ( 𝑦 = 𝑥 → ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ↔ 0 ≤ ( 𝑥 ‘ 𝑡 ) ) )
218 216 breq1d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ‘ 𝑡 ) ≤ 1 ↔ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) )
219 217 218 anbi12d ⊢ ( 𝑦 = 𝑥 → ( ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ↔ ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ) )
220 219 ralbidv ⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ↔ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ) )
221 220 8 elrab2 ⊢ ( 𝑥 ∈ 𝑌 ↔ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ) )
222 214 215 221 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑥 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑥 ‘ 𝑡 ) ) ) ) → 𝑥 ∈ 𝑌 )
223 simprr2 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑥 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑥 ‘ 𝑡 ) ) ) ) → ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑥 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) )
224 simprr3 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑥 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑥 ‘ 𝑡 ) ) ) ) → ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑥 ‘ 𝑡 ) )
225 223 224 jca ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑥 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑥 ‘ 𝑡 ) ) ) ) → ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑥 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑥 ‘ 𝑡 ) ) )
226 nfcv ⊢ Ⅎ 𝑦 𝑥
227 nfv ⊢ Ⅎ 𝑦 ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑥 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑥 ‘ 𝑡 ) )
228 216 breq1d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ↔ ( 𝑥 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ) )
229 228 ralbidv ⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ↔ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑥 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ) )
230 216 breq2d ⊢ ( 𝑦 = 𝑥 → ( ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ↔ ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑥 ‘ 𝑡 ) ) )
231 230 ralbidv ⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ↔ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑥 ‘ 𝑡 ) ) )
232 229 231 anbi12d ⊢ ( 𝑦 = 𝑥 → ( ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) ↔ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑥 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑥 ‘ 𝑡 ) ) ) )
233 226 21 227 232 elrabf ⊢ ( 𝑥 ∈ { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) } ↔ ( 𝑥 ∈ 𝑌 ∧ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑥 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑥 ‘ 𝑡 ) ) ) )
234 222 225 233 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑥 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑥 ‘ 𝑡 ) ) ) ) → 𝑥 ∈ { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) } )
235 234 ex ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑥 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑥 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑥 ‘ 𝑡 ) ) ) → 𝑥 ∈ { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) } ) )
236 235 eximdv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑥 ‘ 𝑡 ) ∧ ( 𝑥 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑥 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑥 ‘ 𝑡 ) ) ) → ∃ 𝑥 𝑥 ∈ { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) } ) )
237 213 236 mpd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ∃ 𝑥 𝑥 ∈ { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) } )
238 ne0i ⊢ ( 𝑥 ∈ { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) } → { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) } ≠ ∅ )
239 238 exlimiv ⊢ ( ∃ 𝑥 𝑥 ∈ { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) } → { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) } ≠ ∅ )
240 237 239 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) } ≠ ∅ )
241 83 240 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝐻 ‘ 𝑗 ) ≠ ∅ )
242 241 3adant3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ ( 𝐻 ‘ 𝑗 ) = 𝑤 ) → ( 𝐻 ‘ 𝑗 ) ≠ ∅ )
243 79 242 eqnetrrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ ( 𝐻 ‘ 𝑗 ) = 𝑤 ) → 𝑤 ≠ ∅ )
244 243 3exp ⊢ ( 𝜑 → ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( ( 𝐻 ‘ 𝑗 ) = 𝑤 → 𝑤 ≠ ∅ ) ) )
245 244 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝐻 ‘ 𝑗 ) = 𝑤 → 𝑤 ≠ ∅ ) )
246 245 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐻 ) → ( ∃ 𝑗 ∈ ( 0 ... 𝑁 ) ( 𝐻 ‘ 𝑗 ) = 𝑤 → 𝑤 ≠ ∅ ) )
247 78 246 mpd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐻 ) → 𝑤 ≠ ∅ )
248 247 adantlr ⊢ ( ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) ∧ 𝑤 ∈ ran 𝐻 ) → 𝑤 ≠ ∅ )
249 rsp ⊢ ( ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) → ( 𝑤 ∈ ran 𝐻 → ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) )
250 63 64 248 249 syl3c ⊢ ( ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) ∧ 𝑤 ∈ ran 𝐻 ) → ( ℎ ‘ 𝑤 ) ∈ 𝑤 )
251 250 ex ⊢ ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) → ( 𝑤 ∈ ran 𝐻 → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) )
252 62 251 ralrimi ⊢ ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) → ∀ 𝑤 ∈ ran 𝐻 ( ℎ ‘ 𝑤 ) ∈ 𝑤 )
253 chfnrn ⊢ ( ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) → ran ℎ ⊆ ∪ ran 𝐻 )
254 47 252 253 syl2anc ⊢ ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) → ran ℎ ⊆ ∪ ran 𝐻 )
255 nfv ⊢ Ⅎ 𝑦 𝜑
256 nfcv ⊢ Ⅎ 𝑦 ℎ
257 nfcv ⊢ Ⅎ 𝑦 ( 0 ... 𝑁 )
258 nfrab1 ⊢ Ⅎ 𝑦 { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) }
259 257 258 nfmpt ⊢ Ⅎ 𝑦 ( 𝑗 ∈ ( 0 ... 𝑁 ) ↦ { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) } )
260 9 259 nfcxfr ⊢ Ⅎ 𝑦 𝐻
261 260 nfrn ⊢ Ⅎ 𝑦 ran 𝐻
262 256 261 nffn ⊢ Ⅎ 𝑦 ℎ Fn ran 𝐻
263 nfv ⊢ Ⅎ 𝑦 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 )
264 261 263 nfralw ⊢ Ⅎ 𝑦 ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 )
265 262 264 nfan ⊢ Ⅎ 𝑦 ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) )
266 255 265 nfan ⊢ Ⅎ 𝑦 ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) )
267 261 nfuni ⊢ Ⅎ 𝑦 ∪ ran 𝐻
268 fnunirn ⊢ ( 𝐻 Fn ( 0 ... 𝑁 ) → ( 𝑦 ∈ ∪ ran 𝐻 ↔ ∃ 𝑧 ∈ ( 0 ... 𝑁 ) 𝑦 ∈ ( 𝐻 ‘ 𝑧 ) ) )
269 nfcv ⊢ Ⅎ 𝑗 𝑧
270 68 269 nffv ⊢ Ⅎ 𝑗 ( 𝐻 ‘ 𝑧 )
271 270 nfcri ⊢ Ⅎ 𝑗 𝑦 ∈ ( 𝐻 ‘ 𝑧 )
272 nfv ⊢ Ⅎ 𝑧 𝑦 ∈ ( 𝐻 ‘ 𝑗 )
273 fveq2 ⊢ ( 𝑧 = 𝑗 → ( 𝐻 ‘ 𝑧 ) = ( 𝐻 ‘ 𝑗 ) )
274 273 eleq2d ⊢ ( 𝑧 = 𝑗 → ( 𝑦 ∈ ( 𝐻 ‘ 𝑧 ) ↔ 𝑦 ∈ ( 𝐻 ‘ 𝑗 ) ) )
275 271 272 274 cbvrexw ⊢ ( ∃ 𝑧 ∈ ( 0 ... 𝑁 ) 𝑦 ∈ ( 𝐻 ‘ 𝑧 ) ↔ ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 𝑦 ∈ ( 𝐻 ‘ 𝑗 ) )
276 268 275 bitrdi ⊢ ( 𝐻 Fn ( 0 ... 𝑁 ) → ( 𝑦 ∈ ∪ ran 𝐻 ↔ ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 𝑦 ∈ ( 𝐻 ‘ 𝑗 ) ) )
277 39 276 syl ⊢ ( 𝜑 → ( 𝑦 ∈ ∪ ran 𝐻 ↔ ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 𝑦 ∈ ( 𝐻 ‘ 𝑗 ) ) )
278 277 biimpa ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻 ) → ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 𝑦 ∈ ( 𝐻 ‘ 𝑗 ) )
279 nfv ⊢ Ⅎ 𝑗 𝜑
280 68 nfrn ⊢ Ⅎ 𝑗 ran 𝐻
281 280 nfuni ⊢ Ⅎ 𝑗 ∪ ran 𝐻
282 281 nfcri ⊢ Ⅎ 𝑗 𝑦 ∈ ∪ ran 𝐻
283 279 282 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻 )
284 nfv ⊢ Ⅎ 𝑗 𝑦 ∈ 𝑌
285 simp1l ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻 ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑗 ) ) → 𝜑 )
286 simp2 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻 ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑗 ) ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
287 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻 ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑗 ) ) → 𝑦 ∈ ( 𝐻 ‘ 𝑗 ) )
288 83 eleq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑦 ∈ ( 𝐻 ‘ 𝑗 ) ↔ 𝑦 ∈ { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) } ) )
289 288 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑗 ) ) → 𝑦 ∈ { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) } )
290 rabid ⊢ ( 𝑦 ∈ { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) } ↔ ( 𝑦 ∈ 𝑌 ∧ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) ) )
291 289 290 sylib ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑗 ) ) → ( 𝑦 ∈ 𝑌 ∧ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) ) )
292 291 simpld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑗 ) ) → 𝑦 ∈ 𝑌 )
293 285 286 287 292 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻 ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑗 ) ) → 𝑦 ∈ 𝑌 )
294 293 3exp ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻 ) → ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑦 ∈ ( 𝐻 ‘ 𝑗 ) → 𝑦 ∈ 𝑌 ) ) )
295 283 284 294 rexlimd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻 ) → ( ∃ 𝑗 ∈ ( 0 ... 𝑁 ) 𝑦 ∈ ( 𝐻 ‘ 𝑗 ) → 𝑦 ∈ 𝑌 ) )
296 278 295 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∪ ran 𝐻 ) → 𝑦 ∈ 𝑌 )
297 296 adantlr ⊢ ( ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) ∧ 𝑦 ∈ ∪ ran 𝐻 ) → 𝑦 ∈ 𝑌 )
298 297 ex ⊢ ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) → ( 𝑦 ∈ ∪ ran 𝐻 → 𝑦 ∈ 𝑌 ) )
299 266 267 21 298 ssrd ⊢ ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) → ∪ ran 𝐻 ⊆ 𝑌 )
300 ssrab2 ⊢ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) } ⊆ 𝐴
301 8 300 eqsstri ⊢ 𝑌 ⊆ 𝐴
302 299 301 sstrdi ⊢ ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) → ∪ ran 𝐻 ⊆ 𝐴 )
303 254 302 sstrd ⊢ ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) → ran ℎ ⊆ 𝐴 )
304 57 303 fssd ⊢ ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) → ℎ : ran 𝐻 ⟶ 𝐴 )
305 dffn3 ⊢ ( 𝐻 Fn ( 0 ... 𝑁 ) ↔ 𝐻 : ( 0 ... 𝑁 ) ⟶ ran 𝐻 )
306 39 305 sylib ⊢ ( 𝜑 → 𝐻 : ( 0 ... 𝑁 ) ⟶ ran 𝐻 )
307 306 adantr ⊢ ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) → 𝐻 : ( 0 ... 𝑁 ) ⟶ ran 𝐻 )
308 fco ⊢ ( ( ℎ : ran 𝐻 ⟶ 𝐴 ∧ 𝐻 : ( 0 ... 𝑁 ) ⟶ ran 𝐻 ) → ( ℎ ∘ 𝐻 ) : ( 0 ... 𝑁 ) ⟶ 𝐴 )
309 304 307 308 syl2anc ⊢ ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) → ( ℎ ∘ 𝐻 ) : ( 0 ... 𝑁 ) ⟶ 𝐴 )
310 nfcv ⊢ Ⅎ 𝑗 ℎ
311 310 280 nffn ⊢ Ⅎ 𝑗 ℎ Fn ran 𝐻
312 nfv ⊢ Ⅎ 𝑗 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 )
313 280 312 nfralw ⊢ Ⅎ 𝑗 ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 )
314 311 313 nfan ⊢ Ⅎ 𝑗 ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) )
315 279 314 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) )
316 simpll ⊢ ( ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝜑 )
317 simpr ⊢ ( ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
318 39 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝐻 Fn ( 0 ... 𝑁 ) )
319 fvco2 ⊢ ( ( 𝐻 Fn ( 0 ... 𝑁 ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) = ( ℎ ‘ ( 𝐻 ‘ 𝑗 ) ) )
320 318 319 sylancom ⊢ ( ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) = ( ℎ ‘ ( 𝐻 ‘ 𝑗 ) ) )
321 simplrr ⊢ ( ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) )
322 fnfun ⊢ ( 𝐻 Fn ( 0 ... 𝑁 ) → Fun 𝐻 )
323 39 322 syl ⊢ ( 𝜑 → Fun 𝐻 )
324 323 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → Fun 𝐻 )
325 39 fndmd ⊢ ( 𝜑 → dom 𝐻 = ( 0 ... 𝑁 ) )
326 325 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → dom 𝐻 = ( 0 ... 𝑁 ) )
327 80 326 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑗 ∈ dom 𝐻 )
328 327 adantlr ⊢ ( ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑗 ∈ dom 𝐻 )
329 fvelrn ⊢ ( ( Fun 𝐻 ∧ 𝑗 ∈ dom 𝐻 ) → ( 𝐻 ‘ 𝑗 ) ∈ ran 𝐻 )
330 324 328 329 syl2anc ⊢ ( ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝐻 ‘ 𝑗 ) ∈ ran 𝐻 )
331 321 330 jca ⊢ ( ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ∧ ( 𝐻 ‘ 𝑗 ) ∈ ran 𝐻 ) )
332 241 adantlr ⊢ ( ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝐻 ‘ 𝑗 ) ≠ ∅ )
333 neeq1 ⊢ ( 𝑤 = ( 𝐻 ‘ 𝑗 ) → ( 𝑤 ≠ ∅ ↔ ( 𝐻 ‘ 𝑗 ) ≠ ∅ ) )
334 fveq2 ⊢ ( 𝑤 = ( 𝐻 ‘ 𝑗 ) → ( ℎ ‘ 𝑤 ) = ( ℎ ‘ ( 𝐻 ‘ 𝑗 ) ) )
335 id ⊢ ( 𝑤 = ( 𝐻 ‘ 𝑗 ) → 𝑤 = ( 𝐻 ‘ 𝑗 ) )
336 334 335 eleq12d ⊢ ( 𝑤 = ( 𝐻 ‘ 𝑗 ) → ( ( ℎ ‘ 𝑤 ) ∈ 𝑤 ↔ ( ℎ ‘ ( 𝐻 ‘ 𝑗 ) ) ∈ ( 𝐻 ‘ 𝑗 ) ) )
337 333 336 imbi12d ⊢ ( 𝑤 = ( 𝐻 ‘ 𝑗 ) → ( ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ↔ ( ( 𝐻 ‘ 𝑗 ) ≠ ∅ → ( ℎ ‘ ( 𝐻 ‘ 𝑗 ) ) ∈ ( 𝐻 ‘ 𝑗 ) ) ) )
338 337 rspccva ⊢ ( ( ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ∧ ( 𝐻 ‘ 𝑗 ) ∈ ran 𝐻 ) → ( ( 𝐻 ‘ 𝑗 ) ≠ ∅ → ( ℎ ‘ ( 𝐻 ‘ 𝑗 ) ) ∈ ( 𝐻 ‘ 𝑗 ) ) )
339 331 332 338 sylc ⊢ ( ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ℎ ‘ ( 𝐻 ‘ 𝑗 ) ) ∈ ( 𝐻 ‘ 𝑗 ) )
340 320 339 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ ( 𝐻 ‘ 𝑗 ) )
341 256 260 nfco ⊢ Ⅎ 𝑦 ( ℎ ∘ 𝐻 )
342 nfcv ⊢ Ⅎ 𝑦 𝑗
343 341 342 nffv ⊢ Ⅎ 𝑦 ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 )
344 nfv ⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) )
345 260 342 nffv ⊢ Ⅎ 𝑦 ( 𝐻 ‘ 𝑗 )
346 343 345 nfel ⊢ Ⅎ 𝑦 ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ ( 𝐻 ‘ 𝑗 )
347 344 346 nfan ⊢ Ⅎ 𝑦 ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ ( 𝐻 ‘ 𝑗 ) )
348 343 21 nfel ⊢ Ⅎ 𝑦 ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ 𝑌
349 347 348 nfim ⊢ Ⅎ 𝑦 ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ ( 𝐻 ‘ 𝑗 ) ) → ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ 𝑌 )
350 eleq1 ⊢ ( 𝑦 = ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) → ( 𝑦 ∈ ( 𝐻 ‘ 𝑗 ) ↔ ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ ( 𝐻 ‘ 𝑗 ) ) )
351 350 anbi2d ⊢ ( 𝑦 = ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑗 ) ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ ( 𝐻 ‘ 𝑗 ) ) ) )
352 eleq1 ⊢ ( 𝑦 = ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) → ( 𝑦 ∈ 𝑌 ↔ ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ 𝑌 ) )
353 351 352 imbi12d ⊢ ( 𝑦 = ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) → ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑗 ) ) → 𝑦 ∈ 𝑌 ) ↔ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ ( 𝐻 ‘ 𝑗 ) ) → ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ 𝑌 ) ) )
354 343 349 353 292 vtoclgf ⊢ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ ( 𝐻 ‘ 𝑗 ) → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ ( 𝐻 ‘ 𝑗 ) ) → ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ 𝑌 ) )
355 354 anabsi7 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ ( 𝐻 ‘ 𝑗 ) ) → ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ 𝑌 )
356 316 317 340 355 syl21anc ⊢ ( ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ 𝑌 )
357 8 eleq2i ⊢ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ 𝑌 ↔ ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) } )
358 nfcv ⊢ Ⅎ 𝑦 𝐴
359 nfcv ⊢ Ⅎ 𝑦 𝑇
360 nfcv ⊢ Ⅎ 𝑦 0
361 nfcv ⊢ Ⅎ 𝑦 ≤
362 nfcv ⊢ Ⅎ 𝑦 𝑡
363 343 362 nffv ⊢ Ⅎ 𝑦 ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 )
364 360 361 363 nfbr ⊢ Ⅎ 𝑦 0 ≤ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 )
365 nfcv ⊢ Ⅎ 𝑦 1
366 363 361 365 nfbr ⊢ Ⅎ 𝑦 ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1
367 364 366 nfan ⊢ Ⅎ 𝑦 ( 0 ≤ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 )
368 359 367 nfralw ⊢ Ⅎ 𝑦 ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 )
369 nfcv ⊢ Ⅎ 𝑡 𝑦
370 nfcv ⊢ Ⅎ 𝑡 ℎ
371 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 )
372 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 )
373 371 372 nfan ⊢ Ⅎ 𝑡 ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) )
374 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 )
375 nfcv ⊢ Ⅎ 𝑡 𝐴
376 374 375 nfrabw ⊢ Ⅎ 𝑡 { 𝑦 ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) }
377 8 376 nfcxfr ⊢ Ⅎ 𝑡 𝑌
378 373 377 nfrabw ⊢ Ⅎ 𝑡 { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) }
379 84 378 nfmpt ⊢ Ⅎ 𝑡 ( 𝑗 ∈ ( 0 ... 𝑁 ) ↦ { 𝑦 ∈ 𝑌 ∣ ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) } )
380 9 379 nfcxfr ⊢ Ⅎ 𝑡 𝐻
381 370 380 nfco ⊢ Ⅎ 𝑡 ( ℎ ∘ 𝐻 )
382 381 88 nffv ⊢ Ⅎ 𝑡 ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 )
383 369 382 nfeq ⊢ Ⅎ 𝑡 𝑦 = ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 )
384 fveq1 ⊢ ( 𝑦 = ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) → ( 𝑦 ‘ 𝑡 ) = ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) )
385 384 breq2d ⊢ ( 𝑦 = ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) → ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ↔ 0 ≤ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ) )
386 384 breq1d ⊢ ( 𝑦 = ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) → ( ( 𝑦 ‘ 𝑡 ) ≤ 1 ↔ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) )
387 385 386 anbi12d ⊢ ( 𝑦 = ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) → ( ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ↔ ( 0 ≤ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ) )
388 383 387 ralbid ⊢ ( 𝑦 = ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ↔ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ) )
389 343 358 368 388 elrabf ⊢ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ { 𝑦 ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) } ↔ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ) )
390 357 389 bitri ⊢ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ 𝑌 ↔ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ) )
391 356 390 sylib ⊢ ( ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ) )
392 391 simprd ⊢ ( ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) )
393 nfcv ⊢ Ⅎ 𝑦 ( 𝐷 ‘ 𝑗 )
394 nfcv ⊢ Ⅎ 𝑦 <
395 nfcv ⊢ Ⅎ 𝑦 ( 𝐸 / 𝑁 )
396 363 394 395 nfbr ⊢ Ⅎ 𝑦 ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 )
397 393 396 nfralw ⊢ Ⅎ 𝑦 ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 )
398 347 397 nfim ⊢ Ⅎ 𝑦 ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ ( 𝐻 ‘ 𝑗 ) ) → ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) )
399 384 breq1d ⊢ ( 𝑦 = ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) → ( ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ↔ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ) )
400 383 399 ralbid ⊢ ( 𝑦 = ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) → ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ↔ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ) )
401 351 400 imbi12d ⊢ ( 𝑦 = ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) → ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑗 ) ) → ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ) ↔ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ ( 𝐻 ‘ 𝑗 ) ) → ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ) ) )
402 291 simprd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑗 ) ) → ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) )
403 402 simpld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑗 ) ) → ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( 𝑦 ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) )
404 343 398 401 403 vtoclgf ⊢ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ ( 𝐻 ‘ 𝑗 ) → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ ( 𝐻 ‘ 𝑗 ) ) → ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ) )
405 404 anabsi7 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ ( 𝐻 ‘ 𝑗 ) ) → ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) )
406 316 317 340 405 syl21anc ⊢ ( ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) )
407 nfcv ⊢ Ⅎ 𝑦 ( 𝐵 ‘ 𝑗 )
408 nfcv ⊢ Ⅎ 𝑦 ( 1 − ( 𝐸 / 𝑁 ) )
409 408 394 363 nfbr ⊢ Ⅎ 𝑦 ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 )
410 407 409 nfralw ⊢ Ⅎ 𝑦 ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 )
411 347 410 nfim ⊢ Ⅎ 𝑦 ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ ( 𝐻 ‘ 𝑗 ) ) → ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) )
412 384 breq2d ⊢ ( 𝑦 = ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) → ( ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ↔ ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ) )
413 383 412 ralbid ⊢ ( 𝑦 = ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) → ( ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ↔ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ) )
414 351 413 imbi12d ⊢ ( 𝑦 = ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) → ( ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑗 ) ) → ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) ) ↔ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ ( 𝐻 ‘ 𝑗 ) ) → ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ) ) )
415 402 simprd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑗 ) ) → ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( 𝑦 ‘ 𝑡 ) )
416 343 411 414 415 vtoclgf ⊢ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ ( 𝐻 ‘ 𝑗 ) → ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ ( 𝐻 ‘ 𝑗 ) ) → ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ) )
417 416 anabsi7 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ∈ ( 𝐻 ‘ 𝑗 ) ) → ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) )
418 316 317 340 417 syl21anc ⊢ ( ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) )
419 392 406 418 3jca ⊢ ( ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ) )
420 419 ex ⊢ ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) → ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ) ) )
421 315 420 ralrimi ⊢ ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) → ∀ 𝑗 ∈ ( 0 ... 𝑁 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ) )
422 309 421 jca ⊢ ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) → ( ( ℎ ∘ 𝐻 ) : ( 0 ... 𝑁 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑁 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ) ) )
423 feq1 ⊢ ( 𝑥 = ( ℎ ∘ 𝐻 ) → ( 𝑥 : ( 0 ... 𝑁 ) ⟶ 𝐴 ↔ ( ℎ ∘ 𝐻 ) : ( 0 ... 𝑁 ) ⟶ 𝐴 ) )
424 nfcv ⊢ Ⅎ 𝑗 𝑥
425 310 68 nfco ⊢ Ⅎ 𝑗 ( ℎ ∘ 𝐻 )
426 424 425 nfeq ⊢ Ⅎ 𝑗 𝑥 = ( ℎ ∘ 𝐻 )
427 nfcv ⊢ Ⅎ 𝑡 𝑥
428 427 381 nfeq ⊢ Ⅎ 𝑡 𝑥 = ( ℎ ∘ 𝐻 )
429 fveq1 ⊢ ( 𝑥 = ( ℎ ∘ 𝐻 ) → ( 𝑥 ‘ 𝑗 ) = ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) )
430 429 fveq1d ⊢ ( 𝑥 = ( ℎ ∘ 𝐻 ) → ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) = ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) )
431 430 breq2d ⊢ ( 𝑥 = ( ℎ ∘ 𝐻 ) → ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ↔ 0 ≤ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ) )
432 430 breq1d ⊢ ( 𝑥 = ( ℎ ∘ 𝐻 ) → ( ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ↔ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) )
433 431 432 anbi12d ⊢ ( 𝑥 = ( ℎ ∘ 𝐻 ) → ( ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ↔ ( 0 ≤ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ) )
434 428 433 ralbid ⊢ ( 𝑥 = ( ℎ ∘ 𝐻 ) → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ↔ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ) )
435 430 breq1d ⊢ ( 𝑥 = ( ℎ ∘ 𝐻 ) → ( ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ↔ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ) )
436 428 435 ralbid ⊢ ( 𝑥 = ( ℎ ∘ 𝐻 ) → ( ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ↔ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ) )
437 430 breq2d ⊢ ( 𝑥 = ( ℎ ∘ 𝐻 ) → ( ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ↔ ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ) )
438 428 437 ralbid ⊢ ( 𝑥 = ( ℎ ∘ 𝐻 ) → ( ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ↔ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ) )
439 434 436 438 3anbi123d ⊢ ( 𝑥 = ( ℎ ∘ 𝐻 ) → ( ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ↔ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ) ) )
440 426 439 ralbid ⊢ ( 𝑥 = ( ℎ ∘ 𝐻 ) → ( ∀ 𝑗 ∈ ( 0 ... 𝑁 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ↔ ∀ 𝑗 ∈ ( 0 ... 𝑁 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ) ) )
441 423 440 anbi12d ⊢ ( 𝑥 = ( ℎ ∘ 𝐻 ) → ( ( 𝑥 : ( 0 ... 𝑁 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑁 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ↔ ( ( ℎ ∘ 𝐻 ) : ( 0 ... 𝑁 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑁 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) )
442 441 spcegv ⊢ ( ( ℎ ∘ 𝐻 ) ∈ V → ( ( ( ℎ ∘ 𝐻 ) : ( 0 ... 𝑁 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑁 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( ( ℎ ∘ 𝐻 ) ‘ 𝑗 ) ‘ 𝑡 ) ) ) → ∃ 𝑥 ( 𝑥 : ( 0 ... 𝑁 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑁 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) ) )
443 55 422 442 sylc ⊢ ( ( 𝜑 ∧ ( ℎ Fn ran 𝐻 ∧ ∀ 𝑤 ∈ ran 𝐻 ( 𝑤 ≠ ∅ → ( ℎ ‘ 𝑤 ) ∈ 𝑤 ) ) ) → ∃ 𝑥 ( 𝑥 : ( 0 ... 𝑁 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑁 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) )
444 46 443 exlimddv ⊢ ( 𝜑 → ∃ 𝑥 ( 𝑥 : ( 0 ... 𝑁 ) ⟶ 𝐴 ∧ ∀ 𝑗 ∈ ( 0 ... 𝑁 ) ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ∧ ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝐷 ‘ 𝑗 ) ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ∧ ∀ 𝑡 ∈ ( 𝐵 ‘ 𝑗 ) ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑥 ‘ 𝑗 ) ‘ 𝑡 ) ) ) )