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 ∈ Fin ∧ B ∈ Fin → A × B = A ⁢ B

Proof

Step Hyp Ref Expression
1 xpeq2 ⊢ B = if B ∈ Fin B ∅ → A × B = A × if B ∈ Fin B ∅
2 1 fveq2d ⊢ B = if B ∈ Fin B ∅ → A × B = A × if B ∈ Fin B ∅
3 fveq2 ⊢ B = if B ∈ Fin B ∅ → B = if B ∈ Fin B ∅
4 3 oveq2d ⊢ B = if B ∈ Fin B ∅ → A ⁢ B = A ⁢ if B ∈ Fin B ∅
5 2 4 eqeq12d ⊢ B = if B ∈ Fin B ∅ → A × B = A ⁢ B ↔ A × if B ∈ Fin B ∅ = A ⁢ if B ∈ Fin B ∅
6 5 imbi2d ⊢ B = if B ∈ Fin B ∅ → A ∈ Fin → A × B = A ⁢ B ↔ A ∈ Fin → A × if B ∈ Fin B ∅ = A ⁢ if B ∈ Fin B ∅
7 0fin ⊢ ∅ ∈ Fin
8 7 elimel ⊢ if B ∈ Fin B ∅ ∈ Fin
9 8 hashxplem ⊢ A ∈ Fin → A × if B ∈ Fin B ∅ = A ⁢ if B ∈ Fin B ∅
10 6 9 dedth ⊢ B ∈ Fin → A ∈ Fin → A × B = A ⁢ B
11 10 impcom ⊢ A ∈ Fin ∧ B ∈ Fin → A × B = A ⁢ B