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

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 ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 xpeq2 ⊢ ( 𝐵 = if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) → ( 𝐴 × 𝐵 ) = ( 𝐴 × if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) ) )
2 1 fveq2d ⊢ ( 𝐵 = if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ♯ ‘ ( 𝐴 × if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) ) ) )
3 fveq2 ⊢ ( 𝐵 = if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) → ( ♯ ‘ 𝐵 ) = ( ♯ ‘ if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) ) )
4 3 oveq2d ⊢ ( 𝐵 = if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) → ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) ) ) )
5 2 4 eqeq12d ⊢ ( 𝐵 = if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) → ( ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ 𝐵 ) ) ↔ ( ♯ ‘ ( 𝐴 × if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) ) ) = ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) ) ) ) )
6 5 imbi2d ⊢ ( 𝐵 = if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) → ( ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ 𝐵 ) ) ) ↔ ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 × if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) ) ) = ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) ) ) ) ) )
7 0fi ⊢ ∅ ∈ Fin
8 7 elimel ⊢ if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) ∈ Fin
9 8 hashxplem ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 × if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) ) ) = ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ if ( 𝐵 ∈ Fin , 𝐵 , ∅ ) ) ) )
10 6 9 dedth ⊢ ( 𝐵 ∈ Fin → ( 𝐴 ∈ Fin → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ 𝐵 ) ) ) )
11 10 impcom ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ ( 𝐴 × 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) · ( ♯ ‘ 𝐵 ) ) )