Theorem xpcomeng

Description: Commutative law for equinumerosity of Cartesian product. Proposition 4.22(d) of Mendelson p. 254. (Contributed by NM, 27-Mar-2006)

	Ref	Expression
Assertion	xpcomeng	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\times B\right)\approx \left(B\times A\right)$$

Proof

Step	Hyp	Ref	Expression
1		xpeq1	$$⊢x=A\to x\times y=A\times y$$
2		xpeq2	$$⊢x=A\to y\times x=y\times A$$
3	1 2	breq12d	$$⊢x=A\to \left(\left(x\times y\right)\approx \left(y\times x\right)\leftrightarrow \left(A\times y\right)\approx \left(y\times A\right)\right)$$
4		xpeq2	$$⊢y=B\to A\times y=A\times B$$
5		xpeq1	$$⊢y=B\to y\times A=B\times A$$
6	4 5	breq12d	$$⊢y=B\to \left(\left(A\times y\right)\approx \left(y\times A\right)\leftrightarrow \left(A\times B\right)\approx \left(B\times A\right)\right)$$
7		vex	$$⊢x\in \mathrm{V}$$
8		vex	$$⊢y\in \mathrm{V}$$
9	7 8	xpcomen	$$⊢\left(x\times y\right)\approx \left(y\times x\right)$$
10	3 6 9	vtocl2g	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\times B\right)\approx \left(B\times A\right)$$