Description: If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | trclubgNEW.rex | |
|
Assertion | trclubgNEW | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | trclubgNEW.rex | |
|
2 | 1 | dmexd | |
3 | rnexg | |
|
4 | 1 3 | syl | |
5 | 2 4 | xpexd | |
6 | unexg | |
|
7 | 1 5 6 | syl2anc | |
8 | id | |
|
9 | 8 8 | coeq12d | |
10 | 9 8 | sseq12d | |
11 | ssun1 | |
|
12 | 11 | a1i | |
13 | cnvssrndm | |
|
14 | coundi | |
|
15 | cnvss | |
|
16 | coss2 | |
|
17 | 15 16 | syl | |
18 | cocnvcnv2 | |
|
19 | cnvxp | |
|
20 | 19 | coeq2i | |
21 | 17 18 20 | 3sstr3g | |
22 | ssequn1 | |
|
23 | 21 22 | sylib | |
24 | coundir | |
|
25 | coss1 | |
|
26 | 15 25 | syl | |
27 | cocnvcnv1 | |
|
28 | 19 | coeq1i | |
29 | 26 27 28 | 3sstr3g | |
30 | ssequn1 | |
|
31 | 29 30 | sylib | |
32 | xptrrel | |
|
33 | ssun2 | |
|
34 | 32 33 | sstri | |
35 | 34 | a1i | |
36 | 31 35 | eqsstrd | |
37 | 24 36 | eqsstrid | |
38 | 23 37 | eqsstrd | |
39 | 14 38 | eqsstrid | |
40 | 13 39 | mp1i | |
41 | 7 10 12 40 | clublem | |