Metamath Proof Explorer

Theorem omxpen

Description: The cardinal and ordinal products are always equinumerous. Exercise 10 of TakeutiZaring p. 89. (Contributed by Mario Carneiro, 3-Mar-2013)

		Ref	Expression
	Assertion	omxpen	$⊢ (A \in On \land B \in On) \to (A \cdot_{𝑜} B) \approx (A \times B)$

Proof

Step	Hyp	Ref	Expression
1		xpcomeng	$⊢ (A \in On \land B \in On) \to (A \times B) \approx (B \times A)$
2		xpexg	$⊢ (B \in On \land A \in On) \to B \times A \in V$
3	2	ancoms	$⊢ (A \in On \land B \in On) \to B \times A \in V$
4		omcl	$⊢ (A \in On \land B \in On) \to A \cdot_{𝑜} B \in On$
5		eqid	$⊢ (x \in B, y \in A ⟼ (A \cdot_{𝑜} x) +_{𝑜} y) = (x \in B, y \in A ⟼ (A \cdot_{𝑜} x) +_{𝑜} y)$
6	5	omxpenlem	$⊢ (A \in On \land B \in On) \to (x \in B, y \in A ⟼ (A \cdot_{𝑜} x) +_{𝑜} y) : B \times A \underset{1-1 onto}{⟶} A \cdot_{𝑜} B$
7		f1oen2g	$⊢ (B \times A \in V \land A \cdot_{𝑜} B \in On \land (x \in B, y \in A ⟼ (A \cdot_{𝑜} x) +_{𝑜} y) : B \times A \underset{1-1 onto}{⟶} A \cdot_{𝑜} B) \to (B \times A) \approx (A \cdot_{𝑜} B)$
8	3 4 6 7	syl3anc	$⊢ (A \in On \land B \in On) \to (B \times A) \approx (A \cdot_{𝑜} B)$
9		entr	$⊢ ((A \times B) \approx (B \times A) \land (B \times A) \approx (A \cdot_{𝑜} B)) \to (A \times B) \approx (A \cdot_{𝑜} B)$
10	1 8 9	syl2anc	$⊢ (A \in On \land B \in On) \to (A \times B) \approx (A \cdot_{𝑜} B)$
11	10	ensymd	$⊢ (A \in On \land B \in On) \to (A \cdot_{𝑜} B) \approx (A \times B)$