Theorem dicelval2N

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

	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	dicelval2N	|- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Y e. ( I ` Q ) <-> ( Y e. ( _V X. _V ) /\ ( ( 1st ` Y ) = ( ( 2nd ` Y ) ` G ) /\ ( 2nd ` Y ) 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	dicelvalN	|- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Y e. ( I ` Q ) <-> ( Y e. ( _V X. _V ) /\ ( ( 1st ` Y ) = ( ( 2nd ` Y ) ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ ( 2nd ` Y ) e. E ) ) ) )
10	8	fveq2i	|- ( ( 2nd ` Y ) ` G ) = ( ( 2nd ` Y ) ` ( iota_ g e. T ( g ` P ) = Q ) )
11	10	eqeq2i	|- ( ( 1st ` Y ) = ( ( 2nd ` Y ) ` G ) <-> ( 1st ` Y ) = ( ( 2nd ` Y ) ` ( iota_ g e. T ( g ` P ) = Q ) ) )
12	11	anbi1i	|- ( ( ( 1st ` Y ) = ( ( 2nd ` Y ) ` G ) /\ ( 2nd ` Y ) e. E ) <-> ( ( 1st ` Y ) = ( ( 2nd ` Y ) ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ ( 2nd ` Y ) e. E ) )
13	12	anbi2i	|- ( ( Y e. ( _V X. _V ) /\ ( ( 1st ` Y ) = ( ( 2nd ` Y ) ` G ) /\ ( 2nd ` Y ) e. E ) ) <-> ( Y e. ( _V X. _V ) /\ ( ( 1st ` Y ) = ( ( 2nd ` Y ) ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ ( 2nd ` Y ) e. E ) ) )
14	9 13	bitr4di	|- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Y e. ( I ` Q ) <-> ( Y e. ( _V X. _V ) /\ ( ( 1st ` Y ) = ( ( 2nd ` Y ) ` G ) /\ ( 2nd ` Y ) e. E ) ) ) )