Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  metrest Structured version   Visualization version   GIF version

Theorem metrest 23134
 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 4158 . . . . . . . . . 10 (𝑢𝑌) ⊆ 𝑢
2 metrest.3 . . . . . . . . . . . . 13 𝐽 = (MetOpen‘𝐶)
32elmopn2 23055 . . . . . . . . . . . 12 (𝐶 ∈ (∞Met‘𝑋) → (𝑢𝐽 ↔ (𝑢𝑋 ∧ ∀𝑦𝑢𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢)))
43simplbda 503 . . . . . . . . . . 11 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢𝐽) → ∀𝑦𝑢𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢)
54adantlr 714 . . . . . . . . . 10 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑢𝐽) → ∀𝑦𝑢𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢)
6 ssralv 3984 . . . . . . . . . 10 ((𝑢𝑌) ⊆ 𝑢 → (∀𝑦𝑢𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢 → ∀𝑦 ∈ (𝑢𝑌)∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢))
71, 5, 6mpsyl 68 . . . . . . . . 9 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑢𝐽) → ∀𝑦 ∈ (𝑢𝑌)∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢)
8 ssrin 4163 . . . . . . . . . . 11 ((𝑦(ball‘𝐶)𝑟) ⊆ 𝑢 → ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢𝑌))
98reximi 3209 . . . . . . . . . 10 (∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢 → ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢𝑌))
109ralimi 3131 . . . . . . . . 9 (∀𝑦 ∈ (𝑢𝑌)∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢 → ∀𝑦 ∈ (𝑢𝑌)∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢𝑌))
117, 10syl 17 . . . . . . . 8 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑢𝐽) → ∀𝑦 ∈ (𝑢𝑌)∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢𝑌))
12 inss2 4159 . . . . . . . 8 (𝑢𝑌) ⊆ 𝑌
1311, 12jctil 523 . . . . . . 7 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑢𝐽) → ((𝑢𝑌) ⊆ 𝑌 ∧ ∀𝑦 ∈ (𝑢𝑌)∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢𝑌)))
14 sseq1 3943 . . . . . . . 8 (𝑥 = (𝑢𝑌) → (𝑥𝑌 ↔ (𝑢𝑌) ⊆ 𝑌))
15 sseq2 3944 . . . . . . . . . 10 (𝑥 = (𝑢𝑌) → (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢𝑌)))
1615rexbidv 3259 . . . . . . . . 9 (𝑥 = (𝑢𝑌) → (∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢𝑌)))
1716raleqbi1dv 3359 . . . . . . . 8 (𝑥 = (𝑢𝑌) → (∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ∀𝑦 ∈ (𝑢𝑌)∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢𝑌)))
1814, 17anbi12d 633 . . . . . . 7 (𝑥 = (𝑢𝑌) → ((𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥) ↔ ((𝑢𝑌) ⊆ 𝑌 ∧ ∀𝑦 ∈ (𝑢𝑌)∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢𝑌))))
1913, 18syl5ibrcom 250 . . . . . 6 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑢𝐽) → (𝑥 = (𝑢𝑌) → (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)))
2019rexlimdva 3246 . . . . 5 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (∃𝑢𝐽 𝑥 = (𝑢𝑌) → (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)))
212mopntop 23050 . . . . . . . . 9 (𝐶 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
2221ad2antrr 725 . . . . . . . 8 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → 𝐽 ∈ Top)
23 ssel2 3913 . . . . . . . . . . . . . 14 ((𝑥𝑌𝑦𝑥) → 𝑦𝑌)
24 ssel2 3913 . . . . . . . . . . . . . . . 16 ((𝑌𝑋𝑦𝑌) → 𝑦𝑋)
25 rpxr 12390 . . . . . . . . . . . . . . . . . 18 (𝑟 ∈ ℝ+𝑟 ∈ ℝ*)
262blopn 23110 . . . . . . . . . . . . . . . . . . . 20 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦𝑋𝑟 ∈ ℝ*) → (𝑦(ball‘𝐶)𝑟) ∈ 𝐽)
27 eleq1a 2888 . . . . . . . . . . . . . . . . . . . 20 ((𝑦(ball‘𝐶)𝑟) ∈ 𝐽 → (𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧𝐽))
2826, 27syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦𝑋𝑟 ∈ ℝ*) → (𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧𝐽))
29283expa 1115 . . . . . . . . . . . . . . . . . 18 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦𝑋) ∧ 𝑟 ∈ ℝ*) → (𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧𝐽))
3025, 29sylan2 595 . . . . . . . . . . . . . . . . 17 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧𝐽))
3130rexlimdva 3246 . . . . . . . . . . . . . . . 16 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦𝑋) → (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧𝐽))
3224, 31sylan2 595 . . . . . . . . . . . . . . 15 ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑌𝑋𝑦𝑌)) → (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧𝐽))
3332anassrs 471 . . . . . . . . . . . . . 14 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑦𝑌) → (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧𝐽))
3423, 33sylan2 595 . . . . . . . . . . . . 13 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌𝑦𝑥)) → (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧𝐽))
3534anassrs 471 . . . . . . . . . . . 12 ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑥𝑌) ∧ 𝑦𝑥) → (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧𝐽))
3635rexlimdva 3246 . . . . . . . . . . 11 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑥𝑌) → (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧𝐽))
3736adantrd 495 . . . . . . . . . 10 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑥𝑌) → ((∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥) → 𝑧𝐽))
3837adantrr 716 . . . . . . . . 9 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → ((∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥) → 𝑧𝐽))
3938abssdv 3999 . . . . . . . 8 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ⊆ 𝐽)
40 uniopn 21505 . . . . . . . 8 ((𝐽 ∈ Top ∧ {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ⊆ 𝐽) → {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ∈ 𝐽)
4122, 39, 40syl2anc 587 . . . . . . 7 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ∈ 𝐽)
42 oveq1 7146 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑢 → (𝑦(ball‘𝐶)𝑟) = (𝑢(ball‘𝐶)𝑟))
4342ineq1d 4141 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑢 → ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) = ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌))
4443sseq1d 3949 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑢 → (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
4544rexbidv 3259 . . . . . . . . . . . . . . 15 (𝑦 = 𝑢 → (∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
4645rspccv 3571 . . . . . . . . . . . . . 14 (∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → (𝑢𝑥 → ∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
4746ad2antll 728 . . . . . . . . . . . . 13 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢𝑥 → ∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
48 ssel 3911 . . . . . . . . . . . . . . 15 (𝑥𝑌 → (𝑢𝑥𝑢𝑌))
49 ssel 3911 . . . . . . . . . . . . . . . 16 (𝑌𝑋 → (𝑢𝑌𝑢𝑋))
50 blcntr 23023 . . . . . . . . . . . . . . . . . . . . 21 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢𝑋𝑟 ∈ ℝ+) → 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))
5150a1d 25 . . . . . . . . . . . . . . . . . . . 20 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢𝑋𝑟 ∈ ℝ+) → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))
5251ancld 554 . . . . . . . . . . . . . . . . . . 19 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢𝑋𝑟 ∈ ℝ+) → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
53523expa 1115 . . . . . . . . . . . . . . . . . 18 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢𝑋) ∧ 𝑟 ∈ ℝ+) → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
5453reximdva 3236 . . . . . . . . . . . . . . . . 17 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢𝑋) → (∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
5554ex 416 . . . . . . . . . . . . . . . 16 (𝐶 ∈ (∞Met‘𝑋) → (𝑢𝑋 → (∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))))
5649, 55sylan9r 512 . . . . . . . . . . . . . . 15 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (𝑢𝑌 → (∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))))
5748, 56sylan9r 512 . . . . . . . . . . . . . 14 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑥𝑌) → (𝑢𝑥 → (∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))))
5857adantrr 716 . . . . . . . . . . . . 13 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢𝑥 → (∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))))
5947, 58mpdd 43 . . . . . . . . . . . 12 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢𝑥 → ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
6042eleq2d 2878 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑢 → (𝑢 ∈ (𝑦(ball‘𝐶)𝑟) ↔ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))
6144, 60anbi12d 633 . . . . . . . . . . . . . . 15 (𝑦 = 𝑢 → ((((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ↔ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
6261rexbidv 3259 . . . . . . . . . . . . . 14 (𝑦 = 𝑢 → (∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ↔ ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
6362rspcev 3574 . . . . . . . . . . . . 13 ((𝑢𝑥 ∧ ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑢(ball‘𝐶)𝑟))) → ∃𝑦𝑥𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)))
6463ex 416 . . . . . . . . . . . 12 (𝑢𝑥 → (∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑢(ball‘𝐶)𝑟)) → ∃𝑦𝑥𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
6559, 64sylcom 30 . . . . . . . . . . 11 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢𝑥 → ∃𝑦𝑥𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
66 simprl 770 . . . . . . . . . . . 12 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → 𝑥𝑌)
6766sseld 3917 . . . . . . . . . . 11 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢𝑥𝑢𝑌))
6865, 67jcad 516 . . . . . . . . . 10 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢𝑥 → (∃𝑦𝑥𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢𝑌)))
69 elin 3900 . . . . . . . . . . . . . . 15 (𝑢 ∈ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ↔ (𝑢 ∈ (𝑦(ball‘𝐶)𝑟) ∧ 𝑢𝑌))
70 ssel2 3913 . . . . . . . . . . . . . . 15 ((((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌)) → 𝑢𝑥)
7169, 70sylan2br 597 . . . . . . . . . . . . . 14 ((((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ (𝑢 ∈ (𝑦(ball‘𝐶)𝑟) ∧ 𝑢𝑌)) → 𝑢𝑥)
7271expr 460 . . . . . . . . . . . . 13 ((((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) → (𝑢𝑌𝑢𝑥))
7372rexlimivw 3244 . . . . . . . . . . . 12 (∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) → (𝑢𝑌𝑢𝑥))
7473rexlimivw 3244 . . . . . . . . . . 11 (∃𝑦𝑥𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) → (𝑢𝑌𝑢𝑥))
7574imp 410 . . . . . . . . . 10 ((∃𝑦𝑥𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢𝑌) → 𝑢𝑥)
7668, 75impbid1 228 . . . . . . . . 9 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢𝑥 ↔ (∃𝑦𝑥𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢𝑌)))
77 elin 3900 . . . . . . . . . 10 (𝑢 ∈ ( {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ∩ 𝑌) ↔ (𝑢 {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ∧ 𝑢𝑌))
78 eluniab 4818 . . . . . . . . . . . 12 (𝑢 {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ↔ ∃𝑧(𝑢𝑧 ∧ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)))
79 ancom 464 . . . . . . . . . . . . . 14 ((𝑢𝑧 ∧ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)) ↔ ((∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥) ∧ 𝑢𝑧))
80 anass 472 . . . . . . . . . . . . . 14 (((∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥) ∧ 𝑢𝑧) ↔ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)))
81 r19.41v 3303 . . . . . . . . . . . . . . . 16 (∃𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)) ↔ (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)))
8281rexbii 3213 . . . . . . . . . . . . . . 15 (∃𝑦𝑥𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)) ↔ ∃𝑦𝑥 (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)))
83 r19.41v 3303 . . . . . . . . . . . . . . 15 (∃𝑦𝑥 (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)) ↔ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)))
8482, 83bitr2i 279 . . . . . . . . . . . . . 14 ((∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)) ↔ ∃𝑦𝑥𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)))
8579, 80, 843bitri 300 . . . . . . . . . . . . 13 ((𝑢𝑧 ∧ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)) ↔ ∃𝑦𝑥𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)))
8685exbii 1849 . . . . . . . . . . . 12 (∃𝑧(𝑢𝑧 ∧ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)) ↔ ∃𝑧𝑦𝑥𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)))
87 ovex 7172 . . . . . . . . . . . . . . . . 17 (𝑦(ball‘𝐶)𝑟) ∈ V
88 ineq1 4134 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑦(ball‘𝐶)𝑟) → (𝑧𝑌) = ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌))
8988sseq1d 3949 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑦(ball‘𝐶)𝑟) → ((𝑧𝑌) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
90 eleq2 2881 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑦(ball‘𝐶)𝑟) → (𝑢𝑧𝑢 ∈ (𝑦(ball‘𝐶)𝑟)))
9189, 90anbi12d 633 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑦(ball‘𝐶)𝑟) → (((𝑧𝑌) ⊆ 𝑥𝑢𝑧) ↔ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
9287, 91ceqsexv 3492 . . . . . . . . . . . . . . . 16 (∃𝑧(𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)) ↔ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)))
9392rexbii 3213 . . . . . . . . . . . . . . 15 (∃𝑟 ∈ ℝ+𝑧(𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)) ↔ ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)))
94 rexcom4 3215 . . . . . . . . . . . . . . 15 (∃𝑟 ∈ ℝ+𝑧(𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)) ↔ ∃𝑧𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)))
9593, 94bitr3i 280 . . . . . . . . . . . . . 14 (∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ↔ ∃𝑧𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)))
9695rexbii 3213 . . . . . . . . . . . . 13 (∃𝑦𝑥𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ↔ ∃𝑦𝑥𝑧𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)))
97 rexcom4 3215 . . . . . . . . . . . . 13 (∃𝑦𝑥𝑧𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)) ↔ ∃𝑧𝑦𝑥𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)))
9896, 97bitr2i 279 . . . . . . . . . . . 12 (∃𝑧𝑦𝑥𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)) ↔ ∃𝑦𝑥𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)))
9978, 86, 983bitri 300 . . . . . . . . . . 11 (𝑢 {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ↔ ∃𝑦𝑥𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)))
10099anbi1i 626 . . . . . . . . . 10 ((𝑢 {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ∧ 𝑢𝑌) ↔ (∃𝑦𝑥𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢𝑌))
10177, 100bitr2i 279 . . . . . . . . 9 ((∃𝑦𝑥𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢𝑌) ↔ 𝑢 ∈ ( {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ∩ 𝑌))
10276, 101syl6bb 290 . . . . . . . 8 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢𝑥𝑢 ∈ ( {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ∩ 𝑌)))
103102eqrdv 2799 . . . . . . 7 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → 𝑥 = ( {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ∩ 𝑌))
104 ineq1 4134 . . . . . . . 8 (𝑢 = {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} → (𝑢𝑌) = ( {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ∩ 𝑌))
105104rspceeqv 3589 . . . . . . 7 (( {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ∈ 𝐽𝑥 = ( {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ∩ 𝑌)) → ∃𝑢𝐽 𝑥 = (𝑢𝑌))
10641, 103, 105syl2anc 587 . . . . . 6 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → ∃𝑢𝐽 𝑥 = (𝑢𝑌))
107106ex 416 . . . . 5 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → ((𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥) → ∃𝑢𝐽 𝑥 = (𝑢𝑌)))
10820, 107impbid 215 . . . 4 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (∃𝑢𝐽 𝑥 = (𝑢𝑌) ↔ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)))
109 simpr 488 . . . . . . . . . . 11 ((𝑌𝑋𝑦𝑌) → 𝑦𝑌)
11024, 109elind 4124 . . . . . . . . . 10 ((𝑌𝑋𝑦𝑌) → 𝑦 ∈ (𝑋𝑌))
111 metrest.1 . . . . . . . . . . . . . . 15 𝐷 = (𝐶 ↾ (𝑌 × 𝑌))
112111blres 23041 . . . . . . . . . . . . . 14 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋𝑌) ∧ 𝑟 ∈ ℝ*) → (𝑦(ball‘𝐷)𝑟) = ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌))
113112sseq1d 3949 . . . . . . . . . . . . 13 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋𝑌) ∧ 𝑟 ∈ ℝ*) → ((𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
1141133expa 1115 . . . . . . . . . . . 12 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋𝑌)) ∧ 𝑟 ∈ ℝ*) → ((𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
11525, 114sylan2 595 . . . . . . . . . . 11 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋𝑌)) ∧ 𝑟 ∈ ℝ+) → ((𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
116115rexbidva 3258 . . . . . . . . . 10 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋𝑌)) → (∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
117110, 116sylan2 595 . . . . . . . . 9 ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑌𝑋𝑦𝑌)) → (∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
118117anassrs 471 . . . . . . . 8 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑦𝑌) → (∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
11923, 118sylan2 595 . . . . . . 7 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌𝑦𝑥)) → (∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
120119anassrs 471 . . . . . 6 ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑥𝑌) ∧ 𝑦𝑥) → (∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
121120ralbidva 3164 . . . . 5 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑥𝑌) → (∀𝑦𝑥𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
122121pm5.32da 582 . . . 4 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → ((𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥) ↔ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)))
123108, 122bitr4d 285 . . 3 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (∃𝑢𝐽 𝑥 = (𝑢𝑌) ↔ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)))
124 id 22 . . . . 5 (𝑌𝑋𝑌𝑋)
1252mopnm 23054 . . . . 5 (𝐶 ∈ (∞Met‘𝑋) → 𝑋𝐽)
126 ssexg 5194 . . . . 5 ((𝑌𝑋𝑋𝐽) → 𝑌 ∈ V)
127124, 125, 126syl2anr 599 . . . 4 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → 𝑌 ∈ V)
128 elrest 16696 . . . 4 ((𝐽 ∈ Top ∧ 𝑌 ∈ V) → (𝑥 ∈ (𝐽t 𝑌) ↔ ∃𝑢𝐽 𝑥 = (𝑢𝑌)))
12921, 127, 128syl2an2r 684 . . 3 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (𝑥 ∈ (𝐽t 𝑌) ↔ ∃𝑢𝐽 𝑥 = (𝑢𝑌)))
130 xmetres2 22971 . . . . 5 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (𝐶 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌))
131111, 130eqeltrid 2897 . . . 4 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → 𝐷 ∈ (∞Met‘𝑌))
132 metrest.4 . . . . 5 𝐾 = (MetOpen‘𝐷)
133132elmopn2 23055 . . . 4 (𝐷 ∈ (∞Met‘𝑌) → (𝑥𝐾 ↔ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)))
134131, 133syl 17 . . 3 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (𝑥𝐾 ↔ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)))
135123, 129, 1343bitr4d 314 . 2 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (𝑥 ∈ (𝐽t 𝑌) ↔ 𝑥𝐾))
136135eqrdv 2799 1 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (𝐽t 𝑌) = 𝐾)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2112  {cab 2779  ∀wral 3109  ∃wrex 3110  Vcvv 3444   ∩ cin 3883   ⊆ wss 3884  ∪ cuni 4803   × cxp 5521   ↾ cres 5525  ‘cfv 6328  (class class class)co 7139  ℝ*cxr 10667  ℝ+crp 12381   ↾t crest 16689  ∞Metcxmet 20079  ballcbl 20081  MetOpencmopn 20084  Topctop 21501 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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607  ax-pre-sup 10608 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-er 8276  df-map 8395  df-en 8497  df-dom 8498  df-sdom 8499  df-sup 8894  df-inf 8895  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-div 11291  df-nn 11630  df-2 11692  df-n0 11890  df-z 11974  df-uz 12236  df-q 12341  df-rp 12382  df-xneg 12499  df-xadd 12500  df-xmul 12501  df-rest 16691  df-topgen 16712  df-psmet 20086  df-xmet 20087  df-bl 20089  df-mopn 20090  df-top 21502  df-topon 21519  df-bases 21554 This theorem is referenced by:  ressxms  23135  nrginvrcn  23301  resubmet  23410  tgioo2  23411  metdscn2  23465  divcn  23476  dfii3  23491  cncfcn  23518  metsscmetcld  23922  cmetss  23923  minveclem4a  24037  ftc1lem6  24647  ulmdvlem3  25000  abelth  25039  cxpcn3  25340  rlimcnp  25554  minvecolem4b  28664  minvecolem4  28666  hhsscms  29064  ftc1cnnc  35122
 Copyright terms: Public domain W3C validator