Metamath Proof Explorer

Theorem iscfilu

Description: The predicate " F is a Cauchy filter base on uniform space U ". (Contributed by Thierry Arnoux, 18-Nov-2017)

Ref Expression
Assertion iscfilu 
|- ( U e. ( UnifOn ` X ) -> ( F e. ( CauFilU ` U ) <-> ( F e. ( fBas ` X ) /\ A. v e. U E. a e. F ( a X. a ) C_ v ) ) )

Proof

Step Hyp Ref Expression
1 elrnust 
 |-  ( U e. ( UnifOn ` X ) -> U e. U. ran UnifOn )
2 unieq 
 |-  ( u = U -> U. u = U. U )
3 2 dmeqd 
 |-  ( u = U -> dom U. u = dom U. U )
4 3 fveq2d 
 |-  ( u = U -> ( fBas ` dom U. u ) = ( fBas ` dom U. U ) )
5 raleq 
 |-  ( u = U -> ( A. v e. u E. a e. f ( a X. a ) C_ v <-> A. v e. U E. a e. f ( a X. a ) C_ v ) )
6 4 5 rabeqbidv 
 |-  ( u = U -> { f e. ( fBas ` dom U. u ) | A. v e. u E. a e. f ( a X. a ) C_ v } = { f e. ( fBas ` dom U. U ) | A. v e. U E. a e. f ( a X. a ) C_ v } )
7 df-cfilu 
 |-  CauFilU = ( u e. U. ran UnifOn |-> { f e. ( fBas ` dom U. u ) | A. v e. u E. a e. f ( a X. a ) C_ v } )
8 fvex 
 |-  ( fBas ` dom U. U ) e. _V
9 8 rabex 
 |-  { f e. ( fBas ` dom U. U ) | A. v e. U E. a e. f ( a X. a ) C_ v } e. _V
10 6 7 9 fvmpt 
 |-  ( U e. U. ran UnifOn -> ( CauFilU ` U ) = { f e. ( fBas ` dom U. U ) | A. v e. U E. a e. f ( a X. a ) C_ v } )
11 1 10 syl 
 |-  ( U e. ( UnifOn ` X ) -> ( CauFilU ` U ) = { f e. ( fBas ` dom U. U ) | A. v e. U E. a e. f ( a X. a ) C_ v } )
12 11 eleq2d 
 |-  ( U e. ( UnifOn ` X ) -> ( F e. ( CauFilU ` U ) <-> F e. { f e. ( fBas ` dom U. U ) | A. v e. U E. a e. f ( a X. a ) C_ v } ) )
13 rexeq 
 |-  ( f = F -> ( E. a e. f ( a X. a ) C_ v <-> E. a e. F ( a X. a ) C_ v ) )
14 13 ralbidv 
 |-  ( f = F -> ( A. v e. U E. a e. f ( a X. a ) C_ v <-> A. v e. U E. a e. F ( a X. a ) C_ v ) )
15 14 elrab 
 |-  ( F e. { f e. ( fBas ` dom U. U ) | A. v e. U E. a e. f ( a X. a ) C_ v } <-> ( F e. ( fBas ` dom U. U ) /\ A. v e. U E. a e. F ( a X. a ) C_ v ) )
16 12 15 bitrdi 
 |-  ( U e. ( UnifOn ` X ) -> ( F e. ( CauFilU ` U ) <-> ( F e. ( fBas ` dom U. U ) /\ A. v e. U E. a e. F ( a X. a ) C_ v ) ) )
17 ustbas2 
 |-  ( U e. ( UnifOn ` X ) -> X = dom U. U )
18 17 fveq2d 
 |-  ( U e. ( UnifOn ` X ) -> ( fBas ` X ) = ( fBas ` dom U. U ) )
19 18 eleq2d 
 |-  ( U e. ( UnifOn ` X ) -> ( F e. ( fBas ` X ) <-> F e. ( fBas ` dom U. U ) ) )
20 19 anbi1d 
 |-  ( U e. ( UnifOn ` X ) -> ( ( F e. ( fBas ` X ) /\ A. v e. U E. a e. F ( a X. a ) C_ v ) <-> ( F e. ( fBas ` dom U. U ) /\ A. v e. U E. a e. F ( a X. a ) C_ v ) ) )
21 16 20 bitr4d 
 |-  ( U e. ( UnifOn ` X ) -> ( F e. ( CauFilU ` U ) <-> ( F e. ( fBas ` X ) /\ A. v e. U E. a e. F ( a X. a ) C_ v ) ) )