neiptoptop

	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	neiptoptop	$⊢ φ \to J \in Top$

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		uniss	$⊢ e \subseteq J \to ⋃ e \subseteq ⋃ J$
9	8	adantl	$⊢ (φ \land e \subseteq J) \to ⋃ e \subseteq ⋃ J$
10	1 2 3 4 5 6 7	neiptopuni	$⊢ φ \to X = ⋃ J$
11	10	adantr	$⊢ (φ \land e \subseteq J) \to X = ⋃ J$
12	9 11	sseqtrrd	$⊢ (φ \land e \subseteq J) \to ⋃ e \subseteq X$
13		simp-4l	$⊢ ((((φ \land e \subseteq J) \land p \in ⋃ e) \land c \in e) \land p \in c) \to φ$
14	12	ad3antrrr	$⊢ ((((φ \land e \subseteq J) \land p \in ⋃ e) \land c \in e) \land p \in c) \to ⋃ e \subseteq X$
15		simpllr	$⊢ ((((φ \land e \subseteq J) \land p \in ⋃ e) \land c \in e) \land p \in c) \to p \in ⋃ e$
16	14 15	sseldd	$⊢ ((((φ \land e \subseteq J) \land p \in ⋃ e) \land c \in e) \land p \in c) \to p \in X$
17	13 16	jca	$⊢ ((((φ \land e \subseteq J) \land p \in ⋃ e) \land c \in e) \land p \in c) \to (φ \land p \in X)$
18		elssuni	$⊢ c \in e \to c \subseteq ⋃ e$
19	18	ad2antlr	$⊢ ((((φ \land e \subseteq J) \land p \in ⋃ e) \land c \in e) \land p \in c) \to c \subseteq ⋃ e$
20	17 19 14	3jca	$⊢ ((((φ \land e \subseteq J) \land p \in ⋃ e) \land c \in e) \land p \in c) \to ((φ \land p \in X) \land c \subseteq ⋃ e \land ⋃ e \subseteq X)$
21		simpr	$⊢ (φ \land e \subseteq J) \to e \subseteq J$
22	21	sselda	$⊢ ((φ \land e \subseteq J) \land c \in e) \to c \in J$
23	1	neipeltop	$⊢ c \in J \leftrightarrow (c \subseteq X \land \forall p \in c c \in N (p))$
24	23	simprbi	$⊢ c \in J \to \forall p \in c c \in N (p)$
25	22 24	syl	$⊢ ((φ \land e \subseteq J) \land c \in e) \to \forall p \in c c \in N (p)$
26	25	r19.21bi	$⊢ (((φ \land e \subseteq J) \land c \in e) \land p \in c) \to c \in N (p)$
27	26	adantllr	$⊢ ((((φ \land e \subseteq J) \land p \in ⋃ e) \land c \in e) \land p \in c) \to c \in N (p)$
28		sseq1	$⊢ a = c \to (a \subseteq ⋃ e \leftrightarrow c \subseteq ⋃ e)$
29	28	3anbi2d	$⊢ a = c \to (((φ \land p \in X) \land a \subseteq ⋃ e \land ⋃ e \subseteq X) \leftrightarrow ((φ \land p \in X) \land c \subseteq ⋃ e \land ⋃ e \subseteq X))$
30		eleq1	$⊢ a = c \to (a \in N (p) \leftrightarrow c \in N (p))$
31	29 30	anbi12d	$⊢ a = c \to ((((φ \land p \in X) \land a \subseteq ⋃ e \land ⋃ e \subseteq X) \land a \in N (p)) \leftrightarrow (((φ \land p \in X) \land c \subseteq ⋃ e \land ⋃ e \subseteq X) \land c \in N (p)))$
32	31	imbi1d	$⊢ a = c \to (((((φ \land p \in X) \land a \subseteq ⋃ e \land ⋃ e \subseteq X) \land a \in N (p)) \to ⋃ e \in N (p)) \leftrightarrow ((((φ \land p \in X) \land c \subseteq ⋃ e \land ⋃ e \subseteq X) \land c \in N (p)) \to ⋃ e \in N (p)))$
33	32	imbi2d	$⊢ a = c \to (((φ \land e \subseteq J) \to ((((φ \land p \in X) \land a \subseteq ⋃ e \land ⋃ e \subseteq X) \land a \in N (p)) \to ⋃ e \in N (p))) \leftrightarrow ((φ \land e \subseteq J) \to ((((φ \land p \in X) \land c \subseteq ⋃ e \land ⋃ e \subseteq X) \land c \in N (p)) \to ⋃ e \in N (p))))$
34		ssidd	$⊢ φ \to X \subseteq X$
35	7	ralrimiva	$⊢ φ \to \forall p \in X X \in N (p)$
36	1	neipeltop	$⊢ X \in J \leftrightarrow (X \subseteq X \land \forall p \in X X \in N (p))$
37	34 35 36	sylanbrc	$⊢ φ \to X \in J$
38		pwexg	$⊢ X \in J \to 𝒫 X \in V$
39		rabexg	$⊢ 𝒫 X \in V \to \{a \in 𝒫 X \| \forall p \in a a \in N (p)\} \in V$
40	37 38 39	3syl	$⊢ φ \to \{a \in 𝒫 X \| \forall p \in a a \in N (p)\} \in V$
41	1 40	eqeltrid	$⊢ φ \to J \in V$
42	41	adantr	$⊢ (φ \land e \subseteq J) \to J \in V$
43	42 21	ssexd	$⊢ (φ \land e \subseteq J) \to e \in V$
44		uniexg	$⊢ e \in V \to ⋃ e \in V$
45		sseq2	$⊢ b = ⋃ e \to (a \subseteq b \leftrightarrow a \subseteq ⋃ e)$
46		sseq1	$⊢ b = ⋃ e \to (b \subseteq X \leftrightarrow ⋃ e \subseteq X)$
47	45 46	3anbi23d	$⊢ b = ⋃ e \to (((φ \land p \in X) \land a \subseteq b \land b \subseteq X) \leftrightarrow ((φ \land p \in X) \land a \subseteq ⋃ e \land ⋃ e \subseteq X))$
48	47	anbi1d	$⊢ b = ⋃ e \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 ⋃ e \land ⋃ e \subseteq X) \land a \in N (p)))$
49		eleq1	$⊢ b = ⋃ e \to (b \in N (p) \leftrightarrow ⋃ e \in N (p))$
50	48 49	imbi12d	$⊢ b = ⋃ e \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 ⋃ e \land ⋃ e \subseteq X) \land a \in N (p)) \to ⋃ e \in N (p)))$
51	50 3	vtoclg	$⊢ ⋃ e \in V \to ((((φ \land p \in X) \land a \subseteq ⋃ e \land ⋃ e \subseteq X) \land a \in N (p)) \to ⋃ e \in N (p))$
52	43 44 51	3syl	$⊢ (φ \land e \subseteq J) \to ((((φ \land p \in X) \land a \subseteq ⋃ e \land ⋃ e \subseteq X) \land a \in N (p)) \to ⋃ e \in N (p))$
53	33 52	chvarvv	$⊢ (φ \land e \subseteq J) \to ((((φ \land p \in X) \land c \subseteq ⋃ e \land ⋃ e \subseteq X) \land c \in N (p)) \to ⋃ e \in N (p))$
54	53	ad3antrrr	$⊢ ((((φ \land e \subseteq J) \land p \in ⋃ e) \land c \in e) \land p \in c) \to ((((φ \land p \in X) \land c \subseteq ⋃ e \land ⋃ e \subseteq X) \land c \in N (p)) \to ⋃ e \in N (p))$
55	20 27 54	mp2and	$⊢ ((((φ \land e \subseteq J) \land p \in ⋃ e) \land c \in e) \land p \in c) \to ⋃ e \in N (p)$
56		simpr	$⊢ ((φ \land e \subseteq J) \land p \in ⋃ e) \to p \in ⋃ e$
57		eluni2	$⊢ p \in ⋃ e \leftrightarrow \exists c \in e p \in c$
58	56 57	sylib	$⊢ ((φ \land e \subseteq J) \land p \in ⋃ e) \to \exists c \in e p \in c$
59	55 58	r19.29a	$⊢ ((φ \land e \subseteq J) \land p \in ⋃ e) \to ⋃ e \in N (p)$
60	59	ralrimiva	$⊢ (φ \land e \subseteq J) \to \forall p \in ⋃ e ⋃ e \in N (p)$
61	1	neipeltop	$⊢ ⋃ e \in J \leftrightarrow (⋃ e \subseteq X \land \forall p \in ⋃ e ⋃ e \in N (p))$
62	12 60 61	sylanbrc	$⊢ (φ \land e \subseteq J) \to ⋃ e \in J$
63	62	ex	$⊢ φ \to (e \subseteq J \to ⋃ e \in J)$
64	63	alrimiv	$⊢ φ \to \forall e (e \subseteq J \to ⋃ e \in J)$
65		inss1	$⊢ e \cap f \subseteq e$
66	1	neipeltop	$⊢ e \in J \leftrightarrow (e \subseteq X \land \forall p \in e e \in N (p))$
67	66	simplbi	$⊢ e \in J \to e \subseteq X$
68	67	ad2antlr	$⊢ ((φ \land e \in J) \land f \in J) \to e \subseteq X$
69	65 68	sstrid	$⊢ ((φ \land e \in J) \land f \in J) \to e \cap f \subseteq X$
70		simplll	$⊢ (((φ \land e \in J) \land f \in J) \land p \in (e \cap f)) \to φ$
71		simpllr	$⊢ (((φ \land e \in J) \land f \in J) \land p \in (e \cap f)) \to e \in J$
72	71 67	syl	$⊢ (((φ \land e \in J) \land f \in J) \land p \in (e \cap f)) \to e \subseteq X$
73		simpr	$⊢ (((φ \land e \in J) \land f \in J) \land p \in (e \cap f)) \to p \in (e \cap f)$
74	73	elin1d	$⊢ (((φ \land e \in J) \land f \in J) \land p \in (e \cap f)) \to p \in e$
75	72 74	sseldd	$⊢ (((φ \land e \in J) \land f \in J) \land p \in (e \cap f)) \to p \in X$
76	70 75 4	syl2anc	$⊢ (((φ \land e \in J) \land f \in J) \land p \in (e \cap f)) \to fi (N (p)) \subseteq N (p)$
77		fvex	$⊢ N (p) \in V$
78	66	simprbi	$⊢ e \in J \to \forall p \in e e \in N (p)$
79	78	r19.21bi	$⊢ (e \in J \land p \in e) \to e \in N (p)$
80	71 74 79	syl2anc	$⊢ (((φ \land e \in J) \land f \in J) \land p \in (e \cap f)) \to e \in N (p)$
81		simplr	$⊢ (((φ \land e \in J) \land f \in J) \land p \in (e \cap f)) \to f \in J$
82	73	elin2d	$⊢ (((φ \land e \in J) \land f \in J) \land p \in (e \cap f)) \to p \in f$
83	1	neipeltop	$⊢ f \in J \leftrightarrow (f \subseteq X \land \forall p \in f f \in N (p))$
84	83	simprbi	$⊢ f \in J \to \forall p \in f f \in N (p)$
85	84	r19.21bi	$⊢ (f \in J \land p \in f) \to f \in N (p)$
86	81 82 85	syl2anc	$⊢ (((φ \land e \in J) \land f \in J) \land p \in (e \cap f)) \to f \in N (p)$
87		inelfi	$⊢ (N (p) \in V \land e \in N (p) \land f \in N (p)) \to e \cap f \in fi (N (p))$
88	77 80 86 87	mp3an2i	$⊢ (((φ \land e \in J) \land f \in J) \land p \in (e \cap f)) \to e \cap f \in fi (N (p))$
89	76 88	sseldd	$⊢ (((φ \land e \in J) \land f \in J) \land p \in (e \cap f)) \to e \cap f \in N (p)$
90	89	ralrimiva	$⊢ ((φ \land e \in J) \land f \in J) \to \forall p \in (e \cap f) e \cap f \in N (p)$
91	1	neipeltop	$⊢ e \cap f \in J \leftrightarrow (e \cap f \subseteq X \land \forall p \in (e \cap f) e \cap f \in N (p))$
92	69 90 91	sylanbrc	$⊢ ((φ \land e \in J) \land f \in J) \to e \cap f \in J$
93	92	ralrimiva	$⊢ (φ \land e \in J) \to \forall f \in J e \cap f \in J$
94	93	ralrimiva	$⊢ φ \to \forall e \in J \forall f \in J e \cap f \in J$
95		istopg	$⊢ J \in V \to (J \in Top \leftrightarrow (\forall e (e \subseteq J \to ⋃ e \in J) \land \forall e \in J \forall f \in J e \cap f \in J))$
96	41 95	syl	$⊢ φ \to (J \in Top \leftrightarrow (\forall e (e \subseteq J \to ⋃ e \in J) \land \forall e \in J \forall f \in J e \cap f \in J))$
97	64 94 96	mpbir2and	$⊢ φ \to J \in Top$

Metamath Proof Explorer

Theorem neiptoptop

Proof