perfi

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

		Ref	Expression
	Hypothesis	lpfval.1	$⊢ X = ⋃ J$
	Assertion	perfi	$⊢ (J \in Perf \land P \in X) \to \neg \{P\} \in J$

Step	Hyp	Ref	Expression
1		lpfval.1	$⊢ X = ⋃ J$
2	1	isperf3	$⊢ J \in Perf \leftrightarrow (J \in Top \land \forall x \in X \neg \{x\} \in J)$
3	2	simprbi	$⊢ J \in Perf \to \forall x \in X \neg \{x\} \in J$
4		sneq	$⊢ x = P \to \{x\} = \{P\}$
5	4	eleq1d	$⊢ x = P \to (\{x\} \in J \leftrightarrow \{P\} \in J)$
6	5	notbid	$⊢ x = P \to (\neg \{x\} \in J \leftrightarrow \neg \{P\} \in J)$
7	6	rspccva	$⊢ (\forall x \in X \neg \{x\} \in J \land P \in X) \to \neg \{P\} \in J$
8	3 7	sylan	$⊢ (J \in Perf \land P \in X) \to \neg \{P\} \in J$

Metamath Proof Explorer