This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ V
brub.2 ⊢ A ∈ V
Assertion brlb ⊢ S LB R A ↔ ∀ x ∈ S A R x

Proof

Step Hyp Ref Expression
1 brub.1 ⊢ S ∈ V
2 brub.2 ⊢ A ∈ V
3 df-lb ⊢ LB R = UB R -1
4 3 breqi ⊢ S LB R A ↔ S UB R -1 A
5 1 2 brub ⊢ S UB R -1 A ↔ ∀ x ∈ S x R -1 A
6 vex ⊢ x ∈ V
7 6 2 brcnv ⊢ x R -1 A ↔ A R x
8 7 ralbii ⊢ ∀ x ∈ S x R -1 A ↔ ∀ x ∈ S A R x
9 4 5 8 3bitri ⊢ S LB R A ↔ ∀ x ∈ S A R x