Theorem dicopelval2

Description: Membership in value of 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 )
	dicelval2.f	|- F e. _V
	dicelval2.s	|- S e. _V
Assertion	dicopelval2	|- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( <. F , S >. e. ( I ` Q ) <-> ( 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		dicelval2.f	|- F e. _V
10		dicelval2.s	|- S e. _V
11	1 2 3 4 5 6 7 9 10	dicopelval	|- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( <. F , S >. e. ( I ` Q ) <-> ( F = ( S ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ S e. E ) ) )
12	8	fveq2i	|- ( S ` G ) = ( S ` ( iota_ g e. T ( g ` P ) = Q ) )
13	12	eqeq2i	|- ( F = ( S ` G ) <-> F = ( S ` ( iota_ g e. T ( g ` P ) = Q ) ) )
14	13	anbi1i	|- ( ( F = ( S ` G ) /\ S e. E ) <-> ( F = ( S ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ S e. E ) )
15	11 14	bitr4di	|- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( <. F , S >. e. ( I ` Q ) <-> ( F = ( S ` G ) /\ S e. E ) ) )