Theorem brlb

Description: Binary relation form of the lower bound functor. (Contributed by Scott Fenton, 3-May-2018)

	Ref	Expression
Hypotheses	brub.1	$$⊢S\in \mathrm{V}$$
	brub.2	$$⊢A\in \mathrm{V}$$
Assertion	brlb	$$⊢S\mathrm{LB}RA\leftrightarrow \forall x\in SARx$$

Proof

Step	Hyp	Ref	Expression
1		brub.1	$$⊢S\in \mathrm{V}$$
2		brub.2	$$⊢A\in \mathrm{V}$$
3		df-lb	$$⊢\mathrm{LB}R=\mathrm{UB}{R}^{-1}$$
4	3	breqi	$$⊢S\mathrm{LB}RA\leftrightarrow S\mathrm{UB}{R}^{-1}A$$
5	1 2	brub	$$⊢S\mathrm{UB}{R}^{-1}A\leftrightarrow \forall x\in Sx{R}^{-1}A$$
6		vex	$$⊢x\in \mathrm{V}$$
7	6 2	brcnv	$$⊢x{R}^{-1}A\leftrightarrow ARx$$
8	7	ralbii	$$⊢\forall x\in Sx{R}^{-1}A\leftrightarrow \forall x\in SARx$$
9	4 5 8	3bitri	$$⊢S\mathrm{LB}RA\leftrightarrow \forall x\in SARx$$