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

Metamath Proof Explorer

Theorem brcodir

Description: Two ways of saying that two elements have an upper bound. (Contributed by Mario Carneiro, 3-Nov-2015)

Ref Expression
Assertion brcodir 
|- ( ( A e. V /\ B e. W ) -> ( A ( `' R o. R ) B <-> E. z ( A R z /\ B R z ) ) )

Proof

Step Hyp Ref Expression
1 brcog 
 |-  ( ( A e. V /\ B e. W ) -> ( A ( `' R o. R ) B <-> E. z ( A R z /\ z `' R B ) ) )
2 vex 
 |-  z e. _V
3 brcnvg 
 |-  ( ( z e. _V /\ B e. W ) -> ( z `' R B <-> B R z ) )
4 2 3 mpan 
 |-  ( B e. W -> ( z `' R B <-> B R z ) )
5 4 anbi2d 
 |-  ( B e. W -> ( ( A R z /\ z `' R B ) <-> ( A R z /\ B R z ) ) )
6 5 adantl 
 |-  ( ( A e. V /\ B e. W ) -> ( ( A R z /\ z `' R B ) <-> ( A R z /\ B R z ) ) )
7 6 exbidv 
 |-  ( ( A e. V /\ B e. W ) -> ( E. z ( A R z /\ z `' R B ) <-> E. z ( A R z /\ B R z ) ) )
8 1 7 bitrd 
 |-  ( ( A e. V /\ B e. W ) -> ( A ( `' R o. R ) B <-> E. z ( A R z /\ B R z ) ) )