Theorem xpwf

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

	Ref	Expression
Assertion	xpwf	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( 𝐴 × 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) )

Proof

Step	Hyp	Ref	Expression
1		unwf	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) ↔ ( 𝐴 ∪ 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) )
2		pwwf	⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) ↔ 𝒫 ( 𝐴 ∪ 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) )
3		pwwf	⊢ ( 𝒫 ( 𝐴 ∪ 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) ↔ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) )
4	1 2 3	3bitri	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) ↔ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) )
5		xpsspw	⊢ ( 𝐴 × 𝐵 ) ⊆ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 )
6		sswf	⊢ ( ( 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) ∧ ( 𝐴 × 𝐵 ) ⊆ 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) ) → ( 𝐴 × 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) )
7	5 6	mpan2	⊢ ( 𝒫 𝒫 ( 𝐴 ∪ 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) → ( 𝐴 × 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) )
8	4 7	sylbi	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( 𝐴 × 𝐵 ) ∈ ∪ ( 𝑅1 “ On ) )