Metamath Proof Explorer


Theorem zfbas

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 ranfBas

Proof

Step Hyp Ref Expression
1 uzf :𝒫
2 frn :𝒫ran𝒫
3 1 2 ax-mp ran𝒫
4 ffn :𝒫Fn
5 1 4 ax-mp Fn
6 1z 1
7 fnfvelrn Fn11ran
8 5 6 7 mp2an 1ran
9 8 ne0ii ran
10 uzid xxx
11 n0i xx¬x=
12 10 11 syl x¬x=
13 12 nrex ¬xx=
14 fvelrnb Fnranxx=
15 5 14 ax-mp ranxx=
16 13 15 mtbir ¬ran
17 16 nelir ran
18 uzin2 xranyranxyran
19 vex xV
20 19 inex1 xyV
21 20 pwid xy𝒫xy
22 inelcm xyranxy𝒫xyran𝒫xy
23 18 21 22 sylancl xranyranran𝒫xy
24 23 rgen2 xranyranran𝒫xy
25 9 17 24 3pm3.2i ranranxranyranran𝒫xy
26 zex V
27 isfbas VranfBasran𝒫ranranxranyranran𝒫xy
28 26 27 ax-mp ranfBasran𝒫ranranxranyranran𝒫xy
29 3 25 28 mpbir2an ranfBas