Metamath Proof Explorer


Theorem cvmsn0

Description: An even covering is nonempty. (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypothesis cvmcov.1 S=kJs𝒫C|s=F-1kusvsuuv=FuC𝑡uHomeoJ𝑡k
Assertion cvmsn0 TSUT

Proof

Step Hyp Ref Expression
1 cvmcov.1 S=kJs𝒫C|s=F-1kusvsuuv=FuC𝑡uHomeoJ𝑡k
2 1 cvmsi TSUUJTCTT=F-1UuTvTuuv=FuC𝑡uHomeoJ𝑡U
3 2 simp2d TSUTCT
4 3 simprd TSUT