Theorem joineu

Description: Uniqueness of join of elements in the domain. (Contributed by NM, 12-Sep-2018)

	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$$
	joinlem.e	$$⊢\phi \to ⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\vee }$$
Assertion	joineu	$$⊢\phi \to \exists !x\in B\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)$$

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		joinlem.e	$$⊢\phi \to ⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\vee }$$
8		eqid	$$⊢\mathrm{lub}\left(K\right)=\mathrm{lub}\left(K\right)$$
9	8 3 4 5 6	joindef	$$⊢\phi \to \left(⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\vee }\leftrightarrow \left\{X,Y\right\}\in \mathrm{dom}\mathrm{lub}\left(K\right)\right)$$
10		biid	$$⊢\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(\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)$$
11	4	adantr	$$⊢\left(\phi \wedge \left\{X,Y\right\}\in \mathrm{dom}\mathrm{lub}\left(K\right)\right)\to K\in V$$
12		simpr	$$⊢\left(\phi \wedge \left\{X,Y\right\}\in \mathrm{dom}\mathrm{lub}\left(K\right)\right)\to \left\{X,Y\right\}\in \mathrm{dom}\mathrm{lub}\left(K\right)$$
13	1 2 8 10 11 12	lubeu	$$⊢\left(\phi \wedge \left\{X,Y\right\}\in \mathrm{dom}\mathrm{lub}\left(K\right)\right)\to \exists !x\in B\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)$$
14	13	ex	$$⊢\phi \to \left(\left\{X,Y\right\}\in \mathrm{dom}\mathrm{lub}\left(K\right)\to \exists !x\in B\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)\right)$$
15	1 2 3 4 5 6	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)$$
16	5 6 15	syl2anc	$$⊢\phi \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)$$
17	16	reubidv	$$⊢\phi \to \left(\exists !x\in B\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 \exists !x\in B\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)$$
18	14 17	sylibd	$$⊢\phi \to \left(\left\{X,Y\right\}\in \mathrm{dom}\mathrm{lub}\left(K\right)\to \exists !x\in B\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)$$
19	9 18	sylbid	$$⊢\phi \to \left(⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\vee }\to \exists !x\in B\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)$$
20	7 19	mpd	$$⊢\phi \to \exists !x\in B\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)$$