Theorem rlimdm

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

	Ref	Expression
Hypotheses	rlimuni.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
	rlimuni.2	⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ )
Assertion	rlimdm	⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝𝑟 ↔ 𝐹 ⇝𝑟 ( ⇝𝑟 ‘ 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rlimuni.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
2		rlimuni.2	⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ )
3		eldmg	⊢ ( 𝐹 ∈ dom ⇝𝑟 → ( 𝐹 ∈ dom ⇝𝑟 ↔ ∃ 𝑥 𝐹 ⇝𝑟 𝑥 ) )
4	3	ibi	⊢ ( 𝐹 ∈ dom ⇝𝑟 → ∃ 𝑥 𝐹 ⇝𝑟 𝑥 )
5		simpr	⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → 𝐹 ⇝𝑟 𝑥 )
6		df-fv	⊢ ( ⇝𝑟 ‘ 𝐹 ) = ( ℩ 𝑦 𝐹 ⇝𝑟 𝑦 )
7	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ⇝𝑟 𝑥 ∧ 𝐹 ⇝𝑟 𝑦 ) ) → 𝐹 : 𝐴 ⟶ ℂ )
8	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ⇝𝑟 𝑥 ∧ 𝐹 ⇝𝑟 𝑦 ) ) → sup ( 𝐴 , ℝ* , < ) = +∞ )
9		simprr	⊢ ( ( 𝜑 ∧ ( 𝐹 ⇝𝑟 𝑥 ∧ 𝐹 ⇝𝑟 𝑦 ) ) → 𝐹 ⇝𝑟 𝑦 )
10		simprl	⊢ ( ( 𝜑 ∧ ( 𝐹 ⇝𝑟 𝑥 ∧ 𝐹 ⇝𝑟 𝑦 ) ) → 𝐹 ⇝𝑟 𝑥 )
11	7 8 9 10	rlimuni	⊢ ( ( 𝜑 ∧ ( 𝐹 ⇝𝑟 𝑥 ∧ 𝐹 ⇝𝑟 𝑦 ) ) → 𝑦 = 𝑥 )
12	11	expr	⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → ( 𝐹 ⇝𝑟 𝑦 → 𝑦 = 𝑥 ) )
13		breq2	⊢ ( 𝑦 = 𝑥 → ( 𝐹 ⇝𝑟 𝑦 ↔ 𝐹 ⇝𝑟 𝑥 ) )
14	5 13	syl5ibrcom	⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → ( 𝑦 = 𝑥 → 𝐹 ⇝𝑟 𝑦 ) )
15	12 14	impbid	⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → ( 𝐹 ⇝𝑟 𝑦 ↔ 𝑦 = 𝑥 ) )
16	15	adantr	⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) ∧ 𝑥 ∈ V ) → ( 𝐹 ⇝𝑟 𝑦 ↔ 𝑦 = 𝑥 ) )
17	16	iota5	⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) ∧ 𝑥 ∈ V ) → ( ℩ 𝑦 𝐹 ⇝𝑟 𝑦 ) = 𝑥 )
18	17	elvd	⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → ( ℩ 𝑦 𝐹 ⇝𝑟 𝑦 ) = 𝑥 )
19	6 18	syl5eq	⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → ( ⇝𝑟 ‘ 𝐹 ) = 𝑥 )
20	5 19	breqtrrd	⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → 𝐹 ⇝𝑟 ( ⇝𝑟 ‘ 𝐹 ) )
21	20	ex	⊢ ( 𝜑 → ( 𝐹 ⇝𝑟 𝑥 → 𝐹 ⇝𝑟 ( ⇝𝑟 ‘ 𝐹 ) ) )
22	21	exlimdv	⊢ ( 𝜑 → ( ∃ 𝑥 𝐹 ⇝𝑟 𝑥 → 𝐹 ⇝𝑟 ( ⇝𝑟 ‘ 𝐹 ) ) )
23	4 22	syl5	⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝𝑟 → 𝐹 ⇝𝑟 ( ⇝𝑟 ‘ 𝐹 ) ) )
24		rlimrel	⊢ Rel ⇝𝑟
25	24	releldmi	⊢ ( 𝐹 ⇝𝑟 ( ⇝𝑟 ‘ 𝐹 ) → 𝐹 ∈ dom ⇝𝑟 )
26	23 25	impbid1	⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝𝑟 ↔ 𝐹 ⇝𝑟 ( ⇝𝑟 ‘ 𝐹 ) ) )