Metamath Proof Explorer


Theorem ulmdm

Description: Two ways to express that a function has a limit. (The expression ( ( ~>uS )F ) is sometimes useful as a shorthand for "the unique limit of the function F "). (Contributed by Mario Carneiro, 5-Jul-2017)

Ref Expression
Assertion ulmdm ( 𝐹 ∈ dom ( ⇝𝑢𝑆 ) ↔ 𝐹 ( ⇝𝑢𝑆 ) ( ( ⇝𝑢𝑆 ) ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 ulmrel Rel ( ⇝𝑢𝑆 )
2 ulmuni ( ( 𝑥 ( ⇝𝑢𝑆 ) 𝑦𝑥 ( ⇝𝑢𝑆 ) 𝑧 ) → 𝑦 = 𝑧 )
3 2 ax-gen 𝑧 ( ( 𝑥 ( ⇝𝑢𝑆 ) 𝑦𝑥 ( ⇝𝑢𝑆 ) 𝑧 ) → 𝑦 = 𝑧 )
4 3 gen2 𝑥𝑦𝑧 ( ( 𝑥 ( ⇝𝑢𝑆 ) 𝑦𝑥 ( ⇝𝑢𝑆 ) 𝑧 ) → 𝑦 = 𝑧 )
5 dffun2 ( Fun ( ⇝𝑢𝑆 ) ↔ ( Rel ( ⇝𝑢𝑆 ) ∧ ∀ 𝑥𝑦𝑧 ( ( 𝑥 ( ⇝𝑢𝑆 ) 𝑦𝑥 ( ⇝𝑢𝑆 ) 𝑧 ) → 𝑦 = 𝑧 ) ) )
6 1 4 5 mpbir2an Fun ( ⇝𝑢𝑆 )
7 funfvbrb ( Fun ( ⇝𝑢𝑆 ) → ( 𝐹 ∈ dom ( ⇝𝑢𝑆 ) ↔ 𝐹 ( ⇝𝑢𝑆 ) ( ( ⇝𝑢𝑆 ) ‘ 𝐹 ) ) )
8 6 7 ax-mp ( 𝐹 ∈ dom ( ⇝𝑢𝑆 ) ↔ 𝐹 ( ⇝𝑢𝑆 ) ( ( ⇝𝑢𝑆 ) ‘ 𝐹 ) )