Theorem 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={\mathrm{Base}}_K$$
	dibval2.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dibval2.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dibval2.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	dibval2.o	$$⊢\underset{\dot{}}{0}=\left(f\in T⟼{\mathrm{I}\upharpoonright }_B\right)$$
	dibval2.j	$$⊢J=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
	dibval2.i	$$⊢I=\mathrm{DIsoB}\left(K\right)\left(W\right)$$
Assertion	dibopelval2	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge \left(X\in B\wedge X\underset{\dot{}}{\le }W\right)\right)\to \left(⟨F,S⟩\in I\left(X\right)\leftrightarrow \left(F\in J\left(X\right)\wedge S=\underset{\dot{}}{0}\right)\right)$$

Proof

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