Theorem onsetreclem2

Description: Lemma for onsetrec . (Contributed by Emmett Weisz, 22-Jun-2021) (New usage is discouraged.)

	Ref	Expression
Hypothesis	onsetreclem2.1	$$⊢F=\left(x\in \mathrm{V}⟼\left\{\bigcup x,\mathrm{suc}\bigcup x\right\}\right)$$
Assertion	onsetreclem2	$$⊢a\subseteq \mathrm{On}\to F\left(a\right)\subseteq \mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		onsetreclem2.1	$$⊢F=\left(x\in \mathrm{V}⟼\left\{\bigcup x,\mathrm{suc}\bigcup x\right\}\right)$$
2	1	onsetreclem1	$$⊢F\left(a\right)=\left\{\bigcup a,\mathrm{suc}\bigcup a\right\}$$
3		vex	$$⊢a\in \mathrm{V}$$
4	3	ssonunii	$$⊢a\subseteq \mathrm{On}\to \bigcup a\in \mathrm{On}$$
5		suceloni	$$⊢\bigcup a\in \mathrm{On}\to \mathrm{suc}\bigcup a\in \mathrm{On}$$
6		prssi	$$⊢\left(\bigcup a\in \mathrm{On}\wedge \mathrm{suc}\bigcup a\in \mathrm{On}\right)\to \left\{\bigcup a,\mathrm{suc}\bigcup a\right\}\subseteq \mathrm{On}$$
7	4 5 6	syl2anc2	$$⊢a\subseteq \mathrm{On}\to \left\{\bigcup a,\mathrm{suc}\bigcup a\right\}\subseteq \mathrm{On}$$
8	2 7	eqsstrid	$$⊢a\subseteq \mathrm{On}\to F\left(a\right)\subseteq \mathrm{On}$$