neiptopnei

	Ref	Expression
Hypotheses	neiptop.o	$⊢ J = \{a \in 𝒫 X \| \forall p \in a a \in N (p)\}$
	neiptop.0	$⊢ φ \to N : X ⟶ 𝒫 𝒫 X$
	neiptop.1	$⊢ (((φ \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \to b \in N (p)$
	neiptop.2	$⊢ (φ \land p \in X) \to fi (N (p)) \subseteq N (p)$
	neiptop.3	$⊢ ((φ \land p \in X) \land a \in N (p)) \to p \in a$
	neiptop.4	$⊢ ((φ \land p \in X) \land a \in N (p)) \to \exists b \in N (p) \forall q \in b a \in N (q)$
	neiptop.5	$⊢ (φ \land p \in X) \to X \in N (p)$
Assertion	neiptopnei	$⊢ φ \to N = (p \in X ⟼ nei (J) (\{p\}))$

Proof

Step	Hyp	Ref	Expression
1		neiptop.o	$⊢ J = \{a \in 𝒫 X \| \forall p \in a a \in N (p)\}$
2		neiptop.0	$⊢ φ \to N : X ⟶ 𝒫 𝒫 X$
3		neiptop.1	$⊢ (((φ \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \to b \in N (p)$
4		neiptop.2	$⊢ (φ \land p \in X) \to fi (N (p)) \subseteq N (p)$
5		neiptop.3	$⊢ ((φ \land p \in X) \land a \in N (p)) \to p \in a$
6		neiptop.4	$⊢ ((φ \land p \in X) \land a \in N (p)) \to \exists b \in N (p) \forall q \in b a \in N (q)$
7		neiptop.5	$⊢ (φ \land p \in X) \to X \in N (p)$
8	2	feqmptd	$⊢ φ \to N = (p \in X ⟼ N (p))$
9	2	ffvelrnda	$⊢ (φ \land p \in X) \to N (p) \in 𝒫 𝒫 X$
10	9	adantr	$⊢ ((φ \land p \in X) \land c \in N (p)) \to N (p) \in 𝒫 𝒫 X$
11	10	elpwid	$⊢ ((φ \land p \in X) \land c \in N (p)) \to N (p) \subseteq 𝒫 X$
12		simpr	$⊢ ((φ \land p \in X) \land c \in N (p)) \to c \in N (p)$
13	11 12	sseldd	$⊢ ((φ \land p \in X) \land c \in N (p)) \to c \in 𝒫 X$
14	13	elpwid	$⊢ ((φ \land p \in X) \land c \in N (p)) \to c \subseteq X$
15	1 2 3 4 5 6 7	neiptopuni	$⊢ φ \to X = ⋃ J$
16	15	adantr	$⊢ (φ \land p \in X) \to X = ⋃ J$
17	16	adantr	$⊢ ((φ \land p \in X) \land c \in N (p)) \to X = ⋃ J$
18	14 17	sseqtrd	$⊢ ((φ \land p \in X) \land c \in N (p)) \to c \subseteq ⋃ J$
19		ssrab2	$⊢ \{q \in X \| c \in N (q)\} \subseteq X$
20	19	a1i	$⊢ ((φ \land p \in X) \land c \in N (p)) \to \{q \in X \| c \in N (q)\} \subseteq X$
21		fveq2	$⊢ q = r \to N (q) = N (r)$
22	21	eleq2d	$⊢ q = r \to (c \in N (q) \leftrightarrow c \in N (r))$
23	22	elrab	$⊢ r \in \{q \in X \| c \in N (q)\} \leftrightarrow (r \in X \land c \in N (r))$
24		simp-5l	$⊢ (((((φ \land p \in X) \land c \in N (p)) \land (r \in X \land c \in N (r))) \land b \in N (r)) \land b \subseteq \{q \in X \| c \in N (q)\}) \to φ$
25		simpr1l	$⊢ (((φ \land p \in X) \land c \in N (p)) \land ((r \in X \land c \in N (r)) \land b \in N (r) \land b \subseteq \{q \in X \| c \in N (q)\})) \to r \in X$
26	25	3anassrs	$⊢ (((((φ \land p \in X) \land c \in N (p)) \land (r \in X \land c \in N (r))) \land b \in N (r)) \land b \subseteq \{q \in X \| c \in N (q)\}) \to r \in X$
27		simpr	$⊢ (((((φ \land p \in X) \land c \in N (p)) \land (r \in X \land c \in N (r))) \land b \in N (r)) \land b \subseteq \{q \in X \| c \in N (q)\}) \to b \subseteq \{q \in X \| c \in N (q)\}$
28		simplr	$⊢ (((((φ \land p \in X) \land c \in N (p)) \land (r \in X \land c \in N (r))) \land b \in N (r)) \land b \subseteq \{q \in X \| c \in N (q)\}) \to b \in N (r)$
29		sseq1	$⊢ a = b \to (a \subseteq \{q \in X \| c \in N (q)\} \leftrightarrow b \subseteq \{q \in X \| c \in N (q)\})$
30	29	3anbi2d	$⊢ a = b \to (((φ \land r \in X) \land a \subseteq \{q \in X \| c \in N (q)\} \land \{q \in X \| c \in N (q)\} \subseteq X) \leftrightarrow ((φ \land r \in X) \land b \subseteq \{q \in X \| c \in N (q)\} \land \{q \in X \| c \in N (q)\} \subseteq X))$
31		eleq1w	$⊢ a = b \to (a \in N (r) \leftrightarrow b \in N (r))$
32	30 31	anbi12d	$⊢ a = b \to ((((φ \land r \in X) \land a \subseteq \{q \in X \| c \in N (q)\} \land \{q \in X \| c \in N (q)\} \subseteq X) \land a \in N (r)) \leftrightarrow (((φ \land r \in X) \land b \subseteq \{q \in X \| c \in N (q)\} \land \{q \in X \| c \in N (q)\} \subseteq X) \land b \in N (r)))$
33	32	imbi1d	$⊢ a = b \to (((((φ \land r \in X) \land a \subseteq \{q \in X \| c \in N (q)\} \land \{q \in X \| c \in N (q)\} \subseteq X) \land a \in N (r)) \to \{q \in X \| c \in N (q)\} \in N (r)) \leftrightarrow ((((φ \land r \in X) \land b \subseteq \{q \in X \| c \in N (q)\} \land \{q \in X \| c \in N (q)\} \subseteq X) \land b \in N (r)) \to \{q \in X \| c \in N (q)\} \in N (r)))$
34		simpl1l	$⊢ (((φ \land r \in X) \land a \subseteq \{q \in X \| c \in N (q)\} \land \{q \in X \| c \in N (q)\} \subseteq X) \land a \in N (r)) \to φ$
35	1 2 3 4 5 6 7	neiptoptop	$⊢ φ \to J \in Top$
36	35	uniexd	$⊢ φ \to ⋃ J \in V$
37	15 36	eqeltrd	$⊢ φ \to X \in V$
38		rabexg	$⊢ X \in V \to \{q \in X \| c \in N (q)\} \in V$
39		sseq2	$⊢ b = \{q \in X \| c \in N (q)\} \to (a \subseteq b \leftrightarrow a \subseteq \{q \in X \| c \in N (q)\})$
40		sseq1	$⊢ b = \{q \in X \| c \in N (q)\} \to (b \subseteq X \leftrightarrow \{q \in X \| c \in N (q)\} \subseteq X)$
41	39 40	3anbi23d	$⊢ b = \{q \in X \| c \in N (q)\} \to (((φ \land r \in X) \land a \subseteq b \land b \subseteq X) \leftrightarrow ((φ \land r \in X) \land a \subseteq \{q \in X \| c \in N (q)\} \land \{q \in X \| c \in N (q)\} \subseteq X))$
42	41	anbi1d	$⊢ b = \{q \in X \| c \in N (q)\} \to ((((φ \land r \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (r)) \leftrightarrow (((φ \land r \in X) \land a \subseteq \{q \in X \| c \in N (q)\} \land \{q \in X \| c \in N (q)\} \subseteq X) \land a \in N (r)))$
43		eleq1	$⊢ b = \{q \in X \| c \in N (q)\} \to (b \in N (r) \leftrightarrow \{q \in X \| c \in N (q)\} \in N (r))$
44	42 43	imbi12d	$⊢ b = \{q \in X \| c \in N (q)\} \to (((((φ \land r \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (r)) \to b \in N (r)) \leftrightarrow ((((φ \land r \in X) \land a \subseteq \{q \in X \| c \in N (q)\} \land \{q \in X \| c \in N (q)\} \subseteq X) \land a \in N (r)) \to \{q \in X \| c \in N (q)\} \in N (r)))$
45		eleq1w	$⊢ p = r \to (p \in X \leftrightarrow r \in X)$
46	45	anbi2d	$⊢ p = r \to ((φ \land p \in X) \leftrightarrow (φ \land r \in X))$
47	46	3anbi1d	$⊢ p = r \to (((φ \land p \in X) \land a \subseteq b \land b \subseteq X) \leftrightarrow ((φ \land r \in X) \land a \subseteq b \land b \subseteq X))$
48		fveq2	$⊢ p = r \to N (p) = N (r)$
49	48	eleq2d	$⊢ p = r \to (a \in N (p) \leftrightarrow a \in N (r))$
50	47 49	anbi12d	$⊢ p = r \to ((((φ \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \leftrightarrow (((φ \land r \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (r)))$
51	48	eleq2d	$⊢ p = r \to (b \in N (p) \leftrightarrow b \in N (r))$
52	50 51	imbi12d	$⊢ p = r \to (((((φ \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \to b \in N (p)) \leftrightarrow ((((φ \land r \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (r)) \to b \in N (r)))$
53	52 3	chvarvv	$⊢ (((φ \land r \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (r)) \to b \in N (r)$
54	44 53	vtoclg	$⊢ \{q \in X \| c \in N (q)\} \in V \to ((((φ \land r \in X) \land a \subseteq \{q \in X \| c \in N (q)\} \land \{q \in X \| c \in N (q)\} \subseteq X) \land a \in N (r)) \to \{q \in X \| c \in N (q)\} \in N (r))$
55	37 38 54	3syl	$⊢ φ \to ((((φ \land r \in X) \land a \subseteq \{q \in X \| c \in N (q)\} \land \{q \in X \| c \in N (q)\} \subseteq X) \land a \in N (r)) \to \{q \in X \| c \in N (q)\} \in N (r))$
56	34 55	mpcom	$⊢ (((φ \land r \in X) \land a \subseteq \{q \in X \| c \in N (q)\} \land \{q \in X \| c \in N (q)\} \subseteq X) \land a \in N (r)) \to \{q \in X \| c \in N (q)\} \in N (r)$
57	33 56	chvarvv	$⊢ (((φ \land r \in X) \land b \subseteq \{q \in X \| c \in N (q)\} \land \{q \in X \| c \in N (q)\} \subseteq X) \land b \in N (r)) \to \{q \in X \| c \in N (q)\} \in N (r)$
58	57	3an1rs	$⊢ (((φ \land r \in X) \land b \subseteq \{q \in X \| c \in N (q)\} \land b \in N (r)) \land \{q \in X \| c \in N (q)\} \subseteq X) \to \{q \in X \| c \in N (q)\} \in N (r)$
59	19 58	mpan2	$⊢ ((φ \land r \in X) \land b \subseteq \{q \in X \| c \in N (q)\} \land b \in N (r)) \to \{q \in X \| c \in N (q)\} \in N (r)$
60	24 26 27 28 59	syl211anc	$⊢ (((((φ \land p \in X) \land c \in N (p)) \land (r \in X \land c \in N (r))) \land b \in N (r)) \land b \subseteq \{q \in X \| c \in N (q)\}) \to \{q \in X \| c \in N (q)\} \in N (r)$
61		simplll	$⊢ (((φ \land p \in X) \land c \in N (p)) \land (r \in X \land c \in N (r))) \to φ$
62		simprl	$⊢ (((φ \land p \in X) \land c \in N (p)) \land (r \in X \land c \in N (r))) \to r \in X$
63		simprr	$⊢ (((φ \land p \in X) \land c \in N (p)) \land (r \in X \land c \in N (r))) \to c \in N (r)$
64	48	eleq2d	$⊢ p = r \to (c \in N (p) \leftrightarrow c \in N (r))$
65	46 64	anbi12d	$⊢ p = r \to (((φ \land p \in X) \land c \in N (p)) \leftrightarrow ((φ \land r \in X) \land c \in N (r)))$
66		fveq2	$⊢ q = s \to N (q) = N (s)$
67	66	eleq2d	$⊢ q = s \to (c \in N (q) \leftrightarrow c \in N (s))$
68	67	cbvralvw	$⊢ \forall q \in b c \in N (q) \leftrightarrow \forall s \in b c \in N (s)$
69	68	a1i	$⊢ p = r \to (\forall q \in b c \in N (q) \leftrightarrow \forall s \in b c \in N (s))$
70	48 69	rexeqbidv	$⊢ p = r \to (\exists b \in N (p) \forall q \in b c \in N (q) \leftrightarrow \exists b \in N (r) \forall s \in b c \in N (s))$
71	65 70	imbi12d	$⊢ p = r \to ((((φ \land p \in X) \land c \in N (p)) \to \exists b \in N (p) \forall q \in b c \in N (q)) \leftrightarrow (((φ \land r \in X) \land c \in N (r)) \to \exists b \in N (r) \forall s \in b c \in N (s)))$
72		eleq1w	$⊢ a = c \to (a \in N (p) \leftrightarrow c \in N (p))$
73	72	anbi2d	$⊢ a = c \to (((φ \land p \in X) \land a \in N (p)) \leftrightarrow ((φ \land p \in X) \land c \in N (p)))$
74		eleq1w	$⊢ a = c \to (a \in N (q) \leftrightarrow c \in N (q))$
75	74	rexralbidv	$⊢ a = c \to (\exists b \in N (p) \forall q \in b a \in N (q) \leftrightarrow \exists b \in N (p) \forall q \in b c \in N (q))$
76	73 75	imbi12d	$⊢ a = c \to ((((φ \land p \in X) \land a \in N (p)) \to \exists b \in N (p) \forall q \in b a \in N (q)) \leftrightarrow (((φ \land p \in X) \land c \in N (p)) \to \exists b \in N (p) \forall q \in b c \in N (q)))$
77	76 6	chvarvv	$⊢ ((φ \land p \in X) \land c \in N (p)) \to \exists b \in N (p) \forall q \in b c \in N (q)$
78	71 77	chvarvv	$⊢ ((φ \land r \in X) \land c \in N (r)) \to \exists b \in N (r) \forall s \in b c \in N (s)$
79	2	ffvelrnda	$⊢ (φ \land r \in X) \to N (r) \in 𝒫 𝒫 X$
80	79	elpwid	$⊢ (φ \land r \in X) \to N (r) \subseteq 𝒫 X$
81	80	sselda	$⊢ ((φ \land r \in X) \land b \in N (r)) \to b \in 𝒫 X$
82	81	elpwid	$⊢ ((φ \land r \in X) \land b \in N (r)) \to b \subseteq X$
83	82	sselda	$⊢ (((φ \land r \in X) \land b \in N (r)) \land s \in b) \to s \in X$
84	83	a1d	$⊢ (((φ \land r \in X) \land b \in N (r)) \land s \in b) \to (c \in N (s) \to s \in X)$
85	84	ancrd	$⊢ (((φ \land r \in X) \land b \in N (r)) \land s \in b) \to (c \in N (s) \to (s \in X \land c \in N (s)))$
86	85	ralimdva	$⊢ ((φ \land r \in X) \land b \in N (r)) \to (\forall s \in b c \in N (s) \to \forall s \in b (s \in X \land c \in N (s)))$
87	86	reximdva	$⊢ (φ \land r \in X) \to (\exists b \in N (r) \forall s \in b c \in N (s) \to \exists b \in N (r) \forall s \in b (s \in X \land c \in N (s)))$
88	87	adantr	$⊢ ((φ \land r \in X) \land c \in N (r)) \to (\exists b \in N (r) \forall s \in b c \in N (s) \to \exists b \in N (r) \forall s \in b (s \in X \land c \in N (s)))$
89	78 88	mpd	$⊢ ((φ \land r \in X) \land c \in N (r)) \to \exists b \in N (r) \forall s \in b (s \in X \land c \in N (s))$
90	67	elrab	$⊢ s \in \{q \in X \| c \in N (q)\} \leftrightarrow (s \in X \land c \in N (s))$
91	90	ralbii	$⊢ \forall s \in b s \in \{q \in X \| c \in N (q)\} \leftrightarrow \forall s \in b (s \in X \land c \in N (s))$
92	91	rexbii	$⊢ \exists b \in N (r) \forall s \in b s \in \{q \in X \| c \in N (q)\} \leftrightarrow \exists b \in N (r) \forall s \in b (s \in X \land c \in N (s))$
93	89 92	sylibr	$⊢ ((φ \land r \in X) \land c \in N (r)) \to \exists b \in N (r) \forall s \in b s \in \{q \in X \| c \in N (q)\}$
94		dfss3	$⊢ b \subseteq \{q \in X \| c \in N (q)\} \leftrightarrow \forall s \in b s \in \{q \in X \| c \in N (q)\}$
95	94	biimpri	$⊢ \forall s \in b s \in \{q \in X \| c \in N (q)\} \to b \subseteq \{q \in X \| c \in N (q)\}$
96	95	reximi	$⊢ \exists b \in N (r) \forall s \in b s \in \{q \in X \| c \in N (q)\} \to \exists b \in N (r) b \subseteq \{q \in X \| c \in N (q)\}$
97	93 96	syl	$⊢ ((φ \land r \in X) \land c \in N (r)) \to \exists b \in N (r) b \subseteq \{q \in X \| c \in N (q)\}$
98	61 62 63 97	syl21anc	$⊢ (((φ \land p \in X) \land c \in N (p)) \land (r \in X \land c \in N (r))) \to \exists b \in N (r) b \subseteq \{q \in X \| c \in N (q)\}$
99	60 98	r19.29a	$⊢ (((φ \land p \in X) \land c \in N (p)) \land (r \in X \land c \in N (r))) \to \{q \in X \| c \in N (q)\} \in N (r)$
100	23 99	sylan2b	$⊢ (((φ \land p \in X) \land c \in N (p)) \land r \in \{q \in X \| c \in N (q)\}) \to \{q \in X \| c \in N (q)\} \in N (r)$
101	100	ralrimiva	$⊢ ((φ \land p \in X) \land c \in N (p)) \to \forall r \in \{q \in X \| c \in N (q)\} \{q \in X \| c \in N (q)\} \in N (r)$
102	48	eleq2d	$⊢ p = r \to (\{q \in X \| c \in N (q)\} \in N (p) \leftrightarrow \{q \in X \| c \in N (q)\} \in N (r))$
103	102	cbvralvw	$⊢ \forall p \in \{q \in X \| c \in N (q)\} \{q \in X \| c \in N (q)\} \in N (p) \leftrightarrow \forall r \in \{q \in X \| c \in N (q)\} \{q \in X \| c \in N (q)\} \in N (r)$
104	101 103	sylibr	$⊢ ((φ \land p \in X) \land c \in N (p)) \to \forall p \in \{q \in X \| c \in N (q)\} \{q \in X \| c \in N (q)\} \in N (p)$
105	1	neipeltop	$⊢ \{q \in X \| c \in N (q)\} \in J \leftrightarrow (\{q \in X \| c \in N (q)\} \subseteq X \land \forall p \in \{q \in X \| c \in N (q)\} \{q \in X \| c \in N (q)\} \in N (p))$
106	20 104 105	sylanbrc	$⊢ ((φ \land p \in X) \land c \in N (p)) \to \{q \in X \| c \in N (q)\} \in J$
107		simpr	$⊢ (φ \land p \in X) \to p \in X$
108	107	anim1i	$⊢ ((φ \land p \in X) \land c \in N (p)) \to (p \in X \land c \in N (p))$
109		fveq2	$⊢ q = p \to N (q) = N (p)$
110	109	eleq2d	$⊢ q = p \to (c \in N (q) \leftrightarrow c \in N (p))$
111	110	elrab	$⊢ p \in \{q \in X \| c \in N (q)\} \leftrightarrow (p \in X \land c \in N (p))$
112	108 111	sylibr	$⊢ ((φ \land p \in X) \land c \in N (p)) \to p \in \{q \in X \| c \in N (q)\}$
113		nfv	$⊢ Ⅎ q ((φ \land p \in X) \land c \in N (p))$
114		nfrab1	$⊢ \underline{Ⅎ} q \{q \in X \| c \in N (q)\}$
115		nfcv	$⊢ \underline{Ⅎ} q c$
116		rabid	$⊢ q \in \{q \in X \| c \in N (q)\} \leftrightarrow (q \in X \land c \in N (q))$
117		simplll	$⊢ (((φ \land p \in X) \land c \in N (p)) \land (q \in X \land c \in N (q))) \to φ$
118		simprl	$⊢ (((φ \land p \in X) \land c \in N (p)) \land (q \in X \land c \in N (q))) \to q \in X$
119		simprr	$⊢ (((φ \land p \in X) \land c \in N (p)) \land (q \in X \land c \in N (q))) \to c \in N (q)$
120		eleq1w	$⊢ p = q \to (p \in X \leftrightarrow q \in X)$
121	120	anbi2d	$⊢ p = q \to ((φ \land p \in X) \leftrightarrow (φ \land q \in X))$
122		fveq2	$⊢ p = q \to N (p) = N (q)$
123	122	eleq2d	$⊢ p = q \to (c \in N (p) \leftrightarrow c \in N (q))$
124	121 123	anbi12d	$⊢ p = q \to (((φ \land p \in X) \land c \in N (p)) \leftrightarrow ((φ \land q \in X) \land c \in N (q)))$
125		elequ1	$⊢ p = q \to (p \in c \leftrightarrow q \in c)$
126	124 125	imbi12d	$⊢ p = q \to ((((φ \land p \in X) \land c \in N (p)) \to p \in c) \leftrightarrow (((φ \land q \in X) \land c \in N (q)) \to q \in c))$
127		elequ2	$⊢ a = c \to (p \in a \leftrightarrow p \in c)$
128	73 127	imbi12d	$⊢ a = c \to ((((φ \land p \in X) \land a \in N (p)) \to p \in a) \leftrightarrow (((φ \land p \in X) \land c \in N (p)) \to p \in c))$
129	128 5	chvarvv	$⊢ ((φ \land p \in X) \land c \in N (p)) \to p \in c$
130	126 129	chvarvv	$⊢ ((φ \land q \in X) \land c \in N (q)) \to q \in c$
131	117 118 119 130	syl21anc	$⊢ (((φ \land p \in X) \land c \in N (p)) \land (q \in X \land c \in N (q))) \to q \in c$
132	131	ex	$⊢ ((φ \land p \in X) \land c \in N (p)) \to ((q \in X \land c \in N (q)) \to q \in c)$
133	116 132	syl5bi	$⊢ ((φ \land p \in X) \land c \in N (p)) \to (q \in \{q \in X \| c \in N (q)\} \to q \in c)$
134	113 114 115 133	ssrd	$⊢ ((φ \land p \in X) \land c \in N (p)) \to \{q \in X \| c \in N (q)\} \subseteq c$
135		eleq2	$⊢ d = \{q \in X \| c \in N (q)\} \to (p \in d \leftrightarrow p \in \{q \in X \| c \in N (q)\})$
136		sseq1	$⊢ d = \{q \in X \| c \in N (q)\} \to (d \subseteq c \leftrightarrow \{q \in X \| c \in N (q)\} \subseteq c)$
137	135 136	anbi12d	$⊢ d = \{q \in X \| c \in N (q)\} \to ((p \in d \land d \subseteq c) \leftrightarrow (p \in \{q \in X \| c \in N (q)\} \land \{q \in X \| c \in N (q)\} \subseteq c))$
138	137	rspcev	$⊢ (\{q \in X \| c \in N (q)\} \in J \land (p \in \{q \in X \| c \in N (q)\} \land \{q \in X \| c \in N (q)\} \subseteq c)) \to \exists d \in J (p \in d \land d \subseteq c)$
139	106 112 134 138	syl12anc	$⊢ ((φ \land p \in X) \land c \in N (p)) \to \exists d \in J (p \in d \land d \subseteq c)$
140	18 139	jca	$⊢ ((φ \land p \in X) \land c \in N (p)) \to (c \subseteq ⋃ J \land \exists d \in J (p \in d \land d \subseteq c))$
141		nfv	$⊢ Ⅎ d (φ \land p \in X)$
142		nfv	$⊢ Ⅎ d c \subseteq ⋃ J$
143		nfre1	$⊢ Ⅎ d \exists d \in J (p \in d \land d \subseteq c)$
144	142 143	nfan	$⊢ Ⅎ d (c \subseteq ⋃ J \land \exists d \in J (p \in d \land d \subseteq c))$
145	141 144	nfan	$⊢ Ⅎ d ((φ \land p \in X) \land (c \subseteq ⋃ J \land \exists d \in J (p \in d \land d \subseteq c)))$
146		simplll	$⊢ ((((φ \land p \in X) \land (c \subseteq ⋃ J \land \exists d \in J (p \in d \land d \subseteq c))) \land d \in N (p)) \land d \subseteq c) \to (φ \land p \in X)$
147		simpr	$⊢ ((((φ \land p \in X) \land (c \subseteq ⋃ J \land \exists d \in J (p \in d \land d \subseteq c))) \land d \in N (p)) \land d \subseteq c) \to d \subseteq c$
148		simpr1l	$⊢ ((φ \land p \in X) \land ((c \subseteq ⋃ J \land \exists d \in J (p \in d \land d \subseteq c)) \land d \in N (p) \land d \subseteq c)) \to c \subseteq ⋃ J$
149	148	3anassrs	$⊢ ((((φ \land p \in X) \land (c \subseteq ⋃ J \land \exists d \in J (p \in d \land d \subseteq c))) \land d \in N (p)) \land d \subseteq c) \to c \subseteq ⋃ J$
150	146 16	syl	$⊢ ((((φ \land p \in X) \land (c \subseteq ⋃ J \land \exists d \in J (p \in d \land d \subseteq c))) \land d \in N (p)) \land d \subseteq c) \to X = ⋃ J$
151	149 150	sseqtrrd	$⊢ ((((φ \land p \in X) \land (c \subseteq ⋃ J \land \exists d \in J (p \in d \land d \subseteq c))) \land d \in N (p)) \land d \subseteq c) \to c \subseteq X$
152		simplr	$⊢ ((((φ \land p \in X) \land (c \subseteq ⋃ J \land \exists d \in J (p \in d \land d \subseteq c))) \land d \in N (p)) \land d \subseteq c) \to d \in N (p)$
153		sseq1	$⊢ a = d \to (a \subseteq c \leftrightarrow d \subseteq c)$
154	153	3anbi2d	$⊢ a = d \to (((φ \land p \in X) \land a \subseteq c \land c \subseteq X) \leftrightarrow ((φ \land p \in X) \land d \subseteq c \land c \subseteq X))$
155		eleq1w	$⊢ a = d \to (a \in N (p) \leftrightarrow d \in N (p))$
156	154 155	anbi12d	$⊢ a = d \to ((((φ \land p \in X) \land a \subseteq c \land c \subseteq X) \land a \in N (p)) \leftrightarrow (((φ \land p \in X) \land d \subseteq c \land c \subseteq X) \land d \in N (p)))$
157	156	imbi1d	$⊢ a = d \to (((((φ \land p \in X) \land a \subseteq c \land c \subseteq X) \land a \in N (p)) \to c \in N (p)) \leftrightarrow ((((φ \land p \in X) \land d \subseteq c \land c \subseteq X) \land d \in N (p)) \to c \in N (p)))$
158		sseq2	$⊢ b = c \to (a \subseteq b \leftrightarrow a \subseteq c)$
159		sseq1	$⊢ b = c \to (b \subseteq X \leftrightarrow c \subseteq X)$
160	158 159	3anbi23d	$⊢ b = c \to (((φ \land p \in X) \land a \subseteq b \land b \subseteq X) \leftrightarrow ((φ \land p \in X) \land a \subseteq c \land c \subseteq X))$
161	160	anbi1d	$⊢ b = c \to ((((φ \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \leftrightarrow (((φ \land p \in X) \land a \subseteq c \land c \subseteq X) \land a \in N (p)))$
162		eleq1w	$⊢ b = c \to (b \in N (p) \leftrightarrow c \in N (p))$
163	161 162	imbi12d	$⊢ b = c \to (((((φ \land p \in X) \land a \subseteq b \land b \subseteq X) \land a \in N (p)) \to b \in N (p)) \leftrightarrow ((((φ \land p \in X) \land a \subseteq c \land c \subseteq X) \land a \in N (p)) \to c \in N (p)))$
164	163 3	chvarvv	$⊢ (((φ \land p \in X) \land a \subseteq c \land c \subseteq X) \land a \in N (p)) \to c \in N (p)$
165	157 164	chvarvv	$⊢ (((φ \land p \in X) \land d \subseteq c \land c \subseteq X) \land d \in N (p)) \to c \in N (p)$
166	146 147 151 152 165	syl31anc	$⊢ ((((φ \land p \in X) \land (c \subseteq ⋃ J \land \exists d \in J (p \in d \land d \subseteq c))) \land d \in N (p)) \land d \subseteq c) \to c \in N (p)$
167	1	neipeltop	$⊢ d \in J \leftrightarrow (d \subseteq X \land \forall p \in d d \in N (p))$
168	167	simprbi	$⊢ d \in J \to \forall p \in d d \in N (p)$
169	168	r19.21bi	$⊢ (d \in J \land p \in d) \to d \in N (p)$
170	169	anim1i	$⊢ ((d \in J \land p \in d) \land d \subseteq c) \to (d \in N (p) \land d \subseteq c)$
171	170	anasss	$⊢ (d \in J \land (p \in d \land d \subseteq c)) \to (d \in N (p) \land d \subseteq c)$
172	171	reximi2	$⊢ \exists d \in J (p \in d \land d \subseteq c) \to \exists d \in N (p) d \subseteq c$
173	172	ad2antll	$⊢ ((φ \land p \in X) \land (c \subseteq ⋃ J \land \exists d \in J (p \in d \land d \subseteq c))) \to \exists d \in N (p) d \subseteq c$
174	145 166 173	r19.29af	$⊢ ((φ \land p \in X) \land (c \subseteq ⋃ J \land \exists d \in J (p \in d \land d \subseteq c))) \to c \in N (p)$
175	140 174	impbida	$⊢ (φ \land p \in X) \to (c \in N (p) \leftrightarrow (c \subseteq ⋃ J \land \exists d \in J (p \in d \land d \subseteq c)))$
176	107 16	eleqtrd	$⊢ (φ \land p \in X) \to p \in ⋃ J$
177		eqid	$⊢ ⋃ J = ⋃ J$
178	177	isneip	$⊢ (J \in Top \land p \in ⋃ J) \to (c \in nei (J) (\{p\}) \leftrightarrow (c \subseteq ⋃ J \land \exists d \in J (p \in d \land d \subseteq c)))$
179	35 176 178	syl2an2r	$⊢ (φ \land p \in X) \to (c \in nei (J) (\{p\}) \leftrightarrow (c \subseteq ⋃ J \land \exists d \in J (p \in d \land d \subseteq c)))$
180	175 179	bitr4d	$⊢ (φ \land p \in X) \to (c \in N (p) \leftrightarrow c \in nei (J) (\{p\}))$
181	180	eqrdv	$⊢ (φ \land p \in X) \to N (p) = nei (J) (\{p\})$
182	181	mpteq2dva	$⊢ φ \to (p \in X ⟼ N (p)) = (p \in X ⟼ nei (J) (\{p\}))$
183	8 182	eqtrd	$⊢ φ \to N = (p \in X ⟼ nei (J) (\{p\}))$

Metamath Proof Explorer

Theorem neiptopnei

Proof