Theorem recnperf

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

	Ref	Expression
Hypothesis	recnperf.k	⊢ 𝐾 = ( TopOpen ‘ ℂfld )
Assertion	recnperf	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝐾 ↾t 𝑆 ) ∈ Perf )

Proof

Step	Hyp	Ref	Expression
1		recnperf.k	⊢ 𝐾 = ( TopOpen ‘ ℂfld )
2		elpri	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) )
3		oveq2	⊢ ( 𝑆 = ℝ → ( 𝐾 ↾t 𝑆 ) = ( 𝐾 ↾t ℝ ) )
4	1	reperf	⊢ ( 𝐾 ↾t ℝ ) ∈ Perf
5	3 4	eqeltrdi	⊢ ( 𝑆 = ℝ → ( 𝐾 ↾t 𝑆 ) ∈ Perf )
6		oveq2	⊢ ( 𝑆 = ℂ → ( 𝐾 ↾t 𝑆 ) = ( 𝐾 ↾t ℂ ) )
7	1	cnfldtopon	⊢ 𝐾 ∈ ( TopOn ‘ ℂ )
8	7	toponunii	⊢ ℂ = ∪ 𝐾
9	8	restid	⊢ ( 𝐾 ∈ ( TopOn ‘ ℂ ) → ( 𝐾 ↾t ℂ ) = 𝐾 )
10	7 9	ax-mp	⊢ ( 𝐾 ↾t ℂ ) = 𝐾
11	1	cnperf	⊢ 𝐾 ∈ Perf
12	10 11	eqeltri	⊢ ( 𝐾 ↾t ℂ ) ∈ Perf
13	6 12	eqeltrdi	⊢ ( 𝑆 = ℂ → ( 𝐾 ↾t 𝑆 ) ∈ Perf )
14	5 13	jaoi	⊢ ( ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) → ( 𝐾 ↾t 𝑆 ) ∈ Perf )
15	2 14	syl	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝐾 ↾t 𝑆 ) ∈ Perf )