Metamath Proof Explorer


Theorem lmfun

Description: The convergence relation is function-like in a Hausdorff space. (Contributed by Mario Carneiro, 26-Dec-2013)

Ref Expression
Assertion lmfun JHausFuntJ

Proof

Step Hyp Ref Expression
1 lmrel ReltJ
2 1 a1i JHausReltJ
3 simpl JHausxtJyxtJzJHaus
4 simprl JHausxtJyxtJzxtJy
5 simprr JHausxtJyxtJzxtJz
6 3 4 5 lmmo JHausxtJyxtJzy=z
7 6 ex JHausxtJyxtJzy=z
8 7 alrimiv JHauszxtJyxtJzy=z
9 8 alrimiv JHausyzxtJyxtJzy=z
10 9 alrimiv JHausxyzxtJyxtJzy=z
11 dffun2 FuntJReltJxyzxtJyxtJzy=z
12 2 10 11 sylanbrc JHausFuntJ