HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem basgen2t 7639
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
basgen2t |- ((J e. Top /\ B (_ J /\ A.x e. J A.y e. x E.z e. B (y e. z /\ z (_ x)) -> (B e. Bases /\ (topGen` B) = J))
Distinct variable groups:   x,y,z,B   x,J,y,z
Proof of Theorem basgen2t
StepHypRef Expression
1 inopnt 7600 . . . . . . . . . 10 |- ((J e. Top /\ w e. J /\ v e. J) -> (w i^i v) e. J)
213expb 834 . . . . . . . . 9 |- ((J e. Top /\ (w e. J /\ v e. J)) -> (w i^i v) e. J)
3 ssel 2063 . . . . . . . . . . 11 |- (B (_ J -> (w e. B -> w e. J))
4 ssel 2063 . . . . . . . . . . 11 |- (B (_ J -> (v e. B -> v e. J))
53, 4anim12d 558 . . . . . . . . . 10 |- (B (_ J -> ((w e. B /\ v e. B) -> (w e. J /\ v e. J)))
65imp 350 . . . . . . . . 9 |- ((B (_ J /\ (w e. B /\ v e. B)) -> (w e. J /\ v e. J))
72, 6sylan2 451 . . . . . . . 8 |- ((J e. Top /\ (B (_ J /\ (w e. B /\ v e. B))) -> (w i^i v) e. J)
87anassrs 441 . . . . . . 7 |- (((J e. Top /\ B (_ J) /\ (w e. B /\ v e. B)) -> (w i^i v) e. J)
9 sseq2 2083 . . . . . . . . . . 11 |- (x = (w i^i v) -> (z (_ x <-> z (_ (w i^i v)))
109anbi2d 616 . . . . . . . . . 10 |- (x = (w i^i v) -> ((y e. z /\ z (_ x) <-> (y e. z /\ z (_ (w i^i v))))
1110rexbidv 1664 . . . . . . . . 9 |- (x = (w i^i v) -> (E.z e. B (y e. z /\ z (_ x) <-> E.z e. B (y e. z /\ z (_ (w i^i v))))
1211raleqd 1791 . . . . . . . 8 |- (x = (w i^i v) -> (A.y e. x E.z e. B (y e. z /\ z (_ x) <-> A.y e. (w i^i v)E.z e. B (y e. z /\ z (_ (w i^i v))))
1312rcla4v 1873 . . . . . . 7 |- ((w i^i v) e. J -> (A.x e. J A.y e. x E.z e. B (y e. z /\ z (_ x) -> A.y e. (w i^i v)E.z e. B (y e. z /\ z (_ (w i^i v))))
148, 13syl 10 . . . . . 6 |- (((J e. Top /\ B (_ J) /\ (w e. B /\ v e. B)) -> (A.x e. J A.y e. x E.z e. B (y e. z /\ z (_ x) -> A.y e. (w i^i v)E.z e. B (y e. z /\ z (_ (w i^i v))))
1514r19.21advva 1722 . . . . 5 |- ((J e. Top /\ B (_ J) -> (A.x e. J A.y e. x E.z e. B (y e. z /\ z (_ x) -> A.w e. B A.v e. B A.y e. (w i^i v)E.z e. B (y e. z /\ z (_ (w i^i v))))
16 ssexg 2721 . . . . . . 7 |- ((B (_ J /\ J e. Top) -> B e. V)
1716ancoms 436 . . . . . 6 |- ((J e. Top /\ B (_ J) -> B e. V)
18 isbasis2g 7612 . . . . . 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 (_ (w i^i v))))
1917, 18syl 10 . . . . 5 |- ((J e. Top /\ B (_ 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 (_ (w i^i v))))
2015, 19sylibrd 204 . . . 4 |- ((J e. Top /\ B (_ J) -> (A.x e. J A.y e. x E.z e. B (y e. z /\ z (_ x) -> B e. Bases))
2120imp 350 . . 3 |- (((J e. Top /\ B (_ J) /\ A.x e. J A.y e. x E.z e. B (y e. z /\ z (_ x)) -> B e. Bases)
22 eltg3t 7626 . . . . . . . 8 |- (B e. Bases -> (x e. (topGen` B) <-> E.y(y (_ B /\ x = U.y)))
2322adantl 388 . . . . . . 7 |- (((J e. Top /\ B (_ J) /\ B e. Bases) -> (x e. (topGen` B) <-> E.y(y (_ B /\ x = U.y)))
24 pm3.27 323 . . . . . . . . . . . . 13 |- (((J e. Top /\ (y (_ B /\ B (_ J)) /\ x = U.y) -> x = U.y)
25 uniopnt 7598 . . . . . . . . . . . . . . 15 |- ((J e. Top /\ y (_ J) -> U.y e. J)
26 sstr 2072 . . . . . . . . . . . . . . 15 |- ((y (_ B /\ B (_ J) -> y (_ J)
2725, 26sylan2 451 . . . . . . . . . . . . . 14 |- ((J e. Top /\ (y (_ B /\ B (_ J)) -> U.y e. J)
2827adantr 389 . . . . . . . . . . . . 13 |- (((J e. Top /\ (y (_ B /\ B (_ J)) /\ x = U.y) -> U.y e. J)
2924, 28eqeltrd 1548 . . . . . . . . . . . 12 |- (((J e. Top /\ (y (_ B /\ B (_ J)) /\ x = U.y) -> x e. J)
3029exp42 383 . . . . . . . . . . 11 |- (J e. Top -> (y (_ B -> (B (_ J -> (x = U.y -> x e. J))))
3130com23 32 . . . . . . . . . 10 |- (J e. Top -> (B (_ J -> (y (_ B -> (x = U.y -> x e. J))))
3231imp4b 365 . . . . . . . . 9 |- ((J e. Top /\ B (_ J) -> ((y (_ B /\ x = U.y) -> x e. J))
333219.23adv 1214 . . . . . . . 8 |- ((J e. Top /\ B (_ J) -> (E.y(y (_ B /\ x = U.y) -> x e. J))
3433adantr 389 . . . . . . 7 |- (((J e. Top /\ B (_ J) /\ B e. Bases) -> (E.y(y (_ B /\ x = U.y) -> x e. J))
3523, 34sylbid 203 . . . . . 6 |- (((J e. Top /\ B (_ J) /\ B e. Bases) -> (x e. (topGen` B) -> x e. J))
3635ssrdv 2070 . . . . 5 |- (((J e. Top /\ B (_ J) /\ B e. Bases) -> (topGen` B) (_ J)
3721, 36syldan 467 . . . 4 |- (((J e. Top /\ B (_ J) /\ A.x e. J A.y e. x E.z e. B (y e. z /\ z (_ x)) -> (topGen` B) (_ J)
38 tgtopt 7628 . . . . . 6 |- (J e. Top -> (topGen` J) = J)
3938ad2antrr 404 . . . . 5 |- (((J e. Top /\ B (_ J) /\ A.x e. J A.y e. x E.z e. B (y e. z /\ z (_ x)) -> (topGen` J) = J)
40 tgss2t 7637 . . . . . . . 8 |- ((J e. Bases /\ B e. Bases /\ U.J = U.B) -> ((topGen` J) (_ (topGen` B) <-> A.y e. U.JA.x e. J (y e. x -> E.z e. B (y e. z /\ z (_ x))))
41403expa 833 . . . . . . 7 |- (((J e. Bases /\ B e. Bases) /\ U.J = U.B) -> ((topGen` J) (_ (topGen` B) <-> A.y e. U.JA.x e. J (y e. x -> E.z e. B (y e. z /\ z (_ x))))
4241biimpar 417 . . . . . 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 (_ x))) -> (topGen` J) (_ (topGen` B))
43 topbast 7627 . . . . . . . . 9 |- (J e. Top -> J e. Bases)
4443ad2antrr 404 . . . . . . . 8 |- (((J e. Top /\ B (_ J) /\ A.x e. J A.y e. x E.z e. B (y e. z /\ z (_ x)) -> J e. Bases)
4544, 21jca 288 . . . . . . 7 |- (((J e. Top /\ B (_ J) /\ A.x e. J A.y e. x E.z e. B (y e. z /\ z (_ x)) -> (J e. Bases /\ B e. Bases))
46 eqid 1475 . . . . . . . . . . . . 13 |- U.J = U.J
4746topopn 7602 . . . . . . . . . . . 12 |- (J e. Top -> U.J e. J)
48 raleq1 1786 . . . . . . . . . . . . . . 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))
4948rcla4v 1873 . . . . . . . . . . . . . 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))
50 elequ1 1136 . . . . . . . . . . . . . . . . 17 |- (y = w -> (y e. z <-> w e. z))
5150rexbidv 1664 . . . . . . . . . . . . . . . 16 |- (y = w -> (E.z e. B y e. z <-> E.z e. B w e. z))
5251rcla4cv 1874 . . . . . . . . . . . . . . 15 |- (A.y e. U.JE.z e. B y e. z -> (w e. U.J -> E.z e. B w e. z))
53 eluni2 2507 . . . . . . . . . . . . . . 15 |- (w e. U.B <-> E.z e. B w e. z)
5452, 53syl6ibr 213 . . . . . . . . . . . . . 14 |- (A.y e. U.JE.z e. B y e. z -> (w e. U.J -> w e. U.B))
5549, 54syl6 22 . . . . . . . . . . . . 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)))
56 pm3.26 319 . . . . . . . . . . . . . . . 16 |- ((y e. z /\ z (_ x) -> y e. z)
5756r19.22si 1734 . . . . . . . . . . . . . . 15 |- (E.z e. B (y e. z /\ z (_ x) -> E.z e. B y e. z)
5857r19.20si 1706 . . . . . . . . . . . . . 14 |- (A.y e. x E.z e. B (y e. z /\ z (_ x) -> A.y e. x E.z e. B y e. z)
5958r19.20si 1706 . . . . . . . . . . . . 13 |- (A.x e. J A.y e. x E.z e. B (y e. z /\ z (_ x) -> A.x e. J A.y e. x E.z e. B y e. z)
6055, 59syl5 21 . . . . . . . . . . . 12 |- (U.J e. J -> (A.x e. J A.y e. x E.z e. B (y e. z /\ z (_ x) -> (w e. U.J -> w e. U.B)))
6147, 60syl 10 . . . . . . . . . . 11 |-