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