Theorem lmfun

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

	Ref	Expression
Assertion	lmfun	⊢ ( 𝐽 ∈ Haus → Fun ( ⇝𝑡 ‘ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		lmrel	⊢ Rel ( ⇝𝑡 ‘ 𝐽 )
2	1	a1i	⊢ ( 𝐽 ∈ Haus → Rel ( ⇝𝑡 ‘ 𝐽 ) )
3		simpl	⊢ ( ( 𝐽 ∈ Haus ∧ ( 𝑥 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 ∧ 𝑥 ( ⇝𝑡 ‘ 𝐽 ) 𝑧 ) ) → 𝐽 ∈ Haus )
4		simprl	⊢ ( ( 𝐽 ∈ Haus ∧ ( 𝑥 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 ∧ 𝑥 ( ⇝𝑡 ‘ 𝐽 ) 𝑧 ) ) → 𝑥 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 )
5		simprr	⊢ ( ( 𝐽 ∈ Haus ∧ ( 𝑥 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 ∧ 𝑥 ( ⇝𝑡 ‘ 𝐽 ) 𝑧 ) ) → 𝑥 ( ⇝𝑡 ‘ 𝐽 ) 𝑧 )
6	3 4 5	lmmo	⊢ ( ( 𝐽 ∈ Haus ∧ ( 𝑥 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 ∧ 𝑥 ( ⇝𝑡 ‘ 𝐽 ) 𝑧 ) ) → 𝑦 = 𝑧 )
7	6	ex	⊢ ( 𝐽 ∈ Haus → ( ( 𝑥 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 ∧ 𝑥 ( ⇝𝑡 ‘ 𝐽 ) 𝑧 ) → 𝑦 = 𝑧 ) )
8	7	alrimiv	⊢ ( 𝐽 ∈ Haus → ∀ 𝑧 ( ( 𝑥 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 ∧ 𝑥 ( ⇝𝑡 ‘ 𝐽 ) 𝑧 ) → 𝑦 = 𝑧 ) )
9	8	alrimiv	⊢ ( 𝐽 ∈ Haus → ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 ∧ 𝑥 ( ⇝𝑡 ‘ 𝐽 ) 𝑧 ) → 𝑦 = 𝑧 ) )
10	9	alrimiv	⊢ ( 𝐽 ∈ Haus → ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 ∧ 𝑥 ( ⇝𝑡 ‘ 𝐽 ) 𝑧 ) → 𝑦 = 𝑧 ) )
11		dffun2	⊢ ( Fun ( ⇝𝑡 ‘ 𝐽 ) ↔ ( Rel ( ⇝𝑡 ‘ 𝐽 ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( ⇝𝑡 ‘ 𝐽 ) 𝑦 ∧ 𝑥 ( ⇝𝑡 ‘ 𝐽 ) 𝑧 ) → 𝑦 = 𝑧 ) ) )
12	2 10 11	sylanbrc	⊢ ( 𝐽 ∈ Haus → Fun ( ⇝𝑡 ‘ 𝐽 ) )