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

Metamath Proof Explorer

Theorem brimage

Description: Binary relation form of the Image functor. (Contributed by Scott Fenton, 4-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Hypotheses brimage.1 
|- A e. _V
brimage.2 
|- B e. _V
Assertion brimage 
|- ( A Image R B <-> B = ( R " A ) )

Proof

Step Hyp Ref Expression
1 brimage.1 
 |-  A e. _V
2 brimage.2 
 |-  B e. _V
3 df-image 
 |-  Image R = ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E o. `' R ) (x) _V ) ) )
4 brxp 
 |-  ( A ( _V X. _V ) B <-> ( A e. _V /\ B e. _V ) )
5 1 2 4 mpbir2an 
 |-  A ( _V X. _V ) B
6 vex 
 |-  x e. _V
7 vex 
 |-  y e. _V
8 6 7 brcnv 
 |-  ( x `' R y <-> y R x )
9 8 rexbii 
 |-  ( E. y e. A x `' R y <-> E. y e. A y R x )
10 6 1 coep 
 |-  ( x ( _E o. `' R ) A <-> E. y e. A x `' R y )
11 6 elima 
 |-  ( x e. ( R " A ) <-> E. y e. A y R x )
12 9 10 11 3bitr4ri 
 |-  ( x e. ( R " A ) <-> x ( _E o. `' R ) A )
13 1 2 3 5 12 brtxpsd3 
 |-  ( A Image R B <-> B = ( R " A ) )