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 ⊢ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 B ≈ A × B

Proof

Step Hyp Ref Expression
1 xpcomeng ⊢ A ∈ On ∧ B ∈ On → A × B ≈ B × A
2 xpexg ⊢ B ∈ On ∧ A ∈ On → B × A ∈ V
3 2 ancoms ⊢ A ∈ On ∧ B ∈ On → B × A ∈ V
4 omcl ⊢ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 B ∈ On
5 eqid ⊢ x ∈ B , y ∈ A ⟼ A ⋅ 𝑜 x + 𝑜 y = x ∈ B , y ∈ A ⟼ A ⋅ 𝑜 x + 𝑜 y
6 5 omxpenlem ⊢ A ∈ On ∧ B ∈ On → x ∈ B , y ∈ A ⟼ A ⋅ 𝑜 x + 𝑜 y : B × A ⟶ 1-1 onto A ⋅ 𝑜 B
7 f1oen2g ⊢ B × A ∈ V ∧ A ⋅ 𝑜 B ∈ On ∧ x ∈ B , y ∈ A ⟼ A ⋅ 𝑜 x + 𝑜 y : B × A ⟶ 1-1 onto A ⋅ 𝑜 B → B × A ≈ A ⋅ 𝑜 B
8 3 4 6 7 syl3anc ⊢ A ∈ On ∧ B ∈ On → B × A ≈ A ⋅ 𝑜 B
9 entr ⊢ A × B ≈ B × A ∧ B × A ≈ A ⋅ 𝑜 B → A × B ≈ A ⋅ 𝑜 B
10 1 8 9 syl2anc ⊢ A ∈ On ∧ B ∈ On → A × B ≈ A ⋅ 𝑜 B
11 10 ensymd ⊢ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 B ≈ A × B