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 )