Metamath Proof Explorer

Theorem cnvref4

Description: Two ways to say that a relation is a subclass. (Contributed by Peter Mazsa, 11-Apr-2023)

Ref Expression
Assertion cnvref4 
|- ( Rel R -> ( ( R i^i ( dom R X. ran R ) ) C_ ( S i^i ( dom R X. ran R ) ) <-> R C_ S ) )

Proof

Step Hyp Ref Expression
1 dfrel6 
 |-  ( Rel R <-> ( R i^i ( dom R X. ran R ) ) = R )
2 1 biimpi 
 |-  ( Rel R -> ( R i^i ( dom R X. ran R ) ) = R )
3 2 dmeqd 
 |-  ( Rel R -> dom ( R i^i ( dom R X. ran R ) ) = dom R )
4 2 rneqd 
 |-  ( Rel R -> ran ( R i^i ( dom R X. ran R ) ) = ran R )
5 3 4 xpeq12d 
 |-  ( Rel R -> ( dom ( R i^i ( dom R X. ran R ) ) X. ran ( R i^i ( dom R X. ran R ) ) ) = ( dom R X. ran R ) )
6 5 ineq2d 
 |-  ( Rel R -> ( S i^i ( dom ( R i^i ( dom R X. ran R ) ) X. ran ( R i^i ( dom R X. ran R ) ) ) ) = ( S i^i ( dom R X. ran R ) ) )
7 6 sseq2d 
 |-  ( Rel R -> ( ( R i^i ( dom R X. ran R ) ) C_ ( S i^i ( dom ( R i^i ( dom R X. ran R ) ) X. ran ( R i^i ( dom R X. ran R ) ) ) ) <-> ( R i^i ( dom R X. ran R ) ) C_ ( S i^i ( dom R X. ran R ) ) ) )
8 relxp 
 |-  Rel ( dom R X. ran R )
9 relin2 
 |-  ( Rel ( dom R X. ran R ) -> Rel ( R i^i ( dom R X. ran R ) ) )
10 relssinxpdmrn 
 |-  ( Rel ( R i^i ( dom R X. ran R ) ) -> ( ( R i^i ( dom R X. ran R ) ) C_ ( S i^i ( dom ( R i^i ( dom R X. ran R ) ) X. ran ( R i^i ( dom R X. ran R ) ) ) ) <-> ( R i^i ( dom R X. ran R ) ) C_ S ) )
11 8 9 10 mp2b 
 |-  ( ( R i^i ( dom R X. ran R ) ) C_ ( S i^i ( dom ( R i^i ( dom R X. ran R ) ) X. ran ( R i^i ( dom R X. ran R ) ) ) ) <-> ( R i^i ( dom R X. ran R ) ) C_ S )
12 2 sseq1d 
 |-  ( Rel R -> ( ( R i^i ( dom R X. ran R ) ) C_ S <-> R C_ S ) )
13 11 12 bitrid 
 |-  ( Rel R -> ( ( R i^i ( dom R X. ran R ) ) C_ ( S i^i ( dom ( R i^i ( dom R X. ran R ) ) X. ran ( R i^i ( dom R X. ran R ) ) ) ) <-> R C_ S ) )
14 7 13 bitr3d 
 |-  ( Rel R -> ( ( R i^i ( dom R X. ran R ) ) C_ ( S i^i ( dom R X. ran R ) ) <-> R C_ S ) )