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	|- ( ph -> I e. Fin )
	qndenserrnopn.j	|- J = ( TopOpen ` ( RR^ ` I ) )
	qndenserrnopn.v	|- ( ph -> V e. J )
	qndenserrnopn.n	|- ( ph -> V =/= (/) )
Assertion	qndenserrnopn	|- ( ph -> E. y e. ( QQ ^m I ) y e. V )

Proof

Step	Hyp	Ref	Expression
1		qndenserrnopn.i	|- ( ph -> I e. Fin )
2		qndenserrnopn.j	|- J = ( TopOpen ` ( RR^ ` I ) )
3		qndenserrnopn.v	|- ( ph -> V e. J )
4		qndenserrnopn.n	|- ( ph -> V =/= (/) )
5		n0	|- ( V =/= (/) <-> E. x x e. V )
6	4 5	sylib	|- ( ph -> E. x x e. V )
7	1	adantr	|- ( ( ph /\ x e. V ) -> I e. Fin )
8	3	adantr	|- ( ( ph /\ x e. V ) -> V e. J )
9		simpr	|- ( ( ph /\ x e. V ) -> x e. V )
10		eqid	|- ( dist ` ( RR^ ` I ) ) = ( dist ` ( RR^ ` I ) )
11	7 2 8 9 10	qndenserrnopnlem	|- ( ( ph /\ x e. V ) -> E. y e. ( QQ ^m I ) y e. V )
12	11	ex	|- ( ph -> ( x e. V -> E. y e. ( QQ ^m I ) y e. V ) )
13	12	exlimdv	|- ( ph -> ( E. x x e. V -> E. y e. ( QQ ^m I ) y e. V ) )
14	6 13	mpd	|- ( ph -> E. y e. ( QQ ^m I ) y e. V )