Theorem oalimcl 4252

Description: The ordinal sum with a limit ordinal is a limit ordinal. Proposition 8.11 of [TakeutiZaring] p. 60.

Assertion

Ref	Expression
oalimcl	|- ((A e. On /\ (B e. C /\ Lim B)) -> Lim (A +o B))

Proof of Theorem oalimcl

Step	Hyp	Ref	Expression
1		oacl 4228	. . . . 5 |- ((A e. On /\ B e. On) -> (A +o B) e. On)
2		eloni 3015	. . . . 5 |- ((A +o B) e. On -> Ord (A +o B))
3	1, 2	syl 10	. . . 4 |- ((A e. On /\ B e. On) -> Ord (A +o B))
4		limelon 3089	. . . 4 |- ((B e. C /\ Lim B) -> B e. On)
5	3, 4	sylan2 462	. . 3 |- ((A e. On /\ (B e. C /\ Lim B)) -> Ord (A +o B))
6		0ellim 3088	. . . . . . . 8 |- (Lim B -> (/) e. B)
7		n0i 2336	. . . . . . . 8 |- ((/) e. B -> -. B = (/))
8	6, 7	syl 10	. . . . . . 7 |- (Lim B -> -. B = (/))
9	8	ad2antll 416	. . . . . 6 |- ((A e. On /\ (B e. C /\ Lim B)) -> -. B = (/))
10		oa00 4251	. . . . . . . . 9 |- ((A e. On /\ B e. On) -> ((A +o B) = (/) <-> (A = (/) /\ B = (/))))
11		pm3.27 330	. . . . . . . . 9 |- ((A = (/) /\ B = (/)) -> B = (/))
12	10, 11	syl6bi 221	. . . . . . . 8 |- ((A e. On /\ B e. On) -> ((A +o B) = (/) -> B = (/)))
13	12	con3d 99	. . . . . . 7 |- ((A e. On /\ B e. On) -> (-. B = (/) -> -. (A +o B) = (/)))
14	13, 4	sylan2 462	. . . . . 6 |- ((A e. On /\ (B e. C /\ Lim B)) -> (-. B = (/) -> -. (A +o B) = (/)))
15	9, 14	mpd 26	. . . . 5 |- ((A e. On /\ (B e. C /\ Lim B)) -> -. (A +o B) = (/))
16		eqeq1 1528	. . . . . . . . . . . . . 14 |- ((A +o B) = suc y -> ((A +o B) = U_x e. B (A +o x) <-> suc y = U_x e. B (A +o x)))
17		oalim 4225	. . . . . . . . . . . . . 14 |- ((A e. On /\ (B e. C /\ Lim B)) -> (A +o B) = U_x e. B (A +o x))
18	16, 17	syl5bi 215	. . . . . . . . . . . . 13 |- ((A +o B) = suc y -> ((A e. On /\ (B e. C /\ Lim B)) -> suc y = U_x e. B (A +o x)))
19	18	imp 357	. . . . . . . . . . . 12 |- (((A +o B) = suc y /\ (A e. On /\ (B e. C /\ Lim B))) -> suc y = U_x e. B (A +o x))
20		visset 1860	. . . . . . . . . . . . 13 |- y e. V
21	20	sucid 3108	. . . . . . . . . . . 12 |- y e. suc y
22	19, 21	syl5eleq 1601	. . . . . . . . . . 11 |- (((A +o B) = suc y /\ (A e. On /\ (B e. C /\ Lim B))) -> y e. U_x e. B (A +o x))
23		eliun 2624	. . . . . . . . . . 11 |- (y e. U_x e. B (A +o x) <-> E.x e. B y e. (A +o x))
24	22, 23	sylib 205	. . . . . . . . . 10 |- (((A +o B) = suc y /\ (A e. On /\ (B e. C /\ Lim B))) -> E.x e. B y e. (A +o x))
25		onelon 3029	. . . . . . . . . . . . . . . . . 18 |- ((B e. On /\ x e. B) -> x e. On)
26	25, 4	sylan 459	. . . . . . . . . . . . . . . . 17 |- (((B e. C /\ Lim B) /\ x e. B) -> x e. On)
27		onnbtwn 3121	. . . . . . . . . . . . . . . . . . . 20 |- (x e. On -> -. (x e. B /\ B e. suc x))
28		imnan 249	. . . . . . . . . . . . . . . . . . . 20 |- ((x e. B -> -. B e. suc x) <-> -. (x e. B /\ B e. suc x))
29	27, 28	sylibr 207	. . . . . . . . . . . . . . . . . . 19 |- (x e. On -> (x e. B -> -. B e. suc x))
30	29	com12 11	. . . . . . . . . . . . . . . . . 18 |- (x e. B -> (x e. On -> -. B e. suc x))
31	30	adantl 397	. . . . . . . . . . . . . . . . 17 |- (((B e. C /\ Lim B) /\ x e. B) -> (x e. On -> -. B e. suc x))
32	26, 31	mpd 26	. . . . . . . . . . . . . . . 16 |- (((B e. C /\ Lim B) /\ x e. B) -> -. B e. suc x)
33	32	ad2antrl 415	. . . . . . . . . . . . . . 15 |- ((A e. On /\ (((B e. C /\ Lim B) /\ x e. B) /\ y e. (A +o x))) -> -. B e. suc x)
34		oacl 4228	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A e. On /\ x e. On) -> (A +o x) e. On)
35		eloni 3015	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A +o x) e. On -> Ord (A +o x))
36		ordsucelsuc 3130	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (Ord (A +o x) -> (y e. (A +o x) <-> suc y e. suc (A +o x)))
37	34, 35, 36	3syl 20	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A e. On /\ x e. On) -> (y e. (A +o x) <-> suc y e. suc (A +o x)))
38		oasuc 4221	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A e. On /\ x e. On) -> (A +o suc x) = suc (A +o x))
39	38	eleq2d 1588	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A e. On /\ x e. On) -> (suc y e. (A +o suc x) <-> suc y e. suc (A +o x)))
40	37, 39	bitr4d 542	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A e. On /\ x e. On) -> (y e. (A +o x) <-> suc y e. (A +o suc x)))
41	40, 26	sylan2 462	. . . . . . . . . . . . . . . . . . . . 21 |- ((A e. On /\ ((B e. C /\ Lim B) /\ x e. B)) -> (y e. (A +o x) <-> suc y e. (A +o suc x)))
42		eleq1 1581	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A +o B) = suc y -> ((A +o B) e. (A +o suc x) <-> suc y e. (A +o suc x)))
43	42	bicomd 532	. . . . . . . . . . . . . . . . . . . . 21 |- ((A +o B) = suc y -> (suc y e. (A +o suc x) <-> (A +o B) e. (A +o suc x)))
44	41, 43	sylan9bbr 552	. . . . . . . . . . . . . . . . . . . 20 |- (((A +o B) = suc y /\ (A e. On /\ ((B e. C /\ Lim B) /\ x e. B))) -> (y e. (A +o x) <-> (A +o B) e. (A +o suc x)))
45		oaord 4239	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((B e. On /\ suc x e. On /\ A e. On) -> (B e. suc x <-> (A +o B) e. (A +o suc x)))
46	45	3expa 845	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((B e. On /\ suc x e. On) /\ A e. On) -> (B e. suc x <-> (A +o B) e. (A +o suc x)))
47	4	adantr 398	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((B e. C /\ Lim B) /\ x e. B) -> B e. On)
48		sucelon 3125	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x e. On <-> suc x e. On)
49	26, 48	sylib 205	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((B e. C /\ Lim B) /\ x e. B) -> suc x e. On)
50	47, 49	jca 295	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((B e. C /\ Lim B) /\ x e. B) -> (B e. On /\ suc x e. On))
51	46, 50	sylan 459	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((B e. C /\ Lim B) /\ x e. B) /\ A e. On) -> (B e. suc x <-> (A +o B) e. (A +o suc x)))
52	51	ancoms 447	. . . . . . . . . . . . . . . . . . . . 21 |- ((A e. On /\ ((B e. C /\ Lim B) /\ x e. B)) -> (B e. suc x <-> (A +o B) e. (A +o suc x)))
53	52	adantl 397	. . . . . . . . . . . . . . . . . . . 20 |- (((A +o B) = suc y /\ (A e. On /\ ((B e. C /\ Lim B) /\ x e. B))) -> (B e. suc x <-> (A +o B) e. (A +o suc x)))
54	44, 53	bitr4d 542	. . . . . . . . . . . . . . . . . . 19 |- (((A +o B) = suc y /\ (A e. On /\ ((B e. C /\ Lim B) /\ x e. B))) -> (y e. (A +o x) <-> B e. suc x))
55	54	biimpd 160	. . . . . . . . . . . . . . . . . 18 |- (((A +o B) = suc y /\ (A e. On /\ ((B e. C /\ Lim B) /\ x e. B))) -> (y e. (A +o x) -> B e. suc x))
56	55	exp32 386	. . . . . . . . . . . . . . . . 17 |- ((A +o B) = suc y -> (A e. On -> (((B e. C /\ Lim B) /\ x e. B) -> (y e. (A +o x) -> B e. suc x))))
57	56	com4l 39	. . . . . . . . . . . . . . . 16 |- (A e. On -> (((B e. C /\ Lim B) /\ x e. B) -> (y e. (A +o x) -> ((A +o B) = suc y -> B e. suc x))))
58	57	imp32 370	. . . . . . . . . . . . . . 15 |- ((A e. On /\ (((B e. C /\ Lim B) /\ x e. B) /\ y e. (A +o x))) -> ((A +o B) = suc y -> B e. suc x))
59	33, 58	mtod 114	. . . . . . . . . . . . . 14 |- ((A e. On /\ (((B e. C /\ Lim B) /\ x e. B) /\ y e. (A +o x))) -> -. (A +o B) = suc y)
60	59	exp44 394	. . . . . . . . . . . . 13 |- (A e. On -> ((B e. C /\ Lim B) -> (x e. B -> (y e. (A +o x) -> -. (A +o B) = suc y))))
61	60	imp 357	. . . . . . . . . . . 12 |- ((A e. On /\ (B e. C /\ Lim B)) -> (x e. B -> (y e. (A +o x) -> -. (A +o B) = suc y)))
62	61	r19.23adv 1793	. . . . . . . . . . 11 |- ((A e. On /\ (B e. C /\ Lim B)) -> (E.x e. B y e. (A +o x) -> -. (A +o B) = suc y))
63	62	adantl 397	. . . . . . . . . 10 |- (((A +o B) = suc y /\ (A e. On /\ (B e. C /\ Lim B))) -> (E.x e. B y e. (A +o x) -> -. (A +o B) = suc y))
64	24, 63	mpd 26	. . . . . . . . 9 |- (((A +o B) = suc y /\ (A e. On /\ (B e. C /\ Lim B))