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 ๐ต ) โ‰ˆ ( ๐ด ร— ๐ต ) )