dibopelval2

Description: Member of the partial isomorphism B. (Contributed by NM, 3-Mar-2014) (Revised by Mario Carneiro, 6-May-2015)

	Ref	Expression
Hypotheses	dibval2.b	$⊢ B = {Base}_{K}$
	dibval2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dibval2.h	$⊢ H = LHyp (K)$
	dibval2.t	$⊢ T = LTrn (K) (W)$
	dibval2.o	$⊢ \underset{˙}{0} = (f \in T ⟼ {I ↾}_{B})$
	dibval2.j	$⊢ J = DIsoA (K) (W)$
	dibval2.i	$⊢ I = DIsoB (K) (W)$
Assertion	dibopelval2	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to (⟨F, S⟩ \in I (X) \leftrightarrow (F \in J (X) \land S = \underset{˙}{0}))$

Step	Hyp	Ref	Expression
1		dibval2.b	$⊢ B = {Base}_{K}$
2		dibval2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dibval2.h	$⊢ H = LHyp (K)$
4		dibval2.t	$⊢ T = LTrn (K) (W)$
5		dibval2.o	$⊢ \underset{˙}{0} = (f \in T ⟼ {I ↾}_{B})$
6		dibval2.j	$⊢ J = DIsoA (K) (W)$
7		dibval2.i	$⊢ I = DIsoB (K) (W)$
8	1 2 3 4 5 6 7	dibval2	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) = J (X) \times \{\underset{˙}{0}\}$
9	8	eleq2d	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to (⟨F, S⟩ \in I (X) \leftrightarrow ⟨F, S⟩ \in (J (X) \times \{\underset{˙}{0}\}))$
10		opelxp	$⊢ ⟨F, S⟩ \in (J (X) \times \{\underset{˙}{0}\}) \leftrightarrow (F \in J (X) \land S \in \{\underset{˙}{0}\})$
11	4	fvexi	$⊢ T \in V$
12	11	mptex	$⊢ (f \in T ⟼ {I ↾}_{B}) \in V$
13	5 12	eqeltri	$⊢ \underset{˙}{0} \in V$
14	13	elsn2	$⊢ S \in \{\underset{˙}{0}\} \leftrightarrow S = \underset{˙}{0}$
15	14	anbi2i	$⊢ (F \in J (X) \land S \in \{\underset{˙}{0}\}) \leftrightarrow (F \in J (X) \land S = \underset{˙}{0})$
16	10 15	bitri	$⊢ ⟨F, S⟩ \in (J (X) \times \{\underset{˙}{0}\}) \leftrightarrow (F \in J (X) \land S = \underset{˙}{0})$
17	9 16	bitrdi	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to (⟨F, S⟩ \in I (X) \leftrightarrow (F \in J (X) \land S = \underset{˙}{0}))$

Metamath Proof Explorer