Description: Conditions allowing the decomposition of a binary relation. (Contributed by RP, 8-Jun-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | brco3f1o.c | |
|
brco3f1o.d | |
||
brco3f1o.e | |
||
brco3f1o.r | |
||
Assertion | brco3f1o | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | brco3f1o.c | |
|
2 | brco3f1o.d | |
|
3 | brco3f1o.e | |
|
4 | brco3f1o.r | |
|
5 | f1ocnv | |
|
6 | f1ofn | |
|
7 | 3 5 6 | 3syl | |
8 | f1ocnv | |
|
9 | f1of | |
|
10 | 2 8 9 | 3syl | |
11 | f1ocnv | |
|
12 | f1of | |
|
13 | 1 11 12 | 3syl | |
14 | relco | |
|
15 | 14 | relbrcnv | |
16 | cnvco | |
|
17 | cnvco | |
|
18 | 17 | coeq2i | |
19 | 16 18 | eqtri | |
20 | 19 | breqi | |
21 | coass | |
|
22 | 21 | breqi | |
23 | 15 20 22 | 3bitr3ri | |
24 | 4 23 | sylib | |
25 | 7 10 13 24 | brcofffn | |
26 | f1orel | |
|
27 | relbrcnvg | |
|
28 | 1 26 27 | 3syl | |
29 | f1orel | |
|
30 | relbrcnvg | |
|
31 | 2 29 30 | 3syl | |
32 | f1orel | |
|
33 | relbrcnvg | |
|
34 | 3 32 33 | 3syl | |
35 | 28 31 34 | 3anbi123d | |
36 | 25 35 | mpbid | |