Theorem neifg

Description: The neighborhood filter of a nonempty set is generated by its open supersets. See comments for opnfbas . (Contributed by Jeff Hankins, 3-Sep-2009)

	Ref	Expression
Hypothesis	neifg.1	⊢ 𝑋 = ∪ 𝐽
Assertion	neifg	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( 𝑋 filGen { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ) = ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		neifg.1	⊢ 𝑋 = ∪ 𝐽
2	1	opnfbas	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∈ ( fBas ‘ 𝑋 ) )
3		fgval	⊢ ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ) = { 𝑡 ∈ 𝒫 𝑋 ∣ ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∩ 𝒫 𝑡 ) ≠ ∅ } )
4	2 3	syl	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( 𝑋 filGen { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ) = { 𝑡 ∈ 𝒫 𝑋 ∣ ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∩ 𝒫 𝑡 ) ≠ ∅ } )
5		pweq	⊢ ( 𝑡 = 𝑢 → 𝒫 𝑡 = 𝒫 𝑢 )
6	5	ineq2d	⊢ ( 𝑡 = 𝑢 → ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∩ 𝒫 𝑡 ) = ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∩ 𝒫 𝑢 ) )
7	6	neeq1d	⊢ ( 𝑡 = 𝑢 → ( ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∩ 𝒫 𝑡 ) ≠ ∅ ↔ ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∩ 𝒫 𝑢 ) ≠ ∅ ) )
8	7	elrab	⊢ ( 𝑢 ∈ { 𝑡 ∈ 𝒫 𝑋 ∣ ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∩ 𝒫 𝑡 ) ≠ ∅ } ↔ ( 𝑢 ∈ 𝒫 𝑋 ∧ ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∩ 𝒫 𝑢 ) ≠ ∅ ) )
9		velpw	⊢ ( 𝑢 ∈ 𝒫 𝑋 ↔ 𝑢 ⊆ 𝑋 )
10	9	a1i	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( 𝑢 ∈ 𝒫 𝑋 ↔ 𝑢 ⊆ 𝑋 ) )
11		n0	⊢ ( ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∩ 𝒫 𝑢 ) ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∩ 𝒫 𝑢 ) )
12		elin	⊢ ( 𝑧 ∈ ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∩ 𝒫 𝑢 ) ↔ ( 𝑧 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∧ 𝑧 ∈ 𝒫 𝑢 ) )
13		sseq2	⊢ ( 𝑥 = 𝑧 → ( 𝑆 ⊆ 𝑥 ↔ 𝑆 ⊆ 𝑧 ) )
14	13	elrab	⊢ ( 𝑧 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ↔ ( 𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧 ) )
15		velpw	⊢ ( 𝑧 ∈ 𝒫 𝑢 ↔ 𝑧 ⊆ 𝑢 )
16	14 15	anbi12i	⊢ ( ( 𝑧 ∈ { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∧ 𝑧 ∈ 𝒫 𝑢 ) ↔ ( ( 𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧 ) ∧ 𝑧 ⊆ 𝑢 ) )
17	12 16	bitri	⊢ ( 𝑧 ∈ ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∩ 𝒫 𝑢 ) ↔ ( ( 𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧 ) ∧ 𝑧 ⊆ 𝑢 ) )
18	17	exbii	⊢ ( ∃ 𝑧 𝑧 ∈ ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∩ 𝒫 𝑢 ) ↔ ∃ 𝑧 ( ( 𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧 ) ∧ 𝑧 ⊆ 𝑢 ) )
19	11 18	bitri	⊢ ( ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∩ 𝒫 𝑢 ) ≠ ∅ ↔ ∃ 𝑧 ( ( 𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧 ) ∧ 𝑧 ⊆ 𝑢 ) )
20	19	a1i	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∩ 𝒫 𝑢 ) ≠ ∅ ↔ ∃ 𝑧 ( ( 𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧 ) ∧ 𝑧 ⊆ 𝑢 ) ) )
21	10 20	anbi12d	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( ( 𝑢 ∈ 𝒫 𝑋 ∧ ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∩ 𝒫 𝑢 ) ≠ ∅ ) ↔ ( 𝑢 ⊆ 𝑋 ∧ ∃ 𝑧 ( ( 𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧 ) ∧ 𝑧 ⊆ 𝑢 ) ) ) )
22		anass	⊢ ( ( ( 𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧 ) ∧ 𝑧 ⊆ 𝑢 ) ↔ ( 𝑧 ∈ 𝐽 ∧ ( 𝑆 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑢 ) ) )
23	22	exbii	⊢ ( ∃ 𝑧 ( ( 𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧 ) ∧ 𝑧 ⊆ 𝑢 ) ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐽 ∧ ( 𝑆 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑢 ) ) )
24		df-rex	⊢ ( ∃ 𝑧 ∈ 𝐽 ( 𝑆 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑢 ) ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐽 ∧ ( 𝑆 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑢 ) ) )
25	23 24	bitr4i	⊢ ( ∃ 𝑧 ( ( 𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧 ) ∧ 𝑧 ⊆ 𝑢 ) ↔ ∃ 𝑧 ∈ 𝐽 ( 𝑆 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑢 ) )
26	25	anbi2i	⊢ ( ( 𝑢 ⊆ 𝑋 ∧ ∃ 𝑧 ( ( 𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧 ) ∧ 𝑧 ⊆ 𝑢 ) ) ↔ ( 𝑢 ⊆ 𝑋 ∧ ∃ 𝑧 ∈ 𝐽 ( 𝑆 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑢 ) ) )
27	1	isnei	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑢 ⊆ 𝑋 ∧ ∃ 𝑧 ∈ 𝐽 ( 𝑆 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑢 ) ) ) )
28	27	3adant3	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑢 ⊆ 𝑋 ∧ ∃ 𝑧 ∈ 𝐽 ( 𝑆 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑢 ) ) ) )
29	26 28	bitr4id	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( ( 𝑢 ⊆ 𝑋 ∧ ∃ 𝑧 ( ( 𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧 ) ∧ 𝑧 ⊆ 𝑢 ) ) ↔ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
30	21 29	bitrd	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( ( 𝑢 ∈ 𝒫 𝑋 ∧ ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∩ 𝒫 𝑢 ) ≠ ∅ ) ↔ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
31	8 30	syl5bb	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( 𝑢 ∈ { 𝑡 ∈ 𝒫 𝑋 ∣ ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∩ 𝒫 𝑡 ) ≠ ∅ } ↔ 𝑢 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) )
32	31	eqrdv	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → { 𝑡 ∈ 𝒫 𝑋 ∣ ( { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ∩ 𝒫 𝑡 ) ≠ ∅ } = ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )
33	4 32	eqtrd	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( 𝑋 filGen { 𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥 } ) = ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )