HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem basgen2 8909
Description: Given a topology J, show that a subset B satisfying the third antecedent is a basis for it. Lemma 2.3 of [Munkres] p. 81.
Assertion
Ref Expression
basgen2 |- ((J e. Top /\ B C_ J /\ A.x e. J A.y e. x E.z e. B (y e. z /\ z C_ x)) -> (B e. Bases /\ (topGen` B) = J))
Distinct variable groups:   x,y,z,B   x,J,y,z
Proof of Theorem basgen2
StepHypRef Expression
1 inopn 8869 . . . . . . . . . 10 |- ((J e. Top /\ w e. J /\ v e. J) -> (w i^i v) e. J)
213expb 1068 . . . . . . . . 9 |- ((J e. Top /\ (w e. J /\ v e. J)) -> (w i^i v) e. J)
3 ssel 2615 . . . . . . . . . . 11 |- (B C_ J -> (w e. B -> w e. J))
4 ssel 2615 . . . . . . . . . . 11 |- (B C_ J -> (v e. B -> v e. J))
53, 4anim12d 617 . . . . . . . . . 10 |- (B C_ J -> ((w e. B /\ v e. B) -> (w e. J /\ v e. J)))
65imp 377 . . . . . . . . 9 |- ((B C_ J /\ (w e. B /\ v e. B)) -> (w e. J /\ v e. J))
72, 6sylan2 500 . . . . . . . 8 |- ((J e. Top /\ (B C_ J /\ (w e. B /\ v e. B))) -> (w i^i v) e. J)
87anassrs 489 . . . . . . 7 |- (((J e. Top /\ B C_ J) /\ (w e. B /\ v e. B)) -> (w i^i v) e. J)
9 sseq2 2639 . . . . . . . . . . 11 |- (x = (w i^i v) -> (z C_ x <-> z C_ (w i^i v)))
109anbi2d 678 . . . . . . . . . 10 |- (x = (w i^i v) -> ((y e. z /\ z C_ x) <-> (y e. z /\ z C_ (w i^i v))))
1110rexbidv 2124 . . . . . . . . 9 |- (x = (w i^i v) -> (E.z e. B (y e. z /\ z C_ x) <-> E.z e. B (y e. z /\ z C_ (w i^i v))))
1211raleqbi1dv 2271 . . . . . . . 8 |- (x = (w i^i v) -> (A.y e. x E.z e. B (y e. z /\ z C_ x) <-> A.y e. (w i^i v)E.z e. B (y e. z /\ z C_ (w i^i v))))
1312rcla4v 2376 . . . . . . 7 |- ((w i^i v) e. J -> (A.x e. J A.y e. x E.z e. B (y e. z /\ z C_ x) -> A.y e. (w i^i v)E.z e. B (y e. z /\ z C_ (w i^i v))))
148, 13syl 12 . . . . . 6 |- (((J e. Top /\ B C_ J) /\ (w e. B /\ v e. B)) -> (A.x e. J A.y e. x E.z e. B (y e. z /\ z C_ x) -> A.y e. (w i^i v)E.z e. B (y e. z /\ z C_ (w i^i v))))
1514r19.21advva 2185 . . . . 5 |- ((J e. Top /\ B C_ J) -> (A.x e. J A.y e. x E.z e. B (y e. z /\ z C_ x) -> A.w e. B A.v e. B A.y e. (w i^i v)E.z e. B (y e. z /\ z C_ (w i^i v))))
16 ssexg 3457 . . . . . . 7 |- ((B C_ J /\ J e. Top) -> B e. _V)
1716ancoms 484 . . . . . 6 |- ((J e. Top /\ B C_ J) -> B e. _V)
18 isbasis2g 8881 . . . . . 6 |- (B e. _V -> (B e. Bases <-> A.w e. B A.v e. B A.y e. (w i^i v)E.z e. B (y e. z /\ z C_ (w i^i v))))
1917, 18syl 12 . . . . 5 |- ((J e. Top /\ B C_ J) -> (B e. Bases <-> A.w e. B A.v e. B A.y e. (w i^i v)E.z e. B (y e. z /\ z C_ (w i^i v))))
2015, 19sylibrd 221 . . . 4 |- ((J e. Top /\ B C_ J) -> (A.x e. J A.y e. x E.z e. B (y e. z /\ z C_ x) -> B e. Bases))
2120imp 377 . . 3 |- (((J e. Top /\ B C_ J) /\ A.x e. J A.y e. x E.z e. B (y e. z /\ z C_ x)) -> B e. Bases)
22 eltg3 8896 . . . . . . . 8 |- (B e. Bases -> (x e. (topGen` B) <-> E.y(y C_ B /\ x = U.y)))
2322adantl 424 . . . . . . 7 |- (((J e. Top /\ B C_ J) /\ B e. Bases) -> (x e. (topGen` B) <-> E.y(y C_ B /\ x = U.y)))
24 simpr 350 . . . . . . . . . . . . 13 |- (((J e. Top /\ (y C_ B /\ B C_ J)) /\ x = U.y) -> x = U.y)
25 uniopn 8867 . . . . . . . . . . . . . . 15 |- ((J e. Top /\ y C_ J) -> U.y e. J)
26 sstr 2625 . . . . . . . . . . . . . . 15 |- ((y C_ B /\ B C_ J) -> y C_ J)
2725, 26sylan2 500 . . . . . . . . . . . . . 14 |- ((J e. Top /\ (y C_ B /\ B C_ J)) -> U.y e. J)
2827adantr 425 . . . . . . . . . . . . 13 |- (((J e. Top /\ (y C_ B /\ B C_ J)) /\ x = U.y) -> U.y e. J)
2924, 28eqeltrd 1971 . . . . . . . . . . . 12 |- (((J e. Top /\ (y C_ B /\ B C_ J)) /\ x = U.y) -> x e. J)
3029exp42 414 . . . . . . . . . . 11 |- (J e. Top -> (y C_ B -> (B C_ J -> (x = U.y -> x e. J))))
3130com23 36 . . . . . . . . . 10 |- (J e. Top -> (B C_ J -> (y C_ B -> (x = U.y -> x e. J))))
3231imp4b 392 . . . . . . . . 9 |- ((J e. Top /\ B C_ J) -> ((y C_ B /\ x = U.y) -> x e. J))
333219.23adv 1584 . . . . . . . 8 |- ((J e. Top /\ B C_ J) -> (E.y(y C_ B /\ x = U.y) -> x e. J))
3433adantr 425 . . . . . . 7 |- (((J e. Top /\ B C_ J) /\ B e. Bases) -> (E.y(y C_ B /\ x = U.y) -> x e. J))
3523, 34sylbid 220 . . . . . 6 |- (((J e. Top /\ B C_ J) /\ B e. Bases) -> (x e. (topGen` B) -> x e. J))
3635ssrdv 2622 . . . . 5 |- (((J e. Top /\ B C_ J) /\ B e. Bases) -> (topGen` B) C_ J)
3721, 36syldan 516 . . . 4 |- (((J e. Top /\ B C_ J) /\ A.x e. J A.y e. x E.z e. B (y e. z /\ z C_ x)) -> (topGen` B) C_ J)
38 tgtop 8898 . . . . . 6 |- (J e. Top -> (topGen` J) = J)
3938ad2antrr 440 . . . . 5 |- (((J e. Top /\ B C_ J) /\ A.x e. J A.y e. x E.z e. B (y e. z /\ z C_ x)) -> (topGen` J) = J)
40 topbas 8897 . . . . . . . 8 |- (J e. Top -> J e. Bases)
4140ad2antrr 440 . . . . . . 7 |- (((J e. Top /\ B C_ J) /\ A.x e. J A.y e. x E.z e. B (y e. z /\ z C_ x)) -> J e. Bases)
42 eqid 1884 . . . . . . . . . . . . 13 |- U.J = U.J
4342topopn 8871 . . . . . . . . . . . 12 |- (J e. Top -> U.J e. J)
44 raleq 2266 . . . . . . . . . . . . . . 15 |- (x = U.J -> (A.y e. x E.z e. B y e. z <-> A.y e. U.JE.z e. B y e. z))
4544rcla4v 2376 . . . . . . . . . . . . . 14 |- (U.J e. J -> (A.x e. J A.y e. x E.z e. B y e. z -> A.y e. U.JE.z e. B y e. z))
46 elequ1 1496 . . . . . . . . . . . . . . . . 17 |- (y = w -> (y e. z <-> w e. z))
4746rexbidv 2124 . . . . . . . . . . . . . . . 16 |- (y = w -> (E.z e. B y e. z <-> E.z e. B w e. z))
4847rcla4cv 2377 . . . . . . . . . . . . . . 15 |- (A.y e. U.JE.z e. B y e. z -> (w e. U.J -> E.z e. B w e. z))
49 eluni2 3181 . . . . . . . . . . . . . . 15 |- (w e. U.B <-> E.z e. B w e. z)
5048, 49syl6ibr 230 . . . . . . . . . . . . . 14 |- (A.y e. U.JE.z e. B y e. z -> (w e. U.J -> w e. U.B))
5145, 50syl6 25 . . . . . . . . . . . . 13 |- (U.J e. J -> (A.x e. J A.y e. x E.z e. B y e. z -> (w e. U.J -> w e. U.B)))
52 simpl 346 . . . . . . . . . . . . . . . 16 |- ((y e. z /\ z C_ x) -> y e. z)
5352reximi 2198 . . . . . . . . . . . . . . 15 |- (E.z e. B (y e. z /\ z C_ x) -> E.z e. B y e. z)
5453ralimi 2168 . . . . . . . . . . . . . 14 |- (A.y e. x E.z e. B (y e. z /\ z C_ x) -> A.y e. x E.z e. B y e. z)
5554ralimi 2168 . . . . . . . . . . . . 13 |- (A.x e. J A.y e. x E.z e. B (y e. z /\ z C_ x) -> A.x e. J A.y e. x E.z e. B y e. z)
5651, 55syl5 20 . . . . . . . . . . . 12 |- (U.J e. J -> (A.x e. J A.y e. x E.z e. B (y e. z /\ z C_ x) -> (w e. U.J -> w e. U.B)))
5743, 56syl 12 . . . . . . . . . . 11 |- (J e. Top -> (A.x e. J A.y e. x E.z e. B (y e. z /\ z C_ x) -> (w e. U.J -> w e. U.B)))
5857imp 377 . . . . . . . . . 10 |- ((J e. Top /\ A.x e. J A.y e. x E.z e. B (y e. z /\ z C_ x)) -> (w e. U.J -> w e. U.B))
5958ssrdv 2622 . . . . . . . . 9 |- ((J e. Top /\ A.x e. J A.y e. x E.z e. B (y e. z /\ z C_ x)) -> U.J C_ U.B)
6059adantlr 429 . . . . . . . 8 |- (((J e. Top /\ B C_ J) /\ A.x e. J A.y e. x E.z e. B (y e. z /\ z C_ x)) -> U.J C_ U.B)
61 uniss 3199 . . . . . . . . 9 |- (B C_ J -> U.B C_ U.J)
6261ad2antlr 441 . . . . . . . 8 |- (((J e. Top /\ B C_ J) /\ A.x e. J A.y e. x E.z e. B (y e. z /\ z C_ x)) -> U.B C_ U.J)
6360, 62eqssd 2633 . . . . . . 7 |- (((J e. Top /\ B C_ J) /\ A.x e. J A.y e. x E.z e. B (y e. z /\ z C_ x)) -> U.J = U.B)
6441, 21, 63jca31 311 . . . . . 6 |- (((J e. Top /\ B C_ J) /\ A.x e. J A.y e. x E.z e. B (y e. z /\ z C_ x)) -> ((J e. Bases /\ B e. Bases) /\ U.J = U.B))
65 ax-1 4 . . . . . . . . . 10 |- ((y e. x -> E.z e. B (y e. z /\ z C_ x)) -> (y e. U.J -> (y e. x -> E.z e. B (y e. z /\ z C_ x))))
6665ralimi2 2165 . . . . . . . . 9 |- (A.y e. x E.z e. B (y e. z /\ z C_ x) -> A.y e. U.J(y e. x -> E.z e. B (y e. z /\ z C_ x)))
6766ralimi 2168 . . . . . . . 8 |- (A.x e. J A.y e. x E.z e. B (y e. z /\ z C_ x) -> A.x e. J A.y e. U.J(y e. x -> E.z e. B (y e. z /\ z C_ x)))
68 ralcom 2242 . . . . . . . 8 |- (A.x e. J A.y e. U.J(y e. x -> E.z e. B (y e. z /\ z C_ x)) <-> A.y e. U.JA.x e. J (y e. x -> E.z e. B (y e. z /\ z C_ x)))
6967, 68sylib 215 . . . . . . 7 |- (A.x e. J A.y e. x E.z e. B (y e. z /\ z C_ x) -> A.y e. U.JA.x e. J (y e. x -> E.z e. B (y e. z /\ z C_ x)))
7069adantl 424 . . . . . 6 |- (((J e. Top /\ B C_ J) /\ A.x e. J A.y e. x E.z e. B (y e. z /\ z C_ x)) -> A.y e. U.JA.x e. J (y e. x -> E.z e. B (y e. z /\ z C_ x)))
71 tgss2 8907 . . . . . . . 8 |- ((J e. Bases /\ B e. Bases /\ U.J = U.B) -> ((topGen` J) C_ (topGen` B) <-> A.y e. U.JA.x e. J (y e. x -> E.z e. B (y e. z /\ z C_ x))))
72713expa 1067 . . . . . . 7 |- (((J e. Bases /\ B e. Bases) /\ U.J = U.B) -> ((topGen` J) C_ (topGen` B) <-> A.y e. U.JA.x e. J (y e. x -> E.z e. B (y e. z /\ z C_ x))))
7372biimpar 461 . . . . . 6 |- ((((J e. Bases /\ B e. Bases) /\ U.J = U.B) /\ A.y e. U.JA.x e. J (y e. x -> E.z e. B (y e. z /\ z C_ x))) -> (topGen` J) C_ (topGen` B))
7464, 70, 73syl11anc 524 . . . . 5 |- (((J e. Top /\ B C_ J) /\ A.x e. J A.y e. x E.z e. B (y e. z /\ z C_ x)) -> (topGen` J) C_ (topGen` B))
7539, 74eqsstr3d 2652 . . . 4 |- (((J e. Top /\ B C_ J) /\ A.x e. J A.y e. x E.z e. B (y e. z /\ z C_ x)) -> J C_ (topGen` B))
7637, 75eqssd 2633 . . 3 |- (((J e. Top /\ B C_ J) /\ A.x e. J A.y e. x E.z e. B (y e. z /\ z C_ x)) -> (topGen` B) = J)
7721, 76jca 310 . 2 |- (((J e. Top /\ B C_ J) /\ A.x e. J A.y e. x E.z e. B (y e. z /\ z C_ x)) -> (B e. Bases /\ (topGen` B) = J))
78773impa 1062 1 |- ((J e. Top /\ B C_ J /\ A.x e. J A.y e. x E.z e. B (y e. z /\ z C_ x)) -> (B e. Bases /\ (topGen` B) = J))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  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:  basgen 8910  bastop1 8912  tgbl 9148  blbas 9149  2ndcctbss 15478  topfneec 15501
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