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

Metamath Proof Explorer

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 eqtrid ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → ( ⇝𝑟 ‘ 𝐹 ) = 𝑥 )
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 ⇝𝑟 ↔ 𝐹 ⇝𝑟 ( ⇝𝑟 ‘ 𝐹 ) ) )