Metamath Proof Explorer


Theorem hlimf

Description: Function-like behavior of the convergence relation. (Contributed by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

Ref Expression
Assertion hlimf 𝑣 : dom ⇝𝑣 ⟶ ℋ

Proof

Step Hyp Ref Expression
1 eqid ⟨ ⟨ + , · ⟩ , norm ⟩ = ⟨ ⟨ + , · ⟩ , norm
2 eqid ( IndMet ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ ) = ( IndMet ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ )
3 1 2 hhxmet ( IndMet ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ ) ∈ ( ∞Met ‘ ℋ )
4 eqid ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ ) ) = ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ ) )
5 4 methaus ( ( IndMet ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ ) ∈ ( ∞Met ‘ ℋ ) → ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ ) ) ∈ Haus )
6 lmfun ( ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ ) ) ∈ Haus → Fun ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ ) ) ) )
7 3 5 6 mp2b Fun ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ ) ) )
8 funres ( Fun ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ ) ) ) → Fun ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ ) ) ) ↾ ( ℋ ↑m ℕ ) ) )
9 7 8 ax-mp Fun ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ ) ) ) ↾ ( ℋ ↑m ℕ ) )
10 1 2 4 hhlm 𝑣 = ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ ) ) ) ↾ ( ℋ ↑m ℕ ) )
11 10 funeqi ( Fun ⇝𝑣 ↔ Fun ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ ) ) ) ↾ ( ℋ ↑m ℕ ) ) )
12 9 11 mpbir Fun ⇝𝑣
13 funfn ( Fun ⇝𝑣 ↔ ⇝𝑣 Fn dom ⇝𝑣 )
14 12 13 mpbi 𝑣 Fn dom ⇝𝑣
15 funfvbrb ( Fun ⇝𝑣 → ( 𝑥 ∈ dom ⇝𝑣𝑥𝑣 ( ⇝𝑣𝑥 ) ) )
16 12 15 ax-mp ( 𝑥 ∈ dom ⇝𝑣𝑥𝑣 ( ⇝𝑣𝑥 ) )
17 fvex ( ⇝𝑣𝑥 ) ∈ V
18 17 hlimveci ( 𝑥𝑣 ( ⇝𝑣𝑥 ) → ( ⇝𝑣𝑥 ) ∈ ℋ )
19 16 18 sylbi ( 𝑥 ∈ dom ⇝𝑣 → ( ⇝𝑣𝑥 ) ∈ ℋ )
20 19 rgen 𝑥 ∈ dom ⇝𝑣 ( ⇝𝑣𝑥 ) ∈ ℋ
21 ffnfv ( ⇝𝑣 : dom ⇝𝑣 ⟶ ℋ ↔ ( ⇝𝑣 Fn dom ⇝𝑣 ∧ ∀ 𝑥 ∈ dom ⇝𝑣 ( ⇝𝑣𝑥 ) ∈ ℋ ) )
22 14 20 21 mpbir2an 𝑣 : dom ⇝𝑣 ⟶ ℋ