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 7 snn0d 
 |-  ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) -> { P } =/= (/) )
10 neifil 
 |-  ( ( J e. ( TopOn ` X ) /\ { P } C_ X /\ { P } =/= (/) ) -> ( ( nei ` J ) ` { P } ) e. ( Fil ` X ) )
11 6 8 9 10 syl3anc 
 |-  ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) -> ( ( nei ` J ) ` { P } ) e. ( Fil ` X ) )
12 filfbas 
 |-  ( ( ( nei ` J ) ` { P } ) e. ( Fil ` X ) -> ( ( nei ` J ) ` { P } ) e. ( fBas ` X ) )
13 11 12 syl 
 |-  ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) -> ( ( nei ` J ) ` { P } ) e. ( fBas ` X ) )
14 eqid 
 |-  ( w " { P } ) = ( w " { P } )
15 imaeq1 
 |-  ( v = w -> ( v " { P } ) = ( w " { P } ) )
16 15 rspceeqv 
 |-  ( ( w e. U /\ ( w " { P } ) = ( w " { P } ) ) -> E. v e. U ( w " { P } ) = ( v " { P } ) )
17 14 16 mpan2 
 |-  ( w e. U -> E. v e. U ( w " { P } ) = ( v " { P } ) )
18 vex 
 |-  w e. _V
19 18 imaex 
 |-  ( w " { P } ) e. _V
20 eqid 
 |-  ( v e. U |-> ( v " { P } ) ) = ( v e. U |-> ( v " { P } ) )
21 20 elrnmpt 
 |-  ( ( w " { P } ) e. _V -> ( ( w " { P } ) e. ran ( v e. U |-> ( v " { P } ) ) <-> E. v e. U ( w " { P } ) = ( v " { P } ) ) )
22 19 21 ax-mp 
 |-  ( ( w " { P } ) e. ran ( v e. U |-> ( v " { P } ) ) <-> E. v e. U ( w " { P } ) = ( v " { P } ) )
23 17 22 sylibr 
 |-  ( w e. U -> ( w " { P } ) e. ran ( v e. U |-> ( v " { P } ) ) )
24 23 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 } ) ) )
25 1 3 2 isusp 
 |-  ( W e. UnifSp <-> ( U e. ( UnifOn ` X ) /\ J = ( unifTop ` U ) ) )
26 25 simplbi 
 |-  ( W e. UnifSp -> U e. ( UnifOn ` X ) )
27 26 3ad2ant1 
 |-  ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) -> U e. ( UnifOn ` X ) )
28 eqid 
 |-  ( unifTop ` U ) = ( unifTop ` U )
29 28 utopsnneip 
 |-  ( ( U e. ( UnifOn ` X ) /\ P e. X ) -> ( ( nei ` ( unifTop ` U ) ) ` { P } ) = ran ( v e. U |-> ( v " { P } ) ) )
30 27 7 29 syl2anc 
 |-  ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) -> ( ( nei ` ( unifTop ` U ) ) ` { P } ) = ran ( v e. U |-> ( v " { P } ) ) )
31 30 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 } ) ) ) )
32 31 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 } ) ) ) )
33 24 32 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 } ) )
34 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 )
35 34 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 )
36 25 simprbi 
 |-  ( W e. UnifSp -> J = ( unifTop ` U ) )
37 35 36 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 ) )
38 37 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 ) ) )
39 38 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 } ) )
40 33 39 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 } ) )
41 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 )
42 id 
 |-  ( a = ( w " { P } ) -> a = ( w " { P } ) )
43 42 sqxpeqd 
 |-  ( a = ( w " { P } ) -> ( a X. a ) = ( ( w " { P } ) X. ( w " { P } ) ) )
44 43 sseq1d 
 |-  ( a = ( w " { P } ) -> ( ( a X. a ) C_ v <-> ( ( w " { P } ) X. ( w " { P } ) ) C_ v ) )
45 44 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 )
46 40 41 45 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 )
47 27 adantr 
 |-  ( ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) /\ v e. U ) -> U e. ( UnifOn ` X ) )
48 7 adantr 
 |-  ( ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) /\ v e. U ) -> P e. X )
49 simpr 
 |-  ( ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) /\ v e. U ) -> v e. U )
50 simpll1 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ P e. X /\ v e. U ) /\ u e. U ) /\ ( u o. u ) C_ v ) -> U e. ( UnifOn ` X ) )
51 simplr 
 |-  ( ( ( ( U e. ( UnifOn ` X ) /\ P e. X /\ v e. U ) /\ u e. U ) /\ ( u o. u ) C_ v ) -> u e. U )
52 ustexsym 
 |-  ( ( U e. ( UnifOn ` X ) /\ u e. U ) -> E. w e. U ( `' w = w /\ w C_ u ) )
53 50 51 52 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 ) )
54 50 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 ) )
55 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 )
56 ustssxp 
 |-  ( ( U e. ( UnifOn ` X ) /\ w e. U ) -> w C_ ( X X. X ) )
57 54 55 56 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 ) )
58 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 )
59 58 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 )
60 ustneism 
 |-  ( ( w C_ ( X X. X ) /\ P e. X ) -> ( ( w " { P } ) X. ( w " { P } ) ) C_ ( w o. `' w ) )
61 57 59 60 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 ) )
62 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 )
63 62 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 ) )
64 coss1 
 |-  ( w C_ u -> ( w o. w ) C_ ( u o. w ) )
65 coss2 
 |-  ( w C_ u -> ( u o. w ) C_ ( u o. u ) )
66 64 65 sstrd 
 |-  ( w C_ u -> ( w o. w ) C_ ( u o. u ) )
67 66 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 ) )
68 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 )
69 67 68 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 )
70 63 69 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 )
71 61 70 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 )
72 71 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 ) )
73 72 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 ) )
74 53 73 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 )
75 ustexhalf 
 |-  ( ( U e. ( UnifOn ` X ) /\ v e. U ) -> E. u e. U ( u o. u ) C_ v )
76 75 3adant2 
 |-  ( ( U e. ( UnifOn ` X ) /\ P e. X /\ v e. U ) -> E. u e. U ( u o. u ) C_ v )
77 74 76 r19.29a 
 |-  ( ( U e. ( UnifOn ` X ) /\ P e. X /\ v e. U ) -> E. w e. U ( ( w " { P } ) X. ( w " { P } ) ) C_ v )
78 47 48 49 77 syl3anc 
 |-  ( ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) /\ v e. U ) -> E. w e. U ( ( w " { P } ) X. ( w " { P } ) ) C_ v )
79 46 78 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 )
80 79 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 )
81 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 ) ) )
82 27 81 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 ) ) )
83 13 80 82 mpbir2and 
 |-  ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) -> ( ( nei ` J ) ` { P } ) e. ( CauFilU ` U ) )