infxp

Description: Absorption law for multiplication with an infinite cardinal. Equivalent to Proposition 10.41 of TakeutiZaring p. 95. (Contributed by NM, 28-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		sdomdom	$⊢ B ≺ A \to B ≼ A$
2		infxpabs	$⊢ ((A \in dom card \land ω ≼ A) \land (B \neq \emptyset \land B ≼ A)) \to (A \times B) \approx A$
3		infunabs	$⊢ (A \in dom card \land ω ≼ A \land B ≼ A) \to (A \cup B) \approx A$
4	3	3expa	$⊢ ((A \in dom card \land ω ≼ A) \land B ≼ A) \to (A \cup B) \approx A$
5	4	adantrl	$⊢ ((A \in dom card \land ω ≼ A) \land (B \neq \emptyset \land B ≼ A)) \to (A \cup B) \approx A$
6	5	ensymd	$⊢ ((A \in dom card \land ω ≼ A) \land (B \neq \emptyset \land B ≼ A)) \to A \approx (A \cup B)$
7		entr	$⊢ ((A \times B) \approx A \land A \approx (A \cup B)) \to (A \times B) \approx (A \cup B)$
8	2 6 7	syl2anc	$⊢ ((A \in dom card \land ω ≼ A) \land (B \neq \emptyset \land B ≼ A)) \to (A \times B) \approx (A \cup B)$
9	8	expr	$⊢ ((A \in dom card \land ω ≼ A) \land B \neq \emptyset) \to (B ≼ A \to (A \times B) \approx (A \cup B))$
10	9	adantrl	$⊢ ((A \in dom card \land ω ≼ A) \land (B \in dom card \land B \neq \emptyset)) \to (B ≼ A \to (A \times B) \approx (A \cup B))$
11	1 10	syl5	$⊢ ((A \in dom card \land ω ≼ A) \land (B \in dom card \land B \neq \emptyset)) \to (B ≺ A \to (A \times B) \approx (A \cup B))$
12		domtri2	$⊢ (A \in dom card \land B \in dom card) \to (A ≼ B \leftrightarrow \neg B ≺ A)$
13	12	ad2ant2r	$⊢ ((A \in dom card \land ω ≼ A) \land (B \in dom card \land B \neq \emptyset)) \to (A ≼ B \leftrightarrow \neg B ≺ A)$
14		xpcomeng	$⊢ (A \in dom card \land B \in dom card) \to (A \times B) \approx (B \times A)$
15	14	ad2ant2r	$⊢ ((A \in dom card \land ω ≼ A) \land (B \in dom card \land B \neq \emptyset)) \to (A \times B) \approx (B \times A)$
16		simplrl	$⊢ (((A \in dom card \land ω ≼ A) \land (B \in dom card \land B \neq \emptyset)) \land A ≼ B) \to B \in dom card$
17		domtr	$⊢ (ω ≼ A \land A ≼ B) \to ω ≼ B$
18	17	ad4ant24	$⊢ (((A \in dom card \land ω ≼ A) \land (B \in dom card \land B \neq \emptyset)) \land A ≼ B) \to ω ≼ B$
19		infn0	$⊢ ω ≼ A \to A \neq \emptyset$
20	19	ad3antlr	$⊢ (((A \in dom card \land ω ≼ A) \land (B \in dom card \land B \neq \emptyset)) \land A ≼ B) \to A \neq \emptyset$
21		simpr	$⊢ (((A \in dom card \land ω ≼ A) \land (B \in dom card \land B \neq \emptyset)) \land A ≼ B) \to A ≼ B$
22		infxpabs	$⊢ ((B \in dom card \land ω ≼ B) \land (A \neq \emptyset \land A ≼ B)) \to (B \times A) \approx B$
23	16 18 20 21 22	syl22anc	$⊢ (((A \in dom card \land ω ≼ A) \land (B \in dom card \land B \neq \emptyset)) \land A ≼ B) \to (B \times A) \approx B$
24		uncom	$⊢ A \cup B = B \cup A$
25		infunabs	$⊢ (B \in dom card \land ω ≼ B \land A ≼ B) \to (B \cup A) \approx B$
26	16 18 21 25	syl3anc	$⊢ (((A \in dom card \land ω ≼ A) \land (B \in dom card \land B \neq \emptyset)) \land A ≼ B) \to (B \cup A) \approx B$
27	24 26	eqbrtrid	$⊢ (((A \in dom card \land ω ≼ A) \land (B \in dom card \land B \neq \emptyset)) \land A ≼ B) \to (A \cup B) \approx B$
28	27	ensymd	$⊢ (((A \in dom card \land ω ≼ A) \land (B \in dom card \land B \neq \emptyset)) \land A ≼ B) \to B \approx (A \cup B)$
29		entr	$⊢ ((B \times A) \approx B \land B \approx (A \cup B)) \to (B \times A) \approx (A \cup B)$
30	23 28 29	syl2anc	$⊢ (((A \in dom card \land ω ≼ A) \land (B \in dom card \land B \neq \emptyset)) \land A ≼ B) \to (B \times A) \approx (A \cup B)$
31		entr	$⊢ ((A \times B) \approx (B \times A) \land (B \times A) \approx (A \cup B)) \to (A \times B) \approx (A \cup B)$
32	15 30 31	syl2an2r	$⊢ (((A \in dom card \land ω ≼ A) \land (B \in dom card \land B \neq \emptyset)) \land A ≼ B) \to (A \times B) \approx (A \cup B)$
33	32	ex	$⊢ ((A \in dom card \land ω ≼ A) \land (B \in dom card \land B \neq \emptyset)) \to (A ≼ B \to (A \times B) \approx (A \cup B))$
34	13 33	sylbird	$⊢ ((A \in dom card \land ω ≼ A) \land (B \in dom card \land B \neq \emptyset)) \to (\neg B ≺ A \to (A \times B) \approx (A \cup B))$
35	11 34	pm2.61d	$⊢ ((A \in dom card \land ω ≼ A) \land (B \in dom card \land B \neq \emptyset)) \to (A \times B) \approx (A \cup B)$

Metamath Proof Explorer

Theorem infxp

Proof