Theorem isperf

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

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

Proof

Step	Hyp	Ref	Expression
1		lpfval.1	⊢ 𝑋 = ∪ 𝐽
2		fveq2	⊢ ( 𝑗 = 𝐽 → ( limPt ‘ 𝑗 ) = ( limPt ‘ 𝐽 ) )
3		unieq	⊢ ( 𝑗 = 𝐽 → ∪ 𝑗 = ∪ 𝐽 )
4	3 1	eqtr4di	⊢ ( 𝑗 = 𝐽 → ∪ 𝑗 = 𝑋 )
5	2 4	fveq12d	⊢ ( 𝑗 = 𝐽 → ( ( limPt ‘ 𝑗 ) ‘ ∪ 𝑗 ) = ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) )
6	5 4	eqeq12d	⊢ ( 𝑗 = 𝐽 → ( ( ( limPt ‘ 𝑗 ) ‘ ∪ 𝑗 ) = ∪ 𝑗 ↔ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 ) )
7		df-perf	⊢ Perf = { 𝑗 ∈ Top ∣ ( ( limPt ‘ 𝑗 ) ‘ ∪ 𝑗 ) = ∪ 𝑗 }
8	6 7	elrab2	⊢ ( 𝐽 ∈ Perf ↔ ( 𝐽 ∈ Top ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 ) )