Metamath Proof Explorer


Theorem cvmsf1o

Description: F , localized to an element of an even covering of U , is a bijection. (Contributed by Mario Carneiro, 14-Feb-2015)

Ref Expression
Hypothesis cvmcov.1 S=kJs𝒫C|s=F-1kusvsuuv=FuC𝑡uHomeoJ𝑡k
Assertion cvmsf1o FCCovMapJTSUATFA:A1-1 ontoU

Proof

Step Hyp Ref Expression
1 cvmcov.1 S=kJs𝒫C|s=F-1kusvsuuv=FuC𝑡uHomeoJ𝑡k
2 cvmtop1 FCCovMapJCTop
3 2 3ad2ant1 FCCovMapJTSUATCTop
4 eqid C=C
5 4 toptopon CTopCTopOnC
6 3 5 sylib FCCovMapJTSUATCTopOnC
7 1 cvmsss TSUTC
8 7 3ad2ant2 FCCovMapJTSUATTC
9 simp3 FCCovMapJTSUATAT
10 8 9 sseldd FCCovMapJTSUATAC
11 elssuni ACAC
12 10 11 syl FCCovMapJTSUATAC
13 resttopon CTopOnCACC𝑡ATopOnA
14 6 12 13 syl2anc FCCovMapJTSUATC𝑡ATopOnA
15 cvmtop2 FCCovMapJJTop
16 15 3ad2ant1 FCCovMapJTSUATJTop
17 eqid J=J
18 17 toptopon JTopJTopOnJ
19 16 18 sylib FCCovMapJTSUATJTopOnJ
20 1 cvmsrcl TSUUJ
21 20 3ad2ant2 FCCovMapJTSUATUJ
22 elssuni UJUJ
23 21 22 syl FCCovMapJTSUATUJ
24 resttopon JTopOnJUJJ𝑡UTopOnU
25 19 23 24 syl2anc FCCovMapJTSUATJ𝑡UTopOnU
26 1 cvmshmeo TSUATFAC𝑡AHomeoJ𝑡U
27 26 3adant1 FCCovMapJTSUATFAC𝑡AHomeoJ𝑡U
28 hmeof1o2 C𝑡ATopOnAJ𝑡UTopOnUFAC𝑡AHomeoJ𝑡UFA:A1-1 ontoU
29 14 25 27 28 syl3anc FCCovMapJTSUATFA:A1-1 ontoU