MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  metrest Structured version   Visualization version   GIF version
Theorem metrest 24453
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 4231 . . . . . . . . . 10 (𝑒 ∩ π‘Œ) βŠ† 𝑒
2 metrest.3 . . . . . . . . . . . . 13 𝐽 = (MetOpenβ€˜πΆ)
32elmopn2 24371 . . . . . . . . . . . 12 (𝐢 ∈ (∞Metβ€˜π‘‹) β†’ (𝑒 ∈ 𝐽 ↔ (𝑒 βŠ† 𝑋 ∧ βˆ€π‘¦ ∈ 𝑒 βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜πΆ)π‘Ÿ) βŠ† 𝑒)))
43simplbda 498 . . . . . . . . . . 11 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑒 ∈ 𝐽) β†’ βˆ€π‘¦ ∈ 𝑒 βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜πΆ)π‘Ÿ) βŠ† 𝑒)
54adantlr 713 . . . . . . . . . 10 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑒 ∈ 𝐽) β†’ βˆ€π‘¦ ∈ 𝑒 βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜πΆ)π‘Ÿ) βŠ† 𝑒)
6 ssralv 4050 . . . . . . . . . 10 ((𝑒 ∩ π‘Œ) βŠ† 𝑒 β†’ (βˆ€π‘¦ ∈ 𝑒 βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜πΆ)π‘Ÿ) βŠ† 𝑒 β†’ βˆ€π‘¦ ∈ (𝑒 ∩ π‘Œ)βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜πΆ)π‘Ÿ) βŠ† 𝑒))
71, 5, 6mpsyl 68 . . . . . . . . 9 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑒 ∈ 𝐽) β†’ βˆ€π‘¦ ∈ (𝑒 ∩ π‘Œ)βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜πΆ)π‘Ÿ) βŠ† 𝑒)
8 ssrin 4236 . . . . . . . . . . 11 ((𝑦(ballβ€˜πΆ)π‘Ÿ) βŠ† 𝑒 β†’ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† (𝑒 ∩ π‘Œ))
98reximi 3081 . . . . . . . . . 10 (βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜πΆ)π‘Ÿ) βŠ† 𝑒 β†’ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† (𝑒 ∩ π‘Œ))
109ralimi 3080 . . . . . . . . 9 (βˆ€π‘¦ ∈ (𝑒 ∩ π‘Œ)βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜πΆ)π‘Ÿ) βŠ† 𝑒 β†’ βˆ€π‘¦ ∈ (𝑒 ∩ π‘Œ)βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† (𝑒 ∩ π‘Œ))
117, 10syl 17 . . . . . . . 8 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑒 ∈ 𝐽) β†’ βˆ€π‘¦ ∈ (𝑒 ∩ π‘Œ)βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† (𝑒 ∩ π‘Œ))
12 inss2 4232 . . . . . . . 8 (𝑒 ∩ π‘Œ) βŠ† π‘Œ
1311, 12jctil 518 . . . . . . 7 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑒 ∈ 𝐽) β†’ ((𝑒 ∩ π‘Œ) βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ (𝑒 ∩ π‘Œ)βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† (𝑒 ∩ π‘Œ)))
14 sseq1 4007 . . . . . . . 8 (π‘₯ = (𝑒 ∩ π‘Œ) β†’ (π‘₯ βŠ† π‘Œ ↔ (𝑒 ∩ π‘Œ) βŠ† π‘Œ))
15 sseq2 4008 . . . . . . . . . 10 (π‘₯ = (𝑒 ∩ π‘Œ) β†’ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ↔ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† (𝑒 ∩ π‘Œ)))
1615rexbidv 3176 . . . . . . . . 9 (π‘₯ = (𝑒 ∩ π‘Œ) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ↔ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† (𝑒 ∩ π‘Œ)))
1716raleqbi1dv 3331 . . . . . . . 8 (π‘₯ = (𝑒 ∩ π‘Œ) β†’ (βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ↔ βˆ€π‘¦ ∈ (𝑒 ∩ π‘Œ)βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† (𝑒 ∩ π‘Œ)))
1814, 17anbi12d 630 . . . . . . 7 (π‘₯ = (𝑒 ∩ π‘Œ) β†’ ((π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯) ↔ ((𝑒 ∩ π‘Œ) βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ (𝑒 ∩ π‘Œ)βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† (𝑒 ∩ π‘Œ))))
1913, 18syl5ibrcom 246 . . . . . 6 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑒 ∈ 𝐽) β†’ (π‘₯ = (𝑒 ∩ π‘Œ) β†’ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)))
2019rexlimdva 3152 . . . . 5 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (βˆƒπ‘’ ∈ 𝐽 π‘₯ = (𝑒 ∩ π‘Œ) β†’ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)))
212mopntop 24366 . . . . . . . . 9 (𝐢 ∈ (∞Metβ€˜π‘‹) β†’ 𝐽 ∈ Top)
2221ad2antrr 724 . . . . . . . 8 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ 𝐽 ∈ Top)
23 ssel2 3977 . . . . . . . . . . . . . 14 ((π‘₯ βŠ† π‘Œ ∧ 𝑦 ∈ π‘₯) β†’ 𝑦 ∈ π‘Œ)
24 ssel2 3977 . . . . . . . . . . . . . . . 16 ((π‘Œ βŠ† 𝑋 ∧ 𝑦 ∈ π‘Œ) β†’ 𝑦 ∈ 𝑋)
25 rpxr 13023 . . . . . . . . . . . . . . . . . 18 (π‘Ÿ ∈ ℝ+ β†’ π‘Ÿ ∈ ℝ*)
262blopn 24429 . . . . . . . . . . . . . . . . . . . 20 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ 𝑋 ∧ π‘Ÿ ∈ ℝ*) β†’ (𝑦(ballβ€˜πΆ)π‘Ÿ) ∈ 𝐽)
27 eleq1a 2824 . . . . . . . . . . . . . . . . . . . 20 ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∈ 𝐽 β†’ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ 𝑧 ∈ 𝐽))
2826, 27syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ 𝑋 ∧ π‘Ÿ ∈ ℝ*) β†’ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ 𝑧 ∈ 𝐽))
29283expa 1115 . . . . . . . . . . . . . . . . . 18 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ 𝑋) ∧ π‘Ÿ ∈ ℝ*) β†’ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ 𝑧 ∈ 𝐽))
3025, 29sylan2 591 . . . . . . . . . . . . . . . . 17 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ 𝑋) ∧ π‘Ÿ ∈ ℝ+) β†’ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ 𝑧 ∈ 𝐽))
3130rexlimdva 3152 . . . . . . . . . . . . . . . 16 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ 𝑋) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ 𝑧 ∈ 𝐽))
3224, 31sylan2 591 . . . . . . . . . . . . . . 15 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑦 ∈ π‘Œ)) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ 𝑧 ∈ 𝐽))
3332anassrs 466 . . . . . . . . . . . . . 14 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑦 ∈ π‘Œ) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ 𝑧 ∈ 𝐽))
3423, 33sylan2 591 . . . . . . . . . . . . 13 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ 𝑦 ∈ π‘₯)) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ 𝑧 ∈ 𝐽))
3534anassrs 466 . . . . . . . . . . . 12 ((((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ 𝑧 ∈ 𝐽))
3635rexlimdva 3152 . . . . . . . . . . 11 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ π‘₯ βŠ† π‘Œ) β†’ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ 𝑧 ∈ 𝐽))
3736adantrd 490 . . . . . . . . . 10 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ π‘₯ βŠ† π‘Œ) β†’ ((βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯) β†’ 𝑧 ∈ 𝐽))
3837adantrr 715 . . . . . . . . 9 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ ((βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯) β†’ 𝑧 ∈ 𝐽))
3938abssdv 4065 . . . . . . . 8 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} βŠ† 𝐽)
40 uniopn 22819 . . . . . . . 8 ((𝐽 ∈ Top ∧ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} βŠ† 𝐽) β†’ βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} ∈ 𝐽)
4122, 39, 40syl2anc 582 . . . . . . 7 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} ∈ 𝐽)
42 oveq1 7433 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑒 β†’ (𝑦(ballβ€˜πΆ)π‘Ÿ) = (𝑒(ballβ€˜πΆ)π‘Ÿ))
4342ineq1d 4213 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑒 β†’ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) = ((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ))
4443sseq1d 4013 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑒 β†’ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ↔ ((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
4544rexbidv 3176 . . . . . . . . . . . . . . 15 (𝑦 = 𝑒 β†’ (βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ↔ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
4645rspccv 3608 . . . . . . . . . . . . . 14 (βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ β†’ (𝑒 ∈ π‘₯ β†’ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
4746ad2antll 727 . . . . . . . . . . . . 13 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ (𝑒 ∈ π‘₯ β†’ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
48 ssel 3975 . . . . . . . . . . . . . . 15 (π‘₯ βŠ† π‘Œ β†’ (𝑒 ∈ π‘₯ β†’ 𝑒 ∈ π‘Œ))
49 ssel 3975 . . . . . . . . . . . . . . . 16 (π‘Œ βŠ† 𝑋 β†’ (𝑒 ∈ π‘Œ β†’ 𝑒 ∈ 𝑋))
50 blcntr 24339 . . . . . . . . . . . . . . . . . . . . 21 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑒 ∈ 𝑋 ∧ π‘Ÿ ∈ ℝ+) β†’ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ))
5150a1d 25 . . . . . . . . . . . . . . . . . . . 20 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑒 ∈ 𝑋 ∧ π‘Ÿ ∈ ℝ+) β†’ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ β†’ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ)))
5251ancld 549 . . . . . . . . . . . . . . . . . . 19 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑒 ∈ 𝑋 ∧ π‘Ÿ ∈ ℝ+) β†’ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ β†’ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ))))
53523expa 1115 . . . . . . . . . . . . . . . . . 18 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑒 ∈ 𝑋) ∧ π‘Ÿ ∈ ℝ+) β†’ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ β†’ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ))))
5453reximdva 3165 . . . . . . . . . . . . . . . . 17 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑒 ∈ 𝑋) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ ((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ β†’ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ))))
5554ex 411 . . . . . . . . . . . . . . . 16 (𝐢 ∈ (∞Metβ€˜π‘‹) β†’ (𝑒 ∈ 𝑋 β†’ (βˆƒπ‘Ÿ ∈ ℝ+ ((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ β†’ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ)))))
5649, 55sylan9r 507 . . . . . . . . . . . . . . 15 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (𝑒 ∈ π‘Œ β†’ (βˆƒπ‘Ÿ ∈ ℝ+ ((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ β†’ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ)))))
5748, 56sylan9r 507 . . . . . . . . . . . . . 14 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ π‘₯ βŠ† π‘Œ) β†’ (𝑒 ∈ π‘₯ β†’ (βˆƒπ‘Ÿ ∈ ℝ+ ((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ β†’ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ)))))
5857adantrr 715 . . . . . . . . . . . . 13 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ (𝑒 ∈ π‘₯ β†’ (βˆƒπ‘Ÿ ∈ ℝ+ ((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ β†’ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ)))))
5947, 58mpdd 43 . . . . . . . . . . . 12 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ (𝑒 ∈ π‘₯ β†’ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ))))
6042eleq2d 2815 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑒 β†’ (𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ) ↔ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ)))
6144, 60anbi12d 630 . . . . . . . . . . . . . . 15 (𝑦 = 𝑒 β†’ ((((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)) ↔ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ))))
6261rexbidv 3176 . . . . . . . . . . . . . 14 (𝑦 = 𝑒 β†’ (βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)) ↔ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ))))
6362rspcev 3611 . . . . . . . . . . . . 13 ((𝑒 ∈ π‘₯ ∧ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ))) β†’ βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)))
6463ex 411 . . . . . . . . . . . 12 (𝑒 ∈ π‘₯ β†’ (βˆƒπ‘Ÿ ∈ ℝ+ (((𝑒(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑒(ballβ€˜πΆ)π‘Ÿ)) β†’ βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ))))
6559, 64sylcom 30 . . . . . . . . . . 11 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ (𝑒 ∈ π‘₯ β†’ βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ))))
66 simprl 769 . . . . . . . . . . . 12 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ π‘₯ βŠ† π‘Œ)
6766sseld 3981 . . . . . . . . . . 11 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ (𝑒 ∈ π‘₯ β†’ 𝑒 ∈ π‘Œ))
6865, 67jcad 511 . . . . . . . . . 10 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ (𝑒 ∈ π‘₯ β†’ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)) ∧ 𝑒 ∈ π‘Œ)))
69 elin 3965 . . . . . . . . . . . . . . 15 (𝑒 ∈ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) ↔ (𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ 𝑒 ∈ π‘Œ))
70 ssel2 3977 . . . . . . . . . . . . . . 15 ((((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ)) β†’ 𝑒 ∈ π‘₯)
7169, 70sylan2br 593 . . . . . . . . . . . . . 14 ((((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ (𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ 𝑒 ∈ π‘Œ)) β†’ 𝑒 ∈ π‘₯)
7271expr 455 . . . . . . . . . . . . 13 ((((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)) β†’ (𝑒 ∈ π‘Œ β†’ 𝑒 ∈ π‘₯))
7372rexlimivw 3148 . . . . . . . . . . . 12 (βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)) β†’ (𝑒 ∈ π‘Œ β†’ 𝑒 ∈ π‘₯))
7473rexlimivw 3148 . . . . . . . . . . 11 (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)) β†’ (𝑒 ∈ π‘Œ β†’ 𝑒 ∈ π‘₯))
7574imp 405 . . . . . . . . . 10 ((βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)) ∧ 𝑒 ∈ π‘Œ) β†’ 𝑒 ∈ π‘₯)
7668, 75impbid1 224 . . . . . . . . 9 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ (𝑒 ∈ π‘₯ ↔ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)) ∧ 𝑒 ∈ π‘Œ)))
77 elin 3965 . . . . . . . . . 10 (𝑒 ∈ (βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} ∩ π‘Œ) ↔ (𝑒 ∈ βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} ∧ 𝑒 ∈ π‘Œ))
78 eluniab 4926 . . . . . . . . . . . 12 (𝑒 ∈ βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} ↔ βˆƒπ‘§(𝑒 ∈ 𝑧 ∧ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)))
79 ancom 459 . . . . . . . . . . . . . 14 ((𝑒 ∈ 𝑧 ∧ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)) ↔ ((βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯) ∧ 𝑒 ∈ 𝑧))
80 anass 467 . . . . . . . . . . . . . 14 (((βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯) ∧ 𝑒 ∈ 𝑧) ↔ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)))
81 r19.41v 3186 . . . . . . . . . . . . . . . 16 (βˆƒπ‘Ÿ ∈ ℝ+ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)) ↔ (βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)))
8281rexbii 3091 . . . . . . . . . . . . . . 15 (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)) ↔ βˆƒπ‘¦ ∈ π‘₯ (βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)))
83 r19.41v 3186 . . . . . . . . . . . . . . 15 (βˆƒπ‘¦ ∈ π‘₯ (βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)) ↔ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)))
8482, 83bitr2i 275 . . . . . . . . . . . . . 14 ((βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)) ↔ βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)))
8579, 80, 843bitri 296 . . . . . . . . . . . . 13 ((𝑒 ∈ 𝑧 ∧ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)) ↔ βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)))
8685exbii 1842 . . . . . . . . . . . 12 (βˆƒπ‘§(𝑒 ∈ 𝑧 ∧ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)) ↔ βˆƒπ‘§βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)))
87 ovex 7459 . . . . . . . . . . . . . . . . 17 (𝑦(ballβ€˜πΆ)π‘Ÿ) ∈ V
88 ineq1 4207 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ (𝑧 ∩ π‘Œ) = ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ))
8988sseq1d 4013 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ↔ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
90 eleq2 2818 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ (𝑒 ∈ 𝑧 ↔ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)))
9189, 90anbi12d 630 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) β†’ (((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧) ↔ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ))))
9287, 91ceqsexv 3525 . . . . . . . . . . . . . . . 16 (βˆƒπ‘§(𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)) ↔ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)))
9392rexbii 3091 . . . . . . . . . . . . . . 15 (βˆƒπ‘Ÿ ∈ ℝ+ βˆƒπ‘§(𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)) ↔ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)))
94 rexcom4 3283 . . . . . . . . . . . . . . 15 (βˆƒπ‘Ÿ ∈ ℝ+ βˆƒπ‘§(𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)) ↔ βˆƒπ‘§βˆƒπ‘Ÿ ∈ ℝ+ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)))
9593, 94bitr3i 276 . . . . . . . . . . . . . 14 (βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)) ↔ βˆƒπ‘§βˆƒπ‘Ÿ ∈ ℝ+ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)))
9695rexbii 3091 . . . . . . . . . . . . 13 (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)) ↔ βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘§βˆƒπ‘Ÿ ∈ ℝ+ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)))
97 rexcom4 3283 . . . . . . . . . . . . 13 (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘§βˆƒπ‘Ÿ ∈ ℝ+ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)) ↔ βˆƒπ‘§βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)))
9896, 97bitr2i 275 . . . . . . . . . . . 12 (βˆƒπ‘§βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ ((𝑧 ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ 𝑧)) ↔ βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)))
9978, 86, 983bitri 296 . . . . . . . . . . 11 (𝑒 ∈ βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} ↔ βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)))
10099anbi1i 622 . . . . . . . . . 10 ((𝑒 ∈ βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} ∧ 𝑒 ∈ π‘Œ) ↔ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)) ∧ 𝑒 ∈ π‘Œ))
10177, 100bitr2i 275 . . . . . . . . 9 ((βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯ ∧ 𝑒 ∈ (𝑦(ballβ€˜πΆ)π‘Ÿ)) ∧ 𝑒 ∈ π‘Œ) ↔ 𝑒 ∈ (βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} ∩ π‘Œ))
10276, 101bitrdi 286 . . . . . . . 8 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ (𝑒 ∈ π‘₯ ↔ 𝑒 ∈ (βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} ∩ π‘Œ)))
103102eqrdv 2726 . . . . . . 7 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ π‘₯ = (βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} ∩ π‘Œ))
104 ineq1 4207 . . . . . . . 8 (𝑒 = βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} β†’ (𝑒 ∩ π‘Œ) = (βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} ∩ π‘Œ))
105104rspceeqv 3633 . . . . . . 7 ((βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} ∈ 𝐽 ∧ π‘₯ = (βˆͺ {𝑧 ∣ (βˆƒπ‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ 𝑧 = (𝑦(ballβ€˜πΆ)π‘Ÿ) ∧ (𝑧 ∩ π‘Œ) βŠ† π‘₯)} ∩ π‘Œ)) β†’ βˆƒπ‘’ ∈ 𝐽 π‘₯ = (𝑒 ∩ π‘Œ))
10641, 103, 105syl2anc 582 . . . . . 6 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)) β†’ βˆƒπ‘’ ∈ 𝐽 π‘₯ = (𝑒 ∩ π‘Œ))
107106ex 411 . . . . 5 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ ((π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯) β†’ βˆƒπ‘’ ∈ 𝐽 π‘₯ = (𝑒 ∩ π‘Œ)))
10820, 107impbid 211 . . . 4 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (βˆƒπ‘’ ∈ 𝐽 π‘₯ = (𝑒 ∩ π‘Œ) ↔ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)))
109 simpr 483 . . . . . . . . . . 11 ((π‘Œ βŠ† 𝑋 ∧ 𝑦 ∈ π‘Œ) β†’ 𝑦 ∈ π‘Œ)
11024, 109elind 4196 . . . . . . . . . 10 ((π‘Œ βŠ† 𝑋 ∧ 𝑦 ∈ π‘Œ) β†’ 𝑦 ∈ (𝑋 ∩ π‘Œ))
111 metrest.1 . . . . . . . . . . . . . . 15 𝐷 = (𝐢 β†Ύ (π‘Œ Γ— π‘Œ))
112111blres 24357 . . . . . . . . . . . . . 14 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ (𝑋 ∩ π‘Œ) ∧ π‘Ÿ ∈ ℝ*) β†’ (𝑦(ballβ€˜π·)π‘Ÿ) = ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ))
113112sseq1d 4013 . . . . . . . . . . . . 13 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ (𝑋 ∩ π‘Œ) ∧ π‘Ÿ ∈ ℝ*) β†’ ((𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯ ↔ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
1141133expa 1115 . . . . . . . . . . . 12 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ (𝑋 ∩ π‘Œ)) ∧ π‘Ÿ ∈ ℝ*) β†’ ((𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯ ↔ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
11525, 114sylan2 591 . . . . . . . . . . 11 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ (𝑋 ∩ π‘Œ)) ∧ π‘Ÿ ∈ ℝ+) β†’ ((𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯ ↔ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
116115rexbidva 3174 . . . . . . . . . 10 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ 𝑦 ∈ (𝑋 ∩ π‘Œ)) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯ ↔ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
117110, 116sylan2 591 . . . . . . . . 9 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ (π‘Œ βŠ† 𝑋 ∧ 𝑦 ∈ π‘Œ)) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯ ↔ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
118117anassrs 466 . . . . . . . 8 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ 𝑦 ∈ π‘Œ) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯ ↔ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
11923, 118sylan2 591 . . . . . . 7 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ (π‘₯ βŠ† π‘Œ ∧ 𝑦 ∈ π‘₯)) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯ ↔ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
120119anassrs 466 . . . . . 6 ((((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ π‘₯ βŠ† π‘Œ) ∧ 𝑦 ∈ π‘₯) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯ ↔ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
121120ralbidva 3173 . . . . 5 (((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) ∧ π‘₯ βŠ† π‘Œ) β†’ (βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯ ↔ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯))
122121pm5.32da 577 . . . 4 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ ((π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯) ↔ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ ((𝑦(ballβ€˜πΆ)π‘Ÿ) ∩ π‘Œ) βŠ† π‘₯)))
123108, 122bitr4d 281 . . 3 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (βˆƒπ‘’ ∈ 𝐽 π‘₯ = (𝑒 ∩ π‘Œ) ↔ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯)))
124 id 22 . . . . 5 (π‘Œ βŠ† 𝑋 β†’ π‘Œ βŠ† 𝑋)
1252mopnm 24370 . . . . 5 (𝐢 ∈ (∞Metβ€˜π‘‹) β†’ 𝑋 ∈ 𝐽)
126 ssexg 5327 . . . . 5 ((π‘Œ βŠ† 𝑋 ∧ 𝑋 ∈ 𝐽) β†’ π‘Œ ∈ V)
127124, 125, 126syl2anr 595 . . . 4 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ π‘Œ ∈ V)
128 elrest 17416 . . . 4 ((𝐽 ∈ Top ∧ π‘Œ ∈ V) β†’ (π‘₯ ∈ (𝐽 β†Ύt π‘Œ) ↔ βˆƒπ‘’ ∈ 𝐽 π‘₯ = (𝑒 ∩ π‘Œ)))
12921, 127, 128syl2an2r 683 . . 3 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (π‘₯ ∈ (𝐽 β†Ύt π‘Œ) ↔ βˆƒπ‘’ ∈ 𝐽 π‘₯ = (𝑒 ∩ π‘Œ)))
130 xmetres2 24287 . . . . 5 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (𝐢 β†Ύ (π‘Œ Γ— π‘Œ)) ∈ (∞Metβ€˜π‘Œ))
131111, 130eqeltrid 2833 . . . 4 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ 𝐷 ∈ (∞Metβ€˜π‘Œ))
132 metrest.4 . . . . 5 𝐾 = (MetOpenβ€˜π·)
133132elmopn2 24371 . . . 4 (𝐷 ∈ (∞Metβ€˜π‘Œ) β†’ (π‘₯ ∈ 𝐾 ↔ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯)))
134131, 133syl 17 . . 3 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (π‘₯ ∈ 𝐾 ↔ (π‘₯ βŠ† π‘Œ ∧ βˆ€π‘¦ ∈ π‘₯ βˆƒπ‘Ÿ ∈ ℝ+ (𝑦(ballβ€˜π·)π‘Ÿ) βŠ† π‘₯)))
135123, 129, 1343bitr4d 310 . 2 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (π‘₯ ∈ (𝐽 β†Ύt π‘Œ) ↔ π‘₯ ∈ 𝐾))
136135eqrdv 2726 1 ((𝐢 ∈ (∞Metβ€˜π‘‹) ∧ π‘Œ βŠ† 𝑋) β†’ (𝐽 β†Ύt π‘Œ) = 𝐾)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1533  βˆƒwex 1773   ∈ wcel 2098  {cab 2705  βˆ€wral 3058  βˆƒwrex 3067  Vcvv 3473   ∩ cin 3948   βŠ† wss 3949  βˆͺ cuni 4912   Γ— cxp 5680   β†Ύ cres 5684  β€˜cfv 6553  (class class class)co 7426  β„*cxr 11285  β„+crp 13014   β†Ύt crest 17409  βˆžMetcxmet 21271  ballcbl 21273  MetOpencmopn 21276  Topctop 22815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223  ax-pre-sup 11224
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7877  df-1st 7999  df-2nd 8000  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-er 8731  df-map 8853  df-en 8971  df-dom 8972  df-sdom 8973  df-sup 9473  df-inf 9474  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-div 11910  df-nn 12251  df-2 12313  df-n0 12511  df-z 12597  df-uz 12861  df-q 12971  df-rp 13015  df-xneg 13132  df-xadd 13133  df-xmul 13134  df-rest 17411  df-topgen 17432  df-psmet 21278  df-xmet 21279  df-bl 21281  df-mopn 21282  df-top 22816  df-topon 22833  df-bases 22869
This theorem is referenced by:  ressxms  24454  nrginvrcn  24629  resubmet  24738  tgioo2  24739  metdscn2  24793  divcnOLD  24804  divcn  24806  dfii3  24823  cncfcn  24850  metsscmetcld  25263  cmetss  25264  minveclem4a  25378  ftc1lem6  25996  ulmdvlem3  26358  abelth  26398  cxpcn3  26703  rlimcnp  26917  minvecolem4b  30708  minvecolem4  30710  hhsscms  31108  ftc1cnnc  37198
  Copyright terms: Public domain W3C validator