brco3f1o

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

	Ref	Expression
Hypotheses	brco3f1o.c	$⊢ φ \to C : Y \underset{1-1 onto}{⟶} Z$
	brco3f1o.d	$⊢ φ \to D : X \underset{1-1 onto}{⟶} Y$
	brco3f1o.e	$⊢ φ \to E : W \underset{1-1 onto}{⟶} X$
	brco3f1o.r	$⊢ φ \to A (C \circ (D \circ E)) B$
Assertion	brco3f1o	$⊢ φ \to (C^{-1} (B) C B \land D^{-1} (C^{-1} (B)) D C^{-1} (B) \land A E D^{-1} (C^{-1} (B)))$

Proof

Step	Hyp	Ref	Expression
1		brco3f1o.c	$⊢ φ \to C : Y \underset{1-1 onto}{⟶} Z$
2		brco3f1o.d	$⊢ φ \to D : X \underset{1-1 onto}{⟶} Y$
3		brco3f1o.e	$⊢ φ \to E : W \underset{1-1 onto}{⟶} X$
4		brco3f1o.r	$⊢ φ \to A (C \circ (D \circ E)) B$
5		f1ocnv	$⊢ E : W \underset{1-1 onto}{⟶} X \to E^{-1} : X \underset{1-1 onto}{⟶} W$
6		f1ofn	$⊢ E^{-1} : X \underset{1-1 onto}{⟶} W \to E^{-1} Fn X$
7	3 5 6	3syl	$⊢ φ \to E^{-1} Fn X$
8		f1ocnv	$⊢ D : X \underset{1-1 onto}{⟶} Y \to D^{-1} : Y \underset{1-1 onto}{⟶} X$
9		f1of	$⊢ D^{-1} : Y \underset{1-1 onto}{⟶} X \to D^{-1} : Y ⟶ X$
10	2 8 9	3syl	$⊢ φ \to D^{-1} : Y ⟶ X$
11		f1ocnv	$⊢ C : Y \underset{1-1 onto}{⟶} Z \to C^{-1} : Z \underset{1-1 onto}{⟶} Y$
12		f1of	$⊢ C^{-1} : Z \underset{1-1 onto}{⟶} Y \to C^{-1} : Z ⟶ Y$
13	1 11 12	3syl	$⊢ φ \to C^{-1} : Z ⟶ Y$
14		relco	$⊢ Rel ((C \circ D) \circ E)$
15	14	relbrcnv	$⊢ B {((C \circ D) \circ E)}^{-1} A \leftrightarrow A ((C \circ D) \circ E) B$
16		cnvco	$⊢ {((C \circ D) \circ E)}^{-1} = E^{-1} \circ {(C \circ D)}^{-1}$
17		cnvco	$⊢ {(C \circ D)}^{-1} = D^{-1} \circ C^{-1}$
18	17	coeq2i	$⊢ E^{-1} \circ {(C \circ D)}^{-1} = E^{-1} \circ (D^{-1} \circ C^{-1})$
19	16 18	eqtri	$⊢ {((C \circ D) \circ E)}^{-1} = E^{-1} \circ (D^{-1} \circ C^{-1})$
20	19	breqi	$⊢ B {((C \circ D) \circ E)}^{-1} A \leftrightarrow B (E^{-1} \circ (D^{-1} \circ C^{-1})) A$
21		coass	$⊢ (C \circ D) \circ E = C \circ (D \circ E)$
22	21	breqi	$⊢ A ((C \circ D) \circ E) B \leftrightarrow A (C \circ (D \circ E)) B$
23	15 20 22	3bitr3ri	$⊢ A (C \circ (D \circ E)) B \leftrightarrow B (E^{-1} \circ (D^{-1} \circ C^{-1})) A$
24	4 23	sylib	$⊢ φ \to B (E^{-1} \circ (D^{-1} \circ C^{-1})) A$
25	7 10 13 24	brcofffn	$⊢ φ \to (B C^{-1} C^{-1} (B) \land C^{-1} (B) D^{-1} D^{-1} (C^{-1} (B)) \land D^{-1} (C^{-1} (B)) E^{-1} A)$
26		f1orel	$⊢ C : Y \underset{1-1 onto}{⟶} Z \to Rel C$
27		relbrcnvg	$⊢ Rel C \to (B C^{-1} C^{-1} (B) \leftrightarrow C^{-1} (B) C B)$
28	1 26 27	3syl	$⊢ φ \to (B C^{-1} C^{-1} (B) \leftrightarrow C^{-1} (B) C B)$
29		f1orel	$⊢ D : X \underset{1-1 onto}{⟶} Y \to Rel D$
30		relbrcnvg	$⊢ Rel D \to (C^{-1} (B) D^{-1} D^{-1} (C^{-1} (B)) \leftrightarrow D^{-1} (C^{-1} (B)) D C^{-1} (B))$
31	2 29 30	3syl	$⊢ φ \to (C^{-1} (B) D^{-1} D^{-1} (C^{-1} (B)) \leftrightarrow D^{-1} (C^{-1} (B)) D C^{-1} (B))$
32		f1orel	$⊢ E : W \underset{1-1 onto}{⟶} X \to Rel E$
33		relbrcnvg	$⊢ Rel E \to (D^{-1} (C^{-1} (B)) E^{-1} A \leftrightarrow A E D^{-1} (C^{-1} (B)))$
34	3 32 33	3syl	$⊢ φ \to (D^{-1} (C^{-1} (B)) E^{-1} A \leftrightarrow A E D^{-1} (C^{-1} (B)))$
35	28 31 34	3anbi123d	$⊢ φ \to ((B C^{-1} C^{-1} (B) \land C^{-1} (B) D^{-1} D^{-1} (C^{-1} (B)) \land D^{-1} (C^{-1} (B)) E^{-1} A) \leftrightarrow (C^{-1} (B) C B \land D^{-1} (C^{-1} (B)) D C^{-1} (B) \land A E D^{-1} (C^{-1} (B))))$
36	25 35	mpbid	$⊢ φ \to (C^{-1} (B) C B \land D^{-1} (C^{-1} (B)) D C^{-1} (B) \land A E D^{-1} (C^{-1} (B)))$

Metamath Proof Explorer

Theorem brco3f1o

Proof