Metamath Proof Explorer


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 ˙=K
dihelval2.a A=AtomsK
dihelval2.h H=LHypK
dihelval2.p P=ocKW
dihelval2.t T=LTrnKW
dihelval2.e E=TEndoKW
dihelval2.i I=DIsoHKW
dihelval2.g G=ιgT|gP=Q
dihelval2.f FV
dihelval2.s SV
Assertion dihopelvalcqat KHLWHQA¬Q˙WFSIQF=SGSE

Proof

Step Hyp Ref Expression
1 dihelval2.l ˙=K
2 dihelval2.a A=AtomsK
3 dihelval2.h H=LHypK
4 dihelval2.p P=ocKW
5 dihelval2.t T=LTrnKW
6 dihelval2.e E=TEndoKW
7 dihelval2.i I=DIsoHKW
8 dihelval2.g G=ιgT|gP=Q
9 dihelval2.f FV
10 dihelval2.s SV
11 eqid DIsoCKW=DIsoCKW
12 1 2 3 11 7 dihvalcqat KHLWHQA¬Q˙WIQ=DIsoCKWQ
13 12 eleq2d KHLWHQA¬Q˙WFSIQFSDIsoCKWQ
14 1 2 3 4 5 6 11 8 9 10 dicopelval2 KHLWHQA¬Q˙WFSDIsoCKWQF=SGSE
15 13 14 bitrd KHLWHQA¬Q˙WFSIQF=SGSE