Theorem rectbntr0

Description: A countable subset of the reals has empty interior. (Contributed by Mario Carneiro, 26-Jul-2014)

	Ref	Expression
Assertion	rectbntr0	$$⊢\left(A\subseteq ℝ\wedge A\preccurlyeq \mathbb{N}\right)\to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
2	1	canth2	$$⊢\mathbb{N}\prec 𝒫\mathbb{N}$$
3		domnsym	$$⊢𝒫\mathbb{N}\preccurlyeq \mathbb{N}\to \neg \mathbb{N}\prec 𝒫\mathbb{N}$$
4	2 3	mt2	$$⊢\neg 𝒫\mathbb{N}\preccurlyeq \mathbb{N}$$
5		retop	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$$
6		simpl	$$⊢\left(A\subseteq ℝ\wedge A\preccurlyeq \mathbb{N}\right)\to A\subseteq ℝ$$
7		uniretop	$$⊢ℝ=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
8	7	ntropn	$$⊢\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}\wedge A\subseteq ℝ\right)\to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
9	5 6 8	sylancr	$$⊢\left(A\subseteq ℝ\wedge A\preccurlyeq \mathbb{N}\right)\to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
10		opnreen	$$⊢\left(\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\wedge \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)\ne \varnothing \right)\to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)\approx 𝒫\mathbb{N}$$
11	10	ex	$$⊢\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\to \left(\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)\ne \varnothing \to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)\approx 𝒫\mathbb{N}\right)$$
12	9 11	syl	$$⊢\left(A\subseteq ℝ\wedge A\preccurlyeq \mathbb{N}\right)\to \left(\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)\ne \varnothing \to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)\approx 𝒫\mathbb{N}\right)$$
13		reex	$$⊢ℝ\in \mathrm{V}$$
14	13	ssex	$$⊢A\subseteq ℝ\to A\in \mathrm{V}$$
15	7	ntrss2	$$⊢\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}\wedge A\subseteq ℝ\right)\to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)\subseteq A$$
16	5 15	mpan	$$⊢A\subseteq ℝ\to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)\subseteq A$$
17		ssdomg	$$⊢A\in \mathrm{V}\to \left(\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)\subseteq A\to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)\preccurlyeq A\right)$$
18	14 16 17	sylc	$$⊢A\subseteq ℝ\to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)\preccurlyeq A$$
19		domtr	$$⊢\left(\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)\preccurlyeq A\wedge A\preccurlyeq \mathbb{N}\right)\to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)\preccurlyeq \mathbb{N}$$
20	18 19	sylan	$$⊢\left(A\subseteq ℝ\wedge A\preccurlyeq \mathbb{N}\right)\to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)\preccurlyeq \mathbb{N}$$
21		ensym	$$⊢\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)\approx 𝒫\mathbb{N}\to 𝒫\mathbb{N}\approx \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)$$
22		endomtr	$$⊢\left(𝒫\mathbb{N}\approx \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)\wedge \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)\preccurlyeq \mathbb{N}\right)\to 𝒫\mathbb{N}\preccurlyeq \mathbb{N}$$
23	22	expcom	$$⊢\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)\preccurlyeq \mathbb{N}\to \left(𝒫\mathbb{N}\approx \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)\to 𝒫\mathbb{N}\preccurlyeq \mathbb{N}\right)$$
24	20 21 23	syl2im	$$⊢\left(A\subseteq ℝ\wedge A\preccurlyeq \mathbb{N}\right)\to \left(\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)\approx 𝒫\mathbb{N}\to 𝒫\mathbb{N}\preccurlyeq \mathbb{N}\right)$$
25	12 24	syld	$$⊢\left(A\subseteq ℝ\wedge A\preccurlyeq \mathbb{N}\right)\to \left(\mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)\ne \varnothing \to 𝒫\mathbb{N}\preccurlyeq \mathbb{N}\right)$$
26	25	necon1bd	$$⊢\left(A\subseteq ℝ\wedge A\preccurlyeq \mathbb{N}\right)\to \left(\neg 𝒫\mathbb{N}\preccurlyeq \mathbb{N}\to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)=\varnothing \right)$$
27	4 26	mpi	$$⊢\left(A\subseteq ℝ\wedge A\preccurlyeq \mathbb{N}\right)\to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(A\right)=\varnothing$$