# Metamath Proof Explorer

## 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}×{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}×{B}\right)\preccurlyeq \left({A}×{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}×{B}\right)\preccurlyeq \left({A}×{A}\right)$
3 infxpidm2 ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {A}\right)\to \left({A}×{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}×{A}\right)\approx {A}$
5 domentr ${⊢}\left(\left({A}×{B}\right)\preccurlyeq \left({A}×{A}\right)\wedge \left({A}×{A}\right)\approx {A}\right)\to \left({A}×{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}×{B}\right)\preccurlyeq {A}$