Theorem dicelval1sta

Description: Membership in value of the partial isomorphism C for a lattice K . (Contributed by NM, 16-Feb-2014)

	Ref	Expression
Hypotheses	dicelval1sta.l	|- .<_ = ( le ` K )
	dicelval1sta.a	|- A = ( Atoms ` K )
	dicelval1sta.h	|- H = ( LHyp ` K )
	dicelval1sta.p	|- P = ( ( oc ` K ) ` W )
	dicelval1sta.t	|- T = ( ( LTrn ` K ) ` W )
	dicelval1sta.i	|- I = ( ( DIsoC ` K ) ` W )
Assertion	dicelval1sta	|- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ Y e. ( I ` Q ) ) -> ( 1st ` Y ) = ( ( 2nd ` Y ) ` ( iota_ g e. T ( g ` P ) = Q ) ) )

Proof

Step	Hyp	Ref	Expression
1		dicelval1sta.l	|- .<_ = ( le ` K )
2		dicelval1sta.a	|- A = ( Atoms ` K )
3		dicelval1sta.h	|- H = ( LHyp ` K )
4		dicelval1sta.p	|- P = ( ( oc ` K ) ` W )
5		dicelval1sta.t	|- T = ( ( LTrn ` K ) ` W )
6		dicelval1sta.i	|- I = ( ( DIsoC ` K ) ` W )
7		eqid	|- ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )
8	1 2 3 4 5 7 6	dicval	|- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } )
9	8	eleq2d	|- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Y e. ( I ` Q ) <-> Y e. { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } ) )
10	9	biimp3a	|- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ Y e. ( I ` Q ) ) -> Y e. { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } )
11		eqeq1	|- ( f = ( 1st ` Y ) -> ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) <-> ( 1st ` Y ) = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) ) )
12	11	anbi1d	|- ( f = ( 1st ` Y ) -> ( ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) <-> ( ( 1st ` Y ) = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) )
13		fveq1	|- ( s = ( 2nd ` Y ) -> ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) = ( ( 2nd ` Y ) ` ( iota_ g e. T ( g ` P ) = Q ) ) )
14	13	eqeq2d	|- ( s = ( 2nd ` Y ) -> ( ( 1st ` Y ) = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) <-> ( 1st ` Y ) = ( ( 2nd ` Y ) ` ( iota_ g e. T ( g ` P ) = Q ) ) ) )
15		eleq1	|- ( s = ( 2nd ` Y ) -> ( s e. ( ( TEndo ` K ) ` W ) <-> ( 2nd ` Y ) e. ( ( TEndo ` K ) ` W ) ) )
16	14 15	anbi12d	|- ( s = ( 2nd ` Y ) -> ( ( ( 1st ` Y ) = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) <-> ( ( 1st ` Y ) = ( ( 2nd ` Y ) ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ ( 2nd ` Y ) e. ( ( TEndo ` K ) ` W ) ) ) )
17	12 16	elopabi	|- ( Y e. { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } -> ( ( 1st ` Y ) = ( ( 2nd ` Y ) ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ ( 2nd ` Y ) e. ( ( TEndo ` K ) ` W ) ) )
18	10 17	syl	|- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ Y e. ( I ` Q ) ) -> ( ( 1st ` Y ) = ( ( 2nd ` Y ) ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ ( 2nd ` Y ) e. ( ( TEndo ` K ) ` W ) ) )
19	18	simpld	|- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ Y e. ( I ` Q ) ) -> ( 1st ` Y ) = ( ( 2nd ` Y ) ` ( iota_ g e. T ( g ` P ) = Q ) ) )