Database
BASIC TOPOLOGY
Topology
Topological bases
basis1
Next ⟩
basis2
Metamath Proof Explorer
Ascii
Unicode
Theorem
basis1
Description:
Property of a basis.
(Contributed by
NM
, 16-Jul-2006)
Ref
Expression
Assertion
basis1
⊢
B
∈
TopBases
∧
C
∈
B
∧
D
∈
B
→
C
∩
D
⊆
⋃
B
∩
𝒫
C
∩
D
Proof
Step
Hyp
Ref
Expression
1
isbasisg
⊢
B
∈
TopBases
→
B
∈
TopBases
↔
∀
x
∈
B
∀
y
∈
B
x
∩
y
⊆
⋃
B
∩
𝒫
x
∩
y
2
1
ibi
⊢
B
∈
TopBases
→
∀
x
∈
B
∀
y
∈
B
x
∩
y
⊆
⋃
B
∩
𝒫
x
∩
y
3
ineq1
⊢
x
=
C
→
x
∩
y
=
C
∩
y
4
3
pweqd
⊢
x
=
C
→
𝒫
x
∩
y
=
𝒫
C
∩
y
5
4
ineq2d
⊢
x
=
C
→
B
∩
𝒫
x
∩
y
=
B
∩
𝒫
C
∩
y
6
5
unieqd
⊢
x
=
C
→
⋃
B
∩
𝒫
x
∩
y
=
⋃
B
∩
𝒫
C
∩
y
7
3
6
sseq12d
⊢
x
=
C
→
x
∩
y
⊆
⋃
B
∩
𝒫
x
∩
y
↔
C
∩
y
⊆
⋃
B
∩
𝒫
C
∩
y
8
ineq2
⊢
y
=
D
→
C
∩
y
=
C
∩
D
9
8
pweqd
⊢
y
=
D
→
𝒫
C
∩
y
=
𝒫
C
∩
D
10
9
ineq2d
⊢
y
=
D
→
B
∩
𝒫
C
∩
y
=
B
∩
𝒫
C
∩
D
11
10
unieqd
⊢
y
=
D
→
⋃
B
∩
𝒫
C
∩
y
=
⋃
B
∩
𝒫
C
∩
D
12
8
11
sseq12d
⊢
y
=
D
→
C
∩
y
⊆
⋃
B
∩
𝒫
C
∩
y
↔
C
∩
D
⊆
⋃
B
∩
𝒫
C
∩
D
13
7
12
rspc2v
⊢
C
∈
B
∧
D
∈
B
→
∀
x
∈
B
∀
y
∈
B
x
∩
y
⊆
⋃
B
∩
𝒫
x
∩
y
→
C
∩
D
⊆
⋃
B
∩
𝒫
C
∩
D
14
2
13
syl5com
⊢
B
∈
TopBases
→
C
∈
B
∧
D
∈
B
→
C
∩
D
⊆
⋃
B
∩
𝒫
C
∩
D
15
14
3impib
⊢
B
∈
TopBases
∧
C
∈
B
∧
D
∈
B
→
C
∩
D
⊆
⋃
B
∩
𝒫
C
∩
D