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 ⊢ B ∖ ∅ ∈ TopBases ↔ B ∈ TopBases

Proof

Step Hyp Ref Expression
1 ssun1 ⊢ B ⊆ B ∪ ∅
2 undif1 ⊢ B ∖ ∅ ∪ ∅ = B ∪ ∅
3 1 2 sseqtrri ⊢ B ⊆ B ∖ ∅ ∪ ∅
4 snex ⊢ ∅ ∈ V
5 unexg ⊢ B ∖ ∅ ∈ TopBases ∧ ∅ ∈ V → B ∖ ∅ ∪ ∅ ∈ V
6 4 5 mpan2 ⊢ B ∖ ∅ ∈ TopBases → B ∖ ∅ ∪ ∅ ∈ V
7 ssexg ⊢ B ⊆ B ∖ ∅ ∪ ∅ ∧ B ∖ ∅ ∪ ∅ ∈ V → B ∈ V
8 3 6 7 sylancr ⊢ B ∖ ∅ ∈ TopBases → B ∈ V
9 elex ⊢ B ∈ TopBases → B ∈ V
10 indif1 ⊢ B ∖ ∅ ∩ 𝒫 x ∩ y = B ∩ 𝒫 x ∩ y ∖ ∅
11 10 unieqi ⊢ ⋃ B ∖ ∅ ∩ 𝒫 x ∩ y = ⋃ B ∩ 𝒫 x ∩ y ∖ ∅
12 unidif0 ⊢ ⋃ B ∩ 𝒫 x ∩ y ∖ ∅ = ⋃ B ∩ 𝒫 x ∩ y
13 11 12 eqtri ⊢ ⋃ B ∖ ∅ ∩ 𝒫 x ∩ y = ⋃ B ∩ 𝒫 x ∩ y
14 13 sseq2i ⊢ x ∩ y ⊆ ⋃ B ∖ ∅ ∩ 𝒫 x ∩ y ↔ x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y
15 14 ralbii ⊢ ∀ y ∈ B ∖ ∅ x ∩ y ⊆ ⋃ B ∖ ∅ ∩ 𝒫 x ∩ y ↔ ∀ y ∈ B ∖ ∅ x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y
16 inss2 ⊢ x ∩ y ⊆ y
17 elinel2 ⊢ y ∈ B ∩ ∅ → y ∈ ∅
18 elsni ⊢ y ∈ ∅ → y = ∅
19 17 18 syl ⊢ y ∈ B ∩ ∅ → y = ∅
20 0ss ⊢ ∅ ⊆ ⋃ B ∩ 𝒫 x ∩ y
21 19 20 eqsstrdi ⊢ y ∈ B ∩ ∅ → y ⊆ ⋃ B ∩ 𝒫 x ∩ y
22 16 21 sstrid ⊢ y ∈ B ∩ ∅ → x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y
23 22 rgen ⊢ ∀ y ∈ B ∩ ∅ x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y
24 ralunb ⊢ ∀ y ∈ B ∩ ∅ ∪ B ∖ ∅ x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y ↔ ∀ y ∈ B ∩ ∅ x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y ∧ ∀ y ∈ B ∖ ∅ x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y
25 23 24 mpbiran ⊢ ∀ y ∈ B ∩ ∅ ∪ B ∖ ∅ x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y ↔ ∀ y ∈ B ∖ ∅ x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y
26 inundif ⊢ B ∩ ∅ ∪ B ∖ ∅ = B
27 26 raleqi ⊢ ∀ y ∈ B ∩ ∅ ∪ B ∖ ∅ x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y ↔ ∀ y ∈ B x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y
28 15 25 27 3bitr2i ⊢ ∀ y ∈ B ∖ ∅ x ∩ y ⊆ ⋃ B ∖ ∅ ∩ 𝒫 x ∩ y ↔ ∀ y ∈ B x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y
29 28 ralbii ⊢ ∀ x ∈ B ∖ ∅ ∀ y ∈ B ∖ ∅ x ∩ y ⊆ ⋃ B ∖ ∅ ∩ 𝒫 x ∩ y ↔ ∀ x ∈ B ∖ ∅ ∀ y ∈ B x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y
30 inss1 ⊢ x ∩ y ⊆ x
31 elinel2 ⊢ x ∈ B ∩ ∅ → x ∈ ∅
32 elsni ⊢ x ∈ ∅ → x = ∅
33 31 32 syl ⊢ x ∈ B ∩ ∅ → x = ∅
34 33 20 eqsstrdi ⊢ x ∈ B ∩ ∅ → x ⊆ ⋃ B ∩ 𝒫 x ∩ y
35 30 34 sstrid ⊢ x ∈ B ∩ ∅ → x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y
36 35 ralrimivw ⊢ x ∈ B ∩ ∅ → ∀ y ∈ B x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y
37 36 rgen ⊢ ∀ x ∈ B ∩ ∅ ∀ y ∈ B x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y
38 ralunb ⊢ ∀ x ∈ B ∩ ∅ ∪ B ∖ ∅ ∀ y ∈ B x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y ↔ ∀ x ∈ B ∩ ∅ ∀ y ∈ B x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y ∧ ∀ x ∈ B ∖ ∅ ∀ y ∈ B x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y
39 37 38 mpbiran ⊢ ∀ x ∈ B ∩ ∅ ∪ B ∖ ∅ ∀ y ∈ B x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y ↔ ∀ x ∈ B ∖ ∅ ∀ y ∈ B x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y
40 26 raleqi ⊢ ∀ x ∈ B ∩ ∅ ∪ B ∖ ∅ ∀ y ∈ B x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y ↔ ∀ x ∈ B ∀ y ∈ B x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y
41 29 39 40 3bitr2i ⊢ ∀ x ∈ B ∖ ∅ ∀ y ∈ B ∖ ∅ x ∩ y ⊆ ⋃ B ∖ ∅ ∩ 𝒫 x ∩ y ↔ ∀ x ∈ B ∀ y ∈ B x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y
42 41 a1i ⊢ B ∈ V → ∀ x ∈ B ∖ ∅ ∀ y ∈ B ∖ ∅ x ∩ y ⊆ ⋃ B ∖ ∅ ∩ 𝒫 x ∩ y ↔ ∀ x ∈ B ∀ y ∈ B x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y
43 difexg ⊢ B ∈ V → B ∖ ∅ ∈ V
44 isbasisg ⊢ B ∖ ∅ ∈ V → B ∖ ∅ ∈ TopBases ↔ ∀ x ∈ B ∖ ∅ ∀ y ∈ B ∖ ∅ x ∩ y ⊆ ⋃ B ∖ ∅ ∩ 𝒫 x ∩ y
45 43 44 syl ⊢ B ∈ V → B ∖ ∅ ∈ TopBases ↔ ∀ x ∈ B ∖ ∅ ∀ y ∈ B ∖ ∅ x ∩ y ⊆ ⋃ B ∖ ∅ ∩ 𝒫 x ∩ y
46 isbasisg ⊢ B ∈ V → B ∈ TopBases ↔ ∀ x ∈ B ∀ y ∈ B x ∩ y ⊆ ⋃ B ∩ 𝒫 x ∩ y
47 42 45 46 3bitr4d ⊢ B ∈ V → B ∖ ∅ ∈ TopBases ↔ B ∈ TopBases
48 8 9 47 pm5.21nii ⊢ B ∖ ∅ ∈ TopBases ↔ B ∈ TopBases