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

Metamath Proof Explorer

Theorem 2ndimaxp

Description: Image of a cartesian product by 2nd . (Contributed by Thierry Arnoux, 23-Jun-2024)

Ref Expression
Assertion 2ndimaxp 
|- ( A =/= (/) -> ( 2nd " ( A X. B ) ) = B )

Proof

Step Hyp Ref Expression
1 ima0 
 |-  ( 2nd " (/) ) = (/)
2 xpeq2 
 |-  ( B = (/) -> ( A X. B ) = ( A X. (/) ) )
3 xp0 
 |-  ( A X. (/) ) = (/)
4 2 3 eqtrdi 
 |-  ( B = (/) -> ( A X. B ) = (/) )
5 4 imaeq2d 
 |-  ( B = (/) -> ( 2nd " ( A X. B ) ) = ( 2nd " (/) ) )
6 id 
 |-  ( B = (/) -> B = (/) )
7 1 5 6 3eqtr4a 
 |-  ( B = (/) -> ( 2nd " ( A X. B ) ) = B )
8 7 adantl 
 |-  ( ( A =/= (/) /\ B = (/) ) -> ( 2nd " ( A X. B ) ) = B )
9 xpnz 
 |-  ( ( A =/= (/) /\ B =/= (/) ) <-> ( A X. B ) =/= (/) )
10 fo2nd 
 |-  2nd : _V -onto-> _V
11 fofn 
 |-  ( 2nd : _V -onto-> _V -> 2nd Fn _V )
12 10 11 mp1i 
 |-  ( ( A X. B ) =/= (/) -> 2nd Fn _V )
13 ssv 
 |-  ( A X. B ) C_ _V
14 13 a1i 
 |-  ( ( A X. B ) =/= (/) -> ( A X. B ) C_ _V )
15 12 14 fvelimabd 
 |-  ( ( A X. B ) =/= (/) -> ( y e. ( 2nd " ( A X. B ) ) <-> E. p e. ( A X. B ) ( 2nd ` p ) = y ) )
16 9 15 sylbi 
 |-  ( ( A =/= (/) /\ B =/= (/) ) -> ( y e. ( 2nd " ( A X. B ) ) <-> E. p e. ( A X. B ) ( 2nd ` p ) = y ) )
17 simpr 
 |-  ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ p e. ( A X. B ) ) /\ ( 2nd ` p ) = y ) -> ( 2nd ` p ) = y )
18 xp2nd 
 |-  ( p e. ( A X. B ) -> ( 2nd ` p ) e. B )
19 18 ad2antlr 
 |-  ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ p e. ( A X. B ) ) /\ ( 2nd ` p ) = y ) -> ( 2nd ` p ) e. B )
20 17 19 eqeltrrd 
 |-  ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ p e. ( A X. B ) ) /\ ( 2nd ` p ) = y ) -> y e. B )
21 20 r19.29an 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ E. p e. ( A X. B ) ( 2nd ` p ) = y ) -> y e. B )
22 n0 
 |-  ( A =/= (/) <-> E. x x e. A )
23 22 biimpi 
 |-  ( A =/= (/) -> E. x x e. A )
24 23 ad2antrr 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ y e. B ) -> E. x x e. A )
25 opelxpi 
 |-  ( ( x e. A /\ y e. B ) -> <. x , y >. e. ( A X. B ) )
26 25 ancoms 
 |-  ( ( y e. B /\ x e. A ) -> <. x , y >. e. ( A X. B ) )
27 26 adantll 
 |-  ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ y e. B ) /\ x e. A ) -> <. x , y >. e. ( A X. B ) )
28 fveqeq2 
 |-  ( p = <. x , y >. -> ( ( 2nd ` p ) = y <-> ( 2nd ` <. x , y >. ) = y ) )
29 28 adantl 
 |-  ( ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ y e. B ) /\ x e. A ) /\ p = <. x , y >. ) -> ( ( 2nd ` p ) = y <-> ( 2nd ` <. x , y >. ) = y ) )
30 vex 
 |-  x e. _V
31 vex 
 |-  y e. _V
32 30 31 op2nd 
 |-  ( 2nd ` <. x , y >. ) = y
33 32 a1i 
 |-  ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ y e. B ) /\ x e. A ) -> ( 2nd ` <. x , y >. ) = y )
34 27 29 33 rspcedvd 
 |-  ( ( ( ( A =/= (/) /\ B =/= (/) ) /\ y e. B ) /\ x e. A ) -> E. p e. ( A X. B ) ( 2nd ` p ) = y )
35 24 34 exlimddv 
 |-  ( ( ( A =/= (/) /\ B =/= (/) ) /\ y e. B ) -> E. p e. ( A X. B ) ( 2nd ` p ) = y )
36 21 35 impbida 
 |-  ( ( A =/= (/) /\ B =/= (/) ) -> ( E. p e. ( A X. B ) ( 2nd ` p ) = y <-> y e. B ) )
37 16 36 bitrd 
 |-  ( ( A =/= (/) /\ B =/= (/) ) -> ( y e. ( 2nd " ( A X. B ) ) <-> y e. B ) )
38 37 eqrdv 
 |-  ( ( A =/= (/) /\ B =/= (/) ) -> ( 2nd " ( A X. B ) ) = B )
39 8 38 pm2.61dane 
 |-  ( A =/= (/) -> ( 2nd " ( A X. B ) ) = B )