Metamath Proof Explorer

Theorem lmfss

Description: Inclusion of a function having a limit (used to ensure the limit relation is a set, under our definition). (Contributed by NM, 7-Dec-2006) (Revised by Mario Carneiro, 23-Dec-2013)

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

Proof

Step	Hyp	Ref	Expression
1		lmfpm	$⊢ (J \in TopOn (X) \land F \underset{t}{⇝} (J) P) \to F \in (X ↑_{𝑝𝑚} ℂ)$
2		toponmax	$⊢ J \in TopOn (X) \to X \in J$
3		cnex	$⊢ ℂ \in V$
4		elpmg	$⊢ (X \in J \land ℂ \in V) \to (F \in (X ↑_{𝑝𝑚} ℂ) \leftrightarrow (Fun F \land F \subseteq ℂ \times X))$
5	2 3 4	sylancl	$⊢ J \in TopOn (X) \to (F \in (X ↑_{𝑝𝑚} ℂ) \leftrightarrow (Fun F \land F \subseteq ℂ \times X))$
6	5	adantr	$⊢ (J \in TopOn (X) \land F \underset{t}{⇝} (J) P) \to (F \in (X ↑_{𝑝𝑚} ℂ) \leftrightarrow (Fun F \land F \subseteq ℂ \times X))$
7	1 6	mpbid	$⊢ (J \in TopOn (X) \land F \underset{t}{⇝} (J) P) \to (Fun F \land F \subseteq ℂ \times X)$
8	7	simprd	$⊢ (J \in TopOn (X) \land F \underset{t}{⇝} (J) P) \to F \subseteq ℂ \times X$