dibelval1st

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

	Ref	Expression
Hypotheses	dibelval1.b	$⊢ B = {Base}_{K}$
	dibelval1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dibelval1.h	$⊢ H = LHyp (K)$
	dibelval1.j	$⊢ J = DIsoA (K) (W)$
	dibelval1.i	$⊢ I = DIsoB (K) (W)$
Assertion	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 J (X)$

Step	Hyp	Ref	Expression
1		dibelval1.b	$⊢ B = {Base}_{K}$
2		dibelval1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dibelval1.h	$⊢ H = LHyp (K)$
4		dibelval1.j	$⊢ J = DIsoA (K) (W)$
5		dibelval1.i	$⊢ I = DIsoB (K) (W)$
6		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
7		eqid	$⊢ (f \in LTrn (K) (W) ⟼ {I ↾}_{B}) = (f \in LTrn (K) (W) ⟼ {I ↾}_{B})$
8	1 2 3 6 7 4 5	dibval2	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) = J (X) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\}$
9	8	eleq2d	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to (Y \in I (X) \leftrightarrow Y \in (J (X) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\}))$
10	9	biimp3a	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W) \land Y \in I (X)) \to Y \in (J (X) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\})$
11		xp1st	$⊢ Y \in (J (X) \times \{(f \in LTrn (K) (W) ⟼ {I ↾}_{B})\}) \to 1^{st} (Y) \in J (X)$
12	10 11	syl	$⊢ ((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 J (X)$

Metamath Proof Explorer