Metamath Proof Explorer


Theorem cvmsrcl

Description: Reverse closure for an even covering. (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 cvmsrcl T S U U J

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 dmmptss dom S J
3 elfvdm T S U U dom S
4 2 3 sseldi T S U U J