Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Mario Carneiro
Covering maps
cvmtop2
Next ⟩
cvmcn
Metamath Proof Explorer
Ascii
Unicode
Theorem
cvmtop2
Description:
Reverse closure for a covering map.
(Contributed by
Mario Carneiro
, 13-Feb-2015)
Ref
Expression
Assertion
cvmtop2
⊢
F
∈
C
CovMap
J
→
J
∈
Top
Proof
Step
Hyp
Ref
Expression
1
n0i
⊢
F
∈
C
CovMap
J
→
¬
C
CovMap
J
=
∅
2
fncvm
⊢
CovMap
Fn
Top
×
Top
3
2
fndmi
⊢
dom
⁡
CovMap
=
Top
×
Top
4
3
ndmov
⊢
¬
C
∈
Top
∧
J
∈
Top
→
C
CovMap
J
=
∅
5
1
4
nsyl2
⊢
F
∈
C
CovMap
J
→
C
∈
Top
∧
J
∈
Top
6
5
simprd
⊢
F
∈
C
CovMap
J
→
J
∈
Top