Theorem neifg 36767

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

Hypothesis

Ref	Expression
neifg.1	⊢ 𝑋 = ∪ 𝐽

Assertion

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

Distinct variable groups:   𝑥,𝐽   𝑥,𝑆   𝑥,𝑋

Proof of Theorem neifg

Dummy variables 𝑢 𝑡 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		neifg.1	. . . 4 ⊢ 𝑋 = ∪ 𝐽
2	1	opnfbas 23964	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∈ (fBas‘𝑋))
3		fgval 23992	. . 3 ⊢ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∈ (fBas‘𝑋) → (𝑋filGen{𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}) = {𝑡 ∈ 𝒫 𝑋 ∣ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑡) ≠ ∅})
4	2, 3	syl 18	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → (𝑋filGen{𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}) = {𝑡 ∈ 𝒫 𝑋 ∣ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑡) ≠ ∅})
5		pweq 4578	. . . . . . 7 ⊢ (𝑡 = 𝑢 → 𝒫 𝑡 = 𝒫 𝑢)
6	5	ineq2d 4181	. . . . . 6 ⊢ (𝑡 = 𝑢 → ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑡) = ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑢))
7	6	neeq1d 3023	. . . . 5 ⊢ (𝑡 = 𝑢 → (({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑡) ≠ ∅ ↔ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑢) ≠ ∅))
8	7	elrab 3659	. . . 4 ⊢ (𝑢 ∈ {𝑡 ∈ 𝒫 𝑋 ∣ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑡) ≠ ∅} ↔ (𝑢 ∈ 𝒫 𝑋 ∧ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑢) ≠ ∅))
9		velpw 4569	. . . . . . 7 ⊢ (𝑢 ∈ 𝒫 𝑋 ↔ 𝑢 ⊆ 𝑋)
10	9	a1i 11	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → (𝑢 ∈ 𝒫 𝑋 ↔ 𝑢 ⊆ 𝑋))
11		n0 4314	. . . . . . . 8 ⊢ (({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑢) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑢))
12		elin 3929	. . . . . . . . . 10 ⊢ (𝑧 ∈ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑢) ↔ (𝑧 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∧ 𝑧 ∈ 𝒫 𝑢))
13		sseq2 3971	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (𝑆 ⊆ 𝑥 ↔ 𝑆 ⊆ 𝑧))
14	13	elrab 3659	. . . . . . . . . . 11 ⊢ (𝑧 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ↔ (𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧))
15		velpw 4569	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝒫 𝑢 ↔ 𝑧 ⊆ 𝑢)
16	14, 15	anbi12i 639	. . . . . . . . . 10 ⊢ ((𝑧 ∈ {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∧ 𝑧 ∈ 𝒫 𝑢) ↔ ((𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧) ∧ 𝑧 ⊆ 𝑢))
17	12, 16	bitri 278	. . . . . . . . 9 ⊢ (𝑧 ∈ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑢) ↔ ((𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧) ∧ 𝑧 ⊆ 𝑢))
18	17	exbii 1875	. . . . . . . 8 ⊢ (∃𝑧 𝑧 ∈ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑢) ↔ ∃𝑧((𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧) ∧ 𝑧 ⊆ 𝑢))
19	11, 18	bitri 278	. . . . . . 7 ⊢ (({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑢) ≠ ∅ ↔ ∃𝑧((𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧) ∧ 𝑧 ⊆ 𝑢))
20	19	a1i 11	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → (({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑢) ≠ ∅ ↔ ∃𝑧((𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧) ∧ 𝑧 ⊆ 𝑢)))
21	10, 20	anbi12d 643	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → ((𝑢 ∈ 𝒫 𝑋 ∧ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑢) ≠ ∅) ↔ (𝑢 ⊆ 𝑋 ∧ ∃𝑧((𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧) ∧ 𝑧 ⊆ 𝑢))))
22		anass 473	. . . . . . . . 9 ⊢ (((𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧) ∧ 𝑧 ⊆ 𝑢) ↔ (𝑧 ∈ 𝐽 ∧ (𝑆 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑢)))
23	22	exbii 1875	. . . . . . . 8 ⊢ (∃𝑧((𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧) ∧ 𝑧 ⊆ 𝑢) ↔ ∃𝑧(𝑧 ∈ 𝐽 ∧ (𝑆 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑢)))
24		df-rex 3096	. . . . . . . 8 ⊢ (∃𝑧 ∈ 𝐽 (𝑆 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑢) ↔ ∃𝑧(𝑧 ∈ 𝐽 ∧ (𝑆 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑢)))
25	23, 24	bitr4i 281	. . . . . . 7 ⊢ (∃𝑧((𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧) ∧ 𝑧 ⊆ 𝑢) ↔ ∃𝑧 ∈ 𝐽 (𝑆 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑢))
26	25	anbi2i 634	. . . . . 6 ⊢ ((𝑢 ⊆ 𝑋 ∧ ∃𝑧((𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧) ∧ 𝑧 ⊆ 𝑢)) ↔ (𝑢 ⊆ 𝑋 ∧ ∃𝑧 ∈ 𝐽 (𝑆 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑢)))
27	1	isnei 23225	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑢 ∈ ((nei‘𝐽)‘𝑆) ↔ (𝑢 ⊆ 𝑋 ∧ ∃𝑧 ∈ 𝐽 (𝑆 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑢))))
28	27	3adant3 1148	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → (𝑢 ∈ ((nei‘𝐽)‘𝑆) ↔ (𝑢 ⊆ 𝑋 ∧ ∃𝑧 ∈ 𝐽 (𝑆 ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑢))))
29	26, 28	bitr4id 293	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → ((𝑢 ⊆ 𝑋 ∧ ∃𝑧((𝑧 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑧) ∧ 𝑧 ⊆ 𝑢)) ↔ 𝑢 ∈ ((nei‘𝐽)‘𝑆)))
30	21, 29	bitrd 282	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → ((𝑢 ∈ 𝒫 𝑋 ∧ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑢) ≠ ∅) ↔ 𝑢 ∈ ((nei‘𝐽)‘𝑆)))
31	8, 30	bitrid 286	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → (𝑢 ∈ {𝑡 ∈ 𝒫 𝑋 ∣ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑡) ≠ ∅} ↔ 𝑢 ∈ ((nei‘𝐽)‘𝑆)))
32	31	eqrdv 2767	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → {𝑡 ∈ 𝒫 𝑋 ∣ ({𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∩ 𝒫 𝑡) ≠ ∅} = ((nei‘𝐽)‘𝑆))
33	4, 32	eqtrd 2804	1 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → (𝑋filGen{𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥}) = ((nei‘𝐽)‘𝑆))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1567  ∃wex 1806   ∈ wcel 2149   ≠ wne 2964  ∃wrex 3095  {crab 3423   ∩ cin 3912   ⊆ wss 3913  ∅c0 4294  𝒫 cpw 4564  ∪ cuni 4873  ‘cfv 6533  (class class class)co 7408  fBascfbas 21475  filGencfg 21476  Topctop 23015  neicnei 23219

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5239  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7411  df-oprab 7412  df-mpo 7413  df-fbas 21484  df-fg 21485  df-top 23016  df-nei 23220

This theorem is referenced by: (None)