Metamath Proof Explorer


Theorem basdif0

Description: A basis is not affected by the addition or removal of the empty set. (Contributed by Mario Carneiro, 28-Aug-2015)

Ref Expression
Assertion basdif0 BTopBasesBTopBases

Proof

Step Hyp Ref Expression
1 ssun1 BB
2 undif1 B=B
3 1 2 sseqtrri BB
4 snex V
5 unexg BTopBasesVBV
6 4 5 mpan2 BTopBasesBV
7 ssexg BBBVBV
8 3 6 7 sylancr BTopBasesBV
9 elex BTopBasesBV
10 indif1 B𝒫xy=B𝒫xy
11 10 unieqi B𝒫xy=B𝒫xy
12 unidif0 B𝒫xy=B𝒫xy
13 11 12 eqtri B𝒫xy=B𝒫xy
14 13 sseq2i xyB𝒫xyxyB𝒫xy
15 14 ralbii yBxyB𝒫xyyBxyB𝒫xy
16 inss2 xyy
17 elinel2 yBy
18 elsni yy=
19 17 18 syl yBy=
20 0ss B𝒫xy
21 19 20 eqsstrdi yByB𝒫xy
22 16 21 sstrid yBxyB𝒫xy
23 22 rgen yBxyB𝒫xy
24 ralunb yBBxyB𝒫xyyBxyB𝒫xyyBxyB𝒫xy
25 23 24 mpbiran yBBxyB𝒫xyyBxyB𝒫xy
26 inundif BB=B
27 26 raleqi yBBxyB𝒫xyyBxyB𝒫xy
28 15 25 27 3bitr2i yBxyB𝒫xyyBxyB𝒫xy
29 28 ralbii xByBxyB𝒫xyxByBxyB𝒫xy
30 inss1 xyx
31 elinel2 xBx
32 elsni xx=
33 31 32 syl xBx=
34 33 20 eqsstrdi xBxB𝒫xy
35 30 34 sstrid xBxyB𝒫xy
36 35 ralrimivw xByBxyB𝒫xy
37 36 rgen xByBxyB𝒫xy
38 ralunb xBByBxyB𝒫xyxByBxyB𝒫xyxByBxyB𝒫xy
39 37 38 mpbiran xBByBxyB𝒫xyxByBxyB𝒫xy
40 26 raleqi xBByBxyB𝒫xyxByBxyB𝒫xy
41 29 39 40 3bitr2i xByBxyB𝒫xyxByBxyB𝒫xy
42 41 a1i BVxByBxyB𝒫xyxByBxyB𝒫xy
43 difexg BVBV
44 isbasisg BVBTopBasesxByBxyB𝒫xy
45 43 44 syl BVBTopBasesxByBxyB𝒫xy
46 isbasisg BVBTopBasesxByBxyB𝒫xy
47 42 45 46 3bitr4d BVBTopBasesBTopBases
48 8 9 47 pm5.21nii BTopBasesBTopBases