isperf2

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

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

Step	Hyp	Ref	Expression
1		lpfval.1	$⊢ X = ⋃ J$
2	1	isperf	$⊢ J \in Perf \leftrightarrow (J \in Top \land limPt (J) (X) = X)$
3		ssid	$⊢ X \subseteq X$
4	1	lpss	$⊢ (J \in Top \land X \subseteq X) \to limPt (J) (X) \subseteq X$
5	3 4	mpan2	$⊢ J \in Top \to limPt (J) (X) \subseteq X$
6		eqss	$⊢ limPt (J) (X) = X \leftrightarrow (limPt (J) (X) \subseteq X \land X \subseteq limPt (J) (X))$
7	6	baib	$⊢ limPt (J) (X) \subseteq X \to (limPt (J) (X) = X \leftrightarrow X \subseteq limPt (J) (X))$
8	5 7	syl	$⊢ J \in Top \to (limPt (J) (X) = X \leftrightarrow X \subseteq limPt (J) (X))$
9	8	pm5.32i	$⊢ (J \in Top \land limPt (J) (X) = X) \leftrightarrow (J \in Top \land X \subseteq limPt (J) (X))$
10	2 9	bitri	$⊢ J \in Perf \leftrightarrow (J \in Top \land X \subseteq limPt (J) (X))$

Metamath Proof Explorer