Metamath Proof Explorer

Theorem trrelsuperrel2dg

Description: Concrete construction of a superclass of relation R which is a transitive relation. (Contributed by RP, 20-Jul-2020)

Ref Expression
Hypothesis trrelsuperrel2dg.s 
|- ( ph -> S = ( R u. ( dom R X. ran R ) ) )
Assertion trrelsuperrel2dg 
|- ( ph -> ( R C_ S /\ ( S o. S ) C_ S ) )

Proof

Step Hyp Ref Expression
1 trrelsuperrel2dg.s 
 |-  ( ph -> S = ( R u. ( dom R X. ran R ) ) )
2 ssun1 
 |-  R C_ ( R u. ( dom R X. ran R ) )
3 2 1 sseqtrrid 
 |-  ( ph -> R C_ S )
4 xptrrel 
 |-  ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) C_ ( dom R X. ran R )
5 ssun2 
 |-  ( dom R X. ran R ) C_ ( R u. ( dom R X. ran R ) )
6 4 5 sstri 
 |-  ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) C_ ( R u. ( dom R X. ran R ) )
7 6 a1i 
 |-  ( ph -> ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) C_ ( R u. ( dom R X. ran R ) ) )
8 1 1 coeq12d 
 |-  ( ph -> ( S o. S ) = ( ( R u. ( dom R X. ran R ) ) o. ( R u. ( dom R X. ran R ) ) ) )
9 coundir 
 |-  ( ( R u. ( dom R X. ran R ) ) o. ( R u. ( dom R X. ran R ) ) ) = ( ( R o. ( R u. ( dom R X. ran R ) ) ) u. ( ( dom R X. ran R ) o. ( R u. ( dom R X. ran R ) ) ) )
10 relcnv 
 |-  Rel `' `' R
11 cocnvcnv1 
 |-  ( `' `' R o. ( R u. ( dom R X. ran R ) ) ) = ( R o. ( R u. ( dom R X. ran R ) ) )
12 relssdmrn 
 |-  ( Rel `' `' R -> `' `' R C_ ( dom `' `' R X. ran `' `' R ) )
13 dmcnvcnv 
 |-  dom `' `' R = dom R
14 rncnvcnv 
 |-  ran `' `' R = ran R
15 13 14 xpeq12i 
 |-  ( dom `' `' R X. ran `' `' R ) = ( dom R X. ran R )
16 12 15 sseqtrdi 
 |-  ( Rel `' `' R -> `' `' R C_ ( dom R X. ran R ) )
17 coss1 
 |-  ( `' `' R C_ ( dom R X. ran R ) -> ( `' `' R o. ( R u. ( dom R X. ran R ) ) ) C_ ( ( dom R X. ran R ) o. ( R u. ( dom R X. ran R ) ) ) )
18 16 17 syl 
 |-  ( Rel `' `' R -> ( `' `' R o. ( R u. ( dom R X. ran R ) ) ) C_ ( ( dom R X. ran R ) o. ( R u. ( dom R X. ran R ) ) ) )
19 11 18 eqsstrrid 
 |-  ( Rel `' `' R -> ( R o. ( R u. ( dom R X. ran R ) ) ) C_ ( ( dom R X. ran R ) o. ( R u. ( dom R X. ran R ) ) ) )
20 ssequn1 
 |-  ( ( R o. ( R u. ( dom R X. ran R ) ) ) C_ ( ( dom R X. ran R ) o. ( R u. ( dom R X. ran R ) ) ) <-> ( ( R o. ( R u. ( dom R X. ran R ) ) ) u. ( ( dom R X. ran R ) o. ( R u. ( dom R X. ran R ) ) ) ) = ( ( dom R X. ran R ) o. ( R u. ( dom R X. ran R ) ) ) )
21 19 20 sylib 
 |-  ( Rel `' `' R -> ( ( R o. ( R u. ( dom R X. ran R ) ) ) u. ( ( dom R X. ran R ) o. ( R u. ( dom R X. ran R ) ) ) ) = ( ( dom R X. ran R ) o. ( R u. ( dom R X. ran R ) ) ) )
22 10 21 ax-mp 
 |-  ( ( R o. ( R u. ( dom R X. ran R ) ) ) u. ( ( dom R X. ran R ) o. ( R u. ( dom R X. ran R ) ) ) ) = ( ( dom R X. ran R ) o. ( R u. ( dom R X. ran R ) ) )
23 9 22 eqtri 
 |-  ( ( R u. ( dom R X. ran R ) ) o. ( R u. ( dom R X. ran R ) ) ) = ( ( dom R X. ran R ) o. ( R u. ( dom R X. ran R ) ) )
24 coundi 
 |-  ( ( dom R X. ran R ) o. ( R u. ( dom R X. ran R ) ) ) = ( ( ( dom R X. ran R ) o. R ) u. ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) )
25 cocnvcnv2 
 |-  ( ( dom R X. ran R ) o. `' `' R ) = ( ( dom R X. ran R ) o. R )
26 coss2 
 |-  ( `' `' R C_ ( dom R X. ran R ) -> ( ( dom R X. ran R ) o. `' `' R ) C_ ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) )
27 16 26 syl 
 |-  ( Rel `' `' R -> ( ( dom R X. ran R ) o. `' `' R ) C_ ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) )
28 25 27 eqsstrrid 
 |-  ( Rel `' `' R -> ( ( dom R X. ran R ) o. R ) C_ ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) )
29 ssequn1 
 |-  ( ( ( dom R X. ran R ) o. R ) C_ ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) <-> ( ( ( dom R X. ran R ) o. R ) u. ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) ) = ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) )
30 28 29 sylib 
 |-  ( Rel `' `' R -> ( ( ( dom R X. ran R ) o. R ) u. ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) ) = ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) )
31 10 30 ax-mp 
 |-  ( ( ( dom R X. ran R ) o. R ) u. ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) ) = ( ( dom R X. ran R ) o. ( dom R X. ran R ) )
32 24 31 eqtri 
 |-  ( ( dom R X. ran R ) o. ( R u. ( dom R X. ran R ) ) ) = ( ( dom R X. ran R ) o. ( dom R X. ran R ) )
33 23 32 eqtri 
 |-  ( ( R u. ( dom R X. ran R ) ) o. ( R u. ( dom R X. ran R ) ) ) = ( ( dom R X. ran R ) o. ( dom R X. ran R ) )
34 8 33 eqtrdi 
 |-  ( ph -> ( S o. S ) = ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) )
35 7 34 1 3sstr4d 
 |-  ( ph -> ( S o. S ) C_ S )
36 3 35 jca 
 |-  ( ph -> ( R C_ S /\ ( S o. S ) C_ S ) )