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 ⊢ ( 𝜑 → 𝐶 Fn 𝑍 )
brcofffn.d ⊢ ( 𝜑 → 𝐷 : 𝑌 ⟶ 𝑍 )
brcofffn.e ⊢ ( 𝜑 → 𝐸 : 𝑋 ⟶ 𝑌 )
brcofffn.r ⊢ ( 𝜑 → 𝐴 ( 𝐶 ∘ ( 𝐷 ∘ 𝐸 ) ) 𝐵 )
Assertion brcofffn ( 𝜑 → ( 𝐴 𝐸 ( 𝐸 ‘ 𝐴 ) ∧ ( 𝐸 ‘ 𝐴 ) 𝐷 ( 𝐷 ‘ ( 𝐸 ‘ 𝐴 ) ) ∧ ( 𝐷 ‘ ( 𝐸 ‘ 𝐴 ) ) 𝐶 𝐵 ) )

Proof

Step Hyp Ref Expression
1 brcofffn.c ⊢ ( 𝜑 → 𝐶 Fn 𝑍 )
2 brcofffn.d ⊢ ( 𝜑 → 𝐷 : 𝑌 ⟶ 𝑍 )
3 brcofffn.e ⊢ ( 𝜑 → 𝐸 : 𝑋 ⟶ 𝑌 )
4 brcofffn.r ⊢ ( 𝜑 → 𝐴 ( 𝐶 ∘ ( 𝐷 ∘ 𝐸 ) ) 𝐵 )
5 fnfco ⊢ ( ( 𝐶 Fn 𝑍 ∧ 𝐷 : 𝑌 ⟶ 𝑍 ) → ( 𝐶 ∘ 𝐷 ) Fn 𝑌 )
6 1 2 5 syl2anc ⊢ ( 𝜑 → ( 𝐶 ∘ 𝐷 ) Fn 𝑌 )
7 coass ⊢ ( ( 𝐶 ∘ 𝐷 ) ∘ 𝐸 ) = ( 𝐶 ∘ ( 𝐷 ∘ 𝐸 ) )
8 7 breqi ⊢ ( 𝐴 ( ( 𝐶 ∘ 𝐷 ) ∘ 𝐸 ) 𝐵 ↔ 𝐴 ( 𝐶 ∘ ( 𝐷 ∘ 𝐸 ) ) 𝐵 )
9 4 8 sylibr ⊢ ( 𝜑 → 𝐴 ( ( 𝐶 ∘ 𝐷 ) ∘ 𝐸 ) 𝐵 )
10 6 3 9 brcoffn ⊢ ( 𝜑 → ( 𝐴 𝐸 ( 𝐸 ‘ 𝐴 ) ∧ ( 𝐸 ‘ 𝐴 ) ( 𝐶 ∘ 𝐷 ) 𝐵 ) )
11 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 𝐸 ( 𝐸 ‘ 𝐴 ) ∧ ( 𝐸 ‘ 𝐴 ) ( 𝐶 ∘ 𝐷 ) 𝐵 ) ) → 𝐶 Fn 𝑍 )
12 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 𝐸 ( 𝐸 ‘ 𝐴 ) ∧ ( 𝐸 ‘ 𝐴 ) ( 𝐶 ∘ 𝐷 ) 𝐵 ) ) → 𝐷 : 𝑌 ⟶ 𝑍 )
13 simprr ⊢ ( ( 𝜑 ∧ ( 𝐴 𝐸 ( 𝐸 ‘ 𝐴 ) ∧ ( 𝐸 ‘ 𝐴 ) ( 𝐶 ∘ 𝐷 ) 𝐵 ) ) → ( 𝐸 ‘ 𝐴 ) ( 𝐶 ∘ 𝐷 ) 𝐵 )
14 11 12 13 brcoffn ⊢ ( ( 𝜑 ∧ ( 𝐴 𝐸 ( 𝐸 ‘ 𝐴 ) ∧ ( 𝐸 ‘ 𝐴 ) ( 𝐶 ∘ 𝐷 ) 𝐵 ) ) → ( ( 𝐸 ‘ 𝐴 ) 𝐷 ( 𝐷 ‘ ( 𝐸 ‘ 𝐴 ) ) ∧ ( 𝐷 ‘ ( 𝐸 ‘ 𝐴 ) ) 𝐶 𝐵 ) )
15 14 ex ⊢ ( 𝜑 → ( ( 𝐴 𝐸 ( 𝐸 ‘ 𝐴 ) ∧ ( 𝐸 ‘ 𝐴 ) ( 𝐶 ∘ 𝐷 ) 𝐵 ) → ( ( 𝐸 ‘ 𝐴 ) 𝐷 ( 𝐷 ‘ ( 𝐸 ‘ 𝐴 ) ) ∧ ( 𝐷 ‘ ( 𝐸 ‘ 𝐴 ) ) 𝐶 𝐵 ) ) )
16 10 15 jcai ⊢ ( 𝜑 → ( ( 𝐴 𝐸 ( 𝐸 ‘ 𝐴 ) ∧ ( 𝐸 ‘ 𝐴 ) ( 𝐶 ∘ 𝐷 ) 𝐵 ) ∧ ( ( 𝐸 ‘ 𝐴 ) 𝐷 ( 𝐷 ‘ ( 𝐸 ‘ 𝐴 ) ) ∧ ( 𝐷 ‘ ( 𝐸 ‘ 𝐴 ) ) 𝐶 𝐵 ) ) )
17 simpll ⊢ ( ( ( 𝐴 𝐸 ( 𝐸 ‘ 𝐴 ) ∧ ( 𝐸 ‘ 𝐴 ) ( 𝐶 ∘ 𝐷 ) 𝐵 ) ∧ ( ( 𝐸 ‘ 𝐴 ) 𝐷 ( 𝐷 ‘ ( 𝐸 ‘ 𝐴 ) ) ∧ ( 𝐷 ‘ ( 𝐸 ‘ 𝐴 ) ) 𝐶 𝐵 ) ) → 𝐴 𝐸 ( 𝐸 ‘ 𝐴 ) )
18 simprl ⊢ ( ( ( 𝐴 𝐸 ( 𝐸 ‘ 𝐴 ) ∧ ( 𝐸 ‘ 𝐴 ) ( 𝐶 ∘ 𝐷 ) 𝐵 ) ∧ ( ( 𝐸 ‘ 𝐴 ) 𝐷 ( 𝐷 ‘ ( 𝐸 ‘ 𝐴 ) ) ∧ ( 𝐷 ‘ ( 𝐸 ‘ 𝐴 ) ) 𝐶 𝐵 ) ) → ( 𝐸 ‘ 𝐴 ) 𝐷 ( 𝐷 ‘ ( 𝐸 ‘ 𝐴 ) ) )
19 simprr ⊢ ( ( ( 𝐴 𝐸 ( 𝐸 ‘ 𝐴 ) ∧ ( 𝐸 ‘ 𝐴 ) ( 𝐶 ∘ 𝐷 ) 𝐵 ) ∧ ( ( 𝐸 ‘ 𝐴 ) 𝐷 ( 𝐷 ‘ ( 𝐸 ‘ 𝐴 ) ) ∧ ( 𝐷 ‘ ( 𝐸 ‘ 𝐴 ) ) 𝐶 𝐵 ) ) → ( 𝐷 ‘ ( 𝐸 ‘ 𝐴 ) ) 𝐶 𝐵 )
20 17 18 19 3jca ⊢ ( ( ( 𝐴 𝐸 ( 𝐸 ‘ 𝐴 ) ∧ ( 𝐸 ‘ 𝐴 ) ( 𝐶 ∘ 𝐷 ) 𝐵 ) ∧ ( ( 𝐸 ‘ 𝐴 ) 𝐷 ( 𝐷 ‘ ( 𝐸 ‘ 𝐴 ) ) ∧ ( 𝐷 ‘ ( 𝐸 ‘ 𝐴 ) ) 𝐶 𝐵 ) ) → ( 𝐴 𝐸 ( 𝐸 ‘ 𝐴 ) ∧ ( 𝐸 ‘ 𝐴 ) 𝐷 ( 𝐷 ‘ ( 𝐸 ‘ 𝐴 ) ) ∧ ( 𝐷 ‘ ( 𝐸 ‘ 𝐴 ) ) 𝐶 𝐵 ) )
21 16 20 syl ⊢ ( 𝜑 → ( 𝐴 𝐸 ( 𝐸 ‘ 𝐴 ) ∧ ( 𝐸 ‘ 𝐴 ) 𝐷 ( 𝐷 ‘ ( 𝐸 ‘ 𝐴 ) ) ∧ ( 𝐷 ‘ ( 𝐸 ‘ 𝐴 ) ) 𝐶 𝐵 ) )