This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐵 ∖ { ∅ } ) ∈ TopBases ↔ 𝐵 ∈ TopBases )

Proof

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