Metamath Proof Explorer

Theorem tgcl

Description: Show that a basis generates a topology. Remark in Munkres p. 79. (Contributed by NM, 17-Jul-2006)

Ref Expression
Assertion tgcl ( 𝐵 ∈ TopBases → ( topGen ‘ 𝐵 ) ∈ Top )

Proof

Step Hyp Ref Expression
1 uniss ⊢ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) → ∪ 𝑢 ⊆ ∪ ( topGen ‘ 𝐵 ) )
2 1 adantl ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑢 ⊆ ( topGen ‘ 𝐵 ) ) → ∪ 𝑢 ⊆ ∪ ( topGen ‘ 𝐵 ) )
3 unitg ⊢ ( 𝐵 ∈ TopBases → ∪ ( topGen ‘ 𝐵 ) = ∪ 𝐵 )
4 3 adantr ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑢 ⊆ ( topGen ‘ 𝐵 ) ) → ∪ ( topGen ‘ 𝐵 ) = ∪ 𝐵 )
5 2 4 sseqtrd ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑢 ⊆ ( topGen ‘ 𝐵 ) ) → ∪ 𝑢 ⊆ ∪ 𝐵 )
6 eluni2 ⊢ ( 𝑥 ∈ ∪ 𝑢 ↔ ∃ 𝑡 ∈ 𝑢 𝑥 ∈ 𝑡 )
7 ssel2 ⊢ ( ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑡 ∈ 𝑢 ) → 𝑡 ∈ ( topGen ‘ 𝐵 ) )
8 eltg2b ⊢ ( 𝐵 ∈ TopBases → ( 𝑡 ∈ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡 ) ) )
9 rsp ⊢ ( ∀ 𝑥 ∈ 𝑡 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡 ) → ( 𝑥 ∈ 𝑡 → ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡 ) ) )
10 8 9 syl6bi ⊢ ( 𝐵 ∈ TopBases → ( 𝑡 ∈ ( topGen ‘ 𝐵 ) → ( 𝑥 ∈ 𝑡 → ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡 ) ) ) )
11 10 imp31 ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑡 ∈ ( topGen ‘ 𝐵 ) ) ∧ 𝑥 ∈ 𝑡 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡 ) )
12 11 an32s ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑥 ∈ 𝑡 ) ∧ 𝑡 ∈ ( topGen ‘ 𝐵 ) ) → ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡 ) )
13 7 12 sylan2 ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑥 ∈ 𝑡 ) ∧ ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑡 ∈ 𝑢 ) ) → ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡 ) )
14 13 an42s ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑢 ⊆ ( topGen ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ 𝑢 ∧ 𝑥 ∈ 𝑡 ) ) → ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡 ) )
15 elssuni ⊢ ( 𝑡 ∈ 𝑢 → 𝑡 ⊆ ∪ 𝑢 )
16 sstr2 ⊢ ( 𝑦 ⊆ 𝑡 → ( 𝑡 ⊆ ∪ 𝑢 → 𝑦 ⊆ ∪ 𝑢 ) )
17 15 16 syl5com ⊢ ( 𝑡 ∈ 𝑢 → ( 𝑦 ⊆ 𝑡 → 𝑦 ⊆ ∪ 𝑢 ) )
18 17 anim2d ⊢ ( 𝑡 ∈ 𝑢 → ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡 ) → ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢 ) ) )
19 18 reximdv ⊢ ( 𝑡 ∈ 𝑢 → ( ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢 ) ) )
20 19 ad2antrl ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑢 ⊆ ( topGen ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ 𝑢 ∧ 𝑥 ∈ 𝑡 ) ) → ( ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑡 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢 ) ) )
21 14 20 mpd ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑢 ⊆ ( topGen ‘ 𝐵 ) ) ∧ ( 𝑡 ∈ 𝑢 ∧ 𝑥 ∈ 𝑡 ) ) → ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢 ) )
22 21 rexlimdvaa ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑢 ⊆ ( topGen ‘ 𝐵 ) ) → ( ∃ 𝑡 ∈ 𝑢 𝑥 ∈ 𝑡 → ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢 ) ) )
23 6 22 syl5bi ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑢 ⊆ ( topGen ‘ 𝐵 ) ) → ( 𝑥 ∈ ∪ 𝑢 → ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢 ) ) )
24 23 ralrimiv ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑢 ⊆ ( topGen ‘ 𝐵 ) ) → ∀ 𝑥 ∈ ∪ 𝑢 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢 ) )
25 5 24 jca ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑢 ⊆ ( topGen ‘ 𝐵 ) ) → ( ∪ 𝑢 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ ∪ 𝑢 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢 ) ) )
26 25 ex ⊢ ( 𝐵 ∈ TopBases → ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) → ( ∪ 𝑢 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ ∪ 𝑢 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢 ) ) ) )
27 eltg2 ⊢ ( 𝐵 ∈ TopBases → ( ∪ 𝑢 ∈ ( topGen ‘ 𝐵 ) ↔ ( ∪ 𝑢 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ ∪ 𝑢 ∃ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ∪ 𝑢 ) ) ) )
28 26 27 sylibrd ⊢ ( 𝐵 ∈ TopBases → ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) → ∪ 𝑢 ∈ ( topGen ‘ 𝐵 ) ) )
29 28 alrimiv ⊢ ( 𝐵 ∈ TopBases → ∀ 𝑢 ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) → ∪ 𝑢 ∈ ( topGen ‘ 𝐵 ) ) )
30 inss1 ⊢ ( 𝑢 ∩ 𝑣 ) ⊆ 𝑢
31 tg1 ⊢ ( 𝑢 ∈ ( topGen ‘ 𝐵 ) → 𝑢 ⊆ ∪ 𝐵 )
32 30 31 sstrid ⊢ ( 𝑢 ∈ ( topGen ‘ 𝐵 ) → ( 𝑢 ∩ 𝑣 ) ⊆ ∪ 𝐵 )
33 32 ad2antrl ⊢ ( ( 𝐵 ∈ TopBases ∧ ( 𝑢 ∈ ( topGen ‘ 𝐵 ) ∧ 𝑣 ∈ ( topGen ‘ 𝐵 ) ) ) → ( 𝑢 ∩ 𝑣 ) ⊆ ∪ 𝐵 )
34 eltg2 ⊢ ( 𝐵 ∈ TopBases → ( 𝑢 ∈ ( topGen ‘ 𝐵 ) ↔ ( 𝑢 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝑢 ∃ 𝑧 ∈ 𝐵 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢 ) ) ) )
35 34 simplbda ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑢 ∈ ( topGen ‘ 𝐵 ) ) → ∀ 𝑥 ∈ 𝑢 ∃ 𝑧 ∈ 𝐵 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢 ) )
36 rsp ⊢ ( ∀ 𝑥 ∈ 𝑢 ∃ 𝑧 ∈ 𝐵 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢 ) → ( 𝑥 ∈ 𝑢 → ∃ 𝑧 ∈ 𝐵 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢 ) ) )
37 35 36 syl ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑢 ∈ ( topGen ‘ 𝐵 ) ) → ( 𝑥 ∈ 𝑢 → ∃ 𝑧 ∈ 𝐵 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢 ) ) )
38 eltg2 ⊢ ( 𝐵 ∈ TopBases → ( 𝑣 ∈ ( topGen ‘ 𝐵 ) ↔ ( 𝑣 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ 𝑣 ∃ 𝑤 ∈ 𝐵 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) ) )
39 38 simplbda ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑣 ∈ ( topGen ‘ 𝐵 ) ) → ∀ 𝑥 ∈ 𝑣 ∃ 𝑤 ∈ 𝐵 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) )
40 rsp ⊢ ( ∀ 𝑥 ∈ 𝑣 ∃ 𝑤 ∈ 𝐵 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) → ( 𝑥 ∈ 𝑣 → ∃ 𝑤 ∈ 𝐵 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) )
41 39 40 syl ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑣 ∈ ( topGen ‘ 𝐵 ) ) → ( 𝑥 ∈ 𝑣 → ∃ 𝑤 ∈ 𝐵 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) )
42 37 41 im2anan9 ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑢 ∈ ( topGen ‘ 𝐵 ) ) ∧ ( 𝐵 ∈ TopBases ∧ 𝑣 ∈ ( topGen ‘ 𝐵 ) ) ) → ( ( 𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣 ) → ( ∃ 𝑧 ∈ 𝐵 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢 ) ∧ ∃ 𝑤 ∈ 𝐵 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) ) )
43 elin ⊢ ( 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) ↔ ( 𝑥 ∈ 𝑢 ∧ 𝑥 ∈ 𝑣 ) )
44 reeanv ⊢ ( ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐵 ( ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) ↔ ( ∃ 𝑧 ∈ 𝐵 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢 ) ∧ ∃ 𝑤 ∈ 𝐵 ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) )
45 42 43 44 3imtr4g ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑢 ∈ ( topGen ‘ 𝐵 ) ) ∧ ( 𝐵 ∈ TopBases ∧ 𝑣 ∈ ( topGen ‘ 𝐵 ) ) ) → ( 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) → ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐵 ( ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) ) )
46 45 anandis ⊢ ( ( 𝐵 ∈ TopBases ∧ ( 𝑢 ∈ ( topGen ‘ 𝐵 ) ∧ 𝑣 ∈ ( topGen ‘ 𝐵 ) ) ) → ( 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) → ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐵 ( ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) ) )
47 elin ⊢ ( 𝑥 ∈ ( 𝑧 ∩ 𝑤 ) ↔ ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤 ) )
48 47 biimpri ⊢ ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤 ) → 𝑥 ∈ ( 𝑧 ∩ 𝑤 ) )
49 ss2in ⊢ ( ( 𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣 ) → ( 𝑧 ∩ 𝑤 ) ⊆ ( 𝑢 ∩ 𝑣 ) )
50 48 49 anim12i ⊢ ( ( ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤 ) ∧ ( 𝑧 ⊆ 𝑢 ∧ 𝑤 ⊆ 𝑣 ) ) → ( 𝑥 ∈ ( 𝑧 ∩ 𝑤 ) ∧ ( 𝑧 ∩ 𝑤 ) ⊆ ( 𝑢 ∩ 𝑣 ) ) )
51 50 an4s ⊢ ( ( ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) → ( 𝑥 ∈ ( 𝑧 ∩ 𝑤 ) ∧ ( 𝑧 ∩ 𝑤 ) ⊆ ( 𝑢 ∩ 𝑣 ) ) )
52 basis2 ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝑧 ∩ 𝑤 ) ) ) → ∃ 𝑡 ∈ 𝐵 ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑧 ∩ 𝑤 ) ) )
53 52 adantllr ⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝑧 ∩ 𝑤 ) ) ) → ∃ 𝑡 ∈ 𝐵 ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑧 ∩ 𝑤 ) ) )
54 53 adantrrr ⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑤 ∈ 𝐵 ∧ ( 𝑥 ∈ ( 𝑧 ∩ 𝑤 ) ∧ ( 𝑧 ∩ 𝑤 ) ⊆ ( 𝑢 ∩ 𝑣 ) ) ) ) → ∃ 𝑡 ∈ 𝐵 ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑧 ∩ 𝑤 ) ) )
55 sstr2 ⊢ ( 𝑡 ⊆ ( 𝑧 ∩ 𝑤 ) → ( ( 𝑧 ∩ 𝑤 ) ⊆ ( 𝑢 ∩ 𝑣 ) → 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) )
56 55 com12 ⊢ ( ( 𝑧 ∩ 𝑤 ) ⊆ ( 𝑢 ∩ 𝑣 ) → ( 𝑡 ⊆ ( 𝑧 ∩ 𝑤 ) → 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) )
57 56 anim2d ⊢ ( ( 𝑧 ∩ 𝑤 ) ⊆ ( 𝑢 ∩ 𝑣 ) → ( ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑧 ∩ 𝑤 ) ) → ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) )
58 57 reximdv ⊢ ( ( 𝑧 ∩ 𝑤 ) ⊆ ( 𝑢 ∩ 𝑣 ) → ( ∃ 𝑡 ∈ 𝐵 ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑡 ∈ 𝐵 ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) )
59 58 adantl ⊢ ( ( 𝑥 ∈ ( 𝑧 ∩ 𝑤 ) ∧ ( 𝑧 ∩ 𝑤 ) ⊆ ( 𝑢 ∩ 𝑣 ) ) → ( ∃ 𝑡 ∈ 𝐵 ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑡 ∈ 𝐵 ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) )
60 59 ad2antll ⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑤 ∈ 𝐵 ∧ ( 𝑥 ∈ ( 𝑧 ∩ 𝑤 ) ∧ ( 𝑧 ∩ 𝑤 ) ⊆ ( 𝑢 ∩ 𝑣 ) ) ) ) → ( ∃ 𝑡 ∈ 𝐵 ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑧 ∩ 𝑤 ) ) → ∃ 𝑡 ∈ 𝐵 ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) )
61 54 60 mpd ⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑤 ∈ 𝐵 ∧ ( 𝑥 ∈ ( 𝑧 ∩ 𝑤 ) ∧ ( 𝑧 ∩ 𝑤 ) ⊆ ( 𝑢 ∩ 𝑣 ) ) ) ) → ∃ 𝑡 ∈ 𝐵 ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) )
62 51 61 sylanr2 ⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑤 ∈ 𝐵 ∧ ( ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) ) ) → ∃ 𝑡 ∈ 𝐵 ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) )
63 62 rexlimdvaa ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( ∃ 𝑤 ∈ 𝐵 ( ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) → ∃ 𝑡 ∈ 𝐵 ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) )
64 63 rexlimdva ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) ) → ( ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐵 ( ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) → ∃ 𝑡 ∈ 𝐵 ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) )
65 64 ex ⊢ ( 𝐵 ∈ TopBases → ( 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) → ( ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐵 ( ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) → ∃ 𝑡 ∈ 𝐵 ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) ) )
66 65 a2d ⊢ ( 𝐵 ∈ TopBases → ( ( 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) → ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐵 ( ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) ) → ( 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) → ∃ 𝑡 ∈ 𝐵 ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) ) )
67 66 imp ⊢ ( ( 𝐵 ∈ TopBases ∧ ( 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) → ∃ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐵 ( ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑢 ) ∧ ( 𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) ) ) → ( 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) → ∃ 𝑡 ∈ 𝐵 ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) )
68 46 67 syldan ⊢ ( ( 𝐵 ∈ TopBases ∧ ( 𝑢 ∈ ( topGen ‘ 𝐵 ) ∧ 𝑣 ∈ ( topGen ‘ 𝐵 ) ) ) → ( 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) → ∃ 𝑡 ∈ 𝐵 ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) )
69 68 ralrimiv ⊢ ( ( 𝐵 ∈ TopBases ∧ ( 𝑢 ∈ ( topGen ‘ 𝐵 ) ∧ 𝑣 ∈ ( topGen ‘ 𝐵 ) ) ) → ∀ 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) ∃ 𝑡 ∈ 𝐵 ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) )
70 33 69 jca ⊢ ( ( 𝐵 ∈ TopBases ∧ ( 𝑢 ∈ ( topGen ‘ 𝐵 ) ∧ 𝑣 ∈ ( topGen ‘ 𝐵 ) ) ) → ( ( 𝑢 ∩ 𝑣 ) ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) ∃ 𝑡 ∈ 𝐵 ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) )
71 70 ex ⊢ ( 𝐵 ∈ TopBases → ( ( 𝑢 ∈ ( topGen ‘ 𝐵 ) ∧ 𝑣 ∈ ( topGen ‘ 𝐵 ) ) → ( ( 𝑢 ∩ 𝑣 ) ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) ∃ 𝑡 ∈ 𝐵 ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) ) )
72 eltg2 ⊢ ( 𝐵 ∈ TopBases → ( ( 𝑢 ∩ 𝑣 ) ∈ ( topGen ‘ 𝐵 ) ↔ ( ( 𝑢 ∩ 𝑣 ) ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ ( 𝑢 ∩ 𝑣 ) ∃ 𝑡 ∈ 𝐵 ( 𝑥 ∈ 𝑡 ∧ 𝑡 ⊆ ( 𝑢 ∩ 𝑣 ) ) ) ) )
73 71 72 sylibrd ⊢ ( 𝐵 ∈ TopBases → ( ( 𝑢 ∈ ( topGen ‘ 𝐵 ) ∧ 𝑣 ∈ ( topGen ‘ 𝐵 ) ) → ( 𝑢 ∩ 𝑣 ) ∈ ( topGen ‘ 𝐵 ) ) )
74 73 ralrimivv ⊢ ( 𝐵 ∈ TopBases → ∀ 𝑢 ∈ ( topGen ‘ 𝐵 ) ∀ 𝑣 ∈ ( topGen ‘ 𝐵 ) ( 𝑢 ∩ 𝑣 ) ∈ ( topGen ‘ 𝐵 ) )
75 fvex ⊢ ( topGen ‘ 𝐵 ) ∈ V
76 istopg ⊢ ( ( topGen ‘ 𝐵 ) ∈ V → ( ( topGen ‘ 𝐵 ) ∈ Top ↔ ( ∀ 𝑢 ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) → ∪ 𝑢 ∈ ( topGen ‘ 𝐵 ) ) ∧ ∀ 𝑢 ∈ ( topGen ‘ 𝐵 ) ∀ 𝑣 ∈ ( topGen ‘ 𝐵 ) ( 𝑢 ∩ 𝑣 ) ∈ ( topGen ‘ 𝐵 ) ) ) )
77 75 76 ax-mp ⊢ ( ( topGen ‘ 𝐵 ) ∈ Top ↔ ( ∀ 𝑢 ( 𝑢 ⊆ ( topGen ‘ 𝐵 ) → ∪ 𝑢 ∈ ( topGen ‘ 𝐵 ) ) ∧ ∀ 𝑢 ∈ ( topGen ‘ 𝐵 ) ∀ 𝑣 ∈ ( topGen ‘ 𝐵 ) ( 𝑢 ∩ 𝑣 ) ∈ ( topGen ‘ 𝐵 ) ) )
78 29 74 77 sylanbrc ⊢ ( 𝐵 ∈ TopBases → ( topGen ‘ 𝐵 ) ∈ Top )