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

Theorem baspartn 17011
 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 20 . . . . . . . . 9
2 pwidg 3803 . . . . . . . . 9
3 elin 3522 . . . . . . . . 9
41, 2, 3sylanbrc 646 . . . . . . . 8
5 elssuni 4035 . . . . . . . 8
64, 5syl 16 . . . . . . 7
7 inidm 3542 . . . . . . . . 9
8 ineq2 3528 . . . . . . . . 9
97, 8syl5eqr 2481 . . . . . . . 8
109pweqd 3796 . . . . . . . . . 10
1110ineq2d 3534 . . . . . . . . 9
1211unieqd 4018 . . . . . . . 8
139, 12sseq12d 3369 . . . . . . 7
146, 13syl5ibcom 212 . . . . . 6
15 0ss 3648 . . . . . . . 8
16 sseq1 3361 . . . . . . . 8
1715, 16mpbiri 225 . . . . . . 7
1817a1i 11 . . . . . 6
1914, 18jaod 370 . . . . 5
2019ralimdv 2777 . . . 4
2120ralimia 2771 . . 3