Metamath Proof Explorer

Theorem xp2nd

Description: Location of the second element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion xp2nd 
|- ( A e. ( B X. C ) -> ( 2nd ` A ) e. C )

Proof

Step Hyp Ref Expression
1 elxp 
 |-  ( A e. ( B X. C ) <-> E. b E. c ( A = <. b , c >. /\ ( b e. B /\ c e. C ) ) )
2 vex 
 |-  b e. _V
3 vex 
 |-  c e. _V
4 2 3 op2ndd 
 |-  ( A = <. b , c >. -> ( 2nd ` A ) = c )
5 4 eleq1d 
 |-  ( A = <. b , c >. -> ( ( 2nd ` A ) e. C <-> c e. C ) )
6 5 biimpar 
 |-  ( ( A = <. b , c >. /\ c e. C ) -> ( 2nd ` A ) e. C )
7 6 adantrl 
 |-  ( ( A = <. b , c >. /\ ( b e. B /\ c e. C ) ) -> ( 2nd ` A ) e. C )
8 7 exlimivv 
 |-  ( E. b E. c ( A = <. b , c >. /\ ( b e. B /\ c e. C ) ) -> ( 2nd ` A ) e. C )
9 1 8 sylbi 
 |-  ( A e. ( B X. C ) -> ( 2nd ` A ) e. C )