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	$$⊢\phi \to R\mathrm{Or}A$$
	infltoreq.2	$$⊢\phi \to B\subseteq A$$
	infltoreq.3	$$⊢\phi \to B\in \mathrm{Fin}$$
	infltoreq.4	$$⊢\phi \to C\in B$$
	infltoreq.5	$$⊢\phi \to S=inf\left(B,A,R\right)$$
Assertion	infltoreq	$$⊢\phi \to \left(SRC\vee C=S\right)$$

Proof

Step	Hyp	Ref	Expression
1		infltoreq.1	$$⊢\phi \to R\mathrm{Or}A$$
2		infltoreq.2	$$⊢\phi \to B\subseteq A$$
3		infltoreq.3	$$⊢\phi \to B\in \mathrm{Fin}$$
4		infltoreq.4	$$⊢\phi \to C\in B$$
5		infltoreq.5	$$⊢\phi \to S=inf\left(B,A,R\right)$$
6		cnvso	$$⊢R\mathrm{Or}A\leftrightarrow R^{-1}\mathrm{Or}A$$
7	1 6	sylib	$$⊢\phi \to R^{-1}\mathrm{Or}A$$
8		df-inf	$$⊢inf\left(B,A,R\right)=sup\left(B,A,R^{-1}\right)$$
9	5 8	eqtrdi	$$⊢\phi \to S=sup\left(B,A,R^{-1}\right)$$
10	7 2 3 4 9	supgtoreq	$$⊢\phi \to \left(C{R}^{-1}S\vee C=S\right)$$
11	4	ne0d	$$⊢\phi \to B\ne \varnothing$$
12		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$$
13	1 3 11 2 12	syl13anc	$$⊢\phi \to inf\left(B,A,R\right)\in B$$
14	5 13	eqeltrd	$$⊢\phi \to S\in B$$
15		brcnvg	$$⊢\left(C\in B\wedge S\in B\right)\to \left(C{R}^{-1}S\leftrightarrow SRC\right)$$
16	15	bicomd	$$⊢\left(C\in B\wedge S\in B\right)\to \left(SRC\leftrightarrow C{R}^{-1}S\right)$$
17	4 14 16	syl2anc	$$⊢\phi \to \left(SRC\leftrightarrow C{R}^{-1}S\right)$$
18	17	orbi1d	$$⊢\phi \to \left(\left(SRC\vee C=S\right)\leftrightarrow \left(C{R}^{-1}S\vee C=S\right)\right)$$
19	10 18	mpbird	$$⊢\phi \to \left(SRC\vee C=S\right)$$