Theorem cvmliftmoi

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)

	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 )
	cvmliftmoi.m	|- ( ph -> M e. ( K Cn C ) )
	cvmliftmoi.n	|- ( ph -> N e. ( K Cn C ) )
	cvmliftmoi.g	|- ( ph -> ( F o. M ) = ( F o. N ) )
	cvmliftmoi.p	|- ( ph -> ( M ` O ) = ( N ` O ) )
Assertion	cvmliftmoi	|- ( ph -> M = N )

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		cvmliftmoi.m	|- ( ph -> M e. ( K Cn C ) )
8		cvmliftmoi.n	|- ( ph -> N e. ( K Cn C ) )
9		cvmliftmoi.g	|- ( ph -> ( F o. M ) = ( F o. N ) )
10		cvmliftmoi.p	|- ( ph -> ( M ` O ) = ( N ` O ) )
11		eqid	|- ( 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 ) ) ) ) } ) = ( 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 ) ) ) ) } )
12	11	cvmscbv	|- ( 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 ) ) ) ) } ) = ( b e. J |-> { m e. ( ~P C \ { (/) } ) | ( U. m = ( `' F " b ) /\ A. r e. m ( A. w e. ( m \ { r } ) ( r i^i w ) = (/) /\ ( F |` r ) e. ( ( C |`t r ) Homeo ( J |`t b ) ) ) ) } )
13	1 2 3 4 5 6 7 8 9 10 12	cvmliftmolem2	|- ( ph -> M = N )