This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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