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 ⇝𝑣 ⟶ ℋ