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