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	⊢ ( 𝜑 → 𝐼 ∈ Fin )
	qndenserrnopn.j	⊢ 𝐽 = ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) )
	qndenserrnopn.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐽 )
	qndenserrnopn.n	⊢ ( 𝜑 → 𝑉 ≠ ∅ )
Assertion	qndenserrnopn	⊢ ( 𝜑 → ∃ 𝑦 ∈ ( ℚ ↑m 𝐼 ) 𝑦 ∈ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		qndenserrnopn.i	⊢ ( 𝜑 → 𝐼 ∈ Fin )
2		qndenserrnopn.j	⊢ 𝐽 = ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) )
3		qndenserrnopn.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐽 )
4		qndenserrnopn.n	⊢ ( 𝜑 → 𝑉 ≠ ∅ )
5		n0	⊢ ( 𝑉 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝑉 )
6	4 5	sylib	⊢ ( 𝜑 → ∃ 𝑥 𝑥 ∈ 𝑉 )
7	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝐼 ∈ Fin )
8	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝑉 ∈ 𝐽 )
9		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ∈ 𝑉 )
10		eqid	⊢ ( dist ‘ ( ℝ^ ‘ 𝐼 ) ) = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
11	7 2 8 9 10	qndenserrnopnlem	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ∃ 𝑦 ∈ ( ℚ ↑m 𝐼 ) 𝑦 ∈ 𝑉 )
12	11	ex	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑉 → ∃ 𝑦 ∈ ( ℚ ↑m 𝐼 ) 𝑦 ∈ 𝑉 ) )
13	12	exlimdv	⊢ ( 𝜑 → ( ∃ 𝑥 𝑥 ∈ 𝑉 → ∃ 𝑦 ∈ ( ℚ ↑m 𝐼 ) 𝑦 ∈ 𝑉 ) )
14	6 13	mpd	⊢ ( 𝜑 → ∃ 𝑦 ∈ ( ℚ ↑m 𝐼 ) 𝑦 ∈ 𝑉 )