Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  baspartn Structured version   Visualization version   Unicode version

Theorem baspartn 19962
 Description: A disjoint system of sets is a basis for a topology. (Contributed by Stefan O'Rear, 22-Feb-2015.)
Assertion
Ref Expression
baspartn
Distinct variable group:   ,,
Allowed substitution hints:   (,)

Proof of Theorem baspartn
StepHypRef Expression
1 id 22 . . . . . . . . 9
2 pwidg 3963 . . . . . . . . 9
31, 2elind 3617 . . . . . . . 8
4 elssuni 4226 . . . . . . . 8
53, 4syl 17 . . . . . . 7
6 inidm 3640 . . . . . . . . 9
7 ineq2 3627 . . . . . . . . 9
86, 7syl5eqr 2498 . . . . . . . 8
98pweqd 3955 . . . . . . . . . 10
109ineq2d 3633 . . . . . . . . 9
1110unieqd 4207 . . . . . . . 8
128, 11sseq12d 3460 . . . . . . 7
135, 12syl5ibcom 224 . . . . . 6
14 0ss 3762 . . . . . . . 8
15 sseq1 3452 . . . . . . . 8
1614, 15mpbiri 237 . . . . . . 7
1716a1i 11 . . . . . 6
1813, 17jaod 382 . . . . 5
1918ralimdv 2797 . . . 4
2019ralimia 2778 . . 3