This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐽 ∈ 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 ( ⇝𝑡 ‘ 𝐽 ) )