Theorem dicval2

Description: The partial isomorphism C for a lattice K . (Contributed by NM, 20-Feb-2014)

	Ref	Expression
Hypotheses	dicval.l	|- .<_ = ( le ` K )
	dicval.a	|- A = ( Atoms ` K )
	dicval.h	|- H = ( LHyp ` K )
	dicval.p	|- P = ( ( oc ` K ) ` W )
	dicval.t	|- T = ( ( LTrn ` K ) ` W )
	dicval.e	|- E = ( ( TEndo ` K ) ` W )
	dicval.i	|- I = ( ( DIsoC ` K ) ` W )
	dicval2.g	|- G = ( iota_ g e. T ( g ` P ) = Q )
Assertion	dicval2	|- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = { <. f , s >. | ( f = ( s ` G ) /\ s e. E ) } )

Proof

Step	Hyp	Ref	Expression
1		dicval.l	|- .<_ = ( le ` K )
2		dicval.a	|- A = ( Atoms ` K )
3		dicval.h	|- H = ( LHyp ` K )
4		dicval.p	|- P = ( ( oc ` K ) ` W )
5		dicval.t	|- T = ( ( LTrn ` K ) ` W )
6		dicval.e	|- E = ( ( TEndo ` K ) ` W )
7		dicval.i	|- I = ( ( DIsoC ` K ) ` W )
8		dicval2.g	|- G = ( iota_ g e. T ( g ` P ) = Q )
9	1 2 3 4 5 6 7	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. E ) } )
10	8	fveq2i	|- ( s ` G ) = ( s ` ( iota_ g e. T ( g ` P ) = Q ) )
11	10	eqeq2i	|- ( f = ( s ` G ) <-> f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) )
12	11	anbi1i	|- ( ( f = ( s ` G ) /\ s e. E ) <-> ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. E ) )
13	12	opabbii	|- { <. f , s >. | ( f = ( s ` G ) /\ s e. E ) } = { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. E ) }
14	9 13	eqtr4di	|- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = { <. f , s >. | ( f = ( s ` G ) /\ s e. E ) } )