Theorem diaclN

Description: Closure of partial isomorphism A for a lattice K . (Contributed by NM, 4-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dia1o.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dia1o.i	$$⊢I=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
Assertion	diaclN	$$⊢\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		dia1o.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		dia1o.i	$$⊢I=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
3	1 2	diaf11N	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to I:\mathrm{dom}I\underset{1-1\; onto}{⟶}\mathrm{ran}I$$
4		f1ofun	$$⊢I:\mathrm{dom}I\underset{1-1\; onto}{⟶}\mathrm{ran}I\to \mathrm{Fun}I$$
5	3 4	syl	$$⊢\left(K\in \mathrm{HL}\wedge W\in H\right)\to \mathrm{Fun}I$$
6		fvelrn	$$⊢\left(\mathrm{Fun}I\wedge X\in \mathrm{dom}I\right)\to I\left(X\right)\in \mathrm{ran}I$$
7	5 6	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$$