Metamath Proof Explorer

Theorem rlimdmafv

Description: Two ways to express that a function has a limit, analogous to rlimdm . (Contributed by Alexander van der Vekens, 27-Nov-2017)

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

Proof

Step Hyp Ref Expression
1 rlimdmafv.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
2 rlimdmafv.2 ⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ )
3 eldmg ⊢ ( 𝐹 ∈ dom ⇝𝑟 → ( 𝐹 ∈ dom ⇝𝑟 ↔ ∃ 𝑥 𝐹 ⇝𝑟 𝑥 ) )
4 3 ibi ⊢ ( 𝐹 ∈ dom ⇝𝑟 → ∃ 𝑥 𝐹 ⇝𝑟 𝑥 )
5 simpr ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → 𝐹 ⇝𝑟 𝑥 )
6 rlimrel ⊢ Rel ⇝𝑟
7 6 brrelex1i ⊢ ( 𝐹 ⇝𝑟 𝑥 → 𝐹 ∈ V )
8 7 adantl ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → 𝐹 ∈ V )
9 vex ⊢ 𝑥 ∈ V
10 9 a1i ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → 𝑥 ∈ V )
11 breldmg ⊢ ( ( 𝐹 ∈ V ∧ 𝑥 ∈ V ∧ 𝐹 ⇝𝑟 𝑥 ) → 𝐹 ∈ dom ⇝𝑟 )
12 8 10 5 11 syl3anc ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → 𝐹 ∈ dom ⇝𝑟 )
13 breq2 ⊢ ( 𝑦 = 𝑥 → ( 𝐹 ⇝𝑟 𝑦 ↔ 𝐹 ⇝𝑟 𝑥 ) )
14 13 biimprd ⊢ ( 𝑦 = 𝑥 → ( 𝐹 ⇝𝑟 𝑥 → 𝐹 ⇝𝑟 𝑦 ) )
15 14 spimevw ⊢ ( 𝐹 ⇝𝑟 𝑥 → ∃ 𝑦 𝐹 ⇝𝑟 𝑦 )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → ∃ 𝑦 𝐹 ⇝𝑟 𝑦 )
17 1 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → 𝐹 : 𝐴 ⟶ ℂ )
18 17 adantr ⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) ∧ ( 𝐹 ⇝𝑟 𝑦 ∧ 𝐹 ⇝𝑟 𝑧 ) ) → 𝐹 : 𝐴 ⟶ ℂ )
19 2 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → sup ( 𝐴 , ℝ* , < ) = +∞ )
20 19 adantr ⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) ∧ ( 𝐹 ⇝𝑟 𝑦 ∧ 𝐹 ⇝𝑟 𝑧 ) ) → sup ( 𝐴 , ℝ* , < ) = +∞ )
21 simprl ⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) ∧ ( 𝐹 ⇝𝑟 𝑦 ∧ 𝐹 ⇝𝑟 𝑧 ) ) → 𝐹 ⇝𝑟 𝑦 )
22 simprr ⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) ∧ ( 𝐹 ⇝𝑟 𝑦 ∧ 𝐹 ⇝𝑟 𝑧 ) ) → 𝐹 ⇝𝑟 𝑧 )
23 18 20 21 22 rlimuni ⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) ∧ ( 𝐹 ⇝𝑟 𝑦 ∧ 𝐹 ⇝𝑟 𝑧 ) ) → 𝑦 = 𝑧 )
24 23 ex ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → ( ( 𝐹 ⇝𝑟 𝑦 ∧ 𝐹 ⇝𝑟 𝑧 ) → 𝑦 = 𝑧 ) )
25 24 alrimivv ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → ∀ 𝑦 ∀ 𝑧 ( ( 𝐹 ⇝𝑟 𝑦 ∧ 𝐹 ⇝𝑟 𝑧 ) → 𝑦 = 𝑧 ) )
26 breq2 ⊢ ( 𝑦 = 𝑧 → ( 𝐹 ⇝𝑟 𝑦 ↔ 𝐹 ⇝𝑟 𝑧 ) )
27 26 eu4 ⊢ ( ∃! 𝑦 𝐹 ⇝𝑟 𝑦 ↔ ( ∃ 𝑦 𝐹 ⇝𝑟 𝑦 ∧ ∀ 𝑦 ∀ 𝑧 ( ( 𝐹 ⇝𝑟 𝑦 ∧ 𝐹 ⇝𝑟 𝑧 ) → 𝑦 = 𝑧 ) ) )
28 16 25 27 sylanbrc ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → ∃! 𝑦 𝐹 ⇝𝑟 𝑦 )
29 dfdfat2 ⊢ ( ⇝𝑟 defAt 𝐹 ↔ ( 𝐹 ∈ dom ⇝𝑟 ∧ ∃! 𝑦 𝐹 ⇝𝑟 𝑦 ) )
30 12 28 29 sylanbrc ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → ⇝𝑟 defAt 𝐹 )
31 afvfundmfveq ⊢ ( ⇝𝑟 defAt 𝐹 → ( ⇝𝑟 ''' 𝐹 ) = ( ⇝𝑟 ‘ 𝐹 ) )
32 30 31 syl ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → ( ⇝𝑟 ''' 𝐹 ) = ( ⇝𝑟 ‘ 𝐹 ) )
33 df-fv ⊢ ( ⇝𝑟 ‘ 𝐹 ) = ( ℩ 𝑤 𝐹 ⇝𝑟 𝑤 )
34 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ⇝𝑟 𝑥 ∧ 𝐹 ⇝𝑟 𝑤 ) ) → 𝐹 : 𝐴 ⟶ ℂ )
35 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ⇝𝑟 𝑥 ∧ 𝐹 ⇝𝑟 𝑤 ) ) → sup ( 𝐴 , ℝ* , < ) = +∞ )
36 simprr ⊢ ( ( 𝜑 ∧ ( 𝐹 ⇝𝑟 𝑥 ∧ 𝐹 ⇝𝑟 𝑤 ) ) → 𝐹 ⇝𝑟 𝑤 )
37 simprl ⊢ ( ( 𝜑 ∧ ( 𝐹 ⇝𝑟 𝑥 ∧ 𝐹 ⇝𝑟 𝑤 ) ) → 𝐹 ⇝𝑟 𝑥 )
38 34 35 36 37 rlimuni ⊢ ( ( 𝜑 ∧ ( 𝐹 ⇝𝑟 𝑥 ∧ 𝐹 ⇝𝑟 𝑤 ) ) → 𝑤 = 𝑥 )
39 38 expr ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → ( 𝐹 ⇝𝑟 𝑤 → 𝑤 = 𝑥 ) )
40 breq2 ⊢ ( 𝑤 = 𝑥 → ( 𝐹 ⇝𝑟 𝑤 ↔ 𝐹 ⇝𝑟 𝑥 ) )
41 5 40 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → ( 𝑤 = 𝑥 → 𝐹 ⇝𝑟 𝑤 ) )
42 39 41 impbid ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → ( 𝐹 ⇝𝑟 𝑤 ↔ 𝑤 = 𝑥 ) )
43 42 adantr ⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) ∧ 𝑥 ∈ V ) → ( 𝐹 ⇝𝑟 𝑤 ↔ 𝑤 = 𝑥 ) )
44 43 iota5 ⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) ∧ 𝑥 ∈ V ) → ( ℩ 𝑤 𝐹 ⇝𝑟 𝑤 ) = 𝑥 )
45 44 elvd ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → ( ℩ 𝑤 𝐹 ⇝𝑟 𝑤 ) = 𝑥 )
46 33 45 eqtrid ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → ( ⇝𝑟 ‘ 𝐹 ) = 𝑥 )
47 32 46 eqtrd ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → ( ⇝𝑟 ''' 𝐹 ) = 𝑥 )
48 5 47 breqtrrd ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → 𝐹 ⇝𝑟 ( ⇝𝑟 ''' 𝐹 ) )
49 48 ex ⊢ ( 𝜑 → ( 𝐹 ⇝𝑟 𝑥 → 𝐹 ⇝𝑟 ( ⇝𝑟 ''' 𝐹 ) ) )
50 49 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑥 𝐹 ⇝𝑟 𝑥 → 𝐹 ⇝𝑟 ( ⇝𝑟 ''' 𝐹 ) ) )
51 4 50 syl5 ⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝𝑟 → 𝐹 ⇝𝑟 ( ⇝𝑟 ''' 𝐹 ) ) )
52 6 releldmi ⊢ ( 𝐹 ⇝𝑟 ( ⇝𝑟 ''' 𝐹 ) → 𝐹 ∈ dom ⇝𝑟 )
53 51 52 impbid1 ⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝𝑟 ↔ 𝐹 ⇝𝑟 ( ⇝𝑟 ''' 𝐹 ) ) )