ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  tgcl GIF version
Theorem tgcl 13567
Description: Show that a basis generates a topology. Remark in [Munkres] p. 79. (Contributed by NM, 17-Jul-2006.)
Assertion
Ref Expression
tgcl (𝐡 ∈ TopBases β†’ (topGenβ€˜π΅) ∈ Top)
Proof of Theorem tgcl
Dummy variables π‘₯ 𝑦 𝑧 𝑒 𝑑 𝑣 𝑀 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uniss 3831 . . . . . . . 8 (𝑒 βŠ† (topGenβ€˜π΅) β†’ βˆͺ 𝑒 βŠ† βˆͺ (topGenβ€˜π΅))
21adantl 277 . . . . . . 7 ((𝐡 ∈ TopBases ∧ 𝑒 βŠ† (topGenβ€˜π΅)) β†’ βˆͺ 𝑒 βŠ† βˆͺ (topGenβ€˜π΅))
3 unitg 13565 . . . . . . . 8 (𝐡 ∈ TopBases β†’ βˆͺ (topGenβ€˜π΅) = βˆͺ 𝐡)
43adantr 276 . . . . . . 7 ((𝐡 ∈ TopBases ∧ 𝑒 βŠ† (topGenβ€˜π΅)) β†’ βˆͺ (topGenβ€˜π΅) = βˆͺ 𝐡)
52, 4sseqtrd 3194 . . . . . 6 ((𝐡 ∈ TopBases ∧ 𝑒 βŠ† (topGenβ€˜π΅)) β†’ βˆͺ 𝑒 βŠ† βˆͺ 𝐡)
6 eluni2 3814 . . . . . . . 8 (π‘₯ ∈ βˆͺ 𝑒 ↔ βˆƒπ‘‘ ∈ 𝑒 π‘₯ ∈ 𝑑)
7 ssel2 3151 . . . . . . . . . . . 12 ((𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑑 ∈ 𝑒) β†’ 𝑑 ∈ (topGenβ€˜π΅))
8 eltg2b 13557 . . . . . . . . . . . . . . 15 (𝐡 ∈ TopBases β†’ (𝑑 ∈ (topGenβ€˜π΅) ↔ βˆ€π‘₯ ∈ 𝑑 βˆƒπ‘¦ ∈ 𝐡 (π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† 𝑑)))
9 rsp 2524 . . . . . . . . . . . . . . 15 (βˆ€π‘₯ ∈ 𝑑 βˆƒπ‘¦ ∈ 𝐡 (π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† 𝑑) β†’ (π‘₯ ∈ 𝑑 β†’ βˆƒπ‘¦ ∈ 𝐡 (π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† 𝑑)))
108, 9syl6bi 163 . . . . . . . . . . . . . 14 (𝐡 ∈ TopBases β†’ (𝑑 ∈ (topGenβ€˜π΅) β†’ (π‘₯ ∈ 𝑑 β†’ βˆƒπ‘¦ ∈ 𝐡 (π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† 𝑑))))
1110imp31 256 . . . . . . . . . . . . 13 (((𝐡 ∈ TopBases ∧ 𝑑 ∈ (topGenβ€˜π΅)) ∧ π‘₯ ∈ 𝑑) β†’ βˆƒπ‘¦ ∈ 𝐡 (π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† 𝑑))
1211an32s 568 . . . . . . . . . . . 12 (((𝐡 ∈ TopBases ∧ π‘₯ ∈ 𝑑) ∧ 𝑑 ∈ (topGenβ€˜π΅)) β†’ βˆƒπ‘¦ ∈ 𝐡 (π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† 𝑑))
137, 12sylan2 286 . . . . . . . . . . 11 (((𝐡 ∈ TopBases ∧ π‘₯ ∈ 𝑑) ∧ (𝑒 βŠ† (topGenβ€˜π΅) ∧ 𝑑 ∈ 𝑒)) β†’ βˆƒπ‘¦ ∈ 𝐡 (π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† 𝑑))
1413an42s 589 . . . . . . . . . 10 (((𝐡 ∈ TopBases ∧ 𝑒 βŠ† (topGenβ€˜π΅)) ∧ (𝑑 ∈ 𝑒 ∧ π‘₯ ∈ 𝑑)) β†’ βˆƒπ‘¦ ∈ 𝐡 (π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† 𝑑))
15 elssuni 3838 . . . . . . . . . . . . . 14 (𝑑 ∈ 𝑒 β†’ 𝑑 βŠ† βˆͺ 𝑒)
16 sstr2 3163 . . . . . . . . . . . . . 14 (𝑦 βŠ† 𝑑 β†’ (𝑑 βŠ† βˆͺ 𝑒 β†’ 𝑦 βŠ† βˆͺ 𝑒))
1715, 16syl5com 29 . . . . . . . . . . . . 13 (𝑑 ∈ 𝑒 β†’ (𝑦 βŠ† 𝑑 β†’ 𝑦 βŠ† βˆͺ 𝑒))
1817anim2d 337 . . . . . . . . . . . 12 (𝑑 ∈ 𝑒 β†’ ((π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† 𝑑) β†’ (π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† βˆͺ 𝑒)))
1918reximdv 2578 . . . . . . . . . . 11 (𝑑 ∈ 𝑒 β†’ (βˆƒπ‘¦ ∈ 𝐡 (π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† 𝑑) β†’ βˆƒπ‘¦ ∈ 𝐡 (π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† βˆͺ 𝑒)))
2019ad2antrl 490 . . . . . . . . . 10 (((𝐡 ∈ TopBases ∧ 𝑒 βŠ† (topGenβ€˜π΅)) ∧ (𝑑 ∈ 𝑒 ∧ π‘₯ ∈ 𝑑)) β†’ (βˆƒπ‘¦ ∈ 𝐡 (π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† 𝑑) β†’ βˆƒπ‘¦ ∈ 𝐡 (π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† βˆͺ 𝑒)))
2114, 20mpd 13 . . . . . . . . 9 (((𝐡 ∈ TopBases ∧ 𝑒 βŠ† (topGenβ€˜π΅)) ∧ (𝑑 ∈ 𝑒 ∧ π‘₯ ∈ 𝑑)) β†’ βˆƒπ‘¦ ∈ 𝐡 (π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† βˆͺ 𝑒))
2221rexlimdvaa 2595 . . . . . . . 8 ((𝐡 ∈ TopBases ∧ 𝑒 βŠ† (topGenβ€˜π΅)) β†’ (βˆƒπ‘‘ ∈ 𝑒 π‘₯ ∈ 𝑑 β†’ βˆƒπ‘¦ ∈ 𝐡 (π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† βˆͺ 𝑒)))
236, 22biimtrid 152 . . . . . . 7 ((𝐡 ∈ TopBases ∧ 𝑒 βŠ† (topGenβ€˜π΅)) β†’ (π‘₯ ∈ βˆͺ 𝑒 β†’ βˆƒπ‘¦ ∈ 𝐡 (π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† βˆͺ 𝑒)))
2423ralrimiv 2549 . . . . . 6 ((𝐡 ∈ TopBases ∧ 𝑒 βŠ† (topGenβ€˜π΅)) β†’ βˆ€π‘₯ ∈ βˆͺ π‘’βˆƒπ‘¦ ∈ 𝐡 (π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† βˆͺ 𝑒))
255, 24jca 306 . . . . 5 ((𝐡 ∈ TopBases ∧ 𝑒 βŠ† (topGenβ€˜π΅)) β†’ (βˆͺ 𝑒 βŠ† βˆͺ 𝐡 ∧ βˆ€π‘₯ ∈ βˆͺ π‘’βˆƒπ‘¦ ∈ 𝐡 (π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† βˆͺ 𝑒)))
2625ex 115 . . . 4 (𝐡 ∈ TopBases β†’ (𝑒 βŠ† (topGenβ€˜π΅) β†’ (βˆͺ 𝑒 βŠ† βˆͺ 𝐡 ∧ βˆ€π‘₯ ∈ βˆͺ π‘’βˆƒπ‘¦ ∈ 𝐡 (π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† βˆͺ 𝑒))))
27 eltg2 13556 . . . 4 (𝐡 ∈ TopBases β†’ (βˆͺ 𝑒 ∈ (topGenβ€˜π΅) ↔ (βˆͺ 𝑒 βŠ† βˆͺ 𝐡 ∧ βˆ€π‘₯ ∈ βˆͺ π‘’βˆƒπ‘¦ ∈ 𝐡 (π‘₯ ∈ 𝑦 ∧ 𝑦 βŠ† βˆͺ 𝑒))))
2826, 27sylibrd 169 . . 3 (𝐡 ∈ TopBases β†’ (𝑒 βŠ† (topGenβ€˜π΅) β†’ βˆͺ 𝑒 ∈ (topGenβ€˜π΅)))
2928alrimiv 1874 . 2 (𝐡 ∈ TopBases β†’ βˆ€π‘’(𝑒 βŠ† (topGenβ€˜π΅) β†’ βˆͺ 𝑒 ∈ (topGenβ€˜π΅)))
30 inss1 3356 . . . . . . . 8 (𝑒 ∩ 𝑣) βŠ† 𝑒
31 tg1 13562 . . . . . . . 8 (𝑒 ∈ (topGenβ€˜π΅) β†’ 𝑒 βŠ† βˆͺ 𝐡)
3230, 31sstrid 3167 . . . . . . 7 (𝑒 ∈ (topGenβ€˜π΅) β†’ (𝑒 ∩ 𝑣) βŠ† βˆͺ 𝐡)
3332ad2antrl 490 . . . . . 6 ((𝐡 ∈ TopBases ∧ (𝑒 ∈ (topGenβ€˜π΅) ∧ 𝑣 ∈ (topGenβ€˜π΅))) β†’ (𝑒 ∩ 𝑣) βŠ† βˆͺ 𝐡)
34 eltg2 13556 . . . . . . . . . . . . 13 (𝐡 ∈ TopBases β†’ (𝑒 ∈ (topGenβ€˜π΅) ↔ (𝑒 βŠ† βˆͺ 𝐡 ∧ βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘§ ∈ 𝐡 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑒))))
3534simplbda 384 . . . . . . . . . . . 12 ((𝐡 ∈ TopBases ∧ 𝑒 ∈ (topGenβ€˜π΅)) β†’ βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘§ ∈ 𝐡 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑒))
36 rsp 2524 . . . . . . . . . . . 12 (βˆ€π‘₯ ∈ 𝑒 βˆƒπ‘§ ∈ 𝐡 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑒) β†’ (π‘₯ ∈ 𝑒 β†’ βˆƒπ‘§ ∈ 𝐡 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑒)))
3735, 36syl 14 . . . . . . . . . . 11 ((𝐡 ∈ TopBases ∧ 𝑒 ∈ (topGenβ€˜π΅)) β†’ (π‘₯ ∈ 𝑒 β†’ βˆƒπ‘§ ∈ 𝐡 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑒)))
38 eltg2 13556 . . . . . . . . . . . . 13 (𝐡 ∈ TopBases β†’ (𝑣 ∈ (topGenβ€˜π΅) ↔ (𝑣 βŠ† βˆͺ 𝐡 ∧ βˆ€π‘₯ ∈ 𝑣 βˆƒπ‘€ ∈ 𝐡 (π‘₯ ∈ 𝑀 ∧ 𝑀 βŠ† 𝑣))))
3938simplbda 384 . . . . . . . . . . . 12 ((𝐡 ∈ TopBases ∧ 𝑣 ∈ (topGenβ€˜π΅)) β†’ βˆ€π‘₯ ∈ 𝑣 βˆƒπ‘€ ∈ 𝐡 (π‘₯ ∈ 𝑀 ∧ 𝑀 βŠ† 𝑣))
40 rsp 2524 . . . . . . . . . . . 12 (βˆ€π‘₯ ∈ 𝑣 βˆƒπ‘€ ∈ 𝐡 (π‘₯ ∈ 𝑀 ∧ 𝑀 βŠ† 𝑣) β†’ (π‘₯ ∈ 𝑣 β†’ βˆƒπ‘€ ∈ 𝐡 (π‘₯ ∈ 𝑀 ∧ 𝑀 βŠ† 𝑣)))
4139, 40syl 14 . . . . . . . . . . 11 ((𝐡 ∈ TopBases ∧ 𝑣 ∈ (topGenβ€˜π΅)) β†’ (π‘₯ ∈ 𝑣 β†’ βˆƒπ‘€ ∈ 𝐡 (π‘₯ ∈ 𝑀 ∧ 𝑀 βŠ† 𝑣)))
4237, 41im2anan9 598 . . . . . . . . . 10 (((𝐡 ∈ TopBases ∧ 𝑒 ∈ (topGenβ€˜π΅)) ∧ (𝐡 ∈ TopBases ∧ 𝑣 ∈ (topGenβ€˜π΅))) β†’ ((π‘₯ ∈ 𝑒 ∧ π‘₯ ∈ 𝑣) β†’ (βˆƒπ‘§ ∈ 𝐡 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑒) ∧ βˆƒπ‘€ ∈ 𝐡 (π‘₯ ∈ 𝑀 ∧ 𝑀 βŠ† 𝑣))))
43 elin 3319 . . . . . . . . . 10 (π‘₯ ∈ (𝑒 ∩ 𝑣) ↔ (π‘₯ ∈ 𝑒 ∧ π‘₯ ∈ 𝑣))
44 reeanv 2647 . . . . . . . . . 10 (βˆƒπ‘§ ∈ 𝐡 βˆƒπ‘€ ∈ 𝐡 ((π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑒) ∧ (π‘₯ ∈ 𝑀 ∧ 𝑀 βŠ† 𝑣)) ↔ (βˆƒπ‘§ ∈ 𝐡 (π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑒) ∧ βˆƒπ‘€ ∈ 𝐡 (π‘₯ ∈ 𝑀 ∧ 𝑀 βŠ† 𝑣)))
4542, 43, 443imtr4g 205 . . . . . . . . 9 (((𝐡 ∈ TopBases ∧ 𝑒 ∈ (topGenβ€˜π΅)) ∧ (𝐡 ∈ TopBases ∧ 𝑣 ∈ (topGenβ€˜π΅))) β†’ (π‘₯ ∈ (𝑒 ∩ 𝑣) β†’ βˆƒπ‘§ ∈ 𝐡 βˆƒπ‘€ ∈ 𝐡 ((π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑒) ∧ (π‘₯ ∈ 𝑀 ∧ 𝑀 βŠ† 𝑣))))
4645anandis 592 . . . . . . . 8 ((𝐡 ∈ TopBases ∧ (𝑒 ∈ (topGenβ€˜π΅) ∧ 𝑣 ∈ (topGenβ€˜π΅))) β†’ (π‘₯ ∈ (𝑒 ∩ 𝑣) β†’ βˆƒπ‘§ ∈ 𝐡 βˆƒπ‘€ ∈ 𝐡 ((π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑒) ∧ (π‘₯ ∈ 𝑀 ∧ 𝑀 βŠ† 𝑣))))
47 elin 3319 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ (𝑧 ∩ 𝑀) ↔ (π‘₯ ∈ 𝑧 ∧ π‘₯ ∈ 𝑀))
4847biimpri 133 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ 𝑧 ∧ π‘₯ ∈ 𝑀) β†’ π‘₯ ∈ (𝑧 ∩ 𝑀))
49 ss2in 3364 . . . . . . . . . . . . . . . 16 ((𝑧 βŠ† 𝑒 ∧ 𝑀 βŠ† 𝑣) β†’ (𝑧 ∩ 𝑀) βŠ† (𝑒 ∩ 𝑣))
5048, 49anim12i 338 . . . . . . . . . . . . . . 15 (((π‘₯ ∈ 𝑧 ∧ π‘₯ ∈ 𝑀) ∧ (𝑧 βŠ† 𝑒 ∧ 𝑀 βŠ† 𝑣)) β†’ (π‘₯ ∈ (𝑧 ∩ 𝑀) ∧ (𝑧 ∩ 𝑀) βŠ† (𝑒 ∩ 𝑣)))
5150an4s 588 . . . . . . . . . . . . . 14 (((π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑒) ∧ (π‘₯ ∈ 𝑀 ∧ 𝑀 βŠ† 𝑣)) β†’ (π‘₯ ∈ (𝑧 ∩ 𝑀) ∧ (𝑧 ∩ 𝑀) βŠ† (𝑒 ∩ 𝑣)))
52 basis2 13551 . . . . . . . . . . . . . . . . 17 (((𝐡 ∈ TopBases ∧ 𝑧 ∈ 𝐡) ∧ (𝑀 ∈ 𝐡 ∧ π‘₯ ∈ (𝑧 ∩ 𝑀))) β†’ βˆƒπ‘‘ ∈ 𝐡 (π‘₯ ∈ 𝑑 ∧ 𝑑 βŠ† (𝑧 ∩ 𝑀)))
5352adantllr 481 . . . . . . . . . . . . . . . 16 ((((𝐡 ∈ TopBases ∧ π‘₯ ∈ (𝑒 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐡) ∧ (𝑀 ∈ 𝐡 ∧ π‘₯ ∈ (𝑧 ∩ 𝑀))) β†’ βˆƒπ‘‘ ∈ 𝐡 (π‘₯ ∈ 𝑑 ∧ 𝑑 βŠ† (𝑧 ∩ 𝑀)))
5453adantrrr 487 . . . . . . . . . . . . . . 15 ((((𝐡 ∈ TopBases ∧ π‘₯ ∈ (𝑒 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐡) ∧ (𝑀 ∈ 𝐡 ∧ (π‘₯ ∈ (𝑧 ∩ 𝑀) ∧ (𝑧 ∩ 𝑀) βŠ† (𝑒 ∩ 𝑣)))) β†’ βˆƒπ‘‘ ∈ 𝐡 (π‘₯ ∈ 𝑑 ∧ 𝑑 βŠ† (𝑧 ∩ 𝑀)))
55 sstr2 3163 . . . . . . . . . . . . . . . . . . . 20 (𝑑 βŠ† (𝑧 ∩ 𝑀) β†’ ((𝑧 ∩ 𝑀) βŠ† (𝑒 ∩ 𝑣) β†’ 𝑑 βŠ† (𝑒 ∩ 𝑣)))
5655com12 30 . . . . . . . . . . . . . . . . . . 19 ((𝑧 ∩ 𝑀) βŠ† (𝑒 ∩ 𝑣) β†’ (𝑑 βŠ† (𝑧 ∩ 𝑀) β†’ 𝑑 βŠ† (𝑒 ∩ 𝑣)))
5756anim2d 337 . . . . . . . . . . . . . . . . . 18 ((𝑧 ∩ 𝑀) βŠ† (𝑒 ∩ 𝑣) β†’ ((π‘₯ ∈ 𝑑 ∧ 𝑑 βŠ† (𝑧 ∩ 𝑀)) β†’ (π‘₯ ∈ 𝑑 ∧ 𝑑 βŠ† (𝑒 ∩ 𝑣))))
5857reximdv 2578 . . . . . . . . . . . . . . . . 17 ((𝑧 ∩ 𝑀) βŠ† (𝑒 ∩ 𝑣) β†’ (βˆƒπ‘‘ ∈ 𝐡 (π‘₯ ∈ 𝑑 ∧ 𝑑 βŠ† (𝑧 ∩ 𝑀)) β†’ βˆƒπ‘‘ ∈ 𝐡 (π‘₯ ∈ 𝑑 ∧ 𝑑 βŠ† (𝑒 ∩ 𝑣))))
5958adantl 277 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ (𝑧 ∩ 𝑀) ∧ (𝑧 ∩ 𝑀) βŠ† (𝑒 ∩ 𝑣)) β†’ (βˆƒπ‘‘ ∈ 𝐡 (π‘₯ ∈ 𝑑 ∧ 𝑑 βŠ† (𝑧 ∩ 𝑀)) β†’ βˆƒπ‘‘ ∈ 𝐡 (π‘₯ ∈ 𝑑 ∧ 𝑑 βŠ† (𝑒 ∩ 𝑣))))
6059ad2antll 491 . . . . . . . . . . . . . . 15 ((((𝐡 ∈ TopBases ∧ π‘₯ ∈ (𝑒 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐡) ∧ (𝑀 ∈ 𝐡 ∧ (π‘₯ ∈ (𝑧 ∩ 𝑀) ∧ (𝑧 ∩ 𝑀) βŠ† (𝑒 ∩ 𝑣)))) β†’ (βˆƒπ‘‘ ∈ 𝐡 (π‘₯ ∈ 𝑑 ∧ 𝑑 βŠ† (𝑧 ∩ 𝑀)) β†’ βˆƒπ‘‘ ∈ 𝐡 (π‘₯ ∈ 𝑑 ∧ 𝑑 βŠ† (𝑒 ∩ 𝑣))))
6154, 60mpd 13 . . . . . . . . . . . . . 14 ((((𝐡 ∈ TopBases ∧ π‘₯ ∈ (𝑒 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐡) ∧ (𝑀 ∈ 𝐡 ∧ (π‘₯ ∈ (𝑧 ∩ 𝑀) ∧ (𝑧 ∩ 𝑀) βŠ† (𝑒 ∩ 𝑣)))) β†’ βˆƒπ‘‘ ∈ 𝐡 (π‘₯ ∈ 𝑑 ∧ 𝑑 βŠ† (𝑒 ∩ 𝑣)))
6251, 61sylanr2 405 . . . . . . . . . . . . 13 ((((𝐡 ∈ TopBases ∧ π‘₯ ∈ (𝑒 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐡) ∧ (𝑀 ∈ 𝐡 ∧ ((π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑒) ∧ (π‘₯ ∈ 𝑀 ∧ 𝑀 βŠ† 𝑣)))) β†’ βˆƒπ‘‘ ∈ 𝐡 (π‘₯ ∈ 𝑑 ∧ 𝑑 βŠ† (𝑒 ∩ 𝑣)))
6362rexlimdvaa 2595 . . . . . . . . . . . 12 (((𝐡 ∈ TopBases ∧ π‘₯ ∈ (𝑒 ∩ 𝑣)) ∧ 𝑧 ∈ 𝐡) β†’ (βˆƒπ‘€ ∈ 𝐡 ((π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑒) ∧ (π‘₯ ∈ 𝑀 ∧ 𝑀 βŠ† 𝑣)) β†’ βˆƒπ‘‘ ∈ 𝐡 (π‘₯ ∈ 𝑑 ∧ 𝑑 βŠ† (𝑒 ∩ 𝑣))))
6463rexlimdva 2594 . . . . . . . . . . 11 ((𝐡 ∈ TopBases ∧ π‘₯ ∈ (𝑒 ∩ 𝑣)) β†’ (βˆƒπ‘§ ∈ 𝐡 βˆƒπ‘€ ∈ 𝐡 ((π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑒) ∧ (π‘₯ ∈ 𝑀 ∧ 𝑀 βŠ† 𝑣)) β†’ βˆƒπ‘‘ ∈ 𝐡 (π‘₯ ∈ 𝑑 ∧ 𝑑 βŠ† (𝑒 ∩ 𝑣))))
6564ex 115 . . . . . . . . . 10 (𝐡 ∈ TopBases β†’ (π‘₯ ∈ (𝑒 ∩ 𝑣) β†’ (βˆƒπ‘§ ∈ 𝐡 βˆƒπ‘€ ∈ 𝐡 ((π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑒) ∧ (π‘₯ ∈ 𝑀 ∧ 𝑀 βŠ† 𝑣)) β†’ βˆƒπ‘‘ ∈ 𝐡 (π‘₯ ∈ 𝑑 ∧ 𝑑 βŠ† (𝑒 ∩ 𝑣)))))
6665a2d 26 . . . . . . . . 9 (𝐡 ∈ TopBases β†’ ((π‘₯ ∈ (𝑒 ∩ 𝑣) β†’ βˆƒπ‘§ ∈ 𝐡 βˆƒπ‘€ ∈ 𝐡 ((π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑒) ∧ (π‘₯ ∈ 𝑀 ∧ 𝑀 βŠ† 𝑣))) β†’ (π‘₯ ∈ (𝑒 ∩ 𝑣) β†’ βˆƒπ‘‘ ∈ 𝐡 (π‘₯ ∈ 𝑑 ∧ 𝑑 βŠ† (𝑒 ∩ 𝑣)))))
6766imp 124 . . . . . . . 8 ((𝐡 ∈ TopBases ∧ (π‘₯ ∈ (𝑒 ∩ 𝑣) β†’ βˆƒπ‘§ ∈ 𝐡 βˆƒπ‘€ ∈ 𝐡 ((π‘₯ ∈ 𝑧 ∧ 𝑧 βŠ† 𝑒) ∧ (π‘₯ ∈ 𝑀 ∧ 𝑀 βŠ† 𝑣)))) β†’ (π‘₯ ∈ (𝑒 ∩ 𝑣) β†’ βˆƒπ‘‘ ∈ 𝐡 (π‘₯ ∈ 𝑑 ∧ 𝑑 βŠ† (𝑒 ∩ 𝑣))))
6846, 67syldan 282 . . . . . . 7 ((𝐡 ∈ TopBases ∧ (𝑒 ∈ (topGenβ€˜π΅) ∧ 𝑣 ∈ (topGenβ€˜π΅))) β†’ (π‘₯ ∈ (𝑒 ∩ 𝑣) β†’ βˆƒπ‘‘ ∈ 𝐡 (π‘₯ ∈ 𝑑 ∧ 𝑑 βŠ† (𝑒 ∩ 𝑣))))
6968ralrimiv 2549 . . . . . 6 ((𝐡 ∈ TopBases ∧ (𝑒 ∈ (topGenβ€˜π΅) ∧ 𝑣 ∈ (topGenβ€˜π΅))) β†’ βˆ€π‘₯ ∈ (𝑒 ∩ 𝑣)βˆƒπ‘‘ ∈ 𝐡 (π‘₯ ∈ 𝑑 ∧ 𝑑 βŠ† (𝑒 ∩ 𝑣)))
7033, 69jca 306 . . . . 5 ((𝐡 ∈ TopBases ∧ (𝑒 ∈ (topGenβ€˜π΅) ∧ 𝑣 ∈ (topGenβ€˜π΅))) β†’ ((𝑒 ∩ 𝑣) βŠ† βˆͺ 𝐡 ∧ βˆ€π‘₯ ∈ (𝑒 ∩ 𝑣)βˆƒπ‘‘ ∈ 𝐡 (π‘₯ ∈ 𝑑 ∧ 𝑑 βŠ† (𝑒 ∩ 𝑣))))
7170ex 115 . . . 4 (𝐡 ∈ TopBases β†’ ((𝑒 ∈ (topGenβ€˜π΅) ∧ 𝑣 ∈ (topGenβ€˜π΅)) β†’ ((𝑒 ∩ 𝑣) βŠ† βˆͺ 𝐡 ∧ βˆ€π‘₯ ∈ (𝑒 ∩ 𝑣)βˆƒπ‘‘ ∈ 𝐡 (π‘₯ ∈ 𝑑 ∧ 𝑑 βŠ† (𝑒 ∩ 𝑣)))))
72 eltg2 13556 . . . 4 (𝐡 ∈ TopBases β†’ ((𝑒 ∩ 𝑣) ∈ (topGenβ€˜π΅) ↔ ((𝑒 ∩ 𝑣) βŠ† βˆͺ 𝐡 ∧ βˆ€π‘₯ ∈ (𝑒 ∩ 𝑣)βˆƒπ‘‘ ∈ 𝐡 (π‘₯ ∈ 𝑑 ∧ 𝑑 βŠ† (𝑒 ∩ 𝑣)))))
7371, 72sylibrd 169 . . 3 (𝐡 ∈ TopBases β†’ ((𝑒 ∈ (topGenβ€˜π΅) ∧ 𝑣 ∈ (topGenβ€˜π΅)) β†’ (𝑒 ∩ 𝑣) ∈ (topGenβ€˜π΅)))
7473ralrimivv 2558 . 2 (𝐡 ∈ TopBases β†’ βˆ€π‘’ ∈ (topGenβ€˜π΅)βˆ€π‘£ ∈ (topGenβ€˜π΅)(𝑒 ∩ 𝑣) ∈ (topGenβ€˜π΅))
75 tgvalex 12712 . . 3 (𝐡 ∈ TopBases β†’ (topGenβ€˜π΅) ∈ V)
76 istopg 13502 . . 3 ((topGenβ€˜π΅) ∈ V β†’ ((topGenβ€˜π΅) ∈ Top ↔ (βˆ€π‘’(𝑒 βŠ† (topGenβ€˜π΅) β†’ βˆͺ 𝑒 ∈ (topGenβ€˜π΅)) ∧ βˆ€π‘’ ∈ (topGenβ€˜π΅)βˆ€π‘£ ∈ (topGenβ€˜π΅)(𝑒 ∩ 𝑣) ∈ (topGenβ€˜π΅))))
7775, 76syl 14 . 2 (𝐡 ∈ TopBases β†’ ((topGenβ€˜π΅) ∈ Top ↔ (βˆ€π‘’(𝑒 βŠ† (topGenβ€˜π΅) β†’ βˆͺ 𝑒 ∈ (topGenβ€˜π΅)) ∧ βˆ€π‘’ ∈ (topGenβ€˜π΅)βˆ€π‘£ ∈ (topGenβ€˜π΅)(𝑒 ∩ 𝑣) ∈ (topGenβ€˜π΅))))
7829, 74, 77mpbir2and 944 1 (𝐡 ∈ TopBases β†’ (topGenβ€˜π΅) ∈ Top)
Colors of variables: wff set class
Syntax hints:   β†’ wi 4   ∧ wa 104   ↔ wb 105  βˆ€wal 1351   = wceq 1353   ∈ wcel 2148  βˆ€wral 2455  βˆƒwrex 2456  Vcvv 2738   ∩ cin 3129   βŠ† wss 3130  βˆͺ cuni 3810  β€˜cfv 5217  topGenctg 12703  Topctop 13500  TopBasesctb 13545
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4122  ax-pow 4175  ax-pr 4210  ax-un 4434
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2740  df-sbc 2964  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-opab 4066  df-mpt 4067  df-id 4294  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-iota 5179  df-fun 5219  df-fv 5225  df-topgen 12709  df-top 13501  df-bases 13546
This theorem is referenced by:  tgclb  13568  tgtopon  13569  bastop  13578  resttop  13673  txtop  13763  mopnval  13945  retop  14027
  Copyright terms: Public domain W3C validator