Metamath Proof Explorer

Theorem cvmfolem

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

Ref Expression
Hypotheses 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 ) ) ) ) } )
cvmseu.1 
|- B = U. C
cvmfolem.2 
|- X = U. J
Assertion cvmfolem 
|- ( F e. ( C CovMap J ) -> F : B -onto-> X )

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 cvmseu.1 
 |-  B = U. C
3 cvmfolem.2 
 |-  X = U. J
4 cvmcn 
 |-  ( F e. ( C CovMap J ) -> F e. ( C Cn J ) )
5 2 3 cnf 
 |-  ( F e. ( C Cn J ) -> F : B --> X )
6 4 5 syl 
 |-  ( F e. ( C CovMap J ) -> F : B --> X )
7 1 3 cvmcov 
 |-  ( ( F e. ( C CovMap J ) /\ x e. X ) -> E. z e. J ( x e. z /\ ( S ` z ) =/= (/) ) )
8 7 ex 
 |-  ( F e. ( C CovMap J ) -> ( x e. X -> E. z e. J ( x e. z /\ ( S ` z ) =/= (/) ) ) )
9 n0 
 |-  ( ( S ` z ) =/= (/) <-> E. w w e. ( S ` z ) )
10 1 cvmsn0 
 |-  ( w e. ( S ` z ) -> w =/= (/) )
11 10 ad2antll 
 |-  ( ( ( F e. ( C CovMap J ) /\ z e. J ) /\ ( x e. z /\ w e. ( S ` z ) ) ) -> w =/= (/) )
12 n0 
 |-  ( w =/= (/) <-> E. t t e. w )
13 11 12 sylib 
 |-  ( ( ( F e. ( C CovMap J ) /\ z e. J ) /\ ( x e. z /\ w e. ( S ` z ) ) ) -> E. t t e. w )
14 simprlr 
 |-  ( ( ( F e. ( C CovMap J ) /\ z e. J ) /\ ( ( x e. z /\ w e. ( S ` z ) ) /\ t e. w ) ) -> w e. ( S ` z ) )
15 1 cvmsss 
 |-  ( w e. ( S ` z ) -> w C_ C )
16 14 15 syl 
 |-  ( ( ( F e. ( C CovMap J ) /\ z e. J ) /\ ( ( x e. z /\ w e. ( S ` z ) ) /\ t e. w ) ) -> w C_ C )
17 simprr 
 |-  ( ( ( F e. ( C CovMap J ) /\ z e. J ) /\ ( ( x e. z /\ w e. ( S ` z ) ) /\ t e. w ) ) -> t e. w )
18 16 17 sseldd 
 |-  ( ( ( F e. ( C CovMap J ) /\ z e. J ) /\ ( ( x e. z /\ w e. ( S ` z ) ) /\ t e. w ) ) -> t e. C )
19 elssuni 
 |-  ( t e. C -> t C_ U. C )
20 18 19 syl 
 |-  ( ( ( F e. ( C CovMap J ) /\ z e. J ) /\ ( ( x e. z /\ w e. ( S ` z ) ) /\ t e. w ) ) -> t C_ U. C )
21 20 2 sseqtrrdi 
 |-  ( ( ( F e. ( C CovMap J ) /\ z e. J ) /\ ( ( x e. z /\ w e. ( S ` z ) ) /\ t e. w ) ) -> t C_ B )
22 simpll 
 |-  ( ( ( F e. ( C CovMap J ) /\ z e. J ) /\ ( ( x e. z /\ w e. ( S ` z ) ) /\ t e. w ) ) -> F e. ( C CovMap J ) )
23 1 cvmsf1o 
 |-  ( ( F e. ( C CovMap J ) /\ w e. ( S ` z ) /\ t e. w ) -> ( F |` t ) : t -1-1-onto-> z )
24 22 14 17 23 syl3anc 
 |-  ( ( ( F e. ( C CovMap J ) /\ z e. J ) /\ ( ( x e. z /\ w e. ( S ` z ) ) /\ t e. w ) ) -> ( F |` t ) : t -1-1-onto-> z )
25 f1ocnv 
 |-  ( ( F |` t ) : t -1-1-onto-> z -> `' ( F |` t ) : z -1-1-onto-> t )
26 f1of 
 |-  ( `' ( F |` t ) : z -1-1-onto-> t -> `' ( F |` t ) : z --> t )
27 24 25 26 3syl 
 |-  ( ( ( F e. ( C CovMap J ) /\ z e. J ) /\ ( ( x e. z /\ w e. ( S ` z ) ) /\ t e. w ) ) -> `' ( F |` t ) : z --> t )
28 simprll 
 |-  ( ( ( F e. ( C CovMap J ) /\ z e. J ) /\ ( ( x e. z /\ w e. ( S ` z ) ) /\ t e. w ) ) -> x e. z )
29 27 28 ffvelrnd 
 |-  ( ( ( F e. ( C CovMap J ) /\ z e. J ) /\ ( ( x e. z /\ w e. ( S ` z ) ) /\ t e. w ) ) -> ( `' ( F |` t ) ` x ) e. t )
30 21 29 sseldd 
 |-  ( ( ( F e. ( C CovMap J ) /\ z e. J ) /\ ( ( x e. z /\ w e. ( S ` z ) ) /\ t e. w ) ) -> ( `' ( F |` t ) ` x ) e. B )
31 f1ocnvfv2 
 |-  ( ( ( F |` t ) : t -1-1-onto-> z /\ x e. z ) -> ( ( F |` t ) ` ( `' ( F |` t ) ` x ) ) = x )
32 24 28 31 syl2anc 
 |-  ( ( ( F e. ( C CovMap J ) /\ z e. J ) /\ ( ( x e. z /\ w e. ( S ` z ) ) /\ t e. w ) ) -> ( ( F |` t ) ` ( `' ( F |` t ) ` x ) ) = x )
33 fvres 
 |-  ( ( `' ( F |` t ) ` x ) e. t -> ( ( F |` t ) ` ( `' ( F |` t ) ` x ) ) = ( F ` ( `' ( F |` t ) ` x ) ) )
34 29 33 syl 
 |-  ( ( ( F e. ( C CovMap J ) /\ z e. J ) /\ ( ( x e. z /\ w e. ( S ` z ) ) /\ t e. w ) ) -> ( ( F |` t ) ` ( `' ( F |` t ) ` x ) ) = ( F ` ( `' ( F |` t ) ` x ) ) )
35 32 34 eqtr3d 
 |-  ( ( ( F e. ( C CovMap J ) /\ z e. J ) /\ ( ( x e. z /\ w e. ( S ` z ) ) /\ t e. w ) ) -> x = ( F ` ( `' ( F |` t ) ` x ) ) )
36 fveq2 
 |-  ( y = ( `' ( F |` t ) ` x ) -> ( F ` y ) = ( F ` ( `' ( F |` t ) ` x ) ) )
37 36 rspceeqv 
 |-  ( ( ( `' ( F |` t ) ` x ) e. B /\ x = ( F ` ( `' ( F |` t ) ` x ) ) ) -> E. y e. B x = ( F ` y ) )
38 30 35 37 syl2anc 
 |-  ( ( ( F e. ( C CovMap J ) /\ z e. J ) /\ ( ( x e. z /\ w e. ( S ` z ) ) /\ t e. w ) ) -> E. y e. B x = ( F ` y ) )
39 38 expr 
 |-  ( ( ( F e. ( C CovMap J ) /\ z e. J ) /\ ( x e. z /\ w e. ( S ` z ) ) ) -> ( t e. w -> E. y e. B x = ( F ` y ) ) )
40 39 exlimdv 
 |-  ( ( ( F e. ( C CovMap J ) /\ z e. J ) /\ ( x e. z /\ w e. ( S ` z ) ) ) -> ( E. t t e. w -> E. y e. B x = ( F ` y ) ) )
41 13 40 mpd 
 |-  ( ( ( F e. ( C CovMap J ) /\ z e. J ) /\ ( x e. z /\ w e. ( S ` z ) ) ) -> E. y e. B x = ( F ` y ) )
42 41 expr 
 |-  ( ( ( F e. ( C CovMap J ) /\ z e. J ) /\ x e. z ) -> ( w e. ( S ` z ) -> E. y e. B x = ( F ` y ) ) )
43 42 exlimdv 
 |-  ( ( ( F e. ( C CovMap J ) /\ z e. J ) /\ x e. z ) -> ( E. w w e. ( S ` z ) -> E. y e. B x = ( F ` y ) ) )
44 9 43 syl5bi 
 |-  ( ( ( F e. ( C CovMap J ) /\ z e. J ) /\ x e. z ) -> ( ( S ` z ) =/= (/) -> E. y e. B x = ( F ` y ) ) )
45 44 expimpd 
 |-  ( ( F e. ( C CovMap J ) /\ z e. J ) -> ( ( x e. z /\ ( S ` z ) =/= (/) ) -> E. y e. B x = ( F ` y ) ) )
46 45 rexlimdva 
 |-  ( F e. ( C CovMap J ) -> ( E. z e. J ( x e. z /\ ( S ` z ) =/= (/) ) -> E. y e. B x = ( F ` y ) ) )
47 8 46 syld 
 |-  ( F e. ( C CovMap J ) -> ( x e. X -> E. y e. B x = ( F ` y ) ) )
48 47 ralrimiv 
 |-  ( F e. ( C CovMap J ) -> A. x e. X E. y e. B x = ( F ` y ) )
49 dffo3 
 |-  ( F : B -onto-> X <-> ( F : B --> X /\ A. x e. X E. y e. B x = ( F ` y ) ) )
50 6 48 49 sylanbrc 
 |-  ( F e. ( C CovMap J ) -> F : B -onto-> X )