Theorem rnwf

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

	Ref	Expression
Assertion	rnwf	$$⊢A\in \bigcup R_1\left[\mathrm{On}\right]\to \mathrm{ran}A\in \bigcup R_1\left[\mathrm{On}\right]$$

Proof

Step	Hyp	Ref	Expression
1		uniwf	$$⊢A\in \bigcup R_1\left[\mathrm{On}\right]\leftrightarrow \bigcup A\in \bigcup R_1\left[\mathrm{On}\right]$$
2		uniwf	$$⊢\bigcup A\in \bigcup R_1\left[\mathrm{On}\right]\leftrightarrow \bigcup \bigcup A\in \bigcup R_1\left[\mathrm{On}\right]$$
3	1 2	bitri	$$⊢A\in \bigcup R_1\left[\mathrm{On}\right]\leftrightarrow \bigcup \bigcup A\in \bigcup R_1\left[\mathrm{On}\right]$$
4		ssun2	$$⊢\mathrm{ran}A\subseteq \mathrm{dom}A\cup \mathrm{ran}A$$
5		dmrnssfld	$$⊢\mathrm{dom}A\cup \mathrm{ran}A\subseteq \bigcup \bigcup A$$
6	4 5	sstri	$$⊢\mathrm{ran}A\subseteq \bigcup \bigcup A$$
7		sswf	$$⊢\left(\bigcup \bigcup A\in \bigcup R_1\left[\mathrm{On}\right]\wedge \mathrm{ran}A\subseteq \bigcup \bigcup A\right)\to \mathrm{ran}A\in \bigcup R_1\left[\mathrm{On}\right]$$
8	6 7	mpan2	$$⊢\bigcup \bigcup A\in \bigcup R_1\left[\mathrm{On}\right]\to \mathrm{ran}A\in \bigcup R_1\left[\mathrm{On}\right]$$
9	3 8	sylbi	$$⊢A\in \bigcup R_1\left[\mathrm{On}\right]\to \mathrm{ran}A\in \bigcup R_1\left[\mathrm{On}\right]$$