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=ifB∈FinB∅→A×B=A×ifB∈FinB∅
2 1 fveq2d ⊢B=ifB∈FinB∅→A×B=A×ifB∈FinB∅
3 fveq2 ⊢B=ifB∈FinB∅→B=ifB∈FinB∅
4 3 oveq2d ⊢B=ifB∈FinB∅→A⁢B=A⁢ifB∈FinB∅
5 2 4 eqeq12d ⊢B=ifB∈FinB∅→A×B=A⁢B↔A×ifB∈FinB∅=A⁢ifB∈FinB∅
6 5 imbi2d ⊢B=ifB∈FinB∅→A∈Fin→A×B=A⁢B↔A∈Fin→A×ifB∈FinB∅=A⁢ifB∈FinB∅
7 0fin ⊢∅∈Fin
8 7 elimel ⊢ifB∈FinB∅∈Fin
9 8 hashxplem ⊢A∈Fin→A×ifB∈FinB∅=A⁢ifB∈FinB∅
10 6 9 dedth ⊢B∈Fin→A∈Fin→A×B=A⁢B
11 10 impcom ⊢A∈Fin∧B∈Fin→A×B=A⁢B