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
|- ( J e. Haus -> Fun ( ~~>t ` J ) )

Proof

Step Hyp Ref Expression
1 lmrel
 |-  Rel ( ~~>t ` J )
2 1 a1i
 |-  ( J e. Haus -> Rel ( ~~>t ` J ) )
3 simpl
 |-  ( ( J e. Haus /\ ( x ( ~~>t ` J ) y /\ x ( ~~>t ` J ) z ) ) -> J e. Haus )
4 simprl
 |-  ( ( J e. Haus /\ ( x ( ~~>t ` J ) y /\ x ( ~~>t ` J ) z ) ) -> x ( ~~>t ` J ) y )
5 simprr
 |-  ( ( J e. Haus /\ ( x ( ~~>t ` J ) y /\ x ( ~~>t ` J ) z ) ) -> x ( ~~>t ` J ) z )
6 3 4 5 lmmo
 |-  ( ( J e. Haus /\ ( x ( ~~>t ` J ) y /\ x ( ~~>t ` J ) z ) ) -> y = z )
7 6 ex
 |-  ( J e. Haus -> ( ( x ( ~~>t ` J ) y /\ x ( ~~>t ` J ) z ) -> y = z ) )
8 7 alrimiv
 |-  ( J e. Haus -> A. z ( ( x ( ~~>t ` J ) y /\ x ( ~~>t ` J ) z ) -> y = z ) )
9 8 alrimiv
 |-  ( J e. Haus -> A. y A. z ( ( x ( ~~>t ` J ) y /\ x ( ~~>t ` J ) z ) -> y = z ) )
10 9 alrimiv
 |-  ( J e. Haus -> A. x A. y A. z ( ( x ( ~~>t ` J ) y /\ x ( ~~>t ` J ) z ) -> y = z ) )
11 dffun2
 |-  ( Fun ( ~~>t ` J ) <-> ( Rel ( ~~>t ` J ) /\ A. x A. y A. z ( ( x ( ~~>t ` J ) y /\ x ( ~~>t ` J ) z ) -> y = z ) ) )
12 2 10 11 sylanbrc
 |-  ( J e. Haus -> Fun ( ~~>t ` J ) )