Metamath Proof Explorer

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 
|- ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( A X. B ) e. U. ( R1 " On ) )

Proof

Step Hyp Ref Expression
1 unwf 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) <-> ( A u. B ) e. U. ( R1 " On ) )
2 pwwf 
 |-  ( ( A u. B ) e. U. ( R1 " On ) <-> ~P ( A u. B ) e. U. ( R1 " On ) )
3 pwwf 
 |-  ( ~P ( A u. B ) e. U. ( R1 " On ) <-> ~P ~P ( A u. B ) e. U. ( R1 " On ) )
4 1 2 3 3bitri 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) <-> ~P ~P ( A u. B ) e. U. ( R1 " On ) )
5 xpsspw 
 |-  ( A X. B ) C_ ~P ~P ( A u. B )
6 sswf 
 |-  ( ( ~P ~P ( A u. B ) e. U. ( R1 " On ) /\ ( A X. B ) C_ ~P ~P ( A u. B ) ) -> ( A X. B ) e. U. ( R1 " On ) )
7 5 6 mpan2 
 |-  ( ~P ~P ( A u. B ) e. U. ( R1 " On ) -> ( A X. B ) e. U. ( R1 " On ) )
8 4 7 sylbi 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. U. ( R1 " On ) ) -> ( A X. B ) e. U. ( R1 " On ) )