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 ‘ 𝐽 ) ‘ { 𝑃 } ) ∈ ( CauFil_u ‘ 𝑈 ) )

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 ‘ 𝐽 ) ‘ { 𝑃 } ) ∈ ( CauFil_u ‘ 𝑈 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) ) )
82	27 81	syl	⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∈ ( CauFil_u ‘ 𝑈 ) ↔ ( ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) ) )
83	13 80 82	mpbir2and	⊢ ( ( 𝑊 ∈ UnifSp ∧ 𝑊 ∈ TopSp ∧ 𝑃 ∈ 𝑋 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ∈ ( CauFil_u ‘ 𝑈 ) )

Metamath Proof Explorer

Theorem neipcfilu

Proof