Metamath Proof Explorer

Theorem cvmliftmo

Description: A lift of a continuous function from a connected and locally connected space over a covering map is unique when it exists. (Contributed by Mario Carneiro, 10-Mar-2015) (Revised by NM, 17-Jun-2017)

Ref Expression
Hypotheses cvmliftmo.b 
|- B = U. C
cvmliftmo.y 
|- Y = U. K
cvmliftmo.f 
|- ( ph -> F e. ( C CovMap J ) )
cvmliftmo.k 
|- ( ph -> K e. Conn )
cvmliftmo.l 
|- ( ph -> K e. N-Locally Conn )
cvmliftmo.o 
|- ( ph -> O e. Y )
cvmliftmo.g 
|- ( ph -> G e. ( K Cn J ) )
cvmliftmo.p 
|- ( ph -> P e. B )
cvmliftmo.e 
|- ( ph -> ( F ` P ) = ( G ` O ) )
Assertion cvmliftmo 
|- ( ph -> E* f e. ( K Cn C ) ( ( F o. f ) = G /\ ( f ` O ) = P ) )

Proof

Step Hyp Ref Expression
1 cvmliftmo.b 
 |-  B = U. C
2 cvmliftmo.y 
 |-  Y = U. K
3 cvmliftmo.f 
 |-  ( ph -> F e. ( C CovMap J ) )
4 cvmliftmo.k 
 |-  ( ph -> K e. Conn )
5 cvmliftmo.l 
 |-  ( ph -> K e. N-Locally Conn )
6 cvmliftmo.o 
 |-  ( ph -> O e. Y )
7 cvmliftmo.g 
 |-  ( ph -> G e. ( K Cn J ) )
8 cvmliftmo.p 
 |-  ( ph -> P e. B )
9 cvmliftmo.e 
 |-  ( ph -> ( F ` P ) = ( G ` O ) )
10 3 ad2antrr 
 |-  ( ( ( ph /\ ( f e. ( K Cn C ) /\ g e. ( K Cn C ) ) ) /\ ( ( ( F o. f ) = G /\ ( f ` O ) = P ) /\ ( ( F o. g ) = G /\ ( g ` O ) = P ) ) ) -> F e. ( C CovMap J ) )
11 4 ad2antrr 
 |-  ( ( ( ph /\ ( f e. ( K Cn C ) /\ g e. ( K Cn C ) ) ) /\ ( ( ( F o. f ) = G /\ ( f ` O ) = P ) /\ ( ( F o. g ) = G /\ ( g ` O ) = P ) ) ) -> K e. Conn )
12 5 ad2antrr 
 |-  ( ( ( ph /\ ( f e. ( K Cn C ) /\ g e. ( K Cn C ) ) ) /\ ( ( ( F o. f ) = G /\ ( f ` O ) = P ) /\ ( ( F o. g ) = G /\ ( g ` O ) = P ) ) ) -> K e. N-Locally Conn )
13 6 ad2antrr 
 |-  ( ( ( ph /\ ( f e. ( K Cn C ) /\ g e. ( K Cn C ) ) ) /\ ( ( ( F o. f ) = G /\ ( f ` O ) = P ) /\ ( ( F o. g ) = G /\ ( g ` O ) = P ) ) ) -> O e. Y )
14 simplrl 
 |-  ( ( ( ph /\ ( f e. ( K Cn C ) /\ g e. ( K Cn C ) ) ) /\ ( ( ( F o. f ) = G /\ ( f ` O ) = P ) /\ ( ( F o. g ) = G /\ ( g ` O ) = P ) ) ) -> f e. ( K Cn C ) )
15 simplrr 
 |-  ( ( ( ph /\ ( f e. ( K Cn C ) /\ g e. ( K Cn C ) ) ) /\ ( ( ( F o. f ) = G /\ ( f ` O ) = P ) /\ ( ( F o. g ) = G /\ ( g ` O ) = P ) ) ) -> g e. ( K Cn C ) )
16 simprll 
 |-  ( ( ( ph /\ ( f e. ( K Cn C ) /\ g e. ( K Cn C ) ) ) /\ ( ( ( F o. f ) = G /\ ( f ` O ) = P ) /\ ( ( F o. g ) = G /\ ( g ` O ) = P ) ) ) -> ( F o. f ) = G )
17 simprrl 
 |-  ( ( ( ph /\ ( f e. ( K Cn C ) /\ g e. ( K Cn C ) ) ) /\ ( ( ( F o. f ) = G /\ ( f ` O ) = P ) /\ ( ( F o. g ) = G /\ ( g ` O ) = P ) ) ) -> ( F o. g ) = G )
18 16 17 eqtr4d 
 |-  ( ( ( ph /\ ( f e. ( K Cn C ) /\ g e. ( K Cn C ) ) ) /\ ( ( ( F o. f ) = G /\ ( f ` O ) = P ) /\ ( ( F o. g ) = G /\ ( g ` O ) = P ) ) ) -> ( F o. f ) = ( F o. g ) )
19 simprlr 
 |-  ( ( ( ph /\ ( f e. ( K Cn C ) /\ g e. ( K Cn C ) ) ) /\ ( ( ( F o. f ) = G /\ ( f ` O ) = P ) /\ ( ( F o. g ) = G /\ ( g ` O ) = P ) ) ) -> ( f ` O ) = P )
20 simprrr 
 |-  ( ( ( ph /\ ( f e. ( K Cn C ) /\ g e. ( K Cn C ) ) ) /\ ( ( ( F o. f ) = G /\ ( f ` O ) = P ) /\ ( ( F o. g ) = G /\ ( g ` O ) = P ) ) ) -> ( g ` O ) = P )
21 19 20 eqtr4d 
 |-  ( ( ( ph /\ ( f e. ( K Cn C ) /\ g e. ( K Cn C ) ) ) /\ ( ( ( F o. f ) = G /\ ( f ` O ) = P ) /\ ( ( F o. g ) = G /\ ( g ` O ) = P ) ) ) -> ( f ` O ) = ( g ` O ) )
22 1 2 10 11 12 13 14 15 18 21 cvmliftmoi 
 |-  ( ( ( ph /\ ( f e. ( K Cn C ) /\ g e. ( K Cn C ) ) ) /\ ( ( ( F o. f ) = G /\ ( f ` O ) = P ) /\ ( ( F o. g ) = G /\ ( g ` O ) = P ) ) ) -> f = g )
23 22 ex 
 |-  ( ( ph /\ ( f e. ( K Cn C ) /\ g e. ( K Cn C ) ) ) -> ( ( ( ( F o. f ) = G /\ ( f ` O ) = P ) /\ ( ( F o. g ) = G /\ ( g ` O ) = P ) ) -> f = g ) )
24 23 ralrimivva 
 |-  ( ph -> A. f e. ( K Cn C ) A. g e. ( K Cn C ) ( ( ( ( F o. f ) = G /\ ( f ` O ) = P ) /\ ( ( F o. g ) = G /\ ( g ` O ) = P ) ) -> f = g ) )
25 coeq2 
 |-  ( f = g -> ( F o. f ) = ( F o. g ) )
26 25 eqeq1d 
 |-  ( f = g -> ( ( F o. f ) = G <-> ( F o. g ) = G ) )
27 fveq1 
 |-  ( f = g -> ( f ` O ) = ( g ` O ) )
28 27 eqeq1d 
 |-  ( f = g -> ( ( f ` O ) = P <-> ( g ` O ) = P ) )
29 26 28 anbi12d 
 |-  ( f = g -> ( ( ( F o. f ) = G /\ ( f ` O ) = P ) <-> ( ( F o. g ) = G /\ ( g ` O ) = P ) ) )
30 29 rmo4 
 |-  ( E* f e. ( K Cn C ) ( ( F o. f ) = G /\ ( f ` O ) = P ) <-> A. f e. ( K Cn C ) A. g e. ( K Cn C ) ( ( ( ( F o. f ) = G /\ ( f ` O ) = P ) /\ ( ( F o. g ) = G /\ ( g ` O ) = P ) ) -> f = g ) )
31 24 30 sylibr 
 |-  ( ph -> E* f e. ( K Cn C ) ( ( F o. f ) = G /\ ( f ` O ) = P ) )