Metamath Proof Explorer


Theorem baspartn

Description: A disjoint system of sets is a basis for a topology. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Assertion baspartn PVxPyPx=yxy=PTopBases

Proof

Step Hyp Ref Expression
1 id xPxP
2 pwidg xPx𝒫x
3 1 2 elind xPxP𝒫x
4 elssuni xP𝒫xxP𝒫x
5 3 4 syl xPxP𝒫x
6 inidm xx=x
7 ineq2 x=yxx=xy
8 6 7 eqtr3id x=yx=xy
9 8 pweqd x=y𝒫x=𝒫xy
10 9 ineq2d x=yP𝒫x=P𝒫xy
11 10 unieqd x=yP𝒫x=P𝒫xy
12 8 11 sseq12d x=yxP𝒫xxyP𝒫xy
13 5 12 syl5ibcom xPx=yxyP𝒫xy
14 0ss P𝒫xy
15 sseq1 xy=xyP𝒫xyP𝒫xy
16 14 15 mpbiri xy=xyP𝒫xy
17 16 a1i xPxy=xyP𝒫xy
18 13 17 jaod xPx=yxy=xyP𝒫xy
19 18 ralimdv xPyPx=yxy=yPxyP𝒫xy
20 19 ralimia xPyPx=yxy=xPyPxyP𝒫xy
21 20 adantl PVxPyPx=yxy=xPyPxyP𝒫xy
22 isbasisg PVPTopBasesxPyPxyP𝒫xy
23 22 adantr PVxPyPx=yxy=PTopBasesxPyPxyP𝒫xy
24 21 23 mpbird PVxPyPx=yxy=PTopBases