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

Proof

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