Metamath Proof Explorer

Theorem trclubgNEW

Description: If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020)

Ref Expression
Hypothesis trclubgNEW.rex 
|- ( ph -> R e. _V )
Assertion trclubgNEW 
|- ( ph -> |^| { x | ( R C_ x /\ ( x o. x ) C_ x ) } C_ ( R u. ( dom R X. ran R ) ) )

Proof

Step Hyp Ref Expression
1 trclubgNEW.rex 
 |-  ( ph -> R e. _V )
2 1 dmexd 
 |-  ( ph -> dom R e. _V )
3 rnexg 
 |-  ( R e. _V -> ran R e. _V )
4 1 3 syl 
 |-  ( ph -> ran R e. _V )
5 2 4 xpexd 
 |-  ( ph -> ( dom R X. ran R ) e. _V )
6 1 5 unexd 
 |-  ( ph -> ( R u. ( dom R X. ran R ) ) e. _V )
7 id 
 |-  ( x = ( R u. ( dom R X. ran R ) ) -> x = ( R u. ( dom R X. ran R ) ) )
8 7 7 coeq12d 
 |-  ( x = ( R u. ( dom R X. ran R ) ) -> ( x o. x ) = ( ( R u. ( dom R X. ran R ) ) o. ( R u. ( dom R X. ran R ) ) ) )
9 8 7 sseq12d 
 |-  ( x = ( R u. ( dom R X. ran R ) ) -> ( ( x o. x ) C_ x <-> ( ( R u. ( dom R X. ran R ) ) o. ( R u. ( dom R X. ran R ) ) ) C_ ( R u. ( dom R X. ran R ) ) ) )
10 ssun1 
 |-  R C_ ( R u. ( dom R X. ran R ) )
11 10 a1i 
 |-  ( ph -> R C_ ( R u. ( dom R X. ran R ) ) )
12 cnvssrndm 
 |-  `' R C_ ( ran R X. dom R )
13 coundi 
 |-  ( ( R u. ( dom R X. ran R ) ) o. ( R u. ( dom R X. ran R ) ) ) = ( ( ( R u. ( dom R X. ran R ) ) o. R ) u. ( ( R u. ( dom R X. ran R ) ) o. ( dom R X. ran R ) ) )
14 cnvss 
 |-  ( `' R C_ ( ran R X. dom R ) -> `' `' R C_ `' ( ran R X. dom R ) )
15 coss2 
 |-  ( `' `' R C_ `' ( ran R X. dom R ) -> ( ( R u. ( dom R X. ran R ) ) o. `' `' R ) C_ ( ( R u. ( dom R X. ran R ) ) o. `' ( ran R X. dom R ) ) )
16 14 15 syl 
 |-  ( `' R C_ ( ran R X. dom R ) -> ( ( R u. ( dom R X. ran R ) ) o. `' `' R ) C_ ( ( R u. ( dom R X. ran R ) ) o. `' ( ran R X. dom R ) ) )
17 cocnvcnv2 
 |-  ( ( R u. ( dom R X. ran R ) ) o. `' `' R ) = ( ( R u. ( dom R X. ran R ) ) o. R )
18 cnvxp 
 |-  `' ( ran R X. dom R ) = ( dom R X. ran R )
19 18 coeq2i 
 |-  ( ( R u. ( dom R X. ran R ) ) o. `' ( ran R X. dom R ) ) = ( ( R u. ( dom R X. ran R ) ) o. ( dom R X. ran R ) )
20 16 17 19 3sstr3g 
 |-  ( `' R C_ ( ran R X. dom R ) -> ( ( R u. ( dom R X. ran R ) ) o. R ) C_ ( ( R u. ( dom R X. ran R ) ) o. ( dom R X. ran R ) ) )
21 ssequn1 
 |-  ( ( ( R u. ( dom R X. ran R ) ) o. R ) C_ ( ( R u. ( dom R X. ran R ) ) o. ( dom R X. ran R ) ) <-> ( ( ( R u. ( dom R X. ran R ) ) o. R ) u. ( ( R u. ( dom R X. ran R ) ) o. ( dom R X. ran R ) ) ) = ( ( R u. ( dom R X. ran R ) ) o. ( dom R X. ran R ) ) )
22 20 21 sylib 
 |-  ( `' R C_ ( ran R X. dom R ) -> ( ( ( R u. ( dom R X. ran R ) ) o. R ) u. ( ( R u. ( dom R X. ran R ) ) o. ( dom R X. ran R ) ) ) = ( ( R u. ( dom R X. ran R ) ) o. ( dom R X. ran R ) ) )
23 coundir 
 |-  ( ( R u. ( dom R X. ran R ) ) o. ( dom R X. ran R ) ) = ( ( R o. ( dom R X. ran R ) ) u. ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) )
24 coss1 
 |-  ( `' `' R C_ `' ( ran R X. dom R ) -> ( `' `' R o. ( dom R X. ran R ) ) C_ ( `' ( ran R X. dom R ) o. ( dom R X. ran R ) ) )
25 14 24 syl 
 |-  ( `' R C_ ( ran R X. dom R ) -> ( `' `' R o. ( dom R X. ran R ) ) C_ ( `' ( ran R X. dom R ) o. ( dom R X. ran R ) ) )
26 cocnvcnv1 
 |-  ( `' `' R o. ( dom R X. ran R ) ) = ( R o. ( dom R X. ran R ) )
27 18 coeq1i 
 |-  ( `' ( ran R X. dom R ) o. ( dom R X. ran R ) ) = ( ( dom R X. ran R ) o. ( dom R X. ran R ) )
28 25 26 27 3sstr3g 
 |-  ( `' R C_ ( ran R X. dom R ) -> ( R o. ( dom R X. ran R ) ) C_ ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) )
29 ssequn1 
 |-  ( ( R o. ( dom R X. ran R ) ) C_ ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) <-> ( ( R o. ( dom R X. ran 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 
 |-  ( `' R C_ ( ran R X. dom R ) -> ( ( R o. ( dom R X. ran 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 xptrrel 
 |-  ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) C_ ( dom R X. ran R )
32 ssun2 
 |-  ( dom R X. ran R ) C_ ( R u. ( dom R X. ran R ) )
33 31 32 sstri 
 |-  ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) C_ ( R u. ( dom R X. ran R ) )
34 33 a1i 
 |-  ( `' R C_ ( ran R X. dom R ) -> ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) C_ ( R u. ( dom R X. ran R ) ) )
35 30 34 eqsstrd 
 |-  ( `' R C_ ( ran R X. dom R ) -> ( ( R o. ( dom R X. ran R ) ) u. ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) ) C_ ( R u. ( dom R X. ran R ) ) )
36 23 35 eqsstrid 
 |-  ( `' R C_ ( ran R X. dom R ) -> ( ( R u. ( dom R X. ran R ) ) o. ( dom R X. ran R ) ) C_ ( R u. ( dom R X. ran R ) ) )
37 22 36 eqsstrd 
 |-  ( `' R C_ ( ran R X. dom R ) -> ( ( ( R u. ( dom R X. ran R ) ) o. R ) u. ( ( R u. ( dom R X. ran R ) ) o. ( dom R X. ran R ) ) ) C_ ( R u. ( dom R X. ran R ) ) )
38 13 37 eqsstrid 
 |-  ( `' R C_ ( ran R X. dom R ) -> ( ( R u. ( dom R X. ran R ) ) o. ( R u. ( dom R X. ran R ) ) ) C_ ( R u. ( dom R X. ran R ) ) )
39 12 38 mp1i 
 |-  ( ph -> ( ( R u. ( dom R X. ran R ) ) o. ( R u. ( dom R X. ran R ) ) ) C_ ( R u. ( dom R X. ran R ) ) )
40 6 9 11 39 clublem 
 |-  ( ph -> |^| { x | ( R C_ x /\ ( x o. x ) C_ x ) } C_ ( R u. ( dom R X. ran R ) ) )