Theorem isperf2

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

	Ref	Expression
Hypothesis	lpfval.1	⊢ 𝑋 = ∪ 𝐽
Assertion	isperf2	⊢ ( 𝐽 ∈ Perf ↔ ( 𝐽 ∈ Top ∧ 𝑋 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lpfval.1	⊢ 𝑋 = ∪ 𝐽
2	1	isperf	⊢ ( 𝐽 ∈ Perf ↔ ( 𝐽 ∈ Top ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 ) )
3		ssid	⊢ 𝑋 ⊆ 𝑋
4	1	lpss	⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 ⊆ 𝑋 ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ⊆ 𝑋 )
5	3 4	mpan2	⊢ ( 𝐽 ∈ Top → ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ⊆ 𝑋 )
6		eqss	⊢ ( ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 ↔ ( ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ⊆ 𝑋 ∧ 𝑋 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ) )
7	6	baib	⊢ ( ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ⊆ 𝑋 → ( ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 ↔ 𝑋 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ) )
8	5 7	syl	⊢ ( 𝐽 ∈ Top → ( ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 ↔ 𝑋 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ) )
9	8	pm5.32i	⊢ ( ( 𝐽 ∈ Top ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 ) ↔ ( 𝐽 ∈ Top ∧ 𝑋 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ) )
10	2 9	bitri	⊢ ( 𝐽 ∈ Perf ↔ ( 𝐽 ∈ Top ∧ 𝑋 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ) )