Theorem dmwf

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

	Ref	Expression
Assertion	dmwf	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → dom 𝐴 ∈ ∪ ( 𝑅1 “ On ) )

Proof

Step	Hyp	Ref	Expression
1		uniwf	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
2		uniwf	⊢ ( ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ ∪ ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
3	1 2	bitri	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ ∪ ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
4		ssun1	⊢ dom 𝐴 ⊆ ( dom 𝐴 ∪ ran 𝐴 )
5		dmrnssfld	⊢ ( dom 𝐴 ∪ ran 𝐴 ) ⊆ ∪ ∪ 𝐴
6	4 5	sstri	⊢ dom 𝐴 ⊆ ∪ ∪ 𝐴
7		sswf	⊢ ( ( ∪ ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ dom 𝐴 ⊆ ∪ ∪ 𝐴 ) → dom 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
8	6 7	mpan2	⊢ ( ∪ ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) → dom 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
9	3 8	sylbi	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → dom 𝐴 ∈ ∪ ( 𝑅1 “ On ) )