lmcl

Description: Closure of a limit. (Contributed by NM, 19-Dec-2006) (Revised by Mario Carneiro, 23-Dec-2013)

		Ref	Expression
	Assertion	lmcl	$⊢ (J \in TopOn (X) \land F \underset{t}{⇝} (J) P) \to P \in X$

Step	Hyp	Ref	Expression
1		id	$⊢ J \in TopOn (X) \to J \in TopOn (X)$
2	1	lmbr	$⊢ J \in TopOn (X) \to (F \underset{t}{⇝} (J) P \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall u \in J (P \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u)))$
3	2	biimpa	$⊢ (J \in TopOn (X) \land F \underset{t}{⇝} (J) P) \to (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall u \in J (P \in u \to \exists y \in ran ℤ_{\geq} ({F ↾}_{y}) : y ⟶ u))$
4	3	simp2d	$⊢ (J \in TopOn (X) \land F \underset{t}{⇝} (J) P) \to P \in X$

Metamath Proof Explorer