Metamath Proof Explorer

Theorem trcfilu

Description: Condition for the trace of a Cauchy filter base to be a Cauchy filter base for the restricted uniform structure. (Contributed by Thierry Arnoux, 24-Jan-2018)

Ref Expression
Assertion trcfilu 
|- ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) -> ( F |`t A ) e. ( CauFilU ` ( U |`t ( A X. A ) ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) -> U e. ( UnifOn ` X ) )
2 simp2l 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) -> F e. ( CauFilU ` U ) )
3 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 ) ) )
4 3 biimpa 
 |-  ( ( 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 ) )
5 1 2 4 syl2anc 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) -> ( F e. ( fBas ` X ) /\ A. v e. U E. a e. F ( a X. a ) C_ v ) )
6 5 simpld 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) -> F e. ( fBas ` X ) )
7 simp3 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) -> A C_ X )
8 simp2r 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) -> -. (/) e. ( F |`t A ) )
9 trfbas2 
 |-  ( ( F e. ( fBas ` X ) /\ A C_ X ) -> ( ( F |`t A ) e. ( fBas ` A ) <-> -. (/) e. ( F |`t A ) ) )
10 9 biimpar 
 |-  ( ( ( F e. ( fBas ` X ) /\ A C_ X ) /\ -. (/) e. ( F |`t A ) ) -> ( F |`t A ) e. ( fBas ` A ) )
11 6 7 8 10 syl21anc 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) -> ( F |`t A ) e. ( fBas ` A ) )
12 2 ad5antr 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) /\ w e. ( U |`t ( A X. A ) ) ) /\ v e. U ) /\ w = ( v i^i ( A X. A ) ) ) /\ a e. F ) /\ ( a X. a ) C_ v ) -> F e. ( CauFilU ` U ) )
13 1 adantr 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) /\ w e. ( U |`t ( A X. A ) ) ) -> U e. ( UnifOn ` X ) )
14 13 elfvexd 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) /\ w e. ( U |`t ( A X. A ) ) ) -> X e. _V )
15 7 adantr 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) /\ w e. ( U |`t ( A X. A ) ) ) -> A C_ X )
16 14 15 ssexd 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) /\ w e. ( U |`t ( A X. A ) ) ) -> A e. _V )
17 16 ad4antr 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) /\ w e. ( U |`t ( A X. A ) ) ) /\ v e. U ) /\ w = ( v i^i ( A X. A ) ) ) /\ a e. F ) /\ ( a X. a ) C_ v ) -> A e. _V )
18 simplr 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) /\ w e. ( U |`t ( A X. A ) ) ) /\ v e. U ) /\ w = ( v i^i ( A X. A ) ) ) /\ a e. F ) /\ ( a X. a ) C_ v ) -> a e. F )
19 elrestr 
 |-  ( ( F e. ( CauFilU ` U ) /\ A e. _V /\ a e. F ) -> ( a i^i A ) e. ( F |`t A ) )
20 12 17 18 19 syl3anc 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) /\ w e. ( U |`t ( A X. A ) ) ) /\ v e. U ) /\ w = ( v i^i ( A X. A ) ) ) /\ a e. F ) /\ ( a X. a ) C_ v ) -> ( a i^i A ) e. ( F |`t A ) )
21 inxp 
 |-  ( ( a X. a ) i^i ( A X. A ) ) = ( ( a i^i A ) X. ( a i^i A ) )
22 simpr 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) /\ w e. ( U |`t ( A X. A ) ) ) /\ v e. U ) /\ w = ( v i^i ( A X. A ) ) ) /\ a e. F ) /\ ( a X. a ) C_ v ) -> ( a X. a ) C_ v )
23 22 ssrind 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) /\ w e. ( U |`t ( A X. A ) ) ) /\ v e. U ) /\ w = ( v i^i ( A X. A ) ) ) /\ a e. F ) /\ ( a X. a ) C_ v ) -> ( ( a X. a ) i^i ( A X. A ) ) C_ ( v i^i ( A X. A ) ) )
24 simpllr 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) /\ w e. ( U |`t ( A X. A ) ) ) /\ v e. U ) /\ w = ( v i^i ( A X. A ) ) ) /\ a e. F ) /\ ( a X. a ) C_ v ) -> w = ( v i^i ( A X. A ) ) )
25 23 24 sseqtrrd 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) /\ w e. ( U |`t ( A X. A ) ) ) /\ v e. U ) /\ w = ( v i^i ( A X. A ) ) ) /\ a e. F ) /\ ( a X. a ) C_ v ) -> ( ( a X. a ) i^i ( A X. A ) ) C_ w )
26 21 25 eqsstrrid 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) /\ w e. ( U |`t ( A X. A ) ) ) /\ v e. U ) /\ w = ( v i^i ( A X. A ) ) ) /\ a e. F ) /\ ( a X. a ) C_ v ) -> ( ( a i^i A ) X. ( a i^i A ) ) C_ w )
27 id 
 |-  ( b = ( a i^i A ) -> b = ( a i^i A ) )
28 27 sqxpeqd 
 |-  ( b = ( a i^i A ) -> ( b X. b ) = ( ( a i^i A ) X. ( a i^i A ) ) )
29 28 sseq1d 
 |-  ( b = ( a i^i A ) -> ( ( b X. b ) C_ w <-> ( ( a i^i A ) X. ( a i^i A ) ) C_ w ) )
30 29 rspcev 
 |-  ( ( ( a i^i A ) e. ( F |`t A ) /\ ( ( a i^i A ) X. ( a i^i A ) ) C_ w ) -> E. b e. ( F |`t A ) ( b X. b ) C_ w )
31 20 26 30 syl2anc 
 |-  ( ( ( ( ( ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) /\ w e. ( U |`t ( A X. A ) ) ) /\ v e. U ) /\ w = ( v i^i ( A X. A ) ) ) /\ a e. F ) /\ ( a X. a ) C_ v ) -> E. b e. ( F |`t A ) ( b X. b ) C_ w )
32 5 simprd 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) -> A. v e. U E. a e. F ( a X. a ) C_ v )
33 32 r19.21bi 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) /\ v e. U ) -> E. a e. F ( a X. a ) C_ v )
34 33 ad4ant13 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) /\ w e. ( U |`t ( A X. A ) ) ) /\ v e. U ) /\ w = ( v i^i ( A X. A ) ) ) -> E. a e. F ( a X. a ) C_ v )
35 31 34 r19.29a 
 |-  ( ( ( ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) /\ w e. ( U |`t ( A X. A ) ) ) /\ v e. U ) /\ w = ( v i^i ( A X. A ) ) ) -> E. b e. ( F |`t A ) ( b X. b ) C_ w )
36 16 16 xpexd 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) /\ w e. ( U |`t ( A X. A ) ) ) -> ( A X. A ) e. _V )
37 simpr 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) /\ w e. ( U |`t ( A X. A ) ) ) -> w e. ( U |`t ( A X. A ) ) )
38 elrest 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( A X. A ) e. _V ) -> ( w e. ( U |`t ( A X. A ) ) <-> E. v e. U w = ( v i^i ( A X. A ) ) ) )
39 38 biimpa 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( A X. A ) e. _V ) /\ w e. ( U |`t ( A X. A ) ) ) -> E. v e. U w = ( v i^i ( A X. A ) ) )
40 13 36 37 39 syl21anc 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) /\ w e. ( U |`t ( A X. A ) ) ) -> E. v e. U w = ( v i^i ( A X. A ) ) )
41 35 40 r19.29a 
 |-  ( ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) /\ w e. ( U |`t ( A X. A ) ) ) -> E. b e. ( F |`t A ) ( b X. b ) C_ w )
42 41 ralrimiva 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) -> A. w e. ( U |`t ( A X. A ) ) E. b e. ( F |`t A ) ( b X. b ) C_ w )
43 trust 
 |-  ( ( U e. ( UnifOn ` X ) /\ A C_ X ) -> ( U |`t ( A X. A ) ) e. ( UnifOn ` A ) )
44 1 7 43 syl2anc 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) -> ( U |`t ( A X. A ) ) e. ( UnifOn ` A ) )
45 iscfilu 
 |-  ( ( U |`t ( A X. A ) ) e. ( UnifOn ` A ) -> ( ( F |`t A ) e. ( CauFilU ` ( U |`t ( A X. A ) ) ) <-> ( ( F |`t A ) e. ( fBas ` A ) /\ A. w e. ( U |`t ( A X. A ) ) E. b e. ( F |`t A ) ( b X. b ) C_ w ) ) )
46 44 45 syl 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) -> ( ( F |`t A ) e. ( CauFilU ` ( U |`t ( A X. A ) ) ) <-> ( ( F |`t A ) e. ( fBas ` A ) /\ A. w e. ( U |`t ( A X. A ) ) E. b e. ( F |`t A ) ( b X. b ) C_ w ) ) )
47 11 42 46 mpbir2and 
 |-  ( ( U e. ( UnifOn ` X ) /\ ( F e. ( CauFilU ` U ) /\ -. (/) e. ( F |`t A ) ) /\ A C_ X ) -> ( F |`t A ) e. ( CauFilU ` ( U |`t ( A X. A ) ) ) )