| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | inss1 4236 | . . . . . . . . . 10
⊢ (𝑢 ∩ 𝑌) ⊆ 𝑢 | 
| 2 |  | metrest.3 | . . . . . . . . . . . . 13
⊢ 𝐽 = (MetOpen‘𝐶) | 
| 3 | 2 | elmopn2 24456 | . . . . . . . . . . . 12
⊢ (𝐶 ∈ (∞Met‘𝑋) → (𝑢 ∈ 𝐽 ↔ (𝑢 ⊆ 𝑋 ∧ ∀𝑦 ∈ 𝑢 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢))) | 
| 4 | 3 | simplbda 499 | . . . . . . . . . . 11
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝐽) → ∀𝑦 ∈ 𝑢 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢) | 
| 5 | 4 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑢 ∈ 𝐽) → ∀𝑦 ∈ 𝑢 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢) | 
| 6 |  | ssralv 4051 | . . . . . . . . . 10
⊢ ((𝑢 ∩ 𝑌) ⊆ 𝑢 → (∀𝑦 ∈ 𝑢 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢 → ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢)) | 
| 7 | 1, 5, 6 | mpsyl 68 | . . . . . . . . 9
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑢 ∈ 𝐽) → ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢) | 
| 8 |  | ssrin 4241 | . . . . . . . . . . 11
⊢ ((𝑦(ball‘𝐶)𝑟) ⊆ 𝑢 → ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌)) | 
| 9 | 8 | reximi 3083 | . . . . . . . . . 10
⊢
(∃𝑟 ∈
ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢 → ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌)) | 
| 10 | 9 | ralimi 3082 | . . . . . . . . 9
⊢
(∀𝑦 ∈
(𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢 → ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌)) | 
| 11 | 7, 10 | syl 17 | . . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑢 ∈ 𝐽) → ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌)) | 
| 12 |  | inss2 4237 | . . . . . . . 8
⊢ (𝑢 ∩ 𝑌) ⊆ 𝑌 | 
| 13 | 11, 12 | jctil 519 | . . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑢 ∈ 𝐽) → ((𝑢 ∩ 𝑌) ⊆ 𝑌 ∧ ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌))) | 
| 14 |  | sseq1 4008 | . . . . . . . 8
⊢ (𝑥 = (𝑢 ∩ 𝑌) → (𝑥 ⊆ 𝑌 ↔ (𝑢 ∩ 𝑌) ⊆ 𝑌)) | 
| 15 |  | sseq2 4009 | . . . . . . . . . 10
⊢ (𝑥 = (𝑢 ∩ 𝑌) → (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌))) | 
| 16 | 15 | rexbidv 3178 | . . . . . . . . 9
⊢ (𝑥 = (𝑢 ∩ 𝑌) → (∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌))) | 
| 17 | 16 | raleqbi1dv 3337 | . . . . . . . 8
⊢ (𝑥 = (𝑢 ∩ 𝑌) → (∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌))) | 
| 18 | 14, 17 | anbi12d 632 | . . . . . . 7
⊢ (𝑥 = (𝑢 ∩ 𝑌) → ((𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥) ↔ ((𝑢 ∩ 𝑌) ⊆ 𝑌 ∧ ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌)))) | 
| 19 | 13, 18 | syl5ibrcom 247 | . . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑢 ∈ 𝐽) → (𝑥 = (𝑢 ∩ 𝑌) → (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))) | 
| 20 | 19 | rexlimdva 3154 | . . . . 5
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌) → (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))) | 
| 21 | 2 | mopntop 24451 | . . . . . . . . 9
⊢ (𝐶 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top) | 
| 22 | 21 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → 𝐽 ∈ Top) | 
| 23 |  | ssel2 3977 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ⊆ 𝑌 ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑌) | 
| 24 |  | ssel2 3977 | . . . . . . . . . . . . . . . 16
⊢ ((𝑌 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋) | 
| 25 |  | rpxr 13045 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) | 
| 26 | 2 | blopn 24514 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ*) → (𝑦(ball‘𝐶)𝑟) ∈ 𝐽) | 
| 27 |  | eleq1a 2835 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦(ball‘𝐶)𝑟) ∈ 𝐽 → (𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽)) | 
| 28 | 26, 27 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ*) → (𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽)) | 
| 29 | 28 | 3expa 1118 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ*) → (𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽)) | 
| 30 | 25, 29 | sylan2 593 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽)) | 
| 31 | 30 | rexlimdva 3154 | . . . . . . . . . . . . . . . 16
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋) → (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽)) | 
| 32 | 24, 31 | sylan2 593 | . . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽)) | 
| 33 | 32 | anassrs 467 | . . . . . . . . . . . . . 14
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑦 ∈ 𝑌) → (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽)) | 
| 34 | 23, 33 | sylan2 593 | . . . . . . . . . . . . 13
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ 𝑦 ∈ 𝑥)) → (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽)) | 
| 35 | 34 | anassrs 467 | . . . . . . . . . . . 12
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) → (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽)) | 
| 36 | 35 | rexlimdva 3154 | . . . . . . . . . . 11
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑌) → (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽)) | 
| 37 | 36 | adantrd 491 | . . . . . . . . . 10
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑌) → ((∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥) → 𝑧 ∈ 𝐽)) | 
| 38 | 37 | adantrr 717 | . . . . . . . . 9
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → ((∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥) → 𝑧 ∈ 𝐽)) | 
| 39 | 38 | abssdv 4067 | . . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ⊆ 𝐽) | 
| 40 |  | uniopn 22904 | . . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ⊆ 𝐽) → ∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∈ 𝐽) | 
| 41 | 22, 39, 40 | syl2anc 584 | . . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → ∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∈ 𝐽) | 
| 42 |  | oveq1 7439 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑢 → (𝑦(ball‘𝐶)𝑟) = (𝑢(ball‘𝐶)𝑟)) | 
| 43 | 42 | ineq1d 4218 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑢 → ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) = ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌)) | 
| 44 | 43 | sseq1d 4014 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑢 → (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) | 
| 45 | 44 | rexbidv 3178 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑢 → (∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) | 
| 46 | 45 | rspccv 3618 | . . . . . . . . . . . . . 14
⊢
(∀𝑦 ∈
𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → (𝑢 ∈ 𝑥 → ∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) | 
| 47 | 46 | ad2antll 729 | . . . . . . . . . . . . 13
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 → ∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) | 
| 48 |  | ssel 3976 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ⊆ 𝑌 → (𝑢 ∈ 𝑥 → 𝑢 ∈ 𝑌)) | 
| 49 |  | ssel 3976 | . . . . . . . . . . . . . . . 16
⊢ (𝑌 ⊆ 𝑋 → (𝑢 ∈ 𝑌 → 𝑢 ∈ 𝑋)) | 
| 50 |  | blcntr 24424 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) → 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)) | 
| 51 | 50 | a1d 25 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))) | 
| 52 | 51 | ancld 550 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))) | 
| 53 | 52 | 3expa 1118 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝑋) ∧ 𝑟 ∈ ℝ+) → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))) | 
| 54 | 53 | reximdva 3167 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝑋) → (∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))) | 
| 55 | 54 | ex 412 | . . . . . . . . . . . . . . . 16
⊢ (𝐶 ∈ (∞Met‘𝑋) → (𝑢 ∈ 𝑋 → (∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))) | 
| 56 | 49, 55 | sylan9r 508 | . . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑢 ∈ 𝑌 → (∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))) | 
| 57 | 48, 56 | sylan9r 508 | . . . . . . . . . . . . . 14
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑌) → (𝑢 ∈ 𝑥 → (∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))) | 
| 58 | 57 | adantrr 717 | . . . . . . . . . . . . 13
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 → (∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))) | 
| 59 | 47, 58 | mpdd 43 | . . . . . . . . . . . 12
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 → ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))) | 
| 60 | 42 | eleq2d 2826 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑢 → (𝑢 ∈ (𝑦(ball‘𝐶)𝑟) ↔ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))) | 
| 61 | 44, 60 | anbi12d 632 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑢 → ((((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ↔ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))) | 
| 62 | 61 | rexbidv 3178 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑢 → (∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ↔ ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))) | 
| 63 | 62 | rspcev 3621 | . . . . . . . . . . . . 13
⊢ ((𝑢 ∈ 𝑥 ∧ ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))) → ∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟))) | 
| 64 | 63 | ex 412 | . . . . . . . . . . . 12
⊢ (𝑢 ∈ 𝑥 → (∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)) → ∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)))) | 
| 65 | 59, 64 | sylcom 30 | . . . . . . . . . . 11
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 → ∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)))) | 
| 66 |  | simprl 770 | . . . . . . . . . . . 12
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → 𝑥 ⊆ 𝑌) | 
| 67 | 66 | sseld 3981 | . . . . . . . . . . 11
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 → 𝑢 ∈ 𝑌)) | 
| 68 | 65, 67 | jcad 512 | . . . . . . . . . 10
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 → (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢 ∈ 𝑌))) | 
| 69 |  | elin 3966 | . . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ↔ (𝑢 ∈ (𝑦(ball‘𝐶)𝑟) ∧ 𝑢 ∈ 𝑌)) | 
| 70 |  | ssel2 3977 | . . . . . . . . . . . . . . 15
⊢ ((((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌)) → 𝑢 ∈ 𝑥) | 
| 71 | 69, 70 | sylan2br 595 | . . . . . . . . . . . . . 14
⊢ ((((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ (𝑢 ∈ (𝑦(ball‘𝐶)𝑟) ∧ 𝑢 ∈ 𝑌)) → 𝑢 ∈ 𝑥) | 
| 72 | 71 | expr 456 | . . . . . . . . . . . . 13
⊢ ((((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) → (𝑢 ∈ 𝑌 → 𝑢 ∈ 𝑥)) | 
| 73 | 72 | rexlimivw 3150 | . . . . . . . . . . . 12
⊢
(∃𝑟 ∈
ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) → (𝑢 ∈ 𝑌 → 𝑢 ∈ 𝑥)) | 
| 74 | 73 | rexlimivw 3150 | . . . . . . . . . . 11
⊢
(∃𝑦 ∈
𝑥 ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) → (𝑢 ∈ 𝑌 → 𝑢 ∈ 𝑥)) | 
| 75 | 74 | imp 406 | . . . . . . . . . 10
⊢
((∃𝑦 ∈
𝑥 ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢 ∈ 𝑌) → 𝑢 ∈ 𝑥) | 
| 76 | 68, 75 | impbid1 225 | . . . . . . . . 9
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 ↔ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢 ∈ 𝑌))) | 
| 77 |  | elin 3966 | . . . . . . . . . 10
⊢ (𝑢 ∈ (∪ {𝑧
∣ (∃𝑦 ∈
𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∩ 𝑌) ↔ (𝑢 ∈ ∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∧ 𝑢 ∈ 𝑌)) | 
| 78 |  | eluniab 4920 | . . . . . . . . . . . 12
⊢ (𝑢 ∈ ∪ {𝑧
∣ (∃𝑦 ∈
𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ↔ ∃𝑧(𝑢 ∈ 𝑧 ∧ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥))) | 
| 79 |  | ancom 460 | . . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ 𝑧 ∧ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)) ↔ ((∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥) ∧ 𝑢 ∈ 𝑧)) | 
| 80 |  | anass 468 | . . . . . . . . . . . . . 14
⊢
(((∃𝑦 ∈
𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥) ∧ 𝑢 ∈ 𝑧) ↔ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧))) | 
| 81 |  | r19.41v 3188 | . . . . . . . . . . . . . . . 16
⊢
(∃𝑟 ∈
ℝ+ (𝑧 =
(𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧))) | 
| 82 | 81 | rexbii 3093 | . . . . . . . . . . . . . . 15
⊢
(∃𝑦 ∈
𝑥 ∃𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ ∃𝑦 ∈ 𝑥 (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧))) | 
| 83 |  | r19.41v 3188 | . . . . . . . . . . . . . . 15
⊢
(∃𝑦 ∈
𝑥 (∃𝑟 ∈ ℝ+
𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧))) | 
| 84 | 82, 83 | bitr2i 276 | . . . . . . . . . . . . . 14
⊢
((∃𝑦 ∈
𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ ∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧))) | 
| 85 | 79, 80, 84 | 3bitri 297 | . . . . . . . . . . . . 13
⊢ ((𝑢 ∈ 𝑧 ∧ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)) ↔ ∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧))) | 
| 86 | 85 | exbii 1847 | . . . . . . . . . . . 12
⊢
(∃𝑧(𝑢 ∈ 𝑧 ∧ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)) ↔ ∃𝑧∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧))) | 
| 87 |  | ovex 7465 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦(ball‘𝐶)𝑟) ∈ V | 
| 88 |  | ineq1 4212 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = (𝑦(ball‘𝐶)𝑟) → (𝑧 ∩ 𝑌) = ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌)) | 
| 89 | 88 | sseq1d 4014 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = (𝑦(ball‘𝐶)𝑟) → ((𝑧 ∩ 𝑌) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) | 
| 90 |  | eleq2 2829 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = (𝑦(ball‘𝐶)𝑟) → (𝑢 ∈ 𝑧 ↔ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟))) | 
| 91 | 89, 90 | anbi12d 632 | . . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝑦(ball‘𝐶)𝑟) → (((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧) ↔ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)))) | 
| 92 | 87, 91 | ceqsexv 3531 | . . . . . . . . . . . . . . . 16
⊢
(∃𝑧(𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟))) | 
| 93 | 92 | rexbii 3093 | . . . . . . . . . . . . . . 15
⊢
(∃𝑟 ∈
ℝ+ ∃𝑧(𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟))) | 
| 94 |  | rexcom4 3287 | . . . . . . . . . . . . . . 15
⊢
(∃𝑟 ∈
ℝ+ ∃𝑧(𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ ∃𝑧∃𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧))) | 
| 95 | 93, 94 | bitr3i 277 | . . . . . . . . . . . . . 14
⊢
(∃𝑟 ∈
ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ↔ ∃𝑧∃𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧))) | 
| 96 | 95 | rexbii 3093 | . . . . . . . . . . . . 13
⊢
(∃𝑦 ∈
𝑥 ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ↔ ∃𝑦 ∈ 𝑥 ∃𝑧∃𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧))) | 
| 97 |  | rexcom4 3287 | . . . . . . . . . . . . 13
⊢
(∃𝑦 ∈
𝑥 ∃𝑧∃𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ ∃𝑧∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧))) | 
| 98 | 96, 97 | bitr2i 276 | . . . . . . . . . . . 12
⊢
(∃𝑧∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ ∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟))) | 
| 99 | 78, 86, 98 | 3bitri 297 | . . . . . . . . . . 11
⊢ (𝑢 ∈ ∪ {𝑧
∣ (∃𝑦 ∈
𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ↔ ∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟))) | 
| 100 | 99 | anbi1i 624 | . . . . . . . . . 10
⊢ ((𝑢 ∈ ∪ {𝑧
∣ (∃𝑦 ∈
𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∧ 𝑢 ∈ 𝑌) ↔ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢 ∈ 𝑌)) | 
| 101 | 77, 100 | bitr2i 276 | . . . . . . . . 9
⊢
((∃𝑦 ∈
𝑥 ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢 ∈ 𝑌) ↔ 𝑢 ∈ (∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∩ 𝑌)) | 
| 102 | 76, 101 | bitrdi 287 | . . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 ↔ 𝑢 ∈ (∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∩ 𝑌))) | 
| 103 | 102 | eqrdv 2734 | . . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → 𝑥 = (∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∩ 𝑌)) | 
| 104 |  | ineq1 4212 | . . . . . . . 8
⊢ (𝑢 = ∪
{𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} → (𝑢 ∩ 𝑌) = (∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∩ 𝑌)) | 
| 105 | 104 | rspceeqv 3644 | . . . . . . 7
⊢ ((∪ {𝑧
∣ (∃𝑦 ∈
𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∈ 𝐽 ∧ 𝑥 = (∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∩ 𝑌)) → ∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌)) | 
| 106 | 41, 103, 105 | syl2anc 584 | . . . . . 6
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → ∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌)) | 
| 107 | 106 | ex 412 | . . . . 5
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → ((𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥) → ∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌))) | 
| 108 | 20, 107 | impbid 212 | . . . 4
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌) ↔ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))) | 
| 109 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝑌 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑌) | 
| 110 | 24, 109 | elind 4199 | . . . . . . . . . 10
⊢ ((𝑌 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ (𝑋 ∩ 𝑌)) | 
| 111 |  | metrest.1 | . . . . . . . . . . . . . . 15
⊢ 𝐷 = (𝐶 ↾ (𝑌 × 𝑌)) | 
| 112 | 111 | blres 24442 | . . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋 ∩ 𝑌) ∧ 𝑟 ∈ ℝ*) → (𝑦(ball‘𝐷)𝑟) = ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌)) | 
| 113 | 112 | sseq1d 4014 | . . . . . . . . . . . . 13
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋 ∩ 𝑌) ∧ 𝑟 ∈ ℝ*) → ((𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) | 
| 114 | 113 | 3expa 1118 | . . . . . . . . . . . 12
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋 ∩ 𝑌)) ∧ 𝑟 ∈ ℝ*) → ((𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) | 
| 115 | 25, 114 | sylan2 593 | . . . . . . . . . . 11
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋 ∩ 𝑌)) ∧ 𝑟 ∈ ℝ+) → ((𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) | 
| 116 | 115 | rexbidva 3176 | . . . . . . . . . 10
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋 ∩ 𝑌)) → (∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) | 
| 117 | 110, 116 | sylan2 593 | . . . . . . . . 9
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) | 
| 118 | 117 | anassrs 467 | . . . . . . . 8
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑦 ∈ 𝑌) → (∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) | 
| 119 | 23, 118 | sylan2 593 | . . . . . . 7
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ 𝑦 ∈ 𝑥)) → (∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) | 
| 120 | 119 | anassrs 467 | . . . . . 6
⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) → (∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) | 
| 121 | 120 | ralbidva 3175 | . . . . 5
⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑌) → (∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) | 
| 122 | 121 | pm5.32da 579 | . . . 4
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → ((𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥) ↔ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))) | 
| 123 | 108, 122 | bitr4d 282 | . . 3
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌) ↔ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥))) | 
| 124 |  | id 22 | . . . . 5
⊢ (𝑌 ⊆ 𝑋 → 𝑌 ⊆ 𝑋) | 
| 125 | 2 | mopnm 24455 | . . . . 5
⊢ (𝐶 ∈ (∞Met‘𝑋) → 𝑋 ∈ 𝐽) | 
| 126 |  | ssexg 5322 | . . . . 5
⊢ ((𝑌 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽) → 𝑌 ∈ V) | 
| 127 | 124, 125,
126 | syl2anr 597 | . . . 4
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → 𝑌 ∈ V) | 
| 128 |  | elrest 17473 | . . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑌 ∈ V) → (𝑥 ∈ (𝐽 ↾t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌))) | 
| 129 | 21, 127, 128 | syl2an2r 685 | . . 3
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑥 ∈ (𝐽 ↾t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌))) | 
| 130 |  | xmetres2 24372 | . . . . 5
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝐶 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌)) | 
| 131 | 111, 130 | eqeltrid 2844 | . . . 4
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → 𝐷 ∈ (∞Met‘𝑌)) | 
| 132 |  | metrest.4 | . . . . 5
⊢ 𝐾 = (MetOpen‘𝐷) | 
| 133 | 132 | elmopn2 24456 | . . . 4
⊢ (𝐷 ∈ (∞Met‘𝑌) → (𝑥 ∈ 𝐾 ↔ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥))) | 
| 134 | 131, 133 | syl 17 | . . 3
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑥 ∈ 𝐾 ↔ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥))) | 
| 135 | 123, 129,
134 | 3bitr4d 311 | . 2
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑥 ∈ (𝐽 ↾t 𝑌) ↔ 𝑥 ∈ 𝐾)) | 
| 136 | 135 | eqrdv 2734 | 1
⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝐽 ↾t 𝑌) = 𝐾) |