This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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