neibastop1

Description: A collection of neighborhood bases determines a topology. Part of Theorem 4.5 of Stephen Willard'sGeneral Topology. (Contributed by Jeff Hankins, 8-Sep-2009) (Proof shortened by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Hypotheses	neibastop1.1	$⊢ φ \to X \in V$
	neibastop1.2	$⊢ φ \to F : X ⟶ 𝒫 𝒫 X ∖ \{\emptyset\}$
	neibastop1.3	$⊢ (φ \land (x \in X \land v \in F (x) \land w \in F (x))) \to F (x) \cap 𝒫 (v \cap w) \neq \emptyset$
	neibastop1.4	$⊢ J = \{o \in 𝒫 X \| \forall x \in o F (x) \cap 𝒫 o \neq \emptyset\}$
Assertion	neibastop1	$⊢ φ \to J \in TopOn (X)$

Proof

Step	Hyp	Ref	Expression
1		neibastop1.1	$⊢ φ \to X \in V$
2		neibastop1.2	$⊢ φ \to F : X ⟶ 𝒫 𝒫 X ∖ \{\emptyset\}$
3		neibastop1.3	$⊢ (φ \land (x \in X \land v \in F (x) \land w \in F (x))) \to F (x) \cap 𝒫 (v \cap w) \neq \emptyset$
4		neibastop1.4	$⊢ J = \{o \in 𝒫 X \| \forall x \in o F (x) \cap 𝒫 o \neq \emptyset\}$
5		simpr	$⊢ (φ \land y \subseteq J) \to y \subseteq J$
6		ssrab2	$⊢ \{o \in 𝒫 X \| \forall x \in o F (x) \cap 𝒫 o \neq \emptyset\} \subseteq 𝒫 X$
7	4 6	eqsstri	$⊢ J \subseteq 𝒫 X$
8	5 7	sstrdi	$⊢ (φ \land y \subseteq J) \to y \subseteq 𝒫 X$
9		sspwuni	$⊢ y \subseteq 𝒫 X \leftrightarrow ⋃ y \subseteq X$
10	8 9	sylib	$⊢ (φ \land y \subseteq J) \to ⋃ y \subseteq X$
11		vuniex	$⊢ ⋃ y \in V$
12	11	elpw	$⊢ ⋃ y \in 𝒫 X \leftrightarrow ⋃ y \subseteq X$
13	10 12	sylibr	$⊢ (φ \land y \subseteq J) \to ⋃ y \in 𝒫 X$
14		eluni2	$⊢ x \in ⋃ y \leftrightarrow \exists z \in y x \in z$
15		elssuni	$⊢ z \in y \to z \subseteq ⋃ y$
16	15	ad2antrl	$⊢ ((φ \land y \subseteq J) \land (z \in y \land x \in z)) \to z \subseteq ⋃ y$
17	16	sspwd	$⊢ ((φ \land y \subseteq J) \land (z \in y \land x \in z)) \to 𝒫 z \subseteq 𝒫 ⋃ y$
18		sslin	$⊢ 𝒫 z \subseteq 𝒫 ⋃ y \to F (x) \cap 𝒫 z \subseteq F (x) \cap 𝒫 ⋃ y$
19	17 18	syl	$⊢ ((φ \land y \subseteq J) \land (z \in y \land x \in z)) \to F (x) \cap 𝒫 z \subseteq F (x) \cap 𝒫 ⋃ y$
20	5	sselda	$⊢ ((φ \land y \subseteq J) \land z \in y) \to z \in J$
21	20	adantrr	$⊢ ((φ \land y \subseteq J) \land (z \in y \land x \in z)) \to z \in J$
22		pweq	$⊢ o = z \to 𝒫 o = 𝒫 z$
23	22	ineq2d	$⊢ o = z \to F (x) \cap 𝒫 o = F (x) \cap 𝒫 z$
24	23	neeq1d	$⊢ o = z \to (F (x) \cap 𝒫 o \neq \emptyset \leftrightarrow F (x) \cap 𝒫 z \neq \emptyset)$
25	24	raleqbi1dv	$⊢ o = z \to (\forall x \in o F (x) \cap 𝒫 o \neq \emptyset \leftrightarrow \forall x \in z F (x) \cap 𝒫 z \neq \emptyset)$
26	25 4	elrab2	$⊢ z \in J \leftrightarrow (z \in 𝒫 X \land \forall x \in z F (x) \cap 𝒫 z \neq \emptyset)$
27	26	simprbi	$⊢ z \in J \to \forall x \in z F (x) \cap 𝒫 z \neq \emptyset$
28	21 27	syl	$⊢ ((φ \land y \subseteq J) \land (z \in y \land x \in z)) \to \forall x \in z F (x) \cap 𝒫 z \neq \emptyset$
29		simprr	$⊢ ((φ \land y \subseteq J) \land (z \in y \land x \in z)) \to x \in z$
30		rsp	$⊢ \forall x \in z F (x) \cap 𝒫 z \neq \emptyset \to (x \in z \to F (x) \cap 𝒫 z \neq \emptyset)$
31	28 29 30	sylc	$⊢ ((φ \land y \subseteq J) \land (z \in y \land x \in z)) \to F (x) \cap 𝒫 z \neq \emptyset$
32		ssn0	$⊢ (F (x) \cap 𝒫 z \subseteq F (x) \cap 𝒫 ⋃ y \land F (x) \cap 𝒫 z \neq \emptyset) \to F (x) \cap 𝒫 ⋃ y \neq \emptyset$
33	19 31 32	syl2anc	$⊢ ((φ \land y \subseteq J) \land (z \in y \land x \in z)) \to F (x) \cap 𝒫 ⋃ y \neq \emptyset$
34	33	rexlimdvaa	$⊢ (φ \land y \subseteq J) \to (\exists z \in y x \in z \to F (x) \cap 𝒫 ⋃ y \neq \emptyset)$
35	14 34	syl5bi	$⊢ (φ \land y \subseteq J) \to (x \in ⋃ y \to F (x) \cap 𝒫 ⋃ y \neq \emptyset)$
36	35	ralrimiv	$⊢ (φ \land y \subseteq J) \to \forall x \in ⋃ y F (x) \cap 𝒫 ⋃ y \neq \emptyset$
37		pweq	$⊢ o = ⋃ y \to 𝒫 o = 𝒫 ⋃ y$
38	37	ineq2d	$⊢ o = ⋃ y \to F (x) \cap 𝒫 o = F (x) \cap 𝒫 ⋃ y$
39	38	neeq1d	$⊢ o = ⋃ y \to (F (x) \cap 𝒫 o \neq \emptyset \leftrightarrow F (x) \cap 𝒫 ⋃ y \neq \emptyset)$
40	39	raleqbi1dv	$⊢ o = ⋃ y \to (\forall x \in o F (x) \cap 𝒫 o \neq \emptyset \leftrightarrow \forall x \in ⋃ y F (x) \cap 𝒫 ⋃ y \neq \emptyset)$
41	40 4	elrab2	$⊢ ⋃ y \in J \leftrightarrow (⋃ y \in 𝒫 X \land \forall x \in ⋃ y F (x) \cap 𝒫 ⋃ y \neq \emptyset)$
42	13 36 41	sylanbrc	$⊢ (φ \land y \subseteq J) \to ⋃ y \in J$
43	42	ex	$⊢ φ \to (y \subseteq J \to ⋃ y \in J)$
44	43	alrimiv	$⊢ φ \to \forall y (y \subseteq J \to ⋃ y \in J)$
45		pweq	$⊢ o = y \to 𝒫 o = 𝒫 y$
46	45	ineq2d	$⊢ o = y \to F (x) \cap 𝒫 o = F (x) \cap 𝒫 y$
47	46	neeq1d	$⊢ o = y \to (F (x) \cap 𝒫 o \neq \emptyset \leftrightarrow F (x) \cap 𝒫 y \neq \emptyset)$
48	47	raleqbi1dv	$⊢ o = y \to (\forall x \in o F (x) \cap 𝒫 o \neq \emptyset \leftrightarrow \forall x \in y F (x) \cap 𝒫 y \neq \emptyset)$
49	48 4	elrab2	$⊢ y \in J \leftrightarrow (y \in 𝒫 X \land \forall x \in y F (x) \cap 𝒫 y \neq \emptyset)$
50	49 26	anbi12i	$⊢ (y \in J \land z \in J) \leftrightarrow ((y \in 𝒫 X \land \forall x \in y F (x) \cap 𝒫 y \neq \emptyset) \land (z \in 𝒫 X \land \forall x \in z F (x) \cap 𝒫 z \neq \emptyset))$
51		an4	$⊢ ((y \in 𝒫 X \land \forall x \in y F (x) \cap 𝒫 y \neq \emptyset) \land (z \in 𝒫 X \land \forall x \in z F (x) \cap 𝒫 z \neq \emptyset)) \leftrightarrow ((y \in 𝒫 X \land z \in 𝒫 X) \land (\forall x \in y F (x) \cap 𝒫 y \neq \emptyset \land \forall x \in z F (x) \cap 𝒫 z \neq \emptyset))$
52	50 51	bitri	$⊢ (y \in J \land z \in J) \leftrightarrow ((y \in 𝒫 X \land z \in 𝒫 X) \land (\forall x \in y F (x) \cap 𝒫 y \neq \emptyset \land \forall x \in z F (x) \cap 𝒫 z \neq \emptyset))$
53		inss1	$⊢ y \cap z \subseteq y$
54		elpwi	$⊢ y \in 𝒫 X \to y \subseteq X$
55	53 54	sstrid	$⊢ y \in 𝒫 X \to y \cap z \subseteq X$
56	55	ad2antrl	$⊢ (φ \land (y \in 𝒫 X \land z \in 𝒫 X)) \to y \cap z \subseteq X$
57	56	adantrr	$⊢ (φ \land ((y \in 𝒫 X \land z \in 𝒫 X) \land (\forall x \in y F (x) \cap 𝒫 y \neq \emptyset \land \forall x \in z F (x) \cap 𝒫 z \neq \emptyset))) \to y \cap z \subseteq X$
58		vex	$⊢ y \in V$
59	58	inex1	$⊢ y \cap z \in V$
60	59	elpw	$⊢ y \cap z \in 𝒫 X \leftrightarrow y \cap z \subseteq X$
61	57 60	sylibr	$⊢ (φ \land ((y \in 𝒫 X \land z \in 𝒫 X) \land (\forall x \in y F (x) \cap 𝒫 y \neq \emptyset \land \forall x \in z F (x) \cap 𝒫 z \neq \emptyset))) \to y \cap z \in 𝒫 X$
62		ssralv	$⊢ y \cap z \subseteq y \to (\forall x \in y F (x) \cap 𝒫 y \neq \emptyset \to \forall x \in (y \cap z) F (x) \cap 𝒫 y \neq \emptyset)$
63	53 62	ax-mp	$⊢ \forall x \in y F (x) \cap 𝒫 y \neq \emptyset \to \forall x \in (y \cap z) F (x) \cap 𝒫 y \neq \emptyset$
64		inss2	$⊢ y \cap z \subseteq z$
65		ssralv	$⊢ y \cap z \subseteq z \to (\forall x \in z F (x) \cap 𝒫 z \neq \emptyset \to \forall x \in (y \cap z) F (x) \cap 𝒫 z \neq \emptyset)$
66	64 65	ax-mp	$⊢ \forall x \in z F (x) \cap 𝒫 z \neq \emptyset \to \forall x \in (y \cap z) F (x) \cap 𝒫 z \neq \emptyset$
67	63 66	anim12i	$⊢ (\forall x \in y F (x) \cap 𝒫 y \neq \emptyset \land \forall x \in z F (x) \cap 𝒫 z \neq \emptyset) \to (\forall x \in (y \cap z) F (x) \cap 𝒫 y \neq \emptyset \land \forall x \in (y \cap z) F (x) \cap 𝒫 z \neq \emptyset)$
68		r19.26	$⊢ \forall x \in (y \cap z) (F (x) \cap 𝒫 y \neq \emptyset \land F (x) \cap 𝒫 z \neq \emptyset) \leftrightarrow (\forall x \in (y \cap z) F (x) \cap 𝒫 y \neq \emptyset \land \forall x \in (y \cap z) F (x) \cap 𝒫 z \neq \emptyset)$
69	67 68	sylibr	$⊢ (\forall x \in y F (x) \cap 𝒫 y \neq \emptyset \land \forall x \in z F (x) \cap 𝒫 z \neq \emptyset) \to \forall x \in (y \cap z) (F (x) \cap 𝒫 y \neq \emptyset \land F (x) \cap 𝒫 z \neq \emptyset)$
70		n0	$⊢ F (x) \cap 𝒫 y \neq \emptyset \leftrightarrow \exists v v \in (F (x) \cap 𝒫 y)$
71		n0	$⊢ F (x) \cap 𝒫 z \neq \emptyset \leftrightarrow \exists w w \in (F (x) \cap 𝒫 z)$
72	70 71	anbi12i	$⊢ (F (x) \cap 𝒫 y \neq \emptyset \land F (x) \cap 𝒫 z \neq \emptyset) \leftrightarrow (\exists v v \in (F (x) \cap 𝒫 y) \land \exists w w \in (F (x) \cap 𝒫 z))$
73		exdistrv	$⊢ \exists v \exists w (v \in (F (x) \cap 𝒫 y) \land w \in (F (x) \cap 𝒫 z)) \leftrightarrow (\exists v v \in (F (x) \cap 𝒫 y) \land \exists w w \in (F (x) \cap 𝒫 z))$
74		inss2	$⊢ F (x) \cap 𝒫 y \subseteq 𝒫 y$
75		simprl	$⊢ (((φ \land (y \in 𝒫 X \land z \in 𝒫 X)) \land x \in (y \cap z)) \land (v \in (F (x) \cap 𝒫 y) \land w \in (F (x) \cap 𝒫 z))) \to v \in (F (x) \cap 𝒫 y)$
76	74 75	sselid	$⊢ (((φ \land (y \in 𝒫 X \land z \in 𝒫 X)) \land x \in (y \cap z)) \land (v \in (F (x) \cap 𝒫 y) \land w \in (F (x) \cap 𝒫 z))) \to v \in 𝒫 y$
77	76	elpwid	$⊢ (((φ \land (y \in 𝒫 X \land z \in 𝒫 X)) \land x \in (y \cap z)) \land (v \in (F (x) \cap 𝒫 y) \land w \in (F (x) \cap 𝒫 z))) \to v \subseteq y$
78		inss2	$⊢ F (x) \cap 𝒫 z \subseteq 𝒫 z$
79		simprr	$⊢ (((φ \land (y \in 𝒫 X \land z \in 𝒫 X)) \land x \in (y \cap z)) \land (v \in (F (x) \cap 𝒫 y) \land w \in (F (x) \cap 𝒫 z))) \to w \in (F (x) \cap 𝒫 z)$
80	78 79	sselid	$⊢ (((φ \land (y \in 𝒫 X \land z \in 𝒫 X)) \land x \in (y \cap z)) \land (v \in (F (x) \cap 𝒫 y) \land w \in (F (x) \cap 𝒫 z))) \to w \in 𝒫 z$
81	80	elpwid	$⊢ (((φ \land (y \in 𝒫 X \land z \in 𝒫 X)) \land x \in (y \cap z)) \land (v \in (F (x) \cap 𝒫 y) \land w \in (F (x) \cap 𝒫 z))) \to w \subseteq z$
82		ss2in	$⊢ (v \subseteq y \land w \subseteq z) \to v \cap w \subseteq y \cap z$
83	77 81 82	syl2anc	$⊢ (((φ \land (y \in 𝒫 X \land z \in 𝒫 X)) \land x \in (y \cap z)) \land (v \in (F (x) \cap 𝒫 y) \land w \in (F (x) \cap 𝒫 z))) \to v \cap w \subseteq y \cap z$
84	83	sspwd	$⊢ (((φ \land (y \in 𝒫 X \land z \in 𝒫 X)) \land x \in (y \cap z)) \land (v \in (F (x) \cap 𝒫 y) \land w \in (F (x) \cap 𝒫 z))) \to 𝒫 (v \cap w) \subseteq 𝒫 (y \cap z)$
85		sslin	$⊢ 𝒫 (v \cap w) \subseteq 𝒫 (y \cap z) \to F (x) \cap 𝒫 (v \cap w) \subseteq F (x) \cap 𝒫 (y \cap z)$
86	84 85	syl	$⊢ (((φ \land (y \in 𝒫 X \land z \in 𝒫 X)) \land x \in (y \cap z)) \land (v \in (F (x) \cap 𝒫 y) \land w \in (F (x) \cap 𝒫 z))) \to F (x) \cap 𝒫 (v \cap w) \subseteq F (x) \cap 𝒫 (y \cap z)$
87		simplll	$⊢ (((φ \land (y \in 𝒫 X \land z \in 𝒫 X)) \land x \in (y \cap z)) \land (v \in (F (x) \cap 𝒫 y) \land w \in (F (x) \cap 𝒫 z))) \to φ$
88	56	ad2antrr	$⊢ (((φ \land (y \in 𝒫 X \land z \in 𝒫 X)) \land x \in (y \cap z)) \land (v \in (F (x) \cap 𝒫 y) \land w \in (F (x) \cap 𝒫 z))) \to y \cap z \subseteq X$
89		simplr	$⊢ (((φ \land (y \in 𝒫 X \land z \in 𝒫 X)) \land x \in (y \cap z)) \land (v \in (F (x) \cap 𝒫 y) \land w \in (F (x) \cap 𝒫 z))) \to x \in (y \cap z)$
90	88 89	sseldd	$⊢ (((φ \land (y \in 𝒫 X \land z \in 𝒫 X)) \land x \in (y \cap z)) \land (v \in (F (x) \cap 𝒫 y) \land w \in (F (x) \cap 𝒫 z))) \to x \in X$
91		inss1	$⊢ F (x) \cap 𝒫 y \subseteq F (x)$
92	91 75	sselid	$⊢ (((φ \land (y \in 𝒫 X \land z \in 𝒫 X)) \land x \in (y \cap z)) \land (v \in (F (x) \cap 𝒫 y) \land w \in (F (x) \cap 𝒫 z))) \to v \in F (x)$
93		inss1	$⊢ F (x) \cap 𝒫 z \subseteq F (x)$
94	93 79	sselid	$⊢ (((φ \land (y \in 𝒫 X \land z \in 𝒫 X)) \land x \in (y \cap z)) \land (v \in (F (x) \cap 𝒫 y) \land w \in (F (x) \cap 𝒫 z))) \to w \in F (x)$
95	87 90 92 94 3	syl13anc	$⊢ (((φ \land (y \in 𝒫 X \land z \in 𝒫 X)) \land x \in (y \cap z)) \land (v \in (F (x) \cap 𝒫 y) \land w \in (F (x) \cap 𝒫 z))) \to F (x) \cap 𝒫 (v \cap w) \neq \emptyset$
96		ssn0	$⊢ (F (x) \cap 𝒫 (v \cap w) \subseteq F (x) \cap 𝒫 (y \cap z) \land F (x) \cap 𝒫 (v \cap w) \neq \emptyset) \to F (x) \cap 𝒫 (y \cap z) \neq \emptyset$
97	86 95 96	syl2anc	$⊢ (((φ \land (y \in 𝒫 X \land z \in 𝒫 X)) \land x \in (y \cap z)) \land (v \in (F (x) \cap 𝒫 y) \land w \in (F (x) \cap 𝒫 z))) \to F (x) \cap 𝒫 (y \cap z) \neq \emptyset$
98	97	ex	$⊢ ((φ \land (y \in 𝒫 X \land z \in 𝒫 X)) \land x \in (y \cap z)) \to ((v \in (F (x) \cap 𝒫 y) \land w \in (F (x) \cap 𝒫 z)) \to F (x) \cap 𝒫 (y \cap z) \neq \emptyset)$
99	98	exlimdvv	$⊢ ((φ \land (y \in 𝒫 X \land z \in 𝒫 X)) \land x \in (y \cap z)) \to (\exists v \exists w (v \in (F (x) \cap 𝒫 y) \land w \in (F (x) \cap 𝒫 z)) \to F (x) \cap 𝒫 (y \cap z) \neq \emptyset)$
100	73 99	syl5bir	$⊢ ((φ \land (y \in 𝒫 X \land z \in 𝒫 X)) \land x \in (y \cap z)) \to ((\exists v v \in (F (x) \cap 𝒫 y) \land \exists w w \in (F (x) \cap 𝒫 z)) \to F (x) \cap 𝒫 (y \cap z) \neq \emptyset)$
101	72 100	syl5bi	$⊢ ((φ \land (y \in 𝒫 X \land z \in 𝒫 X)) \land x \in (y \cap z)) \to ((F (x) \cap 𝒫 y \neq \emptyset \land F (x) \cap 𝒫 z \neq \emptyset) \to F (x) \cap 𝒫 (y \cap z) \neq \emptyset)$
102	101	ralimdva	$⊢ (φ \land (y \in 𝒫 X \land z \in 𝒫 X)) \to (\forall x \in (y \cap z) (F (x) \cap 𝒫 y \neq \emptyset \land F (x) \cap 𝒫 z \neq \emptyset) \to \forall x \in (y \cap z) F (x) \cap 𝒫 (y \cap z) \neq \emptyset)$
103	69 102	syl5	$⊢ (φ \land (y \in 𝒫 X \land z \in 𝒫 X)) \to ((\forall x \in y F (x) \cap 𝒫 y \neq \emptyset \land \forall x \in z F (x) \cap 𝒫 z \neq \emptyset) \to \forall x \in (y \cap z) F (x) \cap 𝒫 (y \cap z) \neq \emptyset)$
104	103	impr	$⊢ (φ \land ((y \in 𝒫 X \land z \in 𝒫 X) \land (\forall x \in y F (x) \cap 𝒫 y \neq \emptyset \land \forall x \in z F (x) \cap 𝒫 z \neq \emptyset))) \to \forall x \in (y \cap z) F (x) \cap 𝒫 (y \cap z) \neq \emptyset$
105		pweq	$⊢ o = y \cap z \to 𝒫 o = 𝒫 (y \cap z)$
106	105	ineq2d	$⊢ o = y \cap z \to F (x) \cap 𝒫 o = F (x) \cap 𝒫 (y \cap z)$
107	106	neeq1d	$⊢ o = y \cap z \to (F (x) \cap 𝒫 o \neq \emptyset \leftrightarrow F (x) \cap 𝒫 (y \cap z) \neq \emptyset)$
108	107	raleqbi1dv	$⊢ o = y \cap z \to (\forall x \in o F (x) \cap 𝒫 o \neq \emptyset \leftrightarrow \forall x \in (y \cap z) F (x) \cap 𝒫 (y \cap z) \neq \emptyset)$
109	108 4	elrab2	$⊢ y \cap z \in J \leftrightarrow (y \cap z \in 𝒫 X \land \forall x \in (y \cap z) F (x) \cap 𝒫 (y \cap z) \neq \emptyset)$
110	61 104 109	sylanbrc	$⊢ (φ \land ((y \in 𝒫 X \land z \in 𝒫 X) \land (\forall x \in y F (x) \cap 𝒫 y \neq \emptyset \land \forall x \in z F (x) \cap 𝒫 z \neq \emptyset))) \to y \cap z \in J$
111	52 110	sylan2b	$⊢ (φ \land (y \in J \land z \in J)) \to y \cap z \in J$
112	111	ralrimivva	$⊢ φ \to \forall y \in J \forall z \in J y \cap z \in J$
113		sspwuni	$⊢ J \subseteq 𝒫 X \leftrightarrow ⋃ J \subseteq X$
114	7 113	mpbi	$⊢ ⋃ J \subseteq X$
115	114	a1i	$⊢ φ \to ⋃ J \subseteq X$
116	1 115	ssexd	$⊢ φ \to ⋃ J \in V$
117		uniexb	$⊢ J \in V \leftrightarrow ⋃ J \in V$
118	116 117	sylibr	$⊢ φ \to J \in V$
119		istopg	$⊢ J \in V \to (J \in Top \leftrightarrow (\forall y (y \subseteq J \to ⋃ y \in J) \land \forall y \in J \forall z \in J y \cap z \in J))$
120	118 119	syl	$⊢ φ \to (J \in Top \leftrightarrow (\forall y (y \subseteq J \to ⋃ y \in J) \land \forall y \in J \forall z \in J y \cap z \in J))$
121	44 112 120	mpbir2and	$⊢ φ \to J \in Top$
122		pwidg	$⊢ X \in V \to X \in 𝒫 X$
123	1 122	syl	$⊢ φ \to X \in 𝒫 X$
124	2	ffvelrnda	$⊢ (φ \land x \in X) \to F (x) \in (𝒫 𝒫 X ∖ \{\emptyset\})$
125		eldifi	$⊢ F (x) \in (𝒫 𝒫 X ∖ \{\emptyset\}) \to F (x) \in 𝒫 𝒫 X$
126		elpwi	$⊢ F (x) \in 𝒫 𝒫 X \to F (x) \subseteq 𝒫 X$
127	124 125 126	3syl	$⊢ (φ \land x \in X) \to F (x) \subseteq 𝒫 X$
128		df-ss	$⊢ F (x) \subseteq 𝒫 X \leftrightarrow F (x) \cap 𝒫 X = F (x)$
129	127 128	sylib	$⊢ (φ \land x \in X) \to F (x) \cap 𝒫 X = F (x)$
130		eldifsni	$⊢ F (x) \in (𝒫 𝒫 X ∖ \{\emptyset\}) \to F (x) \neq \emptyset$
131	124 130	syl	$⊢ (φ \land x \in X) \to F (x) \neq \emptyset$
132	129 131	eqnetrd	$⊢ (φ \land x \in X) \to F (x) \cap 𝒫 X \neq \emptyset$
133	132	ralrimiva	$⊢ φ \to \forall x \in X F (x) \cap 𝒫 X \neq \emptyset$
134		pweq	$⊢ o = X \to 𝒫 o = 𝒫 X$
135	134	ineq2d	$⊢ o = X \to F (x) \cap 𝒫 o = F (x) \cap 𝒫 X$
136	135	neeq1d	$⊢ o = X \to (F (x) \cap 𝒫 o \neq \emptyset \leftrightarrow F (x) \cap 𝒫 X \neq \emptyset)$
137	136	raleqbi1dv	$⊢ o = X \to (\forall x \in o F (x) \cap 𝒫 o \neq \emptyset \leftrightarrow \forall x \in X F (x) \cap 𝒫 X \neq \emptyset)$
138	137 4	elrab2	$⊢ X \in J \leftrightarrow (X \in 𝒫 X \land \forall x \in X F (x) \cap 𝒫 X \neq \emptyset)$
139	123 133 138	sylanbrc	$⊢ φ \to X \in J$
140		elssuni	$⊢ X \in J \to X \subseteq ⋃ J$
141	139 140	syl	$⊢ φ \to X \subseteq ⋃ J$
142	141 115	eqssd	$⊢ φ \to X = ⋃ J$
143		istopon	$⊢ J \in TopOn (X) \leftrightarrow (J \in Top \land X = ⋃ J)$
144	121 142 143	sylanbrc	$⊢ φ \to J \in TopOn (X)$

Metamath Proof Explorer

Theorem neibastop1

Proof