Theorem qndenserrnopnlem

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	qndenserrnopnlem.i	⊢ ( 𝜑 → 𝐼 ∈ Fin )
	qndenserrnopnlem.j	⊢ 𝐽 = ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) )
	qndenserrnopnlem.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐽 )
	qndenserrnopnlem.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	qndenserrnopnlem.d	⊢ 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
Assertion	qndenserrnopnlem	⊢ ( 𝜑 → ∃ 𝑦 ∈ ( ℚ ↑m 𝐼 ) 𝑦 ∈ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		qndenserrnopnlem.i	⊢ ( 𝜑 → 𝐼 ∈ Fin )
2		qndenserrnopnlem.j	⊢ 𝐽 = ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) )
3		qndenserrnopnlem.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐽 )
4		qndenserrnopnlem.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
5		qndenserrnopnlem.d	⊢ 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝐼 ) )
6	5	rrxmetfi	⊢ ( 𝐼 ∈ Fin → 𝐷 ∈ ( Met ‘ ( ℝ ↑m 𝐼 ) ) )
7	1 6	syl	⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ ( ℝ ↑m 𝐼 ) ) )
8		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ ( ℝ ↑m 𝐼 ) ) → 𝐷 ∈ ( ∞Met ‘ ( ℝ ↑m 𝐼 ) ) )
9	7 8	syl	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ ( ℝ ↑m 𝐼 ) ) )
10	3 2	eleqtrdi	⊢ ( 𝜑 → 𝑉 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) ) )
11	1	rrxtopnfi	⊢ ( 𝜑 → ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) ) = ( MetOpen ‘ ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) , 𝑔 ∈ ( ℝ ↑m 𝐼 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) ) )
12	5	a1i	⊢ ( 𝜑 → 𝐷 = ( dist ‘ ( ℝ^ ‘ 𝐼 ) ) )
13		eqid	⊢ ( ℝ^ ‘ 𝐼 ) = ( ℝ^ ‘ 𝐼 )
14		eqid	⊢ ( ℝ ↑m 𝐼 ) = ( ℝ ↑m 𝐼 )
15	13 14	rrxdsfi	⊢ ( 𝐼 ∈ Fin → ( dist ‘ ( ℝ^ ‘ 𝐼 ) ) = ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) , 𝑔 ∈ ( ℝ ↑m 𝐼 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
16	1 15	syl	⊢ ( 𝜑 → ( dist ‘ ( ℝ^ ‘ 𝐼 ) ) = ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) , 𝑔 ∈ ( ℝ ↑m 𝐼 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
17	12 16	eqtr2d	⊢ ( 𝜑 → ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) , 𝑔 ∈ ( ℝ ↑m 𝐼 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) = 𝐷 )
18	17	fveq2d	⊢ ( 𝜑 → ( MetOpen ‘ ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) , 𝑔 ∈ ( ℝ ↑m 𝐼 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) ) = ( MetOpen ‘ 𝐷 ) )
19	11 18	eqtrd	⊢ ( 𝜑 → ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) ) = ( MetOpen ‘ 𝐷 ) )
20	10 19	eleqtrd	⊢ ( 𝜑 → 𝑉 ∈ ( MetOpen ‘ 𝐷 ) )
21		eqid	⊢ ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 )
22	21	mopni2	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ ( ℝ ↑m 𝐼 ) ) ∧ 𝑉 ∈ ( MetOpen ‘ 𝐷 ) ∧ 𝑋 ∈ 𝑉 ) → ∃ 𝑒 ∈ ℝ+ ( 𝑋 ( ball ‘ 𝐷 ) 𝑒 ) ⊆ 𝑉 )
23	9 20 4 22	syl3anc	⊢ ( 𝜑 → ∃ 𝑒 ∈ ℝ+ ( 𝑋 ( ball ‘ 𝐷 ) 𝑒 ) ⊆ 𝑉 )
24	1	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ∧ ( 𝑋 ( ball ‘ 𝐷 ) 𝑒 ) ⊆ 𝑉 ) → 𝐼 ∈ Fin )
25		rrxtps	⊢ ( 𝐼 ∈ Fin → ( ℝ^ ‘ 𝐼 ) ∈ TopSp )
26	1 25	syl	⊢ ( 𝜑 → ( ℝ^ ‘ 𝐼 ) ∈ TopSp )
27		eqid	⊢ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) = ( Base ‘ ( ℝ^ ‘ 𝐼 ) )
28	27 2	istps	⊢ ( ( ℝ^ ‘ 𝐼 ) ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ) )
29	26 28	sylib	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ) )
30	1 13 27	rrxbasefi	⊢ ( 𝜑 → ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) = ( ℝ ↑m 𝐼 ) )
31	30	fveq2d	⊢ ( 𝜑 → ( TopOn ‘ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ) = ( TopOn ‘ ( ℝ ↑m 𝐼 ) ) )
32	29 31	eleqtrd	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ( ℝ ↑m 𝐼 ) ) )
33		toponss	⊢ ( ( 𝐽 ∈ ( TopOn ‘ ( ℝ ↑m 𝐼 ) ) ∧ 𝑉 ∈ 𝐽 ) → 𝑉 ⊆ ( ℝ ↑m 𝐼 ) )
34	32 3 33	syl2anc	⊢ ( 𝜑 → 𝑉 ⊆ ( ℝ ↑m 𝐼 ) )
35	34 4	sseldd	⊢ ( 𝜑 → 𝑋 ∈ ( ℝ ↑m 𝐼 ) )
36	35	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ∧ ( 𝑋 ( ball ‘ 𝐷 ) 𝑒 ) ⊆ 𝑉 ) → 𝑋 ∈ ( ℝ ↑m 𝐼 ) )
37		simp2	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ∧ ( 𝑋 ( ball ‘ 𝐷 ) 𝑒 ) ⊆ 𝑉 ) → 𝑒 ∈ ℝ+ )
38	24 36 5 37	qndenserrnbl	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ∧ ( 𝑋 ( ball ‘ 𝐷 ) 𝑒 ) ⊆ 𝑉 ) → ∃ 𝑦 ∈ ( ℚ ↑m 𝐼 ) 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝑒 ) )
39		ssel	⊢ ( ( 𝑋 ( ball ‘ 𝐷 ) 𝑒 ) ⊆ 𝑉 → ( 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝑒 ) → 𝑦 ∈ 𝑉 ) )
40	39	adantr	⊢ ( ( ( 𝑋 ( ball ‘ 𝐷 ) 𝑒 ) ⊆ 𝑉 ∧ 𝑦 ∈ ( ℚ ↑m 𝐼 ) ) → ( 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝑒 ) → 𝑦 ∈ 𝑉 ) )
41	40	3ad2antl3	⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ∧ ( 𝑋 ( ball ‘ 𝐷 ) 𝑒 ) ⊆ 𝑉 ) ∧ 𝑦 ∈ ( ℚ ↑m 𝐼 ) ) → ( 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝑒 ) → 𝑦 ∈ 𝑉 ) )
42	41	reximdva	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ∧ ( 𝑋 ( ball ‘ 𝐷 ) 𝑒 ) ⊆ 𝑉 ) → ( ∃ 𝑦 ∈ ( ℚ ↑m 𝐼 ) 𝑦 ∈ ( 𝑋 ( ball ‘ 𝐷 ) 𝑒 ) → ∃ 𝑦 ∈ ( ℚ ↑m 𝐼 ) 𝑦 ∈ 𝑉 ) )
43	38 42	mpd	⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ∧ ( 𝑋 ( ball ‘ 𝐷 ) 𝑒 ) ⊆ 𝑉 ) → ∃ 𝑦 ∈ ( ℚ ↑m 𝐼 ) 𝑦 ∈ 𝑉 )
44	43	3exp	⊢ ( 𝜑 → ( 𝑒 ∈ ℝ+ → ( ( 𝑋 ( ball ‘ 𝐷 ) 𝑒 ) ⊆ 𝑉 → ∃ 𝑦 ∈ ( ℚ ↑m 𝐼 ) 𝑦 ∈ 𝑉 ) ) )
45	44	rexlimdv	⊢ ( 𝜑 → ( ∃ 𝑒 ∈ ℝ+ ( 𝑋 ( ball ‘ 𝐷 ) 𝑒 ) ⊆ 𝑉 → ∃ 𝑦 ∈ ( ℚ ↑m 𝐼 ) 𝑦 ∈ 𝑉 ) )
46	23 45	mpd	⊢ ( 𝜑 → ∃ 𝑦 ∈ ( ℚ ↑m 𝐼 ) 𝑦 ∈ 𝑉 )