Metamath Proof Explorer

Theorem met2ndci

Description: A separable metric space (a metric space with a countable dense subset) is second-countable. (Contributed by Mario Carneiro, 13-Apr-2015)

Ref Expression
Hypothesis methaus.1 ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
Assertion met2ndci ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) β†’ 𝐽 ∈ 2ndΟ‰ )

Proof

Step Hyp Ref Expression
1 methaus.1 ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
2 1 mopntop ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ 𝐽 ∈ Top )
3 2 adantr ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) β†’ 𝐽 ∈ Top )
4 simpll ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( π‘₯ ∈ β„• ∧ 𝑦 ∈ 𝐴 ) ) β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
5 simplr1 ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( π‘₯ ∈ β„• ∧ 𝑦 ∈ 𝐴 ) ) β†’ 𝐴 βŠ† 𝑋 )
6 simprr ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( π‘₯ ∈ β„• ∧ 𝑦 ∈ 𝐴 ) ) β†’ 𝑦 ∈ 𝐴 )
7 5 6 sseldd ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( π‘₯ ∈ β„• ∧ 𝑦 ∈ 𝐴 ) ) β†’ 𝑦 ∈ 𝑋 )
8 simprl ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( π‘₯ ∈ β„• ∧ 𝑦 ∈ 𝐴 ) ) β†’ π‘₯ ∈ β„• )
9 8 nnrpd ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( π‘₯ ∈ β„• ∧ 𝑦 ∈ 𝐴 ) ) β†’ π‘₯ ∈ ℝ+ )
10 9 rpreccld ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( π‘₯ ∈ β„• ∧ 𝑦 ∈ 𝐴 ) ) β†’ ( 1 / π‘₯ ) ∈ ℝ+ )
11 10 rpxrd ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( π‘₯ ∈ β„• ∧ 𝑦 ∈ 𝐴 ) ) β†’ ( 1 / π‘₯ ) ∈ ℝ* )
12 1 blopn ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ∧ ( 1 / π‘₯ ) ∈ ℝ* ) β†’ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ∈ 𝐽 )
13 4 7 11 12 syl3anc ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( π‘₯ ∈ β„• ∧ 𝑦 ∈ 𝐴 ) ) β†’ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ∈ 𝐽 )
14 13 ralrimivva ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) β†’ βˆ€ π‘₯ ∈ β„• βˆ€ 𝑦 ∈ 𝐴 ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ∈ 𝐽 )
15 eqid ⊒ ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) = ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) )
16 15 fmpo ⊒ ( βˆ€ π‘₯ ∈ β„• βˆ€ 𝑦 ∈ 𝐴 ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ∈ 𝐽 ↔ ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) : ( β„• Γ— 𝐴 ) ⟢ 𝐽 )
17 14 16 sylib ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) β†’ ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) : ( β„• Γ— 𝐴 ) ⟢ 𝐽 )
18 17 frnd ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) β†’ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) βŠ† 𝐽 )
19 simpll ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
20 simprl ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) β†’ 𝑒 ∈ 𝐽 )
21 simprr ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) β†’ 𝑧 ∈ 𝑒 )
22 1 mopni2 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) β†’ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 )
23 19 20 21 22 syl3anc ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) β†’ βˆƒ π‘Ÿ ∈ ℝ+ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 )
24 simprl ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ) β†’ π‘Ÿ ∈ ℝ+ )
25 24 rphalfcld ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ) β†’ ( π‘Ÿ / 2 ) ∈ ℝ+ )
26 elrp ⊒ ( ( π‘Ÿ / 2 ) ∈ ℝ+ ↔ ( ( π‘Ÿ / 2 ) ∈ ℝ ∧ 0 < ( π‘Ÿ / 2 ) ) )
27 nnrecl ⊒ ( ( ( π‘Ÿ / 2 ) ∈ ℝ ∧ 0 < ( π‘Ÿ / 2 ) ) β†’ βˆƒ 𝑛 ∈ β„• ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) )
28 26 27 sylbi ⊒ ( ( π‘Ÿ / 2 ) ∈ ℝ+ β†’ βˆƒ 𝑛 ∈ β„• ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) )
29 25 28 syl ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ) β†’ βˆƒ 𝑛 ∈ β„• ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) )
30 3 ad2antrr ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) β†’ 𝐽 ∈ Top )
31 simpr1 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) β†’ 𝐴 βŠ† 𝑋 )
32 31 ad2antrr ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) β†’ 𝐴 βŠ† 𝑋 )
33 1 mopnuni ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ 𝑋 = βˆͺ 𝐽 )
34 33 ad3antrrr ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) β†’ 𝑋 = βˆͺ 𝐽 )
35 32 34 sseqtrd ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) β†’ 𝐴 βŠ† βˆͺ 𝐽 )
36 simplrr ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) β†’ 𝑧 ∈ 𝑒 )
37 simplrl ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) β†’ 𝑒 ∈ 𝐽 )
38 elunii ⊒ ( ( 𝑧 ∈ 𝑒 ∧ 𝑒 ∈ 𝐽 ) β†’ 𝑧 ∈ βˆͺ 𝐽 )
39 36 37 38 syl2anc ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) β†’ 𝑧 ∈ βˆͺ 𝐽 )
40 39 34 eleqtrrd ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) β†’ 𝑧 ∈ 𝑋 )
41 simpr3 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) β†’ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 )
42 41 ad2antrr ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) β†’ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 )
43 40 42 eleqtrrd ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) β†’ 𝑧 ∈ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) )
44 19 adantr ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
45 simprrl ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) β†’ 𝑛 ∈ β„• )
46 45 nnrpd ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) β†’ 𝑛 ∈ ℝ+ )
47 46 rpreccld ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) β†’ ( 1 / 𝑛 ) ∈ ℝ+ )
48 47 rpxrd ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) β†’ ( 1 / 𝑛 ) ∈ ℝ* )
49 1 blopn ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ∧ ( 1 / 𝑛 ) ∈ ℝ* ) β†’ ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∈ 𝐽 )
50 44 40 48 49 syl3anc ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) β†’ ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∈ 𝐽 )
51 blcntr ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ∧ ( 1 / 𝑛 ) ∈ ℝ+ ) β†’ 𝑧 ∈ ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) )
52 44 40 47 51 syl3anc ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) β†’ 𝑧 ∈ ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) )
53 eqid ⊒ βˆͺ 𝐽 = βˆͺ 𝐽
54 53 clsndisj ⊒ ( ( ( 𝐽 ∈ Top ∧ 𝐴 βŠ† βˆͺ 𝐽 ∧ 𝑧 ∈ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) ) ∧ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∈ 𝐽 ∧ 𝑧 ∈ ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ) ) β†’ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) β‰  βˆ… )
55 30 35 43 50 52 54 syl32anc ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) β†’ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) β‰  βˆ… )
56 n0 ⊒ ( ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) β‰  βˆ… ↔ βˆƒ 𝑑 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) )
57 55 56 sylib ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) β†’ βˆƒ 𝑑 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) )
58 45 adantr ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) ∧ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) β†’ 𝑛 ∈ β„• )
59 simpr ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) ∧ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) β†’ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) )
60 59 elin2d ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) ∧ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) β†’ 𝑑 ∈ 𝐴 )
61 eqidd ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) ∧ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) β†’ ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) = ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) )
62 oveq2 ⊒ ( π‘₯ = 𝑛 β†’ ( 1 / π‘₯ ) = ( 1 / 𝑛 ) )
63 62 oveq2d ⊒ ( π‘₯ = 𝑛 β†’ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) = ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) )
64 63 eqeq2d ⊒ ( π‘₯ = 𝑛 β†’ ( ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) = ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ↔ ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) = ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ) )
65 oveq1 ⊒ ( 𝑦 = 𝑑 β†’ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) = ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) )
66 65 eqeq2d ⊒ ( 𝑦 = 𝑑 β†’ ( ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) = ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ↔ ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) = ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ) )
67 64 66 rspc2ev ⊒ ( ( 𝑛 ∈ β„• ∧ 𝑑 ∈ 𝐴 ∧ ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) = ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ) β†’ βˆƒ π‘₯ ∈ β„• βˆƒ 𝑦 ∈ 𝐴 ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) = ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) )
68 58 60 61 67 syl3anc ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) ∧ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) β†’ βˆƒ π‘₯ ∈ β„• βˆƒ 𝑦 ∈ 𝐴 ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) = ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) )
69 ovex ⊒ ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∈ V
70 eqeq1 ⊒ ( 𝑧 = ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) β†’ ( 𝑧 = ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ↔ ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) = ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) )
71 70 2rexbidv ⊒ ( 𝑧 = ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) β†’ ( βˆƒ π‘₯ ∈ β„• βˆƒ 𝑦 ∈ 𝐴 𝑧 = ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ↔ βˆƒ π‘₯ ∈ β„• βˆƒ 𝑦 ∈ 𝐴 ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) = ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) )
72 15 rnmpo ⊒ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) = { 𝑧 ∣ βˆƒ π‘₯ ∈ β„• βˆƒ 𝑦 ∈ 𝐴 𝑧 = ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) }
73 69 71 72 elab2 ⊒ ( ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∈ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) ↔ βˆƒ π‘₯ ∈ β„• βˆƒ 𝑦 ∈ 𝐴 ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) = ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) )
74 68 73 sylibr ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) ∧ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) β†’ ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∈ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) )
75 59 elin1d ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) ∧ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) β†’ 𝑑 ∈ ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) )
76 44 adantr ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) ∧ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
77 48 adantr ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) ∧ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) β†’ ( 1 / 𝑛 ) ∈ ℝ* )
78 40 adantr ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) ∧ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) β†’ 𝑧 ∈ 𝑋 )
79 32 adantr ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) ∧ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) β†’ 𝐴 βŠ† 𝑋 )
80 79 60 sseldd ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) ∧ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) β†’ 𝑑 ∈ 𝑋 )
81 blcom ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 1 / 𝑛 ) ∈ ℝ* ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑑 ∈ 𝑋 ) ) β†’ ( 𝑑 ∈ ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ↔ 𝑧 ∈ ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ) )
82 76 77 78 80 81 syl22anc ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) ∧ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) β†’ ( 𝑑 ∈ ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ↔ 𝑧 ∈ ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ) )
83 75 82 mpbid ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) ∧ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) β†’ 𝑧 ∈ ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) )
84 simprll ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) β†’ π‘Ÿ ∈ ℝ+ )
85 84 adantr ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) ∧ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) β†’ π‘Ÿ ∈ ℝ+ )
86 85 rphalfcld ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) ∧ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) β†’ ( π‘Ÿ / 2 ) ∈ ℝ+ )
87 86 rpxrd ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) ∧ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) β†’ ( π‘Ÿ / 2 ) ∈ ℝ* )
88 simprrr ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) β†’ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) )
89 84 rphalfcld ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) β†’ ( π‘Ÿ / 2 ) ∈ ℝ+ )
90 rpre ⊒ ( ( 1 / 𝑛 ) ∈ ℝ+ β†’ ( 1 / 𝑛 ) ∈ ℝ )
91 rpre ⊒ ( ( π‘Ÿ / 2 ) ∈ ℝ+ β†’ ( π‘Ÿ / 2 ) ∈ ℝ )
92 ltle ⊒ ( ( ( 1 / 𝑛 ) ∈ ℝ ∧ ( π‘Ÿ / 2 ) ∈ ℝ ) β†’ ( ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) β†’ ( 1 / 𝑛 ) ≀ ( π‘Ÿ / 2 ) ) )
93 90 91 92 syl2an ⊒ ( ( ( 1 / 𝑛 ) ∈ ℝ+ ∧ ( π‘Ÿ / 2 ) ∈ ℝ+ ) β†’ ( ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) β†’ ( 1 / 𝑛 ) ≀ ( π‘Ÿ / 2 ) ) )
94 47 89 93 syl2anc ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) β†’ ( ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) β†’ ( 1 / 𝑛 ) ≀ ( π‘Ÿ / 2 ) ) )
95 88 94 mpd ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) β†’ ( 1 / 𝑛 ) ≀ ( π‘Ÿ / 2 ) )
96 95 adantr ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) ∧ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) β†’ ( 1 / 𝑛 ) ≀ ( π‘Ÿ / 2 ) )
97 ssbl ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑑 ∈ 𝑋 ) ∧ ( ( 1 / 𝑛 ) ∈ ℝ* ∧ ( π‘Ÿ / 2 ) ∈ ℝ* ) ∧ ( 1 / 𝑛 ) ≀ ( π‘Ÿ / 2 ) ) β†’ ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) βŠ† ( 𝑑 ( ball β€˜ 𝐷 ) ( π‘Ÿ / 2 ) ) )
98 76 80 77 87 96 97 syl221anc ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) ∧ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) β†’ ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) βŠ† ( 𝑑 ( ball β€˜ 𝐷 ) ( π‘Ÿ / 2 ) ) )
99 85 rpred ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) ∧ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) β†’ π‘Ÿ ∈ ℝ )
100 98 83 sseldd ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) ∧ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) β†’ 𝑧 ∈ ( 𝑑 ( ball β€˜ 𝐷 ) ( π‘Ÿ / 2 ) ) )
101 blhalf ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑑 ∈ 𝑋 ) ∧ ( π‘Ÿ ∈ ℝ ∧ 𝑧 ∈ ( 𝑑 ( ball β€˜ 𝐷 ) ( π‘Ÿ / 2 ) ) ) ) β†’ ( 𝑑 ( ball β€˜ 𝐷 ) ( π‘Ÿ / 2 ) ) βŠ† ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) )
102 76 80 99 100 101 syl22anc ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) ∧ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) β†’ ( 𝑑 ( ball β€˜ 𝐷 ) ( π‘Ÿ / 2 ) ) βŠ† ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) )
103 simprlr ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) β†’ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 )
104 103 adantr ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) ∧ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) β†’ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 )
105 102 104 sstrd ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) ∧ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) β†’ ( 𝑑 ( ball β€˜ 𝐷 ) ( π‘Ÿ / 2 ) ) βŠ† 𝑒 )
106 98 105 sstrd ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) ∧ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) β†’ ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) βŠ† 𝑒 )
107 eleq2 ⊒ ( 𝑀 = ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) β†’ ( 𝑧 ∈ 𝑀 ↔ 𝑧 ∈ ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ) )
108 sseq1 ⊒ ( 𝑀 = ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) β†’ ( 𝑀 βŠ† 𝑒 ↔ ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) βŠ† 𝑒 ) )
109 107 108 anbi12d ⊒ ( 𝑀 = ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) β†’ ( ( 𝑧 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑒 ) ↔ ( 𝑧 ∈ ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∧ ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) βŠ† 𝑒 ) ) )
110 109 rspcev ⊒ ( ( ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∈ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) ∧ ( 𝑧 ∈ ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∧ ( 𝑑 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) βŠ† 𝑒 ) ) β†’ βˆƒ 𝑀 ∈ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) ( 𝑧 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑒 ) )
111 74 83 106 110 syl12anc ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) ∧ 𝑑 ∈ ( ( 𝑧 ( ball β€˜ 𝐷 ) ( 1 / 𝑛 ) ) ∩ 𝐴 ) ) β†’ βˆƒ 𝑀 ∈ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) ( 𝑧 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑒 ) )
112 57 111 exlimddv ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) ) β†’ βˆƒ 𝑀 ∈ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) ( 𝑧 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑒 ) )
113 112 anassrs ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ) ∧ ( 𝑛 ∈ β„• ∧ ( 1 / 𝑛 ) < ( π‘Ÿ / 2 ) ) ) β†’ βˆƒ 𝑀 ∈ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) ( 𝑧 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑒 ) )
114 29 113 rexlimddv ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) ∧ ( π‘Ÿ ∈ ℝ+ ∧ ( 𝑧 ( ball β€˜ 𝐷 ) π‘Ÿ ) βŠ† 𝑒 ) ) β†’ βˆƒ 𝑀 ∈ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) ( 𝑧 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑒 ) )
115 23 114 rexlimddv ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) ∧ ( 𝑒 ∈ 𝐽 ∧ 𝑧 ∈ 𝑒 ) ) β†’ βˆƒ 𝑀 ∈ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) ( 𝑧 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑒 ) )
116 115 ralrimivva ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) β†’ βˆ€ 𝑒 ∈ 𝐽 βˆ€ 𝑧 ∈ 𝑒 βˆƒ 𝑀 ∈ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) ( 𝑧 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑒 ) )
117 basgen2 ⊒ ( ( 𝐽 ∈ Top ∧ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) βŠ† 𝐽 ∧ βˆ€ 𝑒 ∈ 𝐽 βˆ€ 𝑧 ∈ 𝑒 βˆƒ 𝑀 ∈ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) ( 𝑧 ∈ 𝑀 ∧ 𝑀 βŠ† 𝑒 ) ) β†’ ( topGen β€˜ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) ) = 𝐽 )
118 3 18 116 117 syl3anc ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) β†’ ( topGen β€˜ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) ) = 𝐽 )
119 118 3 eqeltrd ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) β†’ ( topGen β€˜ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) ) ∈ Top )
120 tgclb ⊒ ( ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) ∈ TopBases ↔ ( topGen β€˜ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) ) ∈ Top )
121 119 120 sylibr ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) β†’ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) ∈ TopBases )
122 omelon ⊒ Ο‰ ∈ On
123 simpr2 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) β†’ 𝐴 β‰Ό Ο‰ )
124 nnex ⊒ β„• ∈ V
125 124 xpdom2 ⊒ ( 𝐴 β‰Ό Ο‰ β†’ ( β„• Γ— 𝐴 ) β‰Ό ( β„• Γ— Ο‰ ) )
126 123 125 syl ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) β†’ ( β„• Γ— 𝐴 ) β‰Ό ( β„• Γ— Ο‰ ) )
127 nnenom ⊒ β„• β‰ˆ Ο‰
128 omex ⊒ Ο‰ ∈ V
129 128 enref ⊒ Ο‰ β‰ˆ Ο‰
130 xpen ⊒ ( ( β„• β‰ˆ Ο‰ ∧ Ο‰ β‰ˆ Ο‰ ) β†’ ( β„• Γ— Ο‰ ) β‰ˆ ( Ο‰ Γ— Ο‰ ) )
131 127 129 130 mp2an ⊒ ( β„• Γ— Ο‰ ) β‰ˆ ( Ο‰ Γ— Ο‰ )
132 xpomen ⊒ ( Ο‰ Γ— Ο‰ ) β‰ˆ Ο‰
133 131 132 entri ⊒ ( β„• Γ— Ο‰ ) β‰ˆ Ο‰
134 domentr ⊒ ( ( ( β„• Γ— 𝐴 ) β‰Ό ( β„• Γ— Ο‰ ) ∧ ( β„• Γ— Ο‰ ) β‰ˆ Ο‰ ) β†’ ( β„• Γ— 𝐴 ) β‰Ό Ο‰ )
135 126 133 134 sylancl ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) β†’ ( β„• Γ— 𝐴 ) β‰Ό Ο‰ )
136 ondomen ⊒ ( ( Ο‰ ∈ On ∧ ( β„• Γ— 𝐴 ) β‰Ό Ο‰ ) β†’ ( β„• Γ— 𝐴 ) ∈ dom card )
137 122 135 136 sylancr ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) β†’ ( β„• Γ— 𝐴 ) ∈ dom card )
138 17 ffnd ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) β†’ ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) Fn ( β„• Γ— 𝐴 ) )
139 dffn4 ⊒ ( ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) Fn ( β„• Γ— 𝐴 ) ↔ ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) : ( β„• Γ— 𝐴 ) –ontoβ†’ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) )
140 138 139 sylib ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) β†’ ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) : ( β„• Γ— 𝐴 ) –ontoβ†’ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) )
141 fodomnum ⊒ ( ( β„• Γ— 𝐴 ) ∈ dom card β†’ ( ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) : ( β„• Γ— 𝐴 ) –ontoβ†’ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) β†’ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) β‰Ό ( β„• Γ— 𝐴 ) ) )
142 137 140 141 sylc ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) β†’ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) β‰Ό ( β„• Γ— 𝐴 ) )
143 domtr ⊒ ( ( ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) β‰Ό ( β„• Γ— 𝐴 ) ∧ ( β„• Γ— 𝐴 ) β‰Ό Ο‰ ) β†’ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) β‰Ό Ο‰ )
144 142 135 143 syl2anc ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) β†’ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) β‰Ό Ο‰ )
145 2ndci ⊒ ( ( ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) ∈ TopBases ∧ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) β‰Ό Ο‰ ) β†’ ( topGen β€˜ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) ) ∈ 2ndΟ‰ )
146 121 144 145 syl2anc ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) β†’ ( topGen β€˜ ran ( π‘₯ ∈ β„• , 𝑦 ∈ 𝐴 ↦ ( 𝑦 ( ball β€˜ 𝐷 ) ( 1 / π‘₯ ) ) ) ) ∈ 2ndΟ‰ )
147 118 146 eqeltrrd ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐴 βŠ† 𝑋 ∧ 𝐴 β‰Ό Ο‰ ∧ ( ( cls β€˜ 𝐽 ) β€˜ 𝐴 ) = 𝑋 ) ) β†’ 𝐽 ∈ 2ndΟ‰ )