Metamath Proof Explorer

Theorem relrelss

Description: Two ways to describe the structure of a two-place operation. (Contributed by NM, 17-Dec-2008)

Ref Expression
Assertion relrelss 
|- ( ( Rel A /\ Rel dom A ) <-> A C_ ( ( _V X. _V ) X. _V ) )

Proof

Step Hyp Ref Expression
1 df-rel 
 |-  ( Rel dom A <-> dom A C_ ( _V X. _V ) )
2 1 anbi2i 
 |-  ( ( Rel A /\ Rel dom A ) <-> ( Rel A /\ dom A C_ ( _V X. _V ) ) )
3 relssdmrn 
 |-  ( Rel A -> A C_ ( dom A X. ran A ) )
4 ssv 
 |-  ran A C_ _V
5 xpss12 
 |-  ( ( dom A C_ ( _V X. _V ) /\ ran A C_ _V ) -> ( dom A X. ran A ) C_ ( ( _V X. _V ) X. _V ) )
6 4 5 mpan2 
 |-  ( dom A C_ ( _V X. _V ) -> ( dom A X. ran A ) C_ ( ( _V X. _V ) X. _V ) )
7 3 6 sylan9ss 
 |-  ( ( Rel A /\ dom A C_ ( _V X. _V ) ) -> A C_ ( ( _V X. _V ) X. _V ) )
8 xpss 
 |-  ( ( _V X. _V ) X. _V ) C_ ( _V X. _V )
9 sstr 
 |-  ( ( A C_ ( ( _V X. _V ) X. _V ) /\ ( ( _V X. _V ) X. _V ) C_ ( _V X. _V ) ) -> A C_ ( _V X. _V ) )
10 8 9 mpan2 
 |-  ( A C_ ( ( _V X. _V ) X. _V ) -> A C_ ( _V X. _V ) )
11 df-rel 
 |-  ( Rel A <-> A C_ ( _V X. _V ) )
12 10 11 sylibr 
 |-  ( A C_ ( ( _V X. _V ) X. _V ) -> Rel A )
13 dmss 
 |-  ( A C_ ( ( _V X. _V ) X. _V ) -> dom A C_ dom ( ( _V X. _V ) X. _V ) )
14 vn0 
 |-  _V =/= (/)
15 dmxp 
 |-  ( _V =/= (/) -> dom ( ( _V X. _V ) X. _V ) = ( _V X. _V ) )
16 14 15 ax-mp 
 |-  dom ( ( _V X. _V ) X. _V ) = ( _V X. _V )
17 13 16 sseqtrdi 
 |-  ( A C_ ( ( _V X. _V ) X. _V ) -> dom A C_ ( _V X. _V ) )
18 12 17 jca 
 |-  ( A C_ ( ( _V X. _V ) X. _V ) -> ( Rel A /\ dom A C_ ( _V X. _V ) ) )
19 7 18 impbii 
 |-  ( ( Rel A /\ dom A C_ ( _V X. _V ) ) <-> A C_ ( ( _V X. _V ) X. _V ) )
20 2 19 bitri 
 |-  ( ( Rel A /\ Rel dom A ) <-> A C_ ( ( _V X. _V ) X. _V ) )