Metamath Proof Explorer

Theorem resssxp

Description: If the R -image of a class A is a subclass of B , then the restriction of R to A is a subset of the Cartesian product of A and B . (Contributed by RP, 24-Dec-2019)

Ref Expression
Assertion resssxp 
|- ( ( R " A ) C_ B <-> ( R |` A ) C_ ( A X. B ) )

Proof

Step Hyp Ref Expression
1 df-ima 
 |-  ( R " A ) = ran ( R |` A )
2 1 sseq1i 
 |-  ( ( R " A ) C_ B <-> ran ( R |` A ) C_ B )
3 dmres 
 |-  dom ( R |` A ) = ( A i^i dom R )
4 inss1 
 |-  ( A i^i dom R ) C_ A
5 3 4 eqsstri 
 |-  dom ( R |` A ) C_ A
6 5 biantrur 
 |-  ( ran ( R |` A ) C_ B <-> ( dom ( R |` A ) C_ A /\ ran ( R |` A ) C_ B ) )
7 relres 
 |-  Rel ( R |` A )
8 relssdmrn 
 |-  ( Rel ( R |` A ) -> ( R |` A ) C_ ( dom ( R |` A ) X. ran ( R |` A ) ) )
9 7 8 ax-mp 
 |-  ( R |` A ) C_ ( dom ( R |` A ) X. ran ( R |` A ) )
10 xpss12 
 |-  ( ( dom ( R |` A ) C_ A /\ ran ( R |` A ) C_ B ) -> ( dom ( R |` A ) X. ran ( R |` A ) ) C_ ( A X. B ) )
11 9 10 sstrid 
 |-  ( ( dom ( R |` A ) C_ A /\ ran ( R |` A ) C_ B ) -> ( R |` A ) C_ ( A X. B ) )
12 dmss 
 |-  ( ( R |` A ) C_ ( A X. B ) -> dom ( R |` A ) C_ dom ( A X. B ) )
13 dmxpss 
 |-  dom ( A X. B ) C_ A
14 12 13 sstrdi 
 |-  ( ( R |` A ) C_ ( A X. B ) -> dom ( R |` A ) C_ A )
15 rnss 
 |-  ( ( R |` A ) C_ ( A X. B ) -> ran ( R |` A ) C_ ran ( A X. B ) )
16 rnxpss 
 |-  ran ( A X. B ) C_ B
17 15 16 sstrdi 
 |-  ( ( R |` A ) C_ ( A X. B ) -> ran ( R |` A ) C_ B )
18 14 17 jca 
 |-  ( ( R |` A ) C_ ( A X. B ) -> ( dom ( R |` A ) C_ A /\ ran ( R |` A ) C_ B ) )
19 11 18 impbii 
 |-  ( ( dom ( R |` A ) C_ A /\ ran ( R |` A ) C_ B ) <-> ( R |` A ) C_ ( A X. B ) )
20 2 6 19 3bitri 
 |-  ( ( R " A ) C_ B <-> ( R |` A ) C_ ( A X. B ) )