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 e. On /\ B e. On ) -> ( A .o B ) ~~ ( A X. B ) )

Proof

Step Hyp Ref Expression
1 xpcomeng
 |-  ( ( A e. On /\ B e. On ) -> ( A X. B ) ~~ ( B X. A ) )
2 xpexg
 |-  ( ( B e. On /\ A e. On ) -> ( B X. A ) e. _V )
3 2 ancoms
 |-  ( ( A e. On /\ B e. On ) -> ( B X. A ) e. _V )
4 omcl
 |-  ( ( A e. On /\ B e. On ) -> ( A .o B ) e. On )
5 eqid
 |-  ( x e. B , y e. A |-> ( ( A .o x ) +o y ) ) = ( x e. B , y e. A |-> ( ( A .o x ) +o y ) )
6 5 omxpenlem
 |-  ( ( A e. On /\ B e. On ) -> ( x e. B , y e. A |-> ( ( A .o x ) +o y ) ) : ( B X. A ) -1-1-onto-> ( A .o B ) )
7 f1oen2g
 |-  ( ( ( B X. A ) e. _V /\ ( A .o B ) e. On /\ ( x e. B , y e. A |-> ( ( A .o x ) +o y ) ) : ( B X. A ) -1-1-onto-> ( A .o B ) ) -> ( B X. A ) ~~ ( A .o B ) )
8 3 4 6 7 syl3anc
 |-  ( ( A e. On /\ B e. On ) -> ( B X. A ) ~~ ( A .o B ) )
9 entr
 |-  ( ( ( A X. B ) ~~ ( B X. A ) /\ ( B X. A ) ~~ ( A .o B ) ) -> ( A X. B ) ~~ ( A .o B ) )
10 1 8 9 syl2anc
 |-  ( ( A e. On /\ B e. On ) -> ( A X. B ) ~~ ( A .o B ) )
11 10 ensymd
 |-  ( ( A e. On /\ B e. On ) -> ( A .o B ) ~~ ( A X. B ) )