Theorem qndenserrn

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	qndenserrn.i	⊢ ( 𝜑 → 𝐼 ∈ Fin )
	qndenserrn.j	⊢ 𝐽 = ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) )
Assertion	qndenserrn	⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ ( ℚ ↑m 𝐼 ) ) = ( ℝ ↑m 𝐼 ) )

Proof

Step	Hyp	Ref	Expression
1		qndenserrn.i	⊢ ( 𝜑 → 𝐼 ∈ Fin )
2		qndenserrn.j	⊢ 𝐽 = ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) )
3	2	rrxtop	⊢ ( 𝐼 ∈ Fin → 𝐽 ∈ Top )
4	1 3	syl	⊢ ( 𝜑 → 𝐽 ∈ Top )
5		reex	⊢ ℝ ∈ V
6		qssre	⊢ ℚ ⊆ ℝ
7		mapss	⊢ ( ( ℝ ∈ V ∧ ℚ ⊆ ℝ ) → ( ℚ ↑m 𝐼 ) ⊆ ( ℝ ↑m 𝐼 ) )
8	5 6 7	mp2an	⊢ ( ℚ ↑m 𝐼 ) ⊆ ( ℝ ↑m 𝐼 )
9	8	a1i	⊢ ( 𝜑 → ( ℚ ↑m 𝐼 ) ⊆ ( ℝ ↑m 𝐼 ) )
10		eqid	⊢ ( ℝ^ ‘ 𝐼 ) = ( ℝ^ ‘ 𝐼 )
11		eqid	⊢ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) = ( Base ‘ ( ℝ^ ‘ 𝐼 ) )
12	1 10 11	rrxbasefi	⊢ ( 𝜑 → ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) = ( ℝ ↑m 𝐼 ) )
13	12	eqcomd	⊢ ( 𝜑 → ( ℝ ↑m 𝐼 ) = ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) )
14		rrxtps	⊢ ( 𝐼 ∈ Fin → ( ℝ^ ‘ 𝐼 ) ∈ TopSp )
15		eqid	⊢ ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) ) = ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) )
16	11 15	tpsuni	⊢ ( ( ℝ^ ‘ 𝐼 ) ∈ TopSp → ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) = ∪ ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) ) )
17	1 14 16	3syl	⊢ ( 𝜑 → ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) = ∪ ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) ) )
18	2	unieqi	⊢ ∪ 𝐽 = ∪ ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) )
19	18	eqcomi	⊢ ∪ ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) ) = ∪ 𝐽
20	19	a1i	⊢ ( 𝜑 → ∪ ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) ) = ∪ 𝐽 )
21	13 17 20	3eqtrd	⊢ ( 𝜑 → ( ℝ ↑m 𝐼 ) = ∪ 𝐽 )
22	9 21	sseqtrd	⊢ ( 𝜑 → ( ℚ ↑m 𝐼 ) ⊆ ∪ 𝐽 )
23		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
24	23	clsss3	⊢ ( ( 𝐽 ∈ Top ∧ ( ℚ ↑m 𝐼 ) ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ ( ℚ ↑m 𝐼 ) ) ⊆ ∪ 𝐽 )
25	4 22 24	syl2anc	⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ ( ℚ ↑m 𝐼 ) ) ⊆ ∪ 𝐽 )
26	21	eqcomd	⊢ ( 𝜑 → ∪ 𝐽 = ( ℝ ↑m 𝐼 ) )
27	25 26	sseqtrd	⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ ( ℚ ↑m 𝐼 ) ) ⊆ ( ℝ ↑m 𝐼 ) )
28	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) → 𝐼 ∈ Fin )
29		id	⊢ ( 𝑣 ∈ 𝐽 → 𝑣 ∈ 𝐽 )
30	29 2	eleqtrdi	⊢ ( 𝑣 ∈ 𝐽 → 𝑣 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) ) )
31	30	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) → 𝑣 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) ) )
32		ne0i	⊢ ( 𝑥 ∈ 𝑣 → 𝑣 ≠ ∅ )
33	32	adantl	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) → 𝑣 ≠ ∅ )
34	28 15 31 33	qndenserrnopn	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) → ∃ 𝑦 ∈ ( ℚ ↑m 𝐼 ) 𝑦 ∈ 𝑣 )
35		df-rex	⊢ ( ∃ 𝑦 ∈ ( ℚ ↑m 𝐼 ) 𝑦 ∈ 𝑣 ↔ ∃ 𝑦 ( 𝑦 ∈ ( ℚ ↑m 𝐼 ) ∧ 𝑦 ∈ 𝑣 ) )
36	34 35	sylib	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) → ∃ 𝑦 ( 𝑦 ∈ ( ℚ ↑m 𝐼 ) ∧ 𝑦 ∈ 𝑣 ) )
37		simpr	⊢ ( ( 𝑦 ∈ ( ℚ ↑m 𝐼 ) ∧ 𝑦 ∈ 𝑣 ) → 𝑦 ∈ 𝑣 )
38		simpl	⊢ ( ( 𝑦 ∈ ( ℚ ↑m 𝐼 ) ∧ 𝑦 ∈ 𝑣 ) → 𝑦 ∈ ( ℚ ↑m 𝐼 ) )
39	37 38	elind	⊢ ( ( 𝑦 ∈ ( ℚ ↑m 𝐼 ) ∧ 𝑦 ∈ 𝑣 ) → 𝑦 ∈ ( 𝑣 ∩ ( ℚ ↑m 𝐼 ) ) )
40	39	a1i	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) → ( ( 𝑦 ∈ ( ℚ ↑m 𝐼 ) ∧ 𝑦 ∈ 𝑣 ) → 𝑦 ∈ ( 𝑣 ∩ ( ℚ ↑m 𝐼 ) ) ) )
41	40	eximdv	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) → ( ∃ 𝑦 ( 𝑦 ∈ ( ℚ ↑m 𝐼 ) ∧ 𝑦 ∈ 𝑣 ) → ∃ 𝑦 𝑦 ∈ ( 𝑣 ∩ ( ℚ ↑m 𝐼 ) ) ) )
42	36 41	mpd	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) → ∃ 𝑦 𝑦 ∈ ( 𝑣 ∩ ( ℚ ↑m 𝐼 ) ) )
43		n0	⊢ ( ( 𝑣 ∩ ( ℚ ↑m 𝐼 ) ) ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ ( 𝑣 ∩ ( ℚ ↑m 𝐼 ) ) )
44	42 43	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ) ∧ 𝑥 ∈ 𝑣 ) → ( 𝑣 ∩ ( ℚ ↑m 𝐼 ) ) ≠ ∅ )
45	44	ex	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐽 ) → ( 𝑥 ∈ 𝑣 → ( 𝑣 ∩ ( ℚ ↑m 𝐼 ) ) ≠ ∅ ) )
46	45	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ↑m 𝐼 ) ) ∧ 𝑣 ∈ 𝐽 ) → ( 𝑥 ∈ 𝑣 → ( 𝑣 ∩ ( ℚ ↑m 𝐼 ) ) ≠ ∅ ) )
47	46	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ↑m 𝐼 ) ) → ∀ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 → ( 𝑣 ∩ ( ℚ ↑m 𝐼 ) ) ≠ ∅ ) )
48	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ↑m 𝐼 ) ) → 𝐽 ∈ Top )
49	22	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ↑m 𝐼 ) ) → ( ℚ ↑m 𝐼 ) ⊆ ∪ 𝐽 )
50		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ↑m 𝐼 ) ) → 𝑥 ∈ ( ℝ ↑m 𝐼 ) )
51	21	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ↑m 𝐼 ) ) → ( ℝ ↑m 𝐼 ) = ∪ 𝐽 )
52	50 51	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ↑m 𝐼 ) ) → 𝑥 ∈ ∪ 𝐽 )
53	23	elcls	⊢ ( ( 𝐽 ∈ Top ∧ ( ℚ ↑m 𝐼 ) ⊆ ∪ 𝐽 ∧ 𝑥 ∈ ∪ 𝐽 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( ℚ ↑m 𝐼 ) ) ↔ ∀ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 → ( 𝑣 ∩ ( ℚ ↑m 𝐼 ) ) ≠ ∅ ) ) )
54	48 49 52 53	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ↑m 𝐼 ) ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( ℚ ↑m 𝐼 ) ) ↔ ∀ 𝑣 ∈ 𝐽 ( 𝑥 ∈ 𝑣 → ( 𝑣 ∩ ( ℚ ↑m 𝐼 ) ) ≠ ∅ ) ) )
55	47 54	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℝ ↑m 𝐼 ) ) → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( ℚ ↑m 𝐼 ) ) )
56	27 55	eqelssd	⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ ( ℚ ↑m 𝐼 ) ) = ( ℝ ↑m 𝐼 ) )