Metamath Proof Explorer

Theorem rlimdmafv2

Description: Two ways to express that a function has a limit, analogous to rlimdm . (Contributed by AV, 5-Sep-2022)

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

Proof

Step Hyp Ref Expression
1 rlimdmafv2.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
2 rlimdmafv2.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 dfatafv2iota ⊢ ( ⇝𝑟 defAt 𝐹 → ( ⇝𝑟 '''' 𝐹 ) = ( ℩ 𝑤 𝐹 ⇝𝑟 𝑤 ) )
32 30 31 syl ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → ( ⇝𝑟 '''' 𝐹 ) = ( ℩ 𝑤 𝐹 ⇝𝑟 𝑤 ) )
33 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ⇝𝑟 𝑥 ∧ 𝐹 ⇝𝑟 𝑤 ) ) → 𝐹 : 𝐴 ⟶ ℂ )
34 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ⇝𝑟 𝑥 ∧ 𝐹 ⇝𝑟 𝑤 ) ) → sup ( 𝐴 , ℝ* , < ) = +∞ )
35 simprr ⊢ ( ( 𝜑 ∧ ( 𝐹 ⇝𝑟 𝑥 ∧ 𝐹 ⇝𝑟 𝑤 ) ) → 𝐹 ⇝𝑟 𝑤 )
36 simprl ⊢ ( ( 𝜑 ∧ ( 𝐹 ⇝𝑟 𝑥 ∧ 𝐹 ⇝𝑟 𝑤 ) ) → 𝐹 ⇝𝑟 𝑥 )
37 33 34 35 36 rlimuni ⊢ ( ( 𝜑 ∧ ( 𝐹 ⇝𝑟 𝑥 ∧ 𝐹 ⇝𝑟 𝑤 ) ) → 𝑤 = 𝑥 )
38 37 expr ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → ( 𝐹 ⇝𝑟 𝑤 → 𝑤 = 𝑥 ) )
39 breq2 ⊢ ( 𝑤 = 𝑥 → ( 𝐹 ⇝𝑟 𝑤 ↔ 𝐹 ⇝𝑟 𝑥 ) )
40 5 39 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → ( 𝑤 = 𝑥 → 𝐹 ⇝𝑟 𝑤 ) )
41 38 40 impbid ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → ( 𝐹 ⇝𝑟 𝑤 ↔ 𝑤 = 𝑥 ) )
42 41 adantr ⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) ∧ 𝑥 ∈ V ) → ( 𝐹 ⇝𝑟 𝑤 ↔ 𝑤 = 𝑥 ) )
43 42 iota5 ⊢ ( ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) ∧ 𝑥 ∈ V ) → ( ℩ 𝑤 𝐹 ⇝𝑟 𝑤 ) = 𝑥 )
44 43 elvd ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → ( ℩ 𝑤 𝐹 ⇝𝑟 𝑤 ) = 𝑥 )
45 32 44 eqtrd ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → ( ⇝𝑟 '''' 𝐹 ) = 𝑥 )
46 5 45 breqtrrd ⊢ ( ( 𝜑 ∧ 𝐹 ⇝𝑟 𝑥 ) → 𝐹 ⇝𝑟 ( ⇝𝑟 '''' 𝐹 ) )
47 46 ex ⊢ ( 𝜑 → ( 𝐹 ⇝𝑟 𝑥 → 𝐹 ⇝𝑟 ( ⇝𝑟 '''' 𝐹 ) ) )
48 47 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑥 𝐹 ⇝𝑟 𝑥 → 𝐹 ⇝𝑟 ( ⇝𝑟 '''' 𝐹 ) ) )
49 4 48 syl5 ⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝𝑟 → 𝐹 ⇝𝑟 ( ⇝𝑟 '''' 𝐹 ) ) )
50 6 releldmi ⊢ ( 𝐹 ⇝𝑟 ( ⇝𝑟 '''' 𝐹 ) → 𝐹 ∈ dom ⇝𝑟 )
51 49 50 impbid1 ⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝𝑟 ↔ 𝐹 ⇝𝑟 ( ⇝𝑟 '''' 𝐹 ) ) )