Theorem dibdiadm

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

	Ref	Expression
Hypotheses	dibfna.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dibfna.j	$$⊢J=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
	dibfna.i	$$⊢I=\mathrm{DIsoB}\left(K\right)\left(W\right)$$
Assertion	dibdiadm	$$⊢\left(K\in V\wedge W\in H\right)\to \mathrm{dom}I=\mathrm{dom}J$$

Proof

Step	Hyp	Ref	Expression
1		dibfna.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dibfna.j	$$⊢J=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
3		dibfna.i	$$⊢I=\mathrm{DIsoB}\left(K\right)\left(W\right)$$
4	1 2 3	dibfna	$$⊢\left(K\in V\wedge W\in H\right)\to IFn\mathrm{dom}J$$
5		fndm	$$⊢IFn\mathrm{dom}J\to \mathrm{dom}I=\mathrm{dom}J$$
6	4 5	syl	$$⊢\left(K\in V\wedge W\in H\right)\to \mathrm{dom}I=\mathrm{dom}J$$