Metamath Proof Explorer


Theorem brlb

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

Ref Expression
Hypotheses brub.1
|- S e. _V
brub.2
|- A e. _V
Assertion brlb
|- ( S LB R A <-> A. x e. S A R x )

Proof

Step Hyp Ref Expression
1 brub.1
 |-  S e. _V
2 brub.2
 |-  A e. _V
3 df-lb
 |-  LB R = UB `' R
4 3 breqi
 |-  ( S LB R A <-> S UB `' R A )
5 1 2 brub
 |-  ( S UB `' R A <-> A. x e. S x `' R A )
6 vex
 |-  x e. _V
7 6 2 brcnv
 |-  ( x `' R A <-> A R x )
8 7 ralbii
 |-  ( A. x e. S x `' R A <-> A. x e. S A R x )
9 4 5 8 3bitri
 |-  ( S LB R A <-> A. x e. S A R x )