Theorem onsetrec

Description: Construct On using set recursion. When x e. On , the function F constructs the least ordinal greater than any of the elements of x , which is U. x for a limit ordinal and suc U. x for a successor ordinal.

For example, ( F{ 1o , 2o } ) = { U. { 1o , 2o } , suc U. { 1o , 2o } } = { 2o , 3o } which contains 3o , and ( F_om ) = { U.om , suc U. om } = {om , om +o 1o } , which contains _om . If we start with the empty set and keep applying F transfinitely many times, all ordinal numbers will be generated.

Any function F fulfilling lemmas onsetreclem2 and onsetreclem3 will recursively generate On ; for example, F = ( x e.V |-> suc suc U. x } ) also works. Whether this function or the function in the theorem is used, taking this theorem as a definition of On is unsatisfying because it relies on the different properties of limit and successor ordinals. A different approach could be to let F = ( x e. V |-> { y e. ~P x | Tr y } ) , based on dfon2 .

The proof of this theorem uses the dummy variable a rather than x to avoid a distinct variable condition between F and x . (Contributed by Emmett Weisz, 22-Jun-2021)

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

Proof

Step	Hyp	Ref	Expression
1		onsetrec.1	$$⊢F=\left(x\in \mathrm{V}⟼\left\{\bigcup x,\mathrm{suc}\bigcup x\right\}\right)$$
2		eqid	$$⊢\mathrm{setrecs}\left(F\right)=\mathrm{setrecs}\left(F\right)$$
3	1	onsetreclem2	$$⊢a\subseteq \mathrm{On}\to F\left(a\right)\subseteq \mathrm{On}$$
4	3	ax-gen	$$⊢\forall a\left(a\subseteq \mathrm{On}\to F\left(a\right)\subseteq \mathrm{On}\right)$$
5	4	a1i	$$⊢\top \to \forall a\left(a\subseteq \mathrm{On}\to F\left(a\right)\subseteq \mathrm{On}\right)$$
6	2 5	setrec2v	$$⊢\top \to \mathrm{setrecs}\left(F\right)\subseteq \mathrm{On}$$
7	6	mptru	$$⊢\mathrm{setrecs}\left(F\right)\subseteq \mathrm{On}$$
8		vex	$$⊢a\in \mathrm{V}$$
9	8	a1i	$$⊢a\subseteq \mathrm{setrecs}\left(F\right)\to a\in \mathrm{V}$$
10		id	$$⊢a\subseteq \mathrm{setrecs}\left(F\right)\to a\subseteq \mathrm{setrecs}\left(F\right)$$
11	2 9 10	setrec1	$$⊢a\subseteq \mathrm{setrecs}\left(F\right)\to F\left(a\right)\subseteq \mathrm{setrecs}\left(F\right)$$
12	1	onsetreclem3	$$⊢a\in \mathrm{On}\to a\in F\left(a\right)$$
13		ssel	$$⊢F\left(a\right)\subseteq \mathrm{setrecs}\left(F\right)\to \left(a\in F\left(a\right)\to a\in \mathrm{setrecs}\left(F\right)\right)$$
14	11 12 13	syl2im	$$⊢a\subseteq \mathrm{setrecs}\left(F\right)\to \left(a\in \mathrm{On}\to a\in \mathrm{setrecs}\left(F\right)\right)$$
15	14	com12	$$⊢a\in \mathrm{On}\to \left(a\subseteq \mathrm{setrecs}\left(F\right)\to a\in \mathrm{setrecs}\left(F\right)\right)$$
16	15	rgen	$$⊢\forall a\in \mathrm{On}\left(a\subseteq \mathrm{setrecs}\left(F\right)\to a\in \mathrm{setrecs}\left(F\right)\right)$$
17		tfi	$$⊢\left(\mathrm{setrecs}\left(F\right)\subseteq \mathrm{On}\wedge \forall a\in \mathrm{On}\left(a\subseteq \mathrm{setrecs}\left(F\right)\to a\in \mathrm{setrecs}\left(F\right)\right)\right)\to \mathrm{setrecs}\left(F\right)=\mathrm{On}$$
18	7 16 17	mp2an	$$⊢\mathrm{setrecs}\left(F\right)=\mathrm{On}$$