Theorem meetval2

Description: Value of meet for a poset with LUB expanded. (Contributed by NM, 16-Sep-2011) (Revised by NM, 11-Sep-2018)

	Ref	Expression
Hypotheses	meetval2.b	$$⊢B={\mathrm{Base}}_K$$
	meetval2.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	meetval2.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	meetval2.k	$$⊢\phi \to K\in V$$
	meetval2.x	$$⊢\phi \to X\in B$$
	meetval2.y	$$⊢\phi \to Y\in B$$
Assertion	meetval2	$$⊢\phi \to X\underset{\dot{}}{\wedge }Y=\left(\iota x\in B|\left(\left(x\underset{\dot{}}{\le }X\wedge x\underset{\dot{}}{\le }Y\right)\wedge \forall z\in B\left(\left(z\underset{\dot{}}{\le }X\wedge z\underset{\dot{}}{\le }Y\right)\to z\underset{\dot{}}{\le }x\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		meetval2.b	$$⊢B={\mathrm{Base}}_K$$
2		meetval2.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		meetval2.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		meetval2.k	$$⊢\phi \to K\in V$$
5		meetval2.x	$$⊢\phi \to X\in B$$
6		meetval2.y	$$⊢\phi \to Y\in B$$
7		eqid	$$⊢\mathrm{glb}\left(K\right)=\mathrm{glb}\left(K\right)$$
8	7 3 4 5 6	meetval	$$⊢\phi \to X\underset{\dot{}}{\wedge }Y=\mathrm{glb}\left(K\right)\left(\left\{X,Y\right\}\right)$$
9		biid	$$⊢\left(\forall y\in \left\{X,Y\right\}x\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in \left\{X,Y\right\}z\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)\leftrightarrow \left(\forall y\in \left\{X,Y\right\}x\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in \left\{X,Y\right\}z\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)$$
10	5 6	prssd	$$⊢\phi \to \left\{X,Y\right\}\subseteq B$$
11	1 2 7 9 4 10	glbval	$$⊢\phi \to \mathrm{glb}\left(K\right)\left(\left\{X,Y\right\}\right)=\left(\iota x\in B|\left(\forall y\in \left\{X,Y\right\}x\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in \left\{X,Y\right\}z\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)\right)$$
12	1 2 3 4 5 6	meetval2lem	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(\left(\forall y\in \left\{X,Y\right\}x\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in \left\{X,Y\right\}z\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)\leftrightarrow \left(\left(x\underset{\dot{}}{\le }X\wedge x\underset{\dot{}}{\le }Y\right)\wedge \forall z\in B\left(\left(z\underset{\dot{}}{\le }X\wedge z\underset{\dot{}}{\le }Y\right)\to z\underset{\dot{}}{\le }x\right)\right)\right)$$
13	12	riotabidv	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(\iota x\in B|\left(\forall y\in \left\{X,Y\right\}x\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in \left\{X,Y\right\}z\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)\right)=\left(\iota x\in B|\left(\left(x\underset{\dot{}}{\le }X\wedge x\underset{\dot{}}{\le }Y\right)\wedge \forall z\in B\left(\left(z\underset{\dot{}}{\le }X\wedge z\underset{\dot{}}{\le }Y\right)\to z\underset{\dot{}}{\le }x\right)\right)\right)$$
14	5 6 13	syl2anc	$$⊢\phi \to \left(\iota x\in B|\left(\forall y\in \left\{X,Y\right\}x\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in \left\{X,Y\right\}z\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)\right)=\left(\iota x\in B|\left(\left(x\underset{\dot{}}{\le }X\wedge x\underset{\dot{}}{\le }Y\right)\wedge \forall z\in B\left(\left(z\underset{\dot{}}{\le }X\wedge z\underset{\dot{}}{\le }Y\right)\to z\underset{\dot{}}{\le }x\right)\right)\right)$$
15	8 11 14	3eqtrd	$$⊢\phi \to X\underset{\dot{}}{\wedge }Y=\left(\iota x\in B|\left(\left(x\underset{\dot{}}{\le }X\wedge x\underset{\dot{}}{\le }Y\right)\wedge \forall z\in B\left(\left(z\underset{\dot{}}{\le }X\wedge z\underset{\dot{}}{\le }Y\right)\to z\underset{\dot{}}{\le }x\right)\right)\right)$$