Theorem neibastop2 36681

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 36679	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
6		topontop 22960	. . . . . . . 8 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
7	5, 6	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐽 ∈ Top)
8	7	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑋) → 𝐽 ∈ Top)
9		eqid 2761	. . . . . . 7 ⊢ ∪ 𝐽 = ∪ 𝐽
10	9	neii1 23153	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑁 ⊆ ∪ 𝐽)
11	8, 10	sylan 589	. . . . 5 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑁 ⊆ ∪ 𝐽)
12		toponuni 22961	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
13	5, 12	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
14	13	ad2antrr 736	. . . . 5 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑋 = ∪ 𝐽)
15	11, 14	sseqtrrd 3971	. . . 4 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑁 ⊆ 𝑋)
16		neii2 23155	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ∃𝑦 ∈ 𝐽 ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))
17	8, 16	sylan 589	. . . . 5 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ∃𝑦 ∈ 𝐽 ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))
18		pweq 4566	. . . . . . . . . . 11 ⊢ (𝑜 = 𝑦 → 𝒫 𝑜 = 𝒫 𝑦)
19	18	ineq2d 4170	. . . . . . . . . 10 ⊢ (𝑜 = 𝑦 → ((𝐹‘𝑥) ∩ 𝒫 𝑜) = ((𝐹‘𝑥) ∩ 𝒫 𝑦))
20	19	neeq1d 3015	. . . . . . . . 9 ⊢ (𝑜 = 𝑦 → (((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅))
21	20	raleqbi1dv 3329	. . . . . . . 8 ⊢ (𝑜 = 𝑦 → (∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅))
22	21, 4	elrab2 3652	. . . . . . 7 ⊢ (𝑦 ∈ 𝐽 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅))
23		simprrr 791	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → 𝑦 ⊆ 𝑁)
24	23	sspwd 4565	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → 𝒫 𝑦 ⊆ 𝒫 𝑁)
25		sslin 4192	. . . . . . . . . . . 12 ⊢ (𝒫 𝑦 ⊆ 𝒫 𝑁 → ((𝐹‘𝑃) ∩ 𝒫 𝑦) ⊆ ((𝐹‘𝑃) ∩ 𝒫 𝑁))
26	24, 25	syl 17	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → ((𝐹‘𝑃) ∩ 𝒫 𝑦) ⊆ ((𝐹‘𝑃) ∩ 𝒫 𝑁))
27		simprrl 790	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → {𝑃} ⊆ 𝑦)
28		snssg 4739	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ 𝑋 → (𝑃 ∈ 𝑦 ↔ {𝑃} ⊆ 𝑦))
29	28	ad3antlr 741	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → (𝑃 ∈ 𝑦 ↔ {𝑃} ⊆ 𝑦))
30	27, 29	mpbird 259	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → 𝑃 ∈ 𝑦)
31		fveq2 6861	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑃 → (𝐹‘𝑥) = (𝐹‘𝑃))
32	31	ineq1d 4169	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑃 → ((𝐹‘𝑥) ∩ 𝒫 𝑦) = ((𝐹‘𝑃) ∩ 𝒫 𝑦))
33	32	neeq1d 3015	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑃 → (((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ↔ ((𝐹‘𝑃) ∩ 𝒫 𝑦) ≠ ∅))
34	33	rspcv 3576	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ 𝑦 → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹‘𝑃) ∩ 𝒫 𝑦) ≠ ∅))
35	30, 34	syl 17	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹‘𝑃) ∩ 𝒫 𝑦) ≠ ∅))
36		ssn0 4355	. . . . . . . . . . 11 ⊢ ((((𝐹‘𝑃) ∩ 𝒫 𝑦) ⊆ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑦) ≠ ∅) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)
37	26, 35, 36	syl6an 694	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅))
38	37	expr 460	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ 𝑦 ∈ 𝒫 𝑋) → (({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁) → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
39	38	com23 86	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ 𝑦 ∈ 𝒫 𝑋) → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → (({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
40	39	expimpd 457	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ((𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅) → (({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
41	22, 40	biimtrid 244	. . . . . 6 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → (𝑦 ∈ 𝐽 → (({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
42	41	rexlimdv 3160	. . . . 5 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → (∃𝑦 ∈ 𝐽 ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅))
43	17, 42	mpd 15	. . . 4 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)
44	15, 43	jca 519	. . 3 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → (𝑁 ⊆ 𝑋 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅))
45	44	ex 416	. 2 ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) → (𝑁 ⊆ 𝑋 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
46		n0 4303	. . . 4 ⊢ (((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅ ↔ ∃𝑠 𝑠 ∈ ((𝐹‘𝑃) ∩ 𝒫 𝑁))
47		elin 3918	. . . . . 6 ⊢ (𝑠 ∈ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ↔ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))
48		simprl 780	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑁 ⊆ 𝑋)
49	13	ad2antrr 736	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑋 = ∪ 𝐽)
50	48, 49	sseqtrd 3970	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑁 ⊆ ∪ 𝐽)
51	1	ad2antrr 736	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑋 ∈ 𝑉)
52	2	ad2antrr 736	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
53		simpll 776	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝜑)
54	53, 3	sylan 589	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥) ∧ 𝑤 ∈ (𝐹‘𝑥))) → ((𝐹‘𝑥) ∩ 𝒫 (𝑣 ∩ 𝑤)) ≠ ∅)
55		neibastop1.5	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → 𝑥 ∈ 𝑣)
56	53, 55	sylan 589	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → 𝑥 ∈ 𝑣)
57		neibastop1.6	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)
58	53, 57	sylan 589	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)
59		simplr 778	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑃 ∈ 𝑋)
60		simprrl 790	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑠 ∈ (𝐹‘𝑃))
61		simprrr 791	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑠 ∈ 𝒫 𝑁)
62	61	elpwid 4561	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑠 ⊆ 𝑁)
63		fveq2 6861	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑥 → (𝐹‘𝑛) = (𝐹‘𝑥))
64	63	ineq1d 4169	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑥 → ((𝐹‘𝑛) ∩ 𝒫 𝑏) = ((𝐹‘𝑥) ∩ 𝒫 𝑏))
65	64	cbviunv 4993	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏) = ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑏)
66		pweq 4566	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑧 → 𝒫 𝑏 = 𝒫 𝑧)
67	66	ineq2d 4170	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑧 → ((𝐹‘𝑥) ∩ 𝒫 𝑏) = ((𝐹‘𝑥) ∩ 𝒫 𝑧))
68	67	iuneq2d 4977	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑧 → ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑏) = ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
69	65, 68	eqtrid 2808	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑧 → ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏) = ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
70	69	cbviunv 4993	. . . . . . . . . . . 12 ⊢ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏) = ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)
71	70	mpteq2i 5193	. . . . . . . . . . 11 ⊢ (𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)) = (𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
72		rdgeq1 8375	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)) = (𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)) → rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) = rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑠}))
73	71, 72	ax-mp 5	. . . . . . . . . 10 ⊢ rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) = rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑠})
74	73	reseq1i 5957	. . . . . . . . 9 ⊢ (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω) = (rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑠}) ↾ ω)
75		pweq 4566	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑓 → 𝒫 𝑔 = 𝒫 𝑓)
76	75	ineq2d 4170	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑓 → ((𝐹‘𝑤) ∩ 𝒫 𝑔) = ((𝐹‘𝑤) ∩ 𝒫 𝑓))
77	76	neeq1d 3015	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑓 → (((𝐹‘𝑤) ∩ 𝒫 𝑔) ≠ ∅ ↔ ((𝐹‘𝑤) ∩ 𝒫 𝑓) ≠ ∅))
78	77	cbvrexvw 3240	. . . . . . . . . . 11 ⊢ (∃𝑔 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑤) ∩ 𝒫 𝑔) ≠ ∅ ↔ ∃𝑓 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑤) ∩ 𝒫 𝑓) ≠ ∅)
79		fveq2 6861	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑦 → (𝐹‘𝑤) = (𝐹‘𝑦))
80	79	ineq1d 4169	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑦 → ((𝐹‘𝑤) ∩ 𝒫 𝑓) = ((𝐹‘𝑦) ∩ 𝒫 𝑓))
81	80	neeq1d 3015	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑦 → (((𝐹‘𝑤) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅))
82	81	rexbidv 3185	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑦 → (∃𝑓 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑤) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑓 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅))
83	78, 82	bitrid 285	. . . . . . . . . 10 ⊢ (𝑤 = 𝑦 → (∃𝑔 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑤) ∩ 𝒫 𝑔) ≠ ∅ ↔ ∃𝑓 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅))
84	83	cbvrabv 3423	. . . . . . . . 9 ⊢ {𝑤 ∈ 𝑋 ∣ ∃𝑔 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑤) ∩ 𝒫 𝑔) ≠ ∅} = {𝑦 ∈ 𝑋 ∣ ∃𝑓 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅}
85	51, 52, 54, 4, 56, 58, 59, 48, 60, 62, 74, 84	neibastop2lem 36680	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁))
86	7	ad2antrr 736	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝐽 ∈ Top)
87	59, 49	eleqtrd 2863	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑃 ∈ ∪ 𝐽)
88	9	isneip 23152	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ ∪ 𝐽) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 ⊆ ∪ 𝐽 ∧ ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁))))
89	86, 87, 88	syl2anc 593	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 ⊆ ∪ 𝐽 ∧ ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁))))
90	50, 85, 89	mpbir2and 723	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃}))
91	90	expr 460	. . . . . 6 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ⊆ 𝑋) → ((𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
92	47, 91	biimtrid 244	. . . . 5 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ⊆ 𝑋) → (𝑠 ∈ ((𝐹‘𝑃) ∩ 𝒫 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
93	92	exlimdv 1952	. . . 4 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ⊆ 𝑋) → (∃𝑠 𝑠 ∈ ((𝐹‘𝑃) ∩ 𝒫 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
94	46, 93	biimtrid 244	. . 3 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ⊆ 𝑋) → (((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅ → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
95	94	expimpd 457	. 2 ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑋) → ((𝑁 ⊆ 𝑋 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
96	45, 95	impbid 214	1 ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 ⊆ 𝑋 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∧ w3a 1097   = wceq 1559  ∃wex 1798   ∈ wcel 2141   ≠ wne 2956  ∀wral 3075  ∃wrex 3085  {crab 3413  Vcvv 3453   ∖ cdif 3899   ∩ cin 3901   ⊆ wss 3902  ∅c0 4283  𝒫 cpw 4552  {csn 4579  ∪ cuni 4862  ∪ ciun 4946   ↦ cmpt 5178  ran crn 5644   ↾ cres 5645  ⟶wf 6511  ‘cfv 6515  ωcom 7840  reccrdg 8373  Topctop 22940  TopOnctopon 22957  neicnei 23144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5224  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7712

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6282  df-ord 6343  df-on 6344  df-lim 6345  df-suc 6346  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522  df-fv 6523  df-ov 7393  df-om 7841  df-2nd 7965  df-frecs 8255  df-wrecs 8286  df-recs 8335  df-rdg 8374  df-top 22941  df-topon 22958  df-nei 23145

This theorem is referenced by:  neibastop3  36682