Theorem omlimcl 4193

Description: The product of any nonzero ordinal with a limit ordinal is a limit ordinal. Proposition 8.24 of [TakeutiZaring] p. 64.

Assertion

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

Proof of Theorem omlimcl

Step	Hyp	Ref	Expression
1		omcl 4155	. . . . . 6 |- ((A e. On /\ B e. On) -> (A .o B) e. On)
2		eloni 2948	. . . . . 6 |- ((A .o B) e. On -> Ord (A .o B))
3	1, 2	syl 10	. . . . 5 |- ((A e. On /\ B e. On) -> Ord (A .o B))
4		limelon 3022	. . . . 5 |- ((B e. C /\ Lim B) -> B e. On)
5	3, 4	sylan2 451	. . . 4 |- ((A e. On /\ (B e. C /\ Lim B)) -> Ord (A .o B))
6	5	adantr 389	. . 3 |- (((A e. On /\ (B e. C /\ Lim B)) /\ (/) e. A) -> Ord (A .o B))
7		n0i 2275	. . . . . . . . . 10 |- ((/) e. A -> -. A = (/))
8		0ellim 3021	. . . . . . . . . . 11 |- (Lim B -> (/) e. B)
9		n0i 2275	. . . . . . . . . . 11 |- ((/) e. B -> -. B = (/))
10	8, 9	syl 10	. . . . . . . . . 10 |- (Lim B -> -. B = (/))
11	7, 10	anim12i 333	. . . . . . . . 9 |- (((/) e. A /\ Lim B) -> (-. A = (/) /\ -. B = (/)))
12	11	ancoms 436	. . . . . . . 8 |- ((Lim B /\ (/) e. A) -> (-. A = (/) /\ -. B = (/)))
13	12	adantll 392	. . . . . . 7 |- (((B e. C /\ Lim B) /\ (/) e. A) -> (-. A = (/) /\ -. B = (/)))
14	13	adantll 392	. . . . . 6 |- (((A e. On /\ (B e. C /\ Lim B)) /\ (/) e. A) -> (-. A = (/) /\ -. B = (/)))
15		om00 4190	. . . . . . . . . 10 |- ((A e. On /\ B e. On) -> ((A .o B) = (/) <-> (A = (/) \/ B = (/))))
16	15	negbid 609	. . . . . . . . 9 |- ((A e. On /\ B e. On) -> (-. (A .o B) = (/) <-> -. (A = (/) \/ B = (/))))
17		ioran 306	. . . . . . . . 9 |- (-. (A = (/) \/ B = (/)) <-> (-. A = (/) /\ -. B = (/)))
18	16, 17	syl6bb 534	. . . . . . . 8 |- ((A e. On /\ B e. On) -> (-. (A .o B) = (/) <-> (-. A = (/) /\ -. B = (/))))
19	18, 4	sylan2 451	. . . . . . 7 |- ((A e. On /\ (B e. C /\ Lim B)) -> (-. (A .o B) = (/) <-> (-. A = (/) /\ -. B = (/))))
20	19	adantr 389	. . . . . 6 |- (((A e. On /\ (B e. C /\ Lim B)) /\ (/) e. A) -> (-. (A .o B) = (/) <-> (-. A = (/) /\ -. B = (/))))
21	14, 20	mpbird 196	. . . . 5 |- (((A e. On /\ (B e. C /\ Lim B)) /\ (/) e. A) -> -. (A .o B) = (/))
22		eqeq1 1473	. . . . . . . . . . . . . . 15 |- ((A .o B) = suc y -> ((A .o B) = U_x e. B (A .o x) <-> suc y = U_x e. B (A .o x)))
23	22	biimpac 418	. . . . . . . . . . . . . 14 |- (((A .o B) = U_x e. B (A .o x) /\ (A .o B) = suc y) -> suc y = U_x e. B (A .o x))
24		omlim 4152	. . . . . . . . . . . . . 14 |- ((A e. On /\ (B e. C /\ Lim B)) -> (A .o B) = U_x e. B (A .o x))
25	23, 24	sylan 448	. . . . . . . . . . . . 13 |- (((A e. On /\ (B e. C /\ Lim B)) /\ (A .o B) = suc y) -> suc y = U_x e. B (A .o x))
26		visset 1804	. . . . . . . . . . . . . 14 |- y e. V
27	26	sucid 3041	. . . . . . . . . . . . 13 |- y e. suc y
28	25, 27	syl5eleq 1546	. . . . . . . . . . . 12 |- (((A e. On /\ (B e. C /\ Lim B)) /\ (A .o B) = suc y) -> y e. U_x e. B (A .o x))
29		eliun 2560	. . . . . . . . . . . 12 |- (y e. U_x e. B (A .o x) <-> E.x e. B y e. (A .o x))
30	28, 29	sylib 198	. . . . . . . . . . 11 |- (((A e. On /\ (B e. C /\ Lim B)) /\ (A .o B) = suc y) -> E.x e. B y e. (A .o x))
31	30	adantlr 393	. . . . . . . . . 10 |- ((((A e. On /\ (B e. C /\ Lim B)) /\ (/) e. A) /\ (A .o B) = suc y) -> E.x e. B y e. (A .o x))
32		onelon 2962	. . . . . . . . . . . . . . . . . . 19 |- ((B e. On /\ x e. B) -> x e. On)
33	32, 4	sylan 448	. . . . . . . . . . . . . . . . . 18 |- (((B e. C /\ Lim B) /\ x e. B) -> x e. On)
34		onnbtwn 3054	. . . . . . . . . . . . . . . . . . . . 21 |- (x e. On -> -. (x e. B /\ B e. suc x))
35		imnan 242	. . . . . . . . . . . . . . . . . . . . 21 |- ((x e. B -> -. B e. suc x) <-> -. (x e. B /\ B e. suc x))
36	34, 35	sylibr 200	. . . . . . . . . . . . . . . . . . . 20 |- (x e. On -> (x e. B -> -. B e. suc x))
37	36	com12 11	. . . . . . . . . . . . . . . . . . 19 |- (x e. B -> (x e. On -> -. B e. suc x))
38	37	adantl 388	. . . . . . . . . . . . . . . . . 18 |- (((B e. C /\ Lim B) /\ x e. B) -> (x e. On -> -. B e. suc x))
39	33, 38	mpd 26	. . . . . . . . . . . . . . . . 17 |- (((B e. C /\ Lim B) /\ x e. B) -> -. B e. suc x)
40	39	adantll 392	. . . . . . . . . . . . . . . 16 |- (((A e. On /\ (B e. C /\ Lim B)) /\ x e. B) -> -. B e. suc x)
41	40	adantlr 393	. . . . . . . . . . . . . . 15 |- ((((A e. On /\ (B e. C /\ Lim B)) /\ (/) e. A) /\ x e. B) -> -. B e. suc x)
42	41	adantr 389	. . . . . . . . . . . . . 14 |- (((((A e. On /\ (B e. C /\ Lim B)) /\ (/) e. A) /\ x e. B) /\ y e. (A .o x)) -> -. B e. suc x)
43		omcl 4155	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A e. On /\ x e. On) -> (A .o x) e. On)
44		eloni 2948	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A .o x) e. On -> Ord (A .o x))
45		ordsucelsuc 3063	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (Ord (A .o x) -> (y e. (A .o x) <-> suc y e. suc (A .o x)))
46	44, 45	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A .o x) e. On -> (y e. (A .o x) <-> suc y e. suc (A .o x)))
47		oa1suc 4148	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A .o x) e. On -> ((A .o x) +o 1o) = suc (A .o x))
48	47	eleq2d 1533	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A .o x) e. On -> (suc y e. ((A .o x) +o 1o) <-> suc y e. suc (A .o x)))
49	46, 48	bitr4d 529	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A .o x) e. On -> (y e. (A .o x) <-> suc y e. ((A .o x) +o 1o)))
50	43, 49	syl 10	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A e. On /\ x e. On) -> (y e. (A .o x) <-> suc y e. ((A .o x) +o 1o)))
51	50	adantr 389	. . . . . . . . . . . . . . . . . . . . . 22 |- (((A e. On /\ x e. On) /\ (/) e. A) -> (y e. (A .o x) <-> suc y e. ((A .o x) +o 1o)))
52		eloni 2948	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (A e. On -> Ord A)
53		ordgt0ge1 4128	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (Ord A -> ((/) e. A <-> 1o (_ A))
54	52, 53	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (A e. On -> ((/) e. A <-> 1o (_ A))
55	54	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A e. On /\ x e. On) -> ((/) e. A <-> 1o (_ A))
56		1on 4122	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- 1o e. On
57		oaword 4167	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((1o e. On /\ A e. On /\ (A .o x) e. On) -> (1o (_ A <-> ((A .o x) +o 1o) (_ ((A .o x) +o A)))
58	56, 57	mp3an1 900	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((A e. On /\ (A .o x) e. On) -> (1o (_ A <-> ((A .o x) +o 1o) (_ ((A .o x) +o A)))
59	43, 58	syldan 467	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A e. On /\ x e. On) -> (1o (_ A <-> ((A .o x) +o 1o) (_ ((A .o x) +o A)))
60	55, 59	bitrd 526	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A e. On /\ x e. On) -> ((/) e. A <-> ((A .o x) +o 1o) (_ ((A .o x) +o A)))
61	60	biimpa 416	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((A e. On /\ x e. On) /\ (/) e. A) -> ((A .o x) +o 1o) (_ ((A .o x) +o A))
62		omsuc 4149	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A e. On /\ x e. On) -> (A .o suc x) = ((A .o x) +o A))
63	62	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((A e. On /\ x e. On) /\ (/) e. A) -> (A .o suc x) = ((A .o x) +o A))
64	61, 63	sseqtr4d 2088	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((A e. On /\ x e. On) /\ (/) e. A) -> ((A .o x) +o 1o) (_ (A .o suc x))
65	64	sseld 2057	. . . . . . . . . . . . . . . . . . . . . 22 |- (((A e. On /\ x e. On) /\ (/) e. A) -> (suc y e. ((A .o x) +o 1o) -> suc y e. (A .o suc x)))
66	51, 65	sylbid 203	. . . . . . . . . . . . . . . . . . . . 21 |- (((A e. On /\ x e. On) /\ (/) e. A) -> (y e. (A .o x) -> suc y e. (A .o suc x)))
67		eleq1 1526	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A .o B) = suc y -> ((A .o B) e. (A .o suc x) <-> suc y e. (A .o suc x)))
68	67	biimprd 154	. . . . . . . . . . . . . . . . . . . . 21 |- ((A .o B) = suc y -> (suc y e. (A .o suc x) -> (A .o B) e. (A .o suc x)))