Theorem opelco3

Description: Alternate way of saying that an ordered pair is in a composition. (Contributed by Scott Fenton, 6-May-2018)

	Ref	Expression
Assertion	opelco3	|- ( <. A , B >. e. ( C o. D ) <-> B e. ( C " ( D " { A } ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-br	|- ( A ( C o. D ) B <-> <. A , B >. e. ( C o. D ) )
2		relco	|- Rel ( C o. D )
3	2	brrelex12i	|- ( A ( C o. D ) B -> ( A e. _V /\ B e. _V ) )
4		snprc	|- ( -. A e. _V <-> { A } = (/) )
5		noel	|- -. B e. (/)
6		imaeq2	|- ( { A } = (/) -> ( D " { A } ) = ( D " (/) ) )
7	6	imaeq2d	|- ( { A } = (/) -> ( C " ( D " { A } ) ) = ( C " ( D " (/) ) ) )
8		ima0	|- ( D " (/) ) = (/)
9	8	imaeq2i	|- ( C " ( D " (/) ) ) = ( C " (/) )
10		ima0	|- ( C " (/) ) = (/)
11	9 10	eqtri	|- ( C " ( D " (/) ) ) = (/)
12	7 11	eqtrdi	|- ( { A } = (/) -> ( C " ( D " { A } ) ) = (/) )
13	12	eleq2d	|- ( { A } = (/) -> ( B e. ( C " ( D " { A } ) ) <-> B e. (/) ) )
14	5 13	mtbiri	|- ( { A } = (/) -> -. B e. ( C " ( D " { A } ) ) )
15	4 14	sylbi	|- ( -. A e. _V -> -. B e. ( C " ( D " { A } ) ) )
16	15	con4i	|- ( B e. ( C " ( D " { A } ) ) -> A e. _V )
17		elex	|- ( B e. ( C " ( D " { A } ) ) -> B e. _V )
18	16 17	jca	|- ( B e. ( C " ( D " { A } ) ) -> ( A e. _V /\ B e. _V ) )
19		df-rex	|- ( E. z e. ( D " { A } ) z C B <-> E. z ( z e. ( D " { A } ) /\ z C B ) )
20		elimasng	|- ( ( A e. _V /\ z e. _V ) -> ( z e. ( D " { A } ) <-> <. A , z >. e. D ) )
21	20	elvd	|- ( A e. _V -> ( z e. ( D " { A } ) <-> <. A , z >. e. D ) )
22		df-br	|- ( A D z <-> <. A , z >. e. D )
23	21 22	bitr4di	|- ( A e. _V -> ( z e. ( D " { A } ) <-> A D z ) )
24	23	adantr	|- ( ( A e. _V /\ B e. _V ) -> ( z e. ( D " { A } ) <-> A D z ) )
25	24	anbi1d	|- ( ( A e. _V /\ B e. _V ) -> ( ( z e. ( D " { A } ) /\ z C B ) <-> ( A D z /\ z C B ) ) )
26	25	exbidv	|- ( ( A e. _V /\ B e. _V ) -> ( E. z ( z e. ( D " { A } ) /\ z C B ) <-> E. z ( A D z /\ z C B ) ) )
27	19 26	bitr2id	|- ( ( A e. _V /\ B e. _V ) -> ( E. z ( A D z /\ z C B ) <-> E. z e. ( D " { A } ) z C B ) )
28		brcog	|- ( ( A e. _V /\ B e. _V ) -> ( A ( C o. D ) B <-> E. z ( A D z /\ z C B ) ) )
29		elimag	|- ( B e. _V -> ( B e. ( C " ( D " { A } ) ) <-> E. z e. ( D " { A } ) z C B ) )
30	29	adantl	|- ( ( A e. _V /\ B e. _V ) -> ( B e. ( C " ( D " { A } ) ) <-> E. z e. ( D " { A } ) z C B ) )
31	27 28 30	3bitr4d	|- ( ( A e. _V /\ B e. _V ) -> ( A ( C o. D ) B <-> B e. ( C " ( D " { A } ) ) ) )
32	3 18 31	pm5.21nii	|- ( A ( C o. D ) B <-> B e. ( C " ( D " { A } ) ) )
33	1 32	bitr3i	|- ( <. A , B >. e. ( C o. D ) <-> B e. ( C " ( D " { A } ) ) )