Theorem joindm3

Description: The join of any two elements always exists iff all unordered pairs have LUB (expanded version). (Contributed by Zhi Wang, 25-Sep-2024)

	Ref	Expression
Hypotheses	joindm2.b	$$⊢B={\mathrm{Base}}_K$$
	joindm2.k	$$⊢\phi \to K\in V$$
	joindm2.u	$$⊢U=\mathrm{lub}\left(K\right)$$
	joindm2.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	joindm3.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
Assertion	joindm3	$$⊢\phi \to \left(\mathrm{dom}\underset{\dot{}}{\vee }=B\times B\leftrightarrow \forall x\in B\forall y\in B\exists !z\in B\left(\left(x\underset{\dot{}}{\le }z\wedge y\underset{\dot{}}{\le }z\right)\wedge \forall w\in B\left(\left(x\underset{\dot{}}{\le }w\wedge y\underset{\dot{}}{\le }w\right)\to z\underset{\dot{}}{\le }w\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		joindm2.b	$$⊢B={\mathrm{Base}}_K$$
2		joindm2.k	$$⊢\phi \to K\in V$$
3		joindm2.u	$$⊢U=\mathrm{lub}\left(K\right)$$
4		joindm2.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
5		joindm3.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
6	1 2 3 4	joindm2	$$⊢\phi \to \left(\mathrm{dom}\underset{\dot{}}{\vee }=B\times B\leftrightarrow \forall x\in B\forall y\in B\left\{x,y\right\}\in \mathrm{dom}U\right)$$
7		simprl	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x\in B$$
8		simprr	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to y\in B$$
9	7 8	prssd	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left\{x,y\right\}\subseteq B$$
10		biid	$$⊢\left(\forall v\in \left\{x,y\right\}v\underset{\dot{}}{\le }z\wedge \forall w\in B\left(\forall v\in \left\{x,y\right\}v\underset{\dot{}}{\le }w\to z\underset{\dot{}}{\le }w\right)\right)\leftrightarrow \left(\forall v\in \left\{x,y\right\}v\underset{\dot{}}{\le }z\wedge \forall w\in B\left(\forall v\in \left\{x,y\right\}v\underset{\dot{}}{\le }w\to z\underset{\dot{}}{\le }w\right)\right)$$
11	1 5 3 10 2	lubeldm	$$⊢\phi \to \left(\left\{x,y\right\}\in \mathrm{dom}U\leftrightarrow \left(\left\{x,y\right\}\subseteq B\wedge \exists !z\in B\left(\forall v\in \left\{x,y\right\}v\underset{\dot{}}{\le }z\wedge \forall w\in B\left(\forall v\in \left\{x,y\right\}v\underset{\dot{}}{\le }w\to z\underset{\dot{}}{\le }w\right)\right)\right)\right)$$
12	11	baibd	$$⊢\left(\phi \wedge \left\{x,y\right\}\subseteq B\right)\to \left(\left\{x,y\right\}\in \mathrm{dom}U\leftrightarrow \exists !z\in B\left(\forall v\in \left\{x,y\right\}v\underset{\dot{}}{\le }z\wedge \forall w\in B\left(\forall v\in \left\{x,y\right\}v\underset{\dot{}}{\le }w\to z\underset{\dot{}}{\le }w\right)\right)\right)$$
13	9 12	syldan	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(\left\{x,y\right\}\in \mathrm{dom}U\leftrightarrow \exists !z\in B\left(\forall v\in \left\{x,y\right\}v\underset{\dot{}}{\le }z\wedge \forall w\in B\left(\forall v\in \left\{x,y\right\}v\underset{\dot{}}{\le }w\to z\underset{\dot{}}{\le }w\right)\right)\right)$$
14	2	adantr	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to K\in V$$
15	1 5 4 14 7 8	joinval2lem	$$⊢\left(x\in B\wedge y\in B\right)\to \left(\left(\forall v\in \left\{x,y\right\}v\underset{\dot{}}{\le }z\wedge \forall w\in B\left(\forall v\in \left\{x,y\right\}v\underset{\dot{}}{\le }w\to z\underset{\dot{}}{\le }w\right)\right)\leftrightarrow \left(\left(x\underset{\dot{}}{\le }z\wedge y\underset{\dot{}}{\le }z\right)\wedge \forall w\in B\left(\left(x\underset{\dot{}}{\le }w\wedge y\underset{\dot{}}{\le }w\right)\to z\underset{\dot{}}{\le }w\right)\right)\right)$$
16	15	reubidv	$$⊢\left(x\in B\wedge y\in B\right)\to \left(\exists !z\in B\left(\forall v\in \left\{x,y\right\}v\underset{\dot{}}{\le }z\wedge \forall w\in B\left(\forall v\in \left\{x,y\right\}v\underset{\dot{}}{\le }w\to z\underset{\dot{}}{\le }w\right)\right)\leftrightarrow \exists !z\in B\left(\left(x\underset{\dot{}}{\le }z\wedge y\underset{\dot{}}{\le }z\right)\wedge \forall w\in B\left(\left(x\underset{\dot{}}{\le }w\wedge y\underset{\dot{}}{\le }w\right)\to z\underset{\dot{}}{\le }w\right)\right)\right)$$
17	16	adantl	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(\exists !z\in B\left(\forall v\in \left\{x,y\right\}v\underset{\dot{}}{\le }z\wedge \forall w\in B\left(\forall v\in \left\{x,y\right\}v\underset{\dot{}}{\le }w\to z\underset{\dot{}}{\le }w\right)\right)\leftrightarrow \exists !z\in B\left(\left(x\underset{\dot{}}{\le }z\wedge y\underset{\dot{}}{\le }z\right)\wedge \forall w\in B\left(\left(x\underset{\dot{}}{\le }w\wedge y\underset{\dot{}}{\le }w\right)\to z\underset{\dot{}}{\le }w\right)\right)\right)$$
18	13 17	bitrd	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(\left\{x,y\right\}\in \mathrm{dom}U\leftrightarrow \exists !z\in B\left(\left(x\underset{\dot{}}{\le }z\wedge y\underset{\dot{}}{\le }z\right)\wedge \forall w\in B\left(\left(x\underset{\dot{}}{\le }w\wedge y\underset{\dot{}}{\le }w\right)\to z\underset{\dot{}}{\le }w\right)\right)\right)$$
19	18	2ralbidva	$$⊢\phi \to \left(\forall x\in B\forall y\in B\left\{x,y\right\}\in \mathrm{dom}U\leftrightarrow \forall x\in B\forall y\in B\exists !z\in B\left(\left(x\underset{\dot{}}{\le }z\wedge y\underset{\dot{}}{\le }z\right)\wedge \forall w\in B\left(\left(x\underset{\dot{}}{\le }w\wedge y\underset{\dot{}}{\le }w\right)\to z\underset{\dot{}}{\le }w\right)\right)\right)$$
20	6 19	bitrd	$$⊢\phi \to \left(\mathrm{dom}\underset{\dot{}}{\vee }=B\times B\leftrightarrow \forall x\in B\forall y\in B\exists !z\in B\left(\left(x\underset{\dot{}}{\le }z\wedge y\underset{\dot{}}{\le }z\right)\wedge \forall w\in B\left(\left(x\underset{\dot{}}{\le }w\wedge y\underset{\dot{}}{\le }w\right)\to z\underset{\dot{}}{\le }w\right)\right)\right)$$