Theorem dibelval1st1

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

	Ref	Expression
Hypotheses	dibelval1st1.b	$$⊢B={\mathrm{Base}}_K$$
	dibelval1st1.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dibelval1st1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dibelval1st1.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	dibelval1st1.i	$$⊢I=\mathrm{DIsoB}\left(K\right)\left(W\right)$$
Assertion	dibelval1st1	$$⊢\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 T$$

Proof

Step	Hyp	Ref	Expression
1		dibelval1st1.b	$$⊢B={\mathrm{Base}}_K$$
2		dibelval1st1.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		dibelval1st1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
4		dibelval1st1.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
5		dibelval1st1.i	$$⊢I=\mathrm{DIsoB}\left(K\right)\left(W\right)$$
6		eqid	$$⊢\mathrm{DIsoA}\left(K\right)\left(W\right)=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
7	1 2 3 6 5	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)$$
8	1 2 3 4 6	diael	$$⊢\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 1^{st}\left(Y\right)\in T$$
9	7 8	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 1^{st}\left(Y\right)\in T$$