Metamath Proof Explorer


Theorem dibeldmN

Description: Member of domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dibfn.b B = Base K
dibfn.l ˙ = K
dibfn.h H = LHyp K
dibfn.i I = DIsoB K W
Assertion dibeldmN K V W H X dom I X B X ˙ W

Proof

Step Hyp Ref Expression
1 dibfn.b B = Base K
2 dibfn.l ˙ = K
3 dibfn.h H = LHyp K
4 dibfn.i I = DIsoB K W
5 eqid DIsoA K W = DIsoA K W
6 3 5 4 dibdiadm K V W H dom I = dom DIsoA K W
7 6 eleq2d K V W H X dom I X dom DIsoA K W
8 1 2 3 5 diaeldm K V W H X dom DIsoA K W X B X ˙ W
9 7 8 bitrd K V W H X dom I X B X ˙ W