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 | |
|
Assertion | cvmsf1o | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cvmcov.1 | |
|
2 | cvmtop1 | |
|
3 | 2 | 3ad2ant1 | |
4 | eqid | |
|
5 | 4 | toptopon | |
6 | 3 5 | sylib | |
7 | 1 | cvmsss | |
8 | 7 | 3ad2ant2 | |
9 | simp3 | |
|
10 | 8 9 | sseldd | |
11 | elssuni | |
|
12 | 10 11 | syl | |
13 | resttopon | |
|
14 | 6 12 13 | syl2anc | |
15 | cvmtop2 | |
|
16 | 15 | 3ad2ant1 | |
17 | eqid | |
|
18 | 17 | toptopon | |
19 | 16 18 | sylib | |
20 | 1 | cvmsrcl | |
21 | 20 | 3ad2ant2 | |
22 | elssuni | |
|
23 | 21 22 | syl | |
24 | resttopon | |
|
25 | 19 23 24 | syl2anc | |
26 | 1 | cvmshmeo | |
27 | 26 | 3adant1 | |
28 | hmeof1o2 | |
|
29 | 14 25 27 28 | syl3anc | |