Theorem infltoreq

Description: The infimum of a finite set is less than or equal to all the elements of the set. (Contributed by AV, 4-Sep-2020)

	Ref	Expression
Hypotheses	infltoreq.1	|- ( ph -> R Or A )
	infltoreq.2	|- ( ph -> B C_ A )
	infltoreq.3	|- ( ph -> B e. Fin )
	infltoreq.4	|- ( ph -> C e. B )
	infltoreq.5	|- ( ph -> S = inf ( B , A , R ) )
Assertion	infltoreq	|- ( ph -> ( S R C \/ C = S ) )

Proof

Step	Hyp	Ref	Expression
1		infltoreq.1	|- ( ph -> R Or A )
2		infltoreq.2	|- ( ph -> B C_ A )
3		infltoreq.3	|- ( ph -> B e. Fin )
4		infltoreq.4	|- ( ph -> C e. B )
5		infltoreq.5	|- ( ph -> S = inf ( B , A , R ) )
6		cnvso	|- ( R Or A <-> `' R Or A )
7	1 6	sylib	|- ( ph -> `' R Or A )
8		df-inf	|- inf ( B , A , R ) = sup ( B , A , `' R )
9	5 8	eqtrdi	|- ( ph -> S = sup ( B , A , `' R ) )
10	7 2 3 4 9	supgtoreq	|- ( ph -> ( C `' R S \/ C = S ) )
11	4	ne0d	|- ( ph -> B =/= (/) )
12		fiinfcl	|- ( ( R Or A /\ ( B e. Fin /\ B =/= (/) /\ B C_ A ) ) -> inf ( B , A , R ) e. B )
13	1 3 11 2 12	syl13anc	|- ( ph -> inf ( B , A , R ) e. B )
14	5 13	eqeltrd	|- ( ph -> S e. B )
15		brcnvg	|- ( ( C e. B /\ S e. B ) -> ( C `' R S <-> S R C ) )
16	15	bicomd	|- ( ( C e. B /\ S e. B ) -> ( S R C <-> C `' R S ) )
17	4 14 16	syl2anc	|- ( ph -> ( S R C <-> C `' R S ) )
18	17	orbi1d	|- ( ph -> ( ( S R C \/ C = S ) <-> ( C `' R S \/ C = S ) ) )
19	10 18	mpbird	|- ( ph -> ( S R C \/ C = S ) )