Metamath Proof Explorer

Theorem hashxp

Description: The size of the Cartesian product of two finite sets is the product of their sizes. (Contributed by Paul Chapman, 30-Nov-2012)

Ref Expression
Assertion hashxp 
|- ( ( A e. Fin /\ B e. Fin ) -> ( # ` ( A X. B ) ) = ( ( # ` A ) x. ( # ` B ) ) )

Proof

Step Hyp Ref Expression
1 xpeq2 
 |-  ( B = if ( B e. Fin , B , (/) ) -> ( A X. B ) = ( A X. if ( B e. Fin , B , (/) ) ) )
2 1 fveq2d 
 |-  ( B = if ( B e. Fin , B , (/) ) -> ( # ` ( A X. B ) ) = ( # ` ( A X. if ( B e. Fin , B , (/) ) ) ) )
3 fveq2 
 |-  ( B = if ( B e. Fin , B , (/) ) -> ( # ` B ) = ( # ` if ( B e. Fin , B , (/) ) ) )
4 3 oveq2d 
 |-  ( B = if ( B e. Fin , B , (/) ) -> ( ( # ` A ) x. ( # ` B ) ) = ( ( # ` A ) x. ( # ` if ( B e. Fin , B , (/) ) ) ) )
5 2 4 eqeq12d 
 |-  ( B = if ( B e. Fin , B , (/) ) -> ( ( # ` ( A X. B ) ) = ( ( # ` A ) x. ( # ` B ) ) <-> ( # ` ( A X. if ( B e. Fin , B , (/) ) ) ) = ( ( # ` A ) x. ( # ` if ( B e. Fin , B , (/) ) ) ) ) )
6 5 imbi2d 
 |-  ( B = if ( B e. Fin , B , (/) ) -> ( ( A e. Fin -> ( # ` ( A X. B ) ) = ( ( # ` A ) x. ( # ` B ) ) ) <-> ( A e. Fin -> ( # ` ( A X. if ( B e. Fin , B , (/) ) ) ) = ( ( # ` A ) x. ( # ` if ( B e. Fin , B , (/) ) ) ) ) ) )
7 0fin 
 |-  (/) e. Fin
8 7 elimel 
 |-  if ( B e. Fin , B , (/) ) e. Fin
9 8 hashxplem 
 |-  ( A e. Fin -> ( # ` ( A X. if ( B e. Fin , B , (/) ) ) ) = ( ( # ` A ) x. ( # ` if ( B e. Fin , B , (/) ) ) ) )
10 6 9 dedth 
 |-  ( B e. Fin -> ( A e. Fin -> ( # ` ( A X. B ) ) = ( ( # ` A ) x. ( # ` B ) ) ) )
11 10 impcom 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( # ` ( A X. B ) ) = ( ( # ` A ) x. ( # ` B ) ) )