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 𝐵 ) ≈ ( 𝐴 × 𝐵 ) )