This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )