Metamath Proof Explorer

Theorem brcofffn

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

Ref Expression
Hypotheses brcofffn.c 
|- ( ph -> C Fn Z )
brcofffn.d 
|- ( ph -> D : Y --> Z )
brcofffn.e 
|- ( ph -> E : X --> Y )
brcofffn.r 
|- ( ph -> A ( C o. ( D o. E ) ) B )
Assertion brcofffn 
|- ( ph -> ( A E ( E ` A ) /\ ( E ` A ) D ( D ` ( E ` A ) ) /\ ( D ` ( E ` A ) ) C B ) )

Proof

Step Hyp Ref Expression
1 brcofffn.c 
 |-  ( ph -> C Fn Z )
2 brcofffn.d 
 |-  ( ph -> D : Y --> Z )
3 brcofffn.e 
 |-  ( ph -> E : X --> Y )
4 brcofffn.r 
 |-  ( ph -> A ( C o. ( D o. E ) ) B )
5 fnfco 
 |-  ( ( C Fn Z /\ D : Y --> Z ) -> ( C o. D ) Fn Y )
6 1 2 5 syl2anc 
 |-  ( ph -> ( C o. D ) Fn Y )
7 coass 
 |-  ( ( C o. D ) o. E ) = ( C o. ( D o. E ) )
8 7 breqi 
 |-  ( A ( ( C o. D ) o. E ) B <-> A ( C o. ( D o. E ) ) B )
9 4 8 sylibr 
 |-  ( ph -> A ( ( C o. D ) o. E ) B )
10 6 3 9 brcoffn 
 |-  ( ph -> ( A E ( E ` A ) /\ ( E ` A ) ( C o. D ) B ) )
11 1 adantr 
 |-  ( ( ph /\ ( A E ( E ` A ) /\ ( E ` A ) ( C o. D ) B ) ) -> C Fn Z )
12 2 adantr 
 |-  ( ( ph /\ ( A E ( E ` A ) /\ ( E ` A ) ( C o. D ) B ) ) -> D : Y --> Z )
13 simprr 
 |-  ( ( ph /\ ( A E ( E ` A ) /\ ( E ` A ) ( C o. D ) B ) ) -> ( E ` A ) ( C o. D ) B )
14 11 12 13 brcoffn 
 |-  ( ( ph /\ ( A E ( E ` A ) /\ ( E ` A ) ( C o. D ) B ) ) -> ( ( E ` A ) D ( D ` ( E ` A ) ) /\ ( D ` ( E ` A ) ) C B ) )
15 14 ex 
 |-  ( ph -> ( ( A E ( E ` A ) /\ ( E ` A ) ( C o. D ) B ) -> ( ( E ` A ) D ( D ` ( E ` A ) ) /\ ( D ` ( E ` A ) ) C B ) ) )
16 10 15 jcai 
 |-  ( ph -> ( ( A E ( E ` A ) /\ ( E ` A ) ( C o. D ) B ) /\ ( ( E ` A ) D ( D ` ( E ` A ) ) /\ ( D ` ( E ` A ) ) C B ) ) )
17 simpll 
 |-  ( ( ( A E ( E ` A ) /\ ( E ` A ) ( C o. D ) B ) /\ ( ( E ` A ) D ( D ` ( E ` A ) ) /\ ( D ` ( E ` A ) ) C B ) ) -> A E ( E ` A ) )
18 simprl 
 |-  ( ( ( A E ( E ` A ) /\ ( E ` A ) ( C o. D ) B ) /\ ( ( E ` A ) D ( D ` ( E ` A ) ) /\ ( D ` ( E ` A ) ) C B ) ) -> ( E ` A ) D ( D ` ( E ` A ) ) )
19 simprr 
 |-  ( ( ( A E ( E ` A ) /\ ( E ` A ) ( C o. D ) B ) /\ ( ( E ` A ) D ( D ` ( E ` A ) ) /\ ( D ` ( E ` A ) ) C B ) ) -> ( D ` ( E ` A ) ) C B )
20 17 18 19 3jca 
 |-  ( ( ( A E ( E ` A ) /\ ( E ` A ) ( C o. D ) B ) /\ ( ( E ` A ) D ( D ` ( E ` A ) ) /\ ( D ` ( E ` A ) ) C B ) ) -> ( A E ( E ` A ) /\ ( E ` A ) D ( D ` ( E ` A ) ) /\ ( D ` ( E ` A ) ) C B ) )
21 16 20 syl 
 |-  ( ph -> ( A E ( E ` A ) /\ ( E ` A ) D ( D ` ( E ` A ) ) /\ ( D ` ( E ` A ) ) C B ) )