Theorem neibastop2 32944

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 32942	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
6		topontop 21125	. . . . . . . 8 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
7	5, 6	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐽 ∈ Top)
8	7	adantr 474	. . . . . 6 ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑋) → 𝐽 ∈ Top)
9		eqid 2777	. . . . . . 7 ⊢ ∪ 𝐽 = ∪ 𝐽
10	9	neii1 21318	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑁 ⊆ ∪ 𝐽)
11	8, 10	sylan 575	. . . . 5 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑁 ⊆ ∪ 𝐽)
12		toponuni 21126	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
13	5, 12	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
14	13	ad2antrr 716	. . . . 5 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑋 = ∪ 𝐽)
15	11, 14	sseqtr4d 3860	. . . 4 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑁 ⊆ 𝑋)
16		neii2 21320	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ∃𝑦 ∈ 𝐽 ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))
17	8, 16	sylan 575	. . . . 5 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ∃𝑦 ∈ 𝐽 ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))
18		pweq 4381	. . . . . . . . . . 11 ⊢ (𝑜 = 𝑦 → 𝒫 𝑜 = 𝒫 𝑦)
19	18	ineq2d 4036	. . . . . . . . . 10 ⊢ (𝑜 = 𝑦 → ((𝐹‘𝑥) ∩ 𝒫 𝑜) = ((𝐹‘𝑥) ∩ 𝒫 𝑦))
20	19	neeq1d 3027	. . . . . . . . 9 ⊢ (𝑜 = 𝑦 → (((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅))
21	20	raleqbi1dv 3327	. . . . . . . 8 ⊢ (𝑜 = 𝑦 → (∀𝑥 ∈ 𝑜 ((𝐹‘𝑥) ∩ 𝒫 𝑜) ≠ ∅ ↔ ∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅))
22	21, 4	elrab2 3575	. . . . . . 7 ⊢ (𝑦 ∈ 𝐽 ↔ (𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅))
23		simprrr 772	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → 𝑦 ⊆ 𝑁)
24		sspwb 5149	. . . . . . . . . . . . 13 ⊢ (𝑦 ⊆ 𝑁 ↔ 𝒫 𝑦 ⊆ 𝒫 𝑁)
25	23, 24	sylib 210	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → 𝒫 𝑦 ⊆ 𝒫 𝑁)
26		sslin 4058	. . . . . . . . . . . 12 ⊢ (𝒫 𝑦 ⊆ 𝒫 𝑁 → ((𝐹‘𝑃) ∩ 𝒫 𝑦) ⊆ ((𝐹‘𝑃) ∩ 𝒫 𝑁))
27	25, 26	syl 17	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → ((𝐹‘𝑃) ∩ 𝒫 𝑦) ⊆ ((𝐹‘𝑃) ∩ 𝒫 𝑁))
28		simprrl 771	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → {𝑃} ⊆ 𝑦)
29		snssg 4547	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ 𝑋 → (𝑃 ∈ 𝑦 ↔ {𝑃} ⊆ 𝑦))
30	29	ad3antlr 721	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → (𝑃 ∈ 𝑦 ↔ {𝑃} ⊆ 𝑦))
31	28, 30	mpbird 249	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → 𝑃 ∈ 𝑦)
32		fveq2 6446	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑃 → (𝐹‘𝑥) = (𝐹‘𝑃))
33	32	ineq1d 4035	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑃 → ((𝐹‘𝑥) ∩ 𝒫 𝑦) = ((𝐹‘𝑃) ∩ 𝒫 𝑦))
34	33	neeq1d 3027	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑃 → (((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ ↔ ((𝐹‘𝑃) ∩ 𝒫 𝑦) ≠ ∅))
35	34	rspcv 3506	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ 𝑦 → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹‘𝑃) ∩ 𝒫 𝑦) ≠ ∅))
36	31, 35	syl 17	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹‘𝑃) ∩ 𝒫 𝑦) ≠ ∅))
37		ssn0 4201	. . . . . . . . . . 11 ⊢ ((((𝐹‘𝑃) ∩ 𝒫 𝑦) ⊆ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑦) ≠ ∅) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)
38	27, 36, 37	syl6an 674	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ (𝑦 ∈ 𝒫 𝑋 ∧ ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁))) → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅))
39	38	expr 450	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ 𝑦 ∈ 𝒫 𝑋) → (({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁) → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
40	39	com23 86	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) ∧ 𝑦 ∈ 𝒫 𝑋) → (∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅ → (({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
41	40	expimpd 447	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ((𝑦 ∈ 𝒫 𝑋 ∧ ∀𝑥 ∈ 𝑦 ((𝐹‘𝑥) ∩ 𝒫 𝑦) ≠ ∅) → (({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
42	22, 41	syl5bi 234	. . . . . 6 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → (𝑦 ∈ 𝐽 → (({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
43	42	rexlimdv 3211	. . . . 5 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → (∃𝑦 ∈ 𝐽 ({𝑃} ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑁) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅))
44	17, 43	mpd 15	. . . 4 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)
45	15, 44	jca 507	. . 3 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → (𝑁 ⊆ 𝑋 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅))
46	45	ex 403	. 2 ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) → (𝑁 ⊆ 𝑋 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))
47		n0 4158	. . . 4 ⊢ (((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅ ↔ ∃𝑠 𝑠 ∈ ((𝐹‘𝑃) ∩ 𝒫 𝑁))
48		elin 4018	. . . . . 6 ⊢ (𝑠 ∈ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ↔ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))
49		simprl 761	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑁 ⊆ 𝑋)
50	13	ad2antrr 716	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑋 = ∪ 𝐽)
51	49, 50	sseqtrd 3859	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑁 ⊆ ∪ 𝐽)
52	1	ad2antrr 716	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑋 ∈ 𝑉)
53	2	ad2antrr 716	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝐹:𝑋⟶(𝒫 𝒫 𝑋 ∖ {∅}))
54		simpll 757	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝜑)
55	54, 3	sylan 575	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥) ∧ 𝑤 ∈ (𝐹‘𝑥))) → ((𝐹‘𝑥) ∩ 𝒫 (𝑣 ∩ 𝑤)) ≠ ∅)
56		neibastop1.5	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → 𝑥 ∈ 𝑣)
57	54, 56	sylan 575	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → 𝑥 ∈ 𝑣)
58		neibastop1.6	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)
59	54, 58	sylan 575	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) ∧ (𝑥 ∈ 𝑋 ∧ 𝑣 ∈ (𝐹‘𝑥))) → ∃𝑡 ∈ (𝐹‘𝑥)∀𝑦 ∈ 𝑡 ((𝐹‘𝑦) ∩ 𝒫 𝑣) ≠ ∅)
60		simplr 759	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑃 ∈ 𝑋)
61		simprrl 771	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑠 ∈ (𝐹‘𝑃))
62		simprrr 772	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑠 ∈ 𝒫 𝑁)
63	62	elpwid 4390	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑠 ⊆ 𝑁)
64		fveq2 6446	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑥 → (𝐹‘𝑛) = (𝐹‘𝑥))
65	64	ineq1d 4035	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑥 → ((𝐹‘𝑛) ∩ 𝒫 𝑏) = ((𝐹‘𝑥) ∩ 𝒫 𝑏))
66	65	cbviunv 4792	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏) = ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑏)
67		pweq 4381	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = 𝑧 → 𝒫 𝑏 = 𝒫 𝑧)
68	67	ineq2d 4036	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑧 → ((𝐹‘𝑥) ∩ 𝒫 𝑏) = ((𝐹‘𝑥) ∩ 𝒫 𝑧))
69	68	iuneq2d 4780	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑧 → ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑏) = ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
70	66, 69	syl5eq 2825	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑧 → ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏) = ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
71	70	cbviunv 4792	. . . . . . . . . . . 12 ⊢ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏) = ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)
72	71	mpteq2i 4976	. . . . . . . . . . 11 ⊢ (𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)) = (𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧))
73		rdgeq1 7790	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)) = (𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)) → rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) = rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑠}))
74	72, 73	ax-mp 5	. . . . . . . . . 10 ⊢ rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) = rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑠})
75	74	reseq1i 5638	. . . . . . . . 9 ⊢ (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω) = (rec((𝑎 ∈ V ↦ ∪ 𝑧 ∈ 𝑎 ∪ 𝑥 ∈ 𝑋 ((𝐹‘𝑥) ∩ 𝒫 𝑧)), {𝑠}) ↾ ω)
76		pweq 4381	. . . . . . . . . . . . . 14 ⊢ (𝑔 = 𝑓 → 𝒫 𝑔 = 𝒫 𝑓)
77	76	ineq2d 4036	. . . . . . . . . . . . 13 ⊢ (𝑔 = 𝑓 → ((𝐹‘𝑤) ∩ 𝒫 𝑔) = ((𝐹‘𝑤) ∩ 𝒫 𝑓))
78	77	neeq1d 3027	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝑓 → (((𝐹‘𝑤) ∩ 𝒫 𝑔) ≠ ∅ ↔ ((𝐹‘𝑤) ∩ 𝒫 𝑓) ≠ ∅))
79	78	cbvrexv 3367	. . . . . . . . . . 11 ⊢ (∃𝑔 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑤) ∩ 𝒫 𝑔) ≠ ∅ ↔ ∃𝑓 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑤) ∩ 𝒫 𝑓) ≠ ∅)
80		fveq2 6446	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑦 → (𝐹‘𝑤) = (𝐹‘𝑦))
81	80	ineq1d 4035	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑦 → ((𝐹‘𝑤) ∩ 𝒫 𝑓) = ((𝐹‘𝑦) ∩ 𝒫 𝑓))
82	81	neeq1d 3027	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑦 → (((𝐹‘𝑤) ∩ 𝒫 𝑓) ≠ ∅ ↔ ((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅))
83	82	rexbidv 3236	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑦 → (∃𝑓 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑤) ∩ 𝒫 𝑓) ≠ ∅ ↔ ∃𝑓 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅))
84	79, 83	syl5bb 275	. . . . . . . . . 10 ⊢ (𝑤 = 𝑦 → (∃𝑔 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑤) ∩ 𝒫 𝑔) ≠ ∅ ↔ ∃𝑓 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅))
85	84	cbvrabv 3395	. . . . . . . . 9 ⊢ {𝑤 ∈ 𝑋 ∣ ∃𝑔 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑤) ∩ 𝒫 𝑔) ≠ ∅} = {𝑦 ∈ 𝑋 ∣ ∃𝑓 ∈ ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑏 ∈ 𝑎 ∪ 𝑛 ∈ 𝑋 ((𝐹‘𝑛) ∩ 𝒫 𝑏)), {𝑠}) ↾ ω)((𝐹‘𝑦) ∩ 𝒫 𝑓) ≠ ∅}
86	52, 53, 55, 4, 57, 59, 60, 49, 61, 63, 75, 85	neibastop2lem 32943	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁))
87	7	ad2antrr 716	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝐽 ∈ Top)
88	60, 50	eleqtrd 2860	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑃 ∈ ∪ 𝐽)
89	9	isneip 21317	. . . . . . . . 9 ⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ ∪ 𝐽) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 ⊆ ∪ 𝐽 ∧ ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁))))
90	87, 88, 89	syl2anc 579	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 ⊆ ∪ 𝐽 ∧ ∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑁))))
91	51, 86, 90	mpbir2and 703	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ (𝑁 ⊆ 𝑋 ∧ (𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁))) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃}))
92	91	expr 450	. . . . . 6 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ⊆ 𝑋) → ((𝑠 ∈ (𝐹‘𝑃) ∧ 𝑠 ∈ 𝒫 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
93	48, 92	syl5bi 234	. . . . 5 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ⊆ 𝑋) → (𝑠 ∈ ((𝐹‘𝑃) ∩ 𝒫 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
94	93	exlimdv 1976	. . . 4 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ⊆ 𝑋) → (∃𝑠 𝑠 ∈ ((𝐹‘𝑃) ∩ 𝒫 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
95	47, 94	syl5bi 234	. . 3 ⊢ (((𝜑 ∧ 𝑃 ∈ 𝑋) ∧ 𝑁 ⊆ 𝑋) → (((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅ → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
96	95	expimpd 447	. 2 ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑋) → ((𝑁 ⊆ 𝑋 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})))
97	46, 96	impbid 204	1 ⊢ ((𝜑 ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 ⊆ 𝑋 ∧ ((𝐹‘𝑃) ∩ 𝒫 𝑁) ≠ ∅)))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   ∧ w3a 1071   = wceq 1601  ∃wex 1823   ∈ wcel 2106   ≠ wne 2968  ∀wral 3089  ∃wrex 3090  {crab 3093  Vcvv 3397   ∖ cdif 3788   ∩ cin 3790   ⊆ wss 3791  ∅c0 4140  𝒫 cpw 4378  {csn 4397  ∪ cuni 4671  ∪ ciun 4753   ↦ cmpt 4965  ran crn 5356   ↾ cres 5357  ⟶wf 6131  ‘cfv 6135  ωcom 7343  reccrdg 7788  Topctop 21105  TopOnctopon 21122  neicnei 21309

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-ral 3094  df-rex 3095  df-reu 3096  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-pss 3807  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4672  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-om 7344  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-top 21106  df-topon 21123  df-nei 21310

This theorem is referenced by:  neibastop3  32945