Theorem oarec 4186

Description: Recursive definition of ordinal addition. Exercise 25 of [Enderton] p. 240.

Assertion

Ref	Expression
oarec	|- ((A e. On /\ B e. On) -> (A +o B) = (A u. {x | E.y e. B x = (A +o y)}))

Distinct variable groups:   x,y,A   x,B,y

Proof of Theorem oarec

Step	Hyp	Ref	Expression
1		opreq2 3960	. . . 4 |- (z = (/) -> (A +o z) = (A +o (/)))
2		rexeq1 1784	. . . . . 6 |- (z = (/) -> (E.y e. z x = (A +o y) <-> E.y e. (/) x = (A +o y)))
3	2	abbidv 1574	. . . . 5 |- (z = (/) -> {x | E.y e. z x = (A +o y)} = {x | E.y e. (/) x = (A +o y)})
4	3	uneq2d 2180	. . . 4 |- (z = (/) -> (A u. {x | E.y e. z x = (A +o y)}) = (A u. {x | E.y e. (/) x = (A +o y)}))
5	1, 4	eqeq12d 1486	. . 3 |- (z = (/) -> ((A +o z) = (A u. {x | E.y e. z x = (A +o y)}) <-> (A +o (/)) = (A u. {x | E.y e. (/) x = (A +o y)})))
6		opreq2 3960	. . . 4 |- (z = w -> (A +o z) = (A +o w))
7		rexeq1 1784	. . . . . 6 |- (z = w -> (E.y e. z x = (A +o y) <-> E.y e. w x = (A +o y)))
8	7	abbidv 1574	. . . . 5 |- (z = w -> {x | E.y e. z x = (A +o y)} = {x | E.y e. w x = (A +o y)})
9	8	uneq2d 2180	. . . 4 |- (z = w -> (A u. {x | E.y e. z x = (A +o y)}) = (A u. {x | E.y e. w x = (A +o y)}))
10	6, 9	eqeq12d 1486	. . 3 |- (z = w -> ((A +o z) = (A u. {x | E.y e. z x = (A +o y)}) <-> (A +o w) = (A u. {x | E.y e. w x = (A +o y)})))
11		opreq2 3960	. . . 4 |- (z = suc w -> (A +o z) = (A +o suc w))
12		rexeq1 1784	. . . . . 6 |- (z = suc w -> (E.y e. z x = (A +o y) <-> E.y e. suc wx = (A +o y)))
13	12	abbidv 1574	. . . . 5 |- (z = suc w -> {x | E.y e. z x = (A +o y)} = {x | E.y e. suc wx = (A +o y)})
14	13	uneq2d 2180	. . . 4 |- (z = suc w -> (A u. {x | E.y e. z x = (A +o y)}) = (A u. {x | E.y e. suc wx = (A +o y)}))
15	11, 14	eqeq12d 1486	. . 3 |- (z = suc w -> ((A +o z) = (A u. {x | E.y e. z x = (A +o y)}) <-> (A +o suc w) = (A u. {x | E.y e. suc wx = (A +o y)})))
16		opreq2 3960	. . . 4 |- (z = B -> (A +o z) = (A +o B))
17		rexeq1 1784	. . . . . 6 |- (z = B -> (E.y e. z x = (A +o y) <-> E.y e. B x = (A +o y)))
18	17	abbidv 1574	. . . . 5 |- (z = B -> {x | E.y e. z x = (A +o y)} = {x | E.y e. B x = (A +o y)})
19	18	uneq2d 2180	. . . 4 |- (z = B -> (A u. {x | E.y e. z x = (A +o y)}) = (A u. {x | E.y e. B x = (A +o y)}))
20	16, 19	eqeq12d 1486	. . 3 |- (z = B -> ((A +o z) = (A u. {x | E.y e. z x = (A +o y)}) <-> (A +o B) = (A u. {x | E.y e. B x = (A +o y)})))
21		oa0 4145	. . . 4 |- (A e. On -> (A +o (/)) = A)
22		rex0 2287	. . . . . . . 8 |- -. E.y e. (/) x = (A +o y)
23	22	nex 1099	. . . . . . 7 |- -. E.xE.y e. (/) x = (A +o y)
24		abn0 2286	. . . . . . . 8 |- ({x | E.y e. (/) x = (A +o y)} =/= (/) <-> E.xE.y e. (/) x = (A +o y))
25	24	necon1bbii 1614	. . . . . . 7 |- (-. E.xE.y e. (/) x = (A +o y) <-> {x | E.y e. (/) x = (A +o y)} = (/))
26	23, 25	mpbi 189	. . . . . 6 |- {x | E.y e. (/) x = (A +o y)} = (/)
27	26	uneq2i 2177	. . . . 5 |- (A u. {x | E.y e. (/) x = (A +o y)}) = (A u. (/))
28		un0 2293	. . . . 5 |- (A u. (/)) = A
29	27, 28	eqtr2 1493	. . . 4 |- A = (A u. {x | E.y e. (/) x = (A +o y)})
30	21, 29	syl6eq 1520	. . 3 |- (A e. On -> (A +o (/)) = (A u. {x | E.y e. (/) x = (A +o y)}))
31		oasuc 4153	. . . . . 6 |- ((A e. On /\ w e. On) -> (A +o suc w) = suc (A +o w))
32		df-sn 2408	. . . . . . . 8 |- {(A +o w)} = {x | x = (A +o w)}
33		uneq12 2175	. . . . . . . 8 |- (((A +o w) = (A u. {x | E.y e. w x = (A +o y)}) /\ {(A +o w)} = {x | x = (A +o w)}) -> ((A +o w) u. {(A +o w)}) = ((A u. {x | E.y e. w x = (A +o y)}) u. {x | x = (A +o w)}))
34	32, 33	mpan2 695	. . . . . . 7 |- ((A +o w) = (A u. {x | E.y e. w x = (A +o y)}) -> ((A +o w) u. {(A +o w)}) = ((A u. {x | E.y e. w x = (A +o y)}) u. {x | x = (A +o w)}))
35		df-suc 2949	. . . . . . 7 |- suc (A +o w) = ((A +o w) u. {(A +o w)})
36		visset 1809	. . . . . . . . . . . . . . . . 17 |- y e. V
37	36	elsuc 3033	. . . . . . . . . . . . . . . 16 |- (y e. suc w <-> (y e. w \/ y = w))
38	37	anbi1i 481	. . . . . . . . . . . . . . 15 |- ((y e. suc w /\ x = (A +o y)) <-> ((y e. w \/ y = w) /\ x = (A +o y)))
39		andir 604	. . . . . . . . . . . . . . 15 |- (((y e. w \/ y = w) /\ x = (A +o y)) <-> ((y e. w /\ x = (A +o y)) \/ (y = w /\ x = (A +o y))))
40	38, 39	bitr 173	. . . . . . . . . . . . . 14 |- ((y e. suc w /\ x = (A +o y)) <-> ((y e. w /\ x = (A +o y)) \/ (y = w /\ x = (A +o y))))
41	40	exbii 1049	. . . . . . . . . . . . 13 |- (E.y(y e. suc w /\ x = (A +o y)) <-> E.y((y e. w /\ x = (A +o y)) \/ (y = w /\ x = (A +o y))))
42		19.43 1086	. . . . . . . . . . . . 13 |- (E.y((y e. w /\ x = (A +o y)) \/ (y = w /\ x = (A +o y))) <-> (E.y(y e. w /\ x = (A +o y)) \/ E.y(y = w /\ x = (A +o y))))
43	41, 42	bitr 173	. . . . . . . . . . . 12 |- (E.y(y e. suc w /\ x = (A +o y)) <-> (E.y(y e. w /\ x = (A +o y)) \/ E.y(y = w /\ x = (A +o y))))
44		df-rex 1647	. . . . . . . . . . . 12 |- (E.y e. suc wx = (A +o y) <-> E.y(y e. suc w /\ x = (A +o y)))
45		df-rex 1647	. . . . . . . . . . . . 13 |- (E.y e. w x = (A +o y) <-> E.y(y e. w /\ x = (A +o y)))
46		visset 1809	. . . . . . . . . . . . . . 15 |- w e. V
47		opreq2 3960	. . . . . . . . . . . . . . . 16 |- (y = w -> (A +o y) = (A +o w))
48	47	eqeq2d 1483	. . . . . . . . . . . . . . 15 |- (y = w -> (x = (A +o y) <-> x = (A +o w)))
49	46, 48	ceqsexv 1831	. . . . . . . . . . . . . 14 |- (E.y(y = w /\ x = (A +o y)) <-> x = (A +o w))
50	49	bicomi 172	. . . . . . . . . . . . 13 |- (x = (A +o w) <-> E.y(y = w /\ x = (A +o y)))
51	45, 50	orbi12i 257	. . . . . . . . . . . 12 |- ((E.y e. w x = (A +o y) \/ x = (A +o w)) <-> (E.y(y e. w /\ x = (A +o y)) \/ E.y(y = w /\ x = (A +o y))))
52	43, 44, 51	3bitr4 183	. . . . . . . . . . 11 |- (E.y e. suc wx = (A +o y) <-> (E.y e. w x = (A +o y) \/ x = (A +o w)))
53	52	abbii 1572	. . . . . . . . . 10 |- {x | E.y e. suc wx = (A +o y)} = {x | (E.y e. w x = (A +o y) \/ x = (A +o w))}
54		unab 2263	. . . . . . . . . 10 |- ({x | E.y e. w x = (A +o y)} u. {x | x = (A +o w)}) = {x | (E.y e. w x = (A +o y) \/ x = (A +o w))}
55	53, 54	eqtr4 1495	. . . . . . . . 9 |- {x | E.y e. suc wx = (A +o y)} = ({x | E.y e. w x = (A +o y)} u. {x | x = (A +o w)})
56	55	uneq2i