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 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐷 ‘ 𝐴 ) ∈ 𝑌 )
29 fnbrfvb ⊢ ( ( 𝐶 Fn 𝑌 ∧ ( 𝐷 ‘ 𝐴 ) ∈ 𝑌 ) → ( ( 𝐶 ‘ ( 𝐷 ‘ 𝐴 ) ) = 𝐵 ↔ ( 𝐷 ‘ 𝐴 ) 𝐶 𝐵 ) )
30 27 28 29 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐶 ‘ ( 𝐷 ‘ 𝐴 ) ) = 𝐵 ↔ ( 𝐷 ‘ 𝐴 ) 𝐶 𝐵 ) )
31 26 30 anbi12d ⊢ ( ( 𝜑 ∧ ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ 𝐴 ) ∧ ( 𝐶 ‘ ( 𝐷 ‘ 𝐴 ) ) = 𝐵 ) ↔ ( 𝐴 𝐷 ( 𝐷 ‘ 𝐴 ) ∧ ( 𝐷 ‘ 𝐴 ) 𝐶 𝐵 ) ) )
32 23 31 mpbid ⊢ ( ( 𝜑 ∧ ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐷 ( 𝐷 ‘ 𝐴 ) ∧ ( 𝐷 ‘ 𝐴 ) 𝐶 𝐵 ) )
33 12 32 syl ⊢ ( 𝜑 → ( 𝐴 𝐷 ( 𝐷 ‘ 𝐴 ) ∧ ( 𝐷 ‘ 𝐴 ) 𝐶 𝐵 ) )