Metamath Proof Explorer


Theorem perfi

Description: Property of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypothesis lpfval.1
|- X = U. J
Assertion perfi
|- ( ( J e. Perf /\ P e. X ) -> -. { P } e. J )

Proof

Step Hyp Ref Expression
1 lpfval.1
 |-  X = U. J
2 1 isperf3
 |-  ( J e. Perf <-> ( J e. Top /\ A. x e. X -. { x } e. J ) )
3 2 simprbi
 |-  ( J e. Perf -> A. x e. X -. { x } e. J )
4 sneq
 |-  ( x = P -> { x } = { P } )
5 4 eleq1d
 |-  ( x = P -> ( { x } e. J <-> { P } e. J ) )
6 5 notbid
 |-  ( x = P -> ( -. { x } e. J <-> -. { P } e. J ) )
7 6 rspccva
 |-  ( ( A. x e. X -. { x } e. J /\ P e. X ) -> -. { P } e. J )
8 3 7 sylan
 |-  ( ( J e. Perf /\ P e. X ) -> -. { P } e. J )