Theorem onsetreclem3

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

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

Proof

Step	Hyp	Ref	Expression
1		onsetreclem3.1	$$⊢F=\left(x\in \mathrm{V}⟼\left\{\bigcup x,\mathrm{suc}\bigcup x\right\}\right)$$
2		eloni	$$⊢a\in \mathrm{On}\to \mathrm{Ord}a$$
3		orduniorsuc	$$⊢\mathrm{Ord}a\to \left(a=\bigcup a\vee a=\mathrm{suc}\bigcup a\right)$$
4	2 3	syl	$$⊢a\in \mathrm{On}\to \left(a=\bigcup a\vee a=\mathrm{suc}\bigcup a\right)$$
5		vex	$$⊢a\in \mathrm{V}$$
6	5	elpr	$$⊢a\in \left\{\bigcup a,\mathrm{suc}\bigcup a\right\}\leftrightarrow \left(a=\bigcup a\vee a=\mathrm{suc}\bigcup a\right)$$
7	4 6	sylibr	$$⊢a\in \mathrm{On}\to a\in \left\{\bigcup a,\mathrm{suc}\bigcup a\right\}$$
8	1	onsetreclem1	$$⊢F\left(a\right)=\left\{\bigcup a,\mathrm{suc}\bigcup a\right\}$$
9	7 8	eleqtrrdi	$$⊢a\in \mathrm{On}\to a\in F\left(a\right)$$