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 ) )