Metamath Proof Explorer

Theorem 2ndconst

Description: The mapping of a restriction of the 2nd function to a converse constant function. (Contributed by NM, 27-Mar-2008) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion 2ndconst 
|- ( A e. V -> ( 2nd |` ( { A } X. B ) ) : ( { A } X. B ) -1-1-onto-> B )

Proof

Step Hyp Ref Expression
1 snnzg 
 |-  ( A e. V -> { A } =/= (/) )
2 fo2ndres 
 |-  ( { A } =/= (/) -> ( 2nd |` ( { A } X. B ) ) : ( { A } X. B ) -onto-> B )
3 1 2 syl 
 |-  ( A e. V -> ( 2nd |` ( { A } X. B ) ) : ( { A } X. B ) -onto-> B )
4 moeq 
 |-  E* x x = <. A , y >.
5 4 moani 
 |-  E* x ( y e. B /\ x = <. A , y >. )
6 vex 
 |-  y e. _V
7 6 brresi 
 |-  ( x ( 2nd |` ( { A } X. B ) ) y <-> ( x e. ( { A } X. B ) /\ x 2nd y ) )
8 fo2nd 
 |-  2nd : _V -onto-> _V
9 fofn 
 |-  ( 2nd : _V -onto-> _V -> 2nd Fn _V )
10 8 9 ax-mp 
 |-  2nd Fn _V
11 vex 
 |-  x e. _V
12 fnbrfvb 
 |-  ( ( 2nd Fn _V /\ x e. _V ) -> ( ( 2nd ` x ) = y <-> x 2nd y ) )
13 10 11 12 mp2an 
 |-  ( ( 2nd ` x ) = y <-> x 2nd y )
14 13 anbi2i 
 |-  ( ( x e. ( { A } X. B ) /\ ( 2nd ` x ) = y ) <-> ( x e. ( { A } X. B ) /\ x 2nd y ) )
15 elxp7 
 |-  ( x e. ( { A } X. B ) <-> ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. { A } /\ ( 2nd ` x ) e. B ) ) )
16 eleq1 
 |-  ( ( 2nd ` x ) = y -> ( ( 2nd ` x ) e. B <-> y e. B ) )
17 16 biimpac 
 |-  ( ( ( 2nd ` x ) e. B /\ ( 2nd ` x ) = y ) -> y e. B )
18 17 adantll 
 |-  ( ( ( ( 1st ` x ) e. { A } /\ ( 2nd ` x ) e. B ) /\ ( 2nd ` x ) = y ) -> y e. B )
19 18 adantll 
 |-  ( ( ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. { A } /\ ( 2nd ` x ) e. B ) ) /\ ( 2nd ` x ) = y ) -> y e. B )
20 elsni 
 |-  ( ( 1st ` x ) e. { A } -> ( 1st ` x ) = A )
21 eqopi 
 |-  ( ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) = A /\ ( 2nd ` x ) = y ) ) -> x = <. A , y >. )
22 21 anassrs 
 |-  ( ( ( x e. ( _V X. _V ) /\ ( 1st ` x ) = A ) /\ ( 2nd ` x ) = y ) -> x = <. A , y >. )
23 20 22 sylanl2 
 |-  ( ( ( x e. ( _V X. _V ) /\ ( 1st ` x ) e. { A } ) /\ ( 2nd ` x ) = y ) -> x = <. A , y >. )
24 23 adantlrr 
 |-  ( ( ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. { A } /\ ( 2nd ` x ) e. B ) ) /\ ( 2nd ` x ) = y ) -> x = <. A , y >. )
25 19 24 jca 
 |-  ( ( ( x e. ( _V X. _V ) /\ ( ( 1st ` x ) e. { A } /\ ( 2nd ` x ) e. B ) ) /\ ( 2nd ` x ) = y ) -> ( y e. B /\ x = <. A , y >. ) )
26 15 25 sylanb 
 |-  ( ( x e. ( { A } X. B ) /\ ( 2nd ` x ) = y ) -> ( y e. B /\ x = <. A , y >. ) )
27 26 adantl 
 |-  ( ( A e. V /\ ( x e. ( { A } X. B ) /\ ( 2nd ` x ) = y ) ) -> ( y e. B /\ x = <. A , y >. ) )
28 simprr 
 |-  ( ( A e. V /\ ( y e. B /\ x = <. A , y >. ) ) -> x = <. A , y >. )
29 snidg 
 |-  ( A e. V -> A e. { A } )
30 29 adantr 
 |-  ( ( A e. V /\ ( y e. B /\ x = <. A , y >. ) ) -> A e. { A } )
31 simprl 
 |-  ( ( A e. V /\ ( y e. B /\ x = <. A , y >. ) ) -> y e. B )
32 30 31 opelxpd 
 |-  ( ( A e. V /\ ( y e. B /\ x = <. A , y >. ) ) -> <. A , y >. e. ( { A } X. B ) )
33 28 32 eqeltrd 
 |-  ( ( A e. V /\ ( y e. B /\ x = <. A , y >. ) ) -> x e. ( { A } X. B ) )
34 fveq2 
 |-  ( x = <. A , y >. -> ( 2nd ` x ) = ( 2nd ` <. A , y >. ) )
35 op2ndg 
 |-  ( ( A e. V /\ y e. _V ) -> ( 2nd ` <. A , y >. ) = y )
36 35 elvd 
 |-  ( A e. V -> ( 2nd ` <. A , y >. ) = y )
37 34 36 sylan9eqr 
 |-  ( ( A e. V /\ x = <. A , y >. ) -> ( 2nd ` x ) = y )
38 37 adantrl 
 |-  ( ( A e. V /\ ( y e. B /\ x = <. A , y >. ) ) -> ( 2nd ` x ) = y )
39 33 38 jca 
 |-  ( ( A e. V /\ ( y e. B /\ x = <. A , y >. ) ) -> ( x e. ( { A } X. B ) /\ ( 2nd ` x ) = y ) )
40 27 39 impbida 
 |-  ( A e. V -> ( ( x e. ( { A } X. B ) /\ ( 2nd ` x ) = y ) <-> ( y e. B /\ x = <. A , y >. ) ) )
41 14 40 bitr3id 
 |-  ( A e. V -> ( ( x e. ( { A } X. B ) /\ x 2nd y ) <-> ( y e. B /\ x = <. A , y >. ) ) )
42 7 41 syl5bb 
 |-  ( A e. V -> ( x ( 2nd |` ( { A } X. B ) ) y <-> ( y e. B /\ x = <. A , y >. ) ) )
43 42 mobidv 
 |-  ( A e. V -> ( E* x x ( 2nd |` ( { A } X. B ) ) y <-> E* x ( y e. B /\ x = <. A , y >. ) ) )
44 5 43 mpbiri 
 |-  ( A e. V -> E* x x ( 2nd |` ( { A } X. B ) ) y )
45 44 alrimiv 
 |-  ( A e. V -> A. y E* x x ( 2nd |` ( { A } X. B ) ) y )
46 funcnv2 
 |-  ( Fun `' ( 2nd |` ( { A } X. B ) ) <-> A. y E* x x ( 2nd |` ( { A } X. B ) ) y )
47 45 46 sylibr 
 |-  ( A e. V -> Fun `' ( 2nd |` ( { A } X. B ) ) )
48 dff1o3 
 |-  ( ( 2nd |` ( { A } X. B ) ) : ( { A } X. B ) -1-1-onto-> B <-> ( ( 2nd |` ( { A } X. B ) ) : ( { A } X. B ) -onto-> B /\ Fun `' ( 2nd |` ( { A } X. B ) ) ) )
49 3 47 48 sylanbrc 
 |-  ( A e. V -> ( 2nd |` ( { A } X. B ) ) : ( { A } X. B ) -1-1-onto-> B )