metrest - Intuitionistic Logic Explorer

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

Theorem metrest 15609

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 3451	. . . . . . . . . 10 ⊢ (𝑢 ∩ 𝑌) ⊆ 𝑢
2		metrest.3	. . . . . . . . . . . . 13 ⊢ 𝐽 = (MetOpen‘𝐶)
3	2	elmopn2 15552	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ (∞Met‘𝑋) → (𝑢 ∈ 𝐽 ↔ (𝑢 ⊆ 𝑋 ∧ ∀𝑦 ∈ 𝑢 ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢)))
4	3	simplbda 384	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝐽) → ∀𝑦 ∈ 𝑢 ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢)
5	4	adantlr 481	. . . . . . . . . 10 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑢 ∈ 𝐽) → ∀𝑦 ∈ 𝑢 ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢)
6		ssralv 3312	. . . . . . . . . 10 ⊢ ((𝑢 ∩ 𝑌) ⊆ 𝑢 → (∀𝑦 ∈ 𝑢 ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢 → ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢))
7	1, 5, 6	mpsyl 65	. . . . . . . . 9 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑢 ∈ 𝐽) → ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢)
8		ssrin 3456	. . . . . . . . . . 11 ⊢ ((𝑦(ball‘𝐶)𝑟) ⊆ 𝑢 → ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌))
9	8	reximi 2647	. . . . . . . . . 10 ⊢ (∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢 → ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌))
10	9	ralimi 2613	. . . . . . . . 9 ⊢ (∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢 → ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌))
11	7, 10	syl 14	. . . . . . . 8 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑢 ∈ 𝐽) → ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌))
12		inss2 3452	. . . . . . . 8 ⊢ (𝑢 ∩ 𝑌) ⊆ 𝑌
13	11, 12	jctil 312	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑢 ∈ 𝐽) → ((𝑢 ∩ 𝑌) ⊆ 𝑌 ∧ ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌)))
14		sseq1 3271	. . . . . . . 8 ⊢ (𝑥 = (𝑢 ∩ 𝑌) → (𝑥 ⊆ 𝑌 ↔ (𝑢 ∩ 𝑌) ⊆ 𝑌))
15		sseq2 3272	. . . . . . . . . 10 ⊢ (𝑥 = (𝑢 ∩ 𝑌) → (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌)))
16	15	rexbidv 2551	. . . . . . . . 9 ⊢ (𝑥 = (𝑢 ∩ 𝑌) → (∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌)))
17	16	raleqbi1dv 2761	. . . . . . . 8 ⊢ (𝑥 = (𝑢 ∩ 𝑌) → (∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌)))
18	14, 17	anbi12d 477	. . . . . . 7 ⊢ (𝑥 = (𝑢 ∩ 𝑌) → ((𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥) ↔ ((𝑢 ∩ 𝑌) ⊆ 𝑌 ∧ ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌))))
19	13, 18	syl5ibrcom 157	. . . . . 6 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑢 ∈ 𝐽) → (𝑥 = (𝑢 ∩ 𝑌) → (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)))
20	19	rexlimdva 2668	. . . . 5 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌) → (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)))
21	2	mopntop 15547	. . . . . . . . 9 ⊢ (𝐶 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
22	21	ad2antrr 492	. . . . . . . 8 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → 𝐽 ∈ Top)
23		ssel2 3243	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ⊆ 𝑌 ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑌)
24		ssel2 3243	. . . . . . . . . . . . . . . 16 ⊢ ((𝑌 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋)
25		rpxr 10064	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ^*)
26	2	blopn 15593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ^*) → (𝑦(ball‘𝐶)𝑟) ∈ 𝐽)
27		eleq1a 2310	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦(ball‘𝐶)𝑟) ∈ 𝐽 → (𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
28	26, 27	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ^*) → (𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
29	28	3expa 1234	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ^*) → (𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
30	25, 29	sylan2 286	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → (𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
31	30	rexlimdva 2668	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋) → (∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
32	24, 31	sylan2 286	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
33	32	anassrs 404	. . . . . . . . . . . . . 14 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑦 ∈ 𝑌) → (∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
34	23, 33	sylan2 286	. . . . . . . . . . . . 13 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ 𝑦 ∈ 𝑥)) → (∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
35	34	anassrs 404	. . . . . . . . . . . 12 ⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) → (∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
36	35	rexlimdva 2668	. . . . . . . . . . 11 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑌) → (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
37	36	adantrd 279	. . . . . . . . . 10 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑌) → ((∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥) → 𝑧 ∈ 𝐽))
38	37	adantrr 483	. . . . . . . . 9 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → ((∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥) → 𝑧 ∈ 𝐽))
39	38	abssdv 3322	. . . . . . . 8 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ⊆ 𝐽)
40		uniopn 15104	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ⊆ 𝐽) → ∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∈ 𝐽)
41	22, 39, 40	syl2anc 415	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → ∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∈ 𝐽)
42		oveq1 6092	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑢 → (𝑦(ball‘𝐶)𝑟) = (𝑢(ball‘𝐶)𝑟))
43	42	ineq1d 3431	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑢 → ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) = ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌))
44	43	sseq1d 3277	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑢 → (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
45	44	rexbidv 2551	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑢 → (∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ⁺ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
46	45	rspccv 2926	. . . . . . . . . . . . . 14 ⊢ (∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → (𝑢 ∈ 𝑥 → ∃𝑟 ∈ ℝ⁺ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
47	46	ad2antll 495	. . . . . . . . . . . . 13 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 → ∃𝑟 ∈ ℝ⁺ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
48		ssel 3242	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ⊆ 𝑌 → (𝑢 ∈ 𝑥 → 𝑢 ∈ 𝑌))
49		ssel 3242	. . . . . . . . . . . . . . . 16 ⊢ (𝑌 ⊆ 𝑋 → (𝑢 ∈ 𝑌 → 𝑢 ∈ 𝑋))
50		blcntr 15519	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺) → 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))
51	50	a1d 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺) → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))
52	51	ancld 325	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺) → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
53	52	3expa 1234	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
54	53	reximdva 2652	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝑋) → (∃𝑟 ∈ ℝ⁺ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ⁺ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
55	54	ex 115	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ∈ (∞Met‘𝑋) → (𝑢 ∈ 𝑋 → (∃𝑟 ∈ ℝ⁺ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ⁺ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))))
56	49, 55	sylan9r 414	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑢 ∈ 𝑌 → (∃𝑟 ∈ ℝ⁺ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ⁺ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))))
57	48, 56	sylan9r 414	. . . . . . . . . . . . . 14 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑌) → (𝑢 ∈ 𝑥 → (∃𝑟 ∈ ℝ⁺ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ⁺ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))))
58	57	adantrr 483	. . . . . . . . . . . . 13 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 → (∃𝑟 ∈ ℝ⁺ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ⁺ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))))
59	47, 58	mpdd 41	. . . . . . . . . . . 12 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 → ∃𝑟 ∈ ℝ⁺ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
60	42	eleq2d 2308	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑢 → (𝑢 ∈ (𝑦(ball‘𝐶)𝑟) ↔ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))
61	44, 60	anbi12d 477	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑢 → ((((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ↔ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
62	61	rexbidv 2551	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑢 → (∃𝑟 ∈ ℝ⁺ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ↔ ∃𝑟 ∈ ℝ⁺ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
63	62	rspcev 2929	. . . . . . . . . . . . 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 535	. . . . . . . . . . . 12 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → 𝑥 ⊆ 𝑌)
67	66	sseld 3247	. . . . . . . . . . 11 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 → 𝑢 ∈ 𝑌))
68	65, 67	jcad 307	. . . . . . . . . 10 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 → (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢 ∈ 𝑌)))
69		elin 3412	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ↔ (𝑢 ∈ (𝑦(ball‘𝐶)𝑟) ∧ 𝑢 ∈ 𝑌))
70		ssel2 3243	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌)) → 𝑢 ∈ 𝑥)
71	69, 70	sylan2br 288	. . . . . . . . . . . . . 14 ⊢ ((((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ (𝑢 ∈ (𝑦(ball‘𝐶)𝑟) ∧ 𝑢 ∈ 𝑌)) → 𝑢 ∈ 𝑥)
72	71	expr 375	. . . . . . . . . . . . 13 ⊢ ((((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) → (𝑢 ∈ 𝑌 → 𝑢 ∈ 𝑥))
73	72	rexlimivw 2664	. . . . . . . . . . . 12 ⊢ (∃𝑟 ∈ ℝ⁺ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) → (𝑢 ∈ 𝑌 → 𝑢 ∈ 𝑥))
74	73	rexlimivw 2664	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) → (𝑢 ∈ 𝑌 → 𝑢 ∈ 𝑥))
75	74	imp 124	. . . . . . . . . 10 ⊢ ((∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢 ∈ 𝑌) → 𝑢 ∈ 𝑥)
76	68, 75	impbid1 142	. . . . . . . . 9 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 ↔ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢 ∈ 𝑌)))
77		elin 3412	. . . . . . . . . . 11 ⊢ (𝑢 ∈ (∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∩ 𝑌) ↔ (𝑢 ∈ ∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∧ 𝑢 ∈ 𝑌))
78		eluniab 3947	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ ∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ↔ ∃𝑧(𝑢 ∈ 𝑧 ∧ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)))
79		ancom 266	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ 𝑧 ∧ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)) ↔ ((∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥) ∧ 𝑢 ∈ 𝑧))
80		anass 405	. . . . . . . . . . . . . . . 16 ⊢ (((∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥) ∧ 𝑢 ∈ 𝑧) ↔ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
81		r19.41v 2707	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑟 ∈ ℝ⁺ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ (∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
82	81	rexbii 2557	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ ∃𝑦 ∈ 𝑥 (∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
83		r19.41v 2707	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑦 ∈ 𝑥 (∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
84	82, 83	bitr2i 185	. . . . . . . . . . . . . . . 16 ⊢ ((∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ ∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
85	79, 80, 84	3bitri 206	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ 𝑧 ∧ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)) ↔ ∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
86	85	exbii 1658	. . . . . . . . . . . . . 14 ⊢ (∃𝑧(𝑢 ∈ 𝑧 ∧ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)) ↔ ∃𝑧∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
87	78, 86	bitri 184	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ ∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ↔ ∃𝑧∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
88		vex 2824	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑦 ∈ V
89		blex 15490	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 ∈ (∞Met‘𝑋) → (ball‘𝐶) ∈ V)
90		vex 2824	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑟 ∈ V
91	90	a1i 9	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → 𝑟 ∈ V)
92		ovexg 6119	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ V ∧ (ball‘𝐶) ∈ V ∧ 𝑟 ∈ V) → (𝑦(ball‘𝐶)𝑟) ∈ V)
93	88, 89, 91, 92	mp3an2ani 1385	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑦(ball‘𝐶)𝑟) ∈ V)
94		ineq1 3425	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = (𝑦(ball‘𝐶)𝑟) → (𝑧 ∩ 𝑌) = ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌))
95	94	sseq1d 3277	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑦(ball‘𝐶)𝑟) → ((𝑧 ∩ 𝑌) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
96		eleq2 2302	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑦(ball‘𝐶)𝑟) → (𝑢 ∈ 𝑧 ↔ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)))
97	95, 96	anbi12d 477	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑦(ball‘𝐶)𝑟) → (((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧) ↔ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
98	97	ceqsexgv 2955	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦(ball‘𝐶)𝑟) ∈ V → (∃𝑧(𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
99	93, 98	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑧(𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
100	99	rexbidv 2551	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑟 ∈ ℝ⁺ ∃𝑧(𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ ∃𝑟 ∈ ℝ⁺ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
101		rexcom4 2845	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑟 ∈ ℝ⁺ ∃𝑧(𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ ∃𝑧∃𝑟 ∈ ℝ⁺ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
102	100, 101	bitr3di 195	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑟 ∈ ℝ⁺ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ↔ ∃𝑧∃𝑟 ∈ ℝ⁺ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧))))
103	102	rexbidv 2551	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ↔ ∃𝑦 ∈ 𝑥 ∃𝑧∃𝑟 ∈ ℝ⁺ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧))))
104		rexcom4 2845	. . . . . . . . . . . . . 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 469	. . . . . . . . . . 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 2236	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → 𝑥 = (∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∩ 𝑌))
112		ineq1 3425	. . . . . . . 8 ⊢ (𝑢 = ∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} → (𝑢 ∩ 𝑌) = (∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∩ 𝑌))
113	112	rspceeqv 2948	. . . . . . 7 ⊢ ((∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∈ 𝐽 ∧ 𝑥 = (∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∩ 𝑌)) → ∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌))
114	41, 111, 113	syl2anc 415	. . . . . 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 3414	. . . . . . . . . 10 ⊢ ((𝑌 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ (𝑋 ∩ 𝑌))
119		metrest.1	. . . . . . . . . . . . . . 15 ⊢ 𝐷 = (𝐶 ↾ (𝑌 × 𝑌))
120	119	blres 15537	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋 ∩ 𝑌) ∧ 𝑟 ∈ ℝ^*) → (𝑦(ball‘𝐷)𝑟) = ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌))
121	120	sseq1d 3277	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋 ∩ 𝑌) ∧ 𝑟 ∈ ℝ^*) → ((𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
122	121	3expa 1234	. . . . . . . . . . . 12 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋 ∩ 𝑌)) ∧ 𝑟 ∈ ℝ^*) → ((𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
123	25, 122	sylan2 286	. . . . . . . . . . 11 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋 ∩ 𝑌)) ∧ 𝑟 ∈ ℝ⁺) → ((𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
124	123	rexbidva 2547	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋 ∩ 𝑌)) → (∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
125	118, 124	sylan2 286	. . . . . . . . 9 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
126	125	anassrs 404	. . . . . . . 8 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑦 ∈ 𝑌) → (∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
127	23, 126	sylan2 286	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ 𝑦 ∈ 𝑥)) → (∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
128	127	anassrs 404	. . . . . 6 ⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) → (∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
129	128	ralbidva 2546	. . . . 5 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑌) → (∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
130	129	pm5.32da 456	. . . 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 15551	. . . . 5 ⊢ (𝐶 ∈ (∞Met‘𝑋) → 𝑋 ∈ 𝐽)
135		ssexg 4272	. . . . 5 ⊢ ((𝑌 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽) → 𝑌 ∈ V)
136	133, 134, 135	syl2anr 290	. . . 4 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → 𝑌 ∈ V)
137		elrest 13602	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑌 ∈ V) → (𝑥 ∈ (𝐽 ↾_t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌)))
138	132, 136, 137	syl2anc 415	. . 3 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑥 ∈ (𝐽 ↾_t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌)))
139		xmetres2 15482	. . . . 5 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝐶 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌))
140	119, 139	eqeltrid 2325	. . . 4 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → 𝐷 ∈ (∞Met‘𝑌))
141		metrest.4	. . . . 5 ⊢ 𝐾 = (MetOpen‘𝐷)
142	141	elmopn2 15552	. . . 4 ⊢ (𝐷 ∈ (∞Met‘𝑌) → (𝑥 ∈ 𝐾 ↔ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)))
143	140, 142	syl 14	. . 3 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑥 ∈ 𝐾 ↔ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)))
144	131, 138, 143	3bitr4d 220	. 2 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑥 ∈ (𝐽 ↾_t 𝑌) ↔ 𝑥 ∈ 𝐾))
145	144	eqrdv 2236	1 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝐽 ↾_t 𝑌) = 𝐾)

Colors of variables: wff set class

This proof depends on syntax axioms: → wi 4 ∧ wa 104 ↔ wb 105 ∧ w3a 1009 = wceq 1402 ∃wex 1545 ∈ wcel 2209 {cab 2224 ∀wral 2528 ∃wrex 2529 Vcvv 2821 ∩ cin 3219 ⊆ wss 3220 ∪ cuni 3935 × cxp 4772 ↾ cres 4776 ‘cfv 5377 (class class class)co 6085 ℝ^*cxr 8359 ℝ⁺crp 10056 ↾_t crest 13595 ∞Metcxmet 14875 ballcbl 14877 MetOpencmopn 14880 Topctop 15100

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4246 ax-sep 4249 ax-nul 4259 ax-pow 4311 ax-pr 4346 ax-un 4578 ax-setind 4684 ax-iinf 4735 ax-cnex 8270 ax-resscn 8271 ax-1cn 8272 ax-1re 8273 ax-icn 8274 ax-addcl 8275 ax-addrcl 8276 ax-mulcl 8277 ax-mulrcl 8278 ax-addcom 8279 ax-mulcom 8280 ax-addass 8281 ax-mulass 8282 ax-distr 8283 ax-i2m1 8284 ax-0lt1 8285 ax-1rid 8286 ax-0id 8287 ax-rnegex 8288 ax-precex 8289 ax-cnre 8290 ax-pre-ltirr 8291 ax-pre-ltwlin 8292 ax-pre-lttrn 8293 ax-pre-apti 8294 ax-pre-ltadd 8295 ax-pre-mulgt0 8296 ax-pre-mulext 8297 ax-arch 8298 ax-caucvg 8299

This proof depends on definitions: df-bi 117 df-stab 843 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-br 4131 df-opab 4193 df-mpt 4194 df-tr 4230 df-id 4438 df-po 4441 df-iso 4442 df-iord 4511 df-on 4513 df-ilim 4514 df-suc 4516 df-iom 4738 df-xp 4780 df-rel 4781 df-cnv 4782 df-co 4783 df-dm 4784 df-rn 4785 df-res 4786 df-ima 4787 df-iota 5337 df-fun 5379 df-fn 5380 df-f 5381 df-f1 5382 df-fo 5383 df-f1o 5384 df-fv 5385 df-isom 5386 df-riota 6038 df-ov 6088 df-oprab 6089 df-mpo 6090 df-1st 6374 df-2nd 6375 df-recs 6576 df-frec 6662 df-map 6924 df-sup 7324 df-inf 7325 df-pnf 8362 df-mnf 8363 df-xr 8364 df-ltxr 8365 df-le 8366 df-sub 8499 df-neg 8500 df-reap 8904 df-ap 8911 df-div 9004 df-inn 9306 df-2 9364 df-3 9365 df-4 9366 df-n0 9566 df-z 9647 df-uz 9924 df-q 10022 df-rp 10057 df-xneg 10176 df-xadd 10177 df-seqfrec 10887 df-exp 10978 df-cj 11609 df-re 11610 df-im 11611 df-rsqrt 11766 df-abs 11767 df-rest 13597 df-topgen 13616 df-psmet 14882 df-xmet 14883 df-bl 14885 df-mopn 14886 df-top 15101 df-topon 15114 df-bases 15146

This theorem is used by: resubmet 15659 tgioo2cntop 15660 tgioo2 15662 divcnap 15668 cncfcncntop 15696 limcimolemlt 15767 cnplimcim 15770 cnplimclemr 15772 limccnpcntop 15778 limccnp2cntop 15780

W3C validator