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 ) |
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 ) |