Metamath Proof Explorer

Theorem stoweidlem39

Description: This lemma is used to prove that there exists a function x as in the proof of Lemma 2 in BrosowskiDeutsh p. 91: assuming that r is a finite subset of W , x indexes a finite set of functions in the subalgebra (of the Stone Weierstrass theorem), such that for all i ranging in the finite indexing set, 0 ≤ x_i ≤ 1, x_i < ε / m on V(t_i), and x_i > 1 - ε / m on B . Here D is used to represent A in the paper's Lemma 2 (because A is used for the subalgebra), M is used to represent m in the paper, E is used to represent ε, and v_i is used to represent V(t_i). W is just a local definition, used to shorten statements. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem39.1 ⊢ Ⅎ ℎ 𝜑
stoweidlem39.2 ⊢ Ⅎ 𝑡 𝜑
stoweidlem39.3 ⊢ Ⅎ 𝑤 𝜑
stoweidlem39.4 ⊢ 𝑈 = ( 𝑇 ∖ 𝐵 )
stoweidlem39.5 ⊢ 𝑌 = { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) }
stoweidlem39.6 ⊢ 𝑊 = { 𝑤 ∈ 𝐽 ∣ ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) }
stoweidlem39.7 ⊢ ( 𝜑 → 𝑟 ∈ ( 𝒫 𝑊 ∩ Fin ) )
stoweidlem39.8 ⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑟 )
stoweidlem39.9 ⊢ ( 𝜑 → 𝐷 ≠ ∅ )
stoweidlem39.10 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
stoweidlem39.11 ⊢ ( 𝜑 → 𝐵 ⊆ 𝑇 )
stoweidlem39.12 ⊢ ( 𝜑 → 𝑊 ∈ V )
stoweidlem39.13 ⊢ ( 𝜑 → 𝐴 ∈ V )
Assertion stoweidlem39 ( 𝜑 → ∃ 𝑚 ∈ ℕ ∃ 𝑣 ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑊 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑥 ( 𝑥 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem39.1 ⊢ Ⅎ ℎ 𝜑
2 stoweidlem39.2 ⊢ Ⅎ 𝑡 𝜑
3 stoweidlem39.3 ⊢ Ⅎ 𝑤 𝜑
4 stoweidlem39.4 ⊢ 𝑈 = ( 𝑇 ∖ 𝐵 )
5 stoweidlem39.5 ⊢ 𝑌 = { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) }
6 stoweidlem39.6 ⊢ 𝑊 = { 𝑤 ∈ 𝐽 ∣ ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) }
7 stoweidlem39.7 ⊢ ( 𝜑 → 𝑟 ∈ ( 𝒫 𝑊 ∩ Fin ) )
8 stoweidlem39.8 ⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑟 )
9 stoweidlem39.9 ⊢ ( 𝜑 → 𝐷 ≠ ∅ )
10 stoweidlem39.10 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
11 stoweidlem39.11 ⊢ ( 𝜑 → 𝐵 ⊆ 𝑇 )
12 stoweidlem39.12 ⊢ ( 𝜑 → 𝑊 ∈ V )
13 stoweidlem39.13 ⊢ ( 𝜑 → 𝐴 ∈ V )
14 8 9 jca ⊢ ( 𝜑 → ( 𝐷 ⊆ ∪ 𝑟 ∧ 𝐷 ≠ ∅ ) )
15 ssn0 ⊢ ( ( 𝐷 ⊆ ∪ 𝑟 ∧ 𝐷 ≠ ∅ ) → ∪ 𝑟 ≠ ∅ )
16 unieq ⊢ ( 𝑟 = ∅ → ∪ 𝑟 = ∪ ∅ )
17 uni0 ⊢ ∪ ∅ = ∅
18 16 17 eqtrdi ⊢ ( 𝑟 = ∅ → ∪ 𝑟 = ∅ )
19 18 necon3i ⊢ ( ∪ 𝑟 ≠ ∅ → 𝑟 ≠ ∅ )
20 14 15 19 3syl ⊢ ( 𝜑 → 𝑟 ≠ ∅ )
21 20 neneqd ⊢ ( 𝜑 → ¬ 𝑟 = ∅ )
22 elinel2 ⊢ ( 𝑟 ∈ ( 𝒫 𝑊 ∩ Fin ) → 𝑟 ∈ Fin )
23 7 22 syl ⊢ ( 𝜑 → 𝑟 ∈ Fin )
24 fz1f1o ⊢ ( 𝑟 ∈ Fin → ( 𝑟 = ∅ ∨ ( ( ♯ ‘ 𝑟 ) ∈ ℕ ∧ ∃ 𝑣 𝑣 : ( 1 ... ( ♯ ‘ 𝑟 ) ) –1-1-onto→ 𝑟 ) ) )
25 pm2.53 ⊢ ( ( 𝑟 = ∅ ∨ ( ( ♯ ‘ 𝑟 ) ∈ ℕ ∧ ∃ 𝑣 𝑣 : ( 1 ... ( ♯ ‘ 𝑟 ) ) –1-1-onto→ 𝑟 ) ) → ( ¬ 𝑟 = ∅ → ( ( ♯ ‘ 𝑟 ) ∈ ℕ ∧ ∃ 𝑣 𝑣 : ( 1 ... ( ♯ ‘ 𝑟 ) ) –1-1-onto→ 𝑟 ) ) )
26 23 24 25 3syl ⊢ ( 𝜑 → ( ¬ 𝑟 = ∅ → ( ( ♯ ‘ 𝑟 ) ∈ ℕ ∧ ∃ 𝑣 𝑣 : ( 1 ... ( ♯ ‘ 𝑟 ) ) –1-1-onto→ 𝑟 ) ) )
27 21 26 mpd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑟 ) ∈ ℕ ∧ ∃ 𝑣 𝑣 : ( 1 ... ( ♯ ‘ 𝑟 ) ) –1-1-onto→ 𝑟 ) )
28 oveq2 ⊢ ( 𝑚 = ( ♯ ‘ 𝑟 ) → ( 1 ... 𝑚 ) = ( 1 ... ( ♯ ‘ 𝑟 ) ) )
29 28 f1oeq2d ⊢ ( 𝑚 = ( ♯ ‘ 𝑟 ) → ( 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 ↔ 𝑣 : ( 1 ... ( ♯ ‘ 𝑟 ) ) –1-1-onto→ 𝑟 ) )
30 29 exbidv ⊢ ( 𝑚 = ( ♯ ‘ 𝑟 ) → ( ∃ 𝑣 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 ↔ ∃ 𝑣 𝑣 : ( 1 ... ( ♯ ‘ 𝑟 ) ) –1-1-onto→ 𝑟 ) )
31 30 rspcev ⊢ ( ( ( ♯ ‘ 𝑟 ) ∈ ℕ ∧ ∃ 𝑣 𝑣 : ( 1 ... ( ♯ ‘ 𝑟 ) ) –1-1-onto→ 𝑟 ) → ∃ 𝑚 ∈ ℕ ∃ 𝑣 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 )
32 27 31 syl ⊢ ( 𝜑 → ∃ 𝑚 ∈ ℕ ∃ 𝑣 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 )
33 f1of ⊢ ( 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 → 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑟 )
34 33 adantl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 ) → 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑟 )
35 simpll ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 ) → 𝜑 )
36 elinel1 ⊢ ( 𝑟 ∈ ( 𝒫 𝑊 ∩ Fin ) → 𝑟 ∈ 𝒫 𝑊 )
37 36 elpwid ⊢ ( 𝑟 ∈ ( 𝒫 𝑊 ∩ Fin ) → 𝑟 ⊆ 𝑊 )
38 35 7 37 3syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 ) → 𝑟 ⊆ 𝑊 )
39 34 38 fssd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 ) → 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑊 )
40 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 ) → 𝐷 ⊆ ∪ 𝑟 )
41 dff1o2 ⊢ ( 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 ↔ ( 𝑣 Fn ( 1 ... 𝑚 ) ∧ Fun ◡ 𝑣 ∧ ran 𝑣 = 𝑟 ) )
42 41 simp3bi ⊢ ( 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 → ran 𝑣 = 𝑟 )
43 42 unieqd ⊢ ( 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 → ∪ ran 𝑣 = ∪ 𝑟 )
44 43 adantl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 ) → ∪ ran 𝑣 = ∪ 𝑟 )
45 40 44 sseqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 ) → 𝐷 ⊆ ∪ ran 𝑣 )
46 nfv ⊢ Ⅎ ℎ 𝑚 ∈ ℕ
47 1 46 nfan ⊢ Ⅎ ℎ ( 𝜑 ∧ 𝑚 ∈ ℕ )
48 nfv ⊢ Ⅎ ℎ 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟
49 47 48 nfan ⊢ Ⅎ ℎ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 )
50 nfv ⊢ Ⅎ 𝑡 𝑚 ∈ ℕ
51 2 50 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑚 ∈ ℕ )
52 nfv ⊢ Ⅎ 𝑡 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟
53 51 52 nfan ⊢ Ⅎ 𝑡 ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 )
54 nfv ⊢ Ⅎ 𝑤 𝑚 ∈ ℕ
55 3 54 nfan ⊢ Ⅎ 𝑤 ( 𝜑 ∧ 𝑚 ∈ ℕ )
56 nfv ⊢ Ⅎ 𝑤 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟
57 55 56 nfan ⊢ Ⅎ 𝑤 ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 )
58 eqid ⊢ ( 𝑤 ∈ 𝑟 ↦ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑚 ) ) < ( ℎ ‘ 𝑡 ) ) } ) = ( 𝑤 ∈ 𝑟 ↦ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑚 ) ) < ( ℎ ‘ 𝑡 ) ) } )
59 simplr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 ) → 𝑚 ∈ ℕ )
60 simpr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 ) → 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 )
61 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 ) → 𝐸 ∈ ℝ+ )
62 11 sselda ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝑇 )
63 notnot ⊢ ( 𝑏 ∈ 𝐵 → ¬ ¬ 𝑏 ∈ 𝐵 )
64 63 intnand ⊢ ( 𝑏 ∈ 𝐵 → ¬ ( 𝑏 ∈ 𝑇 ∧ ¬ 𝑏 ∈ 𝐵 ) )
65 64 adantl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ¬ ( 𝑏 ∈ 𝑇 ∧ ¬ 𝑏 ∈ 𝐵 ) )
66 eldif ⊢ ( 𝑏 ∈ ( 𝑇 ∖ 𝐵 ) ↔ ( 𝑏 ∈ 𝑇 ∧ ¬ 𝑏 ∈ 𝐵 ) )
67 65 66 sylnibr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ¬ 𝑏 ∈ ( 𝑇 ∖ 𝐵 ) )
68 4 eleq2i ⊢ ( 𝑏 ∈ 𝑈 ↔ 𝑏 ∈ ( 𝑇 ∖ 𝐵 ) )
69 67 68 sylnibr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ¬ 𝑏 ∈ 𝑈 )
70 62 69 eldifd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ ( 𝑇 ∖ 𝑈 ) )
71 70 ralrimiva ⊢ ( 𝜑 → ∀ 𝑏 ∈ 𝐵 𝑏 ∈ ( 𝑇 ∖ 𝑈 ) )
72 dfss3 ⊢ ( 𝐵 ⊆ ( 𝑇 ∖ 𝑈 ) ↔ ∀ 𝑏 ∈ 𝐵 𝑏 ∈ ( 𝑇 ∖ 𝑈 ) )
73 71 72 sylibr ⊢ ( 𝜑 → 𝐵 ⊆ ( 𝑇 ∖ 𝑈 ) )
74 73 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 ) → 𝐵 ⊆ ( 𝑇 ∖ 𝑈 ) )
75 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 ) → 𝑊 ∈ V )
76 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 ) → 𝐴 ∈ V )
77 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 ) → 𝑟 ∈ Fin )
78 mptfi ⊢ ( 𝑟 ∈ Fin → ( 𝑤 ∈ 𝑟 ↦ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑚 ) ) < ( ℎ ‘ 𝑡 ) ) } ) ∈ Fin )
79 rnfi ⊢ ( ( 𝑤 ∈ 𝑟 ↦ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑚 ) ) < ( ℎ ‘ 𝑡 ) ) } ) ∈ Fin → ran ( 𝑤 ∈ 𝑟 ↦ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑚 ) ) < ( ℎ ‘ 𝑡 ) ) } ) ∈ Fin )
80 77 78 79 3syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 ) → ran ( 𝑤 ∈ 𝑟 ↦ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑚 ) ) < ( ℎ ‘ 𝑡 ) ) } ) ∈ Fin )
81 49 53 57 5 6 58 38 59 60 61 74 75 76 80 stoweidlem31 ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 ) → ∃ 𝑥 ( 𝑥 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
82 39 45 81 3jca ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 ) → ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑊 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑥 ( 𝑥 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) )
83 82 ex ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 → ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑊 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑥 ( 𝑥 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) ) )
84 83 eximdv ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ∃ 𝑣 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 → ∃ 𝑣 ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑊 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑥 ( 𝑥 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) ) )
85 84 reximdva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ℕ ∃ 𝑣 𝑣 : ( 1 ... 𝑚 ) –1-1-onto→ 𝑟 → ∃ 𝑚 ∈ ℕ ∃ 𝑣 ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑊 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑥 ( 𝑥 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) ) )
86 32 85 mpd ⊢ ( 𝜑 → ∃ 𝑚 ∈ ℕ ∃ 𝑣 ( 𝑣 : ( 1 ... 𝑚 ) ⟶ 𝑊 ∧ 𝐷 ⊆ ∪ ran 𝑣 ∧ ∃ 𝑥 ( 𝑥 : ( 1 ... 𝑚 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑚 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑚 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑚 ) ) < ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) )