Theorem isperf3

Description: A perfect space is a topology which has no open singletons. (Contributed by Mario Carneiro, 24-Dec-2016)

	Ref	Expression
Hypothesis	lpfval.1	⊢ 𝑋 = ∪ 𝐽
Assertion	isperf3	⊢ ( 𝐽 ∈ Perf ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝑋 ¬ { 𝑥 } ∈ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		lpfval.1	⊢ 𝑋 = ∪ 𝐽
2	1	isperf2	⊢ ( 𝐽 ∈ Perf ↔ ( 𝐽 ∈ Top ∧ 𝑋 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ) )
3		dfss3	⊢ ( 𝑋 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ↔ ∀ 𝑥 ∈ 𝑋 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) )
4	1	maxlp	⊢ ( 𝐽 ∈ Top → ( 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ¬ { 𝑥 } ∈ 𝐽 ) ) )
5	4	baibd	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ↔ ¬ { 𝑥 } ∈ 𝐽 ) )
6	5	ralbidva	⊢ ( 𝐽 ∈ Top → ( ∀ 𝑥 ∈ 𝑋 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ↔ ∀ 𝑥 ∈ 𝑋 ¬ { 𝑥 } ∈ 𝐽 ) )
7	3 6	syl5bb	⊢ ( 𝐽 ∈ Top → ( 𝑋 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ↔ ∀ 𝑥 ∈ 𝑋 ¬ { 𝑥 } ∈ 𝐽 ) )
8	7	pm5.32i	⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ) ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝑋 ¬ { 𝑥 } ∈ 𝐽 ) )
9	2 8	bitri	⊢ ( 𝐽 ∈ Perf ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝑋 ¬ { 𝑥 } ∈ 𝐽 ) )