Theorem neibastop2 34550

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 34548	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
6		topontop 22062	. . . . . . . 8 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
7	5, 6	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐽 ∈ Top)
8	7	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑋) → 𝐽 ∈ Top)
9		eqid 2738	. . . . . . 7 ⊢ ∪ 𝐽 = ∪ 𝐽
10	9	neii1 22257	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑁 ⊆ ∪ 𝐽)
11	8, 10	sylan 580	. . . . 5 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑁 ⊆ ∪ 𝐽)
12		toponuni 22063	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
13	5, 12	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
14	13	ad2antrr 723	. . . . 5 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑋 = ∪ 𝐽)
15	11, 14	sseqtrrd 3962	. . . 4 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑁 ⊆ 𝑋)
16		neii2 22259	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ∃𝑦 ∈ 𝐽 ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))
17	8, 16	sylan 580	. . . . 5 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ∃𝑦 ∈ 𝐽 ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))
18		pweq 4549	. . . . . . . . . . 11 ⊢ (𝑜 = 𝑦 → 𝒫 𝑜 = 𝒫 𝑦)
19	18	ineq2d 4146	. . . . . . . . . 10 ⊢ (𝑜 = 𝑦 → ((𝐹‘𝑥) ∩ 𝒫 𝑜) = ((𝐹‘𝑥) ∩ 𝒫 𝑦))
20	19	neeq1d 3003	. . . . . . . . 9 ⊢ (𝑜 = 𝑦 → (((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅))
21	20	raleqbi1dv 3340	. . . . . . . 8 ⊢ (𝑜 = 𝑦 → (∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅))
22	21, 4	elrab2 3627	. . . . . . 7 ⊢ (𝑦 ∈ 𝐽 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅))
23		simprrr 779	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → 𝑦 ⊆ 𝑁)
24	23	sspwd 4548	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → 𝒫 𝑦 ⊆ 𝒫 𝑁)
25		sslin 4168	. . . . . . . . . . . 12 ⊢ (𝒫 𝑦 ⊆ 𝒫 𝑁 → ((𝐹‘𝑃) ∩ 𝒫 𝑦) ⊆ ((𝐹‘𝑃) ∩ 𝒫 𝑁))
26	24, 25	syl 17	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → ((𝐹‘𝑃) ∩ 𝒫 𝑦) ⊆ ((𝐹‘𝑃) ∩ 𝒫 𝑁))
27		simprrl 778	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → {𝑃} ⊆ 𝑦)
28		snssg 4718	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ 𝑋 → (𝑃 ∈ 𝑦 ↔ {𝑃} ⊆ 𝑦))
29	28	ad3antlr 728	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → (𝑃 ∈ 𝑦 ↔ {𝑃} ⊆ 𝑦))
30	27, 29	mpbird 256	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → 𝑃 ∈ 𝑦)
31		fveq2 6774	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑃 → (𝐹‘𝑥) = (𝐹‘𝑃))
32	31	ineq1d 4145	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑃 → ((𝐹‘𝑥) ∩ 𝒫 𝑦) = ((𝐹‘𝑃) ∩ 𝒫 𝑦))
33	32	neeq1d 3003	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑃 → (((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ↔ ((𝐹‘𝑃) ∩ 𝒫 𝑦) ≠ ∅))
34	33	rspcv 3557	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ 𝑦 → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹‘𝑃) ∩ 𝒫 𝑦) ≠ ∅))
35	30, 34	syl 17	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹‘𝑃) ∩ 𝒫 𝑦) ≠ ∅))
36		ssn0 4334	. . . . . . . . . . 11 ⊢ ((((𝐹‘𝑃) ∩ 𝒫 𝑦) ⊆ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑦) ≠ ∅) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)
37	26, 35, 36	syl6an 681	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅))
38	37	expr 457	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ 𝑦 ∈ 𝒫 𝑋) → (({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁) → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
39	38	com23 86	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ 𝑦 ∈ 𝒫 𝑋) → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → (({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
40	39	expimpd 454	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ((𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅) → (({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
41	22, 40	syl5bi 241	. . . . . 6 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → (𝑦 ∈ 𝐽 → (({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
42	41	rexlimdv 3212	. . . . 5 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → (∃𝑦 ∈ 𝐽 ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅))
43	17, 42	mpd 15	. . . 4 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)
44	15, 43	jca 512	. . 3 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → (𝑁 ⊆ 𝑋 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅))
45	44	ex 413	. 2 ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) → (𝑁 ⊆ 𝑋 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
46		n0 4280	. . . 4 ⊢ (((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅ ↔ ∃𝑠 𝑠 ∈ ((𝐹‘𝑃) ∩ 𝒫 𝑁))
47		elin 3903	. . . . . 6 ⊢ (𝑠 ∈ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ↔ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))
48		simprl 768	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑁 ⊆ 𝑋)
49	13	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑋 = ∪ 𝐽)
50	48, 49	sseqtrd 3961	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑁 ⊆ ∪ 𝐽)
51	1	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑋 ∈ 𝑉)
52	2	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
53		simpll 764	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝜑)
54	53, 3	sylan 580	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥) ∧ 𝑤 ∈ (𝐹‘𝑥))) → ((𝐹‘𝑥) ∩ 𝒫 (𝑣 ∩ 𝑤)) ≠ ∅)
55		neibastop1.5	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → 𝑥 ∈ 𝑣)
56	53, 55	sylan 580	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → 𝑥 ∈ 𝑣)
57		neibastop1.6	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)
58	53, 57	sylan 580	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)
59		simplr 766	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑃 ∈ 𝑋)
60		simprrl 778	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑠 ∈ (𝐹‘𝑃))
61		simprrr 779	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑠 ∈ 𝒫 𝑁)
62	61	elpwid 4544	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑠 ⊆ 𝑁)
63		fveq2 6774	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑥 → (𝐹‘𝑛) = (𝐹‘𝑥))
64	63	ineq1d 4145	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑥 → ((𝐹‘𝑛) ∩ 𝒫 𝑏) = ((𝐹‘𝑥) ∩ 𝒫 𝑏))
65	64	cbviunv 4970	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏) = ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑏)
66		pweq 4549	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑧 → 𝒫 𝑏 = 𝒫 𝑧)
67	66	ineq2d 4146	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑧 → ((𝐹‘𝑥) ∩ 𝒫 𝑏) = ((𝐹‘𝑥) ∩ 𝒫 𝑧))
68	67	iuneq2d 4953	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑧 → ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑏) = ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
69	65, 68	eqtrid 2790	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑧 → ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏) = ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
70	69	cbviunv 4970	. . . . . . . . . . . 12 ⊢ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏) = ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)
71	70	mpteq2i 5179	. . . . . . . . . . 11 ⊢ (𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)) = (𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
72		rdgeq1 8242	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)) = (𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)) → rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) = rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑠}))
73	71, 72	ax-mp 5	. . . . . . . . . 10 ⊢ rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) = rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑠})
74	73	reseq1i 5887	. . . . . . . . 9 ⊢ (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω) = (rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑠}) ↾ ω)
75		pweq 4549	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑓 → 𝒫 𝑔 = 𝒫 𝑓)
76	75	ineq2d 4146	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑓 → ((𝐹‘𝑤) ∩ 𝒫 𝑔) = ((𝐹‘𝑤) ∩ 𝒫 𝑓))
77	76	neeq1d 3003	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑓 → (((𝐹‘𝑤) ∩ 𝒫 𝑔) ≠ ∅ ↔ ((𝐹‘𝑤) ∩ 𝒫 𝑓) ≠ ∅))
78	77	cbvrexvw 3384	. . . . . . . . . . 11 ⊢ (∃𝑔 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑤) ∩ 𝒫 𝑔) ≠ ∅ ↔ ∃𝑓 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑤) ∩ 𝒫 𝑓) ≠ ∅)
79		fveq2 6774	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑦 → (𝐹‘𝑤) = (𝐹‘𝑦))
80	79	ineq1d 4145	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑦 → ((𝐹‘𝑤) ∩ 𝒫 𝑓) = ((𝐹‘𝑦) ∩ 𝒫 𝑓))
81	80	neeq1d 3003	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑦 → (((𝐹‘𝑤) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅))
82	81	rexbidv 3226	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑦 → (∃𝑓 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑤) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑓 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅))
83	78, 82	syl5bb 283	. . . . . . . . . 10 ⊢ (𝑤 = 𝑦 → (∃𝑔 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑤) ∩ 𝒫 𝑔) ≠ ∅ ↔ ∃𝑓 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅))
84	83	cbvrabv 3426	. . . . . . . . 9 ⊢ {𝑤 ∈ 𝑋 ∣ ∃𝑔 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑤) ∩ 𝒫 𝑔) ≠ ∅} = {𝑦 ∈ 𝑋 ∣ ∃𝑓 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅}
85	51, 52, 54, 4, 56, 58, 59, 48, 60, 62, 74, 84	neibastop2lem 34549	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁))
86	7	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝐽 ∈ Top)
87	59, 49	eleqtrd 2841	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑃 ∈ ∪ 𝐽)
88	9	isneip 22256	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ ∪ 𝐽) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 ⊆ ∪ 𝐽 ∧ ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁))))
89	86, 87, 88	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 ⊆ ∪ 𝐽 ∧ ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁))))
90	50, 85, 89	mpbir2and 710	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃}))
91	90	expr 457	. . . . . 6 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ⊆ 𝑋) → ((𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
92	47, 91	syl5bi 241	. . . . 5 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ⊆ 𝑋) → (𝑠 ∈ ((𝐹‘𝑃) ∩ 𝒫 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
93	92	exlimdv 1936	. . . 4 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ⊆ 𝑋) → (∃𝑠 𝑠 ∈ ((𝐹‘𝑃) ∩ 𝒫 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
94	46, 93	syl5bi 241	. . 3 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ⊆ 𝑋) → (((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅ → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
95	94	expimpd 454	. 2 ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑋) → ((𝑁 ⊆ 𝑋 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
96	45, 95	impbid 211	1 ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 ⊆ 𝑋 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086   = wceq 1539  ∃wex 1782   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3065  {crab 3068  Vcvv 3432   ∖ cdif 3884   ∩ cin 3886   ⊆ wss 3887  ∅c0 4256  𝒫 cpw 4533  {csn 4561  ∪ cuni 4839  ∪ ciun 4924   ↦ cmpt 5157  ran crn 5590   ↾ cres 5591  ⟶wf 6429  ‘cfv 6433  ωcom 7712  reccrdg 8240  Topctop 22042  TopOnctopon 22059  neicnei 22248

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-om 7713  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-top 22043  df-topon 22060  df-nei 22249

This theorem is referenced by:  neibastop3  34551