Metamath Proof Explorer

Theorem df2nd2

Description: An alternate possible definition of the 2nd function. (Contributed by NM, 10-Aug-2006) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion df2nd2 
|- { <. <. x , y >. , z >. | z = y } = ( 2nd |` ( _V X. _V ) )

Proof

Step Hyp Ref Expression
1 fo2nd 
 |-  2nd : _V -onto-> _V
2 fofn 
 |-  ( 2nd : _V -onto-> _V -> 2nd Fn _V )
3 1 2 ax-mp 
 |-  2nd Fn _V
4 dffn5 
 |-  ( 2nd Fn _V <-> 2nd = ( w e. _V |-> ( 2nd ` w ) ) )
5 3 4 mpbi 
 |-  2nd = ( w e. _V |-> ( 2nd ` w ) )
6 mptv 
 |-  ( w e. _V |-> ( 2nd ` w ) ) = { <. w , z >. | z = ( 2nd ` w ) }
7 5 6 eqtri 
 |-  2nd = { <. w , z >. | z = ( 2nd ` w ) }
8 7 reseq1i 
 |-  ( 2nd |` ( _V X. _V ) ) = ( { <. w , z >. | z = ( 2nd ` w ) } |` ( _V X. _V ) )
9 resopab 
 |-  ( { <. w , z >. | z = ( 2nd ` w ) } |` ( _V X. _V ) ) = { <. w , z >. | ( w e. ( _V X. _V ) /\ z = ( 2nd ` w ) ) }
10 vex 
 |-  x e. _V
11 vex 
 |-  y e. _V
12 10 11 op2ndd 
 |-  ( w = <. x , y >. -> ( 2nd ` w ) = y )
13 12 eqeq2d 
 |-  ( w = <. x , y >. -> ( z = ( 2nd ` w ) <-> z = y ) )
14 13 dfoprab3 
 |-  { <. w , z >. | ( w e. ( _V X. _V ) /\ z = ( 2nd ` w ) ) } = { <. <. x , y >. , z >. | z = y }
15 8 9 14 3eqtrri 
 |-  { <. <. x , y >. , z >. | z = y } = ( 2nd |` ( _V X. _V ) )