Description: A disjoint system of sets is a basis for a topology. (Contributed by Stefan O'Rear, 22-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | baspartn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | |
|
2 | pwidg | |
|
3 | 1 2 | elind | |
4 | elssuni | |
|
5 | 3 4 | syl | |
6 | inidm | |
|
7 | ineq2 | |
|
8 | 6 7 | eqtr3id | |
9 | 8 | pweqd | |
10 | 9 | ineq2d | |
11 | 10 | unieqd | |
12 | 8 11 | sseq12d | |
13 | 5 12 | syl5ibcom | |
14 | 0ss | |
|
15 | sseq1 | |
|
16 | 14 15 | mpbiri | |
17 | 16 | a1i | |
18 | 13 17 | jaod | |
19 | 18 | ralimdv | |
20 | 19 | ralimia | |
21 | 20 | adantl | |
22 | isbasisg | |
|
23 | 22 | adantr | |
24 | 21 23 | mpbird | |