Description: The set of upper sets of integers is a filter base on ZZ , which corresponds to convergence of sequences on ZZ . (Contributed by Mario Carneiro, 13-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | zfbas | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uzf | |
|
2 | frn | |
|
3 | 1 2 | ax-mp | |
4 | ffn | |
|
5 | 1 4 | ax-mp | |
6 | 1z | |
|
7 | fnfvelrn | |
|
8 | 5 6 7 | mp2an | |
9 | 8 | ne0ii | |
10 | uzid | |
|
11 | n0i | |
|
12 | 10 11 | syl | |
13 | 12 | nrex | |
14 | fvelrnb | |
|
15 | 5 14 | ax-mp | |
16 | 13 15 | mtbir | |
17 | 16 | nelir | |
18 | uzin2 | |
|
19 | vex | |
|
20 | 19 | inex1 | |
21 | 20 | pwid | |
22 | inelcm | |
|
23 | 18 21 22 | sylancl | |
24 | 23 | rgen2 | |
25 | 9 17 24 | 3pm3.2i | |
26 | zex | |
|
27 | isfbas | |
|
28 | 26 27 | ax-mp | |
29 | 3 25 28 | mpbir2an | |