Theorem oarec

Description: Recursive definition of ordinal addition. Exercise 25 of Enderton p. 240. (Contributed by NM, 26-Dec-2004) (Revised by Mario Carneiro, 30-May-2015)

	Ref	Expression
Assertion	oarec	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to A{+}_{𝑜}B=A\cup \mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢z=\varnothing \to A{+}_{𝑜}z=A{+}_{𝑜}\varnothing$$
2		mpteq1	$$⊢z=\varnothing \to \left(x\in z⟼A{+}_{𝑜}x\right)=\left(x\in \varnothing ⟼A{+}_{𝑜}x\right)$$
3		mpt0	$$⊢\left(x\in \varnothing ⟼A{+}_{𝑜}x\right)=\varnothing$$
4	2 3	eqtrdi	$$⊢z=\varnothing \to \left(x\in z⟼A{+}_{𝑜}x\right)=\varnothing$$
5	4	rneqd	$$⊢z=\varnothing \to \mathrm{ran}\left(x\in z⟼A{+}_{𝑜}x\right)=\mathrm{ran}\varnothing$$
6		rn0	$$⊢\mathrm{ran}\varnothing =\varnothing$$
7	5 6	eqtrdi	$$⊢z=\varnothing \to \mathrm{ran}\left(x\in z⟼A{+}_{𝑜}x\right)=\varnothing$$
8	7	uneq2d	$$⊢z=\varnothing \to A\cup \mathrm{ran}\left(x\in z⟼A{+}_{𝑜}x\right)=A\cup \varnothing$$
9	1 8	eqeq12d	$$⊢z=\varnothing \to \left(A{+}_{𝑜}z=A\cup \mathrm{ran}\left(x\in z⟼A{+}_{𝑜}x\right)\leftrightarrow A{+}_{𝑜}\varnothing =A\cup \varnothing \right)$$
10		oveq2	$$⊢z=w\to A{+}_{𝑜}z=A{+}_{𝑜}w$$
11		mpteq1	$$⊢z=w\to \left(x\in z⟼A{+}_{𝑜}x\right)=\left(x\in w⟼A{+}_{𝑜}x\right)$$
12	11	rneqd	$$⊢z=w\to \mathrm{ran}\left(x\in z⟼A{+}_{𝑜}x\right)=\mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)$$
13	12	uneq2d	$$⊢z=w\to A\cup \mathrm{ran}\left(x\in z⟼A{+}_{𝑜}x\right)=A\cup \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)$$
14	10 13	eqeq12d	$$⊢z=w\to \left(A{+}_{𝑜}z=A\cup \mathrm{ran}\left(x\in z⟼A{+}_{𝑜}x\right)\leftrightarrow A{+}_{𝑜}w=A\cup \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\right)$$
15		oveq2	$$⊢z=\mathrm{suc}w\to A{+}_{𝑜}z=A{+}_{𝑜}\mathrm{suc}w$$
16		mpteq1	$$⊢z=\mathrm{suc}w\to \left(x\in z⟼A{+}_{𝑜}x\right)=\left(x\in \mathrm{suc}w⟼A{+}_{𝑜}x\right)$$
17	16	rneqd	$$⊢z=\mathrm{suc}w\to \mathrm{ran}\left(x\in z⟼A{+}_{𝑜}x\right)=\mathrm{ran}\left(x\in \mathrm{suc}w⟼A{+}_{𝑜}x\right)$$
18	17	uneq2d	$$⊢z=\mathrm{suc}w\to A\cup \mathrm{ran}\left(x\in z⟼A{+}_{𝑜}x\right)=A\cup \mathrm{ran}\left(x\in \mathrm{suc}w⟼A{+}_{𝑜}x\right)$$
19	15 18	eqeq12d	$$⊢z=\mathrm{suc}w\to \left(A{+}_{𝑜}z=A\cup \mathrm{ran}\left(x\in z⟼A{+}_{𝑜}x\right)\leftrightarrow A{+}_{𝑜}\mathrm{suc}w=A\cup \mathrm{ran}\left(x\in \mathrm{suc}w⟼A{+}_{𝑜}x\right)\right)$$
20		oveq2	$$⊢z=B\to A{+}_{𝑜}z=A{+}_{𝑜}B$$
21		mpteq1	$$⊢z=B\to \left(x\in z⟼A{+}_{𝑜}x\right)=\left(x\in B⟼A{+}_{𝑜}x\right)$$
22	21	rneqd	$$⊢z=B\to \mathrm{ran}\left(x\in z⟼A{+}_{𝑜}x\right)=\mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)$$
23	22	uneq2d	$$⊢z=B\to A\cup \mathrm{ran}\left(x\in z⟼A{+}_{𝑜}x\right)=A\cup \mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)$$
24	20 23	eqeq12d	$$⊢z=B\to \left(A{+}_{𝑜}z=A\cup \mathrm{ran}\left(x\in z⟼A{+}_{𝑜}x\right)\leftrightarrow A{+}_{𝑜}B=A\cup \mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)\right)$$
25		oa0	$$⊢A\in \mathrm{On}\to A{+}_{𝑜}\varnothing =A$$
26		un0	$$⊢A\cup \varnothing =A$$
27	25 26	eqtr4di	$$⊢A\in \mathrm{On}\to A{+}_{𝑜}\varnothing =A\cup \varnothing$$
28		uneq1	$$⊢A{+}_{𝑜}w=A\cup \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\to \left(A{+}_{𝑜}w\right)\cup \left\{A{+}_{𝑜}w\right\}=\left(A\cup \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\right)\cup \left\{A{+}_{𝑜}w\right\}$$
29		unass	$$⊢\left(A\cup \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\right)\cup \left\{A{+}_{𝑜}w\right\}=A\cup \left(\mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\cup \left\{A{+}_{𝑜}w\right\}\right)$$
30		rexun	$$⊢\exists x\in \left(w\cup \left\{w\right\}\right)y=A{+}_{𝑜}x\leftrightarrow \left(\exists x\in wy=A{+}_{𝑜}x\vee \exists x\in \left\{w\right\}y=A{+}_{𝑜}x\right)$$
31		df-suc	$$⊢\mathrm{suc}w=w\cup \left\{w\right\}$$
32	31	rexeqi	$$⊢\exists x\in \mathrm{suc}wy=A{+}_{𝑜}x\leftrightarrow \exists x\in \left(w\cup \left\{w\right\}\right)y=A{+}_{𝑜}x$$
33		eqid	$$⊢\left(x\in w⟼A{+}_{𝑜}x\right)=\left(x\in w⟼A{+}_{𝑜}x\right)$$
34	33	elrnmpt	$$⊢y\in \mathrm{V}\to \left(y\in \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\leftrightarrow \exists x\in wy=A{+}_{𝑜}x\right)$$
35	34	elv	$$⊢y\in \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\leftrightarrow \exists x\in wy=A{+}_{𝑜}x$$
36		velsn	$$⊢y\in \left\{A{+}_{𝑜}w\right\}\leftrightarrow y=A{+}_{𝑜}w$$
37		vex	$$⊢w\in \mathrm{V}$$
38		oveq2	$$⊢x=w\to A{+}_{𝑜}x=A{+}_{𝑜}w$$
39	38	eqeq2d	$$⊢x=w\to \left(y=A{+}_{𝑜}x\leftrightarrow y=A{+}_{𝑜}w\right)$$
40	37 39	rexsn	$$⊢\exists x\in \left\{w\right\}y=A{+}_{𝑜}x\leftrightarrow y=A{+}_{𝑜}w$$
41	36 40	bitr4i	$$⊢y\in \left\{A{+}_{𝑜}w\right\}\leftrightarrow \exists x\in \left\{w\right\}y=A{+}_{𝑜}x$$
42	35 41	orbi12i	$$⊢\left(y\in \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\vee y\in \left\{A{+}_{𝑜}w\right\}\right)\leftrightarrow \left(\exists x\in wy=A{+}_{𝑜}x\vee \exists x\in \left\{w\right\}y=A{+}_{𝑜}x\right)$$
43	30 32 42	3bitr4i	$$⊢\exists x\in \mathrm{suc}wy=A{+}_{𝑜}x\leftrightarrow \left(y\in \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\vee y\in \left\{A{+}_{𝑜}w\right\}\right)$$
44		eqid	$$⊢\left(x\in \mathrm{suc}w⟼A{+}_{𝑜}x\right)=\left(x\in \mathrm{suc}w⟼A{+}_{𝑜}x\right)$$
45		ovex	$$⊢A{+}_{𝑜}x\in \mathrm{V}$$
46	44 45	elrnmpti	$$⊢y\in \mathrm{ran}\left(x\in \mathrm{suc}w⟼A{+}_{𝑜}x\right)\leftrightarrow \exists x\in \mathrm{suc}wy=A{+}_{𝑜}x$$
47		elun	$$⊢y\in \left(\mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\cup \left\{A{+}_{𝑜}w\right\}\right)\leftrightarrow \left(y\in \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\vee y\in \left\{A{+}_{𝑜}w\right\}\right)$$
48	43 46 47	3bitr4i	$$⊢y\in \mathrm{ran}\left(x\in \mathrm{suc}w⟼A{+}_{𝑜}x\right)\leftrightarrow y\in \left(\mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\cup \left\{A{+}_{𝑜}w\right\}\right)$$
49	48	eqriv	$$⊢\mathrm{ran}\left(x\in \mathrm{suc}w⟼A{+}_{𝑜}x\right)=\mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\cup \left\{A{+}_{𝑜}w\right\}$$
50	49	uneq2i	$$⊢A\cup \mathrm{ran}\left(x\in \mathrm{suc}w⟼A{+}_{𝑜}x\right)=A\cup \left(\mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\cup \left\{A{+}_{𝑜}w\right\}\right)$$
51	29 50	eqtr4i	$$⊢\left(A\cup \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\right)\cup \left\{A{+}_{𝑜}w\right\}=A\cup \mathrm{ran}\left(x\in \mathrm{suc}w⟼A{+}_{𝑜}x\right)$$
52	28 51	eqtrdi	$$⊢A{+}_{𝑜}w=A\cup \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\to \left(A{+}_{𝑜}w\right)\cup \left\{A{+}_{𝑜}w\right\}=A\cup \mathrm{ran}\left(x\in \mathrm{suc}w⟼A{+}_{𝑜}x\right)$$
53		oasuc	$$⊢\left(A\in \mathrm{On}\wedge w\in \mathrm{On}\right)\to A{+}_{𝑜}\mathrm{suc}w=\mathrm{suc}\left(A{+}_{𝑜}w\right)$$
54		df-suc	$$⊢\mathrm{suc}\left(A{+}_{𝑜}w\right)=\left(A{+}_{𝑜}w\right)\cup \left\{A{+}_{𝑜}w\right\}$$
55	53 54	eqtrdi	$$⊢\left(A\in \mathrm{On}\wedge w\in \mathrm{On}\right)\to A{+}_{𝑜}\mathrm{suc}w=\left(A{+}_{𝑜}w\right)\cup \left\{A{+}_{𝑜}w\right\}$$
56	55	eqeq1d	$$⊢\left(A\in \mathrm{On}\wedge w\in \mathrm{On}\right)\to \left(A{+}_{𝑜}\mathrm{suc}w=A\cup \mathrm{ran}\left(x\in \mathrm{suc}w⟼A{+}_{𝑜}x\right)\leftrightarrow \left(A{+}_{𝑜}w\right)\cup \left\{A{+}_{𝑜}w\right\}=A\cup \mathrm{ran}\left(x\in \mathrm{suc}w⟼A{+}_{𝑜}x\right)\right)$$
57	52 56	syl5ibr	$$⊢\left(A\in \mathrm{On}\wedge w\in \mathrm{On}\right)\to \left(A{+}_{𝑜}w=A\cup \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\to A{+}_{𝑜}\mathrm{suc}w=A\cup \mathrm{ran}\left(x\in \mathrm{suc}w⟼A{+}_{𝑜}x\right)\right)$$
58	57	expcom	$$⊢w\in \mathrm{On}\to \left(A\in \mathrm{On}\to \left(A{+}_{𝑜}w=A\cup \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\to A{+}_{𝑜}\mathrm{suc}w=A\cup \mathrm{ran}\left(x\in \mathrm{suc}w⟼A{+}_{𝑜}x\right)\right)\right)$$
59		vex	$$⊢z\in \mathrm{V}$$
60		oalim	$$⊢\left(A\in \mathrm{On}\wedge \left(z\in \mathrm{V}\wedge \mathrm{Lim}z\right)\right)\to A{+}_{𝑜}z=\bigcup _{w\in z}\left(A{+}_{𝑜}w\right)$$
61	59 60	mpanr1	$$⊢\left(A\in \mathrm{On}\wedge \mathrm{Lim}z\right)\to A{+}_{𝑜}z=\bigcup _{w\in z}\left(A{+}_{𝑜}w\right)$$
62	61	ancoms	$$⊢\left(\mathrm{Lim}z\wedge A\in \mathrm{On}\right)\to A{+}_{𝑜}z=\bigcup _{w\in z}\left(A{+}_{𝑜}w\right)$$
63	62	adantr	$$⊢\left(\left(\mathrm{Lim}z\wedge A\in \mathrm{On}\right)\wedge \forall w\in zA{+}_{𝑜}w=A\cup \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\right)\to A{+}_{𝑜}z=\bigcup _{w\in z}\left(A{+}_{𝑜}w\right)$$
64		iuneq2	$$⊢\forall w\in zA{+}_{𝑜}w=A\cup \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\to \bigcup _{w\in z}\left(A{+}_{𝑜}w\right)=\bigcup _{w\in z}\left(A\cup \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\right)$$
65	64	adantl	$$⊢\left(\left(\mathrm{Lim}z\wedge A\in \mathrm{On}\right)\wedge \forall w\in zA{+}_{𝑜}w=A\cup \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\right)\to \bigcup _{w\in z}\left(A{+}_{𝑜}w\right)=\bigcup _{w\in z}\left(A\cup \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\right)$$
66		iunun	$$⊢\bigcup _{w\in z}\left(A\cup \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\right)=\bigcup _{w\in z}A\cup \bigcup _{w\in z}\mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)$$
67		0ellim	$$⊢\mathrm{Lim}z\to \varnothing \in z$$
68		ne0i	$$⊢\varnothing \in z\to z\ne \varnothing$$
69		iunconst	$$⊢z\ne \varnothing \to \bigcup _{w\in z}A=A$$
70	67 68 69	3syl	$$⊢\mathrm{Lim}z\to \bigcup _{w\in z}A=A$$
71		df-rex	$$⊢\exists x\in wy=A{+}_{𝑜}x\leftrightarrow \exists x\left(x\in w\wedge y=A{+}_{𝑜}x\right)$$
72	35 71	bitri	$$⊢y\in \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\leftrightarrow \exists x\left(x\in w\wedge y=A{+}_{𝑜}x\right)$$
73	72	rexbii	$$⊢\exists w\in zy\in \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\leftrightarrow \exists w\in z\exists x\left(x\in w\wedge y=A{+}_{𝑜}x\right)$$
74		eluni2	$$⊢x\in \bigcup z\leftrightarrow \exists w\in zx\in w$$
75	74	anbi1i	$$⊢\left(x\in \bigcup z\wedge y=A{+}_{𝑜}x\right)\leftrightarrow \left(\exists w\in zx\in w\wedge y=A{+}_{𝑜}x\right)$$
76		r19.41v	$$⊢\exists w\in z\left(x\in w\wedge y=A{+}_{𝑜}x\right)\leftrightarrow \left(\exists w\in zx\in w\wedge y=A{+}_{𝑜}x\right)$$
77	75 76	bitr4i	$$⊢\left(x\in \bigcup z\wedge y=A{+}_{𝑜}x\right)\leftrightarrow \exists w\in z\left(x\in w\wedge y=A{+}_{𝑜}x\right)$$
78	77	exbii	$$⊢\exists x\left(x\in \bigcup z\wedge y=A{+}_{𝑜}x\right)\leftrightarrow \exists x\exists w\in z\left(x\in w\wedge y=A{+}_{𝑜}x\right)$$
79		df-rex	$$⊢\exists x\in \bigcup zy=A{+}_{𝑜}x\leftrightarrow \exists x\left(x\in \bigcup z\wedge y=A{+}_{𝑜}x\right)$$
80		rexcom4	$$⊢\exists w\in z\exists x\left(x\in w\wedge y=A{+}_{𝑜}x\right)\leftrightarrow \exists x\exists w\in z\left(x\in w\wedge y=A{+}_{𝑜}x\right)$$
81	78 79 80	3bitr4i	$$⊢\exists x\in \bigcup zy=A{+}_{𝑜}x\leftrightarrow \exists w\in z\exists x\left(x\in w\wedge y=A{+}_{𝑜}x\right)$$
82	73 81	bitr4i	$$⊢\exists w\in zy\in \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\leftrightarrow \exists x\in \bigcup zy=A{+}_{𝑜}x$$
83		limuni	$$⊢\mathrm{Lim}z\to z=\bigcup z$$
84	83	rexeqdv	$$⊢\mathrm{Lim}z\to \left(\exists x\in zy=A{+}_{𝑜}x\leftrightarrow \exists x\in \bigcup zy=A{+}_{𝑜}x\right)$$
85	82 84	bitr4id	$$⊢\mathrm{Lim}z\to \left(\exists w\in zy\in \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\leftrightarrow \exists x\in zy=A{+}_{𝑜}x\right)$$
86		eliun	$$⊢y\in \bigcup _{w\in z}\mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\leftrightarrow \exists w\in zy\in \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)$$
87		eqid	$$⊢\left(x\in z⟼A{+}_{𝑜}x\right)=\left(x\in z⟼A{+}_{𝑜}x\right)$$
88	87 45	elrnmpti	$$⊢y\in \mathrm{ran}\left(x\in z⟼A{+}_{𝑜}x\right)\leftrightarrow \exists x\in zy=A{+}_{𝑜}x$$
89	85 86 88	3bitr4g	$$⊢\mathrm{Lim}z\to \left(y\in \bigcup _{w\in z}\mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\leftrightarrow y\in \mathrm{ran}\left(x\in z⟼A{+}_{𝑜}x\right)\right)$$
90	89	eqrdv	$$⊢\mathrm{Lim}z\to \bigcup _{w\in z}\mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)=\mathrm{ran}\left(x\in z⟼A{+}_{𝑜}x\right)$$
91	70 90	uneq12d	$$⊢\mathrm{Lim}z\to \bigcup _{w\in z}A\cup \bigcup _{w\in z}\mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)=A\cup \mathrm{ran}\left(x\in z⟼A{+}_{𝑜}x\right)$$
92	66 91	eqtrid	$$⊢\mathrm{Lim}z\to \bigcup _{w\in z}\left(A\cup \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\right)=A\cup \mathrm{ran}\left(x\in z⟼A{+}_{𝑜}x\right)$$
93	92	ad2antrr	$$⊢\left(\left(\mathrm{Lim}z\wedge A\in \mathrm{On}\right)\wedge \forall w\in zA{+}_{𝑜}w=A\cup \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\right)\to \bigcup _{w\in z}\left(A\cup \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\right)=A\cup \mathrm{ran}\left(x\in z⟼A{+}_{𝑜}x\right)$$
94	63 65 93	3eqtrd	$$⊢\left(\left(\mathrm{Lim}z\wedge A\in \mathrm{On}\right)\wedge \forall w\in zA{+}_{𝑜}w=A\cup \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\right)\to A{+}_{𝑜}z=A\cup \mathrm{ran}\left(x\in z⟼A{+}_{𝑜}x\right)$$
95	94	exp31	$$⊢\mathrm{Lim}z\to \left(A\in \mathrm{On}\to \left(\forall w\in zA{+}_{𝑜}w=A\cup \mathrm{ran}\left(x\in w⟼A{+}_{𝑜}x\right)\to A{+}_{𝑜}z=A\cup \mathrm{ran}\left(x\in z⟼A{+}_{𝑜}x\right)\right)\right)$$
96	9 14 19 24 27 58 95	tfinds3	$$⊢B\in \mathrm{On}\to \left(A\in \mathrm{On}\to A{+}_{𝑜}B=A\cup \mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)\right)$$
97	96	impcom	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to A{+}_{𝑜}B=A\cup \mathrm{ran}\left(x\in B⟼A{+}_{𝑜}x\right)$$