Metamath Proof Explorer


Theorem brco3f1o

Description: Conditions allowing the decomposition of a binary relation. (Contributed by RP, 8-Jun-2021)

Ref Expression
Hypotheses brco3f1o.c φC:Y1-1 ontoZ
brco3f1o.d φD:X1-1 ontoY
brco3f1o.e φE:W1-1 ontoX
brco3f1o.r φACDEB
Assertion brco3f1o φC-1BCBD-1C-1BDC-1BAED-1C-1B

Proof

Step Hyp Ref Expression
1 brco3f1o.c φC:Y1-1 ontoZ
2 brco3f1o.d φD:X1-1 ontoY
3 brco3f1o.e φE:W1-1 ontoX
4 brco3f1o.r φACDEB
5 f1ocnv E:W1-1 ontoXE-1:X1-1 ontoW
6 f1ofn E-1:X1-1 ontoWE-1FnX
7 3 5 6 3syl φE-1FnX
8 f1ocnv D:X1-1 ontoYD-1:Y1-1 ontoX
9 f1of D-1:Y1-1 ontoXD-1:YX
10 2 8 9 3syl φD-1:YX
11 f1ocnv C:Y1-1 ontoZC-1:Z1-1 ontoY
12 f1of C-1:Z1-1 ontoYC-1:ZY
13 1 11 12 3syl φC-1:ZY
14 relco RelCDE
15 14 relbrcnv BCDE-1AACDEB
16 cnvco CDE-1=E-1CD-1
17 cnvco CD-1=D-1C-1
18 17 coeq2i E-1CD-1=E-1D-1C-1
19 16 18 eqtri CDE-1=E-1D-1C-1
20 19 breqi BCDE-1ABE-1D-1C-1A
21 coass CDE=CDE
22 21 breqi ACDEBACDEB
23 15 20 22 3bitr3ri ACDEBBE-1D-1C-1A
24 4 23 sylib φBE-1D-1C-1A
25 7 10 13 24 brcofffn φBC-1C-1BC-1BD-1D-1C-1BD-1C-1BE-1A
26 f1orel C:Y1-1 ontoZRelC
27 relbrcnvg RelCBC-1C-1BC-1BCB
28 1 26 27 3syl φBC-1C-1BC-1BCB
29 f1orel D:X1-1 ontoYRelD
30 relbrcnvg RelDC-1BD-1D-1C-1BD-1C-1BDC-1B
31 2 29 30 3syl φC-1BD-1D-1C-1BD-1C-1BDC-1B
32 f1orel E:W1-1 ontoXRelE
33 relbrcnvg RelED-1C-1BE-1AAED-1C-1B
34 3 32 33 3syl φD-1C-1BE-1AAED-1C-1B
35 28 31 34 3anbi123d φBC-1C-1BC-1BD-1D-1C-1BD-1C-1BE-1AC-1BCBD-1C-1BDC-1BAED-1C-1B
36 25 35 mpbid φC-1BCBD-1C-1BDC-1BAED-1C-1B