Metamath Proof Explorer

Theorem dfcnv2

Description: Alternative definition of the converse of a relation. (Contributed by Thierry Arnoux, 31-Mar-2018)

Ref Expression
Assertion dfcnv2 
|- ( ran R C_ A -> `' R = U_ x e. A ( { x } X. ( `' R " { x } ) ) )

Proof

Step Hyp Ref Expression
1 relcnv 
 |-  Rel `' R
2 relxp 
 |-  Rel ( { x } X. ( `' R " { x } ) )
3 2 rgenw 
 |-  A. x e. A Rel ( { x } X. ( `' R " { x } ) )
4 reliun 
 |-  ( Rel U_ x e. A ( { x } X. ( `' R " { x } ) ) <-> A. x e. A Rel ( { x } X. ( `' R " { x } ) ) )
5 3 4 mpbir 
 |-  Rel U_ x e. A ( { x } X. ( `' R " { x } ) )
6 vex 
 |-  z e. _V
7 vex 
 |-  y e. _V
8 6 7 opeldm 
 |-  ( <. z , y >. e. `' R -> z e. dom `' R )
9 df-rn 
 |-  ran R = dom `' R
10 8 9 eleqtrrdi 
 |-  ( <. z , y >. e. `' R -> z e. ran R )
11 ssel2 
 |-  ( ( ran R C_ A /\ z e. ran R ) -> z e. A )
12 10 11 sylan2 
 |-  ( ( ran R C_ A /\ <. z , y >. e. `' R ) -> z e. A )
13 12 ex 
 |-  ( ran R C_ A -> ( <. z , y >. e. `' R -> z e. A ) )
14 13 pm4.71rd 
 |-  ( ran R C_ A -> ( <. z , y >. e. `' R <-> ( z e. A /\ <. z , y >. e. `' R ) ) )
15 6 7 elimasn 
 |-  ( y e. ( `' R " { z } ) <-> <. z , y >. e. `' R )
16 15 anbi2i 
 |-  ( ( z e. A /\ y e. ( `' R " { z } ) ) <-> ( z e. A /\ <. z , y >. e. `' R ) )
17 14 16 bitr4di 
 |-  ( ran R C_ A -> ( <. z , y >. e. `' R <-> ( z e. A /\ y e. ( `' R " { z } ) ) ) )
18 sneq 
 |-  ( x = z -> { x } = { z } )
19 18 imaeq2d 
 |-  ( x = z -> ( `' R " { x } ) = ( `' R " { z } ) )
20 19 opeliunxp2 
 |-  ( <. z , y >. e. U_ x e. A ( { x } X. ( `' R " { x } ) ) <-> ( z e. A /\ y e. ( `' R " { z } ) ) )
21 17 20 bitr4di 
 |-  ( ran R C_ A -> ( <. z , y >. e. `' R <-> <. z , y >. e. U_ x e. A ( { x } X. ( `' R " { x } ) ) ) )
22 1 5 21 eqrelrdv 
 |-  ( ran R C_ A -> `' R = U_ x e. A ( { x } X. ( `' R " { x } ) ) )