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 ffvelrnd ( ( ( 𝜑𝑗 ∈ ( 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 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑥𝑗 ) ‘ 𝑡 ) ) ) )