Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Mario Carneiro
Covering maps
cvmsn0
Next ⟩
cvmsuni
Metamath Proof Explorer
Ascii
Unicode
Theorem
cvmsn0
Description:
An even covering is nonempty.
(Contributed by
Mario Carneiro
, 11-Feb-2015)
Ref
Expression
Hypothesis
cvmcov.1
⊢
S
=
k
∈
J
⟼
s
∈
𝒫
C
∖
∅
|
⋃
s
=
F
-1
k
∧
∀
u
∈
s
∀
v
∈
s
∖
u
u
∩
v
=
∅
∧
F
↾
u
∈
C
↾
𝑡
u
Homeo
J
↾
𝑡
k
Assertion
cvmsn0
⊢
T
∈
S
⁡
U
→
T
≠
∅
Proof
Step
Hyp
Ref
Expression
1
cvmcov.1
⊢
S
=
k
∈
J
⟼
s
∈
𝒫
C
∖
∅
|
⋃
s
=
F
-1
k
∧
∀
u
∈
s
∀
v
∈
s
∖
u
u
∩
v
=
∅
∧
F
↾
u
∈
C
↾
𝑡
u
Homeo
J
↾
𝑡
k
2
1
cvmsi
⊢
T
∈
S
⁡
U
→
U
∈
J
∧
T
⊆
C
∧
T
≠
∅
∧
⋃
T
=
F
-1
U
∧
∀
u
∈
T
∀
v
∈
T
∖
u
u
∩
v
=
∅
∧
F
↾
u
∈
C
↾
𝑡
u
Homeo
J
↾
𝑡
U
3
2
simp2d
⊢
T
∈
S
⁡
U
→
T
⊆
C
∧
T
≠
∅
4
3
simprd
⊢
T
∈
S
⁡
U
→
T
≠
∅