Metamath Proof Explorer


Theorem cvmfolem

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

Ref Expression
Hypotheses cvmcov.1 S = k J s 𝒫 C | s = F -1 k u s v s u u v = F u C 𝑡 u Homeo J 𝑡 k
cvmseu.1 B = C
cvmfolem.2 X = J
Assertion cvmfolem F C CovMap J F : B onto X

Proof

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