Metamath Proof Explorer

Theorem relwf

Description: A relation is a well-founded set iff its domain and range are. (Contributed by Eric Schmidt, 29-Sep-2025)

Ref Expression
Assertion relwf 
|- ( Rel R -> ( R e. U. ( R1 " On ) <-> ( dom R e. U. ( R1 " On ) /\ ran R e. U. ( R1 " On ) ) ) )

Proof

Step Hyp Ref Expression
1 dmwf 
 |-  ( R e. U. ( R1 " On ) -> dom R e. U. ( R1 " On ) )
2 rnwf 
 |-  ( R e. U. ( R1 " On ) -> ran R e. U. ( R1 " On ) )
3 1 2 jca 
 |-  ( R e. U. ( R1 " On ) -> ( dom R e. U. ( R1 " On ) /\ ran R e. U. ( R1 " On ) ) )
4 xpwf 
 |-  ( ( dom R e. U. ( R1 " On ) /\ ran R e. U. ( R1 " On ) ) -> ( dom R X. ran R ) e. U. ( R1 " On ) )
5 relssdmrn 
 |-  ( Rel R -> R C_ ( dom R X. ran R ) )
6 sswf 
 |-  ( ( ( dom R X. ran R ) e. U. ( R1 " On ) /\ R C_ ( dom R X. ran R ) ) -> R e. U. ( R1 " On ) )
7 5 6 sylan2 
 |-  ( ( ( dom R X. ran R ) e. U. ( R1 " On ) /\ Rel R ) -> R e. U. ( R1 " On ) )
8 7 expcom 
 |-  ( Rel R -> ( ( dom R X. ran R ) e. U. ( R1 " On ) -> R e. U. ( R1 " On ) ) )
9 4 8 syl5 
 |-  ( Rel R -> ( ( dom R e. U. ( R1 " On ) /\ ran R e. U. ( R1 " On ) ) -> R e. U. ( R1 " On ) ) )
10 3 9 impbid2 
 |-  ( Rel R -> ( R e. U. ( R1 " On ) <-> ( dom R e. U. ( R1 " On ) /\ ran R e. U. ( R1 " On ) ) ) )