Theorem fiinfcl

Description: A nonempty finite set contains its infimum. (Contributed by AV, 3-Sep-2020)

	Ref	Expression
Assertion	fiinfcl	$$⊢\left(R\mathrm{Or}A\wedge \left(B\in \mathrm{Fin}\wedge B\ne \varnothing \wedge B\subseteq A\right)\right)\to inf\left(B,A,R\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		df-inf	$$⊢inf\left(B,A,R\right)=sup\left(B,A,R^{-1}\right)$$
2		cnvso	$$⊢R\mathrm{Or}A\leftrightarrow R^{-1}\mathrm{Or}A$$
3		fisupcl	$$⊢\left(R^{-1}\mathrm{Or}A\wedge \left(B\in \mathrm{Fin}\wedge B\ne \varnothing \wedge B\subseteq A\right)\right)\to sup\left(B,A,R^{-1}\right)\in B$$
4	2 3	sylanb	$$⊢\left(R\mathrm{Or}A\wedge \left(B\in \mathrm{Fin}\wedge B\ne \varnothing \wedge B\subseteq A\right)\right)\to sup\left(B,A,R^{-1}\right)\in B$$
5	1 4	eqeltrid	$$⊢\left(R\mathrm{Or}A\wedge \left(B\in \mathrm{Fin}\wedge B\ne \varnothing \wedge B\subseteq A\right)\right)\to inf\left(B,A,R\right)\in B$$