Metamath Proof Explorer

Theorem neiptoptop

Description: Lemma for neiptopreu . (Contributed by Thierry Arnoux, 7-Jan-2018)

Ref Expression
Hypotheses neiptop.o ⊢J=a∈𝒫X|∀p∈aa∈N⁡p
neiptop.0 ⊢φ→N:X⟶𝒫𝒫X
neiptop.1 ⊢φ∧p∈X∧a⊆b∧b⊆X∧a∈N⁡p→b∈N⁡p
neiptop.2 ⊢φ∧p∈X→fi⁡N⁡p⊆N⁡p
neiptop.3 ⊢φ∧p∈X∧a∈N⁡p→p∈a
neiptop.4 ⊢φ∧p∈X∧a∈N⁡p→∃b∈N⁡p∀q∈ba∈N⁡q
neiptop.5 ⊢φ∧p∈X→X∈N⁡p
Assertion neiptoptop ⊢φ→J∈Top

Proof

Step Hyp Ref Expression
1 neiptop.o ⊢J=a∈𝒫X|∀p∈aa∈N⁡p
2 neiptop.0 ⊢φ→N:X⟶𝒫𝒫X
3 neiptop.1 ⊢φ∧p∈X∧a⊆b∧b⊆X∧a∈N⁡p→b∈N⁡p
4 neiptop.2 ⊢φ∧p∈X→fi⁡N⁡p⊆N⁡p
5 neiptop.3 ⊢φ∧p∈X∧a∈N⁡p→p∈a
6 neiptop.4 ⊢φ∧p∈X∧a∈N⁡p→∃b∈N⁡p∀q∈ba∈N⁡q
7 neiptop.5 ⊢φ∧p∈X→X∈N⁡p
8 uniss ⊢e⊆J→⋃e⊆⋃J
9 8 adantl ⊢φ∧e⊆J→⋃e⊆⋃J
10 1 2 3 4 5 6 7 neiptopuni ⊢φ→X=⋃J
11 10 adantr ⊢φ∧e⊆J→X=⋃J
12 9 11 sseqtrrd ⊢φ∧e⊆J→⋃e⊆X
13 simp-4l ⊢φ∧e⊆J∧p∈⋃e∧c∈e∧p∈c→φ
14 12 ad3antrrr ⊢φ∧e⊆J∧p∈⋃e∧c∈e∧p∈c→⋃e⊆X
15 simpllr ⊢φ∧e⊆J∧p∈⋃e∧c∈e∧p∈c→p∈⋃e
16 14 15 sseldd ⊢φ∧e⊆J∧p∈⋃e∧c∈e∧p∈c→p∈X
17 13 16 jca ⊢φ∧e⊆J∧p∈⋃e∧c∈e∧p∈c→φ∧p∈X
18 elssuni ⊢c∈e→c⊆⋃e
19 18 ad2antlr ⊢φ∧e⊆J∧p∈⋃e∧c∈e∧p∈c→c⊆⋃e
20 17 19 14 3jca ⊢φ∧e⊆J∧p∈⋃e∧c∈e∧p∈c→φ∧p∈X∧c⊆⋃e∧⋃e⊆X
21 simpr ⊢φ∧e⊆J→e⊆J
22 21 sselda ⊢φ∧e⊆J∧c∈e→c∈J
23 1 neipeltop ⊢c∈J↔c⊆X∧∀p∈cc∈N⁡p
24 23 simprbi ⊢c∈J→∀p∈cc∈N⁡p
25 22 24 syl ⊢φ∧e⊆J∧c∈e→∀p∈cc∈N⁡p
26 25 r19.21bi ⊢φ∧e⊆J∧c∈e∧p∈c→c∈N⁡p
27 26 adantllr ⊢φ∧e⊆J∧p∈⋃e∧c∈e∧p∈c→c∈N⁡p
28 sseq1 ⊢a=c→a⊆⋃e↔c⊆⋃e
29 28 3anbi2d ⊢a=c→φ∧p∈X∧a⊆⋃e∧⋃e⊆X↔φ∧p∈X∧c⊆⋃e∧⋃e⊆X
30 eleq1 ⊢a=c→a∈N⁡p↔c∈N⁡p
31 29 30 anbi12d ⊢a=c→φ∧p∈X∧a⊆⋃e∧⋃e⊆X∧a∈N⁡p↔φ∧p∈X∧c⊆⋃e∧⋃e⊆X∧c∈N⁡p
32 31 imbi1d ⊢a=c→φ∧p∈X∧a⊆⋃e∧⋃e⊆X∧a∈N⁡p→⋃e∈N⁡p↔φ∧p∈X∧c⊆⋃e∧⋃e⊆X∧c∈N⁡p→⋃e∈N⁡p
33 32 imbi2d ⊢a=c→φ∧e⊆J→φ∧p∈X∧a⊆⋃e∧⋃e⊆X∧a∈N⁡p→⋃e∈N⁡p↔φ∧e⊆J→φ∧p∈X∧c⊆⋃e∧⋃e⊆X∧c∈N⁡p→⋃e∈N⁡p
34 ssidd ⊢φ→X⊆X
35 7 ralrimiva ⊢φ→∀p∈XX∈N⁡p
36 1 neipeltop ⊢X∈J↔X⊆X∧∀p∈XX∈N⁡p
37 34 35 36 sylanbrc ⊢φ→X∈J
38 pwexg ⊢X∈J→𝒫X∈V
39 rabexg ⊢𝒫X∈V→a∈𝒫X|∀p∈aa∈N⁡p∈V
40 37 38 39 3syl ⊢φ→a∈𝒫X|∀p∈aa∈N⁡p∈V
41 1 40 eqeltrid ⊢φ→J∈V
42 41 adantr ⊢φ∧e⊆J→J∈V
43 42 21 ssexd ⊢φ∧e⊆J→e∈V
44 uniexg ⊢e∈V→⋃e∈V
45 sseq2 ⊢b=⋃e→a⊆b↔a⊆⋃e
46 sseq1 ⊢b=⋃e→b⊆X↔⋃e⊆X
47 45 46 3anbi23d ⊢b=⋃e→φ∧p∈X∧a⊆b∧b⊆X↔φ∧p∈X∧a⊆⋃e∧⋃e⊆X
48 47 anbi1d ⊢b=⋃e→φ∧p∈X∧a⊆b∧b⊆X∧a∈N⁡p↔φ∧p∈X∧a⊆⋃e∧⋃e⊆X∧a∈N⁡p
49 eleq1 ⊢b=⋃e→b∈N⁡p↔⋃e∈N⁡p
50 48 49 imbi12d ⊢b=⋃e→φ∧p∈X∧a⊆b∧b⊆X∧a∈N⁡p→b∈N⁡p↔φ∧p∈X∧a⊆⋃e∧⋃e⊆X∧a∈N⁡p→⋃e∈N⁡p
51 50 3 vtoclg ⊢⋃e∈V→φ∧p∈X∧a⊆⋃e∧⋃e⊆X∧a∈N⁡p→⋃e∈N⁡p
52 43 44 51 3syl ⊢φ∧e⊆J→φ∧p∈X∧a⊆⋃e∧⋃e⊆X∧a∈N⁡p→⋃e∈N⁡p
53 33 52 chvarvv ⊢φ∧e⊆J→φ∧p∈X∧c⊆⋃e∧⋃e⊆X∧c∈N⁡p→⋃e∈N⁡p
54 53 ad3antrrr ⊢φ∧e⊆J∧p∈⋃e∧c∈e∧p∈c→φ∧p∈X∧c⊆⋃e∧⋃e⊆X∧c∈N⁡p→⋃e∈N⁡p
55 20 27 54 mp2and ⊢φ∧e⊆J∧p∈⋃e∧c∈e∧p∈c→⋃e∈N⁡p
56 simpr ⊢φ∧e⊆J∧p∈⋃e→p∈⋃e
57 eluni2 ⊢p∈⋃e↔∃c∈ep∈c
58 56 57 sylib ⊢φ∧e⊆J∧p∈⋃e→∃c∈ep∈c
59 55 58 r19.29a ⊢φ∧e⊆J∧p∈⋃e→⋃e∈N⁡p
60 59 ralrimiva ⊢φ∧e⊆J→∀p∈⋃e⋃e∈N⁡p
61 1 neipeltop ⊢⋃e∈J↔⋃e⊆X∧∀p∈⋃e⋃e∈N⁡p
62 12 60 61 sylanbrc ⊢φ∧e⊆J→⋃e∈J
63 62 ex ⊢φ→e⊆J→⋃e∈J
64 63 alrimiv ⊢φ→∀ee⊆J→⋃e∈J
65 inss1 ⊢e∩f⊆e
66 1 neipeltop ⊢e∈J↔e⊆X∧∀p∈ee∈N⁡p
67 66 simplbi ⊢e∈J→e⊆X
68 67 ad2antlr ⊢φ∧e∈J∧f∈J→e⊆X
69 65 68 sstrid ⊢φ∧e∈J∧f∈J→e∩f⊆X
70 simplll ⊢φ∧e∈J∧f∈J∧p∈e∩f→φ
71 simpllr ⊢φ∧e∈J∧f∈J∧p∈e∩f→e∈J
72 71 67 syl ⊢φ∧e∈J∧f∈J∧p∈e∩f→e⊆X
73 simpr ⊢φ∧e∈J∧f∈J∧p∈e∩f→p∈e∩f
74 73 elin1d ⊢φ∧e∈J∧f∈J∧p∈e∩f→p∈e
75 72 74 sseldd ⊢φ∧e∈J∧f∈J∧p∈e∩f→p∈X
76 70 75 4 syl2anc ⊢φ∧e∈J∧f∈J∧p∈e∩f→fi⁡N⁡p⊆N⁡p
77 fvex ⊢N⁡p∈V
78 66 simprbi ⊢e∈J→∀p∈ee∈N⁡p
79 78 r19.21bi ⊢e∈J∧p∈e→e∈N⁡p
80 71 74 79 syl2anc ⊢φ∧e∈J∧f∈J∧p∈e∩f→e∈N⁡p
81 simplr ⊢φ∧e∈J∧f∈J∧p∈e∩f→f∈J
82 73 elin2d ⊢φ∧e∈J∧f∈J∧p∈e∩f→p∈f
83 1 neipeltop ⊢f∈J↔f⊆X∧∀p∈ff∈N⁡p
84 83 simprbi ⊢f∈J→∀p∈ff∈N⁡p
85 84 r19.21bi ⊢f∈J∧p∈f→f∈N⁡p
86 81 82 85 syl2anc ⊢φ∧e∈J∧f∈J∧p∈e∩f→f∈N⁡p
87 inelfi ⊢N⁡p∈V∧e∈N⁡p∧f∈N⁡p→e∩f∈fi⁡N⁡p
88 77 80 86 87 mp3an2i ⊢φ∧e∈J∧f∈J∧p∈e∩f→e∩f∈fi⁡N⁡p
89 76 88 sseldd ⊢φ∧e∈J∧f∈J∧p∈e∩f→e∩f∈N⁡p
90 89 ralrimiva ⊢φ∧e∈J∧f∈J→∀p∈e∩fe∩f∈N⁡p
91 1 neipeltop ⊢e∩f∈J↔e∩f⊆X∧∀p∈e∩fe∩f∈N⁡p
92 69 90 91 sylanbrc ⊢φ∧e∈J∧f∈J→e∩f∈J
93 92 ralrimiva ⊢φ∧e∈J→∀f∈Je∩f∈J
94 93 ralrimiva ⊢φ→∀e∈J∀f∈Je∩f∈J
95 istopg ⊢J∈V→J∈Top↔∀ee⊆J→⋃e∈J∧∀e∈J∀f∈Je∩f∈J
96 41 95 syl ⊢φ→J∈Top↔∀ee⊆J→⋃e∈J∧∀e∈J∀f∈Je∩f∈J
97 64 94 96 mpbir2and ⊢φ→J∈Top