This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isperf

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

		Ref	Expression
	Hypothesis	lpfval.1	$⊢ X = ⋃ J$
	Assertion	isperf	$⊢ J \in Perf \leftrightarrow (J \in Top \land limPt (J) (X) = X)$

Step	Hyp	Ref	Expression
1		lpfval.1	$⊢ X = ⋃ J$
2		fveq2	$⊢ j = J \to limPt (j) = limPt (J)$
3		unieq	$⊢ j = J \to ⋃ j = ⋃ J$
4	3 1	eqtr4di	$⊢ j = J \to ⋃ j = X$
5	2 4	fveq12d	$⊢ j = J \to limPt (j) (⋃ j) = limPt (J) (X)$
6	5 4	eqeq12d	$⊢ j = J \to (limPt (j) (⋃ j) = ⋃ j \leftrightarrow limPt (J) (X) = X)$
7		df-perf	$⊢ Perf = \{j \in Top \| limPt (j) (⋃ j) = ⋃ j\}$
8	6 7	elrab2	$⊢ J \in Perf \leftrightarrow (J \in Top \land limPt (J) (X) = X)$