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 ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐹 ↾t 𝐴 ) ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
2 simp2l ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐹 ∈ ( CauFilu ‘ 𝑈 ) )
3 iscfilu ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ↔ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) ) )
4 3 biimpa ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ) → ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) )
5 1 2 4 syl2anc ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) )
6 5 simpld ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
7 simp3 ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ⊆ 𝑋 )
8 simp2r ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) → ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) )
9 trfbas2 ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) ↔ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) )
10 9 biimpar ⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) → ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) )
11 6 7 8 10 syl21anc ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) )
12 2 ad5antr ⊢ ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑤 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐹 ) ∧ ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) → 𝐹 ∈ ( CauFilu ‘ 𝑈 ) )
13 1 adantr ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑤 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
14 13 elfvexd ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑤 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) → 𝑋 ∈ V )
15 7 adantr ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑤 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) → 𝐴 ⊆ 𝑋 )
16 14 15 ssexd ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑤 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) → 𝐴 ∈ V )
17 16 ad4antr ⊢ ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑤 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐹 ) ∧ ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) → 𝐴 ∈ V )
18 simplr ⊢ ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑤 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐹 ) ∧ ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) → 𝑎 ∈ 𝐹 )
19 elrestr ⊢ ( ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ 𝐴 ∈ V ∧ 𝑎 ∈ 𝐹 ) → ( 𝑎 ∩ 𝐴 ) ∈ ( 𝐹 ↾t 𝐴 ) )
20 12 17 18 19 syl3anc ⊢ ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑤 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐹 ) ∧ ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) → ( 𝑎 ∩ 𝐴 ) ∈ ( 𝐹 ↾t 𝐴 ) )
21 inxp ⊢ ( ( 𝑎 × 𝑎 ) ∩ ( 𝐴 × 𝐴 ) ) = ( ( 𝑎 ∩ 𝐴 ) × ( 𝑎 ∩ 𝐴 ) )
22 simpr ⊢ ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑤 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐹 ) ∧ ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) → ( 𝑎 × 𝑎 ) ⊆ 𝑣 )
23 22 ssrind ⊢ ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑤 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐹 ) ∧ ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) → ( ( 𝑎 × 𝑎 ) ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) )
24 simpllr ⊢ ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑤 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐹 ) ∧ ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) → 𝑤 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) )
25 23 24 sseqtrrd ⊢ ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑤 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐹 ) ∧ ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) → ( ( 𝑎 × 𝑎 ) ∩ ( 𝐴 × 𝐴 ) ) ⊆ 𝑤 )
26 21 25 eqsstrrid ⊢ ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑤 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐹 ) ∧ ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) → ( ( 𝑎 ∩ 𝐴 ) × ( 𝑎 ∩ 𝐴 ) ) ⊆ 𝑤 )
27 id ⊢ ( 𝑏 = ( 𝑎 ∩ 𝐴 ) → 𝑏 = ( 𝑎 ∩ 𝐴 ) )
28 27 sqxpeqd ⊢ ( 𝑏 = ( 𝑎 ∩ 𝐴 ) → ( 𝑏 × 𝑏 ) = ( ( 𝑎 ∩ 𝐴 ) × ( 𝑎 ∩ 𝐴 ) ) )
29 28 sseq1d ⊢ ( 𝑏 = ( 𝑎 ∩ 𝐴 ) → ( ( 𝑏 × 𝑏 ) ⊆ 𝑤 ↔ ( ( 𝑎 ∩ 𝐴 ) × ( 𝑎 ∩ 𝐴 ) ) ⊆ 𝑤 ) )
30 29 rspcev ⊢ ( ( ( 𝑎 ∩ 𝐴 ) ∈ ( 𝐹 ↾t 𝐴 ) ∧ ( ( 𝑎 ∩ 𝐴 ) × ( 𝑎 ∩ 𝐴 ) ) ⊆ 𝑤 ) → ∃ 𝑏 ∈ ( 𝐹 ↾t 𝐴 ) ( 𝑏 × 𝑏 ) ⊆ 𝑤 )
31 20 26 30 syl2anc ⊢ ( ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑤 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ 𝑎 ∈ 𝐹 ) ∧ ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) → ∃ 𝑏 ∈ ( 𝐹 ↾t 𝐴 ) ( 𝑏 × 𝑏 ) ⊆ 𝑤 )
32 5 simprd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) → ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 )
33 32 r19.21bi ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) → ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 )
34 33 ad4ant13 ⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑤 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) → ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 )
35 31 34 r19.29a ⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑤 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) → ∃ 𝑏 ∈ ( 𝐹 ↾t 𝐴 ) ( 𝑏 × 𝑏 ) ⊆ 𝑤 )
36 16 16 xpexd ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑤 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) → ( 𝐴 × 𝐴 ) ∈ V )
37 simpr ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑤 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) → 𝑤 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) )
38 elrest ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐴 × 𝐴 ) ∈ V ) → ( 𝑤 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ↔ ∃ 𝑣 ∈ 𝑈 𝑤 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) ) )
39 38 biimpa ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐴 × 𝐴 ) ∈ V ) ∧ 𝑤 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) → ∃ 𝑣 ∈ 𝑈 𝑤 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) )
40 13 36 37 39 syl21anc ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑤 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) → ∃ 𝑣 ∈ 𝑈 𝑤 = ( 𝑣 ∩ ( 𝐴 × 𝐴 ) ) )
41 35 40 r19.29a ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑤 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) → ∃ 𝑏 ∈ ( 𝐹 ↾t 𝐴 ) ( 𝑏 × 𝑏 ) ⊆ 𝑤 )
42 41 ralrimiva ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) → ∀ 𝑤 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ∃ 𝑏 ∈ ( 𝐹 ↾t 𝐴 ) ( 𝑏 × 𝑏 ) ⊆ 𝑤 )
43 trust ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ∈ ( UnifOn ‘ 𝐴 ) )
44 1 7 43 syl2anc ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ∈ ( UnifOn ‘ 𝐴 ) )
45 iscfilu ⊢ ( ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ∈ ( UnifOn ‘ 𝐴 ) → ( ( 𝐹 ↾t 𝐴 ) ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ↔ ( ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) ∧ ∀ 𝑤 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ∃ 𝑏 ∈ ( 𝐹 ↾t 𝐴 ) ( 𝑏 × 𝑏 ) ⊆ 𝑤 ) ) )
46 44 45 syl ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝐹 ↾t 𝐴 ) ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) ↔ ( ( 𝐹 ↾t 𝐴 ) ∈ ( fBas ‘ 𝐴 ) ∧ ∀ 𝑤 ∈ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ∃ 𝑏 ∈ ( 𝐹 ↾t 𝐴 ) ( 𝑏 × 𝑏 ) ⊆ 𝑤 ) ) )
47 11 42 46 mpbir2and ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ∧ ¬ ∅ ∈ ( 𝐹 ↾t 𝐴 ) ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐹 ↾t 𝐴 ) ∈ ( CauFilu ‘ ( 𝑈 ↾t ( 𝐴 × 𝐴 ) ) ) )