Metamath Proof Explorer


Theorem fncvm

Description: Lemma for covering maps. (Contributed by Mario Carneiro, 13-Feb-2015)

Ref Expression
Assertion fncvm CovMapFnTop×Top

Proof

Step Hyp Ref Expression
1 df-cvm CovMap=cTop,jTopfcCnj|xjkjxks𝒫cs=f-1kusvsuuv=fuc𝑡uHomeoj𝑡k
2 ovex cCnjV
3 2 rabex fcCnj|xjkjxks𝒫cs=f-1kusvsuuv=fuc𝑡uHomeoj𝑡kV
4 1 3 fnmpoi CovMapFnTop×Top