# Metamath Proof Explorer

## Theorem metrest

Description: Two alternate formulations of a subspace topology of a metric space topology. (Contributed by Jeff Hankins, 19-Aug-2009) (Proof shortened by Mario Carneiro, 5-Jan-2014)

Ref Expression
Hypotheses metrest.1 ${⊢}{D}={{C}↾}_{\left({Y}×{Y}\right)}$
metrest.3 ${⊢}{J}=\mathrm{MetOpen}\left({C}\right)$
metrest.4 ${⊢}{K}=\mathrm{MetOpen}\left({D}\right)$
Assertion metrest ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to {J}{↾}_{𝑡}{Y}={K}$

### Proof

Step Hyp Ref Expression
1 metrest.1 ${⊢}{D}={{C}↾}_{\left({Y}×{Y}\right)}$
2 metrest.3 ${⊢}{J}=\mathrm{MetOpen}\left({C}\right)$
3 metrest.4 ${⊢}{K}=\mathrm{MetOpen}\left({D}\right)$
4 inss1 ${⊢}{u}\cap {Y}\subseteq {u}$
5 2 elmopn2 ${⊢}{C}\in \mathrm{\infty Met}\left({X}\right)\to \left({u}\in {J}↔\left({u}\subseteq {X}\wedge \forall {y}\in {u}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({C}\right){r}\subseteq {u}\right)\right)$
6 5 simplbda ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {u}\in {J}\right)\to \forall {y}\in {u}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({C}\right){r}\subseteq {u}$
7 6 adantlr ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {u}\in {J}\right)\to \forall {y}\in {u}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({C}\right){r}\subseteq {u}$
8 ssralv ${⊢}{u}\cap {Y}\subseteq {u}\to \left(\forall {y}\in {u}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({C}\right){r}\subseteq {u}\to \forall {y}\in \left({u}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({C}\right){r}\subseteq {u}\right)$
9 4 7 8 mpsyl ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {u}\in {J}\right)\to \forall {y}\in \left({u}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({C}\right){r}\subseteq {u}$
10 ssrin ${⊢}{y}\mathrm{ball}\left({C}\right){r}\subseteq {u}\to \left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {u}\cap {Y}$
11 10 reximi ${⊢}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({C}\right){r}\subseteq {u}\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {u}\cap {Y}$
12 11 ralimi ${⊢}\forall {y}\in \left({u}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({C}\right){r}\subseteq {u}\to \forall {y}\in \left({u}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {u}\cap {Y}$
13 9 12 syl ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {u}\in {J}\right)\to \forall {y}\in \left({u}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {u}\cap {Y}$
14 inss2 ${⊢}{u}\cap {Y}\subseteq {Y}$
15 13 14 jctil ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {u}\in {J}\right)\to \left({u}\cap {Y}\subseteq {Y}\wedge \forall {y}\in \left({u}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {u}\cap {Y}\right)$
16 sseq1 ${⊢}{x}={u}\cap {Y}\to \left({x}\subseteq {Y}↔{u}\cap {Y}\subseteq {Y}\right)$
17 sseq2 ${⊢}{x}={u}\cap {Y}\to \left(\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}↔\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {u}\cap {Y}\right)$
18 17 rexbidv ${⊢}{x}={u}\cap {Y}\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}↔\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {u}\cap {Y}\right)$
19 18 raleqbi1dv ${⊢}{x}={u}\cap {Y}\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}↔\forall {y}\in \left({u}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {u}\cap {Y}\right)$
20 16 19 anbi12d ${⊢}{x}={u}\cap {Y}\to \left(\left({x}\subseteq {Y}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)↔\left({u}\cap {Y}\subseteq {Y}\wedge \forall {y}\in \left({u}\cap {Y}\right)\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {u}\cap {Y}\right)\right)$
21 15 20 syl5ibrcom ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {u}\in {J}\right)\to \left({x}={u}\cap {Y}\to \left({x}\subseteq {Y}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)\right)$
22 21 rexlimdva ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to \left(\exists {u}\in {J}\phantom{\rule{.4em}{0ex}}{x}={u}\cap {Y}\to \left({x}\subseteq {Y}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)\right)$
23 2 mopntop ${⊢}{C}\in \mathrm{\infty Met}\left({X}\right)\to {J}\in \mathrm{Top}$
24 23 ad2antrr ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({x}\subseteq {Y}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)\right)\to {J}\in \mathrm{Top}$
25 ssel2 ${⊢}\left({x}\subseteq {Y}\wedge {y}\in {x}\right)\to {y}\in {Y}$
26 ssel2 ${⊢}\left({Y}\subseteq {X}\wedge {y}\in {Y}\right)\to {y}\in {X}$
27 rpxr ${⊢}{r}\in {ℝ}^{+}\to {r}\in {ℝ}^{*}$
28 2 blopn ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\to {y}\mathrm{ball}\left({C}\right){r}\in {J}$
29 eleq1a ${⊢}{y}\mathrm{ball}\left({C}\right){r}\in {J}\to \left({z}={y}\mathrm{ball}\left({C}\right){r}\to {z}\in {J}\right)$
30 28 29 syl ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\wedge {r}\in {ℝ}^{*}\right)\to \left({z}={y}\mathrm{ball}\left({C}\right){r}\to {z}\in {J}\right)$
31 30 3expa ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge {r}\in {ℝ}^{*}\right)\to \left({z}={y}\mathrm{ball}\left({C}\right){r}\to {z}\in {J}\right)$
32 27 31 sylan2 ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\right)\wedge {r}\in {ℝ}^{+}\right)\to \left({z}={y}\mathrm{ball}\left({C}\right){r}\to {z}\in {J}\right)$
33 32 rexlimdva ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in {X}\right)\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\to {z}\in {J}\right)$
34 26 33 sylan2 ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({Y}\subseteq {X}\wedge {y}\in {Y}\right)\right)\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\to {z}\in {J}\right)$
35 34 anassrs ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {y}\in {Y}\right)\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\to {z}\in {J}\right)$
36 25 35 sylan2 ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({x}\subseteq {Y}\wedge {y}\in {x}\right)\right)\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\to {z}\in {J}\right)$
37 36 anassrs ${⊢}\left(\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {x}\subseteq {Y}\right)\wedge {y}\in {x}\right)\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\to {z}\in {J}\right)$
38 37 rexlimdva ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {x}\subseteq {Y}\right)\to \left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\to {z}\in {J}\right)$
39 38 adantrd ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {x}\subseteq {Y}\right)\to \left(\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge {z}\cap {Y}\subseteq {x}\right)\to {z}\in {J}\right)$
40 39 adantrr ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({x}\subseteq {Y}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)\right)\to \left(\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge {z}\cap {Y}\subseteq {x}\right)\to {z}\in {J}\right)$
41 40 abssdv ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({x}\subseteq {Y}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)\right)\to \left\{{z}|\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge {z}\cap {Y}\subseteq {x}\right)\right\}\subseteq {J}$
42 uniopn ${⊢}\left({J}\in \mathrm{Top}\wedge \left\{{z}|\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge {z}\cap {Y}\subseteq {x}\right)\right\}\subseteq {J}\right)\to \bigcup \left\{{z}|\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge {z}\cap {Y}\subseteq {x}\right)\right\}\in {J}$
43 24 41 42 syl2anc ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({x}\subseteq {Y}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)\right)\to \bigcup \left\{{z}|\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge {z}\cap {Y}\subseteq {x}\right)\right\}\in {J}$
44 oveq1 ${⊢}{y}={u}\to {y}\mathrm{ball}\left({C}\right){r}={u}\mathrm{ball}\left({C}\right){r}$
45 44 ineq1d ${⊢}{y}={u}\to \left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}=\left({u}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}$
46 45 sseq1d ${⊢}{y}={u}\to \left(\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}↔\left({u}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)$
47 46 rexbidv ${⊢}{y}={u}\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}↔\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({u}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)$
48 47 rspccv ${⊢}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\to \left({u}\in {x}\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({u}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)$
49 48 ad2antll ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({x}\subseteq {Y}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)\right)\to \left({u}\in {x}\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({u}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)$
50 ssel ${⊢}{x}\subseteq {Y}\to \left({u}\in {x}\to {u}\in {Y}\right)$
51 ssel ${⊢}{Y}\subseteq {X}\to \left({u}\in {Y}\to {u}\in {X}\right)$
52 blcntr ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {u}\in {X}\wedge {r}\in {ℝ}^{+}\right)\to {u}\in \left({u}\mathrm{ball}\left({C}\right){r}\right)$
53 52 a1d ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {u}\in {X}\wedge {r}\in {ℝ}^{+}\right)\to \left(\left({u}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\to {u}\in \left({u}\mathrm{ball}\left({C}\right){r}\right)\right)$
54 53 ancld ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {u}\in {X}\wedge {r}\in {ℝ}^{+}\right)\to \left(\left({u}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\to \left(\left({u}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({u}\mathrm{ball}\left({C}\right){r}\right)\right)\right)$
55 54 3expa ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {u}\in {X}\right)\wedge {r}\in {ℝ}^{+}\right)\to \left(\left({u}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\to \left(\left({u}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({u}\mathrm{ball}\left({C}\right){r}\right)\right)\right)$
56 55 reximdva ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {u}\in {X}\right)\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({u}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left(\left({u}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({u}\mathrm{ball}\left({C}\right){r}\right)\right)\right)$
57 56 ex ${⊢}{C}\in \mathrm{\infty Met}\left({X}\right)\to \left({u}\in {X}\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({u}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left(\left({u}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({u}\mathrm{ball}\left({C}\right){r}\right)\right)\right)\right)$
58 51 57 sylan9r ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to \left({u}\in {Y}\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({u}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left(\left({u}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({u}\mathrm{ball}\left({C}\right){r}\right)\right)\right)\right)$
59 50 58 sylan9r ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {x}\subseteq {Y}\right)\to \left({u}\in {x}\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({u}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left(\left({u}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({u}\mathrm{ball}\left({C}\right){r}\right)\right)\right)\right)$
60 59 adantrr ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({x}\subseteq {Y}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)\right)\to \left({u}\in {x}\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({u}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left(\left({u}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({u}\mathrm{ball}\left({C}\right){r}\right)\right)\right)\right)$
61 49 60 mpdd ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({x}\subseteq {Y}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)\right)\to \left({u}\in {x}\to \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left(\left({u}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({u}\mathrm{ball}\left({C}\right){r}\right)\right)\right)$
62 44 eleq2d ${⊢}{y}={u}\to \left({u}\in \left({y}\mathrm{ball}\left({C}\right){r}\right)↔{u}\in \left({u}\mathrm{ball}\left({C}\right){r}\right)\right)$
63 46 62 anbi12d ${⊢}{y}={u}\to \left(\left(\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({y}\mathrm{ball}\left({C}\right){r}\right)\right)↔\left(\left({u}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({u}\mathrm{ball}\left({C}\right){r}\right)\right)\right)$
64 63 rexbidv ${⊢}{y}={u}\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left(\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({y}\mathrm{ball}\left({C}\right){r}\right)\right)↔\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left(\left({u}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({u}\mathrm{ball}\left({C}\right){r}\right)\right)\right)$
65 64 rspcev ${⊢}\left({u}\in {x}\wedge \exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left(\left({u}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({u}\mathrm{ball}\left({C}\right){r}\right)\right)\right)\to \exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left(\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({y}\mathrm{ball}\left({C}\right){r}\right)\right)$
66 65 ex ${⊢}{u}\in {x}\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left(\left({u}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({u}\mathrm{ball}\left({C}\right){r}\right)\right)\to \exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left(\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({y}\mathrm{ball}\left({C}\right){r}\right)\right)\right)$
67 61 66 sylcom ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({x}\subseteq {Y}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)\right)\to \left({u}\in {x}\to \exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left(\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({y}\mathrm{ball}\left({C}\right){r}\right)\right)\right)$
68 simprl ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({x}\subseteq {Y}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)\right)\to {x}\subseteq {Y}$
69 68 sseld ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({x}\subseteq {Y}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)\right)\to \left({u}\in {x}\to {u}\in {Y}\right)$
70 67 69 jcad ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({x}\subseteq {Y}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)\right)\to \left({u}\in {x}\to \left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left(\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({y}\mathrm{ball}\left({C}\right){r}\right)\right)\wedge {u}\in {Y}\right)\right)$
71 elin ${⊢}{u}\in \left(\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\right)↔\left({u}\in \left({y}\mathrm{ball}\left({C}\right){r}\right)\wedge {u}\in {Y}\right)$
72 ssel2 ${⊢}\left(\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left(\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\right)\right)\to {u}\in {x}$
73 71 72 sylan2br ${⊢}\left(\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge \left({u}\in \left({y}\mathrm{ball}\left({C}\right){r}\right)\wedge {u}\in {Y}\right)\right)\to {u}\in {x}$
74 73 expr ${⊢}\left(\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({y}\mathrm{ball}\left({C}\right){r}\right)\right)\to \left({u}\in {Y}\to {u}\in {x}\right)$
75 74 rexlimivw ${⊢}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left(\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({y}\mathrm{ball}\left({C}\right){r}\right)\right)\to \left({u}\in {Y}\to {u}\in {x}\right)$
76 75 rexlimivw ${⊢}\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left(\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({y}\mathrm{ball}\left({C}\right){r}\right)\right)\to \left({u}\in {Y}\to {u}\in {x}\right)$
77 76 imp ${⊢}\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left(\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({y}\mathrm{ball}\left({C}\right){r}\right)\right)\wedge {u}\in {Y}\right)\to {u}\in {x}$
78 70 77 impbid1 ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({x}\subseteq {Y}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)\right)\to \left({u}\in {x}↔\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left(\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({y}\mathrm{ball}\left({C}\right){r}\right)\right)\wedge {u}\in {Y}\right)\right)$
79 elin ${⊢}{u}\in \left(\bigcup \left\{{z}|\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge {z}\cap {Y}\subseteq {x}\right)\right\}\cap {Y}\right)↔\left({u}\in \bigcup \left\{{z}|\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge {z}\cap {Y}\subseteq {x}\right)\right\}\wedge {u}\in {Y}\right)$
80 eluniab ${⊢}{u}\in \bigcup \left\{{z}|\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge {z}\cap {Y}\subseteq {x}\right)\right\}↔\exists {z}\phantom{\rule{.4em}{0ex}}\left({u}\in {z}\wedge \left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge {z}\cap {Y}\subseteq {x}\right)\right)$
81 ancom ${⊢}\left({u}\in {z}\wedge \left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge {z}\cap {Y}\subseteq {x}\right)\right)↔\left(\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge {z}\cap {Y}\subseteq {x}\right)\wedge {u}\in {z}\right)$
82 anass ${⊢}\left(\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge {z}\cap {Y}\subseteq {x}\right)\wedge {u}\in {z}\right)↔\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge \left({z}\cap {Y}\subseteq {x}\wedge {u}\in {z}\right)\right)$
83 r19.41v ${⊢}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({z}={y}\mathrm{ball}\left({C}\right){r}\wedge \left({z}\cap {Y}\subseteq {x}\wedge {u}\in {z}\right)\right)↔\left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge \left({z}\cap {Y}\subseteq {x}\wedge {u}\in {z}\right)\right)$
84 83 rexbii ${⊢}\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({z}={y}\mathrm{ball}\left({C}\right){r}\wedge \left({z}\cap {Y}\subseteq {x}\wedge {u}\in {z}\right)\right)↔\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge \left({z}\cap {Y}\subseteq {x}\wedge {u}\in {z}\right)\right)$
85 r19.41v ${⊢}\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge \left({z}\cap {Y}\subseteq {x}\wedge {u}\in {z}\right)\right)↔\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge \left({z}\cap {Y}\subseteq {x}\wedge {u}\in {z}\right)\right)$
86 84 85 bitr2i ${⊢}\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge \left({z}\cap {Y}\subseteq {x}\wedge {u}\in {z}\right)\right)↔\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({z}={y}\mathrm{ball}\left({C}\right){r}\wedge \left({z}\cap {Y}\subseteq {x}\wedge {u}\in {z}\right)\right)$
87 81 82 86 3bitri ${⊢}\left({u}\in {z}\wedge \left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge {z}\cap {Y}\subseteq {x}\right)\right)↔\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({z}={y}\mathrm{ball}\left({C}\right){r}\wedge \left({z}\cap {Y}\subseteq {x}\wedge {u}\in {z}\right)\right)$
88 87 exbii ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\left({u}\in {z}\wedge \left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge {z}\cap {Y}\subseteq {x}\right)\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({z}={y}\mathrm{ball}\left({C}\right){r}\wedge \left({z}\cap {Y}\subseteq {x}\wedge {u}\in {z}\right)\right)$
89 ovex ${⊢}{y}\mathrm{ball}\left({C}\right){r}\in \mathrm{V}$
90 ineq1 ${⊢}{z}={y}\mathrm{ball}\left({C}\right){r}\to {z}\cap {Y}=\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}$
91 90 sseq1d ${⊢}{z}={y}\mathrm{ball}\left({C}\right){r}\to \left({z}\cap {Y}\subseteq {x}↔\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)$
92 eleq2 ${⊢}{z}={y}\mathrm{ball}\left({C}\right){r}\to \left({u}\in {z}↔{u}\in \left({y}\mathrm{ball}\left({C}\right){r}\right)\right)$
93 91 92 anbi12d ${⊢}{z}={y}\mathrm{ball}\left({C}\right){r}\to \left(\left({z}\cap {Y}\subseteq {x}\wedge {u}\in {z}\right)↔\left(\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({y}\mathrm{ball}\left({C}\right){r}\right)\right)\right)$
94 89 93 ceqsexv ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}\mathrm{ball}\left({C}\right){r}\wedge \left({z}\cap {Y}\subseteq {x}\wedge {u}\in {z}\right)\right)↔\left(\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({y}\mathrm{ball}\left({C}\right){r}\right)\right)$
95 94 rexbii ${⊢}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}\mathrm{ball}\left({C}\right){r}\wedge \left({z}\cap {Y}\subseteq {x}\wedge {u}\in {z}\right)\right)↔\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left(\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({y}\mathrm{ball}\left({C}\right){r}\right)\right)$
96 rexcom4 ${⊢}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}\mathrm{ball}\left({C}\right){r}\wedge \left({z}\cap {Y}\subseteq {x}\wedge {u}\in {z}\right)\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({z}={y}\mathrm{ball}\left({C}\right){r}\wedge \left({z}\cap {Y}\subseteq {x}\wedge {u}\in {z}\right)\right)$
97 95 96 bitr3i ${⊢}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left(\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({y}\mathrm{ball}\left({C}\right){r}\right)\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({z}={y}\mathrm{ball}\left({C}\right){r}\wedge \left({z}\cap {Y}\subseteq {x}\wedge {u}\in {z}\right)\right)$
98 97 rexbii ${⊢}\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left(\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({y}\mathrm{ball}\left({C}\right){r}\right)\right)↔\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({z}={y}\mathrm{ball}\left({C}\right){r}\wedge \left({z}\cap {Y}\subseteq {x}\wedge {u}\in {z}\right)\right)$
99 rexcom4 ${⊢}\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({z}={y}\mathrm{ball}\left({C}\right){r}\wedge \left({z}\cap {Y}\subseteq {x}\wedge {u}\in {z}\right)\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({z}={y}\mathrm{ball}\left({C}\right){r}\wedge \left({z}\cap {Y}\subseteq {x}\wedge {u}\in {z}\right)\right)$
100 98 99 bitr2i ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({z}={y}\mathrm{ball}\left({C}\right){r}\wedge \left({z}\cap {Y}\subseteq {x}\wedge {u}\in {z}\right)\right)↔\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left(\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({y}\mathrm{ball}\left({C}\right){r}\right)\right)$
101 80 88 100 3bitri ${⊢}{u}\in \bigcup \left\{{z}|\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge {z}\cap {Y}\subseteq {x}\right)\right\}↔\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left(\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({y}\mathrm{ball}\left({C}\right){r}\right)\right)$
102 101 anbi1i ${⊢}\left({u}\in \bigcup \left\{{z}|\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge {z}\cap {Y}\subseteq {x}\right)\right\}\wedge {u}\in {Y}\right)↔\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left(\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({y}\mathrm{ball}\left({C}\right){r}\right)\right)\wedge {u}\in {Y}\right)$
103 79 102 bitr2i ${⊢}\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left(\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\wedge {u}\in \left({y}\mathrm{ball}\left({C}\right){r}\right)\right)\wedge {u}\in {Y}\right)↔{u}\in \left(\bigcup \left\{{z}|\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge {z}\cap {Y}\subseteq {x}\right)\right\}\cap {Y}\right)$
104 78 103 syl6bb ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({x}\subseteq {Y}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)\right)\to \left({u}\in {x}↔{u}\in \left(\bigcup \left\{{z}|\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge {z}\cap {Y}\subseteq {x}\right)\right\}\cap {Y}\right)\right)$
105 104 eqrdv ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({x}\subseteq {Y}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)\right)\to {x}=\bigcup \left\{{z}|\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge {z}\cap {Y}\subseteq {x}\right)\right\}\cap {Y}$
106 ineq1 ${⊢}{u}=\bigcup \left\{{z}|\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge {z}\cap {Y}\subseteq {x}\right)\right\}\to {u}\cap {Y}=\bigcup \left\{{z}|\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge {z}\cap {Y}\subseteq {x}\right)\right\}\cap {Y}$
107 106 rspceeqv ${⊢}\left(\bigcup \left\{{z}|\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge {z}\cap {Y}\subseteq {x}\right)\right\}\in {J}\wedge {x}=\bigcup \left\{{z}|\left(\exists {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{z}={y}\mathrm{ball}\left({C}\right){r}\wedge {z}\cap {Y}\subseteq {x}\right)\right\}\cap {Y}\right)\to \exists {u}\in {J}\phantom{\rule{.4em}{0ex}}{x}={u}\cap {Y}$
108 43 105 107 syl2anc ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({x}\subseteq {Y}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)\right)\to \exists {u}\in {J}\phantom{\rule{.4em}{0ex}}{x}={u}\cap {Y}$
109 108 ex ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to \left(\left({x}\subseteq {Y}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)\to \exists {u}\in {J}\phantom{\rule{.4em}{0ex}}{x}={u}\cap {Y}\right)$
110 22 109 impbid ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to \left(\exists {u}\in {J}\phantom{\rule{.4em}{0ex}}{x}={u}\cap {Y}↔\left({x}\subseteq {Y}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)\right)$
111 simpr ${⊢}\left({Y}\subseteq {X}\wedge {y}\in {Y}\right)\to {y}\in {Y}$
112 26 111 elind ${⊢}\left({Y}\subseteq {X}\wedge {y}\in {Y}\right)\to {y}\in \left({X}\cap {Y}\right)$
113 1 blres ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in \left({X}\cap {Y}\right)\wedge {r}\in {ℝ}^{*}\right)\to {y}\mathrm{ball}\left({D}\right){r}=\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}$
114 113 sseq1d ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in \left({X}\cap {Y}\right)\wedge {r}\in {ℝ}^{*}\right)\to \left({y}\mathrm{ball}\left({D}\right){r}\subseteq {x}↔\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)$
115 114 3expa ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in \left({X}\cap {Y}\right)\right)\wedge {r}\in {ℝ}^{*}\right)\to \left({y}\mathrm{ball}\left({D}\right){r}\subseteq {x}↔\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)$
116 27 115 sylan2 ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in \left({X}\cap {Y}\right)\right)\wedge {r}\in {ℝ}^{+}\right)\to \left({y}\mathrm{ball}\left({D}\right){r}\subseteq {x}↔\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)$
117 116 rexbidva ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {y}\in \left({X}\cap {Y}\right)\right)\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({D}\right){r}\subseteq {x}↔\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)$
118 112 117 sylan2 ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({Y}\subseteq {X}\wedge {y}\in {Y}\right)\right)\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({D}\right){r}\subseteq {x}↔\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)$
119 118 anassrs ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {y}\in {Y}\right)\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({D}\right){r}\subseteq {x}↔\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)$
120 25 119 sylan2 ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge \left({x}\subseteq {Y}\wedge {y}\in {x}\right)\right)\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({D}\right){r}\subseteq {x}↔\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)$
121 120 anassrs ${⊢}\left(\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {x}\subseteq {Y}\right)\wedge {y}\in {x}\right)\to \left(\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({D}\right){r}\subseteq {x}↔\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)$
122 121 ralbidva ${⊢}\left(\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\wedge {x}\subseteq {Y}\right)\to \left(\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({D}\right){r}\subseteq {x}↔\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)$
123 122 pm5.32da ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to \left(\left({x}\subseteq {Y}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({D}\right){r}\subseteq {x}\right)↔\left({x}\subseteq {Y}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\left({y}\mathrm{ball}\left({C}\right){r}\right)\cap {Y}\subseteq {x}\right)\right)$
124 110 123 bitr4d ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to \left(\exists {u}\in {J}\phantom{\rule{.4em}{0ex}}{x}={u}\cap {Y}↔\left({x}\subseteq {Y}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({D}\right){r}\subseteq {x}\right)\right)$
125 id ${⊢}{Y}\subseteq {X}\to {Y}\subseteq {X}$
126 2 mopnm ${⊢}{C}\in \mathrm{\infty Met}\left({X}\right)\to {X}\in {J}$
127 ssexg ${⊢}\left({Y}\subseteq {X}\wedge {X}\in {J}\right)\to {Y}\in \mathrm{V}$
128 125 126 127 syl2anr ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to {Y}\in \mathrm{V}$
129 elrest ${⊢}\left({J}\in \mathrm{Top}\wedge {Y}\in \mathrm{V}\right)\to \left({x}\in \left({J}{↾}_{𝑡}{Y}\right)↔\exists {u}\in {J}\phantom{\rule{.4em}{0ex}}{x}={u}\cap {Y}\right)$
130 23 128 129 syl2an2r ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to \left({x}\in \left({J}{↾}_{𝑡}{Y}\right)↔\exists {u}\in {J}\phantom{\rule{.4em}{0ex}}{x}={u}\cap {Y}\right)$
131 xmetres2 ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to {{C}↾}_{\left({Y}×{Y}\right)}\in \mathrm{\infty Met}\left({Y}\right)$
132 1 131 eqeltrid ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to {D}\in \mathrm{\infty Met}\left({Y}\right)$
133 3 elmopn2 ${⊢}{D}\in \mathrm{\infty Met}\left({Y}\right)\to \left({x}\in {K}↔\left({x}\subseteq {Y}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({D}\right){r}\subseteq {x}\right)\right)$
134 132 133 syl ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to \left({x}\in {K}↔\left({x}\subseteq {Y}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {r}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}\mathrm{ball}\left({D}\right){r}\subseteq {x}\right)\right)$
135 124 130 134 3bitr4d ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to \left({x}\in \left({J}{↾}_{𝑡}{Y}\right)↔{x}\in {K}\right)$
136 135 eqrdv ${⊢}\left({C}\in \mathrm{\infty Met}\left({X}\right)\wedge {Y}\subseteq {X}\right)\to {J}{↾}_{𝑡}{Y}={K}$