metrest

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)

	Ref	Expression
Hypotheses	metrest.1	$⊢ D = {C ↾}_{(Y \times Y)}$
	metrest.3	$⊢ J = MetOpen (C)$
	metrest.4	$⊢ K = MetOpen (D)$
Assertion	metrest	$⊢ (C \in ∞Met (X) \land Y \subseteq X) \to J ↾_{𝑡} Y = K$

Proof

Step	Hyp	Ref	Expression
1		metrest.1	$⊢ D = {C ↾}_{(Y \times Y)}$
2		metrest.3	$⊢ J = MetOpen (C)$
3		metrest.4	$⊢ K = MetOpen (D)$
4		inss1	$⊢ u \cap Y \subseteq u$
5	2	elmopn2	$⊢ C \in ∞Met (X) \to (u \in J \leftrightarrow (u \subseteq X \land \forall y \in u \exists r \in ℝ^{+} y ball (C) r \subseteq u))$
6	5	simplbda	$⊢ (C \in ∞Met (X) \land u \in J) \to \forall y \in u \exists r \in ℝ^{+} y ball (C) r \subseteq u$
7	6	adantlr	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land u \in J) \to \forall y \in u \exists r \in ℝ^{+} y ball (C) r \subseteq u$
8		ssralv	$⊢ u \cap Y \subseteq u \to (\forall y \in u \exists r \in ℝ^{+} y ball (C) r \subseteq u \to \forall y \in (u \cap Y) \exists r \in ℝ^{+} y ball (C) r \subseteq u)$
9	4 7 8	mpsyl	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land u \in J) \to \forall y \in (u \cap Y) \exists r \in ℝ^{+} y ball (C) r \subseteq u$
10		ssrin	$⊢ y ball (C) r \subseteq u \to (y ball (C) r) \cap Y \subseteq u \cap Y$
11	10	reximi	$⊢ \exists r \in ℝ^{+} y ball (C) r \subseteq u \to \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq u \cap Y$
12	11	ralimi	$⊢ \forall y \in (u \cap Y) \exists r \in ℝ^{+} y ball (C) r \subseteq u \to \forall y \in (u \cap Y) \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq u \cap Y$
13	9 12	syl	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land u \in J) \to \forall y \in (u \cap Y) \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq u \cap Y$
14		inss2	$⊢ u \cap Y \subseteq Y$
15	13 14	jctil	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land u \in J) \to (u \cap Y \subseteq Y \land \forall y \in (u \cap Y) \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq u \cap Y)$
16		sseq1	$⊢ x = u \cap Y \to (x \subseteq Y \leftrightarrow u \cap Y \subseteq Y)$
17		sseq2	$⊢ x = u \cap Y \to ((y ball (C) r) \cap Y \subseteq x \leftrightarrow (y ball (C) r) \cap Y \subseteq u \cap Y)$
18	17	rexbidv	$⊢ x = u \cap Y \to (\exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x \leftrightarrow \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq u \cap Y)$
19	18	raleqbi1dv	$⊢ x = u \cap Y \to (\forall y \in x \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x \leftrightarrow \forall y \in (u \cap Y) \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq u \cap Y)$
20	16 19	anbi12d	$⊢ x = u \cap Y \to ((x \subseteq Y \land \forall y \in x \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x) \leftrightarrow (u \cap Y \subseteq Y \land \forall y \in (u \cap Y) \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq u \cap Y))$
21	15 20	syl5ibrcom	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land u \in J) \to (x = u \cap Y \to (x \subseteq Y \land \forall y \in x \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x))$
22	21	rexlimdva	$⊢ (C \in ∞Met (X) \land Y \subseteq X) \to (\exists u \in J x = u \cap Y \to (x \subseteq Y \land \forall y \in x \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x))$
23	2	mopntop	$⊢ C \in ∞Met (X) \to J \in Top$
24	23	ad2antrr	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land (x \subseteq Y \land \forall y \in x \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x)) \to J \in Top$
25		ssel2	$⊢ (x \subseteq Y \land y \in x) \to y \in Y$
26		ssel2	$⊢ (Y \subseteq X \land y \in Y) \to y \in X$
27		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
28	2	blopn	$⊢ (C \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \to y ball (C) r \in J$
29		eleq1a	$⊢ y ball (C) r \in J \to (z = y ball (C) r \to z \in J)$
30	28 29	syl	$⊢ (C \in ∞Met (X) \land y \in X \land r \in ℝ^{*}) \to (z = y ball (C) r \to z \in J)$
31	30	3expa	$⊢ ((C \in ∞Met (X) \land y \in X) \land r \in ℝ^{*}) \to (z = y ball (C) r \to z \in J)$
32	27 31	sylan2	$⊢ ((C \in ∞Met (X) \land y \in X) \land r \in ℝ^{+}) \to (z = y ball (C) r \to z \in J)$
33	32	rexlimdva	$⊢ (C \in ∞Met (X) \land y \in X) \to (\exists r \in ℝ^{+} z = y ball (C) r \to z \in J)$
34	26 33	sylan2	$⊢ (C \in ∞Met (X) \land (Y \subseteq X \land y \in Y)) \to (\exists r \in ℝ^{+} z = y ball (C) r \to z \in J)$
35	34	anassrs	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land y \in Y) \to (\exists r \in ℝ^{+} z = y ball (C) r \to z \in J)$
36	25 35	sylan2	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land (x \subseteq Y \land y \in x)) \to (\exists r \in ℝ^{+} z = y ball (C) r \to z \in J)$
37	36	anassrs	$⊢ (((C \in ∞Met (X) \land Y \subseteq X) \land x \subseteq Y) \land y \in x) \to (\exists r \in ℝ^{+} z = y ball (C) r \to z \in J)$
38	37	rexlimdva	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land x \subseteq Y) \to (\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \to z \in J)$
39	38	adantrd	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land x \subseteq Y) \to ((\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land z \cap Y \subseteq x) \to z \in J)$
40	39	adantrr	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land (x \subseteq Y \land \forall y \in x \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x)) \to ((\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land z \cap Y \subseteq x) \to z \in J)$
41	40	abssdv	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land (x \subseteq Y \land \forall y \in x \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x)) \to \{z \| (\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land z \cap Y \subseteq x)\} \subseteq J$
42		uniopn	$⊢ (J \in Top \land \{z \| (\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land z \cap Y \subseteq x)\} \subseteq J) \to ⋃ \{z \| (\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land z \cap Y \subseteq x)\} \in J$
43	24 41 42	syl2anc	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land (x \subseteq Y \land \forall y \in x \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x)) \to ⋃ \{z \| (\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land z \cap Y \subseteq x)\} \in J$
44		oveq1	$⊢ y = u \to y ball (C) r = u ball (C) r$
45	44	ineq1d	$⊢ y = u \to (y ball (C) r) \cap Y = (u ball (C) r) \cap Y$
46	45	sseq1d	$⊢ y = u \to ((y ball (C) r) \cap Y \subseteq x \leftrightarrow (u ball (C) r) \cap Y \subseteq x)$
47	46	rexbidv	$⊢ y = u \to (\exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x \leftrightarrow \exists r \in ℝ^{+} (u ball (C) r) \cap Y \subseteq x)$
48	47	rspccv	$⊢ \forall y \in x \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x \to (u \in x \to \exists r \in ℝ^{+} (u ball (C) r) \cap Y \subseteq x)$
49	48	ad2antll	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land (x \subseteq Y \land \forall y \in x \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x)) \to (u \in x \to \exists r \in ℝ^{+} (u ball (C) r) \cap Y \subseteq x)$
50		ssel	$⊢ x \subseteq Y \to (u \in x \to u \in Y)$
51		ssel	$⊢ Y \subseteq X \to (u \in Y \to u \in X)$
52		blcntr	$⊢ (C \in ∞Met (X) \land u \in X \land r \in ℝ^{+}) \to u \in (u ball (C) r)$
53	52	a1d	$⊢ (C \in ∞Met (X) \land u \in X \land r \in ℝ^{+}) \to ((u ball (C) r) \cap Y \subseteq x \to u \in (u ball (C) r))$
54	53	ancld	$⊢ (C \in ∞Met (X) \land u \in X \land r \in ℝ^{+}) \to ((u ball (C) r) \cap Y \subseteq x \to ((u ball (C) r) \cap Y \subseteq x \land u \in (u ball (C) r)))$
55	54	3expa	$⊢ ((C \in ∞Met (X) \land u \in X) \land r \in ℝ^{+}) \to ((u ball (C) r) \cap Y \subseteq x \to ((u ball (C) r) \cap Y \subseteq x \land u \in (u ball (C) r)))$
56	55	reximdva	$⊢ (C \in ∞Met (X) \land u \in X) \to (\exists r \in ℝ^{+} (u ball (C) r) \cap Y \subseteq x \to \exists r \in ℝ^{+} ((u ball (C) r) \cap Y \subseteq x \land u \in (u ball (C) r)))$
57	56	ex	$⊢ C \in ∞Met (X) \to (u \in X \to (\exists r \in ℝ^{+} (u ball (C) r) \cap Y \subseteq x \to \exists r \in ℝ^{+} ((u ball (C) r) \cap Y \subseteq x \land u \in (u ball (C) r))))$
58	51 57	sylan9r	$⊢ (C \in ∞Met (X) \land Y \subseteq X) \to (u \in Y \to (\exists r \in ℝ^{+} (u ball (C) r) \cap Y \subseteq x \to \exists r \in ℝ^{+} ((u ball (C) r) \cap Y \subseteq x \land u \in (u ball (C) r))))$
59	50 58	sylan9r	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land x \subseteq Y) \to (u \in x \to (\exists r \in ℝ^{+} (u ball (C) r) \cap Y \subseteq x \to \exists r \in ℝ^{+} ((u ball (C) r) \cap Y \subseteq x \land u \in (u ball (C) r))))$
60	59	adantrr	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land (x \subseteq Y \land \forall y \in x \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x)) \to (u \in x \to (\exists r \in ℝ^{+} (u ball (C) r) \cap Y \subseteq x \to \exists r \in ℝ^{+} ((u ball (C) r) \cap Y \subseteq x \land u \in (u ball (C) r))))$
61	49 60	mpdd	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land (x \subseteq Y \land \forall y \in x \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x)) \to (u \in x \to \exists r \in ℝ^{+} ((u ball (C) r) \cap Y \subseteq x \land u \in (u ball (C) r)))$
62	44	eleq2d	$⊢ y = u \to (u \in (y ball (C) r) \leftrightarrow u \in (u ball (C) r))$
63	46 62	anbi12d	$⊢ y = u \to (((y ball (C) r) \cap Y \subseteq x \land u \in (y ball (C) r)) \leftrightarrow ((u ball (C) r) \cap Y \subseteq x \land u \in (u ball (C) r)))$
64	63	rexbidv	$⊢ y = u \to (\exists r \in ℝ^{+} ((y ball (C) r) \cap Y \subseteq x \land u \in (y ball (C) r)) \leftrightarrow \exists r \in ℝ^{+} ((u ball (C) r) \cap Y \subseteq x \land u \in (u ball (C) r)))$
65	64	rspcev	$⊢ (u \in x \land \exists r \in ℝ^{+} ((u ball (C) r) \cap Y \subseteq x \land u \in (u ball (C) r))) \to \exists y \in x \exists r \in ℝ^{+} ((y ball (C) r) \cap Y \subseteq x \land u \in (y ball (C) r))$
66	65	ex	$⊢ u \in x \to (\exists r \in ℝ^{+} ((u ball (C) r) \cap Y \subseteq x \land u \in (u ball (C) r)) \to \exists y \in x \exists r \in ℝ^{+} ((y ball (C) r) \cap Y \subseteq x \land u \in (y ball (C) r)))$
67	61 66	sylcom	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land (x \subseteq Y \land \forall y \in x \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x)) \to (u \in x \to \exists y \in x \exists r \in ℝ^{+} ((y ball (C) r) \cap Y \subseteq x \land u \in (y ball (C) r)))$
68		simprl	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land (x \subseteq Y \land \forall y \in x \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x)) \to x \subseteq Y$
69	68	sseld	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land (x \subseteq Y \land \forall y \in x \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x)) \to (u \in x \to u \in Y)$
70	67 69	jcad	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land (x \subseteq Y \land \forall y \in x \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x)) \to (u \in x \to (\exists y \in x \exists r \in ℝ^{+} ((y ball (C) r) \cap Y \subseteq x \land u \in (y ball (C) r)) \land u \in Y))$
71		elin	$⊢ u \in ((y ball (C) r) \cap Y) \leftrightarrow (u \in (y ball (C) r) \land u \in Y)$
72		ssel2	$⊢ ((y ball (C) r) \cap Y \subseteq x \land u \in ((y ball (C) r) \cap Y)) \to u \in x$
73	71 72	sylan2br	$⊢ ((y ball (C) r) \cap Y \subseteq x \land (u \in (y ball (C) r) \land u \in Y)) \to u \in x$
74	73	expr	$⊢ ((y ball (C) r) \cap Y \subseteq x \land u \in (y ball (C) r)) \to (u \in Y \to u \in x)$
75	74	rexlimivw	$⊢ \exists r \in ℝ^{+} ((y ball (C) r) \cap Y \subseteq x \land u \in (y ball (C) r)) \to (u \in Y \to u \in x)$
76	75	rexlimivw	$⊢ \exists y \in x \exists r \in ℝ^{+} ((y ball (C) r) \cap Y \subseteq x \land u \in (y ball (C) r)) \to (u \in Y \to u \in x)$
77	76	imp	$⊢ (\exists y \in x \exists r \in ℝ^{+} ((y ball (C) r) \cap Y \subseteq x \land u \in (y ball (C) r)) \land u \in Y) \to u \in x$
78	70 77	impbid1	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land (x \subseteq Y \land \forall y \in x \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x)) \to (u \in x \leftrightarrow (\exists y \in x \exists r \in ℝ^{+} ((y ball (C) r) \cap Y \subseteq x \land u \in (y ball (C) r)) \land u \in Y))$
79		elin	$⊢ u \in (⋃ \{z \| (\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land z \cap Y \subseteq x)\} \cap Y) \leftrightarrow (u \in ⋃ \{z \| (\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land z \cap Y \subseteq x)\} \land u \in Y)$
80		eluniab	$⊢ u \in ⋃ \{z \| (\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land z \cap Y \subseteq x)\} \leftrightarrow \exists z (u \in z \land (\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land z \cap Y \subseteq x))$
81		ancom	$⊢ (u \in z \land (\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land z \cap Y \subseteq x)) \leftrightarrow ((\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land z \cap Y \subseteq x) \land u \in z)$
82		anass	$⊢ ((\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land z \cap Y \subseteq x) \land u \in z) \leftrightarrow (\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land (z \cap Y \subseteq x \land u \in z))$
83		r19.41v	$⊢ \exists r \in ℝ^{+} (z = y ball (C) r \land (z \cap Y \subseteq x \land u \in z)) \leftrightarrow (\exists r \in ℝ^{+} z = y ball (C) r \land (z \cap Y \subseteq x \land u \in z))$
84	83	rexbii	$⊢ \exists y \in x \exists r \in ℝ^{+} (z = y ball (C) r \land (z \cap Y \subseteq x \land u \in z)) \leftrightarrow \exists y \in x (\exists r \in ℝ^{+} z = y ball (C) r \land (z \cap Y \subseteq x \land u \in z))$
85		r19.41v	$⊢ \exists y \in x (\exists r \in ℝ^{+} z = y ball (C) r \land (z \cap Y \subseteq x \land u \in z)) \leftrightarrow (\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land (z \cap Y \subseteq x \land u \in z))$
86	84 85	bitr2i	$⊢ (\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land (z \cap Y \subseteq x \land u \in z)) \leftrightarrow \exists y \in x \exists r \in ℝ^{+} (z = y ball (C) r \land (z \cap Y \subseteq x \land u \in z))$
87	81 82 86	3bitri	$⊢ (u \in z \land (\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land z \cap Y \subseteq x)) \leftrightarrow \exists y \in x \exists r \in ℝ^{+} (z = y ball (C) r \land (z \cap Y \subseteq x \land u \in z))$
88	87	exbii	$⊢ \exists z (u \in z \land (\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land z \cap Y \subseteq x)) \leftrightarrow \exists z \exists y \in x \exists r \in ℝ^{+} (z = y ball (C) r \land (z \cap Y \subseteq x \land u \in z))$
89		ovex	$⊢ y ball (C) r \in V$
90		ineq1	$⊢ z = y ball (C) r \to z \cap Y = (y ball (C) r) \cap Y$
91	90	sseq1d	$⊢ z = y ball (C) r \to (z \cap Y \subseteq x \leftrightarrow (y ball (C) r) \cap Y \subseteq x)$
92		eleq2	$⊢ z = y ball (C) r \to (u \in z \leftrightarrow u \in (y ball (C) r))$
93	91 92	anbi12d	$⊢ z = y ball (C) r \to ((z \cap Y \subseteq x \land u \in z) \leftrightarrow ((y ball (C) r) \cap Y \subseteq x \land u \in (y ball (C) r)))$
94	89 93	ceqsexv	$⊢ \exists z (z = y ball (C) r \land (z \cap Y \subseteq x \land u \in z)) \leftrightarrow ((y ball (C) r) \cap Y \subseteq x \land u \in (y ball (C) r))$
95	94	rexbii	$⊢ \exists r \in ℝ^{+} \exists z (z = y ball (C) r \land (z \cap Y \subseteq x \land u \in z)) \leftrightarrow \exists r \in ℝ^{+} ((y ball (C) r) \cap Y \subseteq x \land u \in (y ball (C) r))$
96		rexcom4	$⊢ \exists r \in ℝ^{+} \exists z (z = y ball (C) r \land (z \cap Y \subseteq x \land u \in z)) \leftrightarrow \exists z \exists r \in ℝ^{+} (z = y ball (C) r \land (z \cap Y \subseteq x \land u \in z))$
97	95 96	bitr3i	$⊢ \exists r \in ℝ^{+} ((y ball (C) r) \cap Y \subseteq x \land u \in (y ball (C) r)) \leftrightarrow \exists z \exists r \in ℝ^{+} (z = y ball (C) r \land (z \cap Y \subseteq x \land u \in z))$
98	97	rexbii	$⊢ \exists y \in x \exists r \in ℝ^{+} ((y ball (C) r) \cap Y \subseteq x \land u \in (y ball (C) r)) \leftrightarrow \exists y \in x \exists z \exists r \in ℝ^{+} (z = y ball (C) r \land (z \cap Y \subseteq x \land u \in z))$
99		rexcom4	$⊢ \exists y \in x \exists z \exists r \in ℝ^{+} (z = y ball (C) r \land (z \cap Y \subseteq x \land u \in z)) \leftrightarrow \exists z \exists y \in x \exists r \in ℝ^{+} (z = y ball (C) r \land (z \cap Y \subseteq x \land u \in z))$
100	98 99	bitr2i	$⊢ \exists z \exists y \in x \exists r \in ℝ^{+} (z = y ball (C) r \land (z \cap Y \subseteq x \land u \in z)) \leftrightarrow \exists y \in x \exists r \in ℝ^{+} ((y ball (C) r) \cap Y \subseteq x \land u \in (y ball (C) r))$
101	80 88 100	3bitri	$⊢ u \in ⋃ \{z \| (\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land z \cap Y \subseteq x)\} \leftrightarrow \exists y \in x \exists r \in ℝ^{+} ((y ball (C) r) \cap Y \subseteq x \land u \in (y ball (C) r))$
102	101	anbi1i	$⊢ (u \in ⋃ \{z \| (\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land z \cap Y \subseteq x)\} \land u \in Y) \leftrightarrow (\exists y \in x \exists r \in ℝ^{+} ((y ball (C) r) \cap Y \subseteq x \land u \in (y ball (C) r)) \land u \in Y)$
103	79 102	bitr2i	$⊢ (\exists y \in x \exists r \in ℝ^{+} ((y ball (C) r) \cap Y \subseteq x \land u \in (y ball (C) r)) \land u \in Y) \leftrightarrow u \in (⋃ \{z \| (\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land z \cap Y \subseteq x)\} \cap Y)$
104	78 103	bitrdi	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land (x \subseteq Y \land \forall y \in x \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x)) \to (u \in x \leftrightarrow u \in (⋃ \{z \| (\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land z \cap Y \subseteq x)\} \cap Y))$
105	104	eqrdv	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land (x \subseteq Y \land \forall y \in x \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x)) \to x = ⋃ \{z \| (\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land z \cap Y \subseteq x)\} \cap Y$
106		ineq1	$⊢ u = ⋃ \{z \| (\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land z \cap Y \subseteq x)\} \to u \cap Y = ⋃ \{z \| (\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land z \cap Y \subseteq x)\} \cap Y$
107	106	rspceeqv	$⊢ (⋃ \{z \| (\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land z \cap Y \subseteq x)\} \in J \land x = ⋃ \{z \| (\exists y \in x \exists r \in ℝ^{+} z = y ball (C) r \land z \cap Y \subseteq x)\} \cap Y) \to \exists u \in J x = u \cap Y$
108	43 105 107	syl2anc	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land (x \subseteq Y \land \forall y \in x \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x)) \to \exists u \in J x = u \cap Y$
109	108	ex	$⊢ (C \in ∞Met (X) \land Y \subseteq X) \to ((x \subseteq Y \land \forall y \in x \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x) \to \exists u \in J x = u \cap Y)$
110	22 109	impbid	$⊢ (C \in ∞Met (X) \land Y \subseteq X) \to (\exists u \in J x = u \cap Y \leftrightarrow (x \subseteq Y \land \forall y \in x \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x))$
111		simpr	$⊢ (Y \subseteq X \land y \in Y) \to y \in Y$
112	26 111	elind	$⊢ (Y \subseteq X \land y \in Y) \to y \in (X \cap Y)$
113	1	blres	$⊢ (C \in ∞Met (X) \land y \in (X \cap Y) \land r \in ℝ^{*}) \to y ball (D) r = (y ball (C) r) \cap Y$
114	113	sseq1d	$⊢ (C \in ∞Met (X) \land y \in (X \cap Y) \land r \in ℝ^{*}) \to (y ball (D) r \subseteq x \leftrightarrow (y ball (C) r) \cap Y \subseteq x)$
115	114	3expa	$⊢ ((C \in ∞Met (X) \land y \in (X \cap Y)) \land r \in ℝ^{*}) \to (y ball (D) r \subseteq x \leftrightarrow (y ball (C) r) \cap Y \subseteq x)$
116	27 115	sylan2	$⊢ ((C \in ∞Met (X) \land y \in (X \cap Y)) \land r \in ℝ^{+}) \to (y ball (D) r \subseteq x \leftrightarrow (y ball (C) r) \cap Y \subseteq x)$
117	116	rexbidva	$⊢ (C \in ∞Met (X) \land y \in (X \cap Y)) \to (\exists r \in ℝ^{+} y ball (D) r \subseteq x \leftrightarrow \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x)$
118	112 117	sylan2	$⊢ (C \in ∞Met (X) \land (Y \subseteq X \land y \in Y)) \to (\exists r \in ℝ^{+} y ball (D) r \subseteq x \leftrightarrow \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x)$
119	118	anassrs	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land y \in Y) \to (\exists r \in ℝ^{+} y ball (D) r \subseteq x \leftrightarrow \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x)$
120	25 119	sylan2	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land (x \subseteq Y \land y \in x)) \to (\exists r \in ℝ^{+} y ball (D) r \subseteq x \leftrightarrow \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x)$
121	120	anassrs	$⊢ (((C \in ∞Met (X) \land Y \subseteq X) \land x \subseteq Y) \land y \in x) \to (\exists r \in ℝ^{+} y ball (D) r \subseteq x \leftrightarrow \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x)$
122	121	ralbidva	$⊢ ((C \in ∞Met (X) \land Y \subseteq X) \land x \subseteq Y) \to (\forall y \in x \exists r \in ℝ^{+} y ball (D) r \subseteq x \leftrightarrow \forall y \in x \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x)$
123	122	pm5.32da	$⊢ (C \in ∞Met (X) \land Y \subseteq X) \to ((x \subseteq Y \land \forall y \in x \exists r \in ℝ^{+} y ball (D) r \subseteq x) \leftrightarrow (x \subseteq Y \land \forall y \in x \exists r \in ℝ^{+} (y ball (C) r) \cap Y \subseteq x))$
124	110 123	bitr4d	$⊢ (C \in ∞Met (X) \land Y \subseteq X) \to (\exists u \in J x = u \cap Y \leftrightarrow (x \subseteq Y \land \forall y \in x \exists r \in ℝ^{+} y ball (D) r \subseteq x))$
125		id	$⊢ Y \subseteq X \to Y \subseteq X$
126	2	mopnm	$⊢ C \in ∞Met (X) \to X \in J$
127		ssexg	$⊢ (Y \subseteq X \land X \in J) \to Y \in V$
128	125 126 127	syl2anr	$⊢ (C \in ∞Met (X) \land Y \subseteq X) \to Y \in V$
129		elrest	$⊢ (J \in Top \land Y \in V) \to (x \in (J ↾_{𝑡} Y) \leftrightarrow \exists u \in J x = u \cap Y)$
130	23 128 129	syl2an2r	$⊢ (C \in ∞Met (X) \land Y \subseteq X) \to (x \in (J ↾_{𝑡} Y) \leftrightarrow \exists u \in J x = u \cap Y)$
131		xmetres2	$⊢ (C \in ∞Met (X) \land Y \subseteq X) \to {C ↾}_{(Y \times Y)} \in ∞Met (Y)$
132	1 131	eqeltrid	$⊢ (C \in ∞Met (X) \land Y \subseteq X) \to D \in ∞Met (Y)$
133	3	elmopn2	$⊢ D \in ∞Met (Y) \to (x \in K \leftrightarrow (x \subseteq Y \land \forall y \in x \exists r \in ℝ^{+} y ball (D) r \subseteq x))$
134	132 133	syl	$⊢ (C \in ∞Met (X) \land Y \subseteq X) \to (x \in K \leftrightarrow (x \subseteq Y \land \forall y \in x \exists r \in ℝ^{+} y ball (D) r \subseteq x))$
135	124 130 134	3bitr4d	$⊢ (C \in ∞Met (X) \land Y \subseteq X) \to (x \in (J ↾_{𝑡} Y) \leftrightarrow x \in K)$
136	135	eqrdv	$⊢ (C \in ∞Met (X) \land Y \subseteq X) \to J ↾_{𝑡} Y = K$

Metamath Proof Explorer

Theorem metrest

Proof