Theorem brco2f1o

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

	Ref	Expression
Hypotheses	brco2f1o.c	⊢ ( 𝜑 → 𝐶 : 𝑌 –1-1-onto→ 𝑍 )
	brco2f1o.d	⊢ ( 𝜑 → 𝐷 : 𝑋 –1-1-onto→ 𝑌 )
	brco2f1o.r	⊢ ( 𝜑 → 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 )
Assertion	brco2f1o	⊢ ( 𝜑 → ( ( ◡ 𝐶 ‘ 𝐵 ) 𝐶 𝐵 ∧ 𝐴 𝐷 ( ◡ 𝐶 ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		brco2f1o.c	⊢ ( 𝜑 → 𝐶 : 𝑌 –1-1-onto→ 𝑍 )
2		brco2f1o.d	⊢ ( 𝜑 → 𝐷 : 𝑋 –1-1-onto→ 𝑌 )
3		brco2f1o.r	⊢ ( 𝜑 → 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 )
4		f1ocnv	⊢ ( 𝐷 : 𝑋 –1-1-onto→ 𝑌 → ◡ 𝐷 : 𝑌 –1-1-onto→ 𝑋 )
5		f1ofn	⊢ ( ◡ 𝐷 : 𝑌 –1-1-onto→ 𝑋 → ◡ 𝐷 Fn 𝑌 )
6	2 4 5	3syl	⊢ ( 𝜑 → ◡ 𝐷 Fn 𝑌 )
7		f1ocnv	⊢ ( 𝐶 : 𝑌 –1-1-onto→ 𝑍 → ◡ 𝐶 : 𝑍 –1-1-onto→ 𝑌 )
8		f1of	⊢ ( ◡ 𝐶 : 𝑍 –1-1-onto→ 𝑌 → ◡ 𝐶 : 𝑍 ⟶ 𝑌 )
9	1 7 8	3syl	⊢ ( 𝜑 → ◡ 𝐶 : 𝑍 ⟶ 𝑌 )
10		relco	⊢ Rel ( 𝐶 ∘ 𝐷 )
11	10	relbrcnv	⊢ ( 𝐵 ◡ ( 𝐶 ∘ 𝐷 ) 𝐴 ↔ 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 )
12		cnvco	⊢ ◡ ( 𝐶 ∘ 𝐷 ) = ( ◡ 𝐷 ∘ ◡ 𝐶 )
13	12	breqi	⊢ ( 𝐵 ◡ ( 𝐶 ∘ 𝐷 ) 𝐴 ↔ 𝐵 ( ◡ 𝐷 ∘ ◡ 𝐶 ) 𝐴 )
14	11 13	bitr3i	⊢ ( 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 ↔ 𝐵 ( ◡ 𝐷 ∘ ◡ 𝐶 ) 𝐴 )
15	3 14	sylib	⊢ ( 𝜑 → 𝐵 ( ◡ 𝐷 ∘ ◡ 𝐶 ) 𝐴 )
16	6 9 15	brcoffn	⊢ ( 𝜑 → ( 𝐵 ◡ 𝐶 ( ◡ 𝐶 ‘ 𝐵 ) ∧ ( ◡ 𝐶 ‘ 𝐵 ) ◡ 𝐷 𝐴 ) )
17		f1orel	⊢ ( 𝐶 : 𝑌 –1-1-onto→ 𝑍 → Rel 𝐶 )
18		relbrcnvg	⊢ ( Rel 𝐶 → ( 𝐵 ◡ 𝐶 ( ◡ 𝐶 ‘ 𝐵 ) ↔ ( ◡ 𝐶 ‘ 𝐵 ) 𝐶 𝐵 ) )
19	1 17 18	3syl	⊢ ( 𝜑 → ( 𝐵 ◡ 𝐶 ( ◡ 𝐶 ‘ 𝐵 ) ↔ ( ◡ 𝐶 ‘ 𝐵 ) 𝐶 𝐵 ) )
20		f1orel	⊢ ( 𝐷 : 𝑋 –1-1-onto→ 𝑌 → Rel 𝐷 )
21		relbrcnvg	⊢ ( Rel 𝐷 → ( ( ◡ 𝐶 ‘ 𝐵 ) ◡ 𝐷 𝐴 ↔ 𝐴 𝐷 ( ◡ 𝐶 ‘ 𝐵 ) ) )
22	2 20 21	3syl	⊢ ( 𝜑 → ( ( ◡ 𝐶 ‘ 𝐵 ) ◡ 𝐷 𝐴 ↔ 𝐴 𝐷 ( ◡ 𝐶 ‘ 𝐵 ) ) )
23	19 22	anbi12d	⊢ ( 𝜑 → ( ( 𝐵 ◡ 𝐶 ( ◡ 𝐶 ‘ 𝐵 ) ∧ ( ◡ 𝐶 ‘ 𝐵 ) ◡ 𝐷 𝐴 ) ↔ ( ( ◡ 𝐶 ‘ 𝐵 ) 𝐶 𝐵 ∧ 𝐴 𝐷 ( ◡ 𝐶 ‘ 𝐵 ) ) ) )
24	16 23	mpbid	⊢ ( 𝜑 → ( ( ◡ 𝐶 ‘ 𝐵 ) 𝐶 𝐵 ∧ 𝐴 𝐷 ( ◡ 𝐶 ‘ 𝐵 ) ) )