Theorem posglbd

Description: Properties which determine the greatest lower bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015)

	Ref	Expression
Hypotheses	posglbd.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	posglbd.b	$$⊢\phi \to B={\mathrm{Base}}_K$$
	posglbd.g	$$⊢\phi \to G=\mathrm{glb}\left(K\right)$$
	posglbd.k	$$⊢\phi \to K\in \mathrm{Poset}$$
	posglbd.s	$$⊢\phi \to S\subseteq B$$
	posglbd.t	$$⊢\phi \to T\in B$$
	posglbd.lb	$$⊢\left(\phi \wedge x\in S\right)\to T\underset{\dot{}}{\le }x$$
	posglbd.gt	$$⊢\left(\phi \wedge y\in B\wedge \forall x\in Sy\underset{\dot{}}{\le }x\right)\to y\underset{\dot{}}{\le }T$$
Assertion	posglbd	$$⊢\phi \to G\left(S\right)=T$$

Proof

Step	Hyp	Ref	Expression
1		posglbd.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		posglbd.b	$$⊢\phi \to B={\mathrm{Base}}_K$$
3		posglbd.g	$$⊢\phi \to G=\mathrm{glb}\left(K\right)$$
4		posglbd.k	$$⊢\phi \to K\in \mathrm{Poset}$$
5		posglbd.s	$$⊢\phi \to S\subseteq B$$
6		posglbd.t	$$⊢\phi \to T\in B$$
7		posglbd.lb	$$⊢\left(\phi \wedge x\in S\right)\to T\underset{\dot{}}{\le }x$$
8		posglbd.gt	$$⊢\left(\phi \wedge y\in B\wedge \forall x\in Sy\underset{\dot{}}{\le }x\right)\to y\underset{\dot{}}{\le }T$$
9		eqid	$$⊢\mathrm{ODual}\left(K\right)=\mathrm{ODual}\left(K\right)$$
10	9 1	oduleval	$$⊢{\underset{\dot{}}{\le }}^{-1}={\le }_{\mathrm{ODual}\left(K\right)}$$
11		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
12	9 11	odubas	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_{\mathrm{ODual}\left(K\right)}$$
13	2 12	eqtrdi	$$⊢\phi \to B={\mathrm{Base}}_{\mathrm{ODual}\left(K\right)}$$
14		eqid	$$⊢\mathrm{glb}\left(K\right)=\mathrm{glb}\left(K\right)$$
15	9 14	odulub	$$⊢K\in \mathrm{Poset}\to \mathrm{glb}\left(K\right)=\mathrm{lub}\left(\mathrm{ODual}\left(K\right)\right)$$
16	4 15	syl	$$⊢\phi \to \mathrm{glb}\left(K\right)=\mathrm{lub}\left(\mathrm{ODual}\left(K\right)\right)$$
17	3 16	eqtrd	$$⊢\phi \to G=\mathrm{lub}\left(\mathrm{ODual}\left(K\right)\right)$$
18	9	odupos	$$⊢K\in \mathrm{Poset}\to \mathrm{ODual}\left(K\right)\in \mathrm{Poset}$$
19	4 18	syl	$$⊢\phi \to \mathrm{ODual}\left(K\right)\in \mathrm{Poset}$$
20		vex	$$⊢x\in \mathrm{V}$$
21		brcnvg	$$⊢\left(x\in \mathrm{V}\wedge T\in B\right)\to \left(x{\underset{\dot{}}{\le }}^{-1}T\leftrightarrow T\underset{\dot{}}{\le }x\right)$$
22	20 6 21	sylancr	$$⊢\phi \to \left(x{\underset{\dot{}}{\le }}^{-1}T\leftrightarrow T\underset{\dot{}}{\le }x\right)$$
23	22	adantr	$$⊢\left(\phi \wedge x\in S\right)\to \left(x{\underset{\dot{}}{\le }}^{-1}T\leftrightarrow T\underset{\dot{}}{\le }x\right)$$
24	7 23	mpbird	$$⊢\left(\phi \wedge x\in S\right)\to x{\underset{\dot{}}{\le }}^{-1}T$$
25		vex	$$⊢y\in \mathrm{V}$$
26	20 25	brcnv	$$⊢x{\underset{\dot{}}{\le }}^{-1}y\leftrightarrow y\underset{\dot{}}{\le }x$$
27	26	ralbii	$$⊢\forall x\in Sx{\underset{\dot{}}{\le }}^{-1}y\leftrightarrow \forall x\in Sy\underset{\dot{}}{\le }x$$
28	27 8	syl3an3b	$$⊢\left(\phi \wedge y\in B\wedge \forall x\in Sx{\underset{\dot{}}{\le }}^{-1}y\right)\to y\underset{\dot{}}{\le }T$$
29		brcnvg	$$⊢\left(T\in B\wedge y\in \mathrm{V}\right)\to \left(T{\underset{\dot{}}{\le }}^{-1}y\leftrightarrow y\underset{\dot{}}{\le }T\right)$$
30	6 25 29	sylancl	$$⊢\phi \to \left(T{\underset{\dot{}}{\le }}^{-1}y\leftrightarrow y\underset{\dot{}}{\le }T\right)$$
31	30	3ad2ant1	$$⊢\left(\phi \wedge y\in B\wedge \forall x\in Sx{\underset{\dot{}}{\le }}^{-1}y\right)\to \left(T{\underset{\dot{}}{\le }}^{-1}y\leftrightarrow y\underset{\dot{}}{\le }T\right)$$
32	28 31	mpbird	$$⊢\left(\phi \wedge y\in B\wedge \forall x\in Sx{\underset{\dot{}}{\le }}^{-1}y\right)\to T{\underset{\dot{}}{\le }}^{-1}y$$
33	10 13 17 19 5 6 24 32	poslubdg	$$⊢\phi \to G\left(S\right)=T$$