Theorem dibelval1st2N

Description: Membership in value of the partial isomorphism B for a lattice K . (Contributed by NM, 13-Feb-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dibelval1st2.b	$$⊢B={\mathrm{Base}}_K$$
	dibelval1st2.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dibelval1st2.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dibelval1st2.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	dibelval1st2.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
	dibelval1st2.i	$$⊢I=\mathrm{DIsoB}\left(K\right)\left(W\right)$$
Assertion	dibelval1st2N	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge \left(X\in B\wedge X\underset{\dot{}}{\le }W\right)\wedge Y\in I\left(X\right)\right)\to R\left(1^{st}\left(Y\right)\right)\underset{\dot{}}{\le }X$$

Proof

Step	Hyp	Ref	Expression
1		dibelval1st2.b	$$⊢B={\mathrm{Base}}_K$$
2		dibelval1st2.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		dibelval1st2.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
4		dibelval1st2.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
5		dibelval1st2.r	$$⊢R=\mathrm{trL}\left(K\right)\left(W\right)$$
6		dibelval1st2.i	$$⊢I=\mathrm{DIsoB}\left(K\right)\left(W\right)$$
7		eqid	$$⊢\mathrm{DIsoA}\left(K\right)\left(W\right)=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
8	1 2 3 7 6	dibelval1st	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge \left(X\in B\wedge X\underset{\dot{}}{\le }W\right)\wedge Y\in I\left(X\right)\right)\to 1^{st}\left(Y\right)\in \mathrm{DIsoA}\left(K\right)\left(W\right)\left(X\right)$$
9	1 2 3 4 5 7	diatrl	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge \left(X\in B\wedge X\underset{\dot{}}{\le }W\right)\wedge 1^{st}\left(Y\right)\in \mathrm{DIsoA}\left(K\right)\left(W\right)\left(X\right)\right)\to R\left(1^{st}\left(Y\right)\right)\underset{\dot{}}{\le }X$$
10	8 9	syld3an3	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge \left(X\in B\wedge X\underset{\dot{}}{\le }W\right)\wedge Y\in I\left(X\right)\right)\to R\left(1^{st}\left(Y\right)\right)\underset{\dot{}}{\le }X$$