This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cfiluexsm

Description: For a Cauchy filter base and any entourage V , there is an element of the filter small in V . (Contributed by Thierry Arnoux, 19-Nov-2017)

Ref Expression
Assertion cfiluexsm 
|- ( ( U e. ( UnifOn ` X ) /\ F e. ( CauFilU ` U ) /\ V e. U ) -> E. a e. F ( a X. a ) C_ V )

Proof

Step Hyp Ref Expression
1 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 ) ) )
2 1 simplbda 
 |-  ( ( U e. ( UnifOn ` X ) /\ F e. ( CauFilU ` U ) ) -> A. v e. U E. a e. F ( a X. a ) C_ v )
3 2 3adant3 
 |-  ( ( U e. ( UnifOn ` X ) /\ F e. ( CauFilU ` U ) /\ V e. U ) -> A. v e. U E. a e. F ( a X. a ) C_ v )
4 sseq2 
 |-  ( v = V -> ( ( a X. a ) C_ v <-> ( a X. a ) C_ V ) )
5 4 rexbidv 
 |-  ( v = V -> ( E. a e. F ( a X. a ) C_ v <-> E. a e. F ( a X. a ) C_ V ) )
6 5 rspcv 
 |-  ( V e. U -> ( A. v e. U E. a e. F ( a X. a ) C_ v -> E. a e. F ( a X. a ) C_ V ) )
7 6 3ad2ant3 
 |-  ( ( U e. ( UnifOn ` X ) /\ F e. ( CauFilU ` U ) /\ V e. U ) -> ( A. v e. U E. a e. F ( a X. a ) C_ v -> E. a e. F ( a X. a ) C_ V ) )
8 3 7 mpd 
 |-  ( ( U e. ( UnifOn ` X ) /\ F e. ( CauFilU ` U ) /\ V e. U ) -> E. a e. F ( a X. a ) C_ V )