Theorem oarec 4254

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 4027	. . . 4 |- (z = (/) -> (A +o z) = (A +o (/)))
2		rexeq1 1834	. . . . . 6 |- (z = (/) -> (E.y e. z x = (A +o y) <-> E.y e. (/) x = (A +o y)))
3	2	abbidv 1624	. . . . 5 |- (z = (/) -> {x | E.y e. z x = (A +o y)} = {x | E.y e. (/) x = (A +o y)})
4	3	uneq2d 2235	. . . 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 1536	. . 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 4027	. . . 4 |- (z = w -> (A +o z) = (A +o w))
7		rexeq1 1834	. . . . . 6 |- (z = w -> (E.y e. z x = (A +o y) <-> E.y e. w x = (A +o y)))
8	7	abbidv 1624	. . . . 5 |- (z = w -> {x | E.y e. z x = (A +o y)} = {x | E.y e. w x = (A +o y)})
9	8	uneq2d 2235	. . . 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 1536	. . 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 4027	. . . 4 |- (z = suc w -> (A +o z) = (A +o suc w))
12		rexeq1 1834	. . . . . 6 |- (z = suc w -> (E.y e. z x = (A +o y) <-> E.y e. suc wx = (A +o y)))
13	12	abbidv 1624	. . . . 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 2235	. . . 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 1536	. . 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 4027	. . . 4 |- (z = B -> (A +o z) = (A +o B))
17		rexeq1 1834	. . . . . 6 |- (z = B -> (E.y e. z x = (A +o y) <-> E.y e. B x = (A +o y)))
18	17	abbidv 1624	. . . . 5 |- (z = B -> {x | E.y e. z x = (A +o y)} = {x | E.y e. B x = (A +o y)})
19	18	uneq2d 2235	. . . 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 1536	. . 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 4213	. . . 4 |- (A e. On -> (A +o (/)) = A)
22		rex0 2343	. . . . . . . 8 |- -. E.y e. (/) x = (A +o y)
23	22	nex 1142	. . . . . . 7 |- -. E.xE.y e. (/) x = (A +o y)
24		abn0 2342	. . . . . . . 8 |- ({x | E.y e. (/) x = (A +o y)} =/= (/) <-> E.xE.y e. (/) x = (A +o y))
25	24	necon1bbii 1664	. . . . . . 7 |- (-. E.xE.y e. (/) x = (A +o y) <-> {x | E.y e. (/) x = (A +o y)} = (/))
26	23, 25	mpbi 196	. . . . . 6 |- {x | E.y e. (/) x = (A +o y)} = (/)
27	26	uneq2i 2232	. . . . 5 |- (A u. {x | E.y e. (/) x = (A +o y)}) = (A u. (/))
28		un0 2349	. . . . 5 |- (A u. (/)) = A
29	27, 28	eqtr2i 1543	. . . 4 |- A = (A u. {x | E.y e. (/) x = (A +o y)})
30	21, 29	syl6eq 1570	. . 3 |- (A e. On -> (A +o (/)) = (A u. {x | E.y e. (/) x = (A +o y)}))
31		oasuc 4221	. . . . . 6 |- ((A e. On /\ w e. On) -> (A +o suc w) = suc (A +o w))
32		df-sn 2464	. . . . . . . 8 |- {(A +o w)} = {x | x = (A +o w)}
33		uneq12 2230	. . . . . . . 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 708	. . . . . . 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 3011	. . . . . . 7 |- suc (A +o w) = ((A +o w) u. {(A +o w)})
36		visset 1860	. . . . . . . . . . . . . . . . 17 |- y e. V
37	36	elsuc 3095	. . . . . . . . . . . . . . . 16 |- (y e. suc w <-> (y e. w \/ y = w))
38	37	anbi1i 492	. . . . . . . . . . . . . . 15 |- ((y e. suc w /\ x = (A +o y)) <-> ((y e. w \/ y = w) /\ x = (A +o y)))
39		andir 616	. . . . . . . . . . . . . . 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	bitri 180	. . . . . . . . . . . . . 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 1092	. . . . . . . . . . . . 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 1129	. . . . . . . . . . . . 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	bitri 180	. . . . . . . . . . . 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 1697	. . . . . . . . . . . 12 |- (E.y e. suc wx = (A +o y) <-> E.y(y e. suc w /\ x = (A +o y)))
45		df-rex 1697	. . . . . . . . . . . . 13 |- (E.y e. w x = (A +o y) <-> E.y(y e. w /\ x = (A +o y)))
46		visset 1860	. . . . . . . . . . . . . . 15 |- w e. V
47		opreq2 4027	. . . . . . . . . . . . . . . 16 |- (y = w -> (A +o y) = (A +o w))
48	47	eqeq2d 1533	. . . . . . . . . . . . . . 15 |- (y = w -> (x = (A +o y) <-> x = (A +o w)))
49	46, 48	ceqsexv 1882	. . . . . . . . . . . . . 14 |- (E.y(y = w /\ x = (A +o y)) <-> x = (A +o w))
50	49	bicomi 179	. . . . . . . . . . . . 13 |- (x = (A +o w) <-> E.y(y = w /\ x = (A +o y)))
51	45, 50	orbi12i 264	. . . . . . . . . . . 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	3bitr4i 190	. . . . . . . . . . 11 |- (E.y e. suc wx = (A +o y) <-> (E.y e. w x = (A +o y) \/ x = (A +o w)))
53	52	abbii 1622	. . . . . . . . . 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 2318	. . . . . . . . . 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	eqtr4i 1545	. . . . . . . . 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