Theorem metrest 14826

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.

Step	Hyp	Ref	Expression
1		inss1 3384	. . . . . . . . . 10 ⊢ (𝑢 ∩ 𝑌) ⊆ 𝑢
2		metrest.3	. . . . . . . . . . . . 13 ⊢ 𝐽 = (MetOpen‘𝐶)
3	2	elmopn2 14769	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ (∞Met‘𝑋) → (𝑢 ∈ 𝐽 ↔ (𝑢 ⊆ 𝑋 ∧ ∀𝑦 ∈ 𝑢 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢)))
4	3	simplbda 384	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝐽) → ∀𝑦 ∈ 𝑢 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢)
5	4	adantlr 477	. . . . . . . . . 10 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑢 ∈ 𝐽) → ∀𝑦 ∈ 𝑢 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢)
6		ssralv 3248	. . . . . . . . . 10 ⊢ ((𝑢 ∩ 𝑌) ⊆ 𝑢 → (∀𝑦 ∈ 𝑢 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢 → ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢))
7	1, 5, 6	mpsyl 65	. . . . . . . . 9 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑢 ∈ 𝐽) → ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢)
8		ssrin 3389	. . . . . . . . . . 11 ⊢ ((𝑦(ball‘𝐶)𝑟) ⊆ 𝑢 → ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌))
9	8	reximi 2594	. . . . . . . . . 10 ⊢ (∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢 → ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌))
10	9	ralimi 2560	. . . . . . . . 9 ⊢ (∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢 → ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌))
11	7, 10	syl 14	. . . . . . . 8 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑢 ∈ 𝐽) → ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌))
12		inss2 3385	. . . . . . . 8 ⊢ (𝑢 ∩ 𝑌) ⊆ 𝑌
13	11, 12	jctil 312	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑢 ∈ 𝐽) → ((𝑢 ∩ 𝑌) ⊆ 𝑌 ∧ ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌)))
14		sseq1 3207	. . . . . . . 8 ⊢ (𝑥 = (𝑢 ∩ 𝑌) → (𝑥 ⊆ 𝑌 ↔ (𝑢 ∩ 𝑌) ⊆ 𝑌))
15		sseq2 3208	. . . . . . . . . 10 ⊢ (𝑥 = (𝑢 ∩ 𝑌) → (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌)))
16	15	rexbidv 2498	. . . . . . . . 9 ⊢ (𝑥 = (𝑢 ∩ 𝑌) → (∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌)))
17	16	raleqbi1dv 2705	. . . . . . . 8 ⊢ (𝑥 = (𝑢 ∩ 𝑌) → (∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌)))
18	14, 17	anbi12d 473	. . . . . . 7 ⊢ (𝑥 = (𝑢 ∩ 𝑌) → ((𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥) ↔ ((𝑢 ∩ 𝑌) ⊆ 𝑌 ∧ ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌))))
19	13, 18	syl5ibrcom 157	. . . . . 6 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑢 ∈ 𝐽) → (𝑥 = (𝑢 ∩ 𝑌) → (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)))
20	19	rexlimdva 2614	. . . . 5 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌) → (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)))
21	2	mopntop 14764	. . . . . . . . 9 ⊢ (𝐶 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
22	21	ad2antrr 488	. . . . . . . 8 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → 𝐽 ∈ Top)
23		ssel2 3179	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ⊆ 𝑌 ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑌)
24		ssel2 3179	. . . . . . . . . . . . . . . 16 ⊢ ((𝑌 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋)
25		rpxr 9753	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ*)
26	2	blopn 14810	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ*) → (𝑦(ball‘𝐶)𝑟) ∈ 𝐽)
27		eleq1a 2268	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦(ball‘𝐶)𝑟) ∈ 𝐽 → (𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
28	26, 27	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ*) → (𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
29	28	3expa 1205	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ*) → (𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
30	25, 29	sylan2 286	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ+) → (𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
31	30	rexlimdva 2614	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋) → (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
32	24, 31	sylan2 286	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
33	32	anassrs 400	. . . . . . . . . . . . . 14 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑦 ∈ 𝑌) → (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
34	23, 33	sylan2 286	. . . . . . . . . . . . 13 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ 𝑦 ∈ 𝑥)) → (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
35	34	anassrs 400	. . . . . . . . . . . 12 ⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) → (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
36	35	rexlimdva 2614	. . . . . . . . . . 11 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑌) → (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
37	36	adantrd 279	. . . . . . . . . 10 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑌) → ((∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥) → 𝑧 ∈ 𝐽))
38	37	adantrr 479	. . . . . . . . 9 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → ((∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥) → 𝑧 ∈ 𝐽))
39	38	abssdv 3258	. . . . . . . 8 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ⊆ 𝐽)
40		uniopn 14321	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ⊆ 𝐽) → ∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∈ 𝐽)
41	22, 39, 40	syl2anc 411	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → ∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∈ 𝐽)
42		oveq1 5932	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑢 → (𝑦(ball‘𝐶)𝑟) = (𝑢(ball‘𝐶)𝑟))
43	42	ineq1d 3364	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑢 → ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) = ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌))
44	43	sseq1d 3213	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑢 → (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
45	44	rexbidv 2498	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑢 → (∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
46	45	rspccv 2865	. . . . . . . . . . . . . 14 ⊢ (∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → (𝑢 ∈ 𝑥 → ∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
47	46	ad2antll 491	. . . . . . . . . . . . 13 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 → ∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
48		ssel 3178	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ⊆ 𝑌 → (𝑢 ∈ 𝑥 → 𝑢 ∈ 𝑌))
49		ssel 3178	. . . . . . . . . . . . . . . 16 ⊢ (𝑌 ⊆ 𝑋 → (𝑢 ∈ 𝑌 → 𝑢 ∈ 𝑋))
50		blcntr 14736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) → 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))
51	50	a1d 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))
52	51	ancld 325	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
53	52	3expa 1205	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝑋) ∧ 𝑟 ∈ ℝ+) → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
54	53	reximdva 2599	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝑋) → (∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
55	54	ex 115	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ∈ (∞Met‘𝑋) → (𝑢 ∈ 𝑋 → (∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))))
56	49, 55	sylan9r 410	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑢 ∈ 𝑌 → (∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))))
57	48, 56	sylan9r 410	. . . . . . . . . . . . . 14 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑌) → (𝑢 ∈ 𝑥 → (∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))))
58	57	adantrr 479	. . . . . . . . . . . . 13 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 → (∃𝑟 ∈ ℝ+ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))))
59	47, 58	mpdd 41	. . . . . . . . . . . 12 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 → ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
60	42	eleq2d 2266	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑢 → (𝑢 ∈ (𝑦(ball‘𝐶)𝑟) ↔ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))
61	44, 60	anbi12d 473	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑢 → ((((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ↔ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
62	61	rexbidv 2498	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑢 → (∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ↔ ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
63	62	rspcev 2868	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∈ 𝑥 ∧ ∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))) → ∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)))
64	63	ex 115	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ 𝑥 → (∃𝑟 ∈ ℝ+ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)) → ∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
65	59, 64	sylcom 28	. . . . . . . . . . 11 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 → ∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
66		simprl 529	. . . . . . . . . . . 12 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → 𝑥 ⊆ 𝑌)
67	66	sseld 3183	. . . . . . . . . . 11 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 → 𝑢 ∈ 𝑌))
68	65, 67	jcad 307	. . . . . . . . . 10 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 → (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢 ∈ 𝑌)))
69		elin 3347	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ↔ (𝑢 ∈ (𝑦(ball‘𝐶)𝑟) ∧ 𝑢 ∈ 𝑌))
70		ssel2 3179	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌)) → 𝑢 ∈ 𝑥)
71	69, 70	sylan2br 288	. . . . . . . . . . . . . 14 ⊢ ((((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ (𝑢 ∈ (𝑦(ball‘𝐶)𝑟) ∧ 𝑢 ∈ 𝑌)) → 𝑢 ∈ 𝑥)
72	71	expr 375	. . . . . . . . . . . . 13 ⊢ ((((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) → (𝑢 ∈ 𝑌 → 𝑢 ∈ 𝑥))
73	72	rexlimivw 2610	. . . . . . . . . . . 12 ⊢ (∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) → (𝑢 ∈ 𝑌 → 𝑢 ∈ 𝑥))
74	73	rexlimivw 2610	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) → (𝑢 ∈ 𝑌 → 𝑢 ∈ 𝑥))
75	74	imp 124	. . . . . . . . . 10 ⊢ ((∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢 ∈ 𝑌) → 𝑢 ∈ 𝑥)
76	68, 75	impbid1 142	. . . . . . . . 9 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 ↔ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢 ∈ 𝑌)))
77		elin 3347	. . . . . . . . . . 11 ⊢ (𝑢 ∈ (∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∩ 𝑌) ↔ (𝑢 ∈ ∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∧ 𝑢 ∈ 𝑌))
78		eluniab 3852	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ ∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ↔ ∃𝑧(𝑢 ∈ 𝑧 ∧ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)))
79		ancom 266	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ 𝑧 ∧ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)) ↔ ((∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥) ∧ 𝑢 ∈ 𝑧))
80		anass 401	. . . . . . . . . . . . . . . 16 ⊢ (((∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥) ∧ 𝑢 ∈ 𝑧) ↔ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
81		r19.41v 2653	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
82	81	rexbii 2504	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ ∃𝑦 ∈ 𝑥 (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
83		r19.41v 2653	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑦 ∈ 𝑥 (∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
84	82, 83	bitr2i 185	. . . . . . . . . . . . . . . 16 ⊢ ((∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ ∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
85	79, 80, 84	3bitri 206	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ 𝑧 ∧ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)) ↔ ∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
86	85	exbii 1619	. . . . . . . . . . . . . 14 ⊢ (∃𝑧(𝑢 ∈ 𝑧 ∧ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)) ↔ ∃𝑧∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
87	78, 86	bitri 184	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ ∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ↔ ∃𝑧∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
88		vex 2766	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑦 ∈ V
89		blex 14707	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 ∈ (∞Met‘𝑋) → (ball‘𝐶) ∈ V)
90		vex 2766	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑟 ∈ V
91	90	a1i 9	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → 𝑟 ∈ V)
92		ovexg 5959	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ V ∧ (ball‘𝐶) ∈ V ∧ 𝑟 ∈ V) → (𝑦(ball‘𝐶)𝑟) ∈ V)
93	88, 89, 91, 92	mp3an2ani 1355	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑦(ball‘𝐶)𝑟) ∈ V)
94		ineq1 3358	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = (𝑦(ball‘𝐶)𝑟) → (𝑧 ∩ 𝑌) = ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌))
95	94	sseq1d 3213	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑦(ball‘𝐶)𝑟) → ((𝑧 ∩ 𝑌) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
96		eleq2 2260	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑦(ball‘𝐶)𝑟) → (𝑢 ∈ 𝑧 ↔ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)))
97	95, 96	anbi12d 473	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑦(ball‘𝐶)𝑟) → (((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧) ↔ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
98	97	ceqsexgv 2893	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦(ball‘𝐶)𝑟) ∈ V → (∃𝑧(𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
99	93, 98	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑧(𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
100	99	rexbidv 2498	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑟 ∈ ℝ+ ∃𝑧(𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
101		rexcom4 2786	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑟 ∈ ℝ+ ∃𝑧(𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ ∃𝑧∃𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
102	100, 101	bitr3di 195	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ↔ ∃𝑧∃𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧))))
103	102	rexbidv 2498	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ↔ ∃𝑦 ∈ 𝑥 ∃𝑧∃𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧))))
104		rexcom4 2786	. . . . . . . . . . . . . 14 ⊢ (∃𝑦 ∈ 𝑥 ∃𝑧∃𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ ∃𝑧∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
105	103, 104	bitr2di 197	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑧∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ ∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
106	87, 105	bitrid 192	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑢 ∈ ∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ↔ ∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
107	106	anbi1d 465	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → ((𝑢 ∈ ∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∧ 𝑢 ∈ 𝑌) ↔ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢 ∈ 𝑌)))
108	77, 107	bitr2id 193	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → ((∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢 ∈ 𝑌) ↔ 𝑢 ∈ (∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∩ 𝑌)))
109	108	adantr 276	. . . . . . . . 9 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → ((∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢 ∈ 𝑌) ↔ 𝑢 ∈ (∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∩ 𝑌)))
110	76, 109	bitrd 188	. . . . . . . 8 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 ↔ 𝑢 ∈ (∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∩ 𝑌)))
111	110	eqrdv 2194	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → 𝑥 = (∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∩ 𝑌))
112		ineq1 3358	. . . . . . . 8 ⊢ (𝑢 = ∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} → (𝑢 ∩ 𝑌) = (∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∩ 𝑌))
113	112	rspceeqv 2886	. . . . . . 7 ⊢ ((∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∈ 𝐽 ∧ 𝑥 = (∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∩ 𝑌)) → ∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌))
114	41, 111, 113	syl2anc 411	. . . . . 6 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → ∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌))
115	114	ex 115	. . . . 5 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → ((𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥) → ∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌)))
116	20, 115	impbid 129	. . . 4 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌) ↔ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)))
117		simpr 110	. . . . . . . . . . 11 ⊢ ((𝑌 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑌)
118	24, 117	elind 3349	. . . . . . . . . 10 ⊢ ((𝑌 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ (𝑋 ∩ 𝑌))
119		metrest.1	. . . . . . . . . . . . . . 15 ⊢ 𝐷 = (𝐶 ↾ (𝑌 × 𝑌))
120	119	blres 14754	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋 ∩ 𝑌) ∧ 𝑟 ∈ ℝ*) → (𝑦(ball‘𝐷)𝑟) = ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌))
121	120	sseq1d 3213	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋 ∩ 𝑌) ∧ 𝑟 ∈ ℝ*) → ((𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
122	121	3expa 1205	. . . . . . . . . . . 12 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋 ∩ 𝑌)) ∧ 𝑟 ∈ ℝ*) → ((𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
123	25, 122	sylan2 286	. . . . . . . . . . 11 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋 ∩ 𝑌)) ∧ 𝑟 ∈ ℝ+) → ((𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
124	123	rexbidva 2494	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋 ∩ 𝑌)) → (∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
125	118, 124	sylan2 286	. . . . . . . . 9 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
126	125	anassrs 400	. . . . . . . 8 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑦 ∈ 𝑌) → (∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
127	23, 126	sylan2 286	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ 𝑦 ∈ 𝑥)) → (∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
128	127	anassrs 400	. . . . . 6 ⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) → (∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
129	128	ralbidva 2493	. . . . 5 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑌) → (∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
130	129	pm5.32da 452	. . . 4 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → ((𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥) ↔ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)))
131	116, 130	bitr4d 191	. . 3 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌) ↔ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)))
132	21	adantr 276	. . . 4 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → 𝐽 ∈ Top)
133		id 19	. . . . 5 ⊢ (𝑌 ⊆ 𝑋 → 𝑌 ⊆ 𝑋)
134	2	mopnm 14768	. . . . 5 ⊢ (𝐶 ∈ (∞Met‘𝑋) → 𝑋 ∈ 𝐽)
135		ssexg 4173	. . . . 5 ⊢ ((𝑌 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽) → 𝑌 ∈ V)
136	133, 134, 135	syl2anr 290	. . . 4 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → 𝑌 ∈ V)
137		elrest 12948	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑌 ∈ V) → (𝑥 ∈ (𝐽 ↾t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌)))
138	132, 136, 137	syl2anc 411	. . 3 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑥 ∈ (𝐽 ↾t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌)))
139		xmetres2 14699	. . . . 5 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝐶 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌))
140	119, 139	eqeltrid 2283	. . . 4 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → 𝐷 ∈ (∞Met‘𝑌))
141		metrest.4	. . . . 5 ⊢ 𝐾 = (MetOpen‘𝐷)
142	141	elmopn2 14769	. . . 4 ⊢ (𝐷 ∈ (∞Met‘𝑌) → (𝑥 ∈ 𝐾 ↔ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)))
143	140, 142	syl 14	. . 3 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑥 ∈ 𝐾 ↔ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ+ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)))
144	131, 138, 143	3bitr4d 220	. 2 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑥 ∈ (𝐽 ↾t 𝑌) ↔ 𝑥 ∈ 𝐾))
145	144	eqrdv 2194	1 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝐽 ↾t 𝑌) = 𝐾)

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 980   = wceq 1364  ∃wex 1506   ∈ wcel 2167  {cab 2182  ∀wral 2475  ∃wrex 2476  Vcvv 2763   ∩ cin 3156   ⊆ wss 3157  ∪ cuni 3840   × cxp 4662   ↾ cres 4666  ‘cfv 5259  (class class class)co 5925  ℝ^*cxr 8077  ℝ⁺crp 9745   ↾_t crest 12941  ∞Metcxmet 14168  ballcbl 14170  MetOpencmopn 14173  Topctop 14317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-coll 4149  ax-sep 4152  ax-nul 4160  ax-pow 4208  ax-pr 4243  ax-un 4469  ax-setind 4574  ax-iinf 4625  ax-cnex 7987  ax-resscn 7988  ax-1cn 7989  ax-1re 7990  ax-icn 7991  ax-addcl 7992  ax-addrcl 7993  ax-mulcl 7994  ax-mulrcl 7995  ax-addcom 7996  ax-mulcom 7997  ax-addass 7998  ax-mulass 7999  ax-distr 8000  ax-i2m1 8001  ax-0lt1 8002  ax-1rid 8003  ax-0id 8004  ax-rnegex 8005  ax-precex 8006  ax-cnre 8007  ax-pre-ltirr 8008  ax-pre-ltwlin 8009  ax-pre-lttrn 8010  ax-pre-apti 8011  ax-pre-ltadd 8012  ax-pre-mulgt0 8013  ax-pre-mulext 8014  ax-arch 8015  ax-caucvg 8016

This theorem depends on definitions:  df-bi 117  df-stab 832  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-nel 2463  df-ral 2480  df-rex 2481  df-reu 2482  df-rmo 2483  df-rab 2484  df-v 2765  df-sbc 2990  df-csb 3085  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-nul 3452  df-if 3563  df-pw 3608  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-int 3876  df-iun 3919  df-br 4035  df-opab 4096  df-mpt 4097  df-tr 4133  df-id 4329  df-po 4332  df-iso 4333  df-iord 4402  df-on 4404  df-ilim 4405  df-suc 4407  df-iom 4628  df-xp 4670  df-rel 4671  df-cnv 4672  df-co 4673  df-dm 4674  df-rn 4675  df-res 4676  df-ima 4677  df-iota 5220  df-fun 5261  df-fn 5262  df-f 5263  df-f1 5264  df-fo 5265  df-f1o 5266  df-fv 5267  df-isom 5268  df-riota 5880  df-ov 5928  df-oprab 5929  df-mpo 5930  df-1st 6207  df-2nd 6208  df-recs 6372  df-frec 6458  df-map 6718  df-sup 7059  df-inf 7060  df-pnf 8080  df-mnf 8081  df-xr 8082  df-ltxr 8083  df-le 8084  df-sub 8216  df-neg 8217  df-reap 8619  df-ap 8626  df-div 8717  df-inn 9008  df-2 9066  df-3 9067  df-4 9068  df-n0 9267  df-z 9344  df-uz 9619  df-q 9711  df-rp 9746  df-xneg 9864  df-xadd 9865  df-seqfrec 10557  df-exp 10648  df-cj 11024  df-re 11025  df-im 11026  df-rsqrt 11180  df-abs 11181  df-rest 12943  df-topgen 12962  df-psmet 14175  df-xmet 14176  df-bl 14178  df-mopn 14179  df-top 14318  df-topon 14331  df-bases 14363

This theorem is referenced by:  resubmet  14876  tgioo2cntop  14877  tgioo2  14879  divcnap  14885  cncfcncntop  14913  limcimolemlt  14984  cnplimcim  14987  cnplimclemr  14989  limccnpcntop  14995  limccnp2cntop  14997