Theorem dibclN

Description: Closure of partial isomorphism B for a lattice K . (Contributed by NM, 8-Mar-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dibcl.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dibcl.i	$$⊢I=\mathrm{DIsoB}\left(K\right)\left(W\right)$$
Assertion	dibclN	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\in \mathrm{dom}I\right)\to I\left(X\right)\in \mathrm{ran}I$$

Proof

Step	Hyp	Ref	Expression
1		dibcl.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dibcl.i	$$⊢I=\mathrm{DIsoB}\left(K\right)\left(W\right)$$
3		eqid	$$⊢\mathrm{DIsoA}\left(K\right)\left(W\right)=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
4	1 3 2	dibfna	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to IFn\mathrm{dom}\mathrm{DIsoA}\left(K\right)\left(W\right)$$
5		fnfun	$$⊢IFn\mathrm{dom}\mathrm{DIsoA}\left(K\right)\left(W\right)\to \mathrm{Fun}I$$
6	4 5	syl	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \mathrm{Fun}I$$
7		fvelrn	$$⊢\left(\mathrm{Fun}I\wedge X\in \mathrm{dom}I\right)\to I\left(X\right)\in \mathrm{ran}I$$
8	6 7	sylan	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\in \mathrm{dom}I\right)\to I\left(X\right)\in \mathrm{ran}I$$