Theorem xpexb

Description: A Cartesian product exists iff its converse does. Corollary 6.9(1) in TakeutiZaring p. 26. (Contributed by Andrew Salmon, 13-Nov-2011)

	Ref	Expression
Assertion	xpexb	$$⊢A\times B\in \mathrm{V}\leftrightarrow B\times A\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		cnvxp	$$⊢{\left(A\times B\right)}^{-1}=B\times A$$
2		cnvexg	$$⊢A\times B\in \mathrm{V}\to {\left(A\times B\right)}^{-1}\in \mathrm{V}$$
3	1 2	eqeltrrid	$$⊢A\times B\in \mathrm{V}\to B\times A\in \mathrm{V}$$
4		cnvxp	$$⊢{\left(B\times A\right)}^{-1}=A\times B$$
5		cnvexg	$$⊢B\times A\in \mathrm{V}\to {\left(B\times A\right)}^{-1}\in \mathrm{V}$$
6	4 5	eqeltrrid	$$⊢B\times A\in \mathrm{V}\to A\times B\in \mathrm{V}$$
7	3 6	impbii	$$⊢A\times B\in \mathrm{V}\leftrightarrow B\times A\in \mathrm{V}$$