# 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 ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\to {F}{↾}_{𝑡}{A}\in \mathrm{CauFilU}\left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)$

### Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\to {U}\in \mathrm{UnifOn}\left({X}\right)$
2 simp2l ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\to {F}\in \mathrm{CauFilU}\left({U}\right)$
3 iscfilu ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to \left({F}\in \mathrm{CauFilU}\left({U}\right)↔\left({F}\in \mathrm{fBas}\left({X}\right)\wedge \forall {v}\in {U}\phantom{\rule{.4em}{0ex}}\exists {a}\in {F}\phantom{\rule{.4em}{0ex}}{a}×{a}\subseteq {v}\right)\right)$
4 3 biimpa ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {F}\in \mathrm{CauFilU}\left({U}\right)\right)\to \left({F}\in \mathrm{fBas}\left({X}\right)\wedge \forall {v}\in {U}\phantom{\rule{.4em}{0ex}}\exists {a}\in {F}\phantom{\rule{.4em}{0ex}}{a}×{a}\subseteq {v}\right)$
5 1 2 4 syl2anc ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\to \left({F}\in \mathrm{fBas}\left({X}\right)\wedge \forall {v}\in {U}\phantom{\rule{.4em}{0ex}}\exists {a}\in {F}\phantom{\rule{.4em}{0ex}}{a}×{a}\subseteq {v}\right)$
6 5 simpld ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\to {F}\in \mathrm{fBas}\left({X}\right)$
7 simp3 ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\to {A}\subseteq {X}$
8 simp2r ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\to ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)$
9 trfbas2 ${⊢}\left({F}\in \mathrm{fBas}\left({X}\right)\wedge {A}\subseteq {X}\right)\to \left({F}{↾}_{𝑡}{A}\in \mathrm{fBas}\left({A}\right)↔¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)$
10 9 biimpar ${⊢}\left(\left({F}\in \mathrm{fBas}\left({X}\right)\wedge {A}\subseteq {X}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\to {F}{↾}_{𝑡}{A}\in \mathrm{fBas}\left({A}\right)$
11 6 7 8 10 syl21anc ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\to {F}{↾}_{𝑡}{A}\in \mathrm{fBas}\left({A}\right)$
12 2 ad5antr ${⊢}\left(\left(\left(\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\wedge {w}\in \left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)\right)\wedge {v}\in {U}\right)\wedge {w}={v}\cap \left({A}×{A}\right)\right)\wedge {a}\in {F}\right)\wedge {a}×{a}\subseteq {v}\right)\to {F}\in \mathrm{CauFilU}\left({U}\right)$
13 1 adantr ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\wedge {w}\in \left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)\right)\to {U}\in \mathrm{UnifOn}\left({X}\right)$
14 13 elfvexd ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\wedge {w}\in \left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)\right)\to {X}\in \mathrm{V}$
15 7 adantr ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\wedge {w}\in \left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)\right)\to {A}\subseteq {X}$
16 14 15 ssexd ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\wedge {w}\in \left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)\right)\to {A}\in \mathrm{V}$
17 16 ad4antr ${⊢}\left(\left(\left(\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\wedge {w}\in \left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)\right)\wedge {v}\in {U}\right)\wedge {w}={v}\cap \left({A}×{A}\right)\right)\wedge {a}\in {F}\right)\wedge {a}×{a}\subseteq {v}\right)\to {A}\in \mathrm{V}$
18 simplr ${⊢}\left(\left(\left(\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\wedge {w}\in \left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)\right)\wedge {v}\in {U}\right)\wedge {w}={v}\cap \left({A}×{A}\right)\right)\wedge {a}\in {F}\right)\wedge {a}×{a}\subseteq {v}\right)\to {a}\in {F}$
19 elrestr ${⊢}\left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge {A}\in \mathrm{V}\wedge {a}\in {F}\right)\to {a}\cap {A}\in \left({F}{↾}_{𝑡}{A}\right)$
20 12 17 18 19 syl3anc ${⊢}\left(\left(\left(\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\wedge {w}\in \left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)\right)\wedge {v}\in {U}\right)\wedge {w}={v}\cap \left({A}×{A}\right)\right)\wedge {a}\in {F}\right)\wedge {a}×{a}\subseteq {v}\right)\to {a}\cap {A}\in \left({F}{↾}_{𝑡}{A}\right)$
21 inxp ${⊢}\left({a}×{a}\right)\cap \left({A}×{A}\right)=\left({a}\cap {A}\right)×\left({a}\cap {A}\right)$
22 simpr ${⊢}\left(\left(\left(\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\wedge {w}\in \left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)\right)\wedge {v}\in {U}\right)\wedge {w}={v}\cap \left({A}×{A}\right)\right)\wedge {a}\in {F}\right)\wedge {a}×{a}\subseteq {v}\right)\to {a}×{a}\subseteq {v}$
23 22 ssrind ${⊢}\left(\left(\left(\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\wedge {w}\in \left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)\right)\wedge {v}\in {U}\right)\wedge {w}={v}\cap \left({A}×{A}\right)\right)\wedge {a}\in {F}\right)\wedge {a}×{a}\subseteq {v}\right)\to \left({a}×{a}\right)\cap \left({A}×{A}\right)\subseteq {v}\cap \left({A}×{A}\right)$
24 simpllr ${⊢}\left(\left(\left(\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\wedge {w}\in \left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)\right)\wedge {v}\in {U}\right)\wedge {w}={v}\cap \left({A}×{A}\right)\right)\wedge {a}\in {F}\right)\wedge {a}×{a}\subseteq {v}\right)\to {w}={v}\cap \left({A}×{A}\right)$
25 23 24 sseqtrrd ${⊢}\left(\left(\left(\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\wedge {w}\in \left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)\right)\wedge {v}\in {U}\right)\wedge {w}={v}\cap \left({A}×{A}\right)\right)\wedge {a}\in {F}\right)\wedge {a}×{a}\subseteq {v}\right)\to \left({a}×{a}\right)\cap \left({A}×{A}\right)\subseteq {w}$
26 21 25 eqsstrrid ${⊢}\left(\left(\left(\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\wedge {w}\in \left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)\right)\wedge {v}\in {U}\right)\wedge {w}={v}\cap \left({A}×{A}\right)\right)\wedge {a}\in {F}\right)\wedge {a}×{a}\subseteq {v}\right)\to \left({a}\cap {A}\right)×\left({a}\cap {A}\right)\subseteq {w}$
27 id ${⊢}{b}={a}\cap {A}\to {b}={a}\cap {A}$
28 27 sqxpeqd ${⊢}{b}={a}\cap {A}\to {b}×{b}=\left({a}\cap {A}\right)×\left({a}\cap {A}\right)$
29 28 sseq1d ${⊢}{b}={a}\cap {A}\to \left({b}×{b}\subseteq {w}↔\left({a}\cap {A}\right)×\left({a}\cap {A}\right)\subseteq {w}\right)$
30 29 rspcev ${⊢}\left({a}\cap {A}\in \left({F}{↾}_{𝑡}{A}\right)\wedge \left({a}\cap {A}\right)×\left({a}\cap {A}\right)\subseteq {w}\right)\to \exists {b}\in \left({F}{↾}_{𝑡}{A}\right)\phantom{\rule{.4em}{0ex}}{b}×{b}\subseteq {w}$
31 20 26 30 syl2anc ${⊢}\left(\left(\left(\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\wedge {w}\in \left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)\right)\wedge {v}\in {U}\right)\wedge {w}={v}\cap \left({A}×{A}\right)\right)\wedge {a}\in {F}\right)\wedge {a}×{a}\subseteq {v}\right)\to \exists {b}\in \left({F}{↾}_{𝑡}{A}\right)\phantom{\rule{.4em}{0ex}}{b}×{b}\subseteq {w}$
32 5 simprd ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\to \forall {v}\in {U}\phantom{\rule{.4em}{0ex}}\exists {a}\in {F}\phantom{\rule{.4em}{0ex}}{a}×{a}\subseteq {v}$
33 32 r19.21bi ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\wedge {v}\in {U}\right)\to \exists {a}\in {F}\phantom{\rule{.4em}{0ex}}{a}×{a}\subseteq {v}$
34 33 ad4ant13 ${⊢}\left(\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\wedge {w}\in \left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)\right)\wedge {v}\in {U}\right)\wedge {w}={v}\cap \left({A}×{A}\right)\right)\to \exists {a}\in {F}\phantom{\rule{.4em}{0ex}}{a}×{a}\subseteq {v}$
35 31 34 r19.29a ${⊢}\left(\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\wedge {w}\in \left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)\right)\wedge {v}\in {U}\right)\wedge {w}={v}\cap \left({A}×{A}\right)\right)\to \exists {b}\in \left({F}{↾}_{𝑡}{A}\right)\phantom{\rule{.4em}{0ex}}{b}×{b}\subseteq {w}$
36 16 16 xpexd ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\wedge {w}\in \left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)\right)\to {A}×{A}\in \mathrm{V}$
37 simpr ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\wedge {w}\in \left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)\right)\to {w}\in \left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)$
38 elrest ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {A}×{A}\in \mathrm{V}\right)\to \left({w}\in \left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)↔\exists {v}\in {U}\phantom{\rule{.4em}{0ex}}{w}={v}\cap \left({A}×{A}\right)\right)$
39 38 biimpa ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {A}×{A}\in \mathrm{V}\right)\wedge {w}\in \left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)\right)\to \exists {v}\in {U}\phantom{\rule{.4em}{0ex}}{w}={v}\cap \left({A}×{A}\right)$
40 13 36 37 39 syl21anc ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\wedge {w}\in \left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)\right)\to \exists {v}\in {U}\phantom{\rule{.4em}{0ex}}{w}={v}\cap \left({A}×{A}\right)$
41 35 40 r19.29a ${⊢}\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\wedge {w}\in \left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)\right)\to \exists {b}\in \left({F}{↾}_{𝑡}{A}\right)\phantom{\rule{.4em}{0ex}}{b}×{b}\subseteq {w}$
42 41 ralrimiva ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\to \forall {w}\in \left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {b}\in \left({F}{↾}_{𝑡}{A}\right)\phantom{\rule{.4em}{0ex}}{b}×{b}\subseteq {w}$
43 trust ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {A}\subseteq {X}\right)\to {U}{↾}_{𝑡}\left({A}×{A}\right)\in \mathrm{UnifOn}\left({A}\right)$
44 1 7 43 syl2anc ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\to {U}{↾}_{𝑡}\left({A}×{A}\right)\in \mathrm{UnifOn}\left({A}\right)$
45 iscfilu ${⊢}{U}{↾}_{𝑡}\left({A}×{A}\right)\in \mathrm{UnifOn}\left({A}\right)\to \left({F}{↾}_{𝑡}{A}\in \mathrm{CauFilU}\left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)↔\left({F}{↾}_{𝑡}{A}\in \mathrm{fBas}\left({A}\right)\wedge \forall {w}\in \left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {b}\in \left({F}{↾}_{𝑡}{A}\right)\phantom{\rule{.4em}{0ex}}{b}×{b}\subseteq {w}\right)\right)$
46 44 45 syl ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\to \left({F}{↾}_{𝑡}{A}\in \mathrm{CauFilU}\left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)↔\left({F}{↾}_{𝑡}{A}\in \mathrm{fBas}\left({A}\right)\wedge \forall {w}\in \left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)\phantom{\rule{.4em}{0ex}}\exists {b}\in \left({F}{↾}_{𝑡}{A}\right)\phantom{\rule{.4em}{0ex}}{b}×{b}\subseteq {w}\right)\right)$
47 11 42 46 mpbir2and ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge \left({F}\in \mathrm{CauFilU}\left({U}\right)\wedge ¬\varnothing \in \left({F}{↾}_{𝑡}{A}\right)\right)\wedge {A}\subseteq {X}\right)\to {F}{↾}_{𝑡}{A}\in \mathrm{CauFilU}\left({U}{↾}_{𝑡}\left({A}×{A}\right)\right)$