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	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → 𝐹 ⊆ ( ℂ × 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		lmfpm	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → 𝐹 ∈ ( 𝑋 ↑pm ℂ ) )
2		toponmax	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
3		cnex	⊢ ℂ ∈ V
4		elpmg	⊢ ( ( 𝑋 ∈ 𝐽 ∧ ℂ ∈ V ) → ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ↔ ( Fun 𝐹 ∧ 𝐹 ⊆ ( ℂ × 𝑋 ) ) ) )
5	2 3 4	sylancl	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ↔ ( Fun 𝐹 ∧ 𝐹 ⊆ ( ℂ × 𝑋 ) ) ) )
6	5	adantr	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ↔ ( Fun 𝐹 ∧ 𝐹 ⊆ ( ℂ × 𝑋 ) ) ) )
7	1 6	mpbid	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → ( Fun 𝐹 ∧ 𝐹 ⊆ ( ℂ × 𝑋 ) ) )
8	7	simprd	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) → 𝐹 ⊆ ( ℂ × 𝑋 ) )