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

Metamath Proof Explorer

Theorem reldm

Description: An expression for the domain of a relation. (Contributed by NM, 22-Sep-2013)

Ref Expression
Assertion reldm 
|- ( Rel A -> dom A = ran ( x e. A |-> ( 1st ` x ) ) )

Proof

Step Hyp Ref Expression
1 releldm2 
 |-  ( Rel A -> ( y e. dom A <-> E. z e. A ( 1st ` z ) = y ) )
2 fvex 
 |-  ( 1st ` x ) e. _V
3 eqid 
 |-  ( x e. A |-> ( 1st ` x ) ) = ( x e. A |-> ( 1st ` x ) )
4 2 3 fnmpti 
 |-  ( x e. A |-> ( 1st ` x ) ) Fn A
5 fvelrnb 
 |-  ( ( x e. A |-> ( 1st ` x ) ) Fn A -> ( y e. ran ( x e. A |-> ( 1st ` x ) ) <-> E. z e. A ( ( x e. A |-> ( 1st ` x ) ) ` z ) = y ) )
6 4 5 ax-mp 
 |-  ( y e. ran ( x e. A |-> ( 1st ` x ) ) <-> E. z e. A ( ( x e. A |-> ( 1st ` x ) ) ` z ) = y )
7 fveq2 
 |-  ( x = z -> ( 1st ` x ) = ( 1st ` z ) )
8 fvex 
 |-  ( 1st ` z ) e. _V
9 7 3 8 fvmpt 
 |-  ( z e. A -> ( ( x e. A |-> ( 1st ` x ) ) ` z ) = ( 1st ` z ) )
10 9 eqeq1d 
 |-  ( z e. A -> ( ( ( x e. A |-> ( 1st ` x ) ) ` z ) = y <-> ( 1st ` z ) = y ) )
11 10 rexbiia 
 |-  ( E. z e. A ( ( x e. A |-> ( 1st ` x ) ) ` z ) = y <-> E. z e. A ( 1st ` z ) = y )
12 11 a1i 
 |-  ( Rel A -> ( E. z e. A ( ( x e. A |-> ( 1st ` x ) ) ` z ) = y <-> E. z e. A ( 1st ` z ) = y ) )
13 6 12 bitr2id 
 |-  ( Rel A -> ( E. z e. A ( 1st ` z ) = y <-> y e. ran ( x e. A |-> ( 1st ` x ) ) ) )
14 1 13 bitrd 
 |-  ( Rel A -> ( y e. dom A <-> y e. ran ( x e. A |-> ( 1st ` x ) ) ) )
15 14 eqrdv 
 |-  ( Rel A -> dom A = ran ( x e. A |-> ( 1st ` x ) ) )