This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } ) ) )