Theorem f1stres

Description: Mapping of a restriction of the 1st (first member of an ordered pair) function. (Contributed by NM, 11-Oct-2004) (Revised by Mario Carneiro, 8-Sep-2013)

	Ref	Expression
Assertion	f1stres	|- ( 1st |` ( A X. B ) ) : ( A X. B ) --> A

Proof

Step	Hyp	Ref	Expression
1		vex	|- y e. _V
2		vex	|- z e. _V
3	1 2	op1sta	|- U. dom { <. y , z >. } = y
4	3	eleq1i	|- ( U. dom { <. y , z >. } e. A <-> y e. A )
5	4	biranri	|- ( ( y e. A /\ z e. B ) -> U. dom { <. y , z >. } e. A )
6	5	rgen2	|- A. y e. A A. z e. B U. dom { <. y , z >. } e. A
7		sneq	|- ( x = <. y , z >. -> { x } = { <. y , z >. } )
8	7	dmeqd	|- ( x = <. y , z >. -> dom { x } = dom { <. y , z >. } )
9	8	unieqd	|- ( x = <. y , z >. -> U. dom { x } = U. dom { <. y , z >. } )
10	9	eleq1d	|- ( x = <. y , z >. -> ( U. dom { x } e. A <-> U. dom { <. y , z >. } e. A ) )
11	10	ralxp	|- ( A. x e. ( A X. B ) U. dom { x } e. A <-> A. y e. A A. z e. B U. dom { <. y , z >. } e. A )
12	6 11	mpbir	|- A. x e. ( A X. B ) U. dom { x } e. A
13		df-1st	|- 1st = ( x e. _V |-> U. dom { x } )
14	13	reseq1i	|- ( 1st |` ( A X. B ) ) = ( ( x e. _V |-> U. dom { x } ) |` ( A X. B ) )
15		ssv	|- ( A X. B ) C_ _V
16		resmpt	|- ( ( A X. B ) C_ _V -> ( ( x e. _V |-> U. dom { x } ) |` ( A X. B ) ) = ( x e. ( A X. B ) |-> U. dom { x } ) )
17	15 16	ax-mp	|- ( ( x e. _V |-> U. dom { x } ) |` ( A X. B ) ) = ( x e. ( A X. B ) |-> U. dom { x } )
18	14 17	eqtri	|- ( 1st |` ( A X. B ) ) = ( x e. ( A X. B ) |-> U. dom { x } )
19	18	fmpt	|- ( A. x e. ( A X. B ) U. dom { x } e. A <-> ( 1st |` ( A X. B ) ) : ( A X. B ) --> A )
20	12 19	mpbi	|- ( 1st |` ( A X. B ) ) : ( A X. B ) --> A