Theorem infxpdom

Description: Dominance law for multiplication with an infinite cardinal. (Contributed by NM, 26-Mar-2006) (Revised by Mario Carneiro, 29-Apr-2015)

	Ref	Expression
Assertion	infxpdom	$$⊢\left(A\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq A\wedge B\preccurlyeq A\right)\to \left(A\times B\right)\preccurlyeq A$$

Proof

Step	Hyp	Ref	Expression
1		xpdom2g	$$⊢\left(A\in \mathrm{dom}\mathrm{card}\wedge B\preccurlyeq A\right)\to \left(A\times B\right)\preccurlyeq \left(A\times A\right)$$
2	1	3adant2	$$⊢\left(A\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq A\wedge B\preccurlyeq A\right)\to \left(A\times B\right)\preccurlyeq \left(A\times A\right)$$
3		infxpidm2	$$⊢\left(A\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq A\right)\to \left(A\times A\right)\approx A$$
4	3	3adant3	$$⊢\left(A\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq A\wedge B\preccurlyeq A\right)\to \left(A\times A\right)\approx A$$
5		domentr	$$⊢\left(\left(A\times B\right)\preccurlyeq \left(A\times A\right)\wedge \left(A\times A\right)\approx A\right)\to \left(A\times B\right)\preccurlyeq A$$
6	2 4 5	syl2anc	$$⊢\left(A\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq A\wedge B\preccurlyeq A\right)\to \left(A\times B\right)\preccurlyeq A$$