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 )