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

Metamath Proof Explorer

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