Metamath Proof Explorer

Theorem infxpabs

Description: Absorption law for multiplication with an infinite cardinal. (Contributed by NM, 30-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

		Ref	Expression
	Assertion	infxpabs	$⊢ ((A \in dom card \land ω ≼ A) \land (B \neq \emptyset \land B ≼ A)) \to (A \times B) \approx A$

Proof

Step	Hyp	Ref	Expression
1		infxpdom	$⊢ (A \in dom card \land ω ≼ A \land B ≼ A) \to (A \times B) ≼ A$
2	1	3expa	$⊢ ((A \in dom card \land ω ≼ A) \land B ≼ A) \to (A \times B) ≼ A$
3	2	adantrl	$⊢ ((A \in dom card \land ω ≼ A) \land (B \neq \emptyset \land B ≼ A)) \to (A \times B) ≼ A$
4		simpll	$⊢ ((A \in dom card \land ω ≼ A) \land (B \neq \emptyset \land B ≼ A)) \to A \in dom card$
5		numdom	$⊢ (A \in dom card \land B ≼ A) \to B \in dom card$
6	5	ad2ant2rl	$⊢ ((A \in dom card \land ω ≼ A) \land (B \neq \emptyset \land B ≼ A)) \to B \in dom card$
7		simprl	$⊢ ((A \in dom card \land ω ≼ A) \land (B \neq \emptyset \land B ≼ A)) \to B \neq \emptyset$
8		xpdom3	$⊢ (A \in dom card \land B \in dom card \land B \neq \emptyset) \to A ≼ (A \times B)$
9	4 6 7 8	syl3anc	$⊢ ((A \in dom card \land ω ≼ A) \land (B \neq \emptyset \land B ≼ A)) \to A ≼ (A \times B)$
10		sbth	$⊢ ((A \times B) ≼ A \land A ≼ (A \times B)) \to (A \times B) \approx A$
11	3 9 10	syl2anc	$⊢ ((A \in dom card \land ω ≼ A) \land (B \neq \emptyset \land B ≼ A)) \to (A \times B) \approx A$