Theorem dihopelvalcqat

Description: Ordered pair member of the partial isomorphism H for atom argument not under W . TODO: remove .t hypothesis. (Contributed by NM, 30-Mar-2014)

	Ref	Expression
Hypotheses	dihelval2.l	|- .<_ = ( le ` K )
	dihelval2.a	|- A = ( Atoms ` K )
	dihelval2.h	|- H = ( LHyp ` K )
	dihelval2.p	|- P = ( ( oc ` K ) ` W )
	dihelval2.t	|- T = ( ( LTrn ` K ) ` W )
	dihelval2.e	|- E = ( ( TEndo ` K ) ` W )
	dihelval2.i	|- I = ( ( DIsoH ` K ) ` W )
	dihelval2.g	|- G = ( iota_ g e. T ( g ` P ) = Q )
	dihelval2.f	|- F e. _V
	dihelval2.s	|- S e. _V
Assertion	dihopelvalcqat	|- ( ( ( K e. HL /\ 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		dihelval2.l	|- .<_ = ( le ` K )
2		dihelval2.a	|- A = ( Atoms ` K )
3		dihelval2.h	|- H = ( LHyp ` K )
4		dihelval2.p	|- P = ( ( oc ` K ) ` W )
5		dihelval2.t	|- T = ( ( LTrn ` K ) ` W )
6		dihelval2.e	|- E = ( ( TEndo ` K ) ` W )
7		dihelval2.i	|- I = ( ( DIsoH ` K ) ` W )
8		dihelval2.g	|- G = ( iota_ g e. T ( g ` P ) = Q )
9		dihelval2.f	|- F e. _V
10		dihelval2.s	|- S e. _V
11		eqid	|- ( ( DIsoC ` K ) ` W ) = ( ( DIsoC ` K ) ` W )
12	1 2 3 11 7	dihvalcqat	|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = ( ( ( DIsoC ` K ) ` W ) ` Q ) )
13	12	eleq2d	|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( <. F , S >. e. ( I ` Q ) <-> <. F , S >. e. ( ( ( DIsoC ` K ) ` W ) ` Q ) ) )
14	1 2 3 4 5 6 11 8 9 10	dicopelval2	|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( <. F , S >. e. ( ( ( DIsoC ` K ) ` W ) ` Q ) <-> ( F = ( S ` G ) /\ S e. E ) ) )
15	13 14	bitrd	|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( <. F , S >. e. ( I ` Q ) <-> ( F = ( S ` G ) /\ S e. E ) ) )