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 ( 𝜑𝐶 Fn 𝑌 )
brcoffn.d ( 𝜑𝐷 : 𝑋𝑌 )
brcoffn.r ( 𝜑𝐴 ( 𝐶𝐷 ) 𝐵 )
Assertion brcoffn ( 𝜑 → ( 𝐴 𝐷 ( 𝐷𝐴 ) ∧ ( 𝐷𝐴 ) 𝐶 𝐵 ) )

Proof

Step Hyp Ref Expression
1 brcoffn.c ( 𝜑𝐶 Fn 𝑌 )
2 brcoffn.d ( 𝜑𝐷 : 𝑋𝑌 )
3 brcoffn.r ( 𝜑𝐴 ( 𝐶𝐷 ) 𝐵 )
4 fnfco ( ( 𝐶 Fn 𝑌𝐷 : 𝑋𝑌 ) → ( 𝐶𝐷 ) Fn 𝑋 )
5 1 2 4 syl2anc ( 𝜑 → ( 𝐶𝐷 ) Fn 𝑋 )
6 simpl ( ( 𝜑 ∧ ( 𝐶𝐷 ) Fn 𝑋 ) → 𝜑 )
7 simpr ( ( 𝜑 ∧ ( 𝐶𝐷 ) Fn 𝑋 ) → ( 𝐶𝐷 ) Fn 𝑋 )
8 6 3 syl ( ( 𝜑 ∧ ( 𝐶𝐷 ) Fn 𝑋 ) → 𝐴 ( 𝐶𝐷 ) 𝐵 )
9 fnbr ( ( ( 𝐶𝐷 ) Fn 𝑋𝐴 ( 𝐶𝐷 ) 𝐵 ) → 𝐴𝑋 )
10 7 8 9 syl2anc ( ( 𝜑 ∧ ( 𝐶𝐷 ) Fn 𝑋 ) → 𝐴𝑋 )
11 6 7 10 3jca ( ( 𝜑 ∧ ( 𝐶𝐷 ) Fn 𝑋 ) → ( 𝜑 ∧ ( 𝐶𝐷 ) Fn 𝑋𝐴𝑋 ) )
12 5 11 mpdan ( 𝜑 → ( 𝜑 ∧ ( 𝐶𝐷 ) Fn 𝑋𝐴𝑋 ) )
13 2 3ad2ant1 ( ( 𝜑 ∧ ( 𝐶𝐷 ) Fn 𝑋𝐴𝑋 ) → 𝐷 : 𝑋𝑌 )
14 simp3 ( ( 𝜑 ∧ ( 𝐶𝐷 ) Fn 𝑋𝐴𝑋 ) → 𝐴𝑋 )
15 fvco3 ( ( 𝐷 : 𝑋𝑌𝐴𝑋 ) → ( ( 𝐶𝐷 ) ‘ 𝐴 ) = ( 𝐶 ‘ ( 𝐷𝐴 ) ) )
16 13 14 15 syl2anc ( ( 𝜑 ∧ ( 𝐶𝐷 ) Fn 𝑋𝐴𝑋 ) → ( ( 𝐶𝐷 ) ‘ 𝐴 ) = ( 𝐶 ‘ ( 𝐷𝐴 ) ) )
17 3 3ad2ant1 ( ( 𝜑 ∧ ( 𝐶𝐷 ) Fn 𝑋𝐴𝑋 ) → 𝐴 ( 𝐶𝐷 ) 𝐵 )
18 fnbrfvb ( ( ( 𝐶𝐷 ) Fn 𝑋𝐴𝑋 ) → ( ( ( 𝐶𝐷 ) ‘ 𝐴 ) = 𝐵𝐴 ( 𝐶𝐷 ) 𝐵 ) )
19 18 3adant1 ( ( 𝜑 ∧ ( 𝐶𝐷 ) Fn 𝑋𝐴𝑋 ) → ( ( ( 𝐶𝐷 ) ‘ 𝐴 ) = 𝐵𝐴 ( 𝐶𝐷 ) 𝐵 ) )
20 17 19 mpbird ( ( 𝜑 ∧ ( 𝐶𝐷 ) Fn 𝑋𝐴𝑋 ) → ( ( 𝐶𝐷 ) ‘ 𝐴 ) = 𝐵 )
21 16 20 eqtr3d ( ( 𝜑 ∧ ( 𝐶𝐷 ) Fn 𝑋𝐴𝑋 ) → ( 𝐶 ‘ ( 𝐷𝐴 ) ) = 𝐵 )
22 eqid ( 𝐷𝐴 ) = ( 𝐷𝐴 )
23 21 22 jctil ( ( 𝜑 ∧ ( 𝐶𝐷 ) Fn 𝑋𝐴𝑋 ) → ( ( 𝐷𝐴 ) = ( 𝐷𝐴 ) ∧ ( 𝐶 ‘ ( 𝐷𝐴 ) ) = 𝐵 ) )
24 13 ffnd ( ( 𝜑 ∧ ( 𝐶𝐷 ) Fn 𝑋𝐴𝑋 ) → 𝐷 Fn 𝑋 )
25 fnbrfvb ( ( 𝐷 Fn 𝑋𝐴𝑋 ) → ( ( 𝐷𝐴 ) = ( 𝐷𝐴 ) ↔ 𝐴 𝐷 ( 𝐷𝐴 ) ) )
26 24 14 25 syl2anc ( ( 𝜑 ∧ ( 𝐶𝐷 ) Fn 𝑋𝐴𝑋 ) → ( ( 𝐷𝐴 ) = ( 𝐷𝐴 ) ↔ 𝐴 𝐷 ( 𝐷𝐴 ) ) )
27 1 3ad2ant1 ( ( 𝜑 ∧ ( 𝐶𝐷 ) Fn 𝑋𝐴𝑋 ) → 𝐶 Fn 𝑌 )
28 13 14 ffvelrnd ( ( 𝜑 ∧ ( 𝐶𝐷 ) Fn 𝑋𝐴𝑋 ) → ( 𝐷𝐴 ) ∈ 𝑌 )
29 fnbrfvb ( ( 𝐶 Fn 𝑌 ∧ ( 𝐷𝐴 ) ∈ 𝑌 ) → ( ( 𝐶 ‘ ( 𝐷𝐴 ) ) = 𝐵 ↔ ( 𝐷𝐴 ) 𝐶 𝐵 ) )
30 27 28 29 syl2anc ( ( 𝜑 ∧ ( 𝐶𝐷 ) Fn 𝑋𝐴𝑋 ) → ( ( 𝐶 ‘ ( 𝐷𝐴 ) ) = 𝐵 ↔ ( 𝐷𝐴 ) 𝐶 𝐵 ) )
31 26 30 anbi12d ( ( 𝜑 ∧ ( 𝐶𝐷 ) Fn 𝑋𝐴𝑋 ) → ( ( ( 𝐷𝐴 ) = ( 𝐷𝐴 ) ∧ ( 𝐶 ‘ ( 𝐷𝐴 ) ) = 𝐵 ) ↔ ( 𝐴 𝐷 ( 𝐷𝐴 ) ∧ ( 𝐷𝐴 ) 𝐶 𝐵 ) ) )
32 23 31 mpbid ( ( 𝜑 ∧ ( 𝐶𝐷 ) Fn 𝑋𝐴𝑋 ) → ( 𝐴 𝐷 ( 𝐷𝐴 ) ∧ ( 𝐷𝐴 ) 𝐶 𝐵 ) )
33 12 32 syl ( 𝜑 → ( 𝐴 𝐷 ( 𝐷𝐴 ) ∧ ( 𝐷𝐴 ) 𝐶 𝐵 ) )