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 = ( TopOpen ` CCfld )
Assertion	recnperf	|- ( S e. { RR , CC } -> ( K |`t S ) e. Perf )

Proof

Step	Hyp	Ref	Expression
1		recnperf.k	|- K = ( TopOpen ` CCfld )
2		elpri	|- ( S e. { RR , CC } -> ( S = RR \/ S = CC ) )
3		oveq2	|- ( S = RR -> ( K |`t S ) = ( K |`t RR ) )
4	1	reperf	|- ( K |`t RR ) e. Perf
5	3 4	eqeltrdi	|- ( S = RR -> ( K |`t S ) e. Perf )
6		oveq2	|- ( S = CC -> ( K |`t S ) = ( K |`t CC ) )
7	1	cnfldtopon	|- K e. ( TopOn ` CC )
8	7	toponunii	|- CC = U. K
9	8	restid	|- ( K e. ( TopOn ` CC ) -> ( K |`t CC ) = K )
10	7 9	ax-mp	|- ( K |`t CC ) = K
11	1	cnperf	|- K e. Perf
12	10 11	eqeltri	|- ( K |`t CC ) e. Perf
13	6 12	eqeltrdi	|- ( S = CC -> ( K |`t S ) e. Perf )
14	5 13	jaoi	|- ( ( S = RR \/ S = CC ) -> ( K |`t S ) e. Perf )
15	2 14	syl	|- ( S e. { RR , CC } -> ( K |`t S ) e. Perf )