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	⊢ 𝐴 ∈ V
	xpcomen.2	⊢ 𝐵 ∈ V
Assertion	xpcomen	⊢ ( 𝐴 × 𝐵 ) ≈ ( 𝐵 × 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		xpcomen.1	⊢ 𝐴 ∈ V
2		xpcomen.2	⊢ 𝐵 ∈ V
3	1 2	xpex	⊢ ( 𝐴 × 𝐵 ) ∈ V
4	2 1	xpex	⊢ ( 𝐵 × 𝐴 ) ∈ V
5		eqid	⊢ ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ ∪ ◡ { 𝑥 } ) = ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ ∪ ◡ { 𝑥 } )
6	5	xpcomf1o	⊢ ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ ∪ ◡ { 𝑥 } ) : ( 𝐴 × 𝐵 ) –1-1-onto→ ( 𝐵 × 𝐴 )
7		f1oen2g	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ V ∧ ( 𝐵 × 𝐴 ) ∈ V ∧ ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↦ ∪ ◡ { 𝑥 } ) : ( 𝐴 × 𝐵 ) –1-1-onto→ ( 𝐵 × 𝐴 ) ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐵 × 𝐴 ) )
8	3 4 6 7	mp3an	⊢ ( 𝐴 × 𝐵 ) ≈ ( 𝐵 × 𝐴 )