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 e. V /\ W e. 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 e. V /\ W e. H ) -> I Fn dom J )
5	4	fndmd	|- ( ( K e. V /\ W e. H ) -> dom I = dom J )