Theorem qndenserrnopn

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	qndenserrnopn.i	$$⊢\phi \to I\in \mathrm{Fin}$$
	qndenserrnopn.j
	qndenserrnopn.v	$$⊢\phi \to V\in J$$
	qndenserrnopn.n	$$⊢\phi \to V\ne \varnothing$$
Assertion	qndenserrnopn	$$⊢\phi \to \exists y\in \left({\mathbb{Q}}^I\right)y\in V$$

Proof

Step	Hyp	Ref	Expression
1		qndenserrnopn.i	$$⊢\phi \to I\in \mathrm{Fin}$$
2		qndenserrnopn.j
3		qndenserrnopn.v	$$⊢\phi \to V\in J$$
4		qndenserrnopn.n	$$⊢\phi \to V\ne \varnothing$$
5		n0	$$⊢V\ne \varnothing \leftrightarrow \exists xx\in V$$
6	4 5	sylib	$$⊢\phi \to \exists xx\in V$$
7	1	adantr	$$⊢\left(\phi \wedge x\in V\right)\to I\in \mathrm{Fin}$$
8	3	adantr	$$⊢\left(\phi \wedge x\in V\right)\to V\in J$$
9		simpr	$$⊢\left(\phi \wedge x\in V\right)\to x\in V$$
10		eqid
11	7 2 8 9 10	qndenserrnopnlem	$$⊢\left(\phi \wedge x\in V\right)\to \exists y\in \left({\mathbb{Q}}^I\right)y\in V$$
12	11	ex	$$⊢\phi \to \left(x\in V\to \exists y\in \left({\mathbb{Q}}^I\right)y\in V\right)$$
13	12	exlimdv	$$⊢\phi \to \left(\exists xx\in V\to \exists y\in \left({\mathbb{Q}}^I\right)y\in V\right)$$
14	6 13	mpd	$$⊢\phi \to \exists y\in \left({\mathbb{Q}}^I\right)y\in V$$