prdsxmslem2

Description: Lemma for prdsxms . The topology generated by the supremum metric is the same as the product topology, when the index set is finite. (Contributed by Mario Carneiro, 28-Aug-2015)

	Ref	Expression
Hypotheses	prdsxms.y	$⊢ Y = S ⨉_{𝑠} R$
	prdsxms.s	$⊢ φ \to S \in W$
	prdsxms.i	$⊢ φ \to I \in Fin$
	prdsxms.d	$⊢ D = dist (Y)$
	prdsxms.b	$⊢ B = {Base}_{Y}$
	prdsxms.r	$⊢ φ \to R : I ⟶ ∞MetSp$
	prdsxms.j	$⊢ J = TopOpen (Y)$
	prdsxms.v	$⊢ V = {Base}_{R (k)}$
	prdsxms.e	$⊢ E = {dist (R (k)) ↾}_{(V \times V)}$
	prdsxms.k	$⊢ K = TopOpen (R (k))$
	prdsxms.c	$⊢ C = \{x \| \exists g ((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k) \land \exists z \in Fin \forall k \in (I ∖ z) g (k) = ⋃ (TopOpen \circ R) (k)) \land x = \underset{k \in I}{⨉} g (k))\}$
Assertion	prdsxmslem2	$⊢ φ \to J = MetOpen (D)$

Proof

Step	Hyp	Ref	Expression
1		prdsxms.y	$⊢ Y = S ⨉_{𝑠} R$
2		prdsxms.s	$⊢ φ \to S \in W$
3		prdsxms.i	$⊢ φ \to I \in Fin$
4		prdsxms.d	$⊢ D = dist (Y)$
5		prdsxms.b	$⊢ B = {Base}_{Y}$
6		prdsxms.r	$⊢ φ \to R : I ⟶ ∞MetSp$
7		prdsxms.j	$⊢ J = TopOpen (Y)$
8		prdsxms.v	$⊢ V = {Base}_{R (k)}$
9		prdsxms.e	$⊢ E = {dist (R (k)) ↾}_{(V \times V)}$
10		prdsxms.k	$⊢ K = TopOpen (R (k))$
11		prdsxms.c	$⊢ C = \{x \| \exists g ((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k) \land \exists z \in Fin \forall k \in (I ∖ z) g (k) = ⋃ (TopOpen \circ R) (k)) \land x = \underset{k \in I}{⨉} g (k))\}$
12		topnfn	$⊢ TopOpen Fn V$
13	6	ffnd	$⊢ φ \to R Fn I$
14		dffn2	$⊢ R Fn I \leftrightarrow R : I ⟶ V$
15	13 14	sylib	$⊢ φ \to R : I ⟶ V$
16		fnfco	$⊢ (TopOpen Fn V \land R : I ⟶ V) \to (TopOpen \circ R) Fn I$
17	12 15 16	sylancr	$⊢ φ \to (TopOpen \circ R) Fn I$
18	11	ptval	$⊢ (I \in Fin \land (TopOpen \circ R) Fn I) \to \prod_{𝑡} (TopOpen \circ R) = topGen (C)$
19	3 17 18	syl2anc	$⊢ φ \to \prod_{𝑡} (TopOpen \circ R) = topGen (C)$
20		eldifsn	$⊢ x \in (ran ball (D) ∖ \{\emptyset\}) \leftrightarrow (x \in ran ball (D) \land x \neq \emptyset)$
21	1 2 3 4 5 6	prdsxmslem1	$⊢ φ \to D \in ∞Met (B)$
22		blrn	$⊢ D \in ∞Met (B) \to (x \in ran ball (D) \leftrightarrow \exists p \in B \exists r \in ℝ^{*} x = p ball (D) r)$
23	21 22	syl	$⊢ φ \to (x \in ran ball (D) \leftrightarrow \exists p \in B \exists r \in ℝ^{*} x = p ball (D) r)$
24	21	adantr	$⊢ (φ \land (p \in B \land r \in ℝ^{*})) \to D \in ∞Met (B)$
25		simprl	$⊢ (φ \land (p \in B \land r \in ℝ^{*})) \to p \in B$
26		simprr	$⊢ (φ \land (p \in B \land r \in ℝ^{})) \to r \in ℝ^{}$
27		xbln0	$⊢ (D \in ∞Met (B) \land p \in B \land r \in ℝ^{*}) \to (p ball (D) r \neq \emptyset \leftrightarrow 0 < r)$
28	24 25 26 27	syl3anc	$⊢ (φ \land (p \in B \land r \in ℝ^{*})) \to (p ball (D) r \neq \emptyset \leftrightarrow 0 < r)$
29	3	3ad2ant1	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to I \in Fin$
30	29	mptexd	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) \in V$
31		ovex	$⊢ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r \in V$
32	31	rgenw	$⊢ \forall n \in I p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r \in V$
33		eqid	$⊢ (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) = (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r)$
34	33	fnmpt	$⊢ \forall n \in I p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r \in V \to (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) Fn I$
35	32 34	mp1i	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) Fn I$
36	6	3ad2ant1	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to R : I ⟶ ∞MetSp$
37	36	ffvelcdmda	$⊢ ((φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \land k \in I) \to R (k) \in ∞MetSp$
38	8 9	xmsxmet	$⊢ R (k) \in ∞MetSp \to E \in ∞Met (V)$
39	37 38	syl	$⊢ ((φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \land k \in I) \to E \in ∞Met (V)$
40		eqid	$⊢ S ⨉_{𝑠} (k \in I ⟼ R (k)) = S ⨉_{𝑠} (k \in I ⟼ R (k))$
41		eqid	$⊢ {Base}_{(S ⨉_{𝑠} (k \in I ⟼ R (k)))} = {Base}_{(S ⨉_{𝑠} (k \in I ⟼ R (k)))}$
42	2	3ad2ant1	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to S \in W$
43	37	ralrimiva	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to \forall k \in I R (k) \in ∞MetSp$
44		simp2l	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to p \in B$
45	36	feqmptd	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to R = (k \in I ⟼ R (k))$
46	45	oveq2d	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to S ⨉_{𝑠} R = S ⨉_{𝑠} (k \in I ⟼ R (k))$
47	1 46	eqtrid	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to Y = S ⨉_{𝑠} (k \in I ⟼ R (k))$
48	47	fveq2d	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to {Base}_{Y} = {Base}_{(S ⨉_{𝑠} (k \in I ⟼ R (k)))}$
49	5 48	eqtrid	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to B = {Base}_{(S ⨉_{𝑠} (k \in I ⟼ R (k)))}$
50	44 49	eleqtrd	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to p \in {Base}_{(S ⨉_{𝑠} (k \in I ⟼ R (k)))}$
51	40 41 42 29 43 8 50	prdsbascl	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to \forall k \in I p (k) \in V$
52	51	r19.21bi	$⊢ ((φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \land k \in I) \to p (k) \in V$
53		simp2r	$⊢ (φ \land (p \in B \land r \in ℝ^{}) \land 0 < r) \to r \in ℝ^{}$
54	53	adantr	$⊢ ((φ \land (p \in B \land r \in ℝ^{}) \land 0 < r) \land k \in I) \to r \in ℝ^{}$
55		eqid	$⊢ MetOpen (E) = MetOpen (E)$
56	55	blopn	$⊢ (E \in ∞Met (V) \land p (k) \in V \land r \in ℝ^{*}) \to p (k) ball (E) r \in MetOpen (E)$
57	39 52 54 56	syl3anc	$⊢ ((φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \land k \in I) \to p (k) ball (E) r \in MetOpen (E)$
58		2fveq3	$⊢ n = k \to dist (R (n)) = dist (R (k))$
59		2fveq3	$⊢ n = k \to {Base}_{R (n)} = {Base}_{R (k)}$
60	59 8	eqtr4di	$⊢ n = k \to {Base}_{R (n)} = V$
61	60	sqxpeqd	$⊢ n = k \to {Base}_{R (n)} \times {Base}_{R (n)} = V \times V$
62	58 61	reseq12d	$⊢ n = k \to {dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})} = {dist (R (k)) ↾}_{(V \times V)}$
63	62 9	eqtr4di	$⊢ n = k \to {dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})} = E$
64	63	fveq2d	$⊢ n = k \to ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) = ball (E)$
65		fveq2	$⊢ n = k \to p (n) = p (k)$
66		eqidd	$⊢ n = k \to r = r$
67	64 65 66	oveq123d	$⊢ n = k \to p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r = p (k) ball (E) r$
68		ovex	$⊢ p (k) ball (E) r \in V$
69	67 33 68	fvmpt	$⊢ k \in I \to (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) (k) = p (k) ball (E) r$
70	69	adantl	$⊢ ((φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \land k \in I) \to (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) (k) = p (k) ball (E) r$
71		fvco3	$⊢ (R : I ⟶ ∞MetSp \land k \in I) \to (TopOpen \circ R) (k) = TopOpen (R (k))$
72	71 10	eqtr4di	$⊢ (R : I ⟶ ∞MetSp \land k \in I) \to (TopOpen \circ R) (k) = K$
73	36 72	sylan	$⊢ ((φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \land k \in I) \to (TopOpen \circ R) (k) = K$
74	10 8 9	xmstopn	$⊢ R (k) \in ∞MetSp \to K = MetOpen (E)$
75	37 74	syl	$⊢ ((φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \land k \in I) \to K = MetOpen (E)$
76	73 75	eqtrd	$⊢ ((φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \land k \in I) \to (TopOpen \circ R) (k) = MetOpen (E)$
77	57 70 76	3eltr4d	$⊢ ((φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \land k \in I) \to (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) (k) \in (TopOpen \circ R) (k)$
78	77	ralrimiva	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to \forall k \in I (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) (k) \in (TopOpen \circ R) (k)$
79	36	feqmptd	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to R = (n \in I ⟼ R (n))$
80	79	oveq2d	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to S ⨉_{𝑠} R = S ⨉_{𝑠} (n \in I ⟼ R (n))$
81	1 80	eqtrid	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to Y = S ⨉_{𝑠} (n \in I ⟼ R (n))$
82	81	fveq2d	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to dist (Y) = dist (S ⨉_{𝑠} (n \in I ⟼ R (n)))$
83	4 82	eqtrid	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to D = dist (S ⨉_{𝑠} (n \in I ⟼ R (n)))$
84	83	fveq2d	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to ball (D) = ball (dist (S ⨉_{𝑠} (n \in I ⟼ R (n))))$
85	84	oveqd	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to p ball (D) r = p ball (dist (S ⨉_{𝑠} (n \in I ⟼ R (n)))) r$
86		fveq2	$⊢ n = k \to R (n) = R (k)$
87	86	cbvmptv	$⊢ (n \in I ⟼ R (n)) = (k \in I ⟼ R (k))$
88	87	oveq2i	$⊢ S ⨉_{𝑠} (n \in I ⟼ R (n)) = S ⨉_{𝑠} (k \in I ⟼ R (k))$
89		eqid	$⊢ {Base}_{(S ⨉_{𝑠} (n \in I ⟼ R (n)))} = {Base}_{(S ⨉_{𝑠} (n \in I ⟼ R (n)))}$
90		eqid	$⊢ dist (S ⨉_{𝑠} (n \in I ⟼ R (n))) = dist (S ⨉_{𝑠} (n \in I ⟼ R (n)))$
91	81	fveq2d	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to {Base}_{Y} = {Base}_{(S ⨉_{𝑠} (n \in I ⟼ R (n)))}$
92	5 91	eqtrid	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to B = {Base}_{(S ⨉_{𝑠} (n \in I ⟼ R (n)))}$
93	44 92	eleqtrd	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to p \in {Base}_{(S ⨉_{𝑠} (n \in I ⟼ R (n)))}$
94		simp3	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to 0 < r$
95	88 89 8 9 90 42 29 37 39 93 53 94	prdsbl	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to p ball (dist (S ⨉_{𝑠} (n \in I ⟼ R (n)))) r = \underset{k \in I}{⨉} (p (k) ball (E) r)$
96	85 95	eqtrd	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to p ball (D) r = \underset{k \in I}{⨉} (p (k) ball (E) r)$
97		fneq1	$⊢ g = (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) \to (g Fn I \leftrightarrow (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) Fn I)$
98		fveq1	$⊢ g = (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) \to g (k) = (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) (k)$
99	98	eleq1d	$⊢ g = (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) \to (g (k) \in (TopOpen \circ R) (k) \leftrightarrow (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) (k) \in (TopOpen \circ R) (k))$
100	99	ralbidv	$⊢ g = (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) \to (\forall k \in I g (k) \in (TopOpen \circ R) (k) \leftrightarrow \forall k \in I (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) (k) \in (TopOpen \circ R) (k))$
101	97 100	anbi12d	$⊢ g = (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) \to ((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k)) \leftrightarrow ((n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) Fn I \land \forall k \in I (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) (k) \in (TopOpen \circ R) (k)))$
102	98 69	sylan9eq	$⊢ (g = (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) \land k \in I) \to g (k) = p (k) ball (E) r$
103	102	ixpeq2dva	$⊢ g = (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) \to \underset{k \in I}{⨉} g (k) = \underset{k \in I}{⨉} (p (k) ball (E) r)$
104	103	eqeq2d	$⊢ g = (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) \to (p ball (D) r = \underset{k \in I}{⨉} g (k) \leftrightarrow p ball (D) r = \underset{k \in I}{⨉} (p (k) ball (E) r))$
105	101 104	anbi12d	$⊢ g = (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) \to (((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k)) \land p ball (D) r = \underset{k \in I}{⨉} g (k)) \leftrightarrow (((n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) Fn I \land \forall k \in I (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) (k) \in (TopOpen \circ R) (k)) \land p ball (D) r = \underset{k \in I}{⨉} (p (k) ball (E) r)))$
106	105	spcegv	$⊢ (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) \in V \to ((((n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) Fn I \land \forall k \in I (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) (k) \in (TopOpen \circ R) (k)) \land p ball (D) r = \underset{k \in I}{⨉} (p (k) ball (E) r)) \to \exists g ((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k)) \land p ball (D) r = \underset{k \in I}{⨉} g (k)))$
107	106	3impib	$⊢ ((n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) \in V \land ((n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) Fn I \land \forall k \in I (n \in I ⟼ p (n) ball ({dist (R (n)) ↾}_{({Base}_{R (n)} \times {Base}_{R (n)})}) r) (k) \in (TopOpen \circ R) (k)) \land p ball (D) r = \underset{k \in I}{⨉} (p (k) ball (E) r)) \to \exists g ((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k)) \land p ball (D) r = \underset{k \in I}{⨉} g (k))$
108	30 35 78 96 107	syl121anc	$⊢ (φ \land (p \in B \land r \in ℝ^{*}) \land 0 < r) \to \exists g ((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k)) \land p ball (D) r = \underset{k \in I}{⨉} g (k))$
109	108	3expia	$⊢ (φ \land (p \in B \land r \in ℝ^{*})) \to (0 < r \to \exists g ((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k)) \land p ball (D) r = \underset{k \in I}{⨉} g (k)))$
110	28 109	sylbid	$⊢ (φ \land (p \in B \land r \in ℝ^{*})) \to (p ball (D) r \neq \emptyset \to \exists g ((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k)) \land p ball (D) r = \underset{k \in I}{⨉} g (k)))$
111	110	adantr	$⊢ ((φ \land (p \in B \land r \in ℝ^{*})) \land x = p ball (D) r) \to (p ball (D) r \neq \emptyset \to \exists g ((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k)) \land p ball (D) r = \underset{k \in I}{⨉} g (k)))$
112		simpr	$⊢ ((φ \land (p \in B \land r \in ℝ^{*})) \land x = p ball (D) r) \to x = p ball (D) r$
113	112	neeq1d	$⊢ ((φ \land (p \in B \land r \in ℝ^{*})) \land x = p ball (D) r) \to (x \neq \emptyset \leftrightarrow p ball (D) r \neq \emptyset)$
114		df-3an	$⊢ (g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k) \land \exists z \in Fin \forall k \in (I ∖ z) g (k) = ⋃ (TopOpen \circ R) (k)) \leftrightarrow ((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k)) \land \exists z \in Fin \forall k \in (I ∖ z) g (k) = ⋃ (TopOpen \circ R) (k))$
115		ral0	$⊢ \forall k \in \emptyset g (k) = ⋃ (TopOpen \circ R) (k)$
116		difeq2	$⊢ z = I \to I ∖ z = I ∖ I$
117		difid	$⊢ I ∖ I = \emptyset$
118	116 117	eqtrdi	$⊢ z = I \to I ∖ z = \emptyset$
119	118	raleqdv	$⊢ z = I \to (\forall k \in (I ∖ z) g (k) = ⋃ (TopOpen \circ R) (k) \leftrightarrow \forall k \in \emptyset g (k) = ⋃ (TopOpen \circ R) (k))$
120	119	rspcev	$⊢ (I \in Fin \land \forall k \in \emptyset g (k) = ⋃ (TopOpen \circ R) (k)) \to \exists z \in Fin \forall k \in (I ∖ z) g (k) = ⋃ (TopOpen \circ R) (k)$
121	3 115 120	sylancl	$⊢ φ \to \exists z \in Fin \forall k \in (I ∖ z) g (k) = ⋃ (TopOpen \circ R) (k)$
122	121	adantr	$⊢ (φ \land (p \in B \land r \in ℝ^{*})) \to \exists z \in Fin \forall k \in (I ∖ z) g (k) = ⋃ (TopOpen \circ R) (k)$
123	122	biantrud	$⊢ (φ \land (p \in B \land r \in ℝ^{*})) \to ((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k)) \leftrightarrow ((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k)) \land \exists z \in Fin \forall k \in (I ∖ z) g (k) = ⋃ (TopOpen \circ R) (k)))$
124	114 123	bitr4id	$⊢ (φ \land (p \in B \land r \in ℝ^{*})) \to ((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k) \land \exists z \in Fin \forall k \in (I ∖ z) g (k) = ⋃ (TopOpen \circ R) (k)) \leftrightarrow (g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k)))$
125		eqeq1	$⊢ x = p ball (D) r \to (x = \underset{k \in I}{⨉} g (k) \leftrightarrow p ball (D) r = \underset{k \in I}{⨉} g (k))$
126	124 125	bi2anan9	$⊢ ((φ \land (p \in B \land r \in ℝ^{*})) \land x = p ball (D) r) \to (((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k) \land \exists z \in Fin \forall k \in (I ∖ z) g (k) = ⋃ (TopOpen \circ R) (k)) \land x = \underset{k \in I}{⨉} g (k)) \leftrightarrow ((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k)) \land p ball (D) r = \underset{k \in I}{⨉} g (k)))$
127	126	exbidv	$⊢ ((φ \land (p \in B \land r \in ℝ^{*})) \land x = p ball (D) r) \to (\exists g ((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k) \land \exists z \in Fin \forall k \in (I ∖ z) g (k) = ⋃ (TopOpen \circ R) (k)) \land x = \underset{k \in I}{⨉} g (k)) \leftrightarrow \exists g ((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k)) \land p ball (D) r = \underset{k \in I}{⨉} g (k)))$
128	111 113 127	3imtr4d	$⊢ ((φ \land (p \in B \land r \in ℝ^{*})) \land x = p ball (D) r) \to (x \neq \emptyset \to \exists g ((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k) \land \exists z \in Fin \forall k \in (I ∖ z) g (k) = ⋃ (TopOpen \circ R) (k)) \land x = \underset{k \in I}{⨉} g (k)))$
129	128	ex	$⊢ (φ \land (p \in B \land r \in ℝ^{*})) \to (x = p ball (D) r \to (x \neq \emptyset \to \exists g ((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k) \land \exists z \in Fin \forall k \in (I ∖ z) g (k) = ⋃ (TopOpen \circ R) (k)) \land x = \underset{k \in I}{⨉} g (k))))$
130	129	rexlimdvva	$⊢ φ \to (\exists p \in B \exists r \in ℝ^{*} x = p ball (D) r \to (x \neq \emptyset \to \exists g ((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k) \land \exists z \in Fin \forall k \in (I ∖ z) g (k) = ⋃ (TopOpen \circ R) (k)) \land x = \underset{k \in I}{⨉} g (k))))$
131	23 130	sylbid	$⊢ φ \to (x \in ran ball (D) \to (x \neq \emptyset \to \exists g ((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k) \land \exists z \in Fin \forall k \in (I ∖ z) g (k) = ⋃ (TopOpen \circ R) (k)) \land x = \underset{k \in I}{⨉} g (k))))$
132	131	impd	$⊢ φ \to ((x \in ran ball (D) \land x \neq \emptyset) \to \exists g ((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k) \land \exists z \in Fin \forall k \in (I ∖ z) g (k) = ⋃ (TopOpen \circ R) (k)) \land x = \underset{k \in I}{⨉} g (k)))$
133	20 132	biimtrid	$⊢ φ \to (x \in (ran ball (D) ∖ \{\emptyset\}) \to \exists g ((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k) \land \exists z \in Fin \forall k \in (I ∖ z) g (k) = ⋃ (TopOpen \circ R) (k)) \land x = \underset{k \in I}{⨉} g (k)))$
134	133	alrimiv	$⊢ φ \to \forall x (x \in (ran ball (D) ∖ \{\emptyset\}) \to \exists g ((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k) \land \exists z \in Fin \forall k \in (I ∖ z) g (k) = ⋃ (TopOpen \circ R) (k)) \land x = \underset{k \in I}{⨉} g (k)))$
135		ssab	$⊢ ran ball (D) ∖ \{\emptyset\} \subseteq \{x \| \exists g ((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k) \land \exists z \in Fin \forall k \in (I ∖ z) g (k) = ⋃ (TopOpen \circ R) (k)) \land x = \underset{k \in I}{⨉} g (k))\} \leftrightarrow \forall x (x \in (ran ball (D) ∖ \{\emptyset\}) \to \exists g ((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k) \land \exists z \in Fin \forall k \in (I ∖ z) g (k) = ⋃ (TopOpen \circ R) (k)) \land x = \underset{k \in I}{⨉} g (k)))$
136	134 135	sylibr	$⊢ φ \to ran ball (D) ∖ \{\emptyset\} \subseteq \{x \| \exists g ((g Fn I \land \forall k \in I g (k) \in (TopOpen \circ R) (k) \land \exists z \in Fin \forall k \in (I ∖ z) g (k) = ⋃ (TopOpen \circ R) (k)) \land x = \underset{k \in I}{⨉} g (k))\}$
137	136 11	sseqtrrdi	$⊢ φ \to ran ball (D) ∖ \{\emptyset\} \subseteq C$
138		ssv	$⊢ ∞MetSp \subseteq V$
139		fnssres	$⊢ (TopOpen Fn V \land ∞MetSp \subseteq V) \to ({TopOpen ↾}_{∞MetSp}) Fn ∞MetSp$
140	12 138 139	mp2an	$⊢ ({TopOpen ↾}_{∞MetSp}) Fn ∞MetSp$
141		fvres	$⊢ x \in ∞MetSp \to ({TopOpen ↾}_{∞MetSp}) (x) = TopOpen (x)$
142		xmstps	$⊢ x \in ∞MetSp \to x \in TopSp$
143		eqid	$⊢ TopOpen (x) = TopOpen (x)$
144	143	tpstop	$⊢ x \in TopSp \to TopOpen (x) \in Top$
145	142 144	syl	$⊢ x \in ∞MetSp \to TopOpen (x) \in Top$
146	141 145	eqeltrd	$⊢ x \in ∞MetSp \to ({TopOpen ↾}_{∞MetSp}) (x) \in Top$
147	146	rgen	$⊢ \forall x \in ∞MetSp ({TopOpen ↾}_{∞MetSp}) (x) \in Top$
148		ffnfv	$⊢ ({TopOpen ↾}_{∞MetSp}) : ∞MetSp ⟶ Top \leftrightarrow (({TopOpen ↾}_{∞MetSp}) Fn ∞MetSp \land \forall x \in ∞MetSp ({TopOpen ↾}_{∞MetSp}) (x) \in Top)$
149	140 147 148	mpbir2an	$⊢ ({TopOpen ↾}_{∞MetSp}) : ∞MetSp ⟶ Top$
150		fco2	$⊢ (({TopOpen ↾}_{∞MetSp}) : ∞MetSp ⟶ Top \land R : I ⟶ ∞MetSp) \to (TopOpen \circ R) : I ⟶ Top$
151	149 6 150	sylancr	$⊢ φ \to (TopOpen \circ R) : I ⟶ Top$
152		eqid	$⊢ \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) = \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n)$
153	11 152	ptbasfi	$⊢ (I \in Fin \land (TopOpen \circ R) : I ⟶ Top) \to C = fi (\{\underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n)\} \cup ran (m \in I, u \in (TopOpen \circ R) (m) ⟼ {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (m))}^{-1} [u]))$
154	3 151 153	syl2anc	$⊢ φ \to C = fi (\{\underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n)\} \cup ran (m \in I, u \in (TopOpen \circ R) (m) ⟼ {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (m))}^{-1} [u]))$
155		eqid	$⊢ MetOpen (D) = MetOpen (D)$
156	155	mopntop	$⊢ D \in ∞Met (B) \to MetOpen (D) \in Top$
157	21 156	syl	$⊢ φ \to MetOpen (D) \in Top$
158	1 5 2 3 13	prdsbas2	$⊢ φ \to B = \underset{k \in I}{⨉} {Base}_{R (k)}$
159	6 72	sylan	$⊢ (φ \land k \in I) \to (TopOpen \circ R) (k) = K$
160	6	ffvelcdmda	$⊢ (φ \land k \in I) \to R (k) \in ∞MetSp$
161		xmstps	$⊢ R (k) \in ∞MetSp \to R (k) \in TopSp$
162	160 161	syl	$⊢ (φ \land k \in I) \to R (k) \in TopSp$
163	8 10	istps	$⊢ R (k) \in TopSp \leftrightarrow K \in TopOn (V)$
164	162 163	sylib	$⊢ (φ \land k \in I) \to K \in TopOn (V)$
165	159 164	eqeltrd	$⊢ (φ \land k \in I) \to (TopOpen \circ R) (k) \in TopOn (V)$
166		toponuni	$⊢ (TopOpen \circ R) (k) \in TopOn (V) \to V = ⋃ (TopOpen \circ R) (k)$
167	165 166	syl	$⊢ (φ \land k \in I) \to V = ⋃ (TopOpen \circ R) (k)$
168	8 167	eqtr3id	$⊢ (φ \land k \in I) \to {Base}_{R (k)} = ⋃ (TopOpen \circ R) (k)$
169	168	ixpeq2dva	$⊢ φ \to \underset{k \in I}{⨉} {Base}_{R (k)} = \underset{k \in I}{⨉} ⋃ (TopOpen \circ R) (k)$
170	158 169	eqtrd	$⊢ φ \to B = \underset{k \in I}{⨉} ⋃ (TopOpen \circ R) (k)$
171		fveq2	$⊢ k = n \to (TopOpen \circ R) (k) = (TopOpen \circ R) (n)$
172	171	unieqd	$⊢ k = n \to ⋃ (TopOpen \circ R) (k) = ⋃ (TopOpen \circ R) (n)$
173	172	cbvixpv	$⊢ \underset{k \in I}{⨉} ⋃ (TopOpen \circ R) (k) = \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n)$
174	170 173	eqtrdi	$⊢ φ \to B = \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n)$
175	155	mopntopon	$⊢ D \in ∞Met (B) \to MetOpen (D) \in TopOn (B)$
176	21 175	syl	$⊢ φ \to MetOpen (D) \in TopOn (B)$
177		toponmax	$⊢ MetOpen (D) \in TopOn (B) \to B \in MetOpen (D)$
178	176 177	syl	$⊢ φ \to B \in MetOpen (D)$
179	174 178	eqeltrrd	$⊢ φ \to \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) \in MetOpen (D)$
180	179	snssd	$⊢ φ \to \{\underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n)\} \subseteq MetOpen (D)$
181	174	mpteq1d	$⊢ φ \to (w \in B ⟼ w (k)) = (w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (k))$
182	181	ad2antrr	$⊢ ((φ \land k \in I) \land u \in K) \to (w \in B ⟼ w (k)) = (w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (k))$
183	182	cnveqd	$⊢ ((φ \land k \in I) \land u \in K) \to {(w \in B ⟼ w (k))}^{-1} = {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (k))}^{-1}$
184	183	imaeq1d	$⊢ ((φ \land k \in I) \land u \in K) \to {(w \in B ⟼ w (k))}^{-1} [u] = {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (k))}^{-1} [u]$
185		fveq1	$⊢ w = p \to w (k) = p (k)$
186	185	eleq1d	$⊢ w = p \to (w (k) \in u \leftrightarrow p (k) \in u)$
187		eqid	$⊢ (w \in B ⟼ w (k)) = (w \in B ⟼ w (k))$
188	187	mptpreima	$⊢ {(w \in B ⟼ w (k))}^{-1} [u] = \{w \in B \| w (k) \in u\}$
189	186 188	elrab2	$⊢ p \in {(w \in B ⟼ w (k))}^{-1} [u] \leftrightarrow (p \in B \land p (k) \in u)$
190	160 38	syl	$⊢ (φ \land k \in I) \to E \in ∞Met (V)$
191	190	adantr	$⊢ ((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \to E \in ∞Met (V)$
192		simprl	$⊢ ((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \to u \in K$
193	160 74	syl	$⊢ (φ \land k \in I) \to K = MetOpen (E)$
194	193	adantr	$⊢ ((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \to K = MetOpen (E)$
195	192 194	eleqtrd	$⊢ ((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \to u \in MetOpen (E)$
196		simprrr	$⊢ ((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \to p (k) \in u$
197	55	mopni2	$⊢ (E \in ∞Met (V) \land u \in MetOpen (E) \land p (k) \in u) \to \exists r \in ℝ^{+} p (k) ball (E) r \subseteq u$
198	191 195 196 197	syl3anc	$⊢ ((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \to \exists r \in ℝ^{+} p (k) ball (E) r \subseteq u$
199	21	ad3antrrr	$⊢ (((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \land (r \in ℝ^{+} \land p (k) ball (E) r \subseteq u)) \to D \in ∞Met (B)$
200		simprrl	$⊢ ((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \to p \in B$
201	200	adantr	$⊢ (((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \land (r \in ℝ^{+} \land p (k) ball (E) r \subseteq u)) \to p \in B$
202		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
203	202	ad2antrl	$⊢ (((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \land (r \in ℝ^{+} \land p (k) ball (E) r \subseteq u)) \to r \in ℝ^{*}$
204	155	blopn	$⊢ (D \in ∞Met (B) \land p \in B \land r \in ℝ^{*}) \to p ball (D) r \in MetOpen (D)$
205	199 201 203 204	syl3anc	$⊢ (((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \land (r \in ℝ^{+} \land p (k) ball (E) r \subseteq u)) \to p ball (D) r \in MetOpen (D)$
206		simprl	$⊢ (((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \land (r \in ℝ^{+} \land p (k) ball (E) r \subseteq u)) \to r \in ℝ^{+}$
207		blcntr	$⊢ (D \in ∞Met (B) \land p \in B \land r \in ℝ^{+}) \to p \in (p ball (D) r)$
208	199 201 206 207	syl3anc	$⊢ (((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \land (r \in ℝ^{+} \land p (k) ball (E) r \subseteq u)) \to p \in (p ball (D) r)$
209		blssm	$⊢ (D \in ∞Met (B) \land p \in B \land r \in ℝ^{*}) \to p ball (D) r \subseteq B$
210	199 201 203 209	syl3anc	$⊢ (((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \land (r \in ℝ^{+} \land p (k) ball (E) r \subseteq u)) \to p ball (D) r \subseteq B$
211		simplrr	$⊢ ((((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \land (r \in ℝ^{+} \land p (k) ball (E) r \subseteq u)) \land w \in (p ball (D) r)) \to p (k) ball (E) r \subseteq u$
212		simplll	$⊢ (((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \land (r \in ℝ^{+} \land p (k) ball (E) r \subseteq u)) \to φ$
213		rpgt0	$⊢ r \in ℝ^{+} \to 0 < r$
214	213	ad2antrl	$⊢ (((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \land (r \in ℝ^{+} \land p (k) ball (E) r \subseteq u)) \to 0 < r$
215	212 201 203 214 96	syl121anc	$⊢ (((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \land (r \in ℝ^{+} \land p (k) ball (E) r \subseteq u)) \to p ball (D) r = \underset{k \in I}{⨉} (p (k) ball (E) r)$
216	215	eleq2d	$⊢ (((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \land (r \in ℝ^{+} \land p (k) ball (E) r \subseteq u)) \to (w \in (p ball (D) r) \leftrightarrow w \in \underset{k \in I}{⨉} (p (k) ball (E) r))$
217	216	biimpa	$⊢ ((((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \land (r \in ℝ^{+} \land p (k) ball (E) r \subseteq u)) \land w \in (p ball (D) r)) \to w \in \underset{k \in I}{⨉} (p (k) ball (E) r)$
218		vex	$⊢ w \in V$
219	218	elixp	$⊢ w \in \underset{k \in I}{⨉} (p (k) ball (E) r) \leftrightarrow (w Fn I \land \forall k \in I w (k) \in (p (k) ball (E) r))$
220	219	simprbi	$⊢ w \in \underset{k \in I}{⨉} (p (k) ball (E) r) \to \forall k \in I w (k) \in (p (k) ball (E) r)$
221	217 220	syl	$⊢ ((((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \land (r \in ℝ^{+} \land p (k) ball (E) r \subseteq u)) \land w \in (p ball (D) r)) \to \forall k \in I w (k) \in (p (k) ball (E) r)$
222		simp-4r	$⊢ ((((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \land (r \in ℝ^{+} \land p (k) ball (E) r \subseteq u)) \land w \in (p ball (D) r)) \to k \in I$
223		rsp	$⊢ \forall k \in I w (k) \in (p (k) ball (E) r) \to (k \in I \to w (k) \in (p (k) ball (E) r))$
224	221 222 223	sylc	$⊢ ((((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \land (r \in ℝ^{+} \land p (k) ball (E) r \subseteq u)) \land w \in (p ball (D) r)) \to w (k) \in (p (k) ball (E) r)$
225	211 224	sseldd	$⊢ ((((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \land (r \in ℝ^{+} \land p (k) ball (E) r \subseteq u)) \land w \in (p ball (D) r)) \to w (k) \in u$
226	210 225	ssrabdv	$⊢ (((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \land (r \in ℝ^{+} \land p (k) ball (E) r \subseteq u)) \to p ball (D) r \subseteq \{w \in B \| w (k) \in u\}$
227	226 188	sseqtrrdi	$⊢ (((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \land (r \in ℝ^{+} \land p (k) ball (E) r \subseteq u)) \to p ball (D) r \subseteq {(w \in B ⟼ w (k))}^{-1} [u]$
228		eleq2	$⊢ y = p ball (D) r \to (p \in y \leftrightarrow p \in (p ball (D) r))$
229		sseq1	$⊢ y = p ball (D) r \to (y \subseteq {(w \in B ⟼ w (k))}^{-1} [u] \leftrightarrow p ball (D) r \subseteq {(w \in B ⟼ w (k))}^{-1} [u])$
230	228 229	anbi12d	$⊢ y = p ball (D) r \to ((p \in y \land y \subseteq {(w \in B ⟼ w (k))}^{-1} [u]) \leftrightarrow (p \in (p ball (D) r) \land p ball (D) r \subseteq {(w \in B ⟼ w (k))}^{-1} [u]))$
231	230	rspcev	$⊢ (p ball (D) r \in MetOpen (D) \land (p \in (p ball (D) r) \land p ball (D) r \subseteq {(w \in B ⟼ w (k))}^{-1} [u])) \to \exists y \in MetOpen (D) (p \in y \land y \subseteq {(w \in B ⟼ w (k))}^{-1} [u])$
232	205 208 227 231	syl12anc	$⊢ (((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \land (r \in ℝ^{+} \land p (k) ball (E) r \subseteq u)) \to \exists y \in MetOpen (D) (p \in y \land y \subseteq {(w \in B ⟼ w (k))}^{-1} [u])$
233	198 232	rexlimddv	$⊢ ((φ \land k \in I) \land (u \in K \land (p \in B \land p (k) \in u))) \to \exists y \in MetOpen (D) (p \in y \land y \subseteq {(w \in B ⟼ w (k))}^{-1} [u])$
234	233	expr	$⊢ ((φ \land k \in I) \land u \in K) \to ((p \in B \land p (k) \in u) \to \exists y \in MetOpen (D) (p \in y \land y \subseteq {(w \in B ⟼ w (k))}^{-1} [u]))$
235	189 234	biimtrid	$⊢ ((φ \land k \in I) \land u \in K) \to (p \in {(w \in B ⟼ w (k))}^{-1} [u] \to \exists y \in MetOpen (D) (p \in y \land y \subseteq {(w \in B ⟼ w (k))}^{-1} [u]))$
236	235	ralrimiv	$⊢ ((φ \land k \in I) \land u \in K) \to \forall p \in {(w \in B ⟼ w (k))}^{-1} [u] \exists y \in MetOpen (D) (p \in y \land y \subseteq {(w \in B ⟼ w (k))}^{-1} [u])$
237	157	ad2antrr	$⊢ ((φ \land k \in I) \land u \in K) \to MetOpen (D) \in Top$
238		eltop2	$⊢ MetOpen (D) \in Top \to ({(w \in B ⟼ w (k))}^{-1} [u] \in MetOpen (D) \leftrightarrow \forall p \in {(w \in B ⟼ w (k))}^{-1} [u] \exists y \in MetOpen (D) (p \in y \land y \subseteq {(w \in B ⟼ w (k))}^{-1} [u]))$
239	237 238	syl	$⊢ ((φ \land k \in I) \land u \in K) \to ({(w \in B ⟼ w (k))}^{-1} [u] \in MetOpen (D) \leftrightarrow \forall p \in {(w \in B ⟼ w (k))}^{-1} [u] \exists y \in MetOpen (D) (p \in y \land y \subseteq {(w \in B ⟼ w (k))}^{-1} [u]))$
240	236 239	mpbird	$⊢ ((φ \land k \in I) \land u \in K) \to {(w \in B ⟼ w (k))}^{-1} [u] \in MetOpen (D)$
241	184 240	eqeltrrd	$⊢ ((φ \land k \in I) \land u \in K) \to {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (k))}^{-1} [u] \in MetOpen (D)$
242	241	ralrimiva	$⊢ (φ \land k \in I) \to \forall u \in K {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (k))}^{-1} [u] \in MetOpen (D)$
243	242 159	raleqtrrdv	$⊢ (φ \land k \in I) \to \forall u \in (TopOpen \circ R) (k) {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (k))}^{-1} [u] \in MetOpen (D)$
244	243	ralrimiva	$⊢ φ \to \forall k \in I \forall u \in (TopOpen \circ R) (k) {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (k))}^{-1} [u] \in MetOpen (D)$
245		fveq2	$⊢ k = m \to (TopOpen \circ R) (k) = (TopOpen \circ R) (m)$
246		fveq2	$⊢ k = m \to w (k) = w (m)$
247	246	mpteq2dv	$⊢ k = m \to (w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (k)) = (w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (m))$
248	247	cnveqd	$⊢ k = m \to {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (k))}^{-1} = {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (m))}^{-1}$
249	248	imaeq1d	$⊢ k = m \to {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (k))}^{-1} [u] = {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (m))}^{-1} [u]$
250	249	eleq1d	$⊢ k = m \to ({(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (k))}^{-1} [u] \in MetOpen (D) \leftrightarrow {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (m))}^{-1} [u] \in MetOpen (D))$
251	245 250	raleqbidv	$⊢ k = m \to (\forall u \in (TopOpen \circ R) (k) {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (k))}^{-1} [u] \in MetOpen (D) \leftrightarrow \forall u \in (TopOpen \circ R) (m) {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (m))}^{-1} [u] \in MetOpen (D))$
252	251	cbvralvw	$⊢ \forall k \in I \forall u \in (TopOpen \circ R) (k) {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (k))}^{-1} [u] \in MetOpen (D) \leftrightarrow \forall m \in I \forall u \in (TopOpen \circ R) (m) {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (m))}^{-1} [u] \in MetOpen (D)$
253	244 252	sylib	$⊢ φ \to \forall m \in I \forall u \in (TopOpen \circ R) (m) {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (m))}^{-1} [u] \in MetOpen (D)$
254		eqid	$⊢ (m \in I, u \in (TopOpen \circ R) (m) ⟼ {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (m))}^{-1} [u]) = (m \in I, u \in (TopOpen \circ R) (m) ⟼ {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (m))}^{-1} [u])$
255	254	fmpox	$⊢ \forall m \in I \forall u \in (TopOpen \circ R) (m) {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (m))}^{-1} [u] \in MetOpen (D) \leftrightarrow (m \in I, u \in (TopOpen \circ R) (m) ⟼ {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (m))}^{-1} [u]) : ⋃_{m \in I} (\{m\} \times (TopOpen \circ R) (m)) ⟶ MetOpen (D)$
256	253 255	sylib	$⊢ φ \to (m \in I, u \in (TopOpen \circ R) (m) ⟼ {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (m))}^{-1} [u]) : ⋃_{m \in I} (\{m\} \times (TopOpen \circ R) (m)) ⟶ MetOpen (D)$
257	256	frnd	$⊢ φ \to ran (m \in I, u \in (TopOpen \circ R) (m) ⟼ {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (m))}^{-1} [u]) \subseteq MetOpen (D)$
258	180 257	unssd	$⊢ φ \to \{\underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n)\} \cup ran (m \in I, u \in (TopOpen \circ R) (m) ⟼ {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (m))}^{-1} [u]) \subseteq MetOpen (D)$
259		fiss	$⊢ (MetOpen (D) \in Top \land \{\underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n)\} \cup ran (m \in I, u \in (TopOpen \circ R) (m) ⟼ {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (m))}^{-1} [u]) \subseteq MetOpen (D)) \to fi (\{\underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n)\} \cup ran (m \in I, u \in (TopOpen \circ R) (m) ⟼ {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (m))}^{-1} [u])) \subseteq fi (MetOpen (D))$
260	157 258 259	syl2anc	$⊢ φ \to fi (\{\underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n)\} \cup ran (m \in I, u \in (TopOpen \circ R) (m) ⟼ {(w \in \underset{n \in I}{⨉} ⋃ (TopOpen \circ R) (n) ⟼ w (m))}^{-1} [u])) \subseteq fi (MetOpen (D))$
261	154 260	eqsstrd	$⊢ φ \to C \subseteq fi (MetOpen (D))$
262		fitop	$⊢ MetOpen (D) \in Top \to fi (MetOpen (D)) = MetOpen (D)$
263	157 262	syl	$⊢ φ \to fi (MetOpen (D)) = MetOpen (D)$
264	155	mopnval	$⊢ D \in ∞Met (B) \to MetOpen (D) = topGen (ran ball (D))$
265	21 264	syl	$⊢ φ \to MetOpen (D) = topGen (ran ball (D))$
266		tgdif0	$⊢ topGen (ran ball (D) ∖ \{\emptyset\}) = topGen (ran ball (D))$
267	265 266	eqtr4di	$⊢ φ \to MetOpen (D) = topGen (ran ball (D) ∖ \{\emptyset\})$
268	263 267	eqtrd	$⊢ φ \to fi (MetOpen (D)) = topGen (ran ball (D) ∖ \{\emptyset\})$
269	261 268	sseqtrd	$⊢ φ \to C \subseteq topGen (ran ball (D) ∖ \{\emptyset\})$
270		2basgen	$⊢ (ran ball (D) ∖ \{\emptyset\} \subseteq C \land C \subseteq topGen (ran ball (D) ∖ \{\emptyset\})) \to topGen (ran ball (D) ∖ \{\emptyset\}) = topGen (C)$
271	137 269 270	syl2anc	$⊢ φ \to topGen (ran ball (D) ∖ \{\emptyset\}) = topGen (C)$
272	19 271	eqtr4d	$⊢ φ \to \prod_{𝑡} (TopOpen \circ R) = topGen (ran ball (D) ∖ \{\emptyset\})$
273	1 2 3 13 7	prdstopn	$⊢ φ \to J = \prod_{𝑡} (TopOpen \circ R)$
274	272 273 267	3eqtr4d	$⊢ φ \to J = MetOpen (D)$

Metamath Proof Explorer

Theorem prdsxmslem2

Proof