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 = {Base}_{K}$
	dibelval1st1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dibelval1st1.h	$⊢ H = LHyp (K)$
	dibelval1st1.t	$⊢ T = LTrn (K) (W)$
	dibelval1st1.i	$⊢ I = DIsoB (K) (W)$
Assertion	dibelval1st1	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land Y \in I (X)) \to 1^{st} (Y) \in T$

Step	Hyp	Ref	Expression
1		dibelval1st1.b	$⊢ B = {Base}_{K}$
2		dibelval1st1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dibelval1st1.h	$⊢ H = LHyp (K)$
4		dibelval1st1.t	$⊢ T = LTrn (K) (W)$
5		dibelval1st1.i	$⊢ I = DIsoB (K) (W)$
6		eqid	$⊢ DIsoA (K) (W) = DIsoA (K) (W)$
7	1 2 3 6 5	dibelval1st	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land Y \in I (X)) \to 1^{st} (Y) \in DIsoA (K) (W) (X)$
8	1 2 3 4 6	diael	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land 1^{st} (Y) \in DIsoA (K) (W) (X)) \to 1^{st} (Y) \in T$
9	7 8	syld3an3	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land Y \in I (X)) \to 1^{st} (Y) \in T$

Metamath Proof Explorer