Metamath Proof Explorer

Theorem brcoffn

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

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

Proof

Step Hyp Ref Expression
1 brcoffn.c 
 |-  ( ph -> C Fn Y )
2 brcoffn.d 
 |-  ( ph -> D : X --> Y )
3 brcoffn.r 
 |-  ( ph -> A ( C o. D ) B )
4 fnfco 
 |-  ( ( C Fn Y /\ D : X --> Y ) -> ( C o. D ) Fn X )
5 1 2 4 syl2anc 
 |-  ( ph -> ( C o. D ) Fn X )
6 simpl 
 |-  ( ( ph /\ ( C o. D ) Fn X ) -> ph )
7 simpr 
 |-  ( ( ph /\ ( C o. D ) Fn X ) -> ( C o. D ) Fn X )
8 6 3 syl 
 |-  ( ( ph /\ ( C o. D ) Fn X ) -> A ( C o. D ) B )
9 fnbr 
 |-  ( ( ( C o. D ) Fn X /\ A ( C o. D ) B ) -> A e. X )
10 7 8 9 syl2anc 
 |-  ( ( ph /\ ( C o. D ) Fn X ) -> A e. X )
11 6 7 10 3jca 
 |-  ( ( ph /\ ( C o. D ) Fn X ) -> ( ph /\ ( C o. D ) Fn X /\ A e. X ) )
12 5 11 mpdan 
 |-  ( ph -> ( ph /\ ( C o. D ) Fn X /\ A e. X ) )
13 2 3ad2ant1 
 |-  ( ( ph /\ ( C o. D ) Fn X /\ A e. X ) -> D : X --> Y )
14 simp3 
 |-  ( ( ph /\ ( C o. D ) Fn X /\ A e. X ) -> A e. X )
15 fvco3 
 |-  ( ( D : X --> Y /\ A e. X ) -> ( ( C o. D ) ` A ) = ( C ` ( D ` A ) ) )
16 13 14 15 syl2anc 
 |-  ( ( ph /\ ( C o. D ) Fn X /\ A e. X ) -> ( ( C o. D ) ` A ) = ( C ` ( D ` A ) ) )
17 3 3ad2ant1 
 |-  ( ( ph /\ ( C o. D ) Fn X /\ A e. X ) -> A ( C o. D ) B )
18 fnbrfvb 
 |-  ( ( ( C o. D ) Fn X /\ A e. X ) -> ( ( ( C o. D ) ` A ) = B <-> A ( C o. D ) B ) )
19 18 3adant1 
 |-  ( ( ph /\ ( C o. D ) Fn X /\ A e. X ) -> ( ( ( C o. D ) ` A ) = B <-> A ( C o. D ) B ) )
20 17 19 mpbird 
 |-  ( ( ph /\ ( C o. D ) Fn X /\ A e. X ) -> ( ( C o. D ) ` A ) = B )
21 16 20 eqtr3d 
 |-  ( ( ph /\ ( C o. D ) Fn X /\ A e. X ) -> ( C ` ( D ` A ) ) = B )
22 eqid 
 |-  ( D ` A ) = ( D ` A )
23 21 22 jctil 
 |-  ( ( ph /\ ( C o. D ) Fn X /\ A e. X ) -> ( ( D ` A ) = ( D ` A ) /\ ( C ` ( D ` A ) ) = B ) )
24 13 ffnd 
 |-  ( ( ph /\ ( C o. D ) Fn X /\ A e. X ) -> D Fn X )
25 fnbrfvb 
 |-  ( ( D Fn X /\ A e. X ) -> ( ( D ` A ) = ( D ` A ) <-> A D ( D ` A ) ) )
26 24 14 25 syl2anc 
 |-  ( ( ph /\ ( C o. D ) Fn X /\ A e. X ) -> ( ( D ` A ) = ( D ` A ) <-> A D ( D ` A ) ) )
27 1 3ad2ant1 
 |-  ( ( ph /\ ( C o. D ) Fn X /\ A e. X ) -> C Fn Y )
28 13 14 ffvelrnd 
 |-  ( ( ph /\ ( C o. D ) Fn X /\ A e. X ) -> ( D ` A ) e. Y )
29 fnbrfvb 
 |-  ( ( C Fn Y /\ ( D ` A ) e. Y ) -> ( ( C ` ( D ` A ) ) = B <-> ( D ` A ) C B ) )
30 27 28 29 syl2anc 
 |-  ( ( ph /\ ( C o. D ) Fn X /\ A e. X ) -> ( ( C ` ( D ` A ) ) = B <-> ( D ` A ) C B ) )
31 26 30 anbi12d 
 |-  ( ( ph /\ ( C o. D ) Fn X /\ A e. X ) -> ( ( ( D ` A ) = ( D ` A ) /\ ( C ` ( D ` A ) ) = B ) <-> ( A D ( D ` A ) /\ ( D ` A ) C B ) ) )
32 23 31 mpbid 
 |-  ( ( ph /\ ( C o. D ) Fn X /\ A e. X ) -> ( A D ( D ` A ) /\ ( D ` A ) C B ) )
33 12 32 syl 
 |-  ( ph -> ( A D ( D ` A ) /\ ( D ` A ) C B ) )