# 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
`|- ran ZZ>= e. ( fBas ` ZZ )`

### Proof

Step Hyp Ref Expression
1 uzf
` |-  ZZ>= : ZZ --> ~P ZZ`
2 frn
` |-  ( ZZ>= : ZZ --> ~P ZZ -> ran ZZ>= C_ ~P ZZ )`
3 1 2 ax-mp
` |-  ran ZZ>= C_ ~P ZZ`
4 ffn
` |-  ( ZZ>= : ZZ --> ~P ZZ -> ZZ>= Fn ZZ )`
5 1 4 ax-mp
` |-  ZZ>= Fn ZZ`
6 1z
` |-  1 e. ZZ`
7 fnfvelrn
` |-  ( ( ZZ>= Fn ZZ /\ 1 e. ZZ ) -> ( ZZ>= ` 1 ) e. ran ZZ>= )`
8 5 6 7 mp2an
` |-  ( ZZ>= ` 1 ) e. ran ZZ>=`
9 8 ne0ii
` |-  ran ZZ>= =/= (/)`
10 uzid
` |-  ( x e. ZZ -> x e. ( ZZ>= ` x ) )`
11 n0i
` |-  ( x e. ( ZZ>= ` x ) -> -. ( ZZ>= ` x ) = (/) )`
12 10 11 syl
` |-  ( x e. ZZ -> -. ( ZZ>= ` x ) = (/) )`
13 12 nrex
` |-  -. E. x e. ZZ ( ZZ>= ` x ) = (/)`
14 fvelrnb
` |-  ( ZZ>= Fn ZZ -> ( (/) e. ran ZZ>= <-> E. x e. ZZ ( ZZ>= ` x ) = (/) ) )`
15 5 14 ax-mp
` |-  ( (/) e. ran ZZ>= <-> E. x e. ZZ ( ZZ>= ` x ) = (/) )`
16 13 15 mtbir
` |-  -. (/) e. ran ZZ>=`
17 16 nelir
` |-  (/) e/ ran ZZ>=`
18 uzin2
` |-  ( ( x e. ran ZZ>= /\ y e. ran ZZ>= ) -> ( x i^i y ) e. ran ZZ>= )`
19 vex
` |-  x e. _V`
20 19 inex1
` |-  ( x i^i y ) e. _V`
21 20 pwid
` |-  ( x i^i y ) e. ~P ( x i^i y )`
22 inelcm
` |-  ( ( ( x i^i y ) e. ran ZZ>= /\ ( x i^i y ) e. ~P ( x i^i y ) ) -> ( ran ZZ>= i^i ~P ( x i^i y ) ) =/= (/) )`
23 18 21 22 sylancl
` |-  ( ( x e. ran ZZ>= /\ y e. ran ZZ>= ) -> ( ran ZZ>= i^i ~P ( x i^i y ) ) =/= (/) )`
24 23 rgen2
` |-  A. x e. ran ZZ>= A. y e. ran ZZ>= ( ran ZZ>= i^i ~P ( x i^i y ) ) =/= (/)`
25 9 17 24 3pm3.2i
` |-  ( ran ZZ>= =/= (/) /\ (/) e/ ran ZZ>= /\ A. x e. ran ZZ>= A. y e. ran ZZ>= ( ran ZZ>= i^i ~P ( x i^i y ) ) =/= (/) )`
26 zex
` |-  ZZ e. _V`
27 isfbas
` |-  ( ZZ e. _V -> ( ran ZZ>= e. ( fBas ` ZZ ) <-> ( ran ZZ>= C_ ~P ZZ /\ ( ran ZZ>= =/= (/) /\ (/) e/ ran ZZ>= /\ A. x e. ran ZZ>= A. y e. ran ZZ>= ( ran ZZ>= i^i ~P ( x i^i y ) ) =/= (/) ) ) ) )`
28 26 27 ax-mp
` |-  ( ran ZZ>= e. ( fBas ` ZZ ) <-> ( ran ZZ>= C_ ~P ZZ /\ ( ran ZZ>= =/= (/) /\ (/) e/ ran ZZ>= /\ A. x e. ran ZZ>= A. y e. ran ZZ>= ( ran ZZ>= i^i ~P ( x i^i y ) ) =/= (/) ) ) )`
29 3 25 28 mpbir2an
` |-  ran ZZ>= e. ( fBas ` ZZ )`