xpwf

Description: The Cartesian product of two well-founded sets is well-founded. (Contributed by Eric Schmidt, 12-Sep-2025)

		Ref	Expression
	Assertion	xpwf	$⊢ (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On]) \to A \times B \in ⋃ R_{1} [On]$

Step	Hyp	Ref	Expression
1		unwf	$⊢ (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On]) \leftrightarrow A \cup B \in ⋃ R_{1} [On]$
2		pwwf	$⊢ A \cup B \in ⋃ R_{1} [On] \leftrightarrow 𝒫 (A \cup B) \in ⋃ R_{1} [On]$
3		pwwf	$⊢ 𝒫 (A \cup B) \in ⋃ R_{1} [On] \leftrightarrow 𝒫 𝒫 (A \cup B) \in ⋃ R_{1} [On]$
4	1 2 3	3bitri	$⊢ (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On]) \leftrightarrow 𝒫 𝒫 (A \cup B) \in ⋃ R_{1} [On]$
5		xpsspw	$⊢ A \times B \subseteq 𝒫 𝒫 (A \cup B)$
6		sswf	$⊢ (𝒫 𝒫 (A \cup B) \in ⋃ R_{1} [On] \land A \times B \subseteq 𝒫 𝒫 (A \cup B)) \to A \times B \in ⋃ R_{1} [On]$
7	5 6	mpan2	$⊢ 𝒫 𝒫 (A \cup B) \in ⋃ R_{1} [On] \to A \times B \in ⋃ R_{1} [On]$
8	4 7	sylbi	$⊢ (A \in ⋃ R_{1} [On] \land B \in ⋃ R_{1} [On]) \to A \times B \in ⋃ R_{1} [On]$

Metamath Proof Explorer