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	$$⊢\underset{v}{⇝}:\mathrm{dom}\underset{v}{⇝}⟶\mathscr{H}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
2		eqid	$$⊢\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)=\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
3	1 2	hhxmet	$$⊢\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\in \mathrm{\infty Met}\left(\mathscr{H}\right)$$
4		eqid	$$⊢\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)=\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)$$
5	4	methaus	$$⊢\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\in \mathrm{\infty Met}\left(\mathscr{H}\right)\to \mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\in \mathrm{Haus}$$
6		lmfun	$$⊢\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\in \mathrm{Haus}\to \mathrm{Fun}\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)$$
7	3 5 6	mp2b	$$⊢\mathrm{Fun}\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)$$
8		funres	$$⊢\mathrm{Fun}\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)\to \mathrm{Fun}\left({\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)\upharpoonright }_{\left({\mathscr{H}}^{\mathbb{N}}\right)}\right)$$
9	7 8	ax-mp	$$⊢\mathrm{Fun}\left({\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)\upharpoonright }_{\left({\mathscr{H}}^{\mathbb{N}}\right)}\right)$$
10	1 2 4	hhlm	$$⊢\underset{v}{⇝}={\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)\upharpoonright }_{\left({\mathscr{H}}^{\mathbb{N}}\right)}$$
11	10	funeqi	$$⊢\mathrm{Fun}\underset{v}{⇝}\leftrightarrow \mathrm{Fun}\left({\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)\right)\right)\upharpoonright }_{\left({\mathscr{H}}^{\mathbb{N}}\right)}\right)$$
12	9 11	mpbir	$$⊢\mathrm{Fun}\underset{v}{⇝}$$
13		funfn	$$⊢\mathrm{Fun}\underset{v}{⇝}\leftrightarrow \underset{v}{⇝}Fn\mathrm{dom}\underset{v}{⇝}$$
14	12 13	mpbi	$$⊢\underset{v}{⇝}Fn\mathrm{dom}\underset{v}{⇝}$$
15		funfvbrb	$$⊢\mathrm{Fun}\underset{v}{⇝}\to \left(x\in \mathrm{dom}\underset{v}{⇝}\leftrightarrow x\underset{v}{⇝}\underset{v}{⇝}\left(x\right)\right)$$
16	12 15	ax-mp	$$⊢x\in \mathrm{dom}\underset{v}{⇝}\leftrightarrow x\underset{v}{⇝}\underset{v}{⇝}\left(x\right)$$
17		fvex	$$⊢\underset{v}{⇝}\left(x\right)\in \mathrm{V}$$
18	17	hlimveci	$$⊢x\underset{v}{⇝}\underset{v}{⇝}\left(x\right)\to \underset{v}{⇝}\left(x\right)\in \mathscr{H}$$
19	16 18	sylbi	$$⊢x\in \mathrm{dom}\underset{v}{⇝}\to \underset{v}{⇝}\left(x\right)\in \mathscr{H}$$
20	19	rgen	$$⊢\forall x\in \mathrm{dom}\underset{v}{⇝}\underset{v}{⇝}\left(x\right)\in \mathscr{H}$$
21		ffnfv	$$⊢\underset{v}{⇝}:\mathrm{dom}\underset{v}{⇝}⟶\mathscr{H}\leftrightarrow \left(\underset{v}{⇝}Fn\mathrm{dom}\underset{v}{⇝}\wedge \forall x\in \mathrm{dom}\underset{v}{⇝}\underset{v}{⇝}\left(x\right)\in \mathscr{H}\right)$$
22	14 20 21	mpbir2an	$$⊢\underset{v}{⇝}:\mathrm{dom}\underset{v}{⇝}⟶\mathscr{H}$$