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