Theorem fiinfcl

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

	Ref	Expression
Assertion	fiinfcl	|- ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> inf ( B , A , R ) e. B )

Proof

Step	Hyp	Ref	Expression
1		df-inf	|- inf ( B , A , R ) = sup ( B , A , `' R )
2		cnvso	|- ( R Or A <-> `' R Or A )
3		fisupcl	|- ( ( `' R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> sup ( B , A , `' R ) e. B )
4	2 3	sylanb	|- ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> sup ( B , A , `' R ) e. B )
5	1 4	eqeltrid	|- ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> inf ( B , A , R ) e. B )