Theorem elwf

Description: An element of a well-founded set is well-founded. (Contributed by BTernaryTau, 30-Dec-2025)

	Ref	Expression
Assertion	elwf	$$⊢\left(A\in \bigcup R_1\left[\mathrm{On}\right]\wedge B\in A\right)\to B\in \bigcup R_1\left[\mathrm{On}\right]$$

Proof

Step	Hyp	Ref	Expression
1		elssuni	$$⊢B\in A\to B\subseteq \bigcup A$$
2		uniwf	$$⊢A\in \bigcup R_1\left[\mathrm{On}\right]\leftrightarrow \bigcup A\in \bigcup R_1\left[\mathrm{On}\right]$$
3		sswf	$$⊢\left(\bigcup A\in \bigcup R_1\left[\mathrm{On}\right]\wedge B\subseteq \bigcup A\right)\to B\in \bigcup R_1\left[\mathrm{On}\right]$$
4	2 3	sylanb	$$⊢\left(A\in \bigcup R_1\left[\mathrm{On}\right]\wedge B\subseteq \bigcup A\right)\to B\in \bigcup R_1\left[\mathrm{On}\right]$$
5	1 4	sylan2	$$⊢\left(A\in \bigcup R_1\left[\mathrm{On}\right]\wedge B\in A\right)\to B\in \bigcup R_1\left[\mathrm{On}\right]$$