Theorem xpcomen

Description: Commutative law for equinumerosity of Cartesian product. Proposition 4.22(d) of Mendelson p. 254. (Contributed by NM, 5-Jan-2004) (Revised by Mario Carneiro, 15-Nov-2014)

	Ref	Expression
Hypotheses	xpcomen.1	|- A e. _V
	xpcomen.2	|- B e. _V
Assertion	xpcomen	|- ( A X. B ) ~~ ( B X. A )

Proof

Step	Hyp	Ref	Expression
1		xpcomen.1	|- A e. _V
2		xpcomen.2	|- B e. _V
3	1 2	xpex	|- ( A X. B ) e. _V
4	2 1	xpex	|- ( B X. A ) e. _V
5		eqid	|- ( x e. ( A X. B ) |-> U. `' { x } ) = ( x e. ( A X. B ) |-> U. `' { x } )
6	5	xpcomf1o	|- ( x e. ( A X. B ) |-> U. `' { x } ) : ( A X. B ) -1-1-onto-> ( B X. A )
7		f1oen2g	|- ( ( ( A X. B ) e. _V /\ ( B X. A ) e. _V /\ ( x e. ( A X. B ) |-> U. `' { x } ) : ( A X. B ) -1-1-onto-> ( B X. A ) ) -> ( A X. B ) ~~ ( B X. A ) )
8	3 4 6 7	mp3an	|- ( A X. B ) ~~ ( B X. A )