Description: The limit sequences of Hilbert space. (Contributed by NM, 6-Jun-2008) (Revised by Mario Carneiro, 13-May-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | h2hl.1 | |
|
h2hl.2 | |
||
h2hl.3 | |
||
h2hl.4 | |
||
h2hl.5 | |
||
Assertion | h2hlm | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | h2hl.1 | |
|
2 | h2hl.2 | |
|
3 | h2hl.3 | |
|
4 | h2hl.4 | |
|
5 | h2hl.5 | |
|
6 | df-hlim | |
|
7 | 6 | relopabiv | |
8 | relres | |
|
9 | 6 | eleq2i | |
10 | opabidw | |
|
11 | 3 | hlex | |
12 | nnex | |
|
13 | 11 12 | elmap | |
14 | 13 | anbi1i | |
15 | df-br | |
|
16 | 3 4 | imsxmet | |
17 | 2 16 | mp1i | |
18 | nnuz | |
|
19 | 1zzd | |
|
20 | eqidd | |
|
21 | id | |
|
22 | 5 17 18 19 20 21 | lmmbrf | |
23 | eluznn | |
|
24 | ffvelrn | |
|
25 | 1 2 3 4 | h2hmetdval | |
26 | 24 25 | sylan | |
27 | 26 | breq1d | |
28 | 27 | an32s | |
29 | 23 28 | sylan2 | |
30 | 29 | anassrs | |
31 | 30 | ralbidva | |
32 | 31 | rexbidva | |
33 | 32 | ralbidv | |
34 | 33 | pm5.32da | |
35 | 22 34 | bitrd | |
36 | 15 35 | bitr3id | |
37 | 36 | pm5.32i | |
38 | 14 37 | bitr2i | |
39 | anass | |
|
40 | opelres | |
|
41 | 40 | elv | |
42 | 38 39 41 | 3bitr4i | |
43 | 9 10 42 | 3bitri | |
44 | 7 8 43 | eqrelriiv | |