metrest - Intuitionistic Logic Explorer

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

Theorem metrest 12714

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 3301	. . . . . . . . . 10 ⊢ (𝑢 ∩ 𝑌) ⊆ 𝑢
2		metrest.3	. . . . . . . . . . . . 13 ⊢ 𝐽 = (MetOpen‘𝐶)
3	2	elmopn2 12657	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ (∞Met‘𝑋) → (𝑢 ∈ 𝐽 ↔ (𝑢 ⊆ 𝑋 ∧ ∀𝑦 ∈ 𝑢 ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢)))
4	3	simplbda 382	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝐽) → ∀𝑦 ∈ 𝑢 ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢)
5	4	adantlr 469	. . . . . . . . . 10 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑢 ∈ 𝐽) → ∀𝑦 ∈ 𝑢 ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢)
6		ssralv 3166	. . . . . . . . . 10 ⊢ ((𝑢 ∩ 𝑌) ⊆ 𝑢 → (∀𝑦 ∈ 𝑢 ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢 → ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢))
7	1, 5, 6	mpsyl 65	. . . . . . . . 9 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑢 ∈ 𝐽) → ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢)
8		ssrin 3306	. . . . . . . . . . 11 ⊢ ((𝑦(ball‘𝐶)𝑟) ⊆ 𝑢 → ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌))
9	8	reximi 2532	. . . . . . . . . 10 ⊢ (∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢 → ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌))
10	9	ralimi 2498	. . . . . . . . 9 ⊢ (∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐶)𝑟) ⊆ 𝑢 → ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌))
11	7, 10	syl 14	. . . . . . . 8 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑢 ∈ 𝐽) → ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌))
12		inss2 3302	. . . . . . . 8 ⊢ (𝑢 ∩ 𝑌) ⊆ 𝑌
13	11, 12	jctil 310	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑢 ∈ 𝐽) → ((𝑢 ∩ 𝑌) ⊆ 𝑌 ∧ ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌)))
14		sseq1 3125	. . . . . . . 8 ⊢ (𝑥 = (𝑢 ∩ 𝑌) → (𝑥 ⊆ 𝑌 ↔ (𝑢 ∩ 𝑌) ⊆ 𝑌))
15		sseq2 3126	. . . . . . . . . 10 ⊢ (𝑥 = (𝑢 ∩ 𝑌) → (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌)))
16	15	rexbidv 2439	. . . . . . . . 9 ⊢ (𝑥 = (𝑢 ∩ 𝑌) → (∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌)))
17	16	raleqbi1dv 2637	. . . . . . . 8 ⊢ (𝑥 = (𝑢 ∩ 𝑌) → (∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌)))
18	14, 17	anbi12d 465	. . . . . . 7 ⊢ (𝑥 = (𝑢 ∩ 𝑌) → ((𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥) ↔ ((𝑢 ∩ 𝑌) ⊆ 𝑌 ∧ ∀𝑦 ∈ (𝑢 ∩ 𝑌)∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ (𝑢 ∩ 𝑌))))
19	13, 18	syl5ibrcom 156	. . . . . 6 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑢 ∈ 𝐽) → (𝑥 = (𝑢 ∩ 𝑌) → (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)))
20	19	rexlimdva 2552	. . . . 5 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌) → (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)))
21	2	mopntop 12652	. . . . . . . . 9 ⊢ (𝐶 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
22	21	ad2antrr 480	. . . . . . . 8 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → 𝐽 ∈ Top)
23		ssel2 3097	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ⊆ 𝑌 ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ 𝑌)
24		ssel2 3097	. . . . . . . . . . . . . . . 16 ⊢ ((𝑌 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑋)
25		rpxr 9478	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 ∈ ℝ⁺ → 𝑟 ∈ ℝ^*)
26	2	blopn 12698	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ^*) → (𝑦(ball‘𝐶)𝑟) ∈ 𝐽)
27		eleq1a 2212	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦(ball‘𝐶)𝑟) ∈ 𝐽 → (𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
28	26, 27	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋 ∧ 𝑟 ∈ ℝ^*) → (𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
29	28	3expa 1182	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ^*) → (𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
30	25, 29	sylan2 284	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → (𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
31	30	rexlimdva 2552	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋) → (∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
32	24, 31	sylan2 284	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
33	32	anassrs 398	. . . . . . . . . . . . . 14 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑦 ∈ 𝑌) → (∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
34	23, 33	sylan2 284	. . . . . . . . . . . . 13 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ 𝑦 ∈ 𝑥)) → (∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
35	34	anassrs 398	. . . . . . . . . . . 12 ⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) → (∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
36	35	rexlimdva 2552	. . . . . . . . . . 11 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑌) → (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) → 𝑧 ∈ 𝐽))
37	36	adantrd 277	. . . . . . . . . 10 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑌) → ((∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥) → 𝑧 ∈ 𝐽))
38	37	adantrr 471	. . . . . . . . 9 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → ((∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥) → 𝑧 ∈ 𝐽))
39	38	abssdv 3176	. . . . . . . 8 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ⊆ 𝐽)
40		uniopn 12207	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ⊆ 𝐽) → ∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∈ 𝐽)
41	22, 39, 40	syl2anc 409	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → ∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∈ 𝐽)
42		oveq1 5789	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑢 → (𝑦(ball‘𝐶)𝑟) = (𝑢(ball‘𝐶)𝑟))
43	42	ineq1d 3281	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑢 → ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) = ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌))
44	43	sseq1d 3131	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑢 → (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
45	44	rexbidv 2439	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑢 → (∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ⁺ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
46	45	rspccv 2790	. . . . . . . . . . . . . 14 ⊢ (∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → (𝑢 ∈ 𝑥 → ∃𝑟 ∈ ℝ⁺ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
47	46	ad2antll 483	. . . . . . . . . . . . 13 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 → ∃𝑟 ∈ ℝ⁺ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
48		ssel 3096	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ⊆ 𝑌 → (𝑢 ∈ 𝑥 → 𝑢 ∈ 𝑌))
49		ssel 3096	. . . . . . . . . . . . . . . 16 ⊢ (𝑌 ⊆ 𝑋 → (𝑢 ∈ 𝑌 → 𝑢 ∈ 𝑋))
50		blcntr 12624	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺) → 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))
51	50	a1d 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺) → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))
52	51	ancld 323	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺) → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
53	52	3expa 1182	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝑋) ∧ 𝑟 ∈ ℝ⁺) → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
54	53	reximdva 2537	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝑋) → (∃𝑟 ∈ ℝ⁺ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ⁺ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
55	54	ex 114	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ∈ (∞Met‘𝑋) → (𝑢 ∈ 𝑋 → (∃𝑟 ∈ ℝ⁺ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ⁺ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))))
56	49, 55	sylan9r 408	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑢 ∈ 𝑌 → (∃𝑟 ∈ ℝ⁺ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ⁺ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))))
57	48, 56	sylan9r 408	. . . . . . . . . . . . . 14 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑌) → (𝑢 ∈ 𝑥 → (∃𝑟 ∈ ℝ⁺ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ⁺ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))))
58	57	adantrr 471	. . . . . . . . . . . . 13 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 → (∃𝑟 ∈ ℝ⁺ ((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 → ∃𝑟 ∈ ℝ⁺ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))))
59	47, 58	mpdd 41	. . . . . . . . . . . 12 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 → ∃𝑟 ∈ ℝ⁺ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
60	42	eleq2d 2210	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑢 → (𝑢 ∈ (𝑦(ball‘𝐶)𝑟) ↔ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)))
61	44, 60	anbi12d 465	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑢 → ((((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ↔ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
62	61	rexbidv 2439	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑢 → (∃𝑟 ∈ ℝ⁺ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ↔ ∃𝑟 ∈ ℝ⁺ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))))
63	62	rspcev 2793	. . . . . . . . . . . . 13 ⊢ ((𝑢 ∈ 𝑥 ∧ ∃𝑟 ∈ ℝ⁺ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟))) → ∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)))
64	63	ex 114	. . . . . . . . . . . 12 ⊢ (𝑢 ∈ 𝑥 → (∃𝑟 ∈ ℝ⁺ (((𝑢(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑢(ball‘𝐶)𝑟)) → ∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
65	59, 64	sylcom 28	. . . . . . . . . . 11 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 → ∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
66		simprl 521	. . . . . . . . . . . 12 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → 𝑥 ⊆ 𝑌)
67	66	sseld 3101	. . . . . . . . . . 11 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 → 𝑢 ∈ 𝑌))
68	65, 67	jcad 305	. . . . . . . . . 10 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 → (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢 ∈ 𝑌)))
69		elin 3264	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ↔ (𝑢 ∈ (𝑦(ball‘𝐶)𝑟) ∧ 𝑢 ∈ 𝑌))
70		ssel2 3097	. . . . . . . . . . . . . . 15 ⊢ ((((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌)) → 𝑢 ∈ 𝑥)
71	69, 70	sylan2br 286	. . . . . . . . . . . . . 14 ⊢ ((((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ (𝑢 ∈ (𝑦(ball‘𝐶)𝑟) ∧ 𝑢 ∈ 𝑌)) → 𝑢 ∈ 𝑥)
72	71	expr 373	. . . . . . . . . . . . 13 ⊢ ((((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) → (𝑢 ∈ 𝑌 → 𝑢 ∈ 𝑥))
73	72	rexlimivw 2548	. . . . . . . . . . . 12 ⊢ (∃𝑟 ∈ ℝ⁺ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) → (𝑢 ∈ 𝑌 → 𝑢 ∈ 𝑥))
74	73	rexlimivw 2548	. . . . . . . . . . 11 ⊢ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) → (𝑢 ∈ 𝑌 → 𝑢 ∈ 𝑥))
75	74	imp 123	. . . . . . . . . 10 ⊢ ((∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢 ∈ 𝑌) → 𝑢 ∈ 𝑥)
76	68, 75	impbid1 141	. . . . . . . . 9 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 ↔ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢 ∈ 𝑌)))
77		elin 3264	. . . . . . . . . . 11 ⊢ (𝑢 ∈ (∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∩ 𝑌) ↔ (𝑢 ∈ ∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∧ 𝑢 ∈ 𝑌))
78		eluniab 3756	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ ∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ↔ ∃𝑧(𝑢 ∈ 𝑧 ∧ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)))
79		ancom 264	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ 𝑧 ∧ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)) ↔ ((∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥) ∧ 𝑢 ∈ 𝑧))
80		anass 399	. . . . . . . . . . . . . . . 16 ⊢ (((∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥) ∧ 𝑢 ∈ 𝑧) ↔ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
81		r19.41v 2590	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑟 ∈ ℝ⁺ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ (∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
82	81	rexbii 2445	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ ∃𝑦 ∈ 𝑥 (∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
83		r19.41v 2590	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑦 ∈ 𝑥 (∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
84	82, 83	bitr2i 184	. . . . . . . . . . . . . . . 16 ⊢ ((∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ ∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
85	79, 80, 84	3bitri 205	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ 𝑧 ∧ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)) ↔ ∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
86	85	exbii 1585	. . . . . . . . . . . . . 14 ⊢ (∃𝑧(𝑢 ∈ 𝑧 ∧ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)) ↔ ∃𝑧∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
87	78, 86	bitri 183	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ ∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ↔ ∃𝑧∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
88		vex 2692	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑦 ∈ V
89		blex 12595	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 ∈ (∞Met‘𝑋) → (ball‘𝐶) ∈ V)
90		vex 2692	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑟 ∈ V
91	90	a1i 9	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → 𝑟 ∈ V)
92		ovexg 5813	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ V ∧ (ball‘𝐶) ∈ V ∧ 𝑟 ∈ V) → (𝑦(ball‘𝐶)𝑟) ∈ V)
93	88, 89, 91, 92	mp3an2ani 1323	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑦(ball‘𝐶)𝑟) ∈ V)
94		ineq1 3275	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = (𝑦(ball‘𝐶)𝑟) → (𝑧 ∩ 𝑌) = ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌))
95	94	sseq1d 3131	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑦(ball‘𝐶)𝑟) → ((𝑧 ∩ 𝑌) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
96		eleq2 2204	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = (𝑦(ball‘𝐶)𝑟) → (𝑢 ∈ 𝑧 ↔ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)))
97	95, 96	anbi12d 465	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = (𝑦(ball‘𝐶)𝑟) → (((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧) ↔ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
98	97	ceqsexgv 2818	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦(ball‘𝐶)𝑟) ∈ V → (∃𝑧(𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
99	93, 98	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑧(𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
100	99	rexbidv 2439	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑟 ∈ ℝ⁺ ∃𝑧(𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ ∃𝑟 ∈ ℝ⁺ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
101		rexcom4 2712	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑟 ∈ ℝ⁺ ∃𝑧(𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ ∃𝑧∃𝑟 ∈ ℝ⁺ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
102	100, 101	bitr3di 194	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑟 ∈ ℝ⁺ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ↔ ∃𝑧∃𝑟 ∈ ℝ⁺ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧))))
103	102	rexbidv 2439	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ↔ ∃𝑦 ∈ 𝑥 ∃𝑧∃𝑟 ∈ ℝ⁺ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧))))
104		rexcom4 2712	. . . . . . . . . . . . . 14 ⊢ (∃𝑦 ∈ 𝑥 ∃𝑧∃𝑟 ∈ ℝ⁺ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ ∃𝑧∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)))
105	103, 104	syl6rbb 196	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑧∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ ((𝑧 ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ 𝑧)) ↔ ∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
106	87, 105	syl5bb 191	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑢 ∈ ∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ↔ ∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟))))
107	106	anbi1d 461	. . . . . . . . . . 11 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → ((𝑢 ∈ ∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∧ 𝑢 ∈ 𝑌) ↔ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢 ∈ 𝑌)))
108	77, 107	syl5rbb 192	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → ((∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢 ∈ 𝑌) ↔ 𝑢 ∈ (∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∩ 𝑌)))
109	108	adantr 274	. . . . . . . . 9 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → ((∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥 ∧ 𝑢 ∈ (𝑦(ball‘𝐶)𝑟)) ∧ 𝑢 ∈ 𝑌) ↔ 𝑢 ∈ (∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∩ 𝑌)))
110	76, 109	bitrd 187	. . . . . . . 8 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → (𝑢 ∈ 𝑥 ↔ 𝑢 ∈ (∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∩ 𝑌)))
111	110	eqrdv 2138	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → 𝑥 = (∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∩ 𝑌))
112		ineq1 3275	. . . . . . . 8 ⊢ (𝑢 = ∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} → (𝑢 ∩ 𝑌) = (∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∩ 𝑌))
113	112	rspceeqv 2811	. . . . . . 7 ⊢ ((∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∈ 𝐽 ∧ 𝑥 = (∪ {𝑧 ∣ (∃𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ 𝑧 = (𝑦(ball‘𝐶)𝑟) ∧ (𝑧 ∩ 𝑌) ⊆ 𝑥)} ∩ 𝑌)) → ∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌))
114	41, 111, 113	syl2anc 409	. . . . . 6 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)) → ∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌))
115	114	ex 114	. . . . 5 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → ((𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥) → ∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌)))
116	20, 115	impbid 128	. . . 4 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌) ↔ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)))
117		simpr 109	. . . . . . . . . . 11 ⊢ ((𝑌 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ 𝑌)
118	24, 117	elind 3266	. . . . . . . . . 10 ⊢ ((𝑌 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑌) → 𝑦 ∈ (𝑋 ∩ 𝑌))
119		metrest.1	. . . . . . . . . . . . . . 15 ⊢ 𝐷 = (𝐶 ↾ (𝑌 × 𝑌))
120	119	blres 12642	. . . . . . . . . . . . . 14 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋 ∩ 𝑌) ∧ 𝑟 ∈ ℝ^*) → (𝑦(ball‘𝐷)𝑟) = ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌))
121	120	sseq1d 3131	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋 ∩ 𝑌) ∧ 𝑟 ∈ ℝ^*) → ((𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
122	121	3expa 1182	. . . . . . . . . . . 12 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋 ∩ 𝑌)) ∧ 𝑟 ∈ ℝ^*) → ((𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
123	25, 122	sylan2 284	. . . . . . . . . . 11 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋 ∩ 𝑌)) ∧ 𝑟 ∈ ℝ⁺) → ((𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
124	123	rexbidva 2435	. . . . . . . . . 10 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ (𝑋 ∩ 𝑌)) → (∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
125	118, 124	sylan2 284	. . . . . . . . 9 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
126	125	anassrs 398	. . . . . . . 8 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑦 ∈ 𝑌) → (∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
127	23, 126	sylan2 284	. . . . . . 7 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ (𝑥 ⊆ 𝑌 ∧ 𝑦 ∈ 𝑥)) → (∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
128	127	anassrs 398	. . . . . 6 ⊢ ((((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑌) ∧ 𝑦 ∈ 𝑥) → (∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
129	128	ralbidva 2434	. . . . 5 ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑥 ⊆ 𝑌) → (∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥 ↔ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥))
130	129	pm5.32da 448	. . . 4 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → ((𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥) ↔ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ ((𝑦(ball‘𝐶)𝑟) ∩ 𝑌) ⊆ 𝑥)))
131	116, 130	bitr4d 190	. . 3 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌) ↔ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)))
132	21	adantr 274	. . . 4 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → 𝐽 ∈ Top)
133		id 19	. . . . 5 ⊢ (𝑌 ⊆ 𝑋 → 𝑌 ⊆ 𝑋)
134	2	mopnm 12656	. . . . 5 ⊢ (𝐶 ∈ (∞Met‘𝑋) → 𝑋 ∈ 𝐽)
135		ssexg 4075	. . . . 5 ⊢ ((𝑌 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽) → 𝑌 ∈ V)
136	133, 134, 135	syl2anr 288	. . . 4 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → 𝑌 ∈ V)
137		elrest 12166	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑌 ∈ V) → (𝑥 ∈ (𝐽 ↾_t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌)))
138	132, 136, 137	syl2anc 409	. . 3 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑥 ∈ (𝐽 ↾_t 𝑌) ↔ ∃𝑢 ∈ 𝐽 𝑥 = (𝑢 ∩ 𝑌)))
139		xmetres2 12587	. . . . 5 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝐶 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌))
140	119, 139	eqeltrid 2227	. . . 4 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → 𝐷 ∈ (∞Met‘𝑌))
141		metrest.4	. . . . 5 ⊢ 𝐾 = (MetOpen‘𝐷)
142	141	elmopn2 12657	. . . 4 ⊢ (𝐷 ∈ (∞Met‘𝑌) → (𝑥 ∈ 𝐾 ↔ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)))
143	140, 142	syl 14	. . 3 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑥 ∈ 𝐾 ↔ (𝑥 ⊆ 𝑌 ∧ ∀𝑦 ∈ 𝑥 ∃𝑟 ∈ ℝ⁺ (𝑦(ball‘𝐷)𝑟) ⊆ 𝑥)))
144	131, 138, 143	3bitr4d 219	. 2 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝑥 ∈ (𝐽 ↾_t 𝑌) ↔ 𝑥 ∈ 𝐾))
145	144	eqrdv 2138	1 ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝐽 ↾_t 𝑌) = 𝐾)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∧ w3a 963 = wceq 1332 ∃wex 1469 ∈ wcel 1481 {cab 2126 ∀wral 2417 ∃wrex 2418 Vcvv 2689 ∩ cin 3075 ⊆ wss 3076 ∪ cuni 3744 × cxp 4545 ↾ cres 4549 ‘cfv 5131 (class class class)co 5782 ℝ^*cxr 7823 ℝ⁺crp 9470 ↾_t crest 12159 ∞Metcxmet 12188 ballcbl 12190 MetOpencmopn 12193 Topctop 12203

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 604 ax-in2 605 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-13 1492 ax-14 1493 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 ax-coll 4051 ax-sep 4054 ax-nul 4062 ax-pow 4106 ax-pr 4139 ax-un 4363 ax-setind 4460 ax-iinf 4510 ax-cnex 7735 ax-resscn 7736 ax-1cn 7737 ax-1re 7738 ax-icn 7739 ax-addcl 7740 ax-addrcl 7741 ax-mulcl 7742 ax-mulrcl 7743 ax-addcom 7744 ax-mulcom 7745 ax-addass 7746 ax-mulass 7747 ax-distr 7748 ax-i2m1 7749 ax-0lt1 7750 ax-1rid 7751 ax-0id 7752 ax-rnegex 7753 ax-precex 7754 ax-cnre 7755 ax-pre-ltirr 7756 ax-pre-ltwlin 7757 ax-pre-lttrn 7758 ax-pre-apti 7759 ax-pre-ltadd 7760 ax-pre-mulgt0 7761 ax-pre-mulext 7762 ax-arch 7763 ax-caucvg 7764

This theorem depends on definitions: df-bi 116 df-stab 817 df-dc 821 df-3or 964 df-3an 965 df-tru 1335 df-fal 1338 df-nf 1438 df-sb 1737 df-eu 2003 df-mo 2004 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-ne 2310 df-nel 2405 df-ral 2422 df-rex 2423 df-reu 2424 df-rmo 2425 df-rab 2426 df-v 2691 df-sbc 2914 df-csb 3008 df-dif 3078 df-un 3080 df-in 3082 df-ss 3089 df-nul 3369 df-if 3480 df-pw 3517 df-sn 3538 df-pr 3539 df-op 3541 df-uni 3745 df-int 3780 df-iun 3823 df-br 3938 df-opab 3998 df-mpt 3999 df-tr 4035 df-id 4223 df-po 4226 df-iso 4227 df-iord 4296 df-on 4298 df-ilim 4299 df-suc 4301 df-iom 4513 df-xp 4553 df-rel 4554 df-cnv 4555 df-co 4556 df-dm 4557 df-rn 4558 df-res 4559 df-ima 4560 df-iota 5096 df-fun 5133 df-fn 5134 df-f 5135 df-f1 5136 df-fo 5137 df-f1o 5138 df-fv 5139 df-isom 5140 df-riota 5738 df-ov 5785 df-oprab 5786 df-mpo 5787 df-1st 6046 df-2nd 6047 df-recs 6210 df-frec 6296 df-map 6552 df-sup 6879 df-inf 6880 df-pnf 7826 df-mnf 7827 df-xr 7828 df-ltxr 7829 df-le 7830 df-sub 7959 df-neg 7960 df-reap 8361 df-ap 8368 df-div 8457 df-inn 8745 df-2 8803 df-3 8804 df-4 8805 df-n0 9002 df-z 9079 df-uz 9351 df-q 9439 df-rp 9471 df-xneg 9589 df-xadd 9590 df-seqfrec 10250 df-exp 10324 df-cj 10646 df-re 10647 df-im 10648 df-rsqrt 10802 df-abs 10803 df-rest 12161 df-topgen 12180 df-psmet 12195 df-xmet 12196 df-bl 12198 df-mopn 12199 df-top 12204 df-topon 12217 df-bases 12249

This theorem is referenced by: resubmet 12756 tgioo2cntop 12757 divcnap 12763 cncfcncntop 12788 limcimolemlt 12841 cnplimcim 12844 cnplimclemr 12846 limccnpcntop 12852 limccnp2cntop 12854

W3C validator