# Metamath Proof Explorer

## Theorem infxpidm2

Description: Every infinite well-orderable set is equinumerous to its Cartesian square. This theorem provides the basis for infinite cardinal arithmetic. Proposition 10.40 of TakeutiZaring p. 95. See also infxpidm . (Contributed by Mario Carneiro, 9-Mar-2013) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion infxpidm2 ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {A}\right)\to \left({A}×{A}\right)\approx {A}$

### Proof

Step Hyp Ref Expression
1 cardid2 ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left({A}\right)\approx {A}$
2 1 ensymd ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to {A}\approx \mathrm{card}\left({A}\right)$
3 xpen ${⊢}\left({A}\approx \mathrm{card}\left({A}\right)\wedge {A}\approx \mathrm{card}\left({A}\right)\right)\to \left({A}×{A}\right)\approx \left(\mathrm{card}\left({A}\right)×\mathrm{card}\left({A}\right)\right)$
4 2 2 3 syl2anc ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \left({A}×{A}\right)\approx \left(\mathrm{card}\left({A}\right)×\mathrm{card}\left({A}\right)\right)$
5 4 adantr ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {A}\right)\to \left({A}×{A}\right)\approx \left(\mathrm{card}\left({A}\right)×\mathrm{card}\left({A}\right)\right)$
6 cardon ${⊢}\mathrm{card}\left({A}\right)\in \mathrm{On}$
7 cardom ${⊢}\mathrm{card}\left(\mathrm{\omega }\right)=\mathrm{\omega }$
8 omelon ${⊢}\mathrm{\omega }\in \mathrm{On}$
9 onenon ${⊢}\mathrm{\omega }\in \mathrm{On}\to \mathrm{\omega }\in \mathrm{dom}\mathrm{card}$
10 8 9 ax-mp ${⊢}\mathrm{\omega }\in \mathrm{dom}\mathrm{card}$
11 carddom2 ${⊢}\left(\mathrm{\omega }\in \mathrm{dom}\mathrm{card}\wedge {A}\in \mathrm{dom}\mathrm{card}\right)\to \left(\mathrm{card}\left(\mathrm{\omega }\right)\subseteq \mathrm{card}\left({A}\right)↔\mathrm{\omega }\preccurlyeq {A}\right)$
12 10 11 mpan ${⊢}{A}\in \mathrm{dom}\mathrm{card}\to \left(\mathrm{card}\left(\mathrm{\omega }\right)\subseteq \mathrm{card}\left({A}\right)↔\mathrm{\omega }\preccurlyeq {A}\right)$
13 12 biimpar ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {A}\right)\to \mathrm{card}\left(\mathrm{\omega }\right)\subseteq \mathrm{card}\left({A}\right)$
14 7 13 eqsstrrid ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {A}\right)\to \mathrm{\omega }\subseteq \mathrm{card}\left({A}\right)$
15 infxpen ${⊢}\left(\mathrm{card}\left({A}\right)\in \mathrm{On}\wedge \mathrm{\omega }\subseteq \mathrm{card}\left({A}\right)\right)\to \left(\mathrm{card}\left({A}\right)×\mathrm{card}\left({A}\right)\right)\approx \mathrm{card}\left({A}\right)$
16 6 14 15 sylancr ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {A}\right)\to \left(\mathrm{card}\left({A}\right)×\mathrm{card}\left({A}\right)\right)\approx \mathrm{card}\left({A}\right)$
17 entr ${⊢}\left(\left({A}×{A}\right)\approx \left(\mathrm{card}\left({A}\right)×\mathrm{card}\left({A}\right)\right)\wedge \left(\mathrm{card}\left({A}\right)×\mathrm{card}\left({A}\right)\right)\approx \mathrm{card}\left({A}\right)\right)\to \left({A}×{A}\right)\approx \mathrm{card}\left({A}\right)$
18 5 16 17 syl2anc ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {A}\right)\to \left({A}×{A}\right)\approx \mathrm{card}\left({A}\right)$
19 1 adantr ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {A}\right)\to \mathrm{card}\left({A}\right)\approx {A}$
20 entr ${⊢}\left(\left({A}×{A}\right)\approx \mathrm{card}\left({A}\right)\wedge \mathrm{card}\left({A}\right)\approx {A}\right)\to \left({A}×{A}\right)\approx {A}$
21 18 19 20 syl2anc ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {A}\right)\to \left({A}×{A}\right)\approx {A}$