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	$⊢ (A \in dom card \land ω ≼ A \land B ≼ A) \to (A \times B) ≼ A$

Proof

Step	Hyp	Ref	Expression
1		xpdom2g	$⊢ (A \in dom card \land B ≼ A) \to (A \times B) ≼ (A \times A)$
2	1	3adant2	$⊢ (A \in dom card \land ω ≼ A \land B ≼ A) \to (A \times B) ≼ (A \times A)$
3		infxpidm2	$⊢ (A \in dom card \land ω ≼ A) \to (A \times A) \approx A$
4	3	3adant3	$⊢ (A \in dom card \land ω ≼ A \land B ≼ A) \to (A \times A) \approx A$
5		domentr	$⊢ ((A \times B) ≼ (A \times A) \land (A \times A) \approx A) \to (A \times B) ≼ A$
6	2 4 5	syl2anc	$⊢ (A \in dom card \land ω ≼ A \land B ≼ A) \to (A \times B) ≼ A$

Metamath Proof Explorer

Theorem infxpdom

Proof