MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  neipcfilu Structured version   Visualization version   GIF version

Theorem neipcfilu 22297
Description: In an uniform space, a neighboring filter is a Cauchy filter base. (Contributed by Thierry Arnoux, 24-Jan-2018.)
Hypotheses
Ref Expression
neipcfilu.x 𝑋 = (Base‘𝑊)
neipcfilu.j 𝐽 = (TopOpen‘𝑊)
neipcfilu.u 𝑈 = (UnifSt‘𝑊)
Assertion
Ref Expression
neipcfilu ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) → ((nei‘𝐽)‘{𝑃}) ∈ (CauFilu𝑈))

Proof of Theorem neipcfilu
Dummy variables 𝑣 𝑎 𝑤 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp2 1132 . . . . 5 ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) → 𝑊 ∈ TopSp)
2 neipcfilu.x . . . . . 6 𝑋 = (Base‘𝑊)
3 neipcfilu.j . . . . . 6 𝐽 = (TopOpen‘𝑊)
42, 3istps 20936 . . . . 5 (𝑊 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝑋))
51, 4sylib 208 . . . 4 ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) → 𝐽 ∈ (TopOn‘𝑋))
6 simp3 1133 . . . . 5 ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) → 𝑃𝑋)
76snssd 4481 . . . 4 ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) → {𝑃} ⊆ 𝑋)
8 snnzg 4447 . . . . 5 (𝑃𝑋 → {𝑃} ≠ ∅)
96, 8syl 17 . . . 4 ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) → {𝑃} ≠ ∅)
10 neifil 21881 . . . 4 ((𝐽 ∈ (TopOn‘𝑋) ∧ {𝑃} ⊆ 𝑋 ∧ {𝑃} ≠ ∅) → ((nei‘𝐽)‘{𝑃}) ∈ (Fil‘𝑋))
115, 7, 9, 10syl3anc 1477 . . 3 ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) → ((nei‘𝐽)‘{𝑃}) ∈ (Fil‘𝑋))
12 filfbas 21849 . . 3 (((nei‘𝐽)‘{𝑃}) ∈ (Fil‘𝑋) → ((nei‘𝐽)‘{𝑃}) ∈ (fBas‘𝑋))
1311, 12syl 17 . 2 ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) → ((nei‘𝐽)‘{𝑃}) ∈ (fBas‘𝑋))
14 eqid 2756 . . . . . . . . . 10 (𝑤 “ {𝑃}) = (𝑤 “ {𝑃})
15 imaeq1 5615 . . . . . . . . . . . 12 (𝑣 = 𝑤 → (𝑣 “ {𝑃}) = (𝑤 “ {𝑃}))
1615eqeq2d 2766 . . . . . . . . . . 11 (𝑣 = 𝑤 → ((𝑤 “ {𝑃}) = (𝑣 “ {𝑃}) ↔ (𝑤 “ {𝑃}) = (𝑤 “ {𝑃})))
1716rspcev 3445 . . . . . . . . . 10 ((𝑤𝑈 ∧ (𝑤 “ {𝑃}) = (𝑤 “ {𝑃})) → ∃𝑣𝑈 (𝑤 “ {𝑃}) = (𝑣 “ {𝑃}))
1814, 17mpan2 709 . . . . . . . . 9 (𝑤𝑈 → ∃𝑣𝑈 (𝑤 “ {𝑃}) = (𝑣 “ {𝑃}))
19 vex 3339 . . . . . . . . . . 11 𝑤 ∈ V
2019imaex 7265 . . . . . . . . . 10 (𝑤 “ {𝑃}) ∈ V
21 eqid 2756 . . . . . . . . . . 11 (𝑣𝑈 ↦ (𝑣 “ {𝑃})) = (𝑣𝑈 ↦ (𝑣 “ {𝑃}))
2221elrnmpt 5523 . . . . . . . . . 10 ((𝑤 “ {𝑃}) ∈ V → ((𝑤 “ {𝑃}) ∈ ran (𝑣𝑈 ↦ (𝑣 “ {𝑃})) ↔ ∃𝑣𝑈 (𝑤 “ {𝑃}) = (𝑣 “ {𝑃})))
2320, 22ax-mp 5 . . . . . . . . 9 ((𝑤 “ {𝑃}) ∈ ran (𝑣𝑈 ↦ (𝑣 “ {𝑃})) ↔ ∃𝑣𝑈 (𝑤 “ {𝑃}) = (𝑣 “ {𝑃}))
2418, 23sylibr 224 . . . . . . . 8 (𝑤𝑈 → (𝑤 “ {𝑃}) ∈ ran (𝑣𝑈 ↦ (𝑣 “ {𝑃})))
2524ad2antlr 765 . . . . . . 7 (((((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) ∧ 𝑣𝑈) ∧ 𝑤𝑈) ∧ ((𝑤 “ {𝑃}) × (𝑤 “ {𝑃})) ⊆ 𝑣) → (𝑤 “ {𝑃}) ∈ ran (𝑣𝑈 ↦ (𝑣 “ {𝑃})))
26 neipcfilu.u . . . . . . . . . . . . 13 𝑈 = (UnifSt‘𝑊)
272, 26, 3isusp 22262 . . . . . . . . . . . 12 (𝑊 ∈ UnifSp ↔ (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐽 = (unifTop‘𝑈)))
2827simplbi 478 . . . . . . . . . . 11 (𝑊 ∈ UnifSp → 𝑈 ∈ (UnifOn‘𝑋))
29283ad2ant1 1128 . . . . . . . . . 10 ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) → 𝑈 ∈ (UnifOn‘𝑋))
30 eqid 2756 . . . . . . . . . . 11 (unifTop‘𝑈) = (unifTop‘𝑈)
3130utopsnneip 22249 . . . . . . . . . 10 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃𝑋) → ((nei‘(unifTop‘𝑈))‘{𝑃}) = ran (𝑣𝑈 ↦ (𝑣 “ {𝑃})))
3229, 6, 31syl2anc 696 . . . . . . . . 9 ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) → ((nei‘(unifTop‘𝑈))‘{𝑃}) = ran (𝑣𝑈 ↦ (𝑣 “ {𝑃})))
3332eleq2d 2821 . . . . . . . 8 ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) → ((𝑤 “ {𝑃}) ∈ ((nei‘(unifTop‘𝑈))‘{𝑃}) ↔ (𝑤 “ {𝑃}) ∈ ran (𝑣𝑈 ↦ (𝑣 “ {𝑃}))))
3433ad3antrrr 768 . . . . . . 7 (((((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) ∧ 𝑣𝑈) ∧ 𝑤𝑈) ∧ ((𝑤 “ {𝑃}) × (𝑤 “ {𝑃})) ⊆ 𝑣) → ((𝑤 “ {𝑃}) ∈ ((nei‘(unifTop‘𝑈))‘{𝑃}) ↔ (𝑤 “ {𝑃}) ∈ ran (𝑣𝑈 ↦ (𝑣 “ {𝑃}))))
3525, 34mpbird 247 . . . . . 6 (((((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) ∧ 𝑣𝑈) ∧ 𝑤𝑈) ∧ ((𝑤 “ {𝑃}) × (𝑤 “ {𝑃})) ⊆ 𝑣) → (𝑤 “ {𝑃}) ∈ ((nei‘(unifTop‘𝑈))‘{𝑃}))
36 simpl1 1228 . . . . . . . . . 10 (((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) ∧ (𝑣𝑈𝑤𝑈 ∧ ((𝑤 “ {𝑃}) × (𝑤 “ {𝑃})) ⊆ 𝑣)) → 𝑊 ∈ UnifSp)
37363anassrs 1454 . . . . . . . . 9 (((((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) ∧ 𝑣𝑈) ∧ 𝑤𝑈) ∧ ((𝑤 “ {𝑃}) × (𝑤 “ {𝑃})) ⊆ 𝑣) → 𝑊 ∈ UnifSp)
3827simprbi 483 . . . . . . . . 9 (𝑊 ∈ UnifSp → 𝐽 = (unifTop‘𝑈))
3937, 38syl 17 . . . . . . . 8 (((((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) ∧ 𝑣𝑈) ∧ 𝑤𝑈) ∧ ((𝑤 “ {𝑃}) × (𝑤 “ {𝑃})) ⊆ 𝑣) → 𝐽 = (unifTop‘𝑈))
4039fveq2d 6352 . . . . . . 7 (((((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) ∧ 𝑣𝑈) ∧ 𝑤𝑈) ∧ ((𝑤 “ {𝑃}) × (𝑤 “ {𝑃})) ⊆ 𝑣) → (nei‘𝐽) = (nei‘(unifTop‘𝑈)))
4140fveq1d 6350 . . . . . 6 (((((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) ∧ 𝑣𝑈) ∧ 𝑤𝑈) ∧ ((𝑤 “ {𝑃}) × (𝑤 “ {𝑃})) ⊆ 𝑣) → ((nei‘𝐽)‘{𝑃}) = ((nei‘(unifTop‘𝑈))‘{𝑃}))
4235, 41eleqtrrd 2838 . . . . 5 (((((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) ∧ 𝑣𝑈) ∧ 𝑤𝑈) ∧ ((𝑤 “ {𝑃}) × (𝑤 “ {𝑃})) ⊆ 𝑣) → (𝑤 “ {𝑃}) ∈ ((nei‘𝐽)‘{𝑃}))
43 simpr 479 . . . . 5 (((((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) ∧ 𝑣𝑈) ∧ 𝑤𝑈) ∧ ((𝑤 “ {𝑃}) × (𝑤 “ {𝑃})) ⊆ 𝑣) → ((𝑤 “ {𝑃}) × (𝑤 “ {𝑃})) ⊆ 𝑣)
44 id 22 . . . . . . . 8 (𝑎 = (𝑤 “ {𝑃}) → 𝑎 = (𝑤 “ {𝑃}))
4544sqxpeqd 5294 . . . . . . 7 (𝑎 = (𝑤 “ {𝑃}) → (𝑎 × 𝑎) = ((𝑤 “ {𝑃}) × (𝑤 “ {𝑃})))
4645sseq1d 3769 . . . . . 6 (𝑎 = (𝑤 “ {𝑃}) → ((𝑎 × 𝑎) ⊆ 𝑣 ↔ ((𝑤 “ {𝑃}) × (𝑤 “ {𝑃})) ⊆ 𝑣))
4746rspcev 3445 . . . . 5 (((𝑤 “ {𝑃}) ∈ ((nei‘𝐽)‘{𝑃}) ∧ ((𝑤 “ {𝑃}) × (𝑤 “ {𝑃})) ⊆ 𝑣) → ∃𝑎 ∈ ((nei‘𝐽)‘{𝑃})(𝑎 × 𝑎) ⊆ 𝑣)
4842, 43, 47syl2anc 696 . . . 4 (((((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) ∧ 𝑣𝑈) ∧ 𝑤𝑈) ∧ ((𝑤 “ {𝑃}) × (𝑤 “ {𝑃})) ⊆ 𝑣) → ∃𝑎 ∈ ((nei‘𝐽)‘{𝑃})(𝑎 × 𝑎) ⊆ 𝑣)
4929adantr 472 . . . . 5 (((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) ∧ 𝑣𝑈) → 𝑈 ∈ (UnifOn‘𝑋))
506adantr 472 . . . . 5 (((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) ∧ 𝑣𝑈) → 𝑃𝑋)
51 simpr 479 . . . . 5 (((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) ∧ 𝑣𝑈) → 𝑣𝑈)
52 simpll1 1255 . . . . . . . 8 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃𝑋𝑣𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑣) → 𝑈 ∈ (UnifOn‘𝑋))
53 simplr 809 . . . . . . . 8 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃𝑋𝑣𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑣) → 𝑢𝑈)
54 ustexsym 22216 . . . . . . . 8 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑢𝑈) → ∃𝑤𝑈 (𝑤 = 𝑤𝑤𝑢))
5552, 53, 54syl2anc 696 . . . . . . 7 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃𝑋𝑣𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑣) → ∃𝑤𝑈 (𝑤 = 𝑤𝑤𝑢))
5652ad2antrr 764 . . . . . . . . . . . 12 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃𝑋𝑣𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑣) ∧ 𝑤𝑈) ∧ (𝑤 = 𝑤𝑤𝑢)) → 𝑈 ∈ (UnifOn‘𝑋))
57 simplr 809 . . . . . . . . . . . 12 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃𝑋𝑣𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑣) ∧ 𝑤𝑈) ∧ (𝑤 = 𝑤𝑤𝑢)) → 𝑤𝑈)
58 ustssxp 22205 . . . . . . . . . . . 12 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤𝑈) → 𝑤 ⊆ (𝑋 × 𝑋))
5956, 57, 58syl2anc 696 . . . . . . . . . . 11 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃𝑋𝑣𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑣) ∧ 𝑤𝑈) ∧ (𝑤 = 𝑤𝑤𝑢)) → 𝑤 ⊆ (𝑋 × 𝑋))
60 simpll2 1257 . . . . . . . . . . . 12 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃𝑋𝑣𝑈) ∧ 𝑢𝑈) ∧ ((𝑢𝑢) ⊆ 𝑣𝑤𝑈 ∧ (𝑤 = 𝑤𝑤𝑢))) → 𝑃𝑋)
61603anassrs 1454 . . . . . . . . . . 11 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃𝑋𝑣𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑣) ∧ 𝑤𝑈) ∧ (𝑤 = 𝑤𝑤𝑢)) → 𝑃𝑋)
62 ustneism 22224 . . . . . . . . . . 11 ((𝑤 ⊆ (𝑋 × 𝑋) ∧ 𝑃𝑋) → ((𝑤 “ {𝑃}) × (𝑤 “ {𝑃})) ⊆ (𝑤𝑤))
6359, 61, 62syl2anc 696 . . . . . . . . . 10 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃𝑋𝑣𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑣) ∧ 𝑤𝑈) ∧ (𝑤 = 𝑤𝑤𝑢)) → ((𝑤 “ {𝑃}) × (𝑤 “ {𝑃})) ⊆ (𝑤𝑤))
64 simprl 811 . . . . . . . . . . . 12 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃𝑋𝑣𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑣) ∧ 𝑤𝑈) ∧ (𝑤 = 𝑤𝑤𝑢)) → 𝑤 = 𝑤)
6564coeq2d 5436 . . . . . . . . . . 11 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃𝑋𝑣𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑣) ∧ 𝑤𝑈) ∧ (𝑤 = 𝑤𝑤𝑢)) → (𝑤𝑤) = (𝑤𝑤))
66 coss1 5429 . . . . . . . . . . . . . 14 (𝑤𝑢 → (𝑤𝑤) ⊆ (𝑢𝑤))
67 coss2 5430 . . . . . . . . . . . . . 14 (𝑤𝑢 → (𝑢𝑤) ⊆ (𝑢𝑢))
6866, 67sstrd 3750 . . . . . . . . . . . . 13 (𝑤𝑢 → (𝑤𝑤) ⊆ (𝑢𝑢))
6968ad2antll 767 . . . . . . . . . . . 12 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃𝑋𝑣𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑣) ∧ 𝑤𝑈) ∧ (𝑤 = 𝑤𝑤𝑢)) → (𝑤𝑤) ⊆ (𝑢𝑢))
70 simpllr 817 . . . . . . . . . . . 12 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃𝑋𝑣𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑣) ∧ 𝑤𝑈) ∧ (𝑤 = 𝑤𝑤𝑢)) → (𝑢𝑢) ⊆ 𝑣)
7169, 70sstrd 3750 . . . . . . . . . . 11 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃𝑋𝑣𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑣) ∧ 𝑤𝑈) ∧ (𝑤 = 𝑤𝑤𝑢)) → (𝑤𝑤) ⊆ 𝑣)
7265, 71eqsstrd 3776 . . . . . . . . . 10 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃𝑋𝑣𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑣) ∧ 𝑤𝑈) ∧ (𝑤 = 𝑤𝑤𝑢)) → (𝑤𝑤) ⊆ 𝑣)
7363, 72sstrd 3750 . . . . . . . . 9 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃𝑋𝑣𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑣) ∧ 𝑤𝑈) ∧ (𝑤 = 𝑤𝑤𝑢)) → ((𝑤 “ {𝑃}) × (𝑤 “ {𝑃})) ⊆ 𝑣)
7473ex 449 . . . . . . . 8 (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃𝑋𝑣𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑣) ∧ 𝑤𝑈) → ((𝑤 = 𝑤𝑤𝑢) → ((𝑤 “ {𝑃}) × (𝑤 “ {𝑃})) ⊆ 𝑣))
7574reximdva 3151 . . . . . . 7 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃𝑋𝑣𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑣) → (∃𝑤𝑈 (𝑤 = 𝑤𝑤𝑢) → ∃𝑤𝑈 ((𝑤 “ {𝑃}) × (𝑤 “ {𝑃})) ⊆ 𝑣))
7655, 75mpd 15 . . . . . 6 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃𝑋𝑣𝑈) ∧ 𝑢𝑈) ∧ (𝑢𝑢) ⊆ 𝑣) → ∃𝑤𝑈 ((𝑤 “ {𝑃}) × (𝑤 “ {𝑃})) ⊆ 𝑣)
77 ustexhalf 22211 . . . . . . 7 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑣𝑈) → ∃𝑢𝑈 (𝑢𝑢) ⊆ 𝑣)
78773adant2 1126 . . . . . 6 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃𝑋𝑣𝑈) → ∃𝑢𝑈 (𝑢𝑢) ⊆ 𝑣)
7976, 78r19.29a 3212 . . . . 5 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃𝑋𝑣𝑈) → ∃𝑤𝑈 ((𝑤 “ {𝑃}) × (𝑤 “ {𝑃})) ⊆ 𝑣)
8049, 50, 51, 79syl3anc 1477 . . . 4 (((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) ∧ 𝑣𝑈) → ∃𝑤𝑈 ((𝑤 “ {𝑃}) × (𝑤 “ {𝑃})) ⊆ 𝑣)
8148, 80r19.29a 3212 . . 3 (((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) ∧ 𝑣𝑈) → ∃𝑎 ∈ ((nei‘𝐽)‘{𝑃})(𝑎 × 𝑎) ⊆ 𝑣)
8281ralrimiva 3100 . 2 ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) → ∀𝑣𝑈𝑎 ∈ ((nei‘𝐽)‘{𝑃})(𝑎 × 𝑎) ⊆ 𝑣)
83 iscfilu 22289 . . 3 (𝑈 ∈ (UnifOn‘𝑋) → (((nei‘𝐽)‘{𝑃}) ∈ (CauFilu𝑈) ↔ (((nei‘𝐽)‘{𝑃}) ∈ (fBas‘𝑋) ∧ ∀𝑣𝑈𝑎 ∈ ((nei‘𝐽)‘{𝑃})(𝑎 × 𝑎) ⊆ 𝑣)))
8429, 83syl 17 . 2 ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) → (((nei‘𝐽)‘{𝑃}) ∈ (CauFilu𝑈) ↔ (((nei‘𝐽)‘{𝑃}) ∈ (fBas‘𝑋) ∧ ∀𝑣𝑈𝑎 ∈ ((nei‘𝐽)‘{𝑃})(𝑎 × 𝑎) ⊆ 𝑣)))
8513, 82, 84mpbir2and 995 1 ((𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃𝑋) → ((nei‘𝐽)‘{𝑃}) ∈ (CauFilu𝑈))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1628  wcel 2135  wne 2928  wral 3046  wrex 3047  Vcvv 3336  wss 3711  c0 4054  {csn 4317  cmpt 4877   × cxp 5260  ccnv 5261  ran crn 5263  cima 5265  ccom 5266  cfv 6045  Basecbs 16055  TopOpenctopn 16280  fBascfbas 19932  TopOnctopon 20913  TopSpctps 20934  neicnei 21099  Filcfil 21846  UnifOncust 22200  unifTopcutop 22231  UnifStcuss 22254  UnifSpcusp 22255  CauFiluccfilu 22287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-rep 4919  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-nel 3032  df-ral 3051  df-rex 3052  df-reu 3053  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-pss 3727  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4585  df-int 4624  df-iun 4670  df-br 4801  df-opab 4861  df-mpt 4878  df-tr 4901  df-id 5170  df-eprel 5175  df-po 5183  df-so 5184  df-fr 5221  df-we 5223  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-pred 5837  df-ord 5883  df-on 5884  df-lim 5885  df-suc 5886  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-ov 6812  df-oprab 6813  df-mpt2 6814  df-om 7227  df-wrecs 7572  df-recs 7633  df-rdg 7671  df-1o 7725  df-oadd 7729  df-er 7907  df-en 8118  df-fin 8121  df-fi 8478  df-fbas 19941  df-top 20897  df-topon 20914  df-topsp 20935  df-nei 21100  df-fil 21847  df-ust 22201  df-utop 22232  df-usp 22258  df-cfilu 22288
This theorem is referenced by:  ucnextcn  22305
  Copyright terms: Public domain W3C validator