qndenserrn

Description: n-dimensional rational numbers are dense in the space of n-dimensional real numbers, with respect to the n-dimensional standard topology. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	qndenserrn.i	$⊢ φ \to I \in Fin$
	qndenserrn.j	$⊢ J = TopOpen (msup)$
Assertion	qndenserrn	$⊢ φ \to cls (J) (ℚ^{I}) = ℝ^{I}$

Proof

Step	Hyp	Ref	Expression
1		qndenserrn.i	$⊢ φ \to I \in Fin$
2		qndenserrn.j	$⊢ J = TopOpen (msup)$
3	2	rrxtop	$⊢ I \in Fin \to J \in Top$
4	1 3	syl	$⊢ φ \to J \in Top$
5		reex	$⊢ ℝ \in V$
6		qssre	$⊢ ℚ \subseteq ℝ$
7		mapss	$⊢ (ℝ \in V \land ℚ \subseteq ℝ) \to ℚ^{I} \subseteq ℝ^{I}$
8	5 6 7	mp2an	$⊢ ℚ^{I} \subseteq ℝ^{I}$
9	8	a1i	$⊢ φ \to ℚ^{I} \subseteq ℝ^{I}$
10		eqid	$⊢ msup = msup$
11		eqid	$⊢ {Base}_{msup} = {Base}_{msup}$
12	1 10 11	rrxbasefi	$⊢ φ \to {Base}_{msup} = ℝ^{I}$
13	12	eqcomd	$⊢ φ \to ℝ^{I} = {Base}_{msup}$
14		rrxtps	$⊢ I \in Fin \to msup \in TopSp$
15		eqid	$⊢ TopOpen (msup) = TopOpen (msup)$
16	11 15	tpsuni	$⊢ msup \in TopSp \to {Base}_{msup} = ⋃ TopOpen (msup)$
17	1 14 16	3syl	$⊢ φ \to {Base}_{msup} = ⋃ TopOpen (msup)$
18	2	unieqi	$⊢ ⋃ J = ⋃ TopOpen (msup)$
19	18	eqcomi	$⊢ ⋃ TopOpen (msup) = ⋃ J$
20	19	a1i	$⊢ φ \to ⋃ TopOpen (msup) = ⋃ J$
21	13 17 20	3eqtrd	$⊢ φ \to ℝ^{I} = ⋃ J$
22	9 21	sseqtrd	$⊢ φ \to ℚ^{I} \subseteq ⋃ J$
23		eqid	$⊢ ⋃ J = ⋃ J$
24	23	clsss3	$⊢ (J \in Top \land ℚ^{I} \subseteq ⋃ J) \to cls (J) (ℚ^{I}) \subseteq ⋃ J$
25	4 22 24	syl2anc	$⊢ φ \to cls (J) (ℚ^{I}) \subseteq ⋃ J$
26	21	eqcomd	$⊢ φ \to ⋃ J = ℝ^{I}$
27	25 26	sseqtrd	$⊢ φ \to cls (J) (ℚ^{I}) \subseteq ℝ^{I}$
28	1	ad2antrr	$⊢ ((φ \land v \in J) \land x \in v) \to I \in Fin$
29		id	$⊢ v \in J \to v \in J$
30	29 2	eleqtrdi	$⊢ v \in J \to v \in TopOpen (msup)$
31	30	ad2antlr	$⊢ ((φ \land v \in J) \land x \in v) \to v \in TopOpen (msup)$
32		ne0i	$⊢ x \in v \to v \neq \emptyset$
33	32	adantl	$⊢ ((φ \land v \in J) \land x \in v) \to v \neq \emptyset$
34	28 15 31 33	qndenserrnopn	$⊢ ((φ \land v \in J) \land x \in v) \to \exists y \in (ℚ^{I}) y \in v$
35		df-rex	$⊢ \exists y \in (ℚ^{I}) y \in v \leftrightarrow \exists y (y \in (ℚ^{I}) \land y \in v)$
36	34 35	sylib	$⊢ ((φ \land v \in J) \land x \in v) \to \exists y (y \in (ℚ^{I}) \land y \in v)$
37		simpr	$⊢ (y \in (ℚ^{I}) \land y \in v) \to y \in v$
38		simpl	$⊢ (y \in (ℚ^{I}) \land y \in v) \to y \in (ℚ^{I})$
39	37 38	elind	$⊢ (y \in (ℚ^{I}) \land y \in v) \to y \in (v \cap (ℚ^{I}))$
40	39	a1i	$⊢ ((φ \land v \in J) \land x \in v) \to ((y \in (ℚ^{I}) \land y \in v) \to y \in (v \cap (ℚ^{I})))$
41	40	eximdv	$⊢ ((φ \land v \in J) \land x \in v) \to (\exists y (y \in (ℚ^{I}) \land y \in v) \to \exists y y \in (v \cap (ℚ^{I})))$
42	36 41	mpd	$⊢ ((φ \land v \in J) \land x \in v) \to \exists y y \in (v \cap (ℚ^{I}))$
43		n0	$⊢ v \cap (ℚ^{I}) \neq \emptyset \leftrightarrow \exists y y \in (v \cap (ℚ^{I}))$
44	42 43	sylibr	$⊢ ((φ \land v \in J) \land x \in v) \to v \cap (ℚ^{I}) \neq \emptyset$
45	44	ex	$⊢ (φ \land v \in J) \to (x \in v \to v \cap (ℚ^{I}) \neq \emptyset)$
46	45	adantlr	$⊢ ((φ \land x \in (ℝ^{I})) \land v \in J) \to (x \in v \to v \cap (ℚ^{I}) \neq \emptyset)$
47	46	ralrimiva	$⊢ (φ \land x \in (ℝ^{I})) \to \forall v \in J (x \in v \to v \cap (ℚ^{I}) \neq \emptyset)$
48	4	adantr	$⊢ (φ \land x \in (ℝ^{I})) \to J \in Top$
49	22	adantr	$⊢ (φ \land x \in (ℝ^{I})) \to ℚ^{I} \subseteq ⋃ J$
50		simpr	$⊢ (φ \land x \in (ℝ^{I})) \to x \in (ℝ^{I})$
51	21	adantr	$⊢ (φ \land x \in (ℝ^{I})) \to ℝ^{I} = ⋃ J$
52	50 51	eleqtrd	$⊢ (φ \land x \in (ℝ^{I})) \to x \in ⋃ J$
53	23	elcls	$⊢ (J \in Top \land ℚ^{I} \subseteq ⋃ J \land x \in ⋃ J) \to (x \in cls (J) (ℚ^{I}) \leftrightarrow \forall v \in J (x \in v \to v \cap (ℚ^{I}) \neq \emptyset))$
54	48 49 52 53	syl3anc	$⊢ (φ \land x \in (ℝ^{I})) \to (x \in cls (J) (ℚ^{I}) \leftrightarrow \forall v \in J (x \in v \to v \cap (ℚ^{I}) \neq \emptyset))$
55	47 54	mpbird	$⊢ (φ \land x \in (ℝ^{I})) \to x \in cls (J) (ℚ^{I})$
56	27 55	eqelssd	$⊢ φ \to cls (J) (ℚ^{I}) = ℝ^{I}$

Metamath Proof Explorer

Theorem qndenserrn

Proof