Theorem glbprop

Description: Properties of greatest lower bound of a poset. (Contributed by NM, 7-Sep-2018)

	Ref	Expression
Hypotheses	glbprop.b	$$⊢B={\mathrm{Base}}_K$$
	glbprop.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	glbprop.u	$$⊢U=\mathrm{glb}\left(K\right)$$
	glbprop.k	$$⊢\phi \to K\in V$$
	glbprop.s	$$⊢\phi \to S\in \mathrm{dom}U$$
Assertion	glbprop	$$⊢\phi \to \left(\forall y\in SU\left(S\right)\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in Sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }U\left(S\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		glbprop.b	$$⊢B={\mathrm{Base}}_K$$
2		glbprop.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		glbprop.u	$$⊢U=\mathrm{glb}\left(K\right)$$
4		glbprop.k	$$⊢\phi \to K\in V$$
5		glbprop.s	$$⊢\phi \to S\in \mathrm{dom}U$$
6		biid	$$⊢\left(\forall y\in Sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in Sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)\leftrightarrow \left(\forall y\in Sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in Sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)$$
7	1 2 3 4 5	glbelss	$$⊢\phi \to S\subseteq B$$
8	1 2 3 6 4 7	glbval	$$⊢\phi \to U\left(S\right)=\left(\iota x\in B|\left(\forall y\in Sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in Sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)\right)$$
9	8	eqcomd	$$⊢\phi \to \left(\iota x\in B|\left(\forall y\in Sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in Sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)\right)=U\left(S\right)$$
10	1 3 4 5	glbcl	$$⊢\phi \to U\left(S\right)\in B$$
11	1 2 3 6 4 5	glbeu	$$⊢\phi \to \exists !x\in B\left(\forall y\in Sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in Sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)$$
12		breq1	$$⊢x=U\left(S\right)\to \left(x\underset{\dot{}}{\le }y\leftrightarrow U\left(S\right)\underset{\dot{}}{\le }y\right)$$
13	12	ralbidv	$$⊢x=U\left(S\right)\to \left(\forall y\in Sx\underset{\dot{}}{\le }y\leftrightarrow \forall y\in SU\left(S\right)\underset{\dot{}}{\le }y\right)$$
14		breq2	$$⊢x=U\left(S\right)\to \left(z\underset{\dot{}}{\le }x\leftrightarrow z\underset{\dot{}}{\le }U\left(S\right)\right)$$
15	14	imbi2d	$$⊢x=U\left(S\right)\to \left(\left(\forall y\in Sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\leftrightarrow \left(\forall y\in Sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }U\left(S\right)\right)\right)$$
16	15	ralbidv	$$⊢x=U\left(S\right)\to \left(\forall z\in B\left(\forall y\in Sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\leftrightarrow \forall z\in B\left(\forall y\in Sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }U\left(S\right)\right)\right)$$
17	13 16	anbi12d	$$⊢x=U\left(S\right)\to \left(\left(\forall y\in Sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in Sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)\leftrightarrow \left(\forall y\in SU\left(S\right)\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in Sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }U\left(S\right)\right)\right)\right)$$
18	17	riota2	$$⊢\left(U\left(S\right)\in B\wedge \exists !x\in B\left(\forall y\in Sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in Sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)\right)\to \left(\left(\forall y\in SU\left(S\right)\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in Sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }U\left(S\right)\right)\right)\leftrightarrow \left(\iota x\in B|\left(\forall y\in Sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in Sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)\right)=U\left(S\right)\right)$$
19	10 11 18	syl2anc	$$⊢\phi \to \left(\left(\forall y\in SU\left(S\right)\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in Sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }U\left(S\right)\right)\right)\leftrightarrow \left(\iota x\in B|\left(\forall y\in Sx\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in Sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }x\right)\right)\right)=U\left(S\right)\right)$$
20	9 19	mpbird	$$⊢\phi \to \left(\forall y\in SU\left(S\right)\underset{\dot{}}{\le }y\wedge \forall z\in B\left(\forall y\in Sz\underset{\dot{}}{\le }y\to z\underset{\dot{}}{\le }U\left(S\right)\right)\right)$$