This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem omxpen

Description: The cardinal and ordinal products are always equinumerous. Exercise 10 of TakeutiZaring p. 89. (Contributed by Mario Carneiro, 3-Mar-2013)

Ref Expression
Assertion omxpen ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o 𝐵 ) ≈ ( 𝐴 × 𝐵 ) )

Proof

Step Hyp Ref Expression
1 xpcomeng ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐵 × 𝐴 ) )
2 xpexg ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐵 × 𝐴 ) ∈ V )
3 2 ancoms ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 × 𝐴 ) ∈ V )
4 omcl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o 𝐵 ) ∈ On )
5 eqid ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐴 ↦ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐴 ↦ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) )
6 5 omxpenlem ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐴 ↦ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ) : ( 𝐵 × 𝐴 ) –1-1-onto→ ( 𝐴 ·o 𝐵 ) )
7 f1oen2g ⊢ ( ( ( 𝐵 × 𝐴 ) ∈ V ∧ ( 𝐴 ·o 𝐵 ) ∈ On ∧ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐴 ↦ ( ( 𝐴 ·o 𝑥 ) +o 𝑦 ) ) : ( 𝐵 × 𝐴 ) –1-1-onto→ ( 𝐴 ·o 𝐵 ) ) → ( 𝐵 × 𝐴 ) ≈ ( 𝐴 ·o 𝐵 ) )
8 3 4 6 7 syl3anc ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 × 𝐴 ) ≈ ( 𝐴 ·o 𝐵 ) )
9 entr ⊢ ( ( ( 𝐴 × 𝐵 ) ≈ ( 𝐵 × 𝐴 ) ∧ ( 𝐵 × 𝐴 ) ≈ ( 𝐴 ·o 𝐵 ) ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐴 ·o 𝐵 ) )
10 1 8 9 syl2anc ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐴 ·o 𝐵 ) )
11 10 ensymd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o 𝐵 ) ≈ ( 𝐴 × 𝐵 ) )