Metamath Proof Explorer


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