Theorem joinval2lem

Description: Lemma for joinval2 and joineu . (Contributed by NM, 12-Sep-2018) TODO: combine this through joineu into joinlem ?

	Ref	Expression
Hypotheses	joinval2.b	$$⊢B={\mathrm{Base}}_K$$
	joinval2.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	joinval2.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	joinval2.k	$$⊢\phi \to K\in V$$
	joinval2.x	$$⊢\phi \to X\in B$$
	joinval2.y	$$⊢\phi \to Y\in B$$
Assertion	joinval2lem	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(\left(\forall y\in \left\{X,Y\right\}y\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in \left\{X,Y\right\}y\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\leftrightarrow \left(\left(X\underset{\dot{}}{\le }x\wedge Y\underset{\dot{}}{\le }x\right)\wedge \forall z\in B\left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		joinval2.b	$$⊢B={\mathrm{Base}}_K$$
2		joinval2.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		joinval2.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		joinval2.k	$$⊢\phi \to K\in V$$
5		joinval2.x	$$⊢\phi \to X\in B$$
6		joinval2.y	$$⊢\phi \to Y\in B$$
7		breq1	$$⊢y=X\to \left(y\underset{\dot{}}{\le }x\leftrightarrow X\underset{\dot{}}{\le }x\right)$$
8		breq1	$$⊢y=Y\to \left(y\underset{\dot{}}{\le }x\leftrightarrow Y\underset{\dot{}}{\le }x\right)$$
9	7 8	ralprg	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(\forall y\in \left\{X,Y\right\}y\underset{\dot{}}{\le }x\leftrightarrow \left(X\underset{\dot{}}{\le }x\wedge Y\underset{\dot{}}{\le }x\right)\right)$$
10		breq1	$$⊢y=X\to \left(y\underset{\dot{}}{\le }z\leftrightarrow X\underset{\dot{}}{\le }z\right)$$
11		breq1	$$⊢y=Y\to \left(y\underset{\dot{}}{\le }z\leftrightarrow Y\underset{\dot{}}{\le }z\right)$$
12	10 11	ralprg	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(\forall y\in \left\{X,Y\right\}y\underset{\dot{}}{\le }z\leftrightarrow \left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\right)$$
13	12	imbi1d	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(\left(\forall y\in \left\{X,Y\right\}y\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\leftrightarrow \left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)$$
14	13	ralbidv	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(\forall z\in B\left(\forall y\in \left\{X,Y\right\}y\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\leftrightarrow \forall z\in B\left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)$$
15	9 14	anbi12d	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(\left(\forall y\in \left\{X,Y\right\}y\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in \left\{X,Y\right\}y\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\leftrightarrow \left(\left(X\underset{\dot{}}{\le }x\wedge Y\underset{\dot{}}{\le }x\right)\wedge \forall z\in B\left(\left(X\underset{\dot{}}{\le }z\wedge Y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\right)$$