Metamath Proof Explorer

Theorem perfopn

Description: An open subset of a perfect space is perfect. (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypotheses restcls.1 
|- X = U. J
restcls.2 
|- K = ( J |`t Y )
Assertion perfopn 
|- ( ( J e. Perf /\ Y e. J ) -> K e. Perf )

Proof

Step Hyp Ref Expression
1 restcls.1 
 |-  X = U. J
2 restcls.2 
 |-  K = ( J |`t Y )
3 perftop 
 |-  ( J e. Perf -> J e. Top )
4 3 adantr 
 |-  ( ( J e. Perf /\ Y e. J ) -> J e. Top )
5 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
6 4 5 sylib 
 |-  ( ( J e. Perf /\ Y e. J ) -> J e. ( TopOn ` X ) )
7 elssuni 
 |-  ( Y e. J -> Y C_ U. J )
8 7 adantl 
 |-  ( ( J e. Perf /\ Y e. J ) -> Y C_ U. J )
9 8 1 sseqtrrdi 
 |-  ( ( J e. Perf /\ Y e. J ) -> Y C_ X )
10 resttopon 
 |-  ( ( J e. ( TopOn ` X ) /\ Y C_ X ) -> ( J |`t Y ) e. ( TopOn ` Y ) )
11 6 9 10 syl2anc 
 |-  ( ( J e. Perf /\ Y e. J ) -> ( J |`t Y ) e. ( TopOn ` Y ) )
12 2 11 eqeltrid 
 |-  ( ( J e. Perf /\ Y e. J ) -> K e. ( TopOn ` Y ) )
13 topontop 
 |-  ( K e. ( TopOn ` Y ) -> K e. Top )
14 12 13 syl 
 |-  ( ( J e. Perf /\ Y e. J ) -> K e. Top )
15 9 sselda 
 |-  ( ( ( J e. Perf /\ Y e. J ) /\ x e. Y ) -> x e. X )
16 1 perfi 
 |-  ( ( J e. Perf /\ x e. X ) -> -. { x } e. J )
17 16 adantlr 
 |-  ( ( ( J e. Perf /\ Y e. J ) /\ x e. X ) -> -. { x } e. J )
18 15 17 syldan 
 |-  ( ( ( J e. Perf /\ Y e. J ) /\ x e. Y ) -> -. { x } e. J )
19 2 eleq2i 
 |-  ( { x } e. K <-> { x } e. ( J |`t Y ) )
20 restopn2 
 |-  ( ( J e. Top /\ Y e. J ) -> ( { x } e. ( J |`t Y ) <-> ( { x } e. J /\ { x } C_ Y ) ) )
21 3 20 sylan 
 |-  ( ( J e. Perf /\ Y e. J ) -> ( { x } e. ( J |`t Y ) <-> ( { x } e. J /\ { x } C_ Y ) ) )
22 21 adantr 
 |-  ( ( ( J e. Perf /\ Y e. J ) /\ x e. Y ) -> ( { x } e. ( J |`t Y ) <-> ( { x } e. J /\ { x } C_ Y ) ) )
23 simpl 
 |-  ( ( { x } e. J /\ { x } C_ Y ) -> { x } e. J )
24 22 23 syl6bi 
 |-  ( ( ( J e. Perf /\ Y e. J ) /\ x e. Y ) -> ( { x } e. ( J |`t Y ) -> { x } e. J ) )
25 19 24 syl5bi 
 |-  ( ( ( J e. Perf /\ Y e. J ) /\ x e. Y ) -> ( { x } e. K -> { x } e. J ) )
26 18 25 mtod 
 |-  ( ( ( J e. Perf /\ Y e. J ) /\ x e. Y ) -> -. { x } e. K )
27 26 ralrimiva 
 |-  ( ( J e. Perf /\ Y e. J ) -> A. x e. Y -. { x } e. K )
28 toponuni 
 |-  ( K e. ( TopOn ` Y ) -> Y = U. K )
29 12 28 syl 
 |-  ( ( J e. Perf /\ Y e. J ) -> Y = U. K )
30 29 raleqdv 
 |-  ( ( J e. Perf /\ Y e. J ) -> ( A. x e. Y -. { x } e. K <-> A. x e. U. K -. { x } e. K ) )
31 27 30 mpbid 
 |-  ( ( J e. Perf /\ Y e. J ) -> A. x e. U. K -. { x } e. K )
32 eqid 
 |-  U. K = U. K
33 32 isperf3 
 |-  ( K e. Perf <-> ( K e. Top /\ A. x e. U. K -. { x } e. K ) )
34 14 31 33 sylanbrc 
 |-  ( ( J e. Perf /\ Y e. J ) -> K e. Perf )