dmwf

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

		Ref	Expression
	Assertion	dmwf	$⊢ A \in ⋃ R_{1} [On] \to dom A \in ⋃ R_{1} [On]$

Step	Hyp	Ref	Expression
1		uniwf	$⊢ A \in ⋃ R_{1} [On] \leftrightarrow ⋃ A \in ⋃ R_{1} [On]$
2		uniwf	$⊢ ⋃ A \in ⋃ R_{1} [On] \leftrightarrow ⋃ ⋃ A \in ⋃ R_{1} [On]$
3	1 2	bitri	$⊢ A \in ⋃ R_{1} [On] \leftrightarrow ⋃ ⋃ A \in ⋃ R_{1} [On]$
4		ssun1	$⊢ dom A \subseteq dom A \cup ran A$
5		dmrnssfld	$⊢ dom A \cup ran A \subseteq ⋃ ⋃ A$
6	4 5	sstri	$⊢ dom A \subseteq ⋃ ⋃ A$
7		sswf	$⊢ (⋃ ⋃ A \in ⋃ R_{1} [On] \land dom A \subseteq ⋃ ⋃ A) \to dom A \in ⋃ R_{1} [On]$
8	6 7	mpan2	$⊢ ⋃ ⋃ A \in ⋃ R_{1} [On] \to dom A \in ⋃ R_{1} [On]$
9	3 8	sylbi	$⊢ A \in ⋃ R_{1} [On] \to dom A \in ⋃ R_{1} [On]$

Metamath Proof Explorer