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 ∈ Haus → Fun ⁡ ⇝t ⁡ J

Proof

Step Hyp Ref Expression
1 lmrel ⊢ Rel ⁡ ⇝t ⁡ J
2 1 a1i ⊢ J ∈ Haus → Rel ⁡ ⇝t ⁡ J
3 simpl ⊢ J ∈ Haus ∧ x ⇝t ⁡ J y ∧ x ⇝t ⁡ J z → J ∈ Haus
4 simprl ⊢ J ∈ Haus ∧ x ⇝t ⁡ J y ∧ x ⇝t ⁡ J z → x ⇝t ⁡ J y
5 simprr ⊢ J ∈ Haus ∧ x ⇝t ⁡ J y ∧ x ⇝t ⁡ J z → x ⇝t ⁡ J z
6 3 4 5 lmmo ⊢ J ∈ Haus ∧ x ⇝t ⁡ J y ∧ x ⇝t ⁡ J z → y = z
7 6 ex ⊢ J ∈ Haus → x ⇝t ⁡ J y ∧ x ⇝t ⁡ J z → y = z
8 7 alrimiv ⊢ J ∈ Haus → ∀ z x ⇝t ⁡ J y ∧ x ⇝t ⁡ J z → y = z
9 8 alrimiv ⊢ J ∈ Haus → ∀ y ∀ z x ⇝t ⁡ J y ∧ x ⇝t ⁡ J z → y = z
10 9 alrimiv ⊢ J ∈ Haus → ∀ x ∀ y ∀ z x ⇝t ⁡ J y ∧ x ⇝t ⁡ J z → y = z
11 dffun2 ⊢ Fun ⁡ ⇝t ⁡ J ↔ Rel ⁡ ⇝t ⁡ J ∧ ∀ x ∀ y ∀ z x ⇝t ⁡ J y ∧ x ⇝t ⁡ J z → y = z
12 2 10 11 sylanbrc ⊢ J ∈ Haus → Fun ⁡ ⇝t ⁡ J