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 )