Metamath Proof Explorer


Theorem dibdiadm

Description: Domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014)

Ref Expression
Hypotheses dibfna.h H = LHyp K
dibfna.j J = DIsoA K W
dibfna.i I = DIsoB K W
Assertion dibdiadm K V W H dom I = dom J

Proof

Step Hyp Ref Expression
1 dibfna.h H = LHyp K
2 dibfna.j J = DIsoA K W
3 dibfna.i I = DIsoB K W
4 1 2 3 dibfna K V W H I Fn dom J
5 4 fndmd K V W H dom I = dom J