Theorem brlb 32937

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

Hypotheses

Ref	Expression
brub.1	⊢ 𝑆 ∈ V
brub.2	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
brlb	⊢ (𝑆LB𝑅𝐴 ↔ ∀𝑥 ∈ 𝑆 𝐴𝑅𝑥)

Distinct variable groups:   𝑥,𝐴   𝑥,𝑅   𝑥,𝑆

Proof of Theorem brlb

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

Syntax hints:   ↔ wb 198   ∈ wcel 2050  ∀wral 3082  Vcvv 3409   class class class wbr 4923  ^◡ccnv 5400  UBcub 32834  LBclb 32835

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2744  ax-sep 5054  ax-nul 5061  ax-pr 5180

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-ral 3087  df-rex 3088  df-rab 3091  df-v 3411  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-nul 4173  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-br 4924  df-opab 4986  df-eprel 5311  df-xp 5407  df-cnv 5409  df-co 5410  df-ub 32858  df-lb 32859

This theorem is referenced by: (None)