ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  metrest GIF version

Theorem metrest 12691
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 3296 . . . . . . . . . 10 (𝑢𝑌) ⊆ 𝑢
2 metrest.3 . . . . . . . . . . . . 13 𝐽 = (MetOpen‘𝐶)
32elmopn2 12634 . . . . . . . . . . . 12 (𝐶 ∈ (∞Met‘𝑋) → (𝑢𝐽 ↔ (𝑢𝑋 ∧ ∀𝑦𝑢𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢)))
43simplbda 381 . . . . . . . . . . 11 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢𝐽) → ∀𝑦𝑢𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢)
54adantlr 468 . . . . . . . . . 10 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑢𝐽) → ∀𝑦𝑢𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢)
6 ssralv 3161 . . . . . . . . . 10 ((𝑢𝑌) ⊆ 𝑢 → (∀𝑦𝑢𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢 → ∀𝑦 ∈ (𝑢𝑌)∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢))
71, 5, 6mpsyl 65 . . . . . . . . 9 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑢𝐽) → ∀𝑦 ∈ (𝑢𝑌)∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢)
8 ssrin 3301 . . . . . . . . . . 11 ((𝑦(ball‘𝐶)𝑟) ⊆ 𝑢 → ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢𝑌))
98reximi 2529 . . . . . . . . . 10 (∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢 → ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢𝑌))
109ralimi 2495 . . . . . . . . 9 (∀𝑦 ∈ (𝑢𝑌)∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢 → ∀𝑦 ∈ (𝑢𝑌)∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢𝑌))
117, 10syl 14 . . . . . . . 8 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑢𝐽) → ∀𝑦 ∈ (𝑢𝑌)∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢𝑌))
12 inss2 3297 . . . . . . . 8 (𝑢𝑌) ⊆ 𝑌
1311, 12jctil 310 . . . . . . 7 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑢𝐽) → ((𝑢𝑌) ⊆ 𝑌 ∧ ∀𝑦 ∈ (𝑢𝑌)∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢𝑌)))
14 sseq1 3120 . . . . . . . 8 (𝑥 = (𝑢𝑌) → (𝑥𝑌 ↔ (𝑢𝑌) ⊆ 𝑌))
15 sseq2 3121 . . . . . . . . . 10 (𝑥 = (𝑢𝑌) → (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢𝑌)))
1615rexbidv 2438 . . . . . . . . 9 (𝑥 = (𝑢𝑌) → (∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢𝑌)))
1716raleqbi1dv 2634 . . . . . . . 8 (𝑥 = (𝑢𝑌) → (∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ∀𝑦 ∈ (𝑢𝑌)∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢𝑌)))
1814, 17anbi12d 464 . . . . . . 7 (𝑥 = (𝑢𝑌) → ((𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥) ↔ ((𝑢𝑌) ⊆ 𝑌 ∧ ∀𝑦 ∈ (𝑢𝑌)∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢𝑌))))
1913, 18syl5ibrcom 156 . . . . . 6 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑢𝐽) → (𝑥 = (𝑢𝑌) → (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)))
2019rexlimdva 2549 . . . . 5 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (∃𝑢𝐽 𝑥 = (𝑢𝑌) → (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)))
212mopntop 12629 . . . . . . . . 9 (𝐶 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
2221ad2antrr 479 . . . . . . . 8 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → 𝐽 ∈ Top)
23 ssel2 3092 . . . . . . . . . . . . . 14 ((𝑥𝑌𝑦𝑥) → 𝑦𝑌)
24 ssel2 3092 . . . . . . . . . . . . . . . 16 ((𝑌𝑋𝑦𝑌) → 𝑦𝑋)
25 rpxr 9463 . . . . . . . . . . . . . . . . . 18 (𝑟 ∈ ℝ+𝑟 ∈ ℝ*)
262blopn 12675 . . . . . . . . . . . . . . . . . . . 20 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦𝑋𝑟 ∈ ℝ*) → (𝑦(ball‘𝐶)𝑟) ∈ 𝐽)
27 eleq1a 2211 . . . . . . . . . . . . . . . . . . . 20 ((𝑦(ball‘𝐶)𝑟) ∈ 𝐽 → (𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧𝐽))
2826, 27syl 14 . . . . . . . . . . . . . . . . . . 19 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦𝑋𝑟 ∈ ℝ*) → (𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧𝐽))
29283expa 1181 . . . . . . . . . . . . . . . . . 18 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦𝑋) ∧ 𝑟 ∈ ℝ*) → (𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧𝐽))
3025, 29sylan2 284 . . . . . . . . . . . . . . . . 17 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧𝐽))
3130rexlimdva 2549 . . . . . . . . . . . . . . . 16 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦𝑋) → (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧𝐽))
3224, 31sylan2 284 . . . . . . . . . . . . . . 15 ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑌𝑋𝑦𝑌)) → (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧𝐽))
3332anassrs 397 . . . . . . . . . . . . . 14 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑦𝑌) → (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧𝐽))
3423, 33sylan2 284 . . . . . . . . . . . . 13 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌𝑦𝑥)) → (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧𝐽))
3534anassrs 397 . . . . . . . . . . . 12 ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑥𝑌) ∧ 𝑦𝑥) → (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧𝐽))
3635rexlimdva 2549 . . . . . . . . . . 11 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑥𝑌) → (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧𝐽))
3736adantrd 277 . . . . . . . . . 10 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑥𝑌) → ((∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥) → 𝑧𝐽))
3837adantrr 470 . . . . . . . . 9 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → ((∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥) → 𝑧𝐽))
3938abssdv 3171 . . . . . . . 8 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ⊆ 𝐽)
40 uniopn 12184 . . . . . . . 8 ((𝐽 ∈ Top ∧ {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ⊆ 𝐽) → {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ∈ 𝐽)
4122, 39, 40syl2anc 408 . . . . . . 7 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ∈ 𝐽)
42 oveq1 5781 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑢 → (𝑦(ball‘𝐶)𝑟) = (𝑢(ball‘𝐶)𝑟))
4342ineq1d 3276 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑢 → ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) = ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌))
4443sseq1d 3126 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑢 → (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
4544rexbidv 2438 . . . . . . . . . . . . . . 15 (𝑦 = 𝑢 → (∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
4645rspccv 2786 . . . . . . . . . . . . . 14 (∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → (𝑢𝑥 → ∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
4746ad2antll 482 . . . . . . . . . . . . 13 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢𝑥 → ∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
48 ssel 3091 . . . . . . . . . . . . . . 15 (𝑥𝑌 → (𝑢𝑥𝑢𝑌))
49 ssel 3091 . . . . . . . . . . . . . . . 16 (𝑌𝑋 → (𝑢𝑌𝑢𝑋))
50 blcntr 12601 . . . . . . . . . . . . . . . . . . . . 21 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢𝑋𝑟 ∈ ℝ+) → 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))
5150a1d 22 . . . . . . . . . . . . . . . . . . . 20 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢𝑋𝑟 ∈ ℝ+) → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))
5251ancld 323 . . . . . . . . . . . . . . . . . . 19 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢𝑋𝑟 ∈ ℝ+) → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
53523expa 1181 . . . . . . . . . . . . . . . . . 18 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢𝑋) ∧ 𝑟 ∈ ℝ+) → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
5453reximdva 2534 . . . . . . . . . . . . . . . . 17 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢𝑋) → (∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
5554ex 114 . . . . . . . . . . . . . . . 16 (𝐶 ∈ (∞Met‘𝑋) → (𝑢𝑋 → (∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))))
5649, 55sylan9r 407 . . . . . . . . . . . . . . 15 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (𝑢𝑌 → (∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))))
5748, 56sylan9r 407 . . . . . . . . . . . . . 14 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑥𝑌) → (𝑢𝑥 → (∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))))
5857adantrr 470 . . . . . . . . . . . . 13 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢𝑥 → (∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))))
5947, 58mpdd 41 . . . . . . . . . . . 12 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢𝑥 → ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
6042eleq2d 2209 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑢 → (𝑢 ∈ (𝑦(ball‘𝐶)𝑟) ↔ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))
6144, 60anbi12d 464 . . . . . . . . . . . . . . 15 (𝑦 = 𝑢 → ((((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ↔ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
6261rexbidv 2438 . . . . . . . . . . . . . 14 (𝑦 = 𝑢 → (∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ↔ ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
6362rspcev 2789 . . . . . . . . . . . . 13 ((𝑢𝑥 ∧ ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑢(ball‘𝐶)𝑟))) → ∃𝑦𝑥𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)))
6463ex 114 . . . . . . . . . . . 12 (𝑢𝑥 → (∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑢(ball‘𝐶)𝑟)) → ∃𝑦𝑥𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
6559, 64sylcom 28 . . . . . . . . . . 11 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢𝑥 → ∃𝑦𝑥𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
66 simprl 520 . . . . . . . . . . . 12 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → 𝑥𝑌)
6766sseld 3096 . . . . . . . . . . 11 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢𝑥𝑢𝑌))
6865, 67jcad 305 . . . . . . . . . 10 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢𝑥 → (∃𝑦𝑥𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢𝑌)))
69 elin 3259 . . . . . . . . . . . . . . 15 (𝑢 ∈ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ↔ (𝑢 ∈ (𝑦(ball‘𝐶)𝑟) ∧ 𝑢𝑌))
70 ssel2 3092 . . . . . . . . . . . . . . 15 ((((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌)) → 𝑢𝑥)
7169, 70sylan2br 286 . . . . . . . . . . . . . 14 ((((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ (𝑢 ∈ (𝑦(ball‘𝐶)𝑟) ∧ 𝑢𝑌)) → 𝑢𝑥)
7271expr 372 . . . . . . . . . . . . 13 ((((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) → (𝑢𝑌𝑢𝑥))
7372rexlimivw 2545 . . . . . . . . . . . 12 (∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) → (𝑢𝑌𝑢𝑥))
7473rexlimivw 2545 . . . . . . . . . . 11 (∃𝑦𝑥𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) → (𝑢𝑌𝑢𝑥))
7574imp 123 . . . . . . . . . 10 ((∃𝑦𝑥𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢𝑌) → 𝑢𝑥)
7668, 75impbid1 141 . . . . . . . . 9 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢𝑥 ↔ (∃𝑦𝑥𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢𝑌)))
77 elin 3259 . . . . . . . . . . 11 (𝑢 ∈ ( {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ∩ 𝑌) ↔ (𝑢 {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ∧ 𝑢𝑌))
78 eluniab 3748 . . . . . . . . . . . . . 14 (𝑢 {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ↔ ∃𝑧(𝑢𝑧 ∧ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)))
79 ancom 264 . . . . . . . . . . . . . . . 16 ((𝑢𝑧 ∧ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)) ↔ ((∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥) ∧ 𝑢𝑧))
80 anass 398 . . . . . . . . . . . . . . . 16 (((∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥) ∧ 𝑢𝑧) ↔ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)))
81 r19.41v 2587 . . . . . . . . . . . . . . . . . 18 (∃𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)) ↔ (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)))
8281rexbii 2442 . . . . . . . . . . . . . . . . 17 (∃𝑦𝑥𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)) ↔ ∃𝑦𝑥 (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)))
83 r19.41v 2587 . . . . . . . . . . . . . . . . 17 (∃𝑦𝑥 (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)) ↔ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)))
8482, 83bitr2i 184 . . . . . . . . . . . . . . . 16 ((∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)) ↔ ∃𝑦𝑥𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)))
8579, 80, 843bitri 205 . . . . . . . . . . . . . . 15 ((𝑢𝑧 ∧ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)) ↔ ∃𝑦𝑥𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)))
8685exbii 1584 . . . . . . . . . . . . . 14 (∃𝑧(𝑢𝑧 ∧ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)) ↔ ∃𝑧𝑦𝑥𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)))
8778, 86bitri 183 . . . . . . . . . . . . 13 (𝑢 {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ↔ ∃𝑧𝑦𝑥𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)))
88 vex 2689 . . . . . . . . . . . . . . . . . . 19 𝑦 ∈ V
89 blex 12572 . . . . . . . . . . . . . . . . . . 19 (𝐶 ∈ (∞Met‘𝑋) → (ball‘𝐶) ∈ V)
90 vex 2689 . . . . . . . . . . . . . . . . . . . 20 𝑟 ∈ V
9190a1i 9 . . . . . . . . . . . . . . . . . . 19 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → 𝑟 ∈ V)
92 ovexg 5805 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ V ∧ (ball‘𝐶) ∈ V ∧ 𝑟 ∈ V) → (𝑦(ball‘𝐶)𝑟) ∈ V)
9388, 89, 91, 92mp3an2ani 1322 . . . . . . . . . . . . . . . . . 18 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (𝑦(ball‘𝐶)𝑟) ∈ V)
94 ineq1 3270 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = (𝑦(ball‘𝐶)𝑟) → (𝑧𝑌) = ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌))
9594sseq1d 3126 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝑦(ball‘𝐶)𝑟) → ((𝑧𝑌) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
96 eleq2 2203 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = (𝑦(ball‘𝐶)𝑟) → (𝑢𝑧𝑢 ∈ (𝑦(ball‘𝐶)𝑟)))
9795, 96anbi12d 464 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑦(ball‘𝐶)𝑟) → (((𝑧𝑌) ⊆ 𝑥𝑢𝑧) ↔ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
9897ceqsexgv 2814 . . . . . . . . . . . . . . . . . 18 ((𝑦(ball‘𝐶)𝑟) ∈ V → (∃𝑧(𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)) ↔ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
9993, 98syl 14 . . . . . . . . . . . . . . . . 17 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (∃𝑧(𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)) ↔ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
10099rexbidv 2438 . . . . . . . . . . . . . . . 16 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (∃𝑟 ∈ ℝ+𝑧(𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)) ↔ ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
101 rexcom4 2709 . . . . . . . . . . . . . . . 16 (∃𝑟 ∈ ℝ+𝑧(𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)) ↔ ∃𝑧𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)))
102100, 101bitr3di 194 . . . . . . . . . . . . . . 15 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ↔ ∃𝑧𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧))))
103102rexbidv 2438 . . . . . . . . . . . . . 14 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (∃𝑦𝑥𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ↔ ∃𝑦𝑥𝑧𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧))))
104 rexcom4 2709 . . . . . . . . . . . . . 14 (∃𝑦𝑥𝑧𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)) ↔ ∃𝑧𝑦𝑥𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)))
105103, 104syl6rbb 196 . . . . . . . . . . . . 13 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (∃𝑧𝑦𝑥𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧𝑌) ⊆ 𝑥𝑢𝑧)) ↔ ∃𝑦𝑥𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
10687, 105syl5bb 191 . . . . . . . . . . . 12 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (𝑢 {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ↔ ∃𝑦𝑥𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
107106anbi1d 460 . . . . . . . . . . 11 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → ((𝑢 {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ∧ 𝑢𝑌) ↔ (∃𝑦𝑥𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢𝑌)))
10877, 107syl5rbb 192 . . . . . . . . . 10 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → ((∃𝑦𝑥𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢𝑌) ↔ 𝑢 ∈ ( {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ∩ 𝑌)))
109108adantr 274 . . . . . . . . 9 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → ((∃𝑦𝑥𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢𝑌) ↔ 𝑢 ∈ ( {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ∩ 𝑌)))
11076, 109bitrd 187 . . . . . . . 8 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢𝑥𝑢 ∈ ( {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ∩ 𝑌)))
111110eqrdv 2137 . . . . . . 7 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → 𝑥 = ( {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ∩ 𝑌))
112 ineq1 3270 . . . . . . . 8 (𝑢 = {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} → (𝑢𝑌) = ( {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ∩ 𝑌))
113112rspceeqv 2807 . . . . . . 7 (( {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ∈ 𝐽𝑥 = ( {𝑧 ∣ (∃𝑦𝑥𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧𝑌) ⊆ 𝑥)} ∩ 𝑌)) → ∃𝑢𝐽 𝑥 = (𝑢𝑌))
11441, 111, 113syl2anc 408 . . . . . 6 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → ∃𝑢𝐽 𝑥 = (𝑢𝑌))
115114ex 114 . . . . 5 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → ((𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥) → ∃𝑢𝐽 𝑥 = (𝑢𝑌)))
11620, 115impbid 128 . . . 4 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (∃𝑢𝐽 𝑥 = (𝑢𝑌) ↔ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)))
117 simpr 109 . . . . . . . . . . 11 ((𝑌𝑋𝑦𝑌) → 𝑦𝑌)
11824, 117elind 3261 . . . . . . . . . 10 ((𝑌𝑋𝑦𝑌) → 𝑦 ∈ (𝑋𝑌))
119 metrest.1 . . . . . . . . . . . . . . 15 𝐷 = (𝐶 ↾ (𝑌 × 𝑌))
120119blres 12619 . . . . . . . . . . . . . 14 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋𝑌) ∧ 𝑟 ∈ ℝ*) → (𝑦(ball‘𝐷)𝑟) = ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌))
121120sseq1d 3126 . . . . . . . . . . . . 13 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋𝑌) ∧ 𝑟 ∈ ℝ*) → ((𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
1221213expa 1181 . . . . . . . . . . . 12 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋𝑌)) ∧ 𝑟 ∈ ℝ*) → ((𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
12325, 122sylan2 284 . . . . . . . . . . 11 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋𝑌)) ∧ 𝑟 ∈ ℝ+) → ((𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
124123rexbidva 2434 . . . . . . . . . 10 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋𝑌)) → (∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
125118, 124sylan2 284 . . . . . . . . 9 ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑌𝑋𝑦𝑌)) → (∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
126125anassrs 397 . . . . . . . 8 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑦𝑌) → (∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
12723, 126sylan2 284 . . . . . . 7 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ (𝑥𝑌𝑦𝑥)) → (∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
128127anassrs 397 . . . . . 6 ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑥𝑌) ∧ 𝑦𝑥) → (∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
129128ralbidva 2433 . . . . 5 (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) ∧ 𝑥𝑌) → (∀𝑦𝑥𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
130129pm5.32da 447 . . . 4 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → ((𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥) ↔ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)))
131116, 130bitr4d 190 . . 3 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (∃𝑢𝐽 𝑥 = (𝑢𝑌) ↔ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)))
13221adantr 274 . . . 4 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → 𝐽 ∈ Top)
133 id 19 . . . . 5 (𝑌𝑋𝑌𝑋)
1342mopnm 12633 . . . . 5 (𝐶 ∈ (∞Met‘𝑋) → 𝑋𝐽)
135 ssexg 4067 . . . . 5 ((𝑌𝑋𝑋𝐽) → 𝑌 ∈ V)
136133, 134, 135syl2anr 288 . . . 4 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → 𝑌 ∈ V)
137 elrest 12143 . . . 4 ((𝐽 ∈ Top ∧ 𝑌 ∈ V) → (𝑥 ∈ (𝐽t 𝑌) ↔ ∃𝑢𝐽 𝑥 = (𝑢𝑌)))
138132, 136, 137syl2anc 408 . . 3 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (𝑥 ∈ (𝐽t 𝑌) ↔ ∃𝑢𝐽 𝑥 = (𝑢𝑌)))
139 xmetres2 12564 . . . . 5 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (𝐶 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌))
140119, 139eqeltrid 2226 . . . 4 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → 𝐷 ∈ (∞Met‘𝑌))
141 metrest.4 . . . . 5 𝐾 = (MetOpen‘𝐷)
142141elmopn2 12634 . . . 4 (𝐷 ∈ (∞Met‘𝑌) → (𝑥𝐾 ↔ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)))
143140, 142syl 14 . . 3 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (𝑥𝐾 ↔ (𝑥𝑌 ∧ ∀𝑦𝑥𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)))
144131, 138, 1433bitr4d 219 . 2 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (𝑥 ∈ (𝐽t 𝑌) ↔ 𝑥𝐾))
145144eqrdv 2137 1 ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (𝐽t 𝑌) = 𝐾)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  w3a 962   = wceq 1331  wex 1468  wcel 1480  {cab 2125  wral 2416  wrex 2417  Vcvv 2686  cin 3070  wss 3071   cuni 3736   × cxp 4537  cres 4541  cfv 5123  (class class class)co 5774  *cxr 7813  +crp 9455  t crest 12136  ∞Metcxmet 12165  ballcbl 12167  MetOpencmopn 12170  Topctop 12180
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502  ax-cnex 7725  ax-resscn 7726  ax-1cn 7727  ax-1re 7728  ax-icn 7729  ax-addcl 7730  ax-addrcl 7731  ax-mulcl 7732  ax-mulrcl 7733  ax-addcom 7734  ax-mulcom 7735  ax-addass 7736  ax-mulass 7737  ax-distr 7738  ax-i2m1 7739  ax-0lt1 7740  ax-1rid 7741  ax-0id 7742  ax-rnegex 7743  ax-precex 7744  ax-cnre 7745  ax-pre-ltirr 7746  ax-pre-ltwlin 7747  ax-pre-lttrn 7748  ax-pre-apti 7749  ax-pre-ltadd 7750  ax-pre-mulgt0 7751  ax-pre-mulext 7752  ax-arch 7753  ax-caucvg 7754
This theorem depends on definitions:  df-bi 116  df-stab 816  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rmo 2424  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-if 3475  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-po 4218  df-iso 4219  df-iord 4288  df-on 4290  df-ilim 4291  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-isom 5132  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-frec 6288  df-map 6544  df-sup 6871  df-inf 6872  df-pnf 7816  df-mnf 7817  df-xr 7818  df-ltxr 7819  df-le 7820  df-sub 7949  df-neg 7950  df-reap 8351  df-ap 8358  df-div 8447  df-inn 8735  df-2 8793  df-3 8794  df-4 8795  df-n0 8992  df-z 9069  df-uz 9341  df-q 9426  df-rp 9456  df-xneg 9573  df-xadd 9574  df-seqfrec 10233  df-exp 10307  df-cj 10628  df-re 10629  df-im 10630  df-rsqrt 10784  df-abs 10785  df-rest 12138  df-topgen 12157  df-psmet 12172  df-xmet 12173  df-bl 12175  df-mopn 12176  df-top 12181  df-topon 12194  df-bases 12226
This theorem is referenced by:  resubmet  12733  tgioo2cntop  12734  divcnap  12740  cncfcncntop  12765  limcimolemlt  12818  cnplimcim  12821  cnplimclemr  12823  limccnpcntop  12829  limccnp2cntop  12831
  Copyright terms: Public domain W3C validator