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 unexg 
 |-  ( ( R e. _V /\ ( dom R X. ran R ) e. _V ) -> ( R u. ( dom R X. ran R ) ) e. _V )
7 1 5 6 syl2anc 
 |-  ( ph -> ( R u. ( dom R X. ran R ) ) e. _V )
8 id 
 |-  ( x = ( R u. ( dom R X. ran R ) ) -> x = ( R u. ( dom R X. ran R ) ) )
9 8 8 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 ) ) ) )
10 9 8 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 ) ) ) )
11 ssun1 
 |-  R C_ ( R u. ( dom R X. ran R ) )
12 11 a1i 
 |-  ( ph -> R C_ ( R u. ( dom R X. ran R ) ) )
13 cnvssrndm 
 |-  `' R C_ ( ran R X. dom R )
14 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 ) ) )
15 cnvss 
 |-  ( `' R C_ ( ran R X. dom R ) -> `' `' R C_ `' ( ran R X. dom R ) )
16 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 ) ) )
17 15 16 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 ) ) )
18 cocnvcnv2 
 |-  ( ( R u. ( dom R X. ran R ) ) o. `' `' R ) = ( ( R u. ( dom R X. ran R ) ) o. R )
19 cnvxp 
 |-  `' ( ran R X. dom R ) = ( dom R X. ran R )
20 19 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 ) )
21 17 18 20 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 ) ) )
22 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 ) ) )
23 21 22 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 ) ) )
24 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 ) ) )
25 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 ) ) )
26 15 25 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 ) ) )
27 cocnvcnv1 
 |-  ( `' `' R o. ( dom R X. ran R ) ) = ( R o. ( dom R X. ran R ) )
28 19 coeq1i 
 |-  ( `' ( ran R X. dom R ) o. ( dom R X. ran R ) ) = ( ( dom R X. ran R ) o. ( dom R X. ran R ) )
29 26 27 28 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 ) ) )
30 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 ) ) )
31 29 30 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 ) ) )
32 xptrrel 
 |-  ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) C_ ( dom R X. ran R )
33 ssun2 
 |-  ( dom R X. ran R ) C_ ( R u. ( dom R X. ran R ) )
34 32 33 sstri 
 |-  ( ( dom R X. ran R ) o. ( dom R X. ran R ) ) C_ ( R u. ( dom R X. ran R ) )
35 34 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 ) ) )
36 31 35 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 ) ) )
37 24 36 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 ) ) )
38 23 37 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 ) ) )
39 14 38 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 ) ) )
40 13 39 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 ) ) )
41 7 10 12 40 clublem 
 |-  ( ph -> |^| { x | ( R C_ x /\ ( x o. x ) C_ x ) } C_ ( R u. ( dom R X. ran R ) ) )