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 ⊢ φ → C Fn Z
brcofffn.d ⊢ φ → D : Y ⟶ Z
brcofffn.e ⊢ φ → E : X ⟶ Y
brcofffn.r ⊢ φ → A C ∘ D ∘ E B
Assertion brcofffn ⊢ φ → A E E ⁡ A ∧ E ⁡ A D D ⁡ E ⁡ A ∧ D ⁡ E ⁡ A C B

Proof

Step Hyp Ref Expression
1 brcofffn.c ⊢ φ → C Fn Z
2 brcofffn.d ⊢ φ → D : Y ⟶ Z
3 brcofffn.e ⊢ φ → E : X ⟶ Y
4 brcofffn.r ⊢ φ → A C ∘ D ∘ E B
5 fnfco ⊢ C Fn Z ∧ D : Y ⟶ Z → C ∘ D Fn Y
6 1 2 5 syl2anc ⊢ φ → C ∘ D Fn Y
7 coass ⊢ C ∘ D ∘ E = C ∘ D ∘ E
8 7 breqi ⊢ A C ∘ D ∘ E B ↔ A C ∘ D ∘ E B
9 4 8 sylibr ⊢ φ → A C ∘ D ∘ E B
10 6 3 9 brcoffn ⊢ φ → A E E ⁡ A ∧ E ⁡ A C ∘ D B
11 1 adantr ⊢ φ ∧ A E E ⁡ A ∧ E ⁡ A C ∘ D B → C Fn Z
12 2 adantr ⊢ φ ∧ A E E ⁡ A ∧ E ⁡ A C ∘ D B → D : Y ⟶ Z
13 simprr ⊢ φ ∧ A E E ⁡ A ∧ E ⁡ A C ∘ D B → E ⁡ A C ∘ D B
14 11 12 13 brcoffn ⊢ φ ∧ A E E ⁡ A ∧ E ⁡ A C ∘ D B → E ⁡ A D D ⁡ E ⁡ A ∧ D ⁡ E ⁡ A C B
15 14 ex ⊢ φ → A E E ⁡ A ∧ E ⁡ A C ∘ D B → E ⁡ A D D ⁡ E ⁡ A ∧ D ⁡ E ⁡ A C B
16 10 15 jcai ⊢ φ → A E E ⁡ A ∧ E ⁡ A C ∘ D B ∧ E ⁡ A D D ⁡ E ⁡ A ∧ D ⁡ E ⁡ A C B
17 simpll ⊢ A E E ⁡ A ∧ E ⁡ A C ∘ 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 ∘ 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 ∘ 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 ∘ 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 ⊢ φ → A E E ⁡ A ∧ E ⁡ A D D ⁡ E ⁡ A ∧ D ⁡ E ⁡ A C B