Metamath Proof Explorer

Theorem brco2f1o

Description: Conditions allowing the decomposition of a binary relation. (Contributed by RP, 8-Jun-2021)

Ref Expression
Hypotheses brco2f1o.c ⊢ φ → C : Y ⟶ 1-1 onto Z
brco2f1o.d ⊢ φ → D : X ⟶ 1-1 onto Y
brco2f1o.r ⊢ φ → A C ∘ D B
Assertion brco2f1o ⊢ φ → C -1 ⁡ B C B ∧ A D C -1 ⁡ B

Proof

Step Hyp Ref Expression
1 brco2f1o.c ⊢ φ → C : Y ⟶ 1-1 onto Z
2 brco2f1o.d ⊢ φ → D : X ⟶ 1-1 onto Y
3 brco2f1o.r ⊢ φ → A C ∘ D B
4 f1ocnv ⊢ D : X ⟶ 1-1 onto Y → D -1 : Y ⟶ 1-1 onto X
5 f1ofn ⊢ D -1 : Y ⟶ 1-1 onto X → D -1 Fn Y
6 2 4 5 3syl ⊢ φ → D -1 Fn Y
7 f1ocnv ⊢ C : Y ⟶ 1-1 onto Z → C -1 : Z ⟶ 1-1 onto Y
8 f1of ⊢ C -1 : Z ⟶ 1-1 onto Y → C -1 : Z ⟶ Y
9 1 7 8 3syl ⊢ φ → C -1 : Z ⟶ Y
10 relco ⊢ Rel ⁡ C ∘ D
11 10 relbrcnv ⊢ B C ∘ D -1 A ↔ A C ∘ D B
12 cnvco ⊢ C ∘ D -1 = D -1 ∘ C -1
13 12 breqi ⊢ B C ∘ D -1 A ↔ B D -1 ∘ C -1 A
14 11 13 bitr3i ⊢ A C ∘ D B ↔ B D -1 ∘ C -1 A
15 3 14 sylib ⊢ φ → B D -1 ∘ C -1 A
16 6 9 15 brcoffn ⊢ φ → B C -1 C -1 ⁡ B ∧ C -1 ⁡ B D -1 A
17 f1orel ⊢ C : Y ⟶ 1-1 onto Z → Rel ⁡ C
18 relbrcnvg ⊢ Rel ⁡ C → B C -1 C -1 ⁡ B ↔ C -1 ⁡ B C B
19 1 17 18 3syl ⊢ φ → B C -1 C -1 ⁡ B ↔ C -1 ⁡ B C B
20 f1orel ⊢ D : X ⟶ 1-1 onto Y → Rel ⁡ D
21 relbrcnvg ⊢ Rel ⁡ D → C -1 ⁡ B D -1 A ↔ A D C -1 ⁡ B
22 2 20 21 3syl ⊢ φ → C -1 ⁡ B D -1 A ↔ A D C -1 ⁡ B
23 19 22 anbi12d ⊢ φ → B C -1 C -1 ⁡ B ∧ C -1 ⁡ B D -1 A ↔ C -1 ⁡ B C B ∧ A D C -1 ⁡ B
24 16 23 mpbid ⊢ φ → C -1 ⁡ B C B ∧ A D C -1 ⁡ B