Theorem brco2f1o

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

	Ref	Expression
Hypotheses	brco2f1o.c	|- ( ph -> C : Y -1-1-onto-> Z )
	brco2f1o.d	|- ( ph -> D : X -1-1-onto-> Y )
	brco2f1o.r	|- ( ph -> A ( C o. D ) B )
Assertion	brco2f1o	|- ( ph -> ( ( `' C ` B ) C B /\ A D ( `' C ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		brco2f1o.c	|- ( ph -> C : Y -1-1-onto-> Z )
2		brco2f1o.d	|- ( ph -> D : X -1-1-onto-> Y )
3		brco2f1o.r	|- ( ph -> A ( C o. D ) B )
4		f1ocnv	|- ( D : X -1-1-onto-> Y -> `' D : Y -1-1-onto-> X )
5		f1ofn	|- ( `' D : Y -1-1-onto-> X -> `' D Fn Y )
6	2 4 5	3syl	|- ( ph -> `' D Fn Y )
7		f1ocnv	|- ( C : Y -1-1-onto-> Z -> `' C : Z -1-1-onto-> Y )
8		f1of	|- ( `' C : Z -1-1-onto-> Y -> `' C : Z --> Y )
9	1 7 8	3syl	|- ( ph -> `' C : Z --> Y )
10		relco	|- Rel ( C o. D )
11	10	relbrcnv	|- ( B `' ( C o. D ) A <-> A ( C o. D ) B )
12		cnvco	|- `' ( C o. D ) = ( `' D o. `' C )
13	12	breqi	|- ( B `' ( C o. D ) A <-> B ( `' D o. `' C ) A )
14	11 13	bitr3i	|- ( A ( C o. D ) B <-> B ( `' D o. `' C ) A )
15	3 14	sylib	|- ( ph -> B ( `' D o. `' C ) A )
16	6 9 15	brcoffn	|- ( ph -> ( B `' C ( `' C ` B ) /\ ( `' C ` B ) `' D A ) )
17		f1orel	|- ( C : Y -1-1-onto-> Z -> Rel C )
18		relbrcnvg	|- ( Rel C -> ( B `' C ( `' C ` B ) <-> ( `' C ` B ) C B ) )
19	1 17 18	3syl	|- ( ph -> ( B `' C ( `' C ` B ) <-> ( `' C ` B ) C B ) )
20		f1orel	|- ( D : X -1-1-onto-> Y -> Rel D )
21		relbrcnvg	|- ( Rel D -> ( ( `' C ` B ) `' D A <-> A D ( `' C ` B ) ) )
22	2 20 21	3syl	|- ( ph -> ( ( `' C ` B ) `' D A <-> A D ( `' C ` B ) ) )
23	19 22	anbi12d	|- ( ph -> ( ( B `' C ( `' C ` B ) /\ ( `' C ` B ) `' D A ) <-> ( ( `' C ` B ) C B /\ A D ( `' C ` B ) ) ) )
24	16 23	mpbid	|- ( ph -> ( ( `' C ` B ) C B /\ A D ( `' C ` B ) ) )