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 ( ⇝𝑢 ‘ 𝑆 ) ↔ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) ( ( ⇝𝑢 ‘ 𝑆 ) ‘ 𝐹 ) )