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 
|- ( ph -> C : Y -1-1-onto-> Z )
brco3f1o.d 
|- ( ph -> D : X -1-1-onto-> Y )
brco3f1o.e 
|- ( ph -> E : W -1-1-onto-> X )
brco3f1o.r 
|- ( ph -> A ( C o. ( D o. E ) ) B )
Assertion brco3f1o 
|- ( ph -> ( ( `' C ` B ) C B /\ ( `' D ` ( `' C ` B ) ) D ( `' C ` B ) /\ A E ( `' D ` ( `' C ` B ) ) ) )

Proof

Step Hyp Ref Expression
1 brco3f1o.c 
 |-  ( ph -> C : Y -1-1-onto-> Z )
2 brco3f1o.d 
 |-  ( ph -> D : X -1-1-onto-> Y )
3 brco3f1o.e 
 |-  ( ph -> E : W -1-1-onto-> X )
4 brco3f1o.r 
 |-  ( ph -> A ( C o. ( D o. E ) ) B )
5 f1ocnv 
 |-  ( E : W -1-1-onto-> X -> `' E : X -1-1-onto-> W )
6 f1ofn 
 |-  ( `' E : X -1-1-onto-> W -> `' E Fn X )
7 3 5 6 3syl 
 |-  ( ph -> `' E Fn X )
8 f1ocnv 
 |-  ( D : X -1-1-onto-> Y -> `' D : Y -1-1-onto-> X )
9 f1of 
 |-  ( `' D : Y -1-1-onto-> X -> `' D : Y --> X )
10 2 8 9 3syl 
 |-  ( ph -> `' D : Y --> X )
11 f1ocnv 
 |-  ( C : Y -1-1-onto-> Z -> `' C : Z -1-1-onto-> Y )
12 f1of 
 |-  ( `' C : Z -1-1-onto-> Y -> `' C : Z --> Y )
13 1 11 12 3syl 
 |-  ( ph -> `' C : Z --> Y )
14 relco 
 |-  Rel ( ( C o. D ) o. E )
15 14 relbrcnv 
 |-  ( B `' ( ( C o. D ) o. E ) A <-> A ( ( C o. D ) o. E ) B )
16 cnvco 
 |-  `' ( ( C o. D ) o. E ) = ( `' E o. `' ( C o. D ) )
17 cnvco 
 |-  `' ( C o. D ) = ( `' D o. `' C )
18 17 coeq2i 
 |-  ( `' E o. `' ( C o. D ) ) = ( `' E o. ( `' D o. `' C ) )
19 16 18 eqtri 
 |-  `' ( ( C o. D ) o. E ) = ( `' E o. ( `' D o. `' C ) )
20 19 breqi 
 |-  ( B `' ( ( C o. D ) o. E ) A <-> B ( `' E o. ( `' D o. `' C ) ) A )
21 coass 
 |-  ( ( C o. D ) o. E ) = ( C o. ( D o. E ) )
22 21 breqi 
 |-  ( A ( ( C o. D ) o. E ) B <-> A ( C o. ( D o. E ) ) B )
23 15 20 22 3bitr3ri 
 |-  ( A ( C o. ( D o. E ) ) B <-> B ( `' E o. ( `' D o. `' C ) ) A )
24 4 23 sylib 
 |-  ( ph -> B ( `' E o. ( `' D o. `' C ) ) A )
25 7 10 13 24 brcofffn 
 |-  ( ph -> ( B `' C ( `' C ` B ) /\ ( `' C ` B ) `' D ( `' D ` ( `' C ` B ) ) /\ ( `' D ` ( `' C ` B ) ) `' E A ) )
26 f1orel 
 |-  ( C : Y -1-1-onto-> Z -> Rel C )
27 relbrcnvg 
 |-  ( Rel C -> ( B `' C ( `' C ` B ) <-> ( `' C ` B ) C B ) )
28 1 26 27 3syl 
 |-  ( ph -> ( B `' C ( `' C ` B ) <-> ( `' C ` B ) C B ) )
29 f1orel 
 |-  ( D : X -1-1-onto-> Y -> Rel D )
30 relbrcnvg 
 |-  ( Rel D -> ( ( `' C ` B ) `' D ( `' D ` ( `' C ` B ) ) <-> ( `' D ` ( `' C ` B ) ) D ( `' C ` B ) ) )
31 2 29 30 3syl 
 |-  ( ph -> ( ( `' C ` B ) `' D ( `' D ` ( `' C ` B ) ) <-> ( `' D ` ( `' C ` B ) ) D ( `' C ` B ) ) )
32 f1orel 
 |-  ( E : W -1-1-onto-> X -> Rel E )
33 relbrcnvg 
 |-  ( Rel E -> ( ( `' D ` ( `' C ` B ) ) `' E A <-> A E ( `' D ` ( `' C ` B ) ) ) )
34 3 32 33 3syl 
 |-  ( ph -> ( ( `' D ` ( `' C ` B ) ) `' E A <-> A E ( `' D ` ( `' C ` B ) ) ) )
35 28 31 34 3anbi123d 
 |-  ( ph -> ( ( B `' C ( `' C ` B ) /\ ( `' C ` B ) `' D ( `' D ` ( `' C ` B ) ) /\ ( `' D ` ( `' C ` B ) ) `' E A ) <-> ( ( `' C ` B ) C B /\ ( `' D ` ( `' C ` B ) ) D ( `' C ` B ) /\ A E ( `' D ` ( `' C ` B ) ) ) ) )
36 25 35 mpbid 
 |-  ( ph -> ( ( `' C ` B ) C B /\ ( `' D ` ( `' C ` B ) ) D ( `' C ` B ) /\ A E ( `' D ` ( `' C ` B ) ) ) )