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