HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem tgcl 8894
Description: Show that a basis generates a topology. Remark in [Munkres] p. 79.
Assertion
Ref Expression
tgcl |- (B e. Bases -> (topGen` B) e. Top)
Proof of Theorem tgcl
StepHypRef Expression
1 fvex 4689 . . 3 |- (topGen` B) e. _V
2 istopg 8865 . . 3 |- ((topGen` B) e. _V -> ((topGen` B) e. Top <-> (A.u(u C_ (topGen` B) -> U.u e. (topGen` B)) /\ A.u e. (topGen` B)A.v e. (topGen` B)(u i^i v) e. (topGen` B))))
31, 2ax-mp 7 . 2 |- ((topGen` B) e. Top <-> (A.u(u C_ (topGen` B) -> U.u e. (topGen` B)) /\ A.u e. (topGen` B)A.v e. (topGen` B)(u i^i v) e. (topGen` B)))
4 uniss 3199 . . . . . . . 8 |- (u C_ (topGen` B) -> U.u C_ U.(topGen` B))
54adantl 424 . . . . . . 7 |- ((B e. Bases /\ u C_ (topGen` B)) -> U.u C_ U.(topGen` B))
6 unitg 8893 . . . . . . . 8 |- (B e. Bases -> U.(topGen` B) = U.B)
76adantr 425 . . . . . . 7 |- ((B e. Bases /\ u C_ (topGen` B)) -> U.(topGen` B) = U.B)
85, 7sseqtrd 2653 . . . . . 6 |- ((B e. Bases /\ u C_ (topGen` B)) -> U.u C_ U.B)
9 eltg2 8889 . . . . . . . . . . . . . . . . 17 |- (B e. Bases -> (t e. (topGen` B) <-> (t C_ U.B /\ A.x e. t E.y e. B (x e. y /\ y C_ t))))
10 simpr 350 . . . . . . . . . . . . . . . . 17 |- ((t C_ U.B /\ A.x e. t E.y e. B (x e. y /\ y C_ t)) -> A.x e. t E.y e. B (x e. y /\ y C_ t))
119, 10syl6bi 231 . . . . . . . . . . . . . . . 16 |- (B e. Bases -> (t e. (topGen` B) -> A.x e. t E.y e. B (x e. y /\ y C_ t)))
12 ra4 2155 . . . . . . . . . . . . . . . 16 |- (A.x e. t E.y e. B (x e. y /\ y C_ t) -> (x e. t -> E.y e. B (x e. y /\ y C_ t)))
1311, 12syl6 25 . . . . . . . . . . . . . . 15 |- (B e. Bases -> (t e. (topGen` B) -> (x e. t -> E.y e. B (x e. y /\ y C_ t))))
1413imp31 389 . . . . . . . . . . . . . 14 |- (((B e. Bases /\ t e. (topGen` B)) /\ x e. t) -> E.y e. B (x e. y /\ y C_ t))
1514an1rs 547 . . . . . . . . . . . . 13 |- (((B e. Bases /\ x e. t) /\ t e. (topGen` B)) -> E.y e. B (x e. y /\ y C_ t))
16 ssel2 2616 . . . . . . . . . . . . 13 |- ((u C_ (topGen` B) /\ t e. u) -> t e. (topGen` B))
1715, 16sylan2 500 . . . . . . . . . . . 12 |- (((B e. Bases /\ x e. t) /\ (u C_ (topGen` B) /\ t e. u)) -> E.y e. B (x e. y /\ y C_ t))
1817an42s 567 . . . . . . . . . . 11 |- (((B e. Bases /\ u C_ (topGen` B)) /\ (t e. u /\ x e. t)) -> E.y e. B (x e. y /\ y C_ t))
19 sstr2 2623 . . . . . . . . . . . . . . 15 |- (y C_ t -> (t C_ U.u -> y C_ U.u))
20 elssuni 3206 . . . . . . . . . . . . . . 15 |- (t e. u -> t C_ U.u)
2119, 20syl5com 63 . . . . . . . . . . . . . 14 |- (t e. u -> (y C_ t -> y C_ U.u))
2221anim2d 620 . . . . . . . . . . . . 13 |- (t e. u -> ((x e. y /\ y C_ t) -> (x e. y /\ y C_ U.u)))
2322reximdv 2202 . . . . . . . . . . . 12 |- (t e. u -> (E.y e. B (x e. y /\ y C_ t) -> E.y e. B (x e. y /\ y C_ U.u)))
2423ad2antrl 442 . . . . . . . . . . 11 |- (((B e. Bases /\ u C_ (topGen` B)) /\ (t e. u /\ x e. t)) -> (E.y e. B (x e. y /\ y C_ t) -> E.y e. B (x e. y /\ y C_ U.u)))
2518, 24mpd 29 . . . . . . . . . 10 |- (((B e. Bases /\ u C_ (topGen` B)) /\ (t e. u /\ x e. t)) -> E.y e. B (x e. y /\ y C_ U.u))
2625exp32 408 . . . . . . . . 9 |- ((B e. Bases /\ u C_ (topGen` B)) -> (t e. u -> (x e. t -> E.y e. B (x e. y /\ y C_ U.u))))
2726r19.23adv 2215 . . . . . . . 8 |- ((B e. Bases /\ u C_ (topGen` B)) -> (E.t e. u x e. t -> E.y e. B (x e. y /\ y C_ U.u)))
28 eluni2 3181 . . . . . . . 8 |- (x e. U.u <-> E.t e. u x e. t)
2927, 28syl5ib 223 . . . . . . 7 |- ((B e. Bases /\ u C_ (topGen` B)) -> (x e. U.u -> E.y e. B (x e. y /\ y C_ U.u)))
3029r19.21aiv 2175 . . . . . 6 |- ((B e. Bases /\ u C_ (topGen` B)) -> A.x e. U.uE.y e. B (x e. y /\ y C_ U.u))
318, 30jca 310 . . . . 5 |- ((B e. Bases /\ u C_ (topGen` B)) -> (U.u C_ U.B /\ A.x e. U.uE.y e. B (x e. y /\ y C_ U.u)))
3231ex 402 . . . 4 |- (B e. Bases -> (u C_ (topGen` B) -> (U.u C_ U.B /\ A.x e. U.uE.y e. B (x e. y /\ y C_ U.u))))
33 eltg2 8889 . . . 4 |- (B e. Bases -> (U.u e. (topGen` B) <-> (U.u C_ U.B /\ A.x e. U.uE.y e. B (x e. y /\ y C_ U.u))))
3432, 33sylibrd 221 . . 3 |- (B e. Bases -> (u C_ (topGen` B) -> U.u e. (topGen` B)))
353419.21aiv 1664 . 2 |- (B e. Bases -> A.u(u C_ (topGen` B) -> U.u e. (topGen` B)))
36 tg1 8890 . . . . . . . 8 |- ((B e. Bases /\ u e. (topGen` B)) -> u C_ U.B)
37 ssinss1 2821 . . . . . . . 8 |- (u C_ U.B -> (u i^i v) C_ U.B)
3836, 37syl 12 . . . . . . 7 |- ((B e. Bases /\ u e. (topGen` B)) -> (u i^i v) C_ U.B)
3938adantrr 431 . . . . . 6 |- ((B e. Bases /\ (u e. (topGen` B) /\ v e. (topGen` B))) -> (u i^i v) C_ U.B)
40 eltg2 8889 . . . . . . . . . . . . 13 |- (B e. Bases -> (u e. (topGen` B) <-> (u C_ U.B /\ A.x e. u E.z e. B (x e. z /\ z C_ u))))
4140simplbda 465 . . . . . . . . . . . 12 |- ((B e. Bases /\ u e. (topGen` B)) -> A.x e. u E.z e. B (x e. z /\ z C_ u))
42 ra4 2155 . . . . . . . . . . . 12 |- (A.x e. u E.z e. B (x e. z /\ z C_ u) -> (x e. u -> E.z e. B (x e. z /\ z C_ u)))
4341, 42syl 12 . . . . . . . . . . 11 |- ((B e. Bases /\ u e. (topGen` B)) -> (x e. u -> E.z e. B (x e. z /\ z C_ u)))
44 eltg2 8889 . . . . . . . . . . . . 13 |- (B e. Bases -> (v e. (topGen` B) <-> (v C_ U.B /\ A.x e. v E.w e. B (x e. w /\ w C_ v))))
4544simplbda 465 . . . . . . . . . . . 12 |- ((B e. Bases /\ v e. (topGen` B)) -> A.x e. v E.w e. B (x e. w /\ w C_ v))
46 ra4 2155 . . . . . . . . . . . 12 |- (A.x e. v E.w e. B (x e. w /\ w C_ v) -> (x e. v -> E.w e. B (x e. w /\ w C_ v)))
4745, 46syl 12 . . . . . . . . . . 11 |- ((B e. Bases /\ v e. (topGen` B)) -> (x e. v -> E.w e. B (x e. w /\ w C_ v)))
4843, 47im2anan9 622 . . . . . . . . . 10 |- (((B e. Bases /\ u e. (topGen` B)) /\ (B e. Bases /\ v e. (topGen` B))) -> ((x e. u /\ x e. v) -> (E.z e. B (x e. z /\ z C_ u) /\ E.w e. B (x e. w /\ w C_ v))))
49 elin 2786 . . . . . . . . . 10 |- (x e. (u i^i v) <-> (x e. u /\ x e. v))
50 reeanv 2249 . . . . . . . . . 10 |- (E.z e. B E.w e. B ((x e. z /\ z C_ u) /\ (x e. w /\ w C_ v)) <-> (E.z e. B (x e. z /\ z C_ u) /\ E.w e. B (x e. w /\ w C_ v)))
5148, 49, 503imtr4g 612 . . . . . . . . 9 |- (((B e. Bases /\ u e. (topGen` B)) /\ (B e. Bases /\ v e. (topGen` B))) -> (x e. (u i^i v) -> E.z e. B E.w e. B ((x e. z /\ z C_ u) /\ (x e. w /\ w C_ v))))
5251anandis 570 . . . . . . . 8 |- ((B e. Bases /\ (u e. (topGen` B) /\ v e. (topGen` B))) -> (x e. (u i^i v) -> E.z e. B E.w e. B ((x e. z /\ z C_ u) /\ (x e. w /\ w C_ v))))
53 basis2 8884 . . . . . . . . . . . . . . . . . 18 |- (((B e. Bases /\ z e. B) /\ (w e. B /\ x e. (z i^i w))) -> E.t e. B (x e. t /\ t C_ (z i^i w)))
5453adantllr 433 . . . . . . . . . . . . . . . . 17 |- ((((B e. Bases /\ x e. (u i^i v)) /\ z e. B) /\ (w e. B /\ x e. (z i^i w))) -> E.t e. B (x e. t /\ t C_ (z i^i w)))
5554adantrrr 439 . . . . . . . . . . . . . . . 16 |- ((((B e. Bases /\ x e. (u i^i v)) /\ z e. B) /\ (w e. B /\ (x e. (z i^i w) /\ (z i^i w) C_ (u i^i v)))) -> E.t e. B (x e. t /\ t C_ (z i^i w)))
56 sstr2 2623 . . . . . . . . . . . . . . . . . . . . 21 |- (t C_ (z i^i w) -> ((z i^i w) C_ (u i^i v) -> t C_ (u i^i v)))
5756com12 14 . . . . . . . . . . . . . . . . . . . 20 |- ((z i^i w) C_ (u i^i v) -> (t C_ (z i^i w) -> t C_ (u i^i v)))
5857anim2d 620 . . . . . . . . . . . . . . . . . . 19 |- ((z i^i w) C_ (u i^i v) -> ((x e. t /\ t C_ (z i^i w)) -> (x e. t /\ t C_ (u i^i v))))
5958reximdv 2202 . . . . . . . . . . . . . . . . . 18 |- ((z i^i w) C_ (u i^i v) -> (E.t e. B (x e. t /\ t C_ (z i^i w)) -> E.t e. B (x e. t /\ t C_ (u i^i v))))
6059adantl 424 . . . . . . . . . . . . . . . . 17 |- ((x e. (z i^i w) /\ (z i^i w) C_ (u i^i v)) -> (E.t e. B (x e. t /\ t C_ (z i^i w)) -> E.t e. B (x e. t /\ t C_ (u i^i v))))
6160ad2antll 443 . . . . . . . . . . . . . . . 16 |- ((((B e. Bases /\ x e. (u i^i v)) /\ z e. B) /\ (w e. B /\ (x e. (z i^i w) /\ (z i^i w) C_ (u i^i v)))) -> (E.t e. B (x e. t /\ t C_ (z i^i w)) -> E.t e. B (x e. t /\ t C_ (u i^i v))))
6255, 61mpd 29 . . . . . . . . . . . . . . 15 |- ((((B e. Bases /\ x e. (u i^i v)) /\ z e. B) /\ (w e. B /\ (x e. (z i^i w) /\ (z i^i w) C_ (u i^i v)))) -> E.t e. B (x e. t /\ t C_ (u i^i v)))
63 elin 2786 . . . . . . . . . . . . . . . . . 18 |- (x e. (z i^i w) <-> (x e. z /\ x e. w))
6463biimpri 169 . . . . . . . . . . . . . . . . 17 |- ((x e. z /\ x e. w) -> x e. (z i^i w))
65 ss2in 2820 . . . . . . . . . . . . . . . . 17 |- ((z C_ u /\ w C_ v) -> (z i^i w) C_ (u i^i v))
6664, 65anim12i 360 . . . . . . . . . . . . . . . 16 |- (((x e. z /\ x e. w) /\ (z C_ u /\ w C_ v)) -> (x e. (z i^i w) /\ (z i^i w) C_ (u i^i v)))
6766an4s 566 . . . . . . . . . . . . . . 15 |- (((x e. z /\ z C_ u) /\ (x e. w /\ w C_ v)) -> (x e. (z i^i w) /\ (z i^i w) C_ (u i^i v)))
6862, 67sylanr2 512 . . . . . . . . . . . . . 14 |- ((((B e. Bases /\ x e. (u i^i v)) /\ z e. B) /\ (w e. B /\ ((x e. z /\ z C_ u) /\ (x e. w /\ w C_ v)))) -> E.t e. B (x e. t /\ t C_ (u i^i v)))
6968exp32 408 . . . . . . . . . . . . 13 |- (((B e. Bases /\ x e. (u i^i v)) /\ z e. B) -> (w e. B -> (((x e. z /\ z C_ u) /\ (x e. w /\ w C_ v)) -> E.t e. B (x e. t /\ t C_ (u i^i v)))))
7069r19.23adv 2215 . . . . . . . . . . . 12 |- (((B e. Bases /\ x e. (u i^i v)) /\ z e. B) -> (E.w e. B ((x e. z /\ z C_ u) /\ (x e. w /\ w C_ v)) -> E.t e. B (x e. t /\ t C_ (u i^i v))))
7170r19.23adva 2216 . . . . . . . . . . 11 |- ((B e. Bases /\ x e. (u i^i v)) -> (E.z e. B E.w e. B ((x e. z /\ z C_ u) /\ (x e. w /\ w C_ v)) -> E.t e. B (x e. t /\ t C_ (u i^i v))))
7271ex 402 . . . . . . . . . 10 |- (B e. Bases -> (x e. (u i^i v) -> (E.z e. B E.w e. B ((x e. z /\ z C_ u) /\ (x e. w /\ w C_ v)) -> E.t e. B (x e. t /\ t C_ (u i^i v)))))
7372a2d 16 . . . . . . . . 9 |- (B e. Bases -> ((x e. (u i^i v) -> E.z e. B E.w e. B ((x e. z /\ z C_ u) /\ (x e. w /\ w C_ v))) -> (x e. (u i^i v) -> E.t e. B (x e. t /\ t C_ (u i^i v)))))
7473imp 377 . . . . . . . 8 |- ((B e. Bases /\ (x e. (u i^i v) -> E.z e. B E.w e. B ((x e. z /\ z C_ u) /\ (x e. w /\ w C_ v)))) -> (x e. (u i^i v) -> E.t e. B (x e. t /\ t C_ (u i^i v))))
7552, 74syldan 516 . . . . . . 7 |- ((B e. Bases /\ (u e. (topGen` B) /\ v e. (topGen` B))) -> (x e. (u i^i v) -> E.t e. B (x e. t /\ t C_ (u i^i v))))
7675r19.21aiv 2175 . . . . . 6 |- ((B e. Bases /\ (u e. (topGen` B) /\ v e. (topGen` B))) -> A.x e. (u i^i v)E.t e. B (x e. t /\ t C_ (u i^i v)))
7739, 76jca 310 . . . . 5 |- ((B e. Bases /\ (u e. (topGen` B) /\ v e. (topGen` B))) -> ((u i^i v) C_ U.B /\ A.x e. (u i^i v)E.t e. B (x e. t /\ t C_ (u i^i v))))
7877ex 402 . . . 4 |- (B e. Bases -> ((u e. (topGen` B) /\ v e. (topGen` B)) -> ((u i^i v) C_ U.B /\ A.x e. (u i^i v)E.t e. B (x e. t /\ t C_ (u i^i v)))))
79 eltg2 8889 . . . 4 |- (B e. Bases -> ((u i^i v) e. (topGen` B) <-> ((u i^i v) C_ U.B /\ A.x e. (u i^i v)E.t e. B (x e. t /\ t C_ (u i^i v)))))
8078, 79sylibrd 221 . . 3 |- (B e. Bases -> ((u e. (topGen` B) /\ v e. (topGen` B)) -> (u i^i v) e. (topGen` B)))
8180r19.21aivv 2183 . 2 |- (B e. Bases -> A.u e. (topGen` B)A.v e. (topGen` B)(u i^i v) e. (topGen` B))
823, 35, 81sylanbrc 527 1 |- (B e. Bases -> (topGen` B) e. Top)
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106  _Vcvv 2292   i^i cin 2592   C_ wss 2593  U.cuni 3177  ` cfv 3998  Topctop 8857  Basesctb 8859  topGenctg 8860
This theorem is referenced by:  tgval3 8895  tgidm 8902  bastop 8903  2basgen 8911  retop 8926  txtop 8934  elcls3 8987  alexsub 15441  is2ndc2 15473  topjoin 15527  txsubsp 15912
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790
This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fv 4014  df-top 8861  df-bases 8863  df-topgen 8864
Copyright terms: Public domain