cvmliftiota

Description: Write out a function H that is the unique lift of F . (Contributed by Mario Carneiro, 16-Feb-2015)

	Ref	Expression
Hypotheses	cvmliftiota.b	\|- B = U. C
	cvmliftiota.h	\|- H = ( iota_ f e. ( II Cn C ) ( ( F o. f ) = G /\ ( f ` 0 ) = P ) )
	cvmliftiota.f	\|- ( ph -> F e. ( C CovMap J ) )
	cvmliftiota.g	\|- ( ph -> G e. ( II Cn J ) )
	cvmliftiota.p	\|- ( ph -> P e. B )
	cvmliftiota.e	\|- ( ph -> ( F ` P ) = ( G ` 0 ) )
Assertion	cvmliftiota	\|- ( ph -> ( H e. ( II Cn C ) /\ ( F o. H ) = G /\ ( H ` 0 ) = P ) )

Proof

Step	Hyp	Ref	Expression
1		cvmliftiota.b	\|- B = U. C
2		cvmliftiota.h	\|- H = ( iota_ f e. ( II Cn C ) ( ( F o. f ) = G /\ ( f ` 0 ) = P ) )
3		cvmliftiota.f	\|- ( ph -> F e. ( C CovMap J ) )
4		cvmliftiota.g	\|- ( ph -> G e. ( II Cn J ) )
5		cvmliftiota.p	\|- ( ph -> P e. B )
6		cvmliftiota.e	\|- ( ph -> ( F ` P ) = ( G ` 0 ) )
7		coeq2	\|- ( f = g -> ( F o. f ) = ( F o. g ) )
8	7	eqeq1d	\|- ( f = g -> ( ( F o. f ) = G <-> ( F o. g ) = G ) )
9		fveq1	\|- ( f = g -> ( f ` 0 ) = ( g ` 0 ) )
10	9	eqeq1d	\|- ( f = g -> ( ( f ` 0 ) = P <-> ( g ` 0 ) = P ) )
11	8 10	anbi12d	\|- ( f = g -> ( ( ( F o. f ) = G /\ ( f ` 0 ) = P ) <-> ( ( F o. g ) = G /\ ( g ` 0 ) = P ) ) )
12	11	cbvriotavw	\|- ( iota_ f e. ( II Cn C ) ( ( F o. f ) = G /\ ( f ` 0 ) = P ) ) = ( iota_ g e. ( II Cn C ) ( ( F o. g ) = G /\ ( g ` 0 ) = P ) )
13	2 12	eqtri	\|- H = ( iota_ g e. ( II Cn C ) ( ( F o. g ) = G /\ ( g ` 0 ) = P ) )
14	1	cvmlift	\|- ( ( ( F e. ( C CovMap J ) /\ G e. ( II Cn J ) ) /\ ( P e. B /\ ( F ` P ) = ( G ` 0 ) ) ) -> E! g e. ( II Cn C ) ( ( F o. g ) = G /\ ( g ` 0 ) = P ) )
15	3 4 5 6 14	syl22anc	\|- ( ph -> E! g e. ( II Cn C ) ( ( F o. g ) = G /\ ( g ` 0 ) = P ) )
16		riotacl2	\|- ( E! g e. ( II Cn C ) ( ( F o. g ) = G /\ ( g ` 0 ) = P ) -> ( iota_ g e. ( II Cn C ) ( ( F o. g ) = G /\ ( g ` 0 ) = P ) ) e. { g e. ( II Cn C ) \| ( ( F o. g ) = G /\ ( g ` 0 ) = P ) } )
17	15 16	syl	\|- ( ph -> ( iota_ g e. ( II Cn C ) ( ( F o. g ) = G /\ ( g ` 0 ) = P ) ) e. { g e. ( II Cn C ) \| ( ( F o. g ) = G /\ ( g ` 0 ) = P ) } )
18	13 17	eqeltrid	\|- ( ph -> H e. { g e. ( II Cn C ) \| ( ( F o. g ) = G /\ ( g ` 0 ) = P ) } )
19		coeq2	\|- ( g = H -> ( F o. g ) = ( F o. H ) )
20	19	eqeq1d	\|- ( g = H -> ( ( F o. g ) = G <-> ( F o. H ) = G ) )
21		fveq1	\|- ( g = H -> ( g ` 0 ) = ( H ` 0 ) )
22	21	eqeq1d	\|- ( g = H -> ( ( g ` 0 ) = P <-> ( H ` 0 ) = P ) )
23	20 22	anbi12d	\|- ( g = H -> ( ( ( F o. g ) = G /\ ( g ` 0 ) = P ) <-> ( ( F o. H ) = G /\ ( H ` 0 ) = P ) ) )
24	23	elrab	\|- ( H e. { g e. ( II Cn C ) \| ( ( F o. g ) = G /\ ( g ` 0 ) = P ) } <-> ( H e. ( II Cn C ) /\ ( ( F o. H ) = G /\ ( H ` 0 ) = P ) ) )
25		3anass	\|- ( ( H e. ( II Cn C ) /\ ( F o. H ) = G /\ ( H ` 0 ) = P ) <-> ( H e. ( II Cn C ) /\ ( ( F o. H ) = G /\ ( H ` 0 ) = P ) ) )
26	24 25	bitr4i	\|- ( H e. { g e. ( II Cn C ) \| ( ( F o. g ) = G /\ ( g ` 0 ) = P ) } <-> ( H e. ( II Cn C ) /\ ( F o. H ) = G /\ ( H ` 0 ) = P ) )
27	18 26	sylib	\|- ( ph -> ( H e. ( II Cn C ) /\ ( F o. H ) = G /\ ( H ` 0 ) = P ) )

Metamath Proof Explorer

Theorem cvmliftiota

Proof