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

Metamath Proof Explorer

Theorem ulmdm

Proof