Theorem tosglb

Description: Same theorem as toslub , for infinimum. (Contributed by Thierry Arnoux, 17-Feb-2018) (Revised by AV, 28-Sep-2020)

	Ref	Expression
Hypotheses	tosglb.b	$$⊢B={\mathrm{Base}}_K$$
	tosglb.l	$$⊢\underset{\dot{}}{<}={<}_K$$
	tosglb.1	$$⊢\phi \to K\in \mathrm{Toset}$$
	tosglb.2	$$⊢\phi \to A\subseteq B$$
Assertion	tosglb	$$⊢\phi \to \mathrm{glb}\left(K\right)\left(A\right)=sup\left(A,B,\underset{\dot{}}{<}\right)$$

Proof

Step	Hyp	Ref	Expression
1		tosglb.b	$$⊢B={\mathrm{Base}}_K$$
2		tosglb.l	$$⊢\underset{\dot{}}{<}={<}_K$$
3		tosglb.1	$$⊢\phi \to K\in \mathrm{Toset}$$
4		tosglb.2	$$⊢\phi \to A\subseteq B$$
5		eqid	$$⊢{\le }_K={\le }_K$$
6	1 2 3 4 5	tosglblem	$$⊢\left(\phi \wedge a\in B\right)\to \left(\left(\forall b\in Aa{\le }_{K}b\wedge \forall c\in B\left(\forall b\in Ac{\le }_{K}b\to c{\le }_{K}a\right)\right)\leftrightarrow \left(\forall b\in A\neg a{\underset{\dot{}}{<}}^{-1}b\wedge \forall b\in B\left(b{\underset{\dot{}}{<}}^{-1}a\to \exists d\in Ab{\underset{\dot{}}{<}}^{-1}d\right)\right)\right)$$
7	6	riotabidva	$$⊢\phi \to \left(\iota a\in B|\left(\forall b\in Aa{\le }_{K}b\wedge \forall c\in B\left(\forall b\in Ac{\le }_{K}b\to c{\le }_{K}a\right)\right)\right)=\left(\iota a\in B|\left(\forall b\in A\neg a{\underset{\dot{}}{<}}^{-1}b\wedge \forall b\in B\left(b{\underset{\dot{}}{<}}^{-1}a\to \exists d\in Ab{\underset{\dot{}}{<}}^{-1}d\right)\right)\right)$$
8		eqid	$$⊢\mathrm{glb}\left(K\right)=\mathrm{glb}\left(K\right)$$
9		biid	$$⊢\left(\forall b\in Aa{\le }_{K}b\wedge \forall c\in B\left(\forall b\in Ac{\le }_{K}b\to c{\le }_{K}a\right)\right)\leftrightarrow \left(\forall b\in Aa{\le }_{K}b\wedge \forall c\in B\left(\forall b\in Ac{\le }_{K}b\to c{\le }_{K}a\right)\right)$$
10	1 5 8 9 3 4	glbval	$$⊢\phi \to \mathrm{glb}\left(K\right)\left(A\right)=\left(\iota a\in B|\left(\forall b\in Aa{\le }_{K}b\wedge \forall c\in B\left(\forall b\in Ac{\le }_{K}b\to c{\le }_{K}a\right)\right)\right)$$
11	1 5 2	tosso	$$⊢K\in \mathrm{Toset}\to \left(K\in \mathrm{Toset}\leftrightarrow \left(\underset{\dot{}}{<}\mathrm{Or}B\wedge {\mathrm{I}\upharpoonright }_B\subseteq {\le }_K\right)\right)$$
12	11	ibi	$$⊢K\in \mathrm{Toset}\to \left(\underset{\dot{}}{<}\mathrm{Or}B\wedge {\mathrm{I}\upharpoonright }_B\subseteq {\le }_K\right)$$
13	12	simpld	$$⊢K\in \mathrm{Toset}\to \underset{\dot{}}{<}\mathrm{Or}B$$
14		cnvso	$$⊢\underset{\dot{}}{<}\mathrm{Or}B\leftrightarrow {\underset{\dot{}}{<}}^{-1}\mathrm{Or}B$$
15	13 14	sylib	$$⊢K\in \mathrm{Toset}\to {\underset{\dot{}}{<}}^{-1}\mathrm{Or}B$$
16		id	$$⊢{\underset{\dot{}}{<}}^{-1}\mathrm{Or}B\to {\underset{\dot{}}{<}}^{-1}\mathrm{Or}B$$
17	16	supval2	$$⊢{\underset{\dot{}}{<}}^{-1}\mathrm{Or}B\to sup\left(A,B,{\underset{\dot{}}{<}}^{-1}\right)=\left(\iota a\in B|\left(\forall b\in A\neg a{\underset{\dot{}}{<}}^{-1}b\wedge \forall b\in B\left(b{\underset{\dot{}}{<}}^{-1}a\to \exists d\in Ab{\underset{\dot{}}{<}}^{-1}d\right)\right)\right)$$
18	3 15 17	3syl	$$⊢\phi \to sup\left(A,B,{\underset{\dot{}}{<}}^{-1}\right)=\left(\iota a\in B|\left(\forall b\in A\neg a{\underset{\dot{}}{<}}^{-1}b\wedge \forall b\in B\left(b{\underset{\dot{}}{<}}^{-1}a\to \exists d\in Ab{\underset{\dot{}}{<}}^{-1}d\right)\right)\right)$$
19	7 10 18	3eqtr4d	$$⊢\phi \to \mathrm{glb}\left(K\right)\left(A\right)=sup\left(A,B,{\underset{\dot{}}{<}}^{-1}\right)$$
20		df-inf	$$⊢sup\left(A,B,\underset{\dot{}}{<}\right)=sup\left(A,B,{\underset{\dot{}}{<}}^{-1}\right)$$
21	20	eqcomi	$$⊢sup\left(A,B,{\underset{\dot{}}{<}}^{-1}\right)=sup\left(A,B,\underset{\dot{}}{<}\right)$$
22	21	a1i	$$⊢\phi \to sup\left(A,B,{\underset{\dot{}}{<}}^{-1}\right)=sup\left(A,B,\underset{\dot{}}{<}\right)$$
23	19 22	eqtrd	$$⊢\phi \to \mathrm{glb}\left(K\right)\left(A\right)=sup\left(A,B,\underset{\dot{}}{<}\right)$$