Theorem neibastop2 31526

Description: In the topology generated by a neighborhood base, a set is a neighborhood of a point iff it contains a subset in the base. (Contributed by Jeff Hankins, 9-Sep-2009.) (Proof shortened by Mario Carneiro, 11-Sep-2015.)

Hypotheses

Ref	Expression
neibastop1.1	⊢ (𝜑 → 𝑋 ∈ 𝑉)
neibastop1.2	⊢ (𝜑 → 𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
neibastop1.3	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥) ∧ 𝑤 ∈ (𝐹‘𝑥))) → ((𝐹‘𝑥) ∩ 𝒫 (𝑣 ∩ 𝑤)) ≠ ∅)
neibastop1.4	⊢ 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅}
neibastop1.5	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → 𝑥 ∈ 𝑣)
neibastop1.6	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)

Assertion

Ref	Expression
neibastop2	⊢ ((𝜑 ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 ⊆ 𝑋 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))

Distinct variable groups:   𝑣,𝑡,𝑦,𝑥   𝑣,𝐽   𝑥,𝑦,𝐽   𝑡,𝑜,𝑣,𝑤,𝑥,𝑦,𝑃   𝑜,𝑁,𝑡,𝑣,𝑤,𝑥,𝑦   𝑜,𝐹,𝑡,𝑣,𝑤,𝑥,𝑦   𝜑,𝑜,𝑡,𝑣,𝑤,𝑥,𝑦   𝑜,𝑋,𝑡,𝑣,𝑤,𝑥,𝑦

Allowed substitution hints:   𝐽(𝑤,𝑡,𝑜)   𝑉(𝑥,𝑦,𝑤,𝑣,𝑡,𝑜)

Proof of Theorem neibastop2

Dummy variables 𝑓 𝑛 𝑧 𝑠 𝑢 𝑎 𝑏 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		neibastop1.1	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
2		neibastop1.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
3		neibastop1.3	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥) ∧ 𝑤 ∈ (𝐹‘𝑥))) → ((𝐹‘𝑥) ∩ 𝒫 (𝑣 ∩ 𝑤)) ≠ ∅)
4		neibastop1.4	. . . . . . . . 9 ⊢ 𝐽 = {𝑜 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅}
5	1, 2, 3, 4	neibastop1 31524	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
6		topontop 20541	. . . . . . . 8 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
7	5, 6	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐽 ∈ Top)
8	7	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑋) → 𝐽 ∈ Top)
9		eqid 2610	. . . . . . 7 ⊢ ∪ 𝐽 = ∪ 𝐽
10	9	neii1 20720	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑁 ⊆ ∪ 𝐽)
11	8, 10	sylan 487	. . . . 5 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑁 ⊆ ∪ 𝐽)
12		toponuni 20542	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
13	5, 12	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
14	13	ad2antrr 758	. . . . 5 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑋 = ∪ 𝐽)
15	11, 14	sseqtr4d 3605	. . . 4 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑁 ⊆ 𝑋)
16		neii2 20722	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ∃𝑦 ∈ 𝐽 ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))
17	8, 16	sylan 487	. . . . 5 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ∃𝑦 ∈ 𝐽 ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))
18		pweq 4111	. . . . . . . . . . 11 ⊢ (𝑜 = 𝑦 → 𝒫 𝑜 = 𝒫 𝑦)
19	18	ineq2d 3776	. . . . . . . . . 10 ⊢ (𝑜 = 𝑦 → ((𝐹‘𝑥) ∩ 𝒫 𝑜) = ((𝐹‘𝑥) ∩ 𝒫 𝑦))
20	19	neeq1d 2841	. . . . . . . . 9 ⊢ (𝑜 = 𝑦 → (((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅))
21	20	raleqbi1dv 3123	. . . . . . . 8 ⊢ (𝑜 = 𝑦 → (∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅))
22	21, 4	elrab2 3333	. . . . . . 7 ⊢ (𝑦 ∈ 𝐽 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅))
23		simprrr 801	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → 𝑦 ⊆ 𝑁)
24		sspwb 4844	. . . . . . . . . . . . 13 ⊢ (𝑦 ⊆ 𝑁 ↔ 𝒫 𝑦 ⊆ 𝒫 𝑁)
25	23, 24	sylib 207	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → 𝒫 𝑦 ⊆ 𝒫 𝑁)
26		sslin 3801	. . . . . . . . . . . 12 ⊢ (𝒫 𝑦 ⊆ 𝒫 𝑁 → ((𝐹‘𝑃) ∩ 𝒫 𝑦) ⊆ ((𝐹‘𝑃) ∩ 𝒫 𝑁))
27	25, 26	syl 17	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → ((𝐹‘𝑃) ∩ 𝒫 𝑦) ⊆ ((𝐹‘𝑃) ∩ 𝒫 𝑁))
28		simprrl 800	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → {𝑃} ⊆ 𝑦)
29		snssg 4268	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ 𝑋 → (𝑃 ∈ 𝑦 ↔ {𝑃} ⊆ 𝑦))
30	29	ad3antlr 763	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → (𝑃 ∈ 𝑦 ↔ {𝑃} ⊆ 𝑦))
31	28, 30	mpbird 246	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → 𝑃 ∈ 𝑦)
32		fveq2 6103	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑃 → (𝐹‘𝑥) = (𝐹‘𝑃))
33	32	ineq1d 3775	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑃 → ((𝐹‘𝑥) ∩ 𝒫 𝑦) = ((𝐹‘𝑃) ∩ 𝒫 𝑦))
34	33	neeq1d 2841	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑃 → (((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ↔ ((𝐹‘𝑃) ∩ 𝒫 𝑦) ≠ ∅))
35	34	rspcv 3278	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ 𝑦 → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹‘𝑃) ∩ 𝒫 𝑦) ≠ ∅))
36	31, 35	syl 17	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹‘𝑃) ∩ 𝒫 𝑦) ≠ ∅))
37		ssn0 3928	. . . . . . . . . . 11 ⊢ ((((𝐹‘𝑃) ∩ 𝒫 𝑦) ⊆ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑦) ≠ ∅) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)
38	27, 36, 37	syl6an 566	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅))
39	38	expr 641	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ 𝑦 ∈ 𝒫 𝑋) → (({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁) → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
40	39	com23 84	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ 𝑦 ∈ 𝒫 𝑋) → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → (({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
41	40	expimpd 627	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ((𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅) → (({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
42	22, 41	syl5bi 231	. . . . . 6 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → (𝑦 ∈ 𝐽 → (({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
43	42	rexlimdv 3012	. . . . 5 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → (∃𝑦 ∈ 𝐽 ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅))
44	17, 43	mpd 15	. . . 4 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)
45	15, 44	jca 553	. . 3 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → (𝑁 ⊆ 𝑋 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅))
46	45	ex 449	. 2 ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) → (𝑁 ⊆ 𝑋 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
47		n0 3890	. . . 4 ⊢ (((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅ ↔ ∃𝑠 𝑠 ∈ ((𝐹‘𝑃) ∩ 𝒫 𝑁))
48		elin 3758	. . . . . 6 ⊢ (𝑠 ∈ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ↔ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))
49		simprl 790	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑁 ⊆ 𝑋)
50	13	ad2antrr 758	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑋 = ∪ 𝐽)
51	49, 50	sseqtrd 3604	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑁 ⊆ ∪ 𝐽)
52	1	ad2antrr 758	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑋 ∈ 𝑉)
53	2	ad2antrr 758	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
54		simpll 786	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝜑)
55	54, 3	sylan 487	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥) ∧ 𝑤 ∈ (𝐹‘𝑥))) → ((𝐹‘𝑥) ∩ 𝒫 (𝑣 ∩ 𝑤)) ≠ ∅)
56		neibastop1.5	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → 𝑥 ∈ 𝑣)
57	54, 56	sylan 487	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → 𝑥 ∈ 𝑣)
58		neibastop1.6	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)
59	54, 58	sylan 487	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)
60		simplr 788	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑃 ∈ 𝑋)
61		simprrl 800	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑠 ∈ (𝐹‘𝑃))
62		simprrr 801	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑠 ∈ 𝒫 𝑁)
63	62	elpwid 4118	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑠 ⊆ 𝑁)
64		fveq2 6103	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑥 → (𝐹‘𝑛) = (𝐹‘𝑥))
65	64	ineq1d 3775	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑥 → ((𝐹‘𝑛) ∩ 𝒫 𝑏) = ((𝐹‘𝑥) ∩ 𝒫 𝑏))
66	65	cbviunv 4495	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏) = ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑏)
67		pweq 4111	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑧 → 𝒫 𝑏 = 𝒫 𝑧)
68	67	ineq2d 3776	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑧 → ((𝐹‘𝑥) ∩ 𝒫 𝑏) = ((𝐹‘𝑥) ∩ 𝒫 𝑧))
69	68	iuneq2d 4483	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑧 → ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑏) = ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
70	66, 69	syl5eq 2656	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑧 → ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏) = ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
71	70	cbviunv 4495	. . . . . . . . . . . 12 ⊢ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏) = ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)
72	71	mpteq2i 4669	. . . . . . . . . . 11 ⊢ (𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)) = (𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
73		rdgeq1 7394	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)) = (𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)) → rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) = rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑠}))
74	72, 73	ax-mp 5	. . . . . . . . . 10 ⊢ rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) = rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑠})
75	74	reseq1i 5313	. . . . . . . . 9 ⊢ (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω) = (rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑠}) ↾ ω)
76		pweq 4111	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑓 → 𝒫 𝑔 = 𝒫 𝑓)
77	76	ineq2d 3776	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑓 → ((𝐹‘𝑤) ∩ 𝒫 𝑔) = ((𝐹‘𝑤) ∩ 𝒫 𝑓))
78	77	neeq1d 2841	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑓 → (((𝐹‘𝑤) ∩ 𝒫 𝑔) ≠ ∅ ↔ ((𝐹‘𝑤) ∩ 𝒫 𝑓) ≠ ∅))
79	78	cbvrexv 3148	. . . . . . . . . . 11 ⊢ (∃𝑔 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑤) ∩ 𝒫 𝑔) ≠ ∅ ↔ ∃𝑓 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑤) ∩ 𝒫 𝑓) ≠ ∅)
80		fveq2 6103	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑦 → (𝐹‘𝑤) = (𝐹‘𝑦))
81	80	ineq1d 3775	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑦 → ((𝐹‘𝑤) ∩ 𝒫 𝑓) = ((𝐹‘𝑦) ∩ 𝒫 𝑓))
82	81	neeq1d 2841	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑦 → (((𝐹‘𝑤) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅))
83	82	rexbidv 3034	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑦 → (∃𝑓 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑤) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑓 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅))
84	79, 83	syl5bb 271	. . . . . . . . . 10 ⊢ (𝑤 = 𝑦 → (∃𝑔 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑤) ∩ 𝒫 𝑔) ≠ ∅ ↔ ∃𝑓 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅))
85	84	cbvrabv 3172	. . . . . . . . 9 ⊢ {𝑤 ∈ 𝑋 ∣ ∃𝑔 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑤) ∩ 𝒫 𝑔) ≠ ∅} = {𝑦 ∈ 𝑋 ∣ ∃𝑓 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅}
86	52, 53, 55, 4, 57, 59, 60, 49, 61, 63, 75, 85	neibastop2lem 31525	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁))
87	7	ad2antrr 758	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝐽 ∈ Top)
88	60, 50	eleqtrd 2690	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑃 ∈ ∪ 𝐽)
89	9	isneip 20719	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ ∪ 𝐽) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 ⊆ ∪ 𝐽 ∧ ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁))))
90	87, 88, 89	syl2anc 691	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 ⊆ ∪ 𝐽 ∧ ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁))))
91	51, 86, 90	mpbir2and 959	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃}))
92	91	expr 641	. . . . . 6 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ⊆ 𝑋) → ((𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
93	48, 92	syl5bi 231	. . . . 5 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ⊆ 𝑋) → (𝑠 ∈ ((𝐹‘𝑃) ∩ 𝒫 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
94	93	exlimdv 1848	. . . 4 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ⊆ 𝑋) → (∃𝑠 𝑠 ∈ ((𝐹‘𝑃) ∩ 𝒫 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
95	47, 94	syl5bi 231	. . 3 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ⊆ 𝑋) → (((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅ → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
96	95	expimpd 627	. 2 ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑋) → ((𝑁 ⊆ 𝑋 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
97	46, 96	impbid 201	1 ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 ⊆ 𝑋 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ∖ cdif 3537   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  {csn 4125  ∪ cuni 4372  ∪ ciun 4455   ↦ cmpt 4643  ran crn 5039   ↾ cres 5040  ⟶wf 5800  ‘cfv 5804  ωcom 6957  reccrdg 7392  Topctop 20517  TopOnctopon 20518  neicnei 20711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-top 20521  df-topon 20523  df-nei 20712

This theorem is referenced by:  neibastop3  31527