# 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 ${⊢}{\phi }\to {F}:{A}⟶ℂ$
rlimdmafv2.2 ${⊢}{\phi }\to sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }$
Assertion rlimdmafv2

### Proof

Step Hyp Ref Expression
1 rlimdmafv2.1 ${⊢}{\phi }\to {F}:{A}⟶ℂ$
2 rlimdmafv2.2 ${⊢}{\phi }\to sup\left({A},{ℝ}^{*},<\right)=\mathrm{+\infty }$
3 eldmg
4 3 ibi
5 simpr
6 rlimrel
7 6 brrelex1i
8 7 adantl
9 vex ${⊢}{x}\in \mathrm{V}$
10 9 a1i
11 breldmg
12 8 10 5 11 syl3anc
13 breq2
14 13 biimprd
15 14 spimevw
16 15 adantl
17 1 adantr
18 17 adantr
19 2 adantr
20 19 adantr
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
30 12 28 29 sylanbrc
31 dfatafv2iota
32 30 31 syl
33 1 adantr
34 2 adantr
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
43 42 iota5
44 43 elvd
45 32 44 eqtrd
46 5 45 breqtrrd
47 46 ex
48 47 exlimdv
49 4 48 syl5
50 6 releldmi
51 49 50 impbid1