This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem metss

Description: Two ways of saying that metric D generates a finer topology than metric C . (Contributed by Mario Carneiro, 12-Nov-2013) (Revised by Mario Carneiro, 24-Aug-2015)

Ref Expression
Hypotheses metequiv.3 ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
metequiv.4 ⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
Assertion metss ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( 𝐽 ⊆ 𝐾 ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ) )

Proof

Step Hyp Ref Expression
1 metequiv.3 ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
2 metequiv.4 ⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
3 1 mopnval ⊢ ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 = ( topGen ‘ ran ( ball ‘ 𝐶 ) ) )
4 3 adantr ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → 𝐽 = ( topGen ‘ ran ( ball ‘ 𝐶 ) ) )
5 2 mopnval ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐾 = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) )
6 5 adantl ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → 𝐾 = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) )
7 4 6 sseq12d ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( 𝐽 ⊆ 𝐾 ↔ ( topGen ‘ ran ( ball ‘ 𝐶 ) ) ⊆ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) )
8 blbas ⊢ ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) → ran ( ball ‘ 𝐶 ) ∈ TopBases )
9 unirnbl ⊢ ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) → ∪ ran ( ball ‘ 𝐶 ) = 𝑋 )
10 9 adantr ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ∪ ran ( ball ‘ 𝐶 ) = 𝑋 )
11 unirnbl ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∪ ran ( ball ‘ 𝐷 ) = 𝑋 )
12 11 adantl ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ∪ ran ( ball ‘ 𝐷 ) = 𝑋 )
13 10 12 eqtr4d ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ∪ ran ( ball ‘ 𝐶 ) = ∪ ran ( ball ‘ 𝐷 ) )
14 tgss2 ⊢ ( ( ran ( ball ‘ 𝐶 ) ∈ TopBases ∧ ∪ ran ( ball ‘ 𝐶 ) = ∪ ran ( ball ‘ 𝐷 ) ) → ( ( topGen ‘ ran ( ball ‘ 𝐶 ) ) ⊆ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ↔ ∀ 𝑥 ∈ ∪ ran ( ball ‘ 𝐶 ) ∀ 𝑦 ∈ ran ( ball ‘ 𝐶 ) ( 𝑥 ∈ 𝑦 → ∃ 𝑧 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) )
15 8 13 14 syl2an2r ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( ( topGen ‘ ran ( ball ‘ 𝐶 ) ) ⊆ ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ↔ ∀ 𝑥 ∈ ∪ ran ( ball ‘ 𝐶 ) ∀ 𝑦 ∈ ran ( ball ‘ 𝐶 ) ( 𝑥 ∈ 𝑦 → ∃ 𝑧 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) )
16 10 raleqdv ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( ∀ 𝑥 ∈ ∪ ran ( ball ‘ 𝐶 ) ∀ 𝑦 ∈ ran ( ball ‘ 𝐶 ) ( 𝑥 ∈ 𝑦 → ∃ 𝑧 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ ran ( ball ‘ 𝐶 ) ( 𝑥 ∈ 𝑦 → ∃ 𝑧 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) )
17 blssex ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( ∃ 𝑧 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ↔ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ 𝑦 ) )
18 17 adantll ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ∃ 𝑧 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ↔ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ 𝑦 ) )
19 18 imbi2d ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑦 → ∃ 𝑧 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ↔ ( 𝑥 ∈ 𝑦 → ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ 𝑦 ) ) )
20 19 ralbidv ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑦 ∈ ran ( ball ‘ 𝐶 ) ( 𝑥 ∈ 𝑦 → ∃ 𝑧 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ran ( ball ‘ 𝐶 ) ( 𝑥 ∈ 𝑦 → ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ 𝑦 ) ) )
21 rpxr ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ* )
22 blelrn ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∈ ran ( ball ‘ 𝐶 ) )
23 21 22 syl3an3 ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) → ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∈ ran ( ball ‘ 𝐶 ) )
24 blcntr ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) → 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) )
25 eleq2 ⊢ ( 𝑦 = ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) → ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ) )
26 sseq2 ⊢ ( 𝑦 = ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) → ( ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ 𝑦 ↔ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ) )
27 26 rexbidv ⊢ ( 𝑦 = ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) → ( ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ 𝑦 ↔ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ) )
28 25 27 imbi12d ⊢ ( 𝑦 = ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) → ( ( 𝑥 ∈ 𝑦 → ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ 𝑦 ) ↔ ( 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) → ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ) ) )
29 28 rspcv ⊢ ( ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∈ ran ( ball ‘ 𝐶 ) → ( ∀ 𝑦 ∈ ran ( ball ‘ 𝐶 ) ( 𝑥 ∈ 𝑦 → ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ 𝑦 ) → ( 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) → ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ) ) )
30 29 com23 ⊢ ( ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∈ ran ( ball ‘ 𝐶 ) → ( 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) → ( ∀ 𝑦 ∈ ran ( ball ‘ 𝐶 ) ( 𝑥 ∈ 𝑦 → ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ 𝑦 ) → ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ) ) )
31 23 24 30 sylc ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) → ( ∀ 𝑦 ∈ ran ( ball ‘ 𝐶 ) ( 𝑥 ∈ 𝑦 → ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ 𝑦 ) → ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ) )
32 31 ad4ant134 ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ( ∀ 𝑦 ∈ ran ( ball ‘ 𝐶 ) ( 𝑥 ∈ 𝑦 → ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ 𝑦 ) → ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ) )
33 32 ralrimdva ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑦 ∈ ran ( ball ‘ 𝐶 ) ( 𝑥 ∈ 𝑦 → ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ 𝑦 ) → ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ) )
34 blss ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ ran ( ball ‘ 𝐶 ) ∧ 𝑥 ∈ 𝑦 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ⊆ 𝑦 )
35 34 3expb ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ ran ( ball ‘ 𝐶 ) ∧ 𝑥 ∈ 𝑦 ) ) → ∃ 𝑟 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ⊆ 𝑦 )
36 35 ad4ant14 ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ ran ( ball ‘ 𝐶 ) ∧ 𝑥 ∈ 𝑦 ) ) → ∃ 𝑟 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ⊆ 𝑦 )
37 r19.29 ⊢ ( ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∧ ∃ 𝑟 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ⊆ 𝑦 ) → ∃ 𝑟 ∈ ℝ+ ( ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ⊆ 𝑦 ) )
38 sstr ⊢ ( ( ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ⊆ 𝑦 ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ 𝑦 )
39 38 expcom ⊢ ( ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ⊆ 𝑦 → ( ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ 𝑦 ) )
40 39 reximdv ⊢ ( ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ⊆ 𝑦 → ( ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) → ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ 𝑦 ) )
41 40 impcom ⊢ ( ( ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ⊆ 𝑦 ) → ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ 𝑦 )
42 41 rexlimivw ⊢ ( ∃ 𝑟 ∈ ℝ+ ( ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∧ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ⊆ 𝑦 ) → ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ 𝑦 )
43 37 42 syl ⊢ ( ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ∧ ∃ 𝑟 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ⊆ 𝑦 ) → ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ 𝑦 )
44 43 ex ⊢ ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) → ( ∃ 𝑟 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ⊆ 𝑦 → ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ 𝑦 ) )
45 36 44 syl5com ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ ran ( ball ‘ 𝐶 ) ∧ 𝑥 ∈ 𝑦 ) ) → ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) → ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ 𝑦 ) )
46 45 expr ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ ran ( ball ‘ 𝐶 ) ) → ( 𝑥 ∈ 𝑦 → ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) → ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ 𝑦 ) ) )
47 46 com23 ⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ ran ( ball ‘ 𝐶 ) ) → ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) → ( 𝑥 ∈ 𝑦 → ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ 𝑦 ) ) )
48 47 ralrimdva ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) → ∀ 𝑦 ∈ ran ( ball ‘ 𝐶 ) ( 𝑥 ∈ 𝑦 → ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ 𝑦 ) ) )
49 33 48 impbid ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑦 ∈ ran ( ball ‘ 𝐶 ) ( 𝑥 ∈ 𝑦 → ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ 𝑦 ) ↔ ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ) )
50 20 49 bitrd ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑦 ∈ ran ( ball ‘ 𝐶 ) ( 𝑥 ∈ 𝑦 → ∃ 𝑧 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ↔ ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ) )
51 50 ralbidva ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ ran ( ball ‘ 𝐶 ) ( 𝑥 ∈ 𝑦 → ∃ 𝑧 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ) )
52 16 51 bitrd ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( ∀ 𝑥 ∈ ∪ ran ( ball ‘ 𝐶 ) ∀ 𝑦 ∈ ran ( ball ‘ 𝐶 ) ( 𝑥 ∈ 𝑦 → ∃ 𝑧 ∈ ran ( ball ‘ 𝐷 ) ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ) )
53 7 15 52 3bitrd ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( 𝐽 ⊆ 𝐾 ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ) )