Metamath Proof Explorer


Theorem f1stres

Description: Mapping of a restriction of the 1st (first member of an ordered pair) function. (Contributed by NM, 11-Oct-2004) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion f1stres
|- ( 1st |` ( A X. B ) ) : ( A X. B ) --> A

Proof

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