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 ) )