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 = ( k e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) } )
Assertion cvmsf1o 
|- ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( F |` A ) : A -1-1-onto-> U )

Proof

Step Hyp Ref Expression
1 cvmcov.1 
 |-  S = ( k e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) } )
2 cvmtop1 
 |-  ( F e. ( C CovMap J ) -> C e. Top )
3 2 3ad2ant1 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> C e. Top )
4 eqid 
 |-  U. C = U. C
5 4 toptopon 
 |-  ( C e. Top <-> C e. ( TopOn ` U. C ) )
6 3 5 sylib 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> C e. ( TopOn ` U. C ) )
7 1 cvmsss 
 |-  ( T e. ( S ` U ) -> T C_ C )
8 7 3ad2ant2 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> T C_ C )
9 simp3 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> A e. T )
10 8 9 sseldd 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> A e. C )
11 elssuni 
 |-  ( A e. C -> A C_ U. C )
12 10 11 syl 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> A C_ U. C )
13 resttopon 
 |-  ( ( C e. ( TopOn ` U. C ) /\ A C_ U. C ) -> ( C |`t A ) e. ( TopOn ` A ) )
14 6 12 13 syl2anc 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( C |`t A ) e. ( TopOn ` A ) )
15 cvmtop2 
 |-  ( F e. ( C CovMap J ) -> J e. Top )
16 15 3ad2ant1 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> J e. Top )
17 eqid 
 |-  U. J = U. J
18 17 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
19 16 18 sylib 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> J e. ( TopOn ` U. J ) )
20 1 cvmsrcl 
 |-  ( T e. ( S ` U ) -> U e. J )
21 20 3ad2ant2 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> U e. J )
22 elssuni 
 |-  ( U e. J -> U C_ U. J )
23 21 22 syl 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> U C_ U. J )
24 resttopon 
 |-  ( ( J e. ( TopOn ` U. J ) /\ U C_ U. J ) -> ( J |`t U ) e. ( TopOn ` U ) )
25 19 23 24 syl2anc 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( J |`t U ) e. ( TopOn ` U ) )
26 1 cvmshmeo 
 |-  ( ( T e. ( S ` U ) /\ A e. T ) -> ( F |` A ) e. ( ( C |`t A ) Homeo ( J |`t U ) ) )
27 26 3adant1 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( F |` A ) e. ( ( C |`t A ) Homeo ( J |`t U ) ) )
28 hmeof1o2 
 |-  ( ( ( C |`t A ) e. ( TopOn ` A ) /\ ( J |`t U ) e. ( TopOn ` U ) /\ ( F |` A ) e. ( ( C |`t A ) Homeo ( J |`t U ) ) ) -> ( F |` A ) : A -1-1-onto-> U )
29 14 25 27 28 syl3anc 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ A e. T ) -> ( F |` A ) : A -1-1-onto-> U )