Metamath Proof Explorer

Theorem df2ndres

Description: Definition for a restriction of the 2nd (second member of an ordered pair) function. (Contributed by Thierry Arnoux, 27-Sep-2017)

Ref Expression
Assertion df2ndres 
|- ( 2nd |` ( A X. B ) ) = ( x e. A , y e. B |-> y )

Proof

Step Hyp Ref Expression
1 df2nd2 
 |-  { <. <. x , y >. , z >. | z = y } = ( 2nd |` ( _V X. _V ) )
2 1 reseq1i 
 |-  ( { <. <. x , y >. , z >. | z = y } |` ( A X. B ) ) = ( ( 2nd |` ( _V X. _V ) ) |` ( A X. B ) )
3 resoprab 
 |-  ( { <. <. x , y >. , z >. | z = y } |` ( A X. B ) ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = y ) }
4 resres 
 |-  ( ( 2nd |` ( _V X. _V ) ) |` ( A X. B ) ) = ( 2nd |` ( ( _V X. _V ) i^i ( A X. B ) ) )
5 incom 
 |-  ( ( A X. B ) i^i ( _V X. _V ) ) = ( ( _V X. _V ) i^i ( A X. B ) )
6 xpss 
 |-  ( A X. B ) C_ ( _V X. _V )
7 df-ss 
 |-  ( ( A X. B ) C_ ( _V X. _V ) <-> ( ( A X. B ) i^i ( _V X. _V ) ) = ( A X. B ) )
8 6 7 mpbi 
 |-  ( ( A X. B ) i^i ( _V X. _V ) ) = ( A X. B )
9 5 8 eqtr3i 
 |-  ( ( _V X. _V ) i^i ( A X. B ) ) = ( A X. B )
10 9 reseq2i 
 |-  ( 2nd |` ( ( _V X. _V ) i^i ( A X. B ) ) ) = ( 2nd |` ( A X. B ) )
11 4 10 eqtri 
 |-  ( ( 2nd |` ( _V X. _V ) ) |` ( A X. B ) ) = ( 2nd |` ( A X. B ) )
12 2 3 11 3eqtr3ri 
 |-  ( 2nd |` ( A X. B ) ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = y ) }
13 df-mpo 
 |-  ( x e. A , y e. B |-> y ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = y ) }
14 12 13 eqtr4i 
 |-  ( 2nd |` ( A X. B ) ) = ( x e. A , y e. B |-> y )