MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  metrest Structured version   Visualization version   GIF version
Theorem metrest 24024
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.)
Hypotheses
Ref Expression
metrest.1 𝐷 = (𝐢 β†Ύ (π‘Œ Γ— π‘Œ))
metrest.3 𝐽 = (MetOpenβ€˜πΆ)
metrest.4 𝐾 = (MetOpenβ€˜π·)
Assertion
Ref Expression
metrest ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (𝐽 β†Ύt π‘Œ) = 𝐾)
Proof of Theorem metrest
Dummy variables 𝑒 π‘Ÿ π‘₯ 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 inss1 4227 . . . . . . . . . 10 (𝑒 ∩ π‘Œ) βŠ† 𝑒
2 metrest.3 . . . . . . . . . . . . 13 𝐽 = (MetOpenβ€˜πΆ)
32elmopn2 23942 . . . . . . . . . . . 12 (𝐢 ∈ (∞Metβ€˜π‘‹) β†’ (𝑒 ∈ 𝐽 ↔ (𝑒 βŠ† 𝑋 ∧ βˆ€π‘¦ ∈ 𝑒 βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜πΆ)π‘Ÿ) βŠ† 𝑒)))
43simplbda 500 . . . . . . . . . . 11 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑒 ∈ 𝐽) β†’ βˆ€π‘¦ ∈ 𝑒 βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜πΆ)π‘Ÿ) βŠ† 𝑒)
54adantlr 713 . . . . . . . . . 10 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑒 ∈ 𝐽) β†’ βˆ€π‘¦ ∈ 𝑒 βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜πΆ)π‘Ÿ) βŠ† 𝑒)
6 ssralv 4049 . . . . . . . . . 10 ((𝑒 ∩ π‘Œ) βŠ† 𝑒 β†’ (βˆ€π‘¦ ∈ 𝑒 βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜πΆ)π‘Ÿ) βŠ† 𝑒 β†’ βˆ€π‘¦ ∈ (𝑒 ∩ π‘Œ)βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜πΆ)π‘Ÿ) βŠ† 𝑒))
71, 5, 6mpsyl 68 . . . . . . . . 9 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑒 ∈ 𝐽) β†’ βˆ€π‘¦ ∈ (𝑒 ∩ π‘Œ)βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜πΆ)π‘Ÿ) βŠ† 𝑒)
8 ssrin 4232 . . . . . . . . . . 11 ((𝑦(ballβ€˜πΆ)π‘Ÿ) βŠ† 𝑒 β†’ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† (𝑒 ∩ π‘Œ))
98reximi 3084 . . . . . . . . . 10 (βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜πΆ)π‘Ÿ) βŠ† 𝑒 β†’ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† (𝑒 ∩ π‘Œ))
109ralimi 3083 . . . . . . . . 9 (βˆ€π‘¦ ∈ (𝑒 ∩ π‘Œ)βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜πΆ)π‘Ÿ) βŠ† 𝑒 β†’ βˆ€π‘¦ ∈ (𝑒 ∩ π‘Œ)βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† (𝑒 ∩ π‘Œ))
117, 10syl 17 . . . . . . . 8 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑒 ∈ 𝐽) β†’ βˆ€π‘¦ ∈ (𝑒 ∩ π‘Œ)βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† (𝑒 ∩ π‘Œ))
12 inss2 4228 . . . . . . . 8 (𝑒 ∩ π‘Œ) βŠ† π‘Œ
1311, 12jctil 520 . . . . . . 7 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑒 ∈ 𝐽) β†’ ((𝑒 ∩ π‘Œ) βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ (𝑒 ∩ π‘Œ)βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† (𝑒 ∩ π‘Œ)))
14 sseq1 4006 . . . . . . . 8 (π‘₯ = (𝑒 ∩ π‘Œ) β†’ (π‘₯ βŠ† π‘Œ ↔ (𝑒 ∩ π‘Œ) βŠ† π‘Œ))
15 sseq2 4007 . . . . . . . . . 10 (π‘₯ = (𝑒 ∩ π‘Œ) β†’ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ↔ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† (𝑒 ∩ π‘Œ)))
1615rexbidv 3178 . . . . . . . . 9 (π‘₯ = (𝑒 ∩ π‘Œ) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ↔ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† (𝑒 ∩ π‘Œ)))
1716raleqbi1dv 3333 . . . . . . . 8 (π‘₯ = (𝑒 ∩ π‘Œ) β†’ (βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ↔ βˆ€π‘¦ ∈ (𝑒 ∩ π‘Œ)βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† (𝑒 ∩ π‘Œ)))
1814, 17anbi12d 631 . . . . . . 7 (π‘₯ = (𝑒 ∩ π‘Œ) β†’ ((π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯) ↔ ((𝑒 ∩ π‘Œ) βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ (𝑒 ∩ π‘Œ)βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† (𝑒 ∩ π‘Œ))))
1913, 18syl5ibrcom 246 . . . . . 6 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑒 ∈ 𝐽) β†’ (π‘₯ = (𝑒 ∩ π‘Œ) β†’ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)))
2019rexlimdva 3155 . . . . 5 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (βˆƒπ‘’ ∈ 𝐽 π‘₯ = (𝑒 ∩ π‘Œ) β†’ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)))
212mopntop 23937 . . . . . . . . 9 (𝐢 ∈ (∞Metβ€˜π‘‹) β†’ 𝐽 ∈ Top)
2221ad2antrr 724 . . . . . . . 8 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ 𝐽 ∈ Top)
23 ssel2 3976 . . . . . . . . . . . . . 14 ((π‘₯ βŠ† π‘Œ ∧ 𝑦 ∈ π‘₯) β†’ 𝑦 ∈ π‘Œ)
24 ssel2 3976 . . . . . . . . . . . . . . . 16 ((π‘Œ βŠ† 𝑋 ∧ 𝑦 ∈ π‘Œ) β†’ 𝑦 ∈ 𝑋)
25 rpxr 12979 . . . . . . . . . . . . . . . . . 18 (π‘Ÿ ∈ ℝ+ β†’ π‘Ÿ ∈ ℝ*)
262blopn 24000 . . . . . . . . . . . . . . . . . . . 20 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ 𝑋 ∧ π‘Ÿ ∈ ℝ*) β†’ (𝑦(ballβ€˜πΆ)π‘Ÿ) ∈ 𝐽)
27 eleq1a 2828 . . . . . . . . . . . . . . . . . . . 20 ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∈ 𝐽 β†’ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ 𝑧 ∈ 𝐽))
2826, 27syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ 𝑋 ∧ π‘Ÿ ∈ ℝ*) β†’ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ 𝑧 ∈ 𝐽))
29283expa 1118 . . . . . . . . . . . . . . . . . 18 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ 𝑋) ∧ π‘Ÿ ∈ ℝ*) β†’ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ 𝑧 ∈ 𝐽))
3025, 29sylan2 593 . . . . . . . . . . . . . . . . 17 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ 𝑋) ∧ π‘Ÿ ∈ ℝ+) β†’ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ 𝑧 ∈ 𝐽))
3130rexlimdva 3155 . . . . . . . . . . . . . . . 16 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ 𝑋) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ 𝑧 ∈ 𝐽))
3224, 31sylan2 593 . . . . . . . . . . . . . . 15 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑦 ∈ π‘Œ)) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ 𝑧 ∈ 𝐽))
3332anassrs 468 . . . . . . . . . . . . . 14 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑦 ∈ π‘Œ) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ 𝑧 ∈ 𝐽))
3423, 33sylan2 593 . . . . . . . . . . . . 13 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ 𝑦 ∈ π‘₯)) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ 𝑧 ∈ 𝐽))
3534anassrs 468 . . . . . . . . . . . 12 ((((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ 𝑧 ∈ 𝐽))
3635rexlimdva 3155 . . . . . . . . . . 11 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ π‘₯ βŠ† π‘Œ) β†’ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ 𝑧 ∈ 𝐽))
3736adantrd 492 . . . . . . . . . 10 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ π‘₯ βŠ† π‘Œ) β†’ ((βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯) β†’ 𝑧 ∈ 𝐽))
3837adantrr 715 . . . . . . . . 9 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ ((βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯) β†’ 𝑧 ∈ 𝐽))
3938abssdv 4064 . . . . . . . 8 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} βŠ† 𝐽)
40 uniopn 22390 . . . . . . . 8 ((𝐽 ∈ Top ∧ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} βŠ† 𝐽) β†’ βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} ∈ 𝐽)
4122, 39, 40syl2anc 584 . . . . . . 7 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} ∈ 𝐽)
42 oveq1 7412 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑒 β†’ (𝑦(ballβ€˜πΆ)π‘Ÿ) = (𝑒(ballβ€˜πΆ)π‘Ÿ))
4342ineq1d 4210 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑒 β†’ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) = ((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ))
4443sseq1d 4012 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑒 β†’ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ↔ ((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
4544rexbidv 3178 . . . . . . . . . . . . . . 15 (𝑦 = 𝑒 β†’ (βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ↔ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
4645rspccv 3609 . . . . . . . . . . . . . 14 (βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ β†’ (𝑒 ∈ π‘₯ β†’ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
4746ad2antll 727 . . . . . . . . . . . . 13 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ (𝑒 ∈ π‘₯ β†’ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
48 ssel 3974 . . . . . . . . . . . . . . 15 (π‘₯ βŠ† π‘Œ β†’ (𝑒 ∈ π‘₯ β†’ 𝑒 ∈ π‘Œ))
49 ssel 3974 . . . . . . . . . . . . . . . 16 (π‘Œ βŠ† 𝑋 β†’ (𝑒 ∈ π‘Œ β†’ 𝑒 ∈ 𝑋))
50 blcntr 23910 . . . . . . . . . . . . . . . . . . . . 21 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑒 ∈ 𝑋 ∧ π‘Ÿ ∈ ℝ+) β†’ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ))
5150a1d 25 . . . . . . . . . . . . . . . . . . . 20 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑒 ∈ 𝑋 ∧ π‘Ÿ ∈ ℝ+) β†’ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ β†’ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ)))
5251ancld 551 . . . . . . . . . . . . . . . . . . 19 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑒 ∈ 𝑋 ∧ π‘Ÿ ∈ ℝ+) β†’ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ β†’ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ))))
53523expa 1118 . . . . . . . . . . . . . . . . . 18 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑒 ∈ 𝑋) ∧ π‘Ÿ ∈ ℝ+) β†’ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ β†’ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ))))
5453reximdva 3168 . . . . . . . . . . . . . . . . 17 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑒 ∈ 𝑋) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ ((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ β†’ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ))))
5554ex 413 . . . . . . . . . . . . . . . 16 (𝐢 ∈ (∞Metβ€˜π‘‹) β†’ (𝑒 ∈ 𝑋 β†’ (βˆƒπ‘Ÿ ∈ ℝ+ ((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ β†’ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ)))))
5649, 55sylan9r 509 . . . . . . . . . . . . . . 15 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (𝑒 ∈ π‘Œ β†’ (βˆƒπ‘Ÿ ∈ ℝ+ ((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ β†’ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ)))))
5748, 56sylan9r 509 . . . . . . . . . . . . . 14 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ π‘₯ βŠ† π‘Œ) β†’ (𝑒 ∈ π‘₯ β†’ (βˆƒπ‘Ÿ ∈ ℝ+ ((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ β†’ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ)))))
5857adantrr 715 . . . . . . . . . . . . 13 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ (𝑒 ∈ π‘₯ β†’ (βˆƒπ‘Ÿ ∈ ℝ+ ((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ β†’ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ)))))
5947, 58mpdd 43 . . . . . . . . . . . 12 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ (𝑒 ∈ π‘₯ β†’ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ))))
6042eleq2d 2819 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑒 β†’ (𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ) ↔ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ)))
6144, 60anbi12d 631 . . . . . . . . . . . . . . 15 (𝑦 = 𝑒 β†’ ((((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)) ↔ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ))))
6261rexbidv 3178 . . . . . . . . . . . . . 14 (𝑦 = 𝑒 β†’ (βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)) ↔ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ))))
6362rspcev 3612 . . . . . . . . . . . . 13 ((𝑒 ∈ π‘₯ ∧ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ))) β†’ βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)))
6463ex 413 . . . . . . . . . . . 12 (𝑒 ∈ π‘₯ β†’ (βˆƒπ‘Ÿ ∈ ℝ+ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ)) β†’ βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ))))
6559, 64sylcom 30 . . . . . . . . . . 11 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ (𝑒 ∈ π‘₯ β†’ βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ))))
66 simprl 769 . . . . . . . . . . . 12 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ π‘₯ βŠ† π‘Œ)
6766sseld 3980 . . . . . . . . . . 11 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ (𝑒 ∈ π‘₯ β†’ 𝑒 ∈ π‘Œ))
6865, 67jcad 513 . . . . . . . . . 10 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ (𝑒 ∈ π‘₯ β†’ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)) ∧ 𝑒 ∈ π‘Œ)))
69 elin 3963 . . . . . . . . . . . . . . 15 (𝑒 ∈ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) ↔ (𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ 𝑒 ∈ π‘Œ))
70 ssel2 3976 . . . . . . . . . . . . . . 15 ((((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ)) β†’ 𝑒 ∈ π‘₯)
7169, 70sylan2br 595 . . . . . . . . . . . . . 14 ((((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ (𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ 𝑒 ∈ π‘Œ)) β†’ 𝑒 ∈ π‘₯)
7271expr 457 . . . . . . . . . . . . 13 ((((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)) β†’ (𝑒 ∈ π‘Œ β†’ 𝑒 ∈ π‘₯))
7372rexlimivw 3151 . . . . . . . . . . . 12 (βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)) β†’ (𝑒 ∈ π‘Œ β†’ 𝑒 ∈ π‘₯))
7473rexlimivw 3151 . . . . . . . . . . 11 (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)) β†’ (𝑒 ∈ π‘Œ β†’ 𝑒 ∈ π‘₯))
7574imp 407 . . . . . . . . . 10 ((βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)) ∧ 𝑒 ∈ π‘Œ) β†’ 𝑒 ∈ π‘₯)
7668, 75impbid1 224 . . . . . . . . 9 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ (𝑒 ∈ π‘₯ ↔ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)) ∧ 𝑒 ∈ π‘Œ)))
77 elin 3963 . . . . . . . . . 10 (𝑒 ∈ (βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} ∩ π‘Œ) ↔ (𝑒 ∈ βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} ∧ 𝑒 ∈ π‘Œ))
78 eluniab 4922 . . . . . . . . . . . 12 (𝑒 ∈ βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} ↔ βˆƒπ‘§(𝑒 ∈ 𝑧 ∧ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)))
79 ancom 461 . . . . . . . . . . . . . 14 ((𝑒 ∈ 𝑧 ∧ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)) ↔ ((βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯) ∧ 𝑒 ∈ 𝑧))
80 anass 469 . . . . . . . . . . . . . 14 (((βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯) ∧ 𝑒 ∈ 𝑧) ↔ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)))
81 r19.41v 3188 . . . . . . . . . . . . . . . 16 (βˆƒπ‘Ÿ ∈ ℝ+ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)) ↔ (βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)))
8281rexbii 3094 . . . . . . . . . . . . . . 15 (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)) ↔ βˆƒπ‘¦ ∈ π‘₯ (βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)))
83 r19.41v 3188 . . . . . . . . . . . . . . 15 (βˆƒπ‘¦ ∈ π‘₯ (βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)) ↔ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)))
8482, 83bitr2i 275 . . . . . . . . . . . . . 14 ((βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)) ↔ βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)))
8579, 80, 843bitri 296 . . . . . . . . . . . . 13 ((𝑒 ∈ 𝑧 ∧ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)) ↔ βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)))
8685exbii 1850 . . . . . . . . . . . 12 (βˆƒπ‘§(𝑒 ∈ 𝑧 ∧ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)) ↔ βˆƒπ‘§βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)))
87 ovex 7438 . . . . . . . . . . . . . . . . 17 (𝑦(ballβ€˜πΆ)π‘Ÿ) ∈ V
88 ineq1 4204 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ (𝑧 ∩ π‘Œ) = ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ))
8988sseq1d 4012 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ↔ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
90 eleq2 2822 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ (𝑒 ∈ 𝑧 ↔ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)))
9189, 90anbi12d 631 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ (((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧) ↔ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ))))
9287, 91ceqsexv 3525 . . . . . . . . . . . . . . . 16 (βˆƒπ‘§(𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)) ↔ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)))
9392rexbii 3094 . . . . . . . . . . . . . . 15 (βˆƒπ‘Ÿ ∈ ℝ+ βˆƒπ‘§(𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)) ↔ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)))
94 rexcom4 3285 . . . . . . . . . . . . . . 15 (βˆƒπ‘Ÿ ∈ ℝ+ βˆƒπ‘§(𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)) ↔ βˆƒπ‘§βˆƒπ‘Ÿ ∈ ℝ+ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)))
9593, 94bitr3i 276 . . . . . . . . . . . . . 14 (βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)) ↔ βˆƒπ‘§βˆƒπ‘Ÿ ∈ ℝ+ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)))
9695rexbii 3094 . . . . . . . . . . . . 13 (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)) ↔ βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘§βˆƒπ‘Ÿ ∈ ℝ+ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)))
97 rexcom4 3285 . . . . . . . . . . . . 13 (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘§βˆƒπ‘Ÿ ∈ ℝ+ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)) ↔ βˆƒπ‘§βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)))
9896, 97bitr2i 275 . . . . . . . . . . . 12 (βˆƒπ‘§βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)) ↔ βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)))
9978, 86, 983bitri 296 . . . . . . . . . . 11 (𝑒 ∈ βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} ↔ βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)))
10099anbi1i 624 . . . . . . . . . 10 ((𝑒 ∈ βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} ∧ 𝑒 ∈ π‘Œ) ↔ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)) ∧ 𝑒 ∈ π‘Œ))
10177, 100bitr2i 275 . . . . . . . . 9 ((βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)) ∧ 𝑒 ∈ π‘Œ) ↔ 𝑒 ∈ (βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} ∩ π‘Œ))
10276, 101bitrdi 286 . . . . . . . 8 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ (𝑒 ∈ π‘₯ ↔ 𝑒 ∈ (βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} ∩ π‘Œ)))
103102eqrdv 2730 . . . . . . 7 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ π‘₯ = (βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} ∩ π‘Œ))
104 ineq1 4204 . . . . . . . 8 (𝑒 = βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} β†’ (𝑒 ∩ π‘Œ) = (βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} ∩ π‘Œ))
105104rspceeqv 3632 . . . . . . 7 ((βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} ∈ 𝐽 ∧ π‘₯ = (βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} ∩ π‘Œ)) β†’ βˆƒπ‘’ ∈ 𝐽 π‘₯ = (𝑒 ∩ π‘Œ))
10641, 103, 105syl2anc 584 . . . . . 6 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ βˆƒπ‘’ ∈ 𝐽 π‘₯ = (𝑒 ∩ π‘Œ))
107106ex 413 . . . . 5 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ ((π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯) β†’ βˆƒπ‘’ ∈ 𝐽 π‘₯ = (𝑒 ∩ π‘Œ)))
10820, 107impbid 211 . . . 4 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (βˆƒπ‘’ ∈ 𝐽 π‘₯ = (𝑒 ∩ π‘Œ) ↔ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)))
109 simpr 485 . . . . . . . . . . 11 ((π‘Œ βŠ† 𝑋 ∧ 𝑦 ∈ π‘Œ) β†’ 𝑦 ∈ π‘Œ)
11024, 109elind 4193 . . . . . . . . . 10 ((π‘Œ βŠ† 𝑋 ∧ 𝑦 ∈ π‘Œ) β†’ 𝑦 ∈ (𝑋 ∩ π‘Œ))
111 metrest.1 . . . . . . . . . . . . . . 15 𝐷 = (𝐢 β†Ύ (π‘Œ Γ— π‘Œ))
112111blres 23928 . . . . . . . . . . . . . 14 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ (𝑋 ∩ π‘Œ) ∧ π‘Ÿ ∈ ℝ*) β†’ (𝑦(ballβ€˜π·)π‘Ÿ) = ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ))
113112sseq1d 4012 . . . . . . . . . . . . 13 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ (𝑋 ∩ π‘Œ) ∧ π‘Ÿ ∈ ℝ*) β†’ ((𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯ ↔ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
1141133expa 1118 . . . . . . . . . . . 12 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ (𝑋 ∩ π‘Œ)) ∧ π‘Ÿ ∈ ℝ*) β†’ ((𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯ ↔ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
11525, 114sylan2 593 . . . . . . . . . . 11 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ (𝑋 ∩ π‘Œ)) ∧ π‘Ÿ ∈ ℝ+) β†’ ((𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯ ↔ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
116115rexbidva 3176 . . . . . . . . . 10 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ (𝑋 ∩ π‘Œ)) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯ ↔ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
117110, 116sylan2 593 . . . . . . . . 9 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑦 ∈ π‘Œ)) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯ ↔ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
118117anassrs 468 . . . . . . . 8 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑦 ∈ π‘Œ) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯ ↔ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
11923, 118sylan2 593 . . . . . . 7 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ 𝑦 ∈ π‘₯)) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯ ↔ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
120119anassrs 468 . . . . . 6 ((((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯ ↔ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
121120ralbidva 3175 . . . . 5 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ π‘₯ βŠ† π‘Œ) β†’ (βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯ ↔ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
122121pm5.32da 579 . . . 4 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ ((π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯) ↔ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)))
123108, 122bitr4d 281 . . 3 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (βˆƒπ‘’ ∈ 𝐽 π‘₯ = (𝑒 ∩ π‘Œ) ↔ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯)))
124 id 22 . . . . 5 (π‘Œ βŠ† 𝑋 β†’ π‘Œ βŠ† 𝑋)
1252mopnm 23941 . . . . 5 (𝐢 ∈ (∞Metβ€˜π‘‹) β†’ 𝑋 ∈ 𝐽)
126 ssexg 5322 . . . . 5 ((π‘Œ βŠ† 𝑋 ∧ 𝑋 ∈ 𝐽) β†’ π‘Œ ∈ V)
127124, 125, 126syl2anr 597 . . . 4 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ π‘Œ ∈ V)
128 elrest 17369 . . . 4 ((𝐽 ∈ Top ∧ π‘Œ ∈ V) β†’ (π‘₯ ∈ (𝐽 β†Ύt π‘Œ) ↔ βˆƒπ‘’ ∈ 𝐽 π‘₯ = (𝑒 ∩ π‘Œ)))
12921, 127, 128syl2an2r 683 . . 3 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (π‘₯ ∈ (𝐽 β†Ύt π‘Œ) ↔ βˆƒπ‘’ ∈ 𝐽 π‘₯ = (𝑒 ∩ π‘Œ)))
130 xmetres2 23858 . . . . 5 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (𝐢 β†Ύ (π‘Œ Γ— π‘Œ)) ∈ (∞Metβ€˜π‘Œ))
131111, 130eqeltrid 2837 . . . 4 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ 𝐷 ∈ (∞Metβ€˜π‘Œ))
132 metrest.4 . . . . 5 𝐾 = (MetOpenβ€˜π·)
133132elmopn2 23942 . . . 4 (𝐷 ∈ (∞Metβ€˜π‘Œ) β†’ (π‘₯ ∈ 𝐾 ↔ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯)))
134131, 133syl 17 . . 3 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (π‘₯ ∈ 𝐾 ↔ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯)))
135123, 129, 1343bitr4d 310 . 2 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (π‘₯ ∈ (𝐽 β†Ύt π‘Œ) ↔ π‘₯ ∈ 𝐾))
136135eqrdv 2730 1 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (𝐽 β†Ύt π‘Œ) = 𝐾)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541  βˆƒwex 1781   ∈ wcel 2106  {cab 2709  βˆ€wral 3061  βˆƒwrex 3070  Vcvv 3474   ∩ cin 3946   βŠ† wss 3947  βˆͺ cuni 4907   Γ— cxp 5673   β†Ύ cres 5677  β€˜cfv 6540  (class class class)co 7405  β„*cxr 11243  β„+crp 12970   β†Ύt crest 17362  βˆžMetcxmet 20921  ballcbl 20923  MetOpencmopn 20926  Topctop 22386
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8699  df-map 8818  df-en 8936  df-dom 8937  df-sdom 8938  df-sup 9433  df-inf 9434  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-n0 12469  df-z 12555  df-uz 12819  df-q 12929  df-rp 12971  df-xneg 13088  df-xadd 13089  df-xmul 13090  df-rest 17364  df-topgen 17385  df-psmet 20928  df-xmet 20929  df-bl 20931  df-mopn 20932  df-top 22387  df-topon 22404  df-bases 22440
This theorem is referenced by:  ressxms  24025  nrginvrcn  24200  resubmet  24309  tgioo2  24310  metdscn2  24364  divcn  24375  dfii3  24390  cncfcn  24417  metsscmetcld  24823  cmetss  24824  minveclem4a  24938  ftc1lem6  25549  ulmdvlem3  25905  abelth  25944  cxpcn3  26245  rlimcnp  26459  minvecolem4b  30118  minvecolem4  30120  hhsscms  30518  gg-divcn  35151  ftc1cnnc  36548
  Copyright terms: Public domain W3C validator