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 φRV
Assertion trclubgNEW φx|RxxxxRdomR×ranR

Proof

Step Hyp Ref Expression
1 trclubgNEW.rex φRV
2 1 dmexd φdomRV
3 rnexg RVranRV
4 1 3 syl φranRV
5 2 4 xpexd φdomR×ranRV
6 unexg RVdomR×ranRVRdomR×ranRV
7 1 5 6 syl2anc φRdomR×ranRV
8 id x=RdomR×ranRx=RdomR×ranR
9 8 8 coeq12d x=RdomR×ranRxx=RdomR×ranRRdomR×ranR
10 9 8 sseq12d x=RdomR×ranRxxxRdomR×ranRRdomR×ranRRdomR×ranR
11 ssun1 RRdomR×ranR
12 11 a1i φRRdomR×ranR
13 cnvssrndm R-1ranR×domR
14 coundi RdomR×ranRRdomR×ranR=RdomR×ranRRRdomR×ranRdomR×ranR
15 cnvss R-1ranR×domRR-1-1ranR×domR-1
16 coss2 R-1-1ranR×domR-1RdomR×ranRR-1-1RdomR×ranRranR×domR-1
17 15 16 syl R-1ranR×domRRdomR×ranRR-1-1RdomR×ranRranR×domR-1
18 cocnvcnv2 RdomR×ranRR-1-1=RdomR×ranRR
19 cnvxp ranR×domR-1=domR×ranR
20 19 coeq2i RdomR×ranRranR×domR-1=RdomR×ranRdomR×ranR
21 17 18 20 3sstr3g R-1ranR×domRRdomR×ranRRRdomR×ranRdomR×ranR
22 ssequn1 RdomR×ranRRRdomR×ranRdomR×ranRRdomR×ranRRRdomR×ranRdomR×ranR=RdomR×ranRdomR×ranR
23 21 22 sylib R-1ranR×domRRdomR×ranRRRdomR×ranRdomR×ranR=RdomR×ranRdomR×ranR
24 coundir RdomR×ranRdomR×ranR=RdomR×ranRdomR×ranRdomR×ranR
25 coss1 R-1-1ranR×domR-1R-1-1domR×ranRranR×domR-1domR×ranR
26 15 25 syl R-1ranR×domRR-1-1domR×ranRranR×domR-1domR×ranR
27 cocnvcnv1 R-1-1domR×ranR=RdomR×ranR
28 19 coeq1i ranR×domR-1domR×ranR=domR×ranRdomR×ranR
29 26 27 28 3sstr3g R-1ranR×domRRdomR×ranRdomR×ranRdomR×ranR
30 ssequn1 RdomR×ranRdomR×ranRdomR×ranRRdomR×ranRdomR×ranRdomR×ranR=domR×ranRdomR×ranR
31 29 30 sylib R-1ranR×domRRdomR×ranRdomR×ranRdomR×ranR=domR×ranRdomR×ranR
32 xptrrel domR×ranRdomR×ranRdomR×ranR
33 ssun2 domR×ranRRdomR×ranR
34 32 33 sstri domR×ranRdomR×ranRRdomR×ranR
35 34 a1i R-1ranR×domRdomR×ranRdomR×ranRRdomR×ranR
36 31 35 eqsstrd R-1ranR×domRRdomR×ranRdomR×ranRdomR×ranRRdomR×ranR
37 24 36 eqsstrid R-1ranR×domRRdomR×ranRdomR×ranRRdomR×ranR
38 23 37 eqsstrd R-1ranR×domRRdomR×ranRRRdomR×ranRdomR×ranRRdomR×ranR
39 14 38 eqsstrid R-1ranR×domRRdomR×ranRRdomR×ranRRdomR×ranR
40 13 39 mp1i φRdomR×ranRRdomR×ranRRdomR×ranR
41 7 10 12 40 clublem φx|RxxxxRdomR×ranR