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 ⊢ 𝐷 = ( 𝐶 ↾ ( 𝑌 × 𝑌 ) )
metrest.3 ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
metrest.4 ⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
Assertion metrest ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝑌 ) = 𝐾 )

Proof

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