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 ⊢φ→CFnZ
brcofffn.d ⊢φ→D:Y⟶Z
brcofffn.e ⊢φ→E:X⟶Y
brcofffn.r ⊢φ→AC∘D∘EB
Assertion brcofffn ⊢φ→AEE⁡A∧E⁡ADD⁡E⁡A∧D⁡E⁡ACB

Proof

Step Hyp Ref Expression
1 brcofffn.c ⊢φ→CFnZ
2 brcofffn.d ⊢φ→D:Y⟶Z
3 brcofffn.e ⊢φ→E:X⟶Y
4 brcofffn.r ⊢φ→AC∘D∘EB
5 fnfco ⊢CFnZ∧D:Y⟶Z→C∘DFnY
6 1 2 5 syl2anc ⊢φ→C∘DFnY
7 coass ⊢C∘D∘E=C∘D∘E
8 7 breqi ⊢AC∘D∘EB↔AC∘D∘EB
9 4 8 sylibr ⊢φ→AC∘D∘EB
10 6 3 9 brcoffn ⊢φ→AEE⁡A∧E⁡AC∘DB
11 1 adantr ⊢φ∧AEE⁡A∧E⁡AC∘DB→CFnZ
12 2 adantr ⊢φ∧AEE⁡A∧E⁡AC∘DB→D:Y⟶Z
13 simprr ⊢φ∧AEE⁡A∧E⁡AC∘DB→E⁡AC∘DB
14 11 12 13 brcoffn ⊢φ∧AEE⁡A∧E⁡AC∘DB→E⁡ADD⁡E⁡A∧D⁡E⁡ACB
15 14 ex ⊢φ→AEE⁡A∧E⁡AC∘DB→E⁡ADD⁡E⁡A∧D⁡E⁡ACB
16 10 15 jcai ⊢φ→AEE⁡A∧E⁡AC∘DB∧E⁡ADD⁡E⁡A∧D⁡E⁡ACB
17 simpll ⊢AEE⁡A∧E⁡AC∘DB∧E⁡ADD⁡E⁡A∧D⁡E⁡ACB→AEE⁡A
18 simprl ⊢AEE⁡A∧E⁡AC∘DB∧E⁡ADD⁡E⁡A∧D⁡E⁡ACB→E⁡ADD⁡E⁡A
19 simprr ⊢AEE⁡A∧E⁡AC∘DB∧E⁡ADD⁡E⁡A∧D⁡E⁡ACB→D⁡E⁡ACB
20 17 18 19 3jca ⊢AEE⁡A∧E⁡AC∘DB∧E⁡ADD⁡E⁡A∧D⁡E⁡ACB→AEE⁡A∧E⁡ADD⁡E⁡A∧D⁡E⁡ACB
21 16 20 syl ⊢φ→AEE⁡A∧E⁡ADD⁡E⁡A∧D⁡E⁡ACB