This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )