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 ⊢ 𝑋 = ( Base ‘ 𝑊 )
neipcfilu.j ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
neipcfilu.u ⊢ 𝑈 = ( UnifSt ‘ 𝑊 )
Assertion neipcfilu ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∈ ( CauFilu ‘ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 neipcfilu.x ⊢ 𝑋 = ( Base ‘ 𝑊 )
2 neipcfilu.j ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
3 neipcfilu.u ⊢ 𝑈 = ( UnifSt ‘ 𝑊 )
4 simp2 ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) → 𝑊 ∈ TopSp )
5 1 2 istps ⊢ ( 𝑊 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
6 4 5 sylib ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
7 simp3 ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) → 𝑃 ∈ 𝑋 )
8 7 snssd ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) → { 𝑃 } ⊆ 𝑋 )
9 snnzg ⊢ ( 𝑃 ∈ 𝑋 → { 𝑃 } ≠ ∅ )
10 7 9 syl ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) → { 𝑃 } ≠ ∅ )
11 neifil ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ { 𝑃 } ⊆ 𝑋 ∧ { 𝑃 } ≠ ∅ ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∈ ( Fil ‘ 𝑋 ) )
12 6 8 10 11 syl3anc ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∈ ( Fil ‘ 𝑋 ) )
13 filfbas ⊢ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∈ ( Fil ‘ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∈ ( fBas ‘ 𝑋 ) )
14 12 13 syl ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∈ ( fBas ‘ 𝑋 ) )
15 eqid ⊢ ( 𝑤 “ { 𝑃 } ) = ( 𝑤 “ { 𝑃 } )
16 imaeq1 ⊢ ( 𝑣 = 𝑤 → ( 𝑣 “ { 𝑃 } ) = ( 𝑤 “ { 𝑃 } ) )
17 16 rspceeqv ⊢ ( ( 𝑤 ∈ 𝑈 ∧ ( 𝑤 “ { 𝑃 } ) = ( 𝑤 “ { 𝑃 } ) ) → ∃ 𝑣 ∈ 𝑈 ( 𝑤 “ { 𝑃 } ) = ( 𝑣 “ { 𝑃 } ) )
18 15 17 mpan2 ⊢ ( 𝑤 ∈ 𝑈 → ∃ 𝑣 ∈ 𝑈 ( 𝑤 “ { 𝑃 } ) = ( 𝑣 “ { 𝑃 } ) )
19 vex ⊢ 𝑤 ∈ V
20 19 imaex ⊢ ( 𝑤 “ { 𝑃 } ) ∈ V
21 eqid ⊢ ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) = ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) )
22 21 elrnmpt ⊢ ( ( 𝑤 “ { 𝑃 } ) ∈ V → ( ( 𝑤 “ { 𝑃 } ) ∈ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ↔ ∃ 𝑣 ∈ 𝑈 ( 𝑤 “ { 𝑃 } ) = ( 𝑣 “ { 𝑃 } ) ) )
23 20 22 ax-mp ⊢ ( ( 𝑤 “ { 𝑃 } ) ∈ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ↔ ∃ 𝑣 ∈ 𝑈 ( 𝑤 “ { 𝑃 } ) = ( 𝑣 “ { 𝑃 } ) )
24 18 23 sylibr ⊢ ( 𝑤 ∈ 𝑈 → ( 𝑤 “ { 𝑃 } ) ∈ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) )
25 24 ad2antlr ⊢ ( ( ( ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ( 𝑤 “ { 𝑃 } ) × ( 𝑤 “ { 𝑃 } ) ) ⊆ 𝑣 ) → ( 𝑤 “ { 𝑃 } ) ∈ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) )
26 1 3 2 isusp ⊢ ( 𝑊 ∈ UnifSp ↔ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐽 = ( unifTop ‘ 𝑈 ) ) )
27 26 simplbi ⊢ ( 𝑊 ∈ UnifSp → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
28 27 3ad2ant1 ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
29 eqid ⊢ ( unifTop ‘ 𝑈 ) = ( unifTop ‘ 𝑈 )
30 29 utopsnneip ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( ( nei ‘ ( unifTop ‘ 𝑈 ) ) ‘ { 𝑃 } ) = ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) )
31 28 7 30 syl2anc ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) → ( ( nei ‘ ( unifTop ‘ 𝑈 ) ) ‘ { 𝑃 } ) = ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) )
32 31 eleq2d ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝑤 “ { 𝑃 } ) ∈ ( ( nei ‘ ( unifTop ‘ 𝑈 ) ) ‘ { 𝑃 } ) ↔ ( 𝑤 “ { 𝑃 } ) ∈ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ) )
33 32 ad3antrrr ⊢ ( ( ( ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ( 𝑤 “ { 𝑃 } ) × ( 𝑤 “ { 𝑃 } ) ) ⊆ 𝑣 ) → ( ( 𝑤 “ { 𝑃 } ) ∈ ( ( nei ‘ ( unifTop ‘ 𝑈 ) ) ‘ { 𝑃 } ) ↔ ( 𝑤 “ { 𝑃 } ) ∈ ran ( 𝑣 ∈ 𝑈 ↦ ( 𝑣 “ { 𝑃 } ) ) ) )
34 25 33 mpbird ⊢ ( ( ( ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ( 𝑤 “ { 𝑃 } ) × ( 𝑤 “ { 𝑃 } ) ) ⊆ 𝑣 ) → ( 𝑤 “ { 𝑃 } ) ∈ ( ( nei ‘ ( unifTop ‘ 𝑈 ) ) ‘ { 𝑃 } ) )
35 simpl1 ⊢ ( ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑣 ∈ 𝑈 ∧ 𝑤 ∈ 𝑈 ∧ ( ( 𝑤 “ { 𝑃 } ) × ( 𝑤 “ { 𝑃 } ) ) ⊆ 𝑣 ) ) → 𝑊 ∈ UnifSp )
36 35 3anassrs ⊢ ( ( ( ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ( 𝑤 “ { 𝑃 } ) × ( 𝑤 “ { 𝑃 } ) ) ⊆ 𝑣 ) → 𝑊 ∈ UnifSp )
37 26 simprbi ⊢ ( 𝑊 ∈ UnifSp → 𝐽 = ( unifTop ‘ 𝑈 ) )
38 36 37 syl ⊢ ( ( ( ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ( 𝑤 “ { 𝑃 } ) × ( 𝑤 “ { 𝑃 } ) ) ⊆ 𝑣 ) → 𝐽 = ( unifTop ‘ 𝑈 ) )
39 38 fveq2d ⊢ ( ( ( ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ( 𝑤 “ { 𝑃 } ) × ( 𝑤 “ { 𝑃 } ) ) ⊆ 𝑣 ) → ( nei ‘ 𝐽 ) = ( nei ‘ ( unifTop ‘ 𝑈 ) ) )
40 39 fveq1d ⊢ ( ( ( ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ( 𝑤 “ { 𝑃 } ) × ( 𝑤 “ { 𝑃 } ) ) ⊆ 𝑣 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) = ( ( nei ‘ ( unifTop ‘ 𝑈 ) ) ‘ { 𝑃 } ) )
41 34 40 eleqtrrd ⊢ ( ( ( ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ( 𝑤 “ { 𝑃 } ) × ( 𝑤 “ { 𝑃 } ) ) ⊆ 𝑣 ) → ( 𝑤 “ { 𝑃 } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) )
42 simpr ⊢ ( ( ( ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ( 𝑤 “ { 𝑃 } ) × ( 𝑤 “ { 𝑃 } ) ) ⊆ 𝑣 ) → ( ( 𝑤 “ { 𝑃 } ) × ( 𝑤 “ { 𝑃 } ) ) ⊆ 𝑣 )
43 id ⊢ ( 𝑎 = ( 𝑤 “ { 𝑃 } ) → 𝑎 = ( 𝑤 “ { 𝑃 } ) )
44 43 sqxpeqd ⊢ ( 𝑎 = ( 𝑤 “ { 𝑃 } ) → ( 𝑎 × 𝑎 ) = ( ( 𝑤 “ { 𝑃 } ) × ( 𝑤 “ { 𝑃 } ) ) )
45 44 sseq1d ⊢ ( 𝑎 = ( 𝑤 “ { 𝑃 } ) → ( ( 𝑎 × 𝑎 ) ⊆ 𝑣 ↔ ( ( 𝑤 “ { 𝑃 } ) × ( 𝑤 “ { 𝑃 } ) ) ⊆ 𝑣 ) )
46 45 rspcev ⊢ ( ( ( 𝑤 “ { 𝑃 } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∧ ( ( 𝑤 “ { 𝑃 } ) × ( 𝑤 “ { 𝑃 } ) ) ⊆ 𝑣 ) → ∃ 𝑎 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑎 × 𝑎 ) ⊆ 𝑣 )
47 41 42 46 syl2anc ⊢ ( ( ( ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ( 𝑤 “ { 𝑃 } ) × ( 𝑤 “ { 𝑃 } ) ) ⊆ 𝑣 ) → ∃ 𝑎 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑎 × 𝑎 ) ⊆ 𝑣 )
48 28 adantr ⊢ ( ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
49 7 adantr ⊢ ( ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) → 𝑃 ∈ 𝑋 )
50 simpr ⊢ ( ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) → 𝑣 ∈ 𝑈 )
51 simpll1 ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 ∘ 𝑢 ) ⊆ 𝑣 ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
52 simplr ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 ∘ 𝑢 ) ⊆ 𝑣 ) → 𝑢 ∈ 𝑈 )
53 ustexsym ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 ∈ 𝑈 ) → ∃ 𝑤 ∈ 𝑈 ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑢 ) )
54 51 52 53 syl2anc ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 ∘ 𝑢 ) ⊆ 𝑣 ) → ∃ 𝑤 ∈ 𝑈 ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑢 ) )
55 51 ad2antrr ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 ∘ 𝑢 ) ⊆ 𝑣 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑢 ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
56 simplr ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 ∘ 𝑢 ) ⊆ 𝑣 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑢 ) ) → 𝑤 ∈ 𝑈 )
57 ustssxp ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑤 ∈ 𝑈 ) → 𝑤 ⊆ ( 𝑋 × 𝑋 ) )
58 55 56 57 syl2anc ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 ∘ 𝑢 ) ⊆ 𝑣 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑢 ) ) → 𝑤 ⊆ ( 𝑋 × 𝑋 ) )
59 simpll2 ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( ( 𝑢 ∘ 𝑢 ) ⊆ 𝑣 ∧ 𝑤 ∈ 𝑈 ∧ ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑢 ) ) ) → 𝑃 ∈ 𝑋 )
60 59 3anassrs ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 ∘ 𝑢 ) ⊆ 𝑣 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑢 ) ) → 𝑃 ∈ 𝑋 )
61 ustneism ⊢ ( ( 𝑤 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝑤 “ { 𝑃 } ) × ( 𝑤 “ { 𝑃 } ) ) ⊆ ( 𝑤 ∘ ◡ 𝑤 ) )
62 58 60 61 syl2anc ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 ∘ 𝑢 ) ⊆ 𝑣 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑢 ) ) → ( ( 𝑤 “ { 𝑃 } ) × ( 𝑤 “ { 𝑃 } ) ) ⊆ ( 𝑤 ∘ ◡ 𝑤 ) )
63 simprl ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 ∘ 𝑢 ) ⊆ 𝑣 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑢 ) ) → ◡ 𝑤 = 𝑤 )
64 63 coeq2d ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 ∘ 𝑢 ) ⊆ 𝑣 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑢 ) ) → ( 𝑤 ∘ ◡ 𝑤 ) = ( 𝑤 ∘ 𝑤 ) )
65 coss1 ⊢ ( 𝑤 ⊆ 𝑢 → ( 𝑤 ∘ 𝑤 ) ⊆ ( 𝑢 ∘ 𝑤 ) )
66 coss2 ⊢ ( 𝑤 ⊆ 𝑢 → ( 𝑢 ∘ 𝑤 ) ⊆ ( 𝑢 ∘ 𝑢 ) )
67 65 66 sstrd ⊢ ( 𝑤 ⊆ 𝑢 → ( 𝑤 ∘ 𝑤 ) ⊆ ( 𝑢 ∘ 𝑢 ) )
68 67 ad2antll ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 ∘ 𝑢 ) ⊆ 𝑣 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑢 ) ) → ( 𝑤 ∘ 𝑤 ) ⊆ ( 𝑢 ∘ 𝑢 ) )
69 simpllr ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 ∘ 𝑢 ) ⊆ 𝑣 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑢 ) ) → ( 𝑢 ∘ 𝑢 ) ⊆ 𝑣 )
70 68 69 sstrd ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 ∘ 𝑢 ) ⊆ 𝑣 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑢 ) ) → ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 )
71 64 70 eqsstrd ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 ∘ 𝑢 ) ⊆ 𝑣 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑢 ) ) → ( 𝑤 ∘ ◡ 𝑤 ) ⊆ 𝑣 )
72 62 71 sstrd ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 ∘ 𝑢 ) ⊆ 𝑣 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑢 ) ) → ( ( 𝑤 “ { 𝑃 } ) × ( 𝑤 “ { 𝑃 } ) ) ⊆ 𝑣 )
73 72 ex ⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 ∘ 𝑢 ) ⊆ 𝑣 ) ∧ 𝑤 ∈ 𝑈 ) → ( ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑢 ) → ( ( 𝑤 “ { 𝑃 } ) × ( 𝑤 “ { 𝑃 } ) ) ⊆ 𝑣 ) )
74 73 reximdva ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 ∘ 𝑢 ) ⊆ 𝑣 ) → ( ∃ 𝑤 ∈ 𝑈 ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑢 ) → ∃ 𝑤 ∈ 𝑈 ( ( 𝑤 “ { 𝑃 } ) × ( 𝑤 “ { 𝑃 } ) ) ⊆ 𝑣 ) )
75 54 74 mpd ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑣 ∈ 𝑈 ) ∧ 𝑢 ∈ 𝑈 ) ∧ ( 𝑢 ∘ 𝑢 ) ⊆ 𝑣 ) → ∃ 𝑤 ∈ 𝑈 ( ( 𝑤 “ { 𝑃 } ) × ( 𝑤 “ { 𝑃 } ) ) ⊆ 𝑣 )
76 ustexhalf ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) → ∃ 𝑢 ∈ 𝑈 ( 𝑢 ∘ 𝑢 ) ⊆ 𝑣 )
77 76 3adant2 ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑣 ∈ 𝑈 ) → ∃ 𝑢 ∈ 𝑈 ( 𝑢 ∘ 𝑢 ) ⊆ 𝑣 )
78 75 77 r19.29a ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑣 ∈ 𝑈 ) → ∃ 𝑤 ∈ 𝑈 ( ( 𝑤 “ { 𝑃 } ) × ( 𝑤 “ { 𝑃 } ) ) ⊆ 𝑣 )
79 48 49 50 78 syl3anc ⊢ ( ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) → ∃ 𝑤 ∈ 𝑈 ( ( 𝑤 “ { 𝑃 } ) × ( 𝑤 “ { 𝑃 } ) ) ⊆ 𝑣 )
80 47 79 r19.29a ⊢ ( ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) → ∃ 𝑎 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑎 × 𝑎 ) ⊆ 𝑣 )
81 80 ralrimiva ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) → ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑎 × 𝑎 ) ⊆ 𝑣 )
82 iscfilu ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∈ ( CauFilu ‘ 𝑈 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) ) )
83 28 82 syl ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∈ ( CauFilu ‘ 𝑈 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) ) )
84 14 81 83 mpbir2and ⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∈ ( CauFilu ‘ 𝑈 ) )