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 
|- 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 )