Metamath Proof Explorer

Theorem cfilufg

Description: The filter generated by a Cauchy filter base is still a Cauchy filter base. (Contributed by Thierry Arnoux, 24-Jan-2018)

Ref Expression
Assertion cfilufg 
|- ( ( U e. ( UnifOn ` X ) /\ F e. ( CauFilU ` U ) ) -> ( X filGen F ) e. ( CauFilU ` U ) )

Proof

Step Hyp Ref Expression
1 cfilufbas 
 |-  ( ( U e. ( UnifOn ` X ) /\ F e. ( CauFilU ` U ) ) -> F e. ( fBas ` X ) )
2 fgcl 
 |-  ( F e. ( fBas ` X ) -> ( X filGen F ) e. ( Fil ` X ) )
3 filfbas 
 |-  ( ( X filGen F ) e. ( Fil ` X ) -> ( X filGen F ) e. ( fBas ` X ) )
4 1 2 3 3syl 
 |-  ( ( U e. ( UnifOn ` X ) /\ F e. ( CauFilU ` U ) ) -> ( X filGen F ) e. ( fBas ` X ) )
5 1 ad3antrrr 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ F e. ( CauFilU ` U ) ) /\ v e. U ) /\ b e. F ) /\ ( b X. b ) C_ v ) -> F e. ( fBas ` X ) )
6 ssfg 
 |-  ( F e. ( fBas ` X ) -> F C_ ( X filGen F ) )
7 5 6 syl 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ F e. ( CauFilU ` U ) ) /\ v e. U ) /\ b e. F ) /\ ( b X. b ) C_ v ) -> F C_ ( X filGen F ) )
8 simplr 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ F e. ( CauFilU ` U ) ) /\ v e. U ) /\ b e. F ) /\ ( b X. b ) C_ v ) -> b e. F )
9 7 8 sseldd 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ F e. ( CauFilU ` U ) ) /\ v e. U ) /\ b e. F ) /\ ( b X. b ) C_ v ) -> b e. ( X filGen F ) )
10 id 
 |-  ( a = b -> a = b )
11 10 sqxpeqd 
 |-  ( a = b -> ( a X. a ) = ( b X. b ) )
12 11 sseq1d 
 |-  ( a = b -> ( ( a X. a ) C_ v <-> ( b X. b ) C_ v ) )
13 12 rspcev 
 |-  ( ( b e. ( X filGen F ) /\ ( b X. b ) C_ v ) -> E. a e. ( X filGen F ) ( a X. a ) C_ v )
14 9 13 sylancom 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ F e. ( CauFilU ` U ) ) /\ v e. U ) /\ b e. F ) /\ ( b X. b ) C_ v ) -> E. a e. ( X filGen F ) ( a X. a ) C_ v )
15 iscfilu 
 |-  ( U e. ( UnifOn ` X ) -> ( F e. ( CauFilU ` U ) <-> ( F e. ( fBas ` X ) /\ A. v e. U E. b e. F ( b X. b ) C_ v ) ) )
16 15 simplbda 
 |-  ( ( U e. ( UnifOn ` X ) /\ F e. ( CauFilU ` U ) ) -> A. v e. U E. b e. F ( b X. b ) C_ v )
17 16 r19.21bi 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ F e. ( CauFilU ` U ) ) /\ v e. U ) -> E. b e. F ( b X. b ) C_ v )
18 14 17 r19.29a 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ F e. ( CauFilU ` U ) ) /\ v e. U ) -> E. a e. ( X filGen F ) ( a X. a ) C_ v )
19 18 ralrimiva 
 |-  ( ( U e. ( UnifOn ` X ) /\ F e. ( CauFilU ` U ) ) -> A. v e. U E. a e. ( X filGen F ) ( a X. a ) C_ v )
20 iscfilu 
 |-  ( U e. ( UnifOn ` X ) -> ( ( X filGen F ) e. ( CauFilU ` U ) <-> ( ( X filGen F ) e. ( fBas ` X ) /\ A. v e. U E. a e. ( X filGen F ) ( a X. a ) C_ v ) ) )
21 20 adantr 
 |-  ( ( U e. ( UnifOn ` X ) /\ F e. ( CauFilU ` U ) ) -> ( ( X filGen F ) e. ( CauFilU ` U ) <-> ( ( X filGen F ) e. ( fBas ` X ) /\ A. v e. U E. a e. ( X filGen F ) ( a X. a ) C_ v ) ) )
22 4 19 21 mpbir2and 
 |-  ( ( U e. ( UnifOn ` X ) /\ F e. ( CauFilU ` U ) ) -> ( X filGen F ) e. ( CauFilU ` U ) )