Metamath Proof Explorer


Theorem perfi

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

Ref Expression
Hypothesis lpfval.1 𝑋 = 𝐽
Assertion perfi ( ( 𝐽 ∈ Perf ∧ 𝑃𝑋 ) → ¬ { 𝑃 } ∈ 𝐽 )

Proof

Step Hyp Ref Expression
1 lpfval.1 𝑋 = 𝐽
2 1 isperf3 ( 𝐽 ∈ Perf ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥𝑋 ¬ { 𝑥 } ∈ 𝐽 ) )
3 2 simprbi ( 𝐽 ∈ Perf → ∀ 𝑥𝑋 ¬ { 𝑥 } ∈ 𝐽 )
4 sneq ( 𝑥 = 𝑃 → { 𝑥 } = { 𝑃 } )
5 4 eleq1d ( 𝑥 = 𝑃 → ( { 𝑥 } ∈ 𝐽 ↔ { 𝑃 } ∈ 𝐽 ) )
6 5 notbid ( 𝑥 = 𝑃 → ( ¬ { 𝑥 } ∈ 𝐽 ↔ ¬ { 𝑃 } ∈ 𝐽 ) )
7 6 rspccva ( ( ∀ 𝑥𝑋 ¬ { 𝑥 } ∈ 𝐽𝑃𝑋 ) → ¬ { 𝑃 } ∈ 𝐽 )
8 3 7 sylan ( ( 𝐽 ∈ Perf ∧ 𝑃𝑋 ) → ¬ { 𝑃 } ∈ 𝐽 )