Metamath Proof Explorer

Theorem dmwf

Description: The domain of a well-founded set is well-founded. (Contributed by Eric Schmidt, 12-Sep-2025)

Ref Expression
Assertion dmwf 
|- ( A e. U. ( R1 " On ) -> dom A e. U. ( R1 " On ) )

Proof

Step Hyp Ref Expression
1 uniwf 
 |-  ( A e. U. ( R1 " On ) <-> U. A e. U. ( R1 " On ) )
2 uniwf 
 |-  ( U. A e. U. ( R1 " On ) <-> U. U. A e. U. ( R1 " On ) )
3 1 2 bitri 
 |-  ( A e. U. ( R1 " On ) <-> U. U. A e. U. ( R1 " On ) )
4 ssun1 
 |-  dom A C_ ( dom A u. ran A )
5 dmrnssfld 
 |-  ( dom A u. ran A ) C_ U. U. A
6 4 5 sstri 
 |-  dom A C_ U. U. A
7 sswf 
 |-  ( ( U. U. A e. U. ( R1 " On ) /\ dom A C_ U. U. A ) -> dom A e. U. ( R1 " On ) )
8 6 7 mpan2 
 |-  ( U. U. A e. U. ( R1 " On ) -> dom A e. U. ( R1 " On ) )
9 3 8 sylbi 
 |-  ( A e. U. ( R1 " On ) -> dom A e. U. ( R1 " On ) )