Metamath Proof Explorer


Theorem fo1stres

Description: Onto mapping of a restriction of the 1st (first member of an ordered pair) function. (Contributed by NM, 14-Dec-2008)

Ref Expression
Assertion fo1stres
|- ( B =/= (/) -> ( 1st |` ( A X. B ) ) : ( A X. B ) -onto-> A )

Proof

Step Hyp Ref Expression
1 n0
 |-  ( B =/= (/) <-> E. y y e. B )
2 opelxp
 |-  ( <. x , y >. e. ( A X. B ) <-> ( x e. A /\ y e. B ) )
3 fvres
 |-  ( <. x , y >. e. ( A X. B ) -> ( ( 1st |` ( A X. B ) ) ` <. x , y >. ) = ( 1st ` <. x , y >. ) )
4 vex
 |-  x e. _V
5 vex
 |-  y e. _V
6 4 5 op1st
 |-  ( 1st ` <. x , y >. ) = x
7 3 6 eqtr2di
 |-  ( <. x , y >. e. ( A X. B ) -> x = ( ( 1st |` ( A X. B ) ) ` <. x , y >. ) )
8 f1stres
 |-  ( 1st |` ( A X. B ) ) : ( A X. B ) --> A
9 ffn
 |-  ( ( 1st |` ( A X. B ) ) : ( A X. B ) --> A -> ( 1st |` ( A X. B ) ) Fn ( A X. B ) )
10 8 9 ax-mp
 |-  ( 1st |` ( A X. B ) ) Fn ( A X. B )
11 fnfvelrn
 |-  ( ( ( 1st |` ( A X. B ) ) Fn ( A X. B ) /\ <. x , y >. e. ( A X. B ) ) -> ( ( 1st |` ( A X. B ) ) ` <. x , y >. ) e. ran ( 1st |` ( A X. B ) ) )
12 10 11 mpan
 |-  ( <. x , y >. e. ( A X. B ) -> ( ( 1st |` ( A X. B ) ) ` <. x , y >. ) e. ran ( 1st |` ( A X. B ) ) )
13 7 12 eqeltrd
 |-  ( <. x , y >. e. ( A X. B ) -> x e. ran ( 1st |` ( A X. B ) ) )
14 2 13 sylbir
 |-  ( ( x e. A /\ y e. B ) -> x e. ran ( 1st |` ( A X. B ) ) )
15 14 expcom
 |-  ( y e. B -> ( x e. A -> x e. ran ( 1st |` ( A X. B ) ) ) )
16 15 exlimiv
 |-  ( E. y y e. B -> ( x e. A -> x e. ran ( 1st |` ( A X. B ) ) ) )
17 1 16 sylbi
 |-  ( B =/= (/) -> ( x e. A -> x e. ran ( 1st |` ( A X. B ) ) ) )
18 17 ssrdv
 |-  ( B =/= (/) -> A C_ ran ( 1st |` ( A X. B ) ) )
19 frn
 |-  ( ( 1st |` ( A X. B ) ) : ( A X. B ) --> A -> ran ( 1st |` ( A X. B ) ) C_ A )
20 8 19 ax-mp
 |-  ran ( 1st |` ( A X. B ) ) C_ A
21 18 20 jctil
 |-  ( B =/= (/) -> ( ran ( 1st |` ( A X. B ) ) C_ A /\ A C_ ran ( 1st |` ( A X. B ) ) ) )
22 eqss
 |-  ( ran ( 1st |` ( A X. B ) ) = A <-> ( ran ( 1st |` ( A X. B ) ) C_ A /\ A C_ ran ( 1st |` ( A X. B ) ) ) )
23 21 22 sylibr
 |-  ( B =/= (/) -> ran ( 1st |` ( A X. B ) ) = A )
24 23 8 jctil
 |-  ( B =/= (/) -> ( ( 1st |` ( A X. B ) ) : ( A X. B ) --> A /\ ran ( 1st |` ( A X. B ) ) = A ) )
25 dffo2
 |-  ( ( 1st |` ( A X. B ) ) : ( A X. B ) -onto-> A <-> ( ( 1st |` ( A X. B ) ) : ( A X. B ) --> A /\ ran ( 1st |` ( A X. B ) ) = A ) )
26 24 25 sylibr
 |-  ( B =/= (/) -> ( 1st |` ( A X. B ) ) : ( A X. B ) -onto-> A )