recnperf

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

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

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

Metamath Proof Explorer