qndenserrnbl

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	qndenserrnbl.i	$⊢ φ \to I \in Fin$
	qndenserrnbl.x	$⊢ φ \to X \in (ℝ^{I})$
	qndenserrnbl.d	$⊢ D = dist (I)$
	qndenserrnbl.e	$⊢ φ \to E \in ℝ^{+}$
Assertion	qndenserrnbl	$⊢ φ \to \exists y \in (ℚ^{I}) y \in (X ball (D) E)$

Proof

Step	Hyp	Ref	Expression
1		qndenserrnbl.i	$⊢ φ \to I \in Fin$
2		qndenserrnbl.x	$⊢ φ \to X \in (ℝ^{I})$
3		qndenserrnbl.d	$⊢ D = dist (I)$
4		qndenserrnbl.e	$⊢ φ \to E \in ℝ^{+}$
5		0ex	$⊢ \emptyset \in V$
6	5	snid	$⊢ \emptyset \in \{\emptyset\}$
7	6	a1i	$⊢ (φ \land I = \emptyset) \to \emptyset \in \{\emptyset\}$
8		oveq2	$⊢ I = \emptyset \to ℚ^{I} = ℚ^{\emptyset}$
9		qex	$⊢ ℚ \in V$
10		mapdm0	$⊢ ℚ \in V \to ℚ^{\emptyset} = \{\emptyset\}$
11	9 10	ax-mp	$⊢ ℚ^{\emptyset} = \{\emptyset\}$
12	11	a1i	$⊢ I = \emptyset \to ℚ^{\emptyset} = \{\emptyset\}$
13	8 12	eqtr2d	$⊢ I = \emptyset \to \{\emptyset\} = ℚ^{I}$
14	13	adantl	$⊢ (φ \land I = \emptyset) \to \{\emptyset\} = ℚ^{I}$
15	7 14	eleqtrd	$⊢ (φ \land I = \emptyset) \to \emptyset \in (ℚ^{I})$
16	3	rrxmetfi	$⊢ I \in Fin \to D \in Met (ℝ^{I})$
17	1 16	syl	$⊢ φ \to D \in Met (ℝ^{I})$
18		metxmet	$⊢ D \in Met (ℝ^{I}) \to D \in ∞Met (ℝ^{I})$
19	17 18	syl	$⊢ φ \to D \in ∞Met (ℝ^{I})$
20	19	adantr	$⊢ (φ \land I = \emptyset) \to D \in ∞Met (ℝ^{I})$
21	2	adantr	$⊢ (φ \land I = \emptyset) \to X \in (ℝ^{I})$
22		oveq2	$⊢ I = \emptyset \to ℝ^{I} = ℝ^{\emptyset}$
23		reex	$⊢ ℝ \in V$
24		mapdm0	$⊢ ℝ \in V \to ℝ^{\emptyset} = \{\emptyset\}$
25	23 24	ax-mp	$⊢ ℝ^{\emptyset} = \{\emptyset\}$
26	25	a1i	$⊢ I = \emptyset \to ℝ^{\emptyset} = \{\emptyset\}$
27	22 26	eqtrd	$⊢ I = \emptyset \to ℝ^{I} = \{\emptyset\}$
28	27	adantl	$⊢ (φ \land I = \emptyset) \to ℝ^{I} = \{\emptyset\}$
29	21 28	eleqtrd	$⊢ (φ \land I = \emptyset) \to X \in \{\emptyset\}$
30		elsng	$⊢ X \in (ℝ^{I}) \to (X \in \{\emptyset\} \leftrightarrow X = \emptyset)$
31	2 30	syl	$⊢ φ \to (X \in \{\emptyset\} \leftrightarrow X = \emptyset)$
32	31	adantr	$⊢ (φ \land I = \emptyset) \to (X \in \{\emptyset\} \leftrightarrow X = \emptyset)$
33	29 32	mpbid	$⊢ (φ \land I = \emptyset) \to X = \emptyset$
34	33	eqcomd	$⊢ (φ \land I = \emptyset) \to \emptyset = X$
35	34 21	eqeltrd	$⊢ (φ \land I = \emptyset) \to \emptyset \in (ℝ^{I})$
36	4	rpxrd	$⊢ φ \to E \in ℝ^{*}$
37	4	rpgt0d	$⊢ φ \to 0 < E$
38	36 37	jca	$⊢ φ \to (E \in ℝ^{*} \land 0 < E)$
39	38	adantr	$⊢ (φ \land I = \emptyset) \to (E \in ℝ^{*} \land 0 < E)$
40		xblcntr	$⊢ (D \in ∞Met (ℝ^{I}) \land \emptyset \in (ℝ^{I}) \land (E \in ℝ^{*} \land 0 < E)) \to \emptyset \in (\emptyset ball (D) E)$
41	20 35 39 40	syl3anc	$⊢ (φ \land I = \emptyset) \to \emptyset \in (\emptyset ball (D) E)$
42	34	oveq1d	$⊢ (φ \land I = \emptyset) \to \emptyset ball (D) E = X ball (D) E$
43	41 42	eleqtrd	$⊢ (φ \land I = \emptyset) \to \emptyset \in (X ball (D) E)$
44		eleq1	$⊢ y = \emptyset \to (y \in (X ball (D) E) \leftrightarrow \emptyset \in (X ball (D) E))$
45	44	rspcev	$⊢ (\emptyset \in (ℚ^{I}) \land \emptyset \in (X ball (D) E)) \to \exists y \in (ℚ^{I}) y \in (X ball (D) E)$
46	15 43 45	syl2anc	$⊢ (φ \land I = \emptyset) \to \exists y \in (ℚ^{I}) y \in (X ball (D) E)$
47	1	adantr	$⊢ (φ \land \neg I = \emptyset) \to I \in Fin$
48		neqne	$⊢ \neg I = \emptyset \to I \neq \emptyset$
49	48	adantl	$⊢ (φ \land \neg I = \emptyset) \to I \neq \emptyset$
50	2	adantr	$⊢ (φ \land \neg I = \emptyset) \to X \in (ℝ^{I})$
51	4	adantr	$⊢ (φ \land \neg I = \emptyset) \to E \in ℝ^{+}$
52	47 49 50 3 51	qndenserrnbllem	$⊢ (φ \land \neg I = \emptyset) \to \exists y \in (ℚ^{I}) y \in (X ball (D) E)$
53	46 52	pm2.61dan	$⊢ φ \to \exists y \in (ℚ^{I}) y \in (X ball (D) E)$

Metamath Proof Explorer

Theorem qndenserrnbl

Proof