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 ⊢φ→CFnY
brcoffn.d ⊢φ→D:X⟶Y
brcoffn.r ⊢φ→AC∘DB
Assertion brcoffn ⊢φ→ADD⁡A∧D⁡ACB

Proof

Step Hyp Ref Expression
1 brcoffn.c ⊢φ→CFnY
2 brcoffn.d ⊢φ→D:X⟶Y
3 brcoffn.r ⊢φ→AC∘DB
4 fnfco ⊢CFnY∧D:X⟶Y→C∘DFnX
5 1 2 4 syl2anc ⊢φ→C∘DFnX
6 simpl ⊢φ∧C∘DFnX→φ
7 simpr ⊢φ∧C∘DFnX→C∘DFnX
8 6 3 syl ⊢φ∧C∘DFnX→AC∘DB
9 fnbr ⊢C∘DFnX∧AC∘DB→A∈X
10 7 8 9 syl2anc ⊢φ∧C∘DFnX→A∈X
11 6 7 10 3jca ⊢φ∧C∘DFnX→φ∧C∘DFnX∧A∈X
12 5 11 mpdan ⊢φ→φ∧C∘DFnX∧A∈X
13 2 3ad2ant1 ⊢φ∧C∘DFnX∧A∈X→D:X⟶Y
14 simp3 ⊢φ∧C∘DFnX∧A∈X→A∈X
15 fvco3 ⊢D:X⟶Y∧A∈X→C∘D⁡A=C⁡D⁡A
16 13 14 15 syl2anc ⊢φ∧C∘DFnX∧A∈X→C∘D⁡A=C⁡D⁡A
17 3 3ad2ant1 ⊢φ∧C∘DFnX∧A∈X→AC∘DB
18 fnbrfvb ⊢C∘DFnX∧A∈X→C∘D⁡A=B↔AC∘DB
19 18 3adant1 ⊢φ∧C∘DFnX∧A∈X→C∘D⁡A=B↔AC∘DB
20 17 19 mpbird ⊢φ∧C∘DFnX∧A∈X→C∘D⁡A=B
21 16 20 eqtr3d ⊢φ∧C∘DFnX∧A∈X→C⁡D⁡A=B
22 eqid ⊢D⁡A=D⁡A
23 21 22 jctil ⊢φ∧C∘DFnX∧A∈X→D⁡A=D⁡A∧C⁡D⁡A=B
24 13 ffnd ⊢φ∧C∘DFnX∧A∈X→DFnX
25 fnbrfvb ⊢DFnX∧A∈X→D⁡A=D⁡A↔ADD⁡A
26 24 14 25 syl2anc ⊢φ∧C∘DFnX∧A∈X→D⁡A=D⁡A↔ADD⁡A
27 1 3ad2ant1 ⊢φ∧C∘DFnX∧A∈X→CFnY
28 13 14 ffvelcdmd ⊢φ∧C∘DFnX∧A∈X→D⁡A∈Y
29 fnbrfvb ⊢CFnY∧D⁡A∈Y→C⁡D⁡A=B↔D⁡ACB
30 27 28 29 syl2anc ⊢φ∧C∘DFnX∧A∈X→C⁡D⁡A=B↔D⁡ACB
31 26 30 anbi12d ⊢φ∧C∘DFnX∧A∈X→D⁡A=D⁡A∧C⁡D⁡A=B↔ADD⁡A∧D⁡ACB
32 23 31 mpbid ⊢φ∧C∘DFnX∧A∈X→ADD⁡A∧D⁡ACB
33 12 32 syl ⊢φ→ADD⁡A∧D⁡ACB