Metamath Proof Explorer

Theorem fprodcom

Description: Interchange product order. (Contributed by Scott Fenton, 2-Feb-2018)

	Ref	Expression
Hypotheses	fprodcom.1	$⊢ φ \to A \in Fin$
	fprodcom.2	$⊢ φ \to B \in Fin$
	fprodcom.3	$⊢ (φ \land (j \in A \land k \in B)) \to C \in ℂ$
Assertion	fprodcom	$⊢ φ \to \prod_{j \in A} \prod_{k \in B} C = \prod_{k \in B} \prod_{j \in A} C$

Step	Hyp	Ref	Expression
1		fprodcom.1	$⊢ φ \to A \in Fin$
2		fprodcom.2	$⊢ φ \to B \in Fin$
3		fprodcom.3	$⊢ (φ \land (j \in A \land k \in B)) \to C \in ℂ$
4	2	adantr	$⊢ (φ \land j \in A) \to B \in Fin$
5		ancom	$⊢ (j \in A \land k \in B) \leftrightarrow (k \in B \land j \in A)$
6	5	a1i	$⊢ φ \to ((j \in A \land k \in B) \leftrightarrow (k \in B \land j \in A))$
7	1 2 4 6 3	fprodcom2	$⊢ φ \to \prod_{j \in A} \prod_{k \in B} C = \prod_{k \in B} \prod_{j \in A} C$