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\times 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\times A\right)\approx \left(\mathrm{card}\left(A\right)\times \mathrm{card}\left(A\right)\right)$$
4	2 2 3	syl2anc	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left(A\times A\right)\approx \left(\mathrm{card}\left(A\right)\times \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\times A\right)\approx \left(\mathrm{card}\left(A\right)\times \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)\leftrightarrow \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)\leftrightarrow \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)\times \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)\times \mathrm{card}\left(A\right)\right)\approx \mathrm{card}\left(A\right)$$
17		entr	$$⊢\left(\left(A\times A\right)\approx \left(\mathrm{card}\left(A\right)\times \mathrm{card}\left(A\right)\right)\wedge \left(\mathrm{card}\left(A\right)\times \mathrm{card}\left(A\right)\right)\approx \mathrm{card}\left(A\right)\right)\to \left(A\times 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\times 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\times A\right)\approx \mathrm{card}\left(A\right)\wedge \mathrm{card}\left(A\right)\approx A\right)\to \left(A\times 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\times A\right)\approx A$$