Metamath Proof Explorer

Theorem codir

Description: Two ways of saying a relation is directed. (Contributed by Mario Carneiro, 22-Nov-2013)

Ref Expression
Assertion codir 
|- ( ( A X. B ) C_ ( `' R o. R ) <-> A. x e. A A. y e. B E. z ( x R z /\ y R z ) )

Proof

Step Hyp Ref Expression
1 opelxp 
 |-  ( <. x , y >. e. ( A X. B ) <-> ( x e. A /\ y e. B ) )
2 df-br 
 |-  ( x ( `' R o. R ) y <-> <. x , y >. e. ( `' R o. R ) )
3 brcodir 
 |-  ( ( x e. _V /\ y e. _V ) -> ( x ( `' R o. R ) y <-> E. z ( x R z /\ y R z ) ) )
4 3 el2v 
 |-  ( x ( `' R o. R ) y <-> E. z ( x R z /\ y R z ) )
5 2 4 bitr3i 
 |-  ( <. x , y >. e. ( `' R o. R ) <-> E. z ( x R z /\ y R z ) )
6 1 5 imbi12i 
 |-  ( ( <. x , y >. e. ( A X. B ) -> <. x , y >. e. ( `' R o. R ) ) <-> ( ( x e. A /\ y e. B ) -> E. z ( x R z /\ y R z ) ) )
7 6 2albii 
 |-  ( A. x A. y ( <. x , y >. e. ( A X. B ) -> <. x , y >. e. ( `' R o. R ) ) <-> A. x A. y ( ( x e. A /\ y e. B ) -> E. z ( x R z /\ y R z ) ) )
8 relxp 
 |-  Rel ( A X. B )
9 ssrel 
 |-  ( Rel ( A X. B ) -> ( ( A X. B ) C_ ( `' R o. R ) <-> A. x A. y ( <. x , y >. e. ( A X. B ) -> <. x , y >. e. ( `' R o. R ) ) ) )
10 8 9 ax-mp 
 |-  ( ( A X. B ) C_ ( `' R o. R ) <-> A. x A. y ( <. x , y >. e. ( A X. B ) -> <. x , y >. e. ( `' R o. R ) ) )
11 r2al 
 |-  ( A. x e. A A. y e. B E. z ( x R z /\ y R z ) <-> A. x A. y ( ( x e. A /\ y e. B ) -> E. z ( x R z /\ y R z ) ) )
12 7 10 11 3bitr4i 
 |-  ( ( A X. B ) C_ ( `' R o. R ) <-> A. x e. A A. y e. B E. z ( x R z /\ y R z ) )