Theorem recnperf

Description: Both RR and CC are perfect subsets of CC . (Contributed by Mario Carneiro, 28-Dec-2016)

	Ref	Expression
Hypothesis	recnperf.k	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	recnperf	$$⊢S\in \left\{ℝ,ℂ\right\}\to K{\upharpoonright }_{𝑡}S\in \mathrm{Perf}$$

Proof

Step	Hyp	Ref	Expression
1		recnperf.k	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2		elpri	$$⊢S\in \left\{ℝ,ℂ\right\}\to \left(S=ℝ\vee S=ℂ\right)$$
3		oveq2	$$⊢S=ℝ\to K{\upharpoonright }_{𝑡}S=K{\upharpoonright }_{𝑡}ℝ$$
4	1	reperf	$$⊢K{\upharpoonright }_{𝑡}ℝ\in \mathrm{Perf}$$
5	3 4	eqeltrdi	$$⊢S=ℝ\to K{\upharpoonright }_{𝑡}S\in \mathrm{Perf}$$
6		oveq2	$$⊢S=ℂ\to K{\upharpoonright }_{𝑡}S=K{\upharpoonright }_{𝑡}ℂ$$
7	1	cnfldtopon	$$⊢K\in \mathrm{TopOn}\left(ℂ\right)$$
8	7	toponunii	$$⊢ℂ=\bigcup K$$
9	8	restid	$$⊢K\in \mathrm{TopOn}\left(ℂ\right)\to K{\upharpoonright }_{𝑡}ℂ=K$$
10	7 9	ax-mp	$$⊢K{\upharpoonright }_{𝑡}ℂ=K$$
11	1	cnperf	$$⊢K\in \mathrm{Perf}$$
12	10 11	eqeltri	$$⊢K{\upharpoonright }_{𝑡}ℂ\in \mathrm{Perf}$$
13	6 12	eqeltrdi	$$⊢S=ℂ\to K{\upharpoonright }_{𝑡}S\in \mathrm{Perf}$$
14	5 13	jaoi	$$⊢\left(S=ℝ\vee S=ℂ\right)\to K{\upharpoonright }_{𝑡}S\in \mathrm{Perf}$$
15	2 14	syl	$$⊢S\in \left\{ℝ,ℂ\right\}\to K{\upharpoonright }_{𝑡}S\in \mathrm{Perf}$$