Theorem oarec 4332

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 1833	. . . . . 6 |- (z = (/) -> (E.y e. z x = (A +o y) <-> E.y e. (/) x = (A +o y)))
3	2	abbidv 1620	. . . . 5 |- (z = (/) -> {x | E.y e. z x = (A +o y)} = {x | E.y e. (/) x = (A +o y)})
4	3	uneq2d 2236	. . . 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 1532	. . 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 1833	. . . . . 6 |- (z = w -> (E.y e. z x = (A +o y) <-> E.y e. w x = (A +o y)))
8	7	abbidv 1620	. . . . 5 |- (z = w -> {x | E.y e. z x = (A +o y)} = {x | E.y e. w x = (A +o y)})
9	8	uneq2d 2236	. . . 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 1532	. . 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 1833	. . . . . 6 |- (z = suc w -> (E.y e. z x = (A +o y) <-> E.y e. suc wx = (A +o y)))
13	12	abbidv 1620	. . . . 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 2236	. . . 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 1532	. . 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 1833	. . . . . 6 |- (z = B -> (E.y e. z x = (A +o y) <-> E.y e. B x = (A +o y)))
18	17	abbidv 1620	. . . . 5 |- (z = B -> {x | E.y e. z x = (A +o y)} = {x | E.y e. B x = (A +o y)})
19	18	uneq2d 2236	. . . 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 1532	. . 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 4291	. . . 4 |- (A e. On -> (A +o (/)) = A)
22		rex0 2344	. . . . . . . 8 |- -. E.y e. (/) x = (A +o y)
23	22	nex 1137	. . . . . . 7 |- -. E.xE.y e. (/) x = (A +o y)
24		abn0 2343	. . . . . . . 8 |- ({x | E.y e. (/) x = (A +o y)} =/= (/) <-> E.xE.y e. (/) x = (A +o y))
25	24	necon1bbii 1661	. . . . . . 7 |- (-. E.xE.y e. (/) x = (A +o y) <-> {x | E.y e. (/) x = (A +o y)} = (/))
26	23, 25	mpbi 187	. . . . . 6 |- {x | E.y e. (/) x = (A +o y)} = (/)
27	26	uneq2i 2233	. . . . 5 |- (A u. {x | E.y e. (/) x = (A +o y)}) = (A u. (/))
28		un0 2350	. . . . 5 |- (A u. (/)) = A
29	27, 28	eqtr2i 1539	. . . 4 |- A = (A u. {x | E.y e. (/) x = (A +o y)})
30	21, 29	syl6eq 1566	. . 3 |- (A e. On -> (A +o (/)) = (A u. {x | E.y e. (/) x = (A +o y)}))
31		oasuc 4299	. . . . . 6 |- ((A e. On /\ w e. On) -> (A +o suc w) = suc (A +o w))
32		df-sn 2470	. . . . . . . 8 |- {(A +o w)} = {x | x = (A +o w)}
33		uneq12 2231	. . . . . . . 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 700	. . . . . . 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 2981	. . . . . . 7 |- suc (A +o w) = ((A +o w) u. {(A +o w)})
36		visset 1859	. . . . . . . . . . . . . . . . 17 |- y e. V
37	36	elsuc 3042	. . . . . . . . . . . . . . . 16 |- (y e. suc w <-> (y e. w \/ y = w))
38	37	anbi1i 484	. . . . . . . . . . . . . . 15 |- ((y e. suc w /\ x = (A +o y)) <-> ((y e. w \/ y = w) /\ x = (A +o y)))
39		andir 608	. . . . . . . . . . . . . . 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 171	. . . . . . . . . . . . . 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 1087	. . . . . . . . . . . . 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 1124	. . . . . . . . . . . . 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 171	. . . . . . . . . . . 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 1696	. . . . . . . . . . . 12 |- (E.y e. suc wx = (A +o y) <-> E.y(y e. suc w /\ x = (A +o y)))
45		df-rex 1696	. . . . . . . . . . . . 13 |- (E.y e. w x = (A +o y) <-> E.y(y e. w /\ x = (A +o y)))
46		visset 1859	. . . . . . . . . . . . . . 15 |- w e. V
47		opreq2 4027	. . . . . . . . . . . . . . . 16 |- (y = w -> (A +o y) = (A +o w))
48	47	eqeq2d 1529	. . . . . . . . . . . . . . 15 |- (y = w -> (x = (A +o y) <-> x = (A +o w)))
49	46, 48	ceqsexv 1881	. . . . . . . . . . . . . 14 |- (E.y(y = w /\ x = (A +o y)) <-> x = (A +o w))
50	49	bicomi 170	. . . . . . . . . . . . 13 |- (x = (A +o w) <-> E.y(y = w /\ x = (A +o y)))
51	45, 50	orbi12i 255	. . . . . . . . . . . 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 181	. . . . . . . . . . 11 |- (E.y e. suc wx = (A +o y) <-> (E.y e. w x = (A +o y) \/ x = (A +o w)))
53	52	abbii 1618	. . . . . . . . . 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 2319	. . . . . . . . . 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 1541	. . . . . . . . 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 2233	. . . . . . . 8 |- (A u. {x | E.y e. suc wx = (A +o y)}) = (A u. ({x | E.y e. w x = (A +o y)} u. {x | x = (A +o w)}))
57		unass 2239	. . . . . . . 8 |- ((A u. {x | E.y e. w x = (A +o y)}) u. {x | x = (A +o w)}) = (A u. ({x | E.y e. w x = (A +o y)} u. {x | x = (A +o w)}))
58	56, 57	eqtr4i 1541	. . . . . . 7 |- (A u. {x | E.y e. suc wx = (A +o y)}) = ((A u. {x | E.y e. w x = (A +o y)}) u. {x | x = (A +o w)})
59	34, 35, 58	3eqtr4g 1574	. . . . . 6 |- ((A +o w) = (A u. {x | E.y e. w x = (A +o y)}) -> suc (A +o w) = (A u. {x | E.y e. suc wx = (A +o y)}))
60	31, 59	sylan9eq 1570	. . . . 5 |- (((A e. On /\ w e. On) /\ (A +o w) = (A u. {x | E.y e. w x = (A +o y)})) -> (A +o suc w) = (A u. {x | E.y e. suc wx = (A +o y)}))
61	60	exp31 376	. . . 4 |- (A e. On -> (w e. On -> ((A +o w) = (A u. {x | E.y e. w x = (A +o y)}) -> (A +o suc w) = (A u. {x | E.y e. suc wx = (A +o y)}))))
62	61	com12 11	. . 3 |- (w e. On -> (A e. On -> ((A +o w) = (A u. {x | E.y e. w x = (A +o y)}) -> (A +o suc w) = (A u. {x | E.y e. suc wx = (A +o y)}))))
63		visset 1859	. . . . . . . 8 |- z e. V
64		oalim 4303	. . . . . . . 8 |- ((A e. On /\ (z e. V /\ Lim z)) -> (A +o z) = U_w e. z (A +o w))
65	63, 64	mpanr1 713	. . . . . . 7 |- ((A e. On /\ Lim z) -> (A +o z) = U_w e. z (A +o w))
66	65	ancoms 438	. . . . . 6 |- ((Lim z /\ A e. On) -> (A +o z) = U_w e. z (A +o w))
67	66	adantr 389	. . . . 5 |- (((Lim z /\ A e. On) /\ A.w e. z (A +o w) = (A u. {x | E.y e. w x = (A +o y)})) -> (A +o z) = U_w e. z (A +o w))
68		iuneq2 2646	. . . . . 6 |- (A.w e. z (A +o w) = (A u. {x | E.y e. w x = (A +o y)}) -> U_w e. z (A +o w) = U_w e. z (A u. {x | E.y e. w x = (A +o y)}))
69	68	adantl 388	. . . . 5 |- (((Lim z /\ A e. On) /\ A.w e. z (A +o w) = (A u. {x | E.y e. w x = (A +o y)})) -> U_w e. z (A +o w) = U_w e. z (A u. {x | E.y e. w x = (A +o y)}))
70		0ellim 3035	. . . . . . . . 9 |- (Lim z -> (/) e. z)
71		ne0i 2338	. . . . . . . . 9 |- ((/) e. z -> z =/= (/))
72		iunconst 2640	. . . . . . . . 9 |- (z =/= (/) -> U_w e. z A = A)
73	70, 71, 72	3syl 20	. . . . . . . 8 |- (Lim z -> U_w e. z A = A)
74		limord 3032	. . . . . . . . . . . . . . . . . 18 |- (Lim z -> Ord z)
75		ordtr1 3018	. . . . . . . . . . . . . . . . . 18 |- (Ord z -> ((y e. w /\ w e. z) -> y e. z))
76	74, 75	syl 10	. . . . . . . . . . . . . . . . 17 |- (Lim z -> ((y e. w /\ w e. z) -> y e. z))
77	76	exp3a 374	. . . . . . . . . . . . . . . 16 |- (Lim z -> (y e. w -> (w e. z -> y e. z)))
78	77	com23 32	. . . . . . . . . . . . . . 15 |- (Lim z -> (w e. z -> (y e. w -> y e. z)))
79	78	imp 348	. . . . . . . . . . . . . 14 |- ((Lim z /\ w e. z) -> (y e. w -> y e. z))
80	79	anim1d 563	. . . . . . . . . . . . 13 |- ((Lim z /\ w e. z) -> ((y e. w /\ x = (A +o y)) -> (y e. z /\ x = (A +o y))))
81	80	r19.22dv2 1782	. . . . . . . . . . . 12 |- ((Lim z /\ w e. z) -> (E.y e. w x = (A +o y) -> E.y e. z x = (A +o y)))
82	81	r19.23adva 1793	. . . . . . . . . . 11 |- (Lim z -> (E.w e. z E.y e. w x = (A +o y) -> E.y e. z x = (A +o y)))
83		ax-17 1007	. . . . . . . . . . . 12 |- (Lim z -> A.yLim z)
84		ax-17 1007	. . . . . . . . . . . . 13 |- (w e. z -> A.y w e. z)
85		hbre1 1735	. . . . . . . . . . . . 13 |- (E.y e. w x = (A +o y) -> A.yE.y e. w x = (A +o y))
86	84, 85	hbrex 1734	. . . . . . . . . . . 12 |- (E.w e. z E.y e. w x = (A +o y) -> A.yE.w e. z E.y e. w x = (A +o y))
87		limsuc 3203	. . . . . . . . . . . . . . . . 17 |- (Lim z -> (y e. z <-> suc y e. z))
88	87	biimpd 151	. . . . . . . . . . . . . . . 16 |- (Lim z -> (y e. z -> suc y e. z))
89		sucidg 3052	. . . . . . . . . . . . . . . . 17 |- (y e. z -> y e. suc y)
90	89	a1i 8	. . . . . . . . . . . . . . . 16 |- (Lim z -> (y e. z -> y e. suc y))
91	88, 90	jcad 603	. . . . . . . . . . . . . . 15 |- (Lim z -> (y e. z -> (suc y e. z /\ y e. suc y)))
92	91	anim1d 563	. . . . . . . . . . . . . 14 |- (Lim z -> ((y e. z /\ x = (A +o y)) -> ((suc y e. z /\ y e. suc y) /\ x = (A +o y))))
93		eleq2 1578	. . . . . . . . . . . . . . . . . 18 |- (w = suc y -> (y e. w <-> y e. suc y))
94	93	anbi1d 620	. . . . . . . . . . . . . . . . 17 |- (w = suc y -> ((y e. w /\ x = (A +o y)) <-> (y e. suc y /\ x = (A +o y))))
95	94	rcla4ev 1923	. . . . . . . . . . . . . . . 16 |- ((suc y e. z /\ (y e. suc y /\ x = (A +o y))) -> E.w e. z (y e. w /\ x = (A +o y)))
96		ra4e 1741	. . . . . . . . . . . . . . . . 17 |- ((y e. w /\ x = (A +o y)) -> E.y e. w x = (A +o y))
97	96	r19.22si 1780	. . . . . . . . . . . . . . . 16 |- (E.w e. z (y e. w /\ x = (A +o y)) -> E.w e. z E.y e. w x = (A +o y))
98	95, 97	syl 10	. . . . . . . . . . . . . . 15 |- ((suc y e. z /\ (y e. suc y /\ x = (A +o y))) -> E.w e. z E.y e. w x = (A +o y))
99	98	anassrs 443	. . . . . . . . . . . . . 14 |- (((suc y e. z /\ y e. suc y) /\ x = (A +o y)) -> E.w e. z E.y e. w x = (A +o y))
100	92, 99	syl6 22	. . . . . . . . . . . . 13 |- (Lim z -> ((y e. z /\ x = (A +o y)) -> E.w e. z E.y e. w x = (A +o y)))
101	100	exp3a 374	. . . . . . . . . . . 12 |- (Lim z -> (y e. z -> (x = (A +o y) -> E.w e. z E.y e. w x = (A +o y))))
102	83, 86, 101	r19.23ad 1791	. . . . . . . . . . 11 |- (Lim z -> (E.y e. z x = (A +o y) -> E.w e. z E.y e. w x = (A +o y)))
103	82, 102	impbid 519	. . . . . . . . . 10 |- (Lim z -> (E.w e. z E.y e. w x = (A +o y) <-> E.y e. z x = (A +o y)))
104	103	abbidv 1620	. . . . . . . . 9 |- (Lim z -> {x | E.w e. z E.y e. w x = (A +o y)} = {x | E.y e. z x = (A +o y)})
105		iunab 2665	. . . . . . . . 9 |- U_w e. z {x | E.y e. w x = (A +o y)} = {x | E.w e. z E.y e. w x = (A +o y)}
106	104, 105	syl5eq 1562	. . . . . . . 8 |- (Lim z -> U_w e. z {x | E.y e. w x = (A +o y)} = {x | E.y e. z x = (A +o y)})
107	73, 106	uneq12d 2237	. . . . . . 7 |- (Lim z -> (U_w e. z A u. U_w e. z {x | E.y e. w x = (A +o y)}) = (A u. {x | E.y e. z x = (A +o y)}))
108		iunun 2683	. . . . . . 7 |- U_w e. z (A u. {x | E.y e. w x = (A +o y)}) = (U_w e. z A u. U_w e. z {x | E.y e. w x = (A +o y)})
109	107, 108	syl5eq 1562	. . . . . 6 |- (Lim z -> U_w e. z (A u. {x | E.y e. w x = (A +o y)}) = (A u. {x | E.y e. z x = (A +o y)}))
110	109	ad2antrr 404	. . . . 5 |- (((Lim z /\ A e. On) /\ A.w e. z (A +o w) = (A u. {x | E.y e. w x = (A +o y)})) -> U_w e. z (A u. {x | E.y e. w x = (A +o y)}) = (A u. {x | E.y e. z x = (A +o y)}))
111	67, 69, 110	3eqtrd 1554	. . . 4 |- (((Lim z /\ A e. On) /\ A.w e. z (A +o w) = (A u. {x | E.y e. w x = (A +o y)})) -> (A +o z) = (A u. {x | E.y e. z x = (A +o y)}))
112	111	exp31 376	. . 3 |- (Lim z -> (A e. On -> (A.w e. z (A +o w) = (A u. {x | E.y e. w x = (A +o y)}) -> (A +o z) = (A u. {x | E.y e. z x = (A +o y)}))))
113	5, 10, 15, 20, 30, 62, 112	tfinds3 3217	. 2 |- (B e. On -> (A e. On -> (A +o B) = (A u. {x | E.y e. B x = (A +o y)})))
114	113	impcom 349	1 |- ((A e. On /\ B e. On) -> (A +o B) = (A u. {x | E.y e. B x = (A +o y)}))

Syntax hints:  -. wn 2   -> wi 3   \/ wo 220   /\ wa 221   = wceq 992   e. wcel 994  E.wex 1016  {cab 1505   =/= wne 1628  A.wral 1691  E.wrex 1692  Vcvv 1857   u. cun 2097  (/)c0 2332  {csn 2467  U_ciun 2633  Ord word 2974  Oncon0 2975  Lim wlim 2976  suc csuc 2977  (class class class)co 4021   +o coa 4266

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-9 1001  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-rep 2767  ax-sep 2777  ax-nul 2784  ax-pow 2818  ax-pr 2855  ax-un 3089

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 782  df-3an 783  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-ral 1695  df-rex 1696  df-rab 1698  df-v 1858  df-sbc 1987  df-csb 2052  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-if 2416  df-pw 2459  df-sn 2470  df-pr 2471  df-tp 2473  df-op 2474  df-uni 2570  df-iun 2635  df-br 2693  df-opab 2741  df-tr 2755  df-eprel 2910  df-id 2913  df-po 2918  df-so 2929  df-fr 2947  df-we 2962  df-ord 2978  df-on 2979  df-lim 2980  df-suc 2981  df-xp 3265  df-rel 3266  df-cnv 3267  df-co 3268  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fun 3273  df-fn 3274  df-fv 3279  df-opr 4023  df-oprab 4024  df-rdg 4233  df-oadd 4271

Copyright terms: Public domain