Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hoiqssbllem3 Structured version   Visualization version   GIF version

Theorem hoiqssbllem3 41410
Description: A n-dimensional ball contains a nonempty half-open interval with vertices with rational components. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
Hypotheses
Ref Expression
hoiqssbllem3.x (𝜑𝑋 ∈ Fin)
hoiqssbllem3.n (𝜑𝑋 ≠ ∅)
hoiqssbllem3.y (𝜑𝑌 ∈ (ℝ ↑𝑚 𝑋))
hoiqssbllem3.e (𝜑𝐸 ∈ ℝ+)
Assertion
Ref Expression
hoiqssbllem3 (𝜑 → ∃𝑐 ∈ (ℚ ↑𝑚 𝑋)∃𝑑 ∈ (ℚ ↑𝑚 𝑋)(𝑌X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ∧ X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸)))
Distinct variable groups:   𝐸,𝑐,𝑑,𝑖   𝑋,𝑐,𝑑,𝑖   𝑌,𝑐,𝑑,𝑖   𝜑,𝑐,𝑑,𝑖

Proof of Theorem hoiqssbllem3
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 hoiqssbllem3.x . . . . . . 7 (𝜑𝑋 ∈ Fin)
2 qex 12000 . . . . . . . . 9 ℚ ∈ V
32inex1 4959 . . . . . . . 8 (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∈ V
43a1i 11 . . . . . . 7 ((𝜑𝑖𝑋) → (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∈ V)
5 hoiqssbllem3.y . . . . . . . . . . . . 13 (𝜑𝑌 ∈ (ℝ ↑𝑚 𝑋))
6 elmapi 8081 . . . . . . . . . . . . 13 (𝑌 ∈ (ℝ ↑𝑚 𝑋) → 𝑌:𝑋⟶ℝ)
75, 6syl 17 . . . . . . . . . . . 12 (𝜑𝑌:𝑋⟶ℝ)
87ffvelrnda 6548 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → (𝑌𝑖) ∈ ℝ)
9 hoiqssbllem3.e . . . . . . . . . . . . 13 (𝜑𝐸 ∈ ℝ+)
10 2rp 12032 . . . . . . . . . . . . . . 15 2 ∈ ℝ+
1110a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 2 ∈ ℝ+)
12 hoiqssbllem3.n . . . . . . . . . . . . . . . . 17 (𝜑𝑋 ≠ ∅)
13 hashnncl 13358 . . . . . . . . . . . . . . . . . 18 (𝑋 ∈ Fin → ((♯‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅))
141, 13syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((♯‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅))
1512, 14mpbird 248 . . . . . . . . . . . . . . . 16 (𝜑 → (♯‘𝑋) ∈ ℕ)
16 nnrp 12040 . . . . . . . . . . . . . . . 16 ((♯‘𝑋) ∈ ℕ → (♯‘𝑋) ∈ ℝ+)
1715, 16syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (♯‘𝑋) ∈ ℝ+)
1817rpsqrtcld 14436 . . . . . . . . . . . . . 14 (𝜑 → (√‘(♯‘𝑋)) ∈ ℝ+)
1911, 18rpmulcld 12085 . . . . . . . . . . . . 13 (𝜑 → (2 · (√‘(♯‘𝑋))) ∈ ℝ+)
209, 19rpdivcld 12086 . . . . . . . . . . . 12 (𝜑 → (𝐸 / (2 · (√‘(♯‘𝑋)))) ∈ ℝ+)
2120adantr 472 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → (𝐸 / (2 · (√‘(♯‘𝑋)))) ∈ ℝ+)
228, 21ltsubrpd 12101 . . . . . . . . . 10 ((𝜑𝑖𝑋) → ((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) < (𝑌𝑖))
2321rpred 12069 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → (𝐸 / (2 · (√‘(♯‘𝑋)))) ∈ ℝ)
248, 23resubcld 10711 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → ((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ)
2524, 8ltnled 10437 . . . . . . . . . 10 ((𝜑𝑖𝑋) → (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) < (𝑌𝑖) ↔ ¬ (𝑌𝑖) ≤ ((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))))
2622, 25mpbid 223 . . . . . . . . 9 ((𝜑𝑖𝑋) → ¬ (𝑌𝑖) ≤ ((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))))
2724rexrd 10342 . . . . . . . . . 10 ((𝜑𝑖𝑋) → ((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ*)
288rexrd 10342 . . . . . . . . . 10 ((𝜑𝑖𝑋) → (𝑌𝑖) ∈ ℝ*)
2927, 28qinioo 40332 . . . . . . . . 9 ((𝜑𝑖𝑋) → ((ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) = ∅ ↔ (𝑌𝑖) ≤ ((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))))
3026, 29mtbird 316 . . . . . . . 8 ((𝜑𝑖𝑋) → ¬ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) = ∅)
3130neqned 2943 . . . . . . 7 ((𝜑𝑖𝑋) → (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ≠ ∅)
321, 4, 31choicefi 39969 . . . . . 6 (𝜑 → ∃𝑐(𝑐 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖)))))
33 simpl 474 . . . . . . . . . . . . 13 ((𝑐 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖)))) → 𝑐 Fn 𝑋)
34 nfra1 3087 . . . . . . . . . . . . . . 15 𝑖𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖)))
35 rspa 3076 . . . . . . . . . . . . . . . . 17 ((∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ 𝑖𝑋) → (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))))
36 elinel1 3960 . . . . . . . . . . . . . . . . 17 ((𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) → (𝑐𝑖) ∈ ℚ)
3735, 36syl 17 . . . . . . . . . . . . . . . 16 ((∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ 𝑖𝑋) → (𝑐𝑖) ∈ ℚ)
3837ex 401 . . . . . . . . . . . . . . 15 (∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) → (𝑖𝑋 → (𝑐𝑖) ∈ ℚ))
3934, 38ralrimi 3103 . . . . . . . . . . . . . 14 (∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) → ∀𝑖𝑋 (𝑐𝑖) ∈ ℚ)
4039adantl 473 . . . . . . . . . . . . 13 ((𝑐 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖)))) → ∀𝑖𝑋 (𝑐𝑖) ∈ ℚ)
4133, 40jca 507 . . . . . . . . . . . 12 ((𝑐 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖)))) → (𝑐 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑐𝑖) ∈ ℚ))
4241adantl 473 . . . . . . . . . . 11 ((𝜑 ∧ (𝑐 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))))) → (𝑐 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑐𝑖) ∈ ℚ))
43 ffnfv 6577 . . . . . . . . . . 11 (𝑐:𝑋⟶ℚ ↔ (𝑐 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑐𝑖) ∈ ℚ))
4442, 43sylibr 225 . . . . . . . . . 10 ((𝜑 ∧ (𝑐 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))))) → 𝑐:𝑋⟶ℚ)
452a1i 11 . . . . . . . . . . . 12 (𝜑 → ℚ ∈ V)
46 elmapg 8072 . . . . . . . . . . . 12 ((ℚ ∈ V ∧ 𝑋 ∈ Fin) → (𝑐 ∈ (ℚ ↑𝑚 𝑋) ↔ 𝑐:𝑋⟶ℚ))
4745, 1, 46syl2anc 579 . . . . . . . . . . 11 (𝜑 → (𝑐 ∈ (ℚ ↑𝑚 𝑋) ↔ 𝑐:𝑋⟶ℚ))
4847adantr 472 . . . . . . . . . 10 ((𝜑 ∧ (𝑐 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))))) → (𝑐 ∈ (ℚ ↑𝑚 𝑋) ↔ 𝑐:𝑋⟶ℚ))
4944, 48mpbird 248 . . . . . . . . 9 ((𝜑 ∧ (𝑐 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))))) → 𝑐 ∈ (ℚ ↑𝑚 𝑋))
50 simprr 789 . . . . . . . . 9 ((𝜑 ∧ (𝑐 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))))) → ∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))))
5149, 50jca 507 . . . . . . . 8 ((𝜑 ∧ (𝑐 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))))) → (𝑐 ∈ (ℚ ↑𝑚 𝑋) ∧ ∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖)))))
5251ex 401 . . . . . . 7 (𝜑 → ((𝑐 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖)))) → (𝑐 ∈ (ℚ ↑𝑚 𝑋) ∧ ∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))))))
5352eximdv 2012 . . . . . 6 (𝜑 → (∃𝑐(𝑐 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖)))) → ∃𝑐(𝑐 ∈ (ℚ ↑𝑚 𝑋) ∧ ∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))))))
5432, 53mpd 15 . . . . 5 (𝜑 → ∃𝑐(𝑐 ∈ (ℚ ↑𝑚 𝑋) ∧ ∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖)))))
55 df-rex 3060 . . . . 5 (∃𝑐 ∈ (ℚ ↑𝑚 𝑋)∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ↔ ∃𝑐(𝑐 ∈ (ℚ ↑𝑚 𝑋) ∧ ∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖)))))
5654, 55sylibr 225 . . . 4 (𝜑 → ∃𝑐 ∈ (ℚ ↑𝑚 𝑋)∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))))
572inex1 4959 . . . . . . . 8 (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) ∈ V
5857a1i 11 . . . . . . 7 ((𝜑𝑖𝑋) → (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) ∈ V)
598, 21ltaddrpd 12102 . . . . . . . . . 10 ((𝜑𝑖𝑋) → (𝑌𝑖) < ((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))
608, 23readdcld 10322 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → ((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ)
618, 60ltnled 10437 . . . . . . . . . 10 ((𝜑𝑖𝑋) → ((𝑌𝑖) < ((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ↔ ¬ ((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ≤ (𝑌𝑖)))
6259, 61mpbid 223 . . . . . . . . 9 ((𝜑𝑖𝑋) → ¬ ((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ≤ (𝑌𝑖))
6360rexrd 10342 . . . . . . . . . 10 ((𝜑𝑖𝑋) → ((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ∈ ℝ*)
6428, 63qinioo 40332 . . . . . . . . 9 ((𝜑𝑖𝑋) → ((ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) = ∅ ↔ ((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) ≤ (𝑌𝑖)))
6562, 64mtbird 316 . . . . . . . 8 ((𝜑𝑖𝑋) → ¬ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) = ∅)
6665neqned 2943 . . . . . . 7 ((𝜑𝑖𝑋) → (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) ≠ ∅)
671, 58, 66choicefi 39969 . . . . . 6 (𝜑 → ∃𝑑(𝑑 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))))
68 simpl 474 . . . . . . . . . . . . 13 ((𝑑 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))) → 𝑑 Fn 𝑋)
69 nfra1 3087 . . . . . . . . . . . . . . 15 𝑖𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))
70 rspa 3076 . . . . . . . . . . . . . . . . 17 ((∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) ∧ 𝑖𝑋) → (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))
71 elinel1 3960 . . . . . . . . . . . . . . . . 17 ((𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) → (𝑑𝑖) ∈ ℚ)
7270, 71syl 17 . . . . . . . . . . . . . . . 16 ((∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) ∧ 𝑖𝑋) → (𝑑𝑖) ∈ ℚ)
7372ex 401 . . . . . . . . . . . . . . 15 (∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) → (𝑖𝑋 → (𝑑𝑖) ∈ ℚ))
7469, 73ralrimi 3103 . . . . . . . . . . . . . 14 (∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) → ∀𝑖𝑋 (𝑑𝑖) ∈ ℚ)
7574adantl 473 . . . . . . . . . . . . 13 ((𝑑 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))) → ∀𝑖𝑋 (𝑑𝑖) ∈ ℚ)
7668, 75jca 507 . . . . . . . . . . . 12 ((𝑑 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))) → (𝑑 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ ℚ))
7776adantl 473 . . . . . . . . . . 11 ((𝜑 ∧ (𝑑 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) → (𝑑 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ ℚ))
78 ffnfv 6577 . . . . . . . . . . 11 (𝑑:𝑋⟶ℚ ↔ (𝑑 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ ℚ))
7977, 78sylibr 225 . . . . . . . . . 10 ((𝜑 ∧ (𝑑 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) → 𝑑:𝑋⟶ℚ)
80 elmapg 8072 . . . . . . . . . . . 12 ((ℚ ∈ V ∧ 𝑋 ∈ Fin) → (𝑑 ∈ (ℚ ↑𝑚 𝑋) ↔ 𝑑:𝑋⟶ℚ))
8145, 1, 80syl2anc 579 . . . . . . . . . . 11 (𝜑 → (𝑑 ∈ (ℚ ↑𝑚 𝑋) ↔ 𝑑:𝑋⟶ℚ))
8281adantr 472 . . . . . . . . . 10 ((𝜑 ∧ (𝑑 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) → (𝑑 ∈ (ℚ ↑𝑚 𝑋) ↔ 𝑑:𝑋⟶ℚ))
8379, 82mpbird 248 . . . . . . . . 9 ((𝜑 ∧ (𝑑 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) → 𝑑 ∈ (ℚ ↑𝑚 𝑋))
84 simprr 789 . . . . . . . . 9 ((𝜑 ∧ (𝑑 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) → ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))
8583, 84jca 507 . . . . . . . 8 ((𝜑 ∧ (𝑑 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) → (𝑑 ∈ (ℚ ↑𝑚 𝑋) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))))
8685ex 401 . . . . . . 7 (𝜑 → ((𝑑 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))) → (𝑑 ∈ (ℚ ↑𝑚 𝑋) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))))
8786eximdv 2012 . . . . . 6 (𝜑 → (∃𝑑(𝑑 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))) → ∃𝑑(𝑑 ∈ (ℚ ↑𝑚 𝑋) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))))
8867, 87mpd 15 . . . . 5 (𝜑 → ∃𝑑(𝑑 ∈ (ℚ ↑𝑚 𝑋) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))))
89 df-rex 3060 . . . . 5 (∃𝑑 ∈ (ℚ ↑𝑚 𝑋)∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) ↔ ∃𝑑(𝑑 ∈ (ℚ ↑𝑚 𝑋) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))))
9088, 89sylibr 225 . . . 4 (𝜑 → ∃𝑑 ∈ (ℚ ↑𝑚 𝑋)∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))
9156, 90jca 507 . . 3 (𝜑 → (∃𝑐 ∈ (ℚ ↑𝑚 𝑋)∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∃𝑑 ∈ (ℚ ↑𝑚 𝑋)∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))))
92 reeanv 3253 . . 3 (∃𝑐 ∈ (ℚ ↑𝑚 𝑋)∃𝑑 ∈ (ℚ ↑𝑚 𝑋)(∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))) ↔ (∃𝑐 ∈ (ℚ ↑𝑚 𝑋)∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∃𝑑 ∈ (ℚ ↑𝑚 𝑋)∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))))
9391, 92sylibr 225 . 2 (𝜑 → ∃𝑐 ∈ (ℚ ↑𝑚 𝑋)∃𝑑 ∈ (ℚ ↑𝑚 𝑋)(∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))))
94 nfv 2009 . . . . . . . 8 𝑖((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋))
9534, 69nfan 1998 . . . . . . . 8 𝑖(∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))
9694, 95nfan 1998 . . . . . . 7 𝑖(((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))))
971ad3antrrr 721 . . . . . . 7 ((((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) → 𝑋 ∈ Fin)
9812ad3antrrr 721 . . . . . . 7 ((((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) → 𝑋 ≠ ∅)
995ad3antrrr 721 . . . . . . 7 ((((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) → 𝑌 ∈ (ℝ ↑𝑚 𝑋))
100 elmapi 8081 . . . . . . . . . 10 (𝑐 ∈ (ℚ ↑𝑚 𝑋) → 𝑐:𝑋⟶ℚ)
101 qssre 11998 . . . . . . . . . . 11 ℚ ⊆ ℝ
102101a1i 11 . . . . . . . . . 10 (𝑐 ∈ (ℚ ↑𝑚 𝑋) → ℚ ⊆ ℝ)
103100, 102fssd 6236 . . . . . . . . 9 (𝑐 ∈ (ℚ ↑𝑚 𝑋) → 𝑐:𝑋⟶ℝ)
104103adantl 473 . . . . . . . 8 ((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) → 𝑐:𝑋⟶ℝ)
105104ad2antrr 717 . . . . . . 7 ((((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) → 𝑐:𝑋⟶ℝ)
106 elmapi 8081 . . . . . . . . 9 (𝑑 ∈ (ℚ ↑𝑚 𝑋) → 𝑑:𝑋⟶ℚ)
107101a1i 11 . . . . . . . . 9 (𝑑 ∈ (ℚ ↑𝑚 𝑋) → ℚ ⊆ ℝ)
108106, 107fssd 6236 . . . . . . . 8 (𝑑 ∈ (ℚ ↑𝑚 𝑋) → 𝑑:𝑋⟶ℝ)
109108ad2antlr 718 . . . . . . 7 ((((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) → 𝑑:𝑋⟶ℝ)
1109ad3antrrr 721 . . . . . . 7 ((((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) → 𝐸 ∈ ℝ+)
11135elin2d 3964 . . . . . . . . 9 ((∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ 𝑖𝑋) → (𝑐𝑖) ∈ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖)))
112111adantlr 706 . . . . . . . 8 (((∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))) ∧ 𝑖𝑋) → (𝑐𝑖) ∈ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖)))
113112adantll 705 . . . . . . 7 (((((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) ∧ 𝑖𝑋) → (𝑐𝑖) ∈ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖)))
11470elin2d 3964 . . . . . . . . 9 ((∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) ∧ 𝑖𝑋) → (𝑑𝑖) ∈ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))
115114adantll 705 . . . . . . . 8 (((∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))) ∧ 𝑖𝑋) → (𝑑𝑖) ∈ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))
116115adantll 705 . . . . . . 7 (((((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) ∧ 𝑖𝑋) → (𝑑𝑖) ∈ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))
11796, 97, 98, 99, 105, 109, 110, 113, 116hoiqssbllem1 41408 . . . . . 6 ((((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) → 𝑌X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)))
118 simpl 474 . . . . . . 7 ((((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) → ((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)))
119 fveq2 6374 . . . . . . . . . . . . 13 (𝑖 = 𝑘 → (𝑐𝑖) = (𝑐𝑘))
120 fveq2 6374 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑘 → (𝑌𝑖) = (𝑌𝑘))
121120oveq1d 6856 . . . . . . . . . . . . . . 15 (𝑖 = 𝑘 → ((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋))))) = ((𝑌𝑘) − (𝐸 / (2 · (√‘(♯‘𝑋))))))
122121, 120oveq12d 6859 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖)) = (((𝑌𝑘) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑘)))
123122ineq2d 3975 . . . . . . . . . . . . 13 (𝑖 = 𝑘 → (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) = (ℚ ∩ (((𝑌𝑘) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑘))))
124119, 123eleq12d 2837 . . . . . . . . . . . 12 (𝑖 = 𝑘 → ((𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ↔ (𝑐𝑘) ∈ (ℚ ∩ (((𝑌𝑘) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑘)))))
125124cbvralv 3318 . . . . . . . . . . 11 (∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ↔ ∀𝑘𝑋 (𝑐𝑘) ∈ (ℚ ∩ (((𝑌𝑘) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑘))))
126125biimpi 207 . . . . . . . . . 10 (∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) → ∀𝑘𝑋 (𝑐𝑘) ∈ (ℚ ∩ (((𝑌𝑘) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑘))))
127126adantr 472 . . . . . . . . 9 ((∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))) → ∀𝑘𝑋 (𝑐𝑘) ∈ (ℚ ∩ (((𝑌𝑘) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑘))))
128 fveq2 6374 . . . . . . . . . . . . 13 (𝑖 = 𝑘 → (𝑑𝑖) = (𝑑𝑘))
129120oveq1d 6856 . . . . . . . . . . . . . . 15 (𝑖 = 𝑘 → ((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))) = ((𝑌𝑘) + (𝐸 / (2 · (√‘(♯‘𝑋))))))
130120, 129oveq12d 6859 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))) = ((𝑌𝑘)(,)((𝑌𝑘) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))
131130ineq2d 3975 . . . . . . . . . . . . 13 (𝑖 = 𝑘 → (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) = (ℚ ∩ ((𝑌𝑘)(,)((𝑌𝑘) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))
132128, 131eleq12d 2837 . . . . . . . . . . . 12 (𝑖 = 𝑘 → ((𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) ↔ (𝑑𝑘) ∈ (ℚ ∩ ((𝑌𝑘)(,)((𝑌𝑘) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))))
133132cbvralv 3318 . . . . . . . . . . 11 (∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) ↔ ∀𝑘𝑋 (𝑑𝑘) ∈ (ℚ ∩ ((𝑌𝑘)(,)((𝑌𝑘) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))
134133biimpi 207 . . . . . . . . . 10 (∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) → ∀𝑘𝑋 (𝑑𝑘) ∈ (ℚ ∩ ((𝑌𝑘)(,)((𝑌𝑘) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))
135134adantl 473 . . . . . . . . 9 ((∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))) → ∀𝑘𝑋 (𝑑𝑘) ∈ (ℚ ∩ ((𝑌𝑘)(,)((𝑌𝑘) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))
136127, 135jca 507 . . . . . . . 8 ((∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))) → (∀𝑘𝑋 (𝑐𝑘) ∈ (ℚ ∩ (((𝑌𝑘) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑘))) ∧ ∀𝑘𝑋 (𝑑𝑘) ∈ (ℚ ∩ ((𝑌𝑘)(,)((𝑌𝑘) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))))
137136adantl 473 . . . . . . 7 ((((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) → (∀𝑘𝑋 (𝑐𝑘) ∈ (ℚ ∩ (((𝑌𝑘) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑘))) ∧ ∀𝑘𝑋 (𝑑𝑘) ∈ (ℚ ∩ ((𝑌𝑘)(,)((𝑌𝑘) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))))
138 nfv 2009 . . . . . . . 8 𝑖(((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (∀𝑘𝑋 (𝑐𝑘) ∈ (ℚ ∩ (((𝑌𝑘) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑘))) ∧ ∀𝑘𝑋 (𝑑𝑘) ∈ (ℚ ∩ ((𝑌𝑘)(,)((𝑌𝑘) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))))
1391ad3antrrr 721 . . . . . . . 8 ((((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (∀𝑘𝑋 (𝑐𝑘) ∈ (ℚ ∩ (((𝑌𝑘) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑘))) ∧ ∀𝑘𝑋 (𝑑𝑘) ∈ (ℚ ∩ ((𝑌𝑘)(,)((𝑌𝑘) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) → 𝑋 ∈ Fin)
14012ad3antrrr 721 . . . . . . . 8 ((((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (∀𝑘𝑋 (𝑐𝑘) ∈ (ℚ ∩ (((𝑌𝑘) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑘))) ∧ ∀𝑘𝑋 (𝑑𝑘) ∈ (ℚ ∩ ((𝑌𝑘)(,)((𝑌𝑘) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) → 𝑋 ≠ ∅)
1415ad3antrrr 721 . . . . . . . 8 ((((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (∀𝑘𝑋 (𝑐𝑘) ∈ (ℚ ∩ (((𝑌𝑘) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑘))) ∧ ∀𝑘𝑋 (𝑑𝑘) ∈ (ℚ ∩ ((𝑌𝑘)(,)((𝑌𝑘) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) → 𝑌 ∈ (ℝ ↑𝑚 𝑋))
142104ad2antrr 717 . . . . . . . 8 ((((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (∀𝑘𝑋 (𝑐𝑘) ∈ (ℚ ∩ (((𝑌𝑘) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑘))) ∧ ∀𝑘𝑋 (𝑑𝑘) ∈ (ℚ ∩ ((𝑌𝑘)(,)((𝑌𝑘) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) → 𝑐:𝑋⟶ℝ)
143108ad2antlr 718 . . . . . . . 8 ((((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (∀𝑘𝑋 (𝑐𝑘) ∈ (ℚ ∩ (((𝑌𝑘) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑘))) ∧ ∀𝑘𝑋 (𝑑𝑘) ∈ (ℚ ∩ ((𝑌𝑘)(,)((𝑌𝑘) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) → 𝑑:𝑋⟶ℝ)
1449ad3antrrr 721 . . . . . . . 8 ((((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (∀𝑘𝑋 (𝑐𝑘) ∈ (ℚ ∩ (((𝑌𝑘) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑘))) ∧ ∀𝑘𝑋 (𝑑𝑘) ∈ (ℚ ∩ ((𝑌𝑘)(,)((𝑌𝑘) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) → 𝐸 ∈ ℝ+)
145125, 111sylanbr 577 . . . . . . . . . 10 ((∀𝑘𝑋 (𝑐𝑘) ∈ (ℚ ∩ (((𝑌𝑘) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑘))) ∧ 𝑖𝑋) → (𝑐𝑖) ∈ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖)))
146145adantlr 706 . . . . . . . . 9 (((∀𝑘𝑋 (𝑐𝑘) ∈ (ℚ ∩ (((𝑌𝑘) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑘))) ∧ ∀𝑘𝑋 (𝑑𝑘) ∈ (ℚ ∩ ((𝑌𝑘)(,)((𝑌𝑘) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))) ∧ 𝑖𝑋) → (𝑐𝑖) ∈ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖)))
147146adantll 705 . . . . . . . 8 (((((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (∀𝑘𝑋 (𝑐𝑘) ∈ (ℚ ∩ (((𝑌𝑘) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑘))) ∧ ∀𝑘𝑋 (𝑑𝑘) ∈ (ℚ ∩ ((𝑌𝑘)(,)((𝑌𝑘) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) ∧ 𝑖𝑋) → (𝑐𝑖) ∈ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖)))
148133, 114sylanbr 577 . . . . . . . . . 10 ((∀𝑘𝑋 (𝑑𝑘) ∈ (ℚ ∩ ((𝑌𝑘)(,)((𝑌𝑘) + (𝐸 / (2 · (√‘(♯‘𝑋))))))) ∧ 𝑖𝑋) → (𝑑𝑖) ∈ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))
149148adantll 705 . . . . . . . . 9 (((∀𝑘𝑋 (𝑐𝑘) ∈ (ℚ ∩ (((𝑌𝑘) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑘))) ∧ ∀𝑘𝑋 (𝑑𝑘) ∈ (ℚ ∩ ((𝑌𝑘)(,)((𝑌𝑘) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))) ∧ 𝑖𝑋) → (𝑑𝑖) ∈ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))
150149adantll 705 . . . . . . . 8 (((((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (∀𝑘𝑋 (𝑐𝑘) ∈ (ℚ ∩ (((𝑌𝑘) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑘))) ∧ ∀𝑘𝑋 (𝑑𝑘) ∈ (ℚ ∩ ((𝑌𝑘)(,)((𝑌𝑘) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) ∧ 𝑖𝑋) → (𝑑𝑖) ∈ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))
151138, 139, 140, 141, 142, 143, 144, 147, 150hoiqssbllem2 41409 . . . . . . 7 ((((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (∀𝑘𝑋 (𝑐𝑘) ∈ (ℚ ∩ (((𝑌𝑘) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑘))) ∧ ∀𝑘𝑋 (𝑑𝑘) ∈ (ℚ ∩ ((𝑌𝑘)(,)((𝑌𝑘) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) → X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))
152118, 137, 151syl2anc 579 . . . . . 6 ((((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) → X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))
153117, 152jca 507 . . . . 5 ((((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋))))))))) → (𝑌X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ∧ X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸)))
154153ex 401 . . . 4 (((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) → ((∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))) → (𝑌X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ∧ X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))))
155154reximdva 3162 . . 3 ((𝜑𝑐 ∈ (ℚ ↑𝑚 𝑋)) → (∃𝑑 ∈ (ℚ ↑𝑚 𝑋)(∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))) → ∃𝑑 ∈ (ℚ ↑𝑚 𝑋)(𝑌X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ∧ X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))))
156155reximdva 3162 . 2 (𝜑 → (∃𝑐 ∈ (ℚ ↑𝑚 𝑋)∃𝑑 ∈ (ℚ ↑𝑚 𝑋)(∀𝑖𝑋 (𝑐𝑖) ∈ (ℚ ∩ (((𝑌𝑖) − (𝐸 / (2 · (√‘(♯‘𝑋)))))(,)(𝑌𝑖))) ∧ ∀𝑖𝑋 (𝑑𝑖) ∈ (ℚ ∩ ((𝑌𝑖)(,)((𝑌𝑖) + (𝐸 / (2 · (√‘(♯‘𝑋)))))))) → ∃𝑐 ∈ (ℚ ↑𝑚 𝑋)∃𝑑 ∈ (ℚ ↑𝑚 𝑋)(𝑌X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ∧ X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸))))
15793, 156mpd 15 1 (𝜑 → ∃𝑐 ∈ (ℚ ↑𝑚 𝑋)∃𝑑 ∈ (ℚ ↑𝑚 𝑋)(𝑌X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ∧ X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ⊆ (𝑌(ball‘(dist‘(ℝ^‘𝑋)))𝐸)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1652  wex 1874  wcel 2155  wne 2936  wral 3054  wrex 3055  Vcvv 3349  cin 3730  wss 3731  c0 4078   class class class wbr 4808   Fn wfn 6062  wf 6063  cfv 6067  (class class class)co 6841  𝑚 cmap 8059  Xcixp 8112  Fincfn 8159  cr 10187   + caddc 10191   · cmul 10193   < clt 10327  cle 10328  cmin 10519   / cdiv 10937  cn 11273  2c2 11326  cq 11988  +crp 12027  (,)cioo 12376  [,)cico 12378  chash 13320  csqrt 14259  distcds 16224  ballcbl 20005  ℝ^crrx 23459
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-inf2 8752  ax-cnex 10244  ax-resscn 10245  ax-1cn 10246  ax-icn 10247  ax-addcl 10248  ax-addrcl 10249  ax-mulcl 10250  ax-mulrcl 10251  ax-mulcom 10252  ax-addass 10253  ax-mulass 10254  ax-distr 10255  ax-i2m1 10256  ax-1ne0 10257  ax-1rid 10258  ax-rnegex 10259  ax-rrecex 10260  ax-cnre 10261  ax-pre-lttri 10262  ax-pre-lttrn 10263  ax-pre-ltadd 10264  ax-pre-mulgt0 10265  ax-pre-sup 10266  ax-addf 10267  ax-mulf 10268
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-uni 4594  df-int 4633  df-iun 4677  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-se 5236  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-lim 5912  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-isom 6076  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-of 7094  df-om 7263  df-1st 7365  df-2nd 7366  df-supp 7497  df-tpos 7554  df-wrecs 7609  df-recs 7671  df-rdg 7709  df-1o 7763  df-oadd 7767  df-er 7946  df-map 8061  df-ixp 8113  df-en 8160  df-dom 8161  df-sdom 8162  df-fin 8163  df-fsupp 8482  df-sup 8554  df-inf 8555  df-oi 8621  df-card 9015  df-pnf 10329  df-mnf 10330  df-xr 10331  df-ltxr 10332  df-le 10333  df-sub 10521  df-neg 10522  df-div 10938  df-nn 11274  df-2 11334  df-3 11335  df-4 11336  df-5 11337  df-6 11338  df-7 11339  df-8 11340  df-9 11341  df-n0 11538  df-z 11624  df-dec 11740  df-uz 11886  df-q 11989  df-rp 12028  df-xadd 12146  df-ioo 12380  df-ico 12382  df-fz 12533  df-fzo 12673  df-seq 13008  df-exp 13067  df-hash 13321  df-cj 14125  df-re 14126  df-im 14127  df-sqrt 14261  df-abs 14262  df-clim 14505  df-sum 14703  df-struct 16133  df-ndx 16134  df-slot 16135  df-base 16137  df-sets 16138  df-ress 16139  df-plusg 16228  df-mulr 16229  df-starv 16230  df-sca 16231  df-vsca 16232  df-ip 16233  df-tset 16234  df-ple 16235  df-ds 16237  df-unif 16238  df-hom 16239  df-cco 16240  df-0g 16369  df-gsum 16370  df-prds 16375  df-pws 16377  df-mgm 17509  df-sgrp 17551  df-mnd 17562  df-mhm 17602  df-grp 17693  df-minusg 17694  df-sbg 17695  df-subg 17856  df-ghm 17923  df-cntz 18014  df-cmn 18460  df-abl 18461  df-mgp 18756  df-ur 18768  df-ring 18815  df-cring 18816  df-oppr 18889  df-dvdsr 18907  df-unit 18908  df-invr 18938  df-dvr 18949  df-rnghom 18983  df-drng 19017  df-field 19018  df-subrg 19046  df-staf 19113  df-srng 19114  df-lmod 19133  df-lss 19201  df-sra 19445  df-rgmod 19446  df-psmet 20010  df-xmet 20011  df-met 20012  df-bl 20013  df-cnfld 20019  df-refld 20224  df-dsmm 20351  df-frlm 20366  df-nm 22665  df-tng 22667  df-tcph 23246  df-rrx 23461
This theorem is referenced by:  hoiqssbl  41411
  Copyright terms: Public domain W3C validator