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 ∧ 𝑃 ∈ 𝑋 ) → ¬ { 𝑃 } ∈ 𝐽 )