Theorem onsetreclem1

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

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

Proof

Step	Hyp	Ref	Expression
1		onsetreclem1.1	$$⊢F=\left(x\in \mathrm{V}⟼\left\{\bigcup x,\mathrm{suc}\bigcup x\right\}\right)$$
2		unieq	$$⊢x=a\to \bigcup x=\bigcup a$$
3		suceq	$$⊢\bigcup x=\bigcup a\to \mathrm{suc}\bigcup x=\mathrm{suc}\bigcup a$$
4	2 3	syl	$$⊢x=a\to \mathrm{suc}\bigcup x=\mathrm{suc}\bigcup a$$
5	2 4	preq12d	$$⊢x=a\to \left\{\bigcup x,\mathrm{suc}\bigcup x\right\}=\left\{\bigcup a,\mathrm{suc}\bigcup a\right\}$$
6		prex	$$⊢\left\{\bigcup a,\mathrm{suc}\bigcup a\right\}\in \mathrm{V}$$
7	5 1 6	fvmpt	$$⊢a\in \mathrm{V}\to F\left(a\right)=\left\{\bigcup a,\mathrm{suc}\bigcup a\right\}$$
8	7	elv	$$⊢F\left(a\right)=\left\{\bigcup a,\mathrm{suc}\bigcup a\right\}$$