Metamath Proof Explorer

Theorem hoiqssbllem3

Description: A n-dimensional ball contains a nonempty half-open interval with vertices with rational components. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses hoiqssbllem3.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
hoiqssbllem3.n ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
hoiqssbllem3.y ⊢ ( 𝜑 → 𝑌 ∈ ( ℝ ↑m 𝑋 ) )
hoiqssbllem3.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
Assertion hoiqssbllem3 ( 𝜑 → ∃ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ( 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ∧ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 hoiqssbllem3.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
2 hoiqssbllem3.n ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
3 hoiqssbllem3.y ⊢ ( 𝜑 → 𝑌 ∈ ( ℝ ↑m 𝑋 ) )
4 hoiqssbllem3.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
5 qex ⊢ ℚ ∈ V
6 5 inex1 ⊢ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∈ V
7 6 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∈ V )
8 elmapi ⊢ ( 𝑌 ∈ ( ℝ ↑m 𝑋 ) → 𝑌 : 𝑋 ⟶ ℝ )
9 3 8 syl ⊢ ( 𝜑 → 𝑌 : 𝑋 ⟶ ℝ )
10 9 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑌 ‘ 𝑖 ) ∈ ℝ )
11 2rp ⊢ 2 ∈ ℝ+
12 11 a1i ⊢ ( 𝜑 → 2 ∈ ℝ+ )
13 hashnncl ⊢ ( 𝑋 ∈ Fin → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) )
14 1 13 syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) )
15 2 14 mpbird ⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℕ )
16 nnrp ⊢ ( ( ♯ ‘ 𝑋 ) ∈ ℕ → ( ♯ ‘ 𝑋 ) ∈ ℝ+ )
17 15 16 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℝ+ )
18 17 rpsqrtcld ⊢ ( 𝜑 → ( √ ‘ ( ♯ ‘ 𝑋 ) ) ∈ ℝ+ )
19 12 18 rpmulcld ⊢ ( 𝜑 → ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ∈ ℝ+ )
20 4 19 rpdivcld ⊢ ( 𝜑 → ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ∈ ℝ+ )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ∈ ℝ+ )
22 10 21 ltsubrpd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) < ( 𝑌 ‘ 𝑖 ) )
23 21 rpred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ∈ ℝ )
24 10 23 resubcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ )
25 24 10 ltnled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) < ( 𝑌 ‘ 𝑖 ) ↔ ¬ ( 𝑌 ‘ 𝑖 ) ≤ ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) )
26 22 25 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ¬ ( 𝑌 ‘ 𝑖 ) ≤ ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) )
27 24 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ* )
28 10 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑌 ‘ 𝑖 ) ∈ ℝ* )
29 27 28 qinioo ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) = ∅ ↔ ( 𝑌 ‘ 𝑖 ) ≤ ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) )
30 26 29 mtbird ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ¬ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) = ∅ )
31 30 neqned ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ≠ ∅ )
32 1 7 31 choicefi ⊢ ( 𝜑 → ∃ 𝑐 ( 𝑐 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ) )
33 simpl ⊢ ( ( 𝑐 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ) → 𝑐 Fn 𝑋 )
34 nfra1 ⊢ Ⅎ 𝑖 ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) )
35 rspa ⊢ ( ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) )
36 elinel1 ⊢ ( ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) → ( 𝑐 ‘ 𝑖 ) ∈ ℚ )
37 35 36 syl ⊢ ( ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑐 ‘ 𝑖 ) ∈ ℚ )
38 37 ex ⊢ ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) → ( 𝑖 ∈ 𝑋 → ( 𝑐 ‘ 𝑖 ) ∈ ℚ ) )
39 34 38 ralrimi ⊢ ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) → ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ℚ )
40 39 adantl ⊢ ( ( 𝑐 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ) → ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ℚ )
41 33 40 jca ⊢ ( ( 𝑐 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ) → ( 𝑐 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ℚ ) )
42 41 adantl ⊢ ( ( 𝜑 ∧ ( 𝑐 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ) ) → ( 𝑐 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ℚ ) )
43 ffnfv ⊢ ( 𝑐 : 𝑋 ⟶ ℚ ↔ ( 𝑐 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ℚ ) )
44 42 43 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑐 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ) ) → 𝑐 : 𝑋 ⟶ ℚ )
45 5 a1i ⊢ ( 𝜑 → ℚ ∈ V )
46 elmapg ⊢ ( ( ℚ ∈ V ∧ 𝑋 ∈ Fin ) → ( 𝑐 ∈ ( ℚ ↑m 𝑋 ) ↔ 𝑐 : 𝑋 ⟶ ℚ ) )
47 45 1 46 syl2anc ⊢ ( 𝜑 → ( 𝑐 ∈ ( ℚ ↑m 𝑋 ) ↔ 𝑐 : 𝑋 ⟶ ℚ ) )
48 47 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ) ) → ( 𝑐 ∈ ( ℚ ↑m 𝑋 ) ↔ 𝑐 : 𝑋 ⟶ ℚ ) )
49 44 48 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑐 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ) ) → 𝑐 ∈ ( ℚ ↑m 𝑋 ) )
50 simprr ⊢ ( ( 𝜑 ∧ ( 𝑐 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ) ) → ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) )
51 49 50 jca ⊢ ( ( 𝜑 ∧ ( 𝑐 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ) ) → ( 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ) )
52 51 ex ⊢ ( 𝜑 → ( ( 𝑐 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ) → ( 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ) ) )
53 52 eximdv ⊢ ( 𝜑 → ( ∃ 𝑐 ( 𝑐 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ) → ∃ 𝑐 ( 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ) ) )
54 32 53 mpd ⊢ ( 𝜑 → ∃ 𝑐 ( 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ) )
55 df-rex ⊢ ( ∃ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ↔ ∃ 𝑐 ( 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ) )
56 54 55 sylibr ⊢ ( 𝜑 → ∃ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) )
57 5 inex1 ⊢ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ∈ V
58 57 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ∈ V )
59 10 21 ltaddrpd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( 𝑌 ‘ 𝑖 ) < ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) )
60 10 23 readdcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ )
61 10 60 ltnled ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑌 ‘ 𝑖 ) < ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ↔ ¬ ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ≤ ( 𝑌 ‘ 𝑖 ) ) )
62 59 61 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ¬ ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ≤ ( 𝑌 ‘ 𝑖 ) )
63 60 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ∈ ℝ* )
64 28 63 qinioo ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) = ∅ ↔ ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ≤ ( 𝑌 ‘ 𝑖 ) ) )
65 62 64 mtbird ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ¬ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) = ∅ )
66 65 neqned ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ) → ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ≠ ∅ )
67 1 58 66 choicefi ⊢ ( 𝜑 → ∃ 𝑑 ( 𝑑 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) )
68 simpl ⊢ ( ( 𝑑 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) → 𝑑 Fn 𝑋 )
69 nfra1 ⊢ Ⅎ 𝑖 ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) )
70 rspa ⊢ ( ( ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) )
71 elinel1 ⊢ ( ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) → ( 𝑑 ‘ 𝑖 ) ∈ ℚ )
72 70 71 syl ⊢ ( ( ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑑 ‘ 𝑖 ) ∈ ℚ )
73 72 ex ⊢ ( ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) → ( 𝑖 ∈ 𝑋 → ( 𝑑 ‘ 𝑖 ) ∈ ℚ ) )
74 69 73 ralrimi ⊢ ( ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) → ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ℚ )
75 74 adantl ⊢ ( ( 𝑑 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) → ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ℚ )
76 68 75 jca ⊢ ( ( 𝑑 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) → ( 𝑑 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ℚ ) )
77 76 adantl ⊢ ( ( 𝜑 ∧ ( 𝑑 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) → ( 𝑑 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ℚ ) )
78 ffnfv ⊢ ( 𝑑 : 𝑋 ⟶ ℚ ↔ ( 𝑑 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ℚ ) )
79 77 78 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑑 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) → 𝑑 : 𝑋 ⟶ ℚ )
80 elmapg ⊢ ( ( ℚ ∈ V ∧ 𝑋 ∈ Fin ) → ( 𝑑 ∈ ( ℚ ↑m 𝑋 ) ↔ 𝑑 : 𝑋 ⟶ ℚ ) )
81 45 1 80 syl2anc ⊢ ( 𝜑 → ( 𝑑 ∈ ( ℚ ↑m 𝑋 ) ↔ 𝑑 : 𝑋 ⟶ ℚ ) )
82 81 adantr ⊢ ( ( 𝜑 ∧ ( 𝑑 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) → ( 𝑑 ∈ ( ℚ ↑m 𝑋 ) ↔ 𝑑 : 𝑋 ⟶ ℚ ) )
83 79 82 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑑 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) → 𝑑 ∈ ( ℚ ↑m 𝑋 ) )
84 simprr ⊢ ( ( 𝜑 ∧ ( 𝑑 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) → ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) )
85 83 84 jca ⊢ ( ( 𝜑 ∧ ( 𝑑 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) → ( 𝑑 ∈ ( ℚ ↑m 𝑋 ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) )
86 85 ex ⊢ ( 𝜑 → ( ( 𝑑 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) → ( 𝑑 ∈ ( ℚ ↑m 𝑋 ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) )
87 86 eximdv ⊢ ( 𝜑 → ( ∃ 𝑑 ( 𝑑 Fn 𝑋 ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) → ∃ 𝑑 ( 𝑑 ∈ ( ℚ ↑m 𝑋 ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) )
88 67 87 mpd ⊢ ( 𝜑 → ∃ 𝑑 ( 𝑑 ∈ ( ℚ ↑m 𝑋 ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) )
89 df-rex ⊢ ( ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ↔ ∃ 𝑑 ( 𝑑 ∈ ( ℚ ↑m 𝑋 ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) )
90 88 89 sylibr ⊢ ( 𝜑 → ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) )
91 56 90 jca ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) )
92 reeanv ⊢ ( ∃ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ↔ ( ∃ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) )
93 91 92 sylibr ⊢ ( 𝜑 → ∃ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) )
94 nfv ⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) )
95 34 69 nfan ⊢ Ⅎ 𝑖 ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) )
96 94 95 nfan ⊢ Ⅎ 𝑖 ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ) ∧ ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) )
97 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ) ∧ ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) → 𝑋 ∈ Fin )
98 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ) ∧ ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) → 𝑋 ≠ ∅ )
99 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ) ∧ ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) → 𝑌 ∈ ( ℝ ↑m 𝑋 ) )
100 elmapi ⊢ ( 𝑐 ∈ ( ℚ ↑m 𝑋 ) → 𝑐 : 𝑋 ⟶ ℚ )
101 qssre ⊢ ℚ ⊆ ℝ
102 101 a1i ⊢ ( 𝑐 ∈ ( ℚ ↑m 𝑋 ) → ℚ ⊆ ℝ )
103 100 102 fssd ⊢ ( 𝑐 ∈ ( ℚ ↑m 𝑋 ) → 𝑐 : 𝑋 ⟶ ℝ )
104 103 adantl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) → 𝑐 : 𝑋 ⟶ ℝ )
105 104 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ) ∧ ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) → 𝑐 : 𝑋 ⟶ ℝ )
106 elmapi ⊢ ( 𝑑 ∈ ( ℚ ↑m 𝑋 ) → 𝑑 : 𝑋 ⟶ ℚ )
107 101 a1i ⊢ ( 𝑑 ∈ ( ℚ ↑m 𝑋 ) → ℚ ⊆ ℝ )
108 106 107 fssd ⊢ ( 𝑑 ∈ ( ℚ ↑m 𝑋 ) → 𝑑 : 𝑋 ⟶ ℝ )
109 108 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ) ∧ ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) → 𝑑 : 𝑋 ⟶ ℝ )
110 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ) ∧ ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) → 𝐸 ∈ ℝ+ )
111 35 elin2d ⊢ ( ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑐 ‘ 𝑖 ) ∈ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) )
112 111 adantlr ⊢ ( ( ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑐 ‘ 𝑖 ) ∈ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) )
113 112 adantll ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ) ∧ ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑐 ‘ 𝑖 ) ∈ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) )
114 70 elin2d ⊢ ( ( ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑑 ‘ 𝑖 ) ∈ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) )
115 114 adantll ⊢ ( ( ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑑 ‘ 𝑖 ) ∈ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) )
116 115 adantll ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ) ∧ ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑑 ‘ 𝑖 ) ∈ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) )
117 96 97 98 99 105 109 110 113 116 hoiqssbllem1 ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ) ∧ ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) → 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) )
118 simpl ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ) ∧ ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) → ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ) )
119 fveq2 ⊢ ( 𝑖 = 𝑘 → ( 𝑐 ‘ 𝑖 ) = ( 𝑐 ‘ 𝑘 ) )
120 fveq2 ⊢ ( 𝑖 = 𝑘 → ( 𝑌 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑘 ) )
121 120 oveq1d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) = ( ( 𝑌 ‘ 𝑘 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) )
122 121 120 oveq12d ⊢ ( 𝑖 = 𝑘 → ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) = ( ( ( 𝑌 ‘ 𝑘 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑘 ) ) )
123 122 ineq2d ⊢ ( 𝑖 = 𝑘 → ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) = ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑘 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑘 ) ) ) )
124 119 123 eleq12d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ↔ ( 𝑐 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑘 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑘 ) ) ) ) )
125 124 cbvralvw ⊢ ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ↔ ∀ 𝑘 ∈ 𝑋 ( 𝑐 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑘 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑘 ) ) ) )
126 125 biimpi ⊢ ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) → ∀ 𝑘 ∈ 𝑋 ( 𝑐 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑘 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑘 ) ) ) )
127 126 adantr ⊢ ( ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) → ∀ 𝑘 ∈ 𝑋 ( 𝑐 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑘 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑘 ) ) ) )
128 fveq2 ⊢ ( 𝑖 = 𝑘 → ( 𝑑 ‘ 𝑖 ) = ( 𝑑 ‘ 𝑘 ) )
129 120 oveq1d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) = ( ( 𝑌 ‘ 𝑘 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) )
130 120 129 oveq12d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) = ( ( 𝑌 ‘ 𝑘 ) (,) ( ( 𝑌 ‘ 𝑘 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) )
131 130 ineq2d ⊢ ( 𝑖 = 𝑘 → ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) = ( ℚ ∩ ( ( 𝑌 ‘ 𝑘 ) (,) ( ( 𝑌 ‘ 𝑘 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) )
132 128 131 eleq12d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ↔ ( 𝑑 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑘 ) (,) ( ( 𝑌 ‘ 𝑘 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) )
133 132 cbvralvw ⊢ ( ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ↔ ∀ 𝑘 ∈ 𝑋 ( 𝑑 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑘 ) (,) ( ( 𝑌 ‘ 𝑘 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) )
134 133 biimpi ⊢ ( ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) → ∀ 𝑘 ∈ 𝑋 ( 𝑑 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑘 ) (,) ( ( 𝑌 ‘ 𝑘 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) )
135 134 adantl ⊢ ( ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) → ∀ 𝑘 ∈ 𝑋 ( 𝑑 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑘 ) (,) ( ( 𝑌 ‘ 𝑘 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) )
136 127 135 jca ⊢ ( ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) → ( ∀ 𝑘 ∈ 𝑋 ( 𝑐 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑘 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑘 ) ) ) ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑑 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑘 ) (,) ( ( 𝑌 ‘ 𝑘 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) )
137 136 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ) ∧ ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) → ( ∀ 𝑘 ∈ 𝑋 ( 𝑐 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑘 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑘 ) ) ) ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑑 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑘 ) (,) ( ( 𝑌 ‘ 𝑘 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) )
138 nfv ⊢ Ⅎ 𝑖 ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ) ∧ ( ∀ 𝑘 ∈ 𝑋 ( 𝑐 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑘 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑘 ) ) ) ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑑 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑘 ) (,) ( ( 𝑌 ‘ 𝑘 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) )
139 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ) ∧ ( ∀ 𝑘 ∈ 𝑋 ( 𝑐 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑘 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑘 ) ) ) ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑑 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑘 ) (,) ( ( 𝑌 ‘ 𝑘 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) → 𝑋 ∈ Fin )
140 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ) ∧ ( ∀ 𝑘 ∈ 𝑋 ( 𝑐 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑘 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑘 ) ) ) ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑑 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑘 ) (,) ( ( 𝑌 ‘ 𝑘 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) → 𝑋 ≠ ∅ )
141 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ) ∧ ( ∀ 𝑘 ∈ 𝑋 ( 𝑐 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑘 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑘 ) ) ) ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑑 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑘 ) (,) ( ( 𝑌 ‘ 𝑘 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) → 𝑌 ∈ ( ℝ ↑m 𝑋 ) )
142 104 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ) ∧ ( ∀ 𝑘 ∈ 𝑋 ( 𝑐 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑘 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑘 ) ) ) ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑑 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑘 ) (,) ( ( 𝑌 ‘ 𝑘 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) → 𝑐 : 𝑋 ⟶ ℝ )
143 108 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ) ∧ ( ∀ 𝑘 ∈ 𝑋 ( 𝑐 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑘 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑘 ) ) ) ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑑 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑘 ) (,) ( ( 𝑌 ‘ 𝑘 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) → 𝑑 : 𝑋 ⟶ ℝ )
144 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ) ∧ ( ∀ 𝑘 ∈ 𝑋 ( 𝑐 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑘 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑘 ) ) ) ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑑 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑘 ) (,) ( ( 𝑌 ‘ 𝑘 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) → 𝐸 ∈ ℝ+ )
145 125 111 sylanbr ⊢ ( ( ∀ 𝑘 ∈ 𝑋 ( 𝑐 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑘 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑘 ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑐 ‘ 𝑖 ) ∈ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) )
146 145 adantlr ⊢ ( ( ( ∀ 𝑘 ∈ 𝑋 ( 𝑐 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑘 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑘 ) ) ) ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑑 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑘 ) (,) ( ( 𝑌 ‘ 𝑘 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑐 ‘ 𝑖 ) ∈ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) )
147 146 adantll ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ) ∧ ( ∀ 𝑘 ∈ 𝑋 ( 𝑐 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑘 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑘 ) ) ) ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑑 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑘 ) (,) ( ( 𝑌 ‘ 𝑘 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑐 ‘ 𝑖 ) ∈ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) )
148 133 114 sylanbr ⊢ ( ( ∀ 𝑘 ∈ 𝑋 ( 𝑑 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑘 ) (,) ( ( 𝑌 ‘ 𝑘 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑑 ‘ 𝑖 ) ∈ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) )
149 148 adantll ⊢ ( ( ( ∀ 𝑘 ∈ 𝑋 ( 𝑐 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑘 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑘 ) ) ) ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑑 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑘 ) (,) ( ( 𝑌 ‘ 𝑘 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑑 ‘ 𝑖 ) ∈ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) )
150 149 adantll ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ) ∧ ( ∀ 𝑘 ∈ 𝑋 ( 𝑐 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑘 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑘 ) ) ) ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑑 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑘 ) (,) ( ( 𝑌 ‘ 𝑘 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) ∧ 𝑖 ∈ 𝑋 ) → ( 𝑑 ‘ 𝑖 ) ∈ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) )
151 138 139 140 141 142 143 144 147 150 hoiqssbllem2 ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ) ∧ ( ∀ 𝑘 ∈ 𝑋 ( 𝑐 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑘 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑘 ) ) ) ∧ ∀ 𝑘 ∈ 𝑋 ( 𝑑 ‘ 𝑘 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑘 ) (,) ( ( 𝑌 ‘ 𝑘 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) → X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) )
152 118 137 151 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ) ∧ ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) → X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) )
153 117 152 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ) ∧ ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) ) → ( 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ∧ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) ) )
154 153 ex ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) ∧ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ) → ( ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) → ( 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ∧ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) ) ) )
155 154 reximdva ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ) → ( ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) → ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ( 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ∧ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) ) ) )
156 155 reximdva ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ( ∀ 𝑖 ∈ 𝑋 ( 𝑐 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( ( 𝑌 ‘ 𝑖 ) − ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) (,) ( 𝑌 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ 𝑋 ( 𝑑 ‘ 𝑖 ) ∈ ( ℚ ∩ ( ( 𝑌 ‘ 𝑖 ) (,) ( ( 𝑌 ‘ 𝑖 ) + ( 𝐸 / ( 2 · ( √ ‘ ( ♯ ‘ 𝑋 ) ) ) ) ) ) ) ) → ∃ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ( 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ∧ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) ) ) )
157 93 156 mpd ⊢ ( 𝜑 → ∃ 𝑐 ∈ ( ℚ ↑m 𝑋 ) ∃ 𝑑 ∈ ( ℚ ↑m 𝑋 ) ( 𝑌 ∈ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ∧ X 𝑖 ∈ 𝑋 ( ( 𝑐 ‘ 𝑖 ) [,) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( 𝑌 ( ball ‘ ( dist ‘ ( ℝ^ ‘ 𝑋 ) ) ) 𝐸 ) ) )