Metamath Proof Explorer

Theorem df1stres

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

Ref Expression
Assertion df1stres 
|- ( 1st |` ( A X. B ) ) = ( x e. A , y e. B |-> x )

Proof

Step Hyp Ref Expression
1 df1st2 
 |-  { <. <. x , y >. , z >. | z = x } = ( 1st |` ( _V X. _V ) )
2 1 reseq1i 
 |-  ( { <. <. x , y >. , z >. | z = x } |` ( A X. B ) ) = ( ( 1st |` ( _V X. _V ) ) |` ( A X. B ) )
3 resoprab 
 |-  ( { <. <. x , y >. , z >. | z = x } |` ( A X. B ) ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = x ) }
4 resres 
 |-  ( ( 1st |` ( _V X. _V ) ) |` ( A X. B ) ) = ( 1st |` ( ( _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 
 |-  ( 1st |` ( ( _V X. _V ) i^i ( A X. B ) ) ) = ( 1st |` ( A X. B ) )
11 4 10 eqtri 
 |-  ( ( 1st |` ( _V X. _V ) ) |` ( A X. B ) ) = ( 1st |` ( A X. B ) )
12 2 3 11 3eqtr3ri 
 |-  ( 1st |` ( A X. B ) ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = x ) }
13 df-mpo 
 |-  ( x e. A , y e. B |-> x ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = x ) }
14 12 13 eqtr4i 
 |-  ( 1st |` ( A X. B ) ) = ( x e. A , y e. B |-> x )