Theorem brlb

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

	Ref	Expression
Hypotheses	brub.1	⊢ 𝑆 ∈ V
	brub.2	⊢ 𝐴 ∈ V
Assertion	brlb	⊢ ( 𝑆 LB 𝑅 𝐴 ↔ ∀ 𝑥 ∈ 𝑆 𝐴 𝑅 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		brub.1	⊢ 𝑆 ∈ V
2		brub.2	⊢ 𝐴 ∈ V
3		df-lb	⊢ LB 𝑅 = UB ◡ 𝑅
4	3	breqi	⊢ ( 𝑆 LB 𝑅 𝐴 ↔ 𝑆 UB ◡ 𝑅 𝐴 )
5	1 2	brub	⊢ ( 𝑆 UB ◡ 𝑅 𝐴 ↔ ∀ 𝑥 ∈ 𝑆 𝑥 ◡ 𝑅 𝐴 )
6		vex	⊢ 𝑥 ∈ V
7	6 2	brcnv	⊢ ( 𝑥 ◡ 𝑅 𝐴 ↔ 𝐴 𝑅 𝑥 )
8	7	ralbii	⊢ ( ∀ 𝑥 ∈ 𝑆 𝑥 ◡ 𝑅 𝐴 ↔ ∀ 𝑥 ∈ 𝑆 𝐴 𝑅 𝑥 )
9	4 5 8	3bitri	⊢ ( 𝑆 LB 𝑅 𝐴 ↔ ∀ 𝑥 ∈ 𝑆 𝐴 𝑅 𝑥 )