Theorem f2ndres

Description: Mapping of a restriction of the 2nd (second member of an ordered pair) function. (Contributed by NM, 7-Aug-2006) (Revised by Mario Carneiro, 8-Sep-2013)

	Ref	Expression
Assertion	f2ndres	|- ( 2nd |` ( A X. B ) ) : ( A X. B ) --> B

Proof

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