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