Metamath Proof Explorer

Theorem neipcfilu

Description: In an uniform space, a neighboring filter is a Cauchy filter base. (Contributed by Thierry Arnoux, 24-Jan-2018)

Ref Expression
Hypotheses neipcfilu.x 
|- X = ( Base ` W )
neipcfilu.j 
|- J = ( TopOpen ` W )
neipcfilu.u 
|- U = ( UnifSt ` W )
Assertion neipcfilu 
|- ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) -> ( ( nei ` J ) ` { P } ) e. ( CauFilU ` U ) )

Proof

Step Hyp Ref Expression
1 neipcfilu.x 
 |-  X = ( Base ` W )
2 neipcfilu.j 
 |-  J = ( TopOpen ` W )
3 neipcfilu.u 
 |-  U = ( UnifSt ` W )
4 simp2 
 |-  ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) -> W e. TopSp )
5 1 2 istps 
 |-  ( W e. TopSp <-> J e. ( TopOn ` X ) )
6 4 5 sylib 
 |-  ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) -> J e. ( TopOn ` X ) )
7 simp3 
 |-  ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) -> P e. X )
8 7 snssd 
 |-  ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) -> { P } C_ X )
9 snnzg 
 |-  ( P e. X -> { P } =/= (/) )
10 7 9 syl 
 |-  ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) -> { P } =/= (/) )
11 neifil 
 |-  ( ( J e. ( TopOn ` X ) /\ { P } C_ X /\ { P } =/= (/) ) -> ( ( nei ` J ) ` { P } ) e. ( Fil ` X ) )
12 6 8 10 11 syl3anc 
 |-  ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) -> ( ( nei ` J ) ` { P } ) e. ( Fil ` X ) )
13 filfbas 
 |-  ( ( ( nei ` J ) ` { P } ) e. ( Fil ` X ) -> ( ( nei ` J ) ` { P } ) e. ( fBas ` X ) )
14 12 13 syl 
 |-  ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) -> ( ( nei ` J ) ` { P } ) e. ( fBas ` X ) )
15 eqid 
 |-  ( w " { P } ) = ( w " { P } )
16 imaeq1 
 |-  ( v = w -> ( v " { P } ) = ( w " { P } ) )
17 16 rspceeqv 
 |-  ( ( w e. U /\ ( w " { P } ) = ( w " { P } ) ) -> E. v e. U ( w " { P } ) = ( v " { P } ) )
18 15 17 mpan2 
 |-  ( w e. U -> E. v e. U ( w " { P } ) = ( v " { P } ) )
19 vex 
 |-  w e. _V
20 19 imaex 
 |-  ( w " { P } ) e. _V
21 eqid 
 |-  ( v e. U |-> ( v " { P } ) ) = ( v e. U |-> ( v " { P } ) )
22 21 elrnmpt 
 |-  ( ( w " { P } ) e. _V -> ( ( w " { P } ) e. ran ( v e. U |-> ( v " { P } ) ) <-> E. v e. U ( w " { P } ) = ( v " { P } ) ) )
23 20 22 ax-mp 
 |-  ( ( w " { P } ) e. ran ( v e. U |-> ( v " { P } ) ) <-> E. v e. U ( w " { P } ) = ( v " { P } ) )
24 18 23 sylibr 
 |-  ( w e. U -> ( w " { P } ) e. ran ( v e. U |-> ( v " { P } ) ) )
25 24 ad2antlr 
 |-  ( ( ( ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) /\ v e. U ) /\ w e. U ) /\ ( ( w " { P } ) X. ( w " { P } ) ) C_ v ) -> ( w " { P } ) e. ran ( v e. U |-> ( v " { P } ) ) )
26 1 3 2 isusp 
 |-  ( W e. UnifSp <-> ( U e. ( UnifOn ` X ) /\ J = ( unifTop ` U ) ) )
27 26 simplbi 
 |-  ( W e. UnifSp -> U e. ( UnifOn ` X ) )
28 27 3ad2ant1 
 |-  ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) -> U e. ( UnifOn ` X ) )
29 eqid 
 |-  ( unifTop ` U ) = ( unifTop ` U )
30 29 utopsnneip 
 |-  ( ( U e. ( UnifOn ` X ) /\ P e. X ) -> ( ( nei ` ( unifTop ` U ) ) ` { P } ) = ran ( v e. U |-> ( v " { P } ) ) )
31 28 7 30 syl2anc 
 |-  ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) -> ( ( nei ` ( unifTop ` U ) ) ` { P } ) = ran ( v e. U |-> ( v " { P } ) ) )
32 31 eleq2d 
 |-  ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) -> ( ( w " { P } ) e. ( ( nei ` ( unifTop ` U ) ) ` { P } ) <-> ( w " { P } ) e. ran ( v e. U |-> ( v " { P } ) ) ) )
33 32 ad3antrrr 
 |-  ( ( ( ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) /\ v e. U ) /\ w e. U ) /\ ( ( w " { P } ) X. ( w " { P } ) ) C_ v ) -> ( ( w " { P } ) e. ( ( nei ` ( unifTop ` U ) ) ` { P } ) <-> ( w " { P } ) e. ran ( v e. U |-> ( v " { P } ) ) ) )
34 25 33 mpbird 
 |-  ( ( ( ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) /\ v e. U ) /\ w e. U ) /\ ( ( w " { P } ) X. ( w " { P } ) ) C_ v ) -> ( w " { P } ) e. ( ( nei ` ( unifTop ` U ) ) ` { P } ) )
35 simpl1 
 |-  ( ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) /\ ( v e. U /\ w e. U /\ ( ( w " { P } ) X. ( w " { P } ) ) C_ v ) ) -> W e. UnifSp )
36 35 3anassrs 
 |-  ( ( ( ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) /\ v e. U ) /\ w e. U ) /\ ( ( w " { P } ) X. ( w " { P } ) ) C_ v ) -> W e. UnifSp )
37 26 simprbi 
 |-  ( W e. UnifSp -> J = ( unifTop ` U ) )
38 36 37 syl 
 |-  ( ( ( ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) /\ v e. U ) /\ w e. U ) /\ ( ( w " { P } ) X. ( w " { P } ) ) C_ v ) -> J = ( unifTop ` U ) )
39 38 fveq2d 
 |-  ( ( ( ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) /\ v e. U ) /\ w e. U ) /\ ( ( w " { P } ) X. ( w " { P } ) ) C_ v ) -> ( nei ` J ) = ( nei ` ( unifTop ` U ) ) )
40 39 fveq1d 
 |-  ( ( ( ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) /\ v e. U ) /\ w e. U ) /\ ( ( w " { P } ) X. ( w " { P } ) ) C_ v ) -> ( ( nei ` J ) ` { P } ) = ( ( nei ` ( unifTop ` U ) ) ` { P } ) )
41 34 40 eleqtrrd 
 |-  ( ( ( ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) /\ v e. U ) /\ w e. U ) /\ ( ( w " { P } ) X. ( w " { P } ) ) C_ v ) -> ( w " { P } ) e. ( ( nei ` J ) ` { P } ) )
42 simpr 
 |-  ( ( ( ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) /\ v e. U ) /\ w e. U ) /\ ( ( w " { P } ) X. ( w " { P } ) ) C_ v ) -> ( ( w " { P } ) X. ( w " { P } ) ) C_ v )
43 id 
 |-  ( a = ( w " { P } ) -> a = ( w " { P } ) )
44 43 sqxpeqd 
 |-  ( a = ( w " { P } ) -> ( a X. a ) = ( ( w " { P } ) X. ( w " { P } ) ) )
45 44 sseq1d 
 |-  ( a = ( w " { P } ) -> ( ( a X. a ) C_ v <-> ( ( w " { P } ) X. ( w " { P } ) ) C_ v ) )
46 45 rspcev 
 |-  ( ( ( w " { P } ) e. ( ( nei ` J ) ` { P } ) /\ ( ( w " { P } ) X. ( w " { P } ) ) C_ v ) -> E. a e. ( ( nei ` J ) ` { P } ) ( a X. a ) C_ v )
47 41 42 46 syl2anc 
 |-  ( ( ( ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) /\ v e. U ) /\ w e. U ) /\ ( ( w " { P } ) X. ( w " { P } ) ) C_ v ) -> E. a e. ( ( nei ` J ) ` { P } ) ( a X. a ) C_ v )
48 28 adantr 
 |-  ( ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) /\ v e. U ) -> U e. ( UnifOn ` X ) )
49 7 adantr 
 |-  ( ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) /\ v e. U ) -> P e. X )
50 simpr 
 |-  ( ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) /\ v e. U ) -> v e. U )
51 simpll1 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ P e. X /\ v e. U ) /\ u e. U ) /\ ( u o. u ) C_ v ) -> U e. ( UnifOn ` X ) )
52 simplr 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ P e. X /\ v e. U ) /\ u e. U ) /\ ( u o. u ) C_ v ) -> u e. U )
53 ustexsym 
 |-  ( ( U e. ( UnifOn ` X ) /\ u e. U ) -> E. w e. U ( `' w = w /\ w C_ u ) )
54 51 52 53 syl2anc 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ P e. X /\ v e. U ) /\ u e. U ) /\ ( u o. u ) C_ v ) -> E. w e. U ( `' w = w /\ w C_ u ) )
55 51 ad2antrr 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ P e. X /\ v e. U ) /\ u e. U ) /\ ( u o. u ) C_ v ) /\ w e. U ) /\ ( `' w = w /\ w C_ u ) ) -> U e. ( UnifOn ` X ) )
56 simplr 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ P e. X /\ v e. U ) /\ u e. U ) /\ ( u o. u ) C_ v ) /\ w e. U ) /\ ( `' w = w /\ w C_ u ) ) -> w e. U )
57 ustssxp 
 |-  ( ( U e. ( UnifOn ` X ) /\ w e. U ) -> w C_ ( X X. X ) )
58 55 56 57 syl2anc 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ P e. X /\ v e. U ) /\ u e. U ) /\ ( u o. u ) C_ v ) /\ w e. U ) /\ ( `' w = w /\ w C_ u ) ) -> w C_ ( X X. X ) )
59 simpll2 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ P e. X /\ v e. U ) /\ u e. U ) /\ ( ( u o. u ) C_ v /\ w e. U /\ ( `' w = w /\ w C_ u ) ) ) -> P e. X )
60 59 3anassrs 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ P e. X /\ v e. U ) /\ u e. U ) /\ ( u o. u ) C_ v ) /\ w e. U ) /\ ( `' w = w /\ w C_ u ) ) -> P e. X )
61 ustneism 
 |-  ( ( w C_ ( X X. X ) /\ P e. X ) -> ( ( w " { P } ) X. ( w " { P } ) ) C_ ( w o. `' w ) )
62 58 60 61 syl2anc 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ P e. X /\ v e. U ) /\ u e. U ) /\ ( u o. u ) C_ v ) /\ w e. U ) /\ ( `' w = w /\ w C_ u ) ) -> ( ( w " { P } ) X. ( w " { P } ) ) C_ ( w o. `' w ) )
63 simprl 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ P e. X /\ v e. U ) /\ u e. U ) /\ ( u o. u ) C_ v ) /\ w e. U ) /\ ( `' w = w /\ w C_ u ) ) -> `' w = w )
64 63 coeq2d 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ P e. X /\ v e. U ) /\ u e. U ) /\ ( u o. u ) C_ v ) /\ w e. U ) /\ ( `' w = w /\ w C_ u ) ) -> ( w o. `' w ) = ( w o. w ) )
65 coss1 
 |-  ( w C_ u -> ( w o. w ) C_ ( u o. w ) )
66 coss2 
 |-  ( w C_ u -> ( u o. w ) C_ ( u o. u ) )
67 65 66 sstrd 
 |-  ( w C_ u -> ( w o. w ) C_ ( u o. u ) )
68 67 ad2antll 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ P e. X /\ v e. U ) /\ u e. U ) /\ ( u o. u ) C_ v ) /\ w e. U ) /\ ( `' w = w /\ w C_ u ) ) -> ( w o. w ) C_ ( u o. u ) )
69 simpllr 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ P e. X /\ v e. U ) /\ u e. U ) /\ ( u o. u ) C_ v ) /\ w e. U ) /\ ( `' w = w /\ w C_ u ) ) -> ( u o. u ) C_ v )
70 68 69 sstrd 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ P e. X /\ v e. U ) /\ u e. U ) /\ ( u o. u ) C_ v ) /\ w e. U ) /\ ( `' w = w /\ w C_ u ) ) -> ( w o. w ) C_ v )
71 64 70 eqsstrd 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ P e. X /\ v e. U ) /\ u e. U ) /\ ( u o. u ) C_ v ) /\ w e. U ) /\ ( `' w = w /\ w C_ u ) ) -> ( w o. `' w ) C_ v )
72 62 71 sstrd 
 |-  ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ P e. X /\ v e. U ) /\ u e. U ) /\ ( u o. u ) C_ v ) /\ w e. U ) /\ ( `' w = w /\ w C_ u ) ) -> ( ( w " { P } ) X. ( w " { P } ) ) C_ v )
73 72 ex 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ P e. X /\ v e. U ) /\ u e. U ) /\ ( u o. u ) C_ v ) /\ w e. U ) -> ( ( `' w = w /\ w C_ u ) -> ( ( w " { P } ) X. ( w " { P } ) ) C_ v ) )
74 73 reximdva 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ P e. X /\ v e. U ) /\ u e. U ) /\ ( u o. u ) C_ v ) -> ( E. w e. U ( `' w = w /\ w C_ u ) -> E. w e. U ( ( w " { P } ) X. ( w " { P } ) ) C_ v ) )
75 54 74 mpd 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ P e. X /\ v e. U ) /\ u e. U ) /\ ( u o. u ) C_ v ) -> E. w e. U ( ( w " { P } ) X. ( w " { P } ) ) C_ v )
76 ustexhalf 
 |-  ( ( U e. ( UnifOn ` X ) /\ v e. U ) -> E. u e. U ( u o. u ) C_ v )
77 76 3adant2 
 |-  ( ( U e. ( UnifOn ` X ) /\ P e. X /\ v e. U ) -> E. u e. U ( u o. u ) C_ v )
78 75 77 r19.29a 
 |-  ( ( U e. ( UnifOn ` X ) /\ P e. X /\ v e. U ) -> E. w e. U ( ( w " { P } ) X. ( w " { P } ) ) C_ v )
79 48 49 50 78 syl3anc 
 |-  ( ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) /\ v e. U ) -> E. w e. U ( ( w " { P } ) X. ( w " { P } ) ) C_ v )
80 47 79 r19.29a 
 |-  ( ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) /\ v e. U ) -> E. a e. ( ( nei ` J ) ` { P } ) ( a X. a ) C_ v )
81 80 ralrimiva 
 |-  ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) -> A. v e. U E. a e. ( ( nei ` J ) ` { P } ) ( a X. a ) C_ v )
82 iscfilu 
 |-  ( U e. ( UnifOn ` X ) -> ( ( ( nei ` J ) ` { P } ) e. ( CauFilU ` U ) <-> ( ( ( nei ` J ) ` { P } ) e. ( fBas ` X ) /\ A. v e. U E. a e. ( ( nei ` J ) ` { P } ) ( a X. a ) C_ v ) ) )
83 28 82 syl 
 |-  ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) -> ( ( ( nei ` J ) ` { P } ) e. ( CauFilU ` U ) <-> ( ( ( nei ` J ) ` { P } ) e. ( fBas ` X ) /\ A. v e. U E. a e. ( ( nei ` J ) ` { P } ) ( a X. a ) C_ v ) ) )
84 14 81 83 mpbir2and 
 |-  ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) -> ( ( nei ` J ) ` { P } ) e. ( CauFilU ` U ) )