Theorem neibastop2 35235

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 35233	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
6		topontop 22407	. . . . . . . 8 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
7	5, 6	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐽 ∈ Top)
8	7	adantr 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑋) → 𝐽 ∈ Top)
9		eqid 2733	. . . . . . 7 ⊢ ∪ 𝐽 = ∪ 𝐽
10	9	neii1 22602	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑁 ⊆ ∪ 𝐽)
11	8, 10	sylan 581	. . . . 5 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑁 ⊆ ∪ 𝐽)
12		toponuni 22408	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
13	5, 12	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
14	13	ad2antrr 725	. . . . 5 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑋 = ∪ 𝐽)
15	11, 14	sseqtrrd 4023	. . . 4 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑁 ⊆ 𝑋)
16		neii2 22604	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ∃𝑦 ∈ 𝐽 ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))
17	8, 16	sylan 581	. . . . 5 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ∃𝑦 ∈ 𝐽 ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))
18		pweq 4616	. . . . . . . . . . 11 ⊢ (𝑜 = 𝑦 → 𝒫 𝑜 = 𝒫 𝑦)
19	18	ineq2d 4212	. . . . . . . . . 10 ⊢ (𝑜 = 𝑦 → ((𝐹‘𝑥) ∩ 𝒫 𝑜) = ((𝐹‘𝑥) ∩ 𝒫 𝑦))
20	19	neeq1d 3001	. . . . . . . . 9 ⊢ (𝑜 = 𝑦 → (((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅))
21	20	raleqbi1dv 3334	. . . . . . . 8 ⊢ (𝑜 = 𝑦 → (∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅))
22	21, 4	elrab2 3686	. . . . . . 7 ⊢ (𝑦 ∈ 𝐽 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅))
23		simprrr 781	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → 𝑦 ⊆ 𝑁)
24	23	sspwd 4615	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → 𝒫 𝑦 ⊆ 𝒫 𝑁)
25		sslin 4234	. . . . . . . . . . . 12 ⊢ (𝒫 𝑦 ⊆ 𝒫 𝑁 → ((𝐹‘𝑃) ∩ 𝒫 𝑦) ⊆ ((𝐹‘𝑃) ∩ 𝒫 𝑁))
26	24, 25	syl 17	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → ((𝐹‘𝑃) ∩ 𝒫 𝑦) ⊆ ((𝐹‘𝑃) ∩ 𝒫 𝑁))
27		simprrl 780	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → {𝑃} ⊆ 𝑦)
28		snssg 4787	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ 𝑋 → (𝑃 ∈ 𝑦 ↔ {𝑃} ⊆ 𝑦))
29	28	ad3antlr 730	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → (𝑃 ∈ 𝑦 ↔ {𝑃} ⊆ 𝑦))
30	27, 29	mpbird 257	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → 𝑃 ∈ 𝑦)
31		fveq2 6889	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑃 → (𝐹‘𝑥) = (𝐹‘𝑃))
32	31	ineq1d 4211	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑃 → ((𝐹‘𝑥) ∩ 𝒫 𝑦) = ((𝐹‘𝑃) ∩ 𝒫 𝑦))
33	32	neeq1d 3001	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑃 → (((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ↔ ((𝐹‘𝑃) ∩ 𝒫 𝑦) ≠ ∅))
34	33	rspcv 3609	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ 𝑦 → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹‘𝑃) ∩ 𝒫 𝑦) ≠ ∅))
35	30, 34	syl 17	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹‘𝑃) ∩ 𝒫 𝑦) ≠ ∅))
36		ssn0 4400	. . . . . . . . . . 11 ⊢ ((((𝐹‘𝑃) ∩ 𝒫 𝑦) ⊆ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑦) ≠ ∅) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)
37	26, 35, 36	syl6an 683	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅))
38	37	expr 458	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ 𝑦 ∈ 𝒫 𝑋) → (({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁) → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
39	38	com23 86	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ 𝑦 ∈ 𝒫 𝑋) → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → (({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
40	39	expimpd 455	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ((𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅) → (({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
41	22, 40	biimtrid 241	. . . . . 6 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → (𝑦 ∈ 𝐽 → (({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
42	41	rexlimdv 3154	. . . . 5 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → (∃𝑦 ∈ 𝐽 ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅))
43	17, 42	mpd 15	. . . 4 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)
44	15, 43	jca 513	. . 3 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → (𝑁 ⊆ 𝑋 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅))
45	44	ex 414	. 2 ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) → (𝑁 ⊆ 𝑋 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
46		n0 4346	. . . 4 ⊢ (((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅ ↔ ∃𝑠 𝑠 ∈ ((𝐹‘𝑃) ∩ 𝒫 𝑁))
47		elin 3964	. . . . . 6 ⊢ (𝑠 ∈ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ↔ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))
48		simprl 770	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑁 ⊆ 𝑋)
49	13	ad2antrr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑋 = ∪ 𝐽)
50	48, 49	sseqtrd 4022	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑁 ⊆ ∪ 𝐽)
51	1	ad2antrr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑋 ∈ 𝑉)
52	2	ad2antrr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
53		simpll 766	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝜑)
54	53, 3	sylan 581	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥) ∧ 𝑤 ∈ (𝐹‘𝑥))) → ((𝐹‘𝑥) ∩ 𝒫 (𝑣 ∩ 𝑤)) ≠ ∅)
55		neibastop1.5	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → 𝑥 ∈ 𝑣)
56	53, 55	sylan 581	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → 𝑥 ∈ 𝑣)
57		neibastop1.6	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)
58	53, 57	sylan 581	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)
59		simplr 768	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑃 ∈ 𝑋)
60		simprrl 780	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑠 ∈ (𝐹‘𝑃))
61		simprrr 781	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑠 ∈ 𝒫 𝑁)
62	61	elpwid 4611	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑠 ⊆ 𝑁)
63		fveq2 6889	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑥 → (𝐹‘𝑛) = (𝐹‘𝑥))
64	63	ineq1d 4211	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑥 → ((𝐹‘𝑛) ∩ 𝒫 𝑏) = ((𝐹‘𝑥) ∩ 𝒫 𝑏))
65	64	cbviunv 5043	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏) = ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑏)
66		pweq 4616	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑧 → 𝒫 𝑏 = 𝒫 𝑧)
67	66	ineq2d 4212	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑧 → ((𝐹‘𝑥) ∩ 𝒫 𝑏) = ((𝐹‘𝑥) ∩ 𝒫 𝑧))
68	67	iuneq2d 5026	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑧 → ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑏) = ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
69	65, 68	eqtrid 2785	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑧 → ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏) = ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
70	69	cbviunv 5043	. . . . . . . . . . . 12 ⊢ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏) = ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)
71	70	mpteq2i 5253	. . . . . . . . . . 11 ⊢ (𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)) = (𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
72		rdgeq1 8408	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)) = (𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)) → rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) = rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑠}))
73	71, 72	ax-mp 5	. . . . . . . . . 10 ⊢ rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) = rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑠})
74	73	reseq1i 5976	. . . . . . . . 9 ⊢ (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω) = (rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑠}) ↾ ω)
75		pweq 4616	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑓 → 𝒫 𝑔 = 𝒫 𝑓)
76	75	ineq2d 4212	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑓 → ((𝐹‘𝑤) ∩ 𝒫 𝑔) = ((𝐹‘𝑤) ∩ 𝒫 𝑓))
77	76	neeq1d 3001	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑓 → (((𝐹‘𝑤) ∩ 𝒫 𝑔) ≠ ∅ ↔ ((𝐹‘𝑤) ∩ 𝒫 𝑓) ≠ ∅))
78	77	cbvrexvw 3236	. . . . . . . . . . 11 ⊢ (∃𝑔 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑤) ∩ 𝒫 𝑔) ≠ ∅ ↔ ∃𝑓 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑤) ∩ 𝒫 𝑓) ≠ ∅)
79		fveq2 6889	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑦 → (𝐹‘𝑤) = (𝐹‘𝑦))
80	79	ineq1d 4211	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑦 → ((𝐹‘𝑤) ∩ 𝒫 𝑓) = ((𝐹‘𝑦) ∩ 𝒫 𝑓))
81	80	neeq1d 3001	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑦 → (((𝐹‘𝑤) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅))
82	81	rexbidv 3179	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑦 → (∃𝑓 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑤) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑓 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅))
83	78, 82	bitrid 283	. . . . . . . . . 10 ⊢ (𝑤 = 𝑦 → (∃𝑔 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑤) ∩ 𝒫 𝑔) ≠ ∅ ↔ ∃𝑓 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅))
84	83	cbvrabv 3443	. . . . . . . . 9 ⊢ {𝑤 ∈ 𝑋 ∣ ∃𝑔 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑤) ∩ 𝒫 𝑔) ≠ ∅} = {𝑦 ∈ 𝑋 ∣ ∃𝑓 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅}
85	51, 52, 54, 4, 56, 58, 59, 48, 60, 62, 74, 84	neibastop2lem 35234	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁))
86	7	ad2antrr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝐽 ∈ Top)
87	59, 49	eleqtrd 2836	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑃 ∈ ∪ 𝐽)
88	9	isneip 22601	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ ∪ 𝐽) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 ⊆ ∪ 𝐽 ∧ ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁))))
89	86, 87, 88	syl2anc 585	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 ⊆ ∪ 𝐽 ∧ ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁))))
90	50, 85, 89	mpbir2and 712	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃}))
91	90	expr 458	. . . . . 6 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ⊆ 𝑋) → ((𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
92	47, 91	biimtrid 241	. . . . 5 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ⊆ 𝑋) → (𝑠 ∈ ((𝐹‘𝑃) ∩ 𝒫 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
93	92	exlimdv 1937	. . . 4 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ⊆ 𝑋) → (∃𝑠 𝑠 ∈ ((𝐹‘𝑃) ∩ 𝒫 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
94	46, 93	biimtrid 241	. . 3 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ⊆ 𝑋) → (((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅ → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
95	94	expimpd 455	. 2 ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑋) → ((𝑁 ⊆ 𝑋 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
96	45, 95	impbid 211	1 ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 ⊆ 𝑋 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542  ∃wex 1782   ∈ wcel 2107   ≠ wne 2941  ∀wral 3062  ∃wrex 3071  {crab 3433  Vcvv 3475   ∖ cdif 3945   ∩ cin 3947   ⊆ wss 3948  ∅c0 4322  𝒫 cpw 4602  {csn 4628  ∪ cuni 4908  ∪ ciun 4997   ↦ cmpt 5231  ran crn 5677   ↾ cres 5678  ⟶wf 6537  ‘cfv 6541  ωcom 7852  reccrdg 8406  Topctop 22387  TopOnctopon 22404  neicnei 22593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7409  df-om 7853  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-top 22388  df-topon 22405  df-nei 22594

This theorem is referenced by:  neibastop3  35236