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

Metamath Proof Explorer

Theorem fo2ndres

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

Ref Expression
Assertion fo2ndres 
|- ( A =/= (/) -> ( 2nd |` ( A X. B ) ) : ( A X. B ) -onto-> B )

Proof

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