This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Union Equinumerosity 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 ⊢ ( 𝐴 × 𝐵 ) ≈ ( 𝐵 × 𝐴 )