Theorem meetdm3

Description: The meet of any two elements always exists iff all unordered pairs have GLB (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$$
	meetdm2.g	$$⊢G=\mathrm{glb}\left(K\right)$$
	meetdm2.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	meetdm3.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
Assertion	meetdm3	$$⊢\phi \to \left(\mathrm{dom}\underset{\dot{}}{\wedge }=B\times B\leftrightarrow \forall x\in B\forall y\in B\exists !z\in B\left(\left(z\underset{\dot{}}{\le }x\wedge z\underset{\dot{}}{\le }y\right)\wedge \forall w\in B\left(\left(w\underset{\dot{}}{\le }x\wedge w\underset{\dot{}}{\le }y\right)\to w\underset{\dot{}}{\le }z\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		joindm2.b	$$⊢B={\mathrm{Base}}_K$$
2		joindm2.k	$$⊢\phi \to K\in V$$
3		meetdm2.g	$$⊢G=\mathrm{glb}\left(K\right)$$
4		meetdm2.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
5		meetdm3.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
6	1 2 3 4	meetdm2	$$⊢\phi \to \left(\mathrm{dom}\underset{\dot{}}{\wedge }=B\times B\leftrightarrow \forall x\in B\forall y\in B\left\{x,y\right\}\in \mathrm{dom}G\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\}z\underset{\dot{}}{\le }v\wedge \forall w\in B\left(\forall v\in \left\{x,y\right\}w\underset{\dot{}}{\le }v\to w\underset{\dot{}}{\le }z\right)\right)\leftrightarrow \left(\forall v\in \left\{x,y\right\}z\underset{\dot{}}{\le }v\wedge \forall w\in B\left(\forall v\in \left\{x,y\right\}w\underset{\dot{}}{\le }v\to w\underset{\dot{}}{\le }z\right)\right)$$
11	1 5 3 10 2	glbeldm	$$⊢\phi \to \left(\left\{x,y\right\}\in \mathrm{dom}G\leftrightarrow \left(\left\{x,y\right\}\subseteq B\wedge \exists !z\in B\left(\forall v\in \left\{x,y\right\}z\underset{\dot{}}{\le }v\wedge \forall w\in B\left(\forall v\in \left\{x,y\right\}w\underset{\dot{}}{\le }v\to w\underset{\dot{}}{\le }z\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}G\leftrightarrow \exists !z\in B\left(\forall v\in \left\{x,y\right\}z\underset{\dot{}}{\le }v\wedge \forall w\in B\left(\forall v\in \left\{x,y\right\}w\underset{\dot{}}{\le }v\to w\underset{\dot{}}{\le }z\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}G\leftrightarrow \exists !z\in B\left(\forall v\in \left\{x,y\right\}z\underset{\dot{}}{\le }v\wedge \forall w\in B\left(\forall v\in \left\{x,y\right\}w\underset{\dot{}}{\le }v\to w\underset{\dot{}}{\le }z\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	meetval2lem	$$⊢\left(x\in B\wedge y\in B\right)\to \left(\left(\forall v\in \left\{x,y\right\}z\underset{\dot{}}{\le }v\wedge \forall w\in B\left(\forall v\in \left\{x,y\right\}w\underset{\dot{}}{\le }v\to w\underset{\dot{}}{\le }z\right)\right)\leftrightarrow \left(\left(z\underset{\dot{}}{\le }x\wedge z\underset{\dot{}}{\le }y\right)\wedge \forall w\in B\left(\left(w\underset{\dot{}}{\le }x\wedge w\underset{\dot{}}{\le }y\right)\to w\underset{\dot{}}{\le }z\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\}z\underset{\dot{}}{\le }v\wedge \forall w\in B\left(\forall v\in \left\{x,y\right\}w\underset{\dot{}}{\le }v\to w\underset{\dot{}}{\le }z\right)\right)\leftrightarrow \exists !z\in B\left(\left(z\underset{\dot{}}{\le }x\wedge z\underset{\dot{}}{\le }y\right)\wedge \forall w\in B\left(\left(w\underset{\dot{}}{\le }x\wedge w\underset{\dot{}}{\le }y\right)\to w\underset{\dot{}}{\le }z\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\}z\underset{\dot{}}{\le }v\wedge \forall w\in B\left(\forall v\in \left\{x,y\right\}w\underset{\dot{}}{\le }v\to w\underset{\dot{}}{\le }z\right)\right)\leftrightarrow \exists !z\in B\left(\left(z\underset{\dot{}}{\le }x\wedge z\underset{\dot{}}{\le }y\right)\wedge \forall w\in B\left(\left(w\underset{\dot{}}{\le }x\wedge w\underset{\dot{}}{\le }y\right)\to w\underset{\dot{}}{\le }z\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}G\leftrightarrow \exists !z\in B\left(\left(z\underset{\dot{}}{\le }x\wedge z\underset{\dot{}}{\le }y\right)\wedge \forall w\in B\left(\left(w\underset{\dot{}}{\le }x\wedge w\underset{\dot{}}{\le }y\right)\to w\underset{\dot{}}{\le }z\right)\right)\right)$$
19	18	2ralbidva	$$⊢\phi \to \left(\forall x\in B\forall y\in B\left\{x,y\right\}\in \mathrm{dom}G\leftrightarrow \forall x\in B\forall y\in B\exists !z\in B\left(\left(z\underset{\dot{}}{\le }x\wedge z\underset{\dot{}}{\le }y\right)\wedge \forall w\in B\left(\left(w\underset{\dot{}}{\le }x\wedge w\underset{\dot{}}{\le }y\right)\to w\underset{\dot{}}{\le }z\right)\right)\right)$$
20	6 19	bitrd	$$⊢\phi \to \left(\mathrm{dom}\underset{\dot{}}{\wedge }=B\times B\leftrightarrow \forall x\in B\forall y\in B\exists !z\in B\left(\left(z\underset{\dot{}}{\le }x\wedge z\underset{\dot{}}{\le }y\right)\wedge \forall w\in B\left(\left(w\underset{\dot{}}{\le }x\wedge w\underset{\dot{}}{\le }y\right)\to w\underset{\dot{}}{\le }z\right)\right)\right)$$