Theorem cvmlift3lem1

Description: Lemma for cvmlift3 . (Contributed by Mario Carneiro, 6-Jul-2015)

	Ref	Expression
Hypotheses	cvmlift3.b	|- B = U. C
	cvmlift3.y	|- Y = U. K
	cvmlift3.f	|- ( ph -> F e. ( C CovMap J ) )
	cvmlift3.k	|- ( ph -> K e. SConn )
	cvmlift3.l	|- ( ph -> K e. N-Locally PConn )
	cvmlift3.o	|- ( ph -> O e. Y )
	cvmlift3.g	|- ( ph -> G e. ( K Cn J ) )
	cvmlift3.p	|- ( ph -> P e. B )
	cvmlift3.e	|- ( ph -> ( F ` P ) = ( G ` O ) )
	cvmlift3lem1.1	|- ( ph -> M e. ( II Cn K ) )
	cvmlift3lem1.2	|- ( ph -> ( M ` 0 ) = O )
	cvmlift3lem1.3	|- ( ph -> N e. ( II Cn K ) )
	cvmlift3lem1.4	|- ( ph -> ( N ` 0 ) = O )
	cvmlift3lem1.5	|- ( ph -> ( M ` 1 ) = ( N ` 1 ) )
Assertion	cvmlift3lem1	|- ( ph -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. M ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. N ) /\ ( g ` 0 ) = P ) ) ` 1 ) )

Proof

Step	Hyp	Ref	Expression
1		cvmlift3.b	|- B = U. C
2		cvmlift3.y	|- Y = U. K
3		cvmlift3.f	|- ( ph -> F e. ( C CovMap J ) )
4		cvmlift3.k	|- ( ph -> K e. SConn )
5		cvmlift3.l	|- ( ph -> K e. N-Locally PConn )
6		cvmlift3.o	|- ( ph -> O e. Y )
7		cvmlift3.g	|- ( ph -> G e. ( K Cn J ) )
8		cvmlift3.p	|- ( ph -> P e. B )
9		cvmlift3.e	|- ( ph -> ( F ` P ) = ( G ` O ) )
10		cvmlift3lem1.1	|- ( ph -> M e. ( II Cn K ) )
11		cvmlift3lem1.2	|- ( ph -> ( M ` 0 ) = O )
12		cvmlift3lem1.3	|- ( ph -> N e. ( II Cn K ) )
13		cvmlift3lem1.4	|- ( ph -> ( N ` 0 ) = O )
14		cvmlift3lem1.5	|- ( ph -> ( M ` 1 ) = ( N ` 1 ) )
15		eqid	|- ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. M ) /\ ( g ` 0 ) = P ) ) = ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. M ) /\ ( g ` 0 ) = P ) )
16		eqid	|- ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. N ) /\ ( g ` 0 ) = P ) ) = ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. N ) /\ ( g ` 0 ) = P ) )
17	11	fveq2d	|- ( ph -> ( G ` ( M ` 0 ) ) = ( G ` O ) )
18	9 17	eqtr4d	|- ( ph -> ( F ` P ) = ( G ` ( M ` 0 ) ) )
19		iiuni	|- ( 0 [,] 1 ) = U. II
20	19 2	cnf	|- ( M e. ( II Cn K ) -> M : ( 0 [,] 1 ) --> Y )
21	10 20	syl	|- ( ph -> M : ( 0 [,] 1 ) --> Y )
22		0elunit	|- 0 e. ( 0 [,] 1 )
23		fvco3	|- ( ( M : ( 0 [,] 1 ) --> Y /\ 0 e. ( 0 [,] 1 ) ) -> ( ( G o. M ) ` 0 ) = ( G ` ( M ` 0 ) ) )
24	21 22 23	sylancl	|- ( ph -> ( ( G o. M ) ` 0 ) = ( G ` ( M ` 0 ) ) )
25	18 24	eqtr4d	|- ( ph -> ( F ` P ) = ( ( G o. M ) ` 0 ) )
26	11 13	eqtr4d	|- ( ph -> ( M ` 0 ) = ( N ` 0 ) )
27	4 10 12 26 14	sconnpht2	|- ( ph -> M ( ~=ph ` K ) N )
28	27 7	phtpcco2	|- ( ph -> ( G o. M ) ( ~=ph ` J ) ( G o. N ) )
29	1 15 16 3 8 25 28	cvmliftpht	|- ( ph -> ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. M ) /\ ( g ` 0 ) = P ) ) ( ~=ph ` C ) ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. N ) /\ ( g ` 0 ) = P ) ) )
30		phtpc01	|- ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. M ) /\ ( g ` 0 ) = P ) ) ( ~=ph ` C ) ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. N ) /\ ( g ` 0 ) = P ) ) -> ( ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. M ) /\ ( g ` 0 ) = P ) ) ` 0 ) = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. N ) /\ ( g ` 0 ) = P ) ) ` 0 ) /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. M ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. N ) /\ ( g ` 0 ) = P ) ) ` 1 ) ) )
31	29 30	syl	|- ( ph -> ( ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. M ) /\ ( g ` 0 ) = P ) ) ` 0 ) = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. N ) /\ ( g ` 0 ) = P ) ) ` 0 ) /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. M ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. N ) /\ ( g ` 0 ) = P ) ) ` 1 ) ) )
32	31	simprd	|- ( ph -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. M ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. N ) /\ ( g ` 0 ) = P ) ) ` 1 ) )