Metamath Proof Explorer

Theorem omlimcl

Description: The product of any nonzero ordinal with a limit ordinal is a limit ordinal. Proposition 8.24 of TakeutiZaring p. 64. (Contributed by NM, 25-Dec-2004)

Ref Expression
Assertion omlimcl ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B ∧ ∅ ∈ A → Lim ⁡ A ⋅ 𝑜 B

Proof

Step Hyp Ref Expression
1 limelon ⊢ B ∈ C ∧ Lim ⁡ B → B ∈ On
2 omcl ⊢ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 B ∈ On
3 eloni ⊢ A ⋅ 𝑜 B ∈ On → Ord ⁡ A ⋅ 𝑜 B
4 2 3 syl ⊢ A ∈ On ∧ B ∈ On → Ord ⁡ A ⋅ 𝑜 B
5 1 4 sylan2 ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B → Ord ⁡ A ⋅ 𝑜 B
6 5 adantr ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B ∧ ∅ ∈ A → Ord ⁡ A ⋅ 𝑜 B
7 0ellim ⊢ Lim ⁡ B → ∅ ∈ B
8 n0i ⊢ ∅ ∈ B → ¬ B = ∅
9 7 8 syl ⊢ Lim ⁡ B → ¬ B = ∅
10 n0i ⊢ ∅ ∈ A → ¬ A = ∅
11 9 10 anim12ci ⊢ Lim ⁡ B ∧ ∅ ∈ A → ¬ A = ∅ ∧ ¬ B = ∅
12 11 adantll ⊢ B ∈ C ∧ Lim ⁡ B ∧ ∅ ∈ A → ¬ A = ∅ ∧ ¬ B = ∅
13 12 adantll ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B ∧ ∅ ∈ A → ¬ A = ∅ ∧ ¬ B = ∅
14 om00 ⊢ A ∈ On ∧ B ∈ On → A ⋅ 𝑜 B = ∅ ↔ A = ∅ ∨ B = ∅
15 14 notbid ⊢ A ∈ On ∧ B ∈ On → ¬ A ⋅ 𝑜 B = ∅ ↔ ¬ A = ∅ ∨ B = ∅
16 ioran ⊢ ¬ A = ∅ ∨ B = ∅ ↔ ¬ A = ∅ ∧ ¬ B = ∅
17 15 16 bitrdi ⊢ A ∈ On ∧ B ∈ On → ¬ A ⋅ 𝑜 B = ∅ ↔ ¬ A = ∅ ∧ ¬ B = ∅
18 1 17 sylan2 ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B → ¬ A ⋅ 𝑜 B = ∅ ↔ ¬ A = ∅ ∧ ¬ B = ∅
19 18 adantr ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B ∧ ∅ ∈ A → ¬ A ⋅ 𝑜 B = ∅ ↔ ¬ A = ∅ ∧ ¬ B = ∅
20 13 19 mpbird ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B ∧ ∅ ∈ A → ¬ A ⋅ 𝑜 B = ∅
21 vex ⊢ y ∈ V
22 21 sucid ⊢ y ∈ suc ⁡ y
23 omlim ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B → A ⋅ 𝑜 B = ⋃ x ∈ B A ⋅ 𝑜 x
24 eqeq1 ⊢ A ⋅ 𝑜 B = suc ⁡ y → A ⋅ 𝑜 B = ⋃ x ∈ B A ⋅ 𝑜 x ↔ suc ⁡ y = ⋃ x ∈ B A ⋅ 𝑜 x
25 24 biimpac ⊢ A ⋅ 𝑜 B = ⋃ x ∈ B A ⋅ 𝑜 x ∧ A ⋅ 𝑜 B = suc ⁡ y → suc ⁡ y = ⋃ x ∈ B A ⋅ 𝑜 x
26 23 25 sylan ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B ∧ A ⋅ 𝑜 B = suc ⁡ y → suc ⁡ y = ⋃ x ∈ B A ⋅ 𝑜 x
27 22 26 eleqtrid ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B ∧ A ⋅ 𝑜 B = suc ⁡ y → y ∈ ⋃ x ∈ B A ⋅ 𝑜 x
28 eliun ⊢ y ∈ ⋃ x ∈ B A ⋅ 𝑜 x ↔ ∃ x ∈ B y ∈ A ⋅ 𝑜 x
29 27 28 sylib ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B ∧ A ⋅ 𝑜 B = suc ⁡ y → ∃ x ∈ B y ∈ A ⋅ 𝑜 x
30 29 adantlr ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B ∧ ∅ ∈ A ∧ A ⋅ 𝑜 B = suc ⁡ y → ∃ x ∈ B y ∈ A ⋅ 𝑜 x
31 onelon ⊢ B ∈ On ∧ x ∈ B → x ∈ On
32 1 31 sylan ⊢ B ∈ C ∧ Lim ⁡ B ∧ x ∈ B → x ∈ On
33 onnbtwn ⊢ x ∈ On → ¬ x ∈ B ∧ B ∈ suc ⁡ x
34 imnan ⊢ x ∈ B → ¬ B ∈ suc ⁡ x ↔ ¬ x ∈ B ∧ B ∈ suc ⁡ x
35 33 34 sylibr ⊢ x ∈ On → x ∈ B → ¬ B ∈ suc ⁡ x
36 35 com12 ⊢ x ∈ B → x ∈ On → ¬ B ∈ suc ⁡ x
37 36 adantl ⊢ B ∈ C ∧ Lim ⁡ B ∧ x ∈ B → x ∈ On → ¬ B ∈ suc ⁡ x
38 32 37 mpd ⊢ B ∈ C ∧ Lim ⁡ B ∧ x ∈ B → ¬ B ∈ suc ⁡ x
39 38 ad5ant24 ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B ∧ ∅ ∈ A ∧ x ∈ B ∧ y ∈ A ⋅ 𝑜 x → ¬ B ∈ suc ⁡ x
40 simpl ⊢ B ∈ On ∧ x ∈ B → B ∈ On
41 40 31 jca ⊢ B ∈ On ∧ x ∈ B → B ∈ On ∧ x ∈ On
42 1 41 sylan ⊢ B ∈ C ∧ Lim ⁡ B ∧ x ∈ B → B ∈ On ∧ x ∈ On
43 42 anim2i ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B ∧ x ∈ B → A ∈ On ∧ B ∈ On ∧ x ∈ On
44 43 anassrs ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B ∧ x ∈ B → A ∈ On ∧ B ∈ On ∧ x ∈ On
45 omcl ⊢ A ∈ On ∧ x ∈ On → A ⋅ 𝑜 x ∈ On
46 eloni ⊢ A ⋅ 𝑜 x ∈ On → Ord ⁡ A ⋅ 𝑜 x
47 ordsucelsuc ⊢ Ord ⁡ A ⋅ 𝑜 x → y ∈ A ⋅ 𝑜 x ↔ suc ⁡ y ∈ suc ⁡ A ⋅ 𝑜 x
48 46 47 syl ⊢ A ⋅ 𝑜 x ∈ On → y ∈ A ⋅ 𝑜 x ↔ suc ⁡ y ∈ suc ⁡ A ⋅ 𝑜 x
49 oa1suc ⊢ A ⋅ 𝑜 x ∈ On → A ⋅ 𝑜 x + 𝑜 1 𝑜 = suc ⁡ A ⋅ 𝑜 x
50 49 eleq2d ⊢ A ⋅ 𝑜 x ∈ On → suc ⁡ y ∈ A ⋅ 𝑜 x + 𝑜 1 𝑜 ↔ suc ⁡ y ∈ suc ⁡ A ⋅ 𝑜 x
51 48 50 bitr4d ⊢ A ⋅ 𝑜 x ∈ On → y ∈ A ⋅ 𝑜 x ↔ suc ⁡ y ∈ A ⋅ 𝑜 x + 𝑜 1 𝑜
52 45 51 syl ⊢ A ∈ On ∧ x ∈ On → y ∈ A ⋅ 𝑜 x ↔ suc ⁡ y ∈ A ⋅ 𝑜 x + 𝑜 1 𝑜
53 52 adantr ⊢ A ∈ On ∧ x ∈ On ∧ ∅ ∈ A → y ∈ A ⋅ 𝑜 x ↔ suc ⁡ y ∈ A ⋅ 𝑜 x + 𝑜 1 𝑜
54 eloni ⊢ A ∈ On → Ord ⁡ A
55 ordgt0ge1 ⊢ Ord ⁡ A → ∅ ∈ A ↔ 1 𝑜 ⊆ A
56 54 55 syl ⊢ A ∈ On → ∅ ∈ A ↔ 1 𝑜 ⊆ A
57 56 adantr ⊢ A ∈ On ∧ x ∈ On → ∅ ∈ A ↔ 1 𝑜 ⊆ A
58 1on ⊢ 1 𝑜 ∈ On
59 oaword ⊢ 1 𝑜 ∈ On ∧ A ∈ On ∧ A ⋅ 𝑜 x ∈ On → 1 𝑜 ⊆ A ↔ A ⋅ 𝑜 x + 𝑜 1 𝑜 ⊆ A ⋅ 𝑜 x + 𝑜 A
60 58 59 mp3an1 ⊢ A ∈ On ∧ A ⋅ 𝑜 x ∈ On → 1 𝑜 ⊆ A ↔ A ⋅ 𝑜 x + 𝑜 1 𝑜 ⊆ A ⋅ 𝑜 x + 𝑜 A
61 45 60 syldan ⊢ A ∈ On ∧ x ∈ On → 1 𝑜 ⊆ A ↔ A ⋅ 𝑜 x + 𝑜 1 𝑜 ⊆ A ⋅ 𝑜 x + 𝑜 A
62 57 61 bitrd ⊢ A ∈ On ∧ x ∈ On → ∅ ∈ A ↔ A ⋅ 𝑜 x + 𝑜 1 𝑜 ⊆ A ⋅ 𝑜 x + 𝑜 A
63 62 biimpa ⊢ A ∈ On ∧ x ∈ On ∧ ∅ ∈ A → A ⋅ 𝑜 x + 𝑜 1 𝑜 ⊆ A ⋅ 𝑜 x + 𝑜 A
64 omsuc ⊢ A ∈ On ∧ x ∈ On → A ⋅ 𝑜 suc ⁡ x = A ⋅ 𝑜 x + 𝑜 A
65 64 adantr ⊢ A ∈ On ∧ x ∈ On ∧ ∅ ∈ A → A ⋅ 𝑜 suc ⁡ x = A ⋅ 𝑜 x + 𝑜 A
66 63 65 sseqtrrd ⊢ A ∈ On ∧ x ∈ On ∧ ∅ ∈ A → A ⋅ 𝑜 x + 𝑜 1 𝑜 ⊆ A ⋅ 𝑜 suc ⁡ x
67 66 sseld ⊢ A ∈ On ∧ x ∈ On ∧ ∅ ∈ A → suc ⁡ y ∈ A ⋅ 𝑜 x + 𝑜 1 𝑜 → suc ⁡ y ∈ A ⋅ 𝑜 suc ⁡ x
68 53 67 sylbid ⊢ A ∈ On ∧ x ∈ On ∧ ∅ ∈ A → y ∈ A ⋅ 𝑜 x → suc ⁡ y ∈ A ⋅ 𝑜 suc ⁡ x
69 eleq1 ⊢ A ⋅ 𝑜 B = suc ⁡ y → A ⋅ 𝑜 B ∈ A ⋅ 𝑜 suc ⁡ x ↔ suc ⁡ y ∈ A ⋅ 𝑜 suc ⁡ x
70 69 biimprd ⊢ A ⋅ 𝑜 B = suc ⁡ y → suc ⁡ y ∈ A ⋅ 𝑜 suc ⁡ x → A ⋅ 𝑜 B ∈ A ⋅ 𝑜 suc ⁡ x
71 68 70 syl9 ⊢ A ∈ On ∧ x ∈ On ∧ ∅ ∈ A → A ⋅ 𝑜 B = suc ⁡ y → y ∈ A ⋅ 𝑜 x → A ⋅ 𝑜 B ∈ A ⋅ 𝑜 suc ⁡ x
72 71 com23 ⊢ A ∈ On ∧ x ∈ On ∧ ∅ ∈ A → y ∈ A ⋅ 𝑜 x → A ⋅ 𝑜 B = suc ⁡ y → A ⋅ 𝑜 B ∈ A ⋅ 𝑜 suc ⁡ x
73 72 adantlrl ⊢ A ∈ On ∧ B ∈ On ∧ x ∈ On ∧ ∅ ∈ A → y ∈ A ⋅ 𝑜 x → A ⋅ 𝑜 B = suc ⁡ y → A ⋅ 𝑜 B ∈ A ⋅ 𝑜 suc ⁡ x
74 sucelon ⊢ x ∈ On ↔ suc ⁡ x ∈ On
75 omord ⊢ B ∈ On ∧ suc ⁡ x ∈ On ∧ A ∈ On → B ∈ suc ⁡ x ∧ ∅ ∈ A ↔ A ⋅ 𝑜 B ∈ A ⋅ 𝑜 suc ⁡ x
76 simpl ⊢ B ∈ suc ⁡ x ∧ ∅ ∈ A → B ∈ suc ⁡ x
77 75 76 syl6bir ⊢ B ∈ On ∧ suc ⁡ x ∈ On ∧ A ∈ On → A ⋅ 𝑜 B ∈ A ⋅ 𝑜 suc ⁡ x → B ∈ suc ⁡ x
78 74 77 syl3an2b ⊢ B ∈ On ∧ x ∈ On ∧ A ∈ On → A ⋅ 𝑜 B ∈ A ⋅ 𝑜 suc ⁡ x → B ∈ suc ⁡ x
79 78 3comr ⊢ A ∈ On ∧ B ∈ On ∧ x ∈ On → A ⋅ 𝑜 B ∈ A ⋅ 𝑜 suc ⁡ x → B ∈ suc ⁡ x
80 79 3expb ⊢ A ∈ On ∧ B ∈ On ∧ x ∈ On → A ⋅ 𝑜 B ∈ A ⋅ 𝑜 suc ⁡ x → B ∈ suc ⁡ x
81 80 adantr ⊢ A ∈ On ∧ B ∈ On ∧ x ∈ On ∧ ∅ ∈ A → A ⋅ 𝑜 B ∈ A ⋅ 𝑜 suc ⁡ x → B ∈ suc ⁡ x
82 73 81 syl6d ⊢ A ∈ On ∧ B ∈ On ∧ x ∈ On ∧ ∅ ∈ A → y ∈ A ⋅ 𝑜 x → A ⋅ 𝑜 B = suc ⁡ y → B ∈ suc ⁡ x
83 44 82 sylan ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B ∧ x ∈ B ∧ ∅ ∈ A → y ∈ A ⋅ 𝑜 x → A ⋅ 𝑜 B = suc ⁡ y → B ∈ suc ⁡ x
84 83 an32s ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B ∧ ∅ ∈ A ∧ x ∈ B → y ∈ A ⋅ 𝑜 x → A ⋅ 𝑜 B = suc ⁡ y → B ∈ suc ⁡ x
85 84 imp ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B ∧ ∅ ∈ A ∧ x ∈ B ∧ y ∈ A ⋅ 𝑜 x → A ⋅ 𝑜 B = suc ⁡ y → B ∈ suc ⁡ x
86 39 85 mtod ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B ∧ ∅ ∈ A ∧ x ∈ B ∧ y ∈ A ⋅ 𝑜 x → ¬ A ⋅ 𝑜 B = suc ⁡ y
87 86 rexlimdva2 ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B ∧ ∅ ∈ A → ∃ x ∈ B y ∈ A ⋅ 𝑜 x → ¬ A ⋅ 𝑜 B = suc ⁡ y
88 87 adantr ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B ∧ ∅ ∈ A ∧ A ⋅ 𝑜 B = suc ⁡ y → ∃ x ∈ B y ∈ A ⋅ 𝑜 x → ¬ A ⋅ 𝑜 B = suc ⁡ y
89 30 88 mpd ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B ∧ ∅ ∈ A ∧ A ⋅ 𝑜 B = suc ⁡ y → ¬ A ⋅ 𝑜 B = suc ⁡ y
90 89 pm2.01da ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B ∧ ∅ ∈ A → ¬ A ⋅ 𝑜 B = suc ⁡ y
91 90 adantr ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B ∧ ∅ ∈ A ∧ y ∈ On → ¬ A ⋅ 𝑜 B = suc ⁡ y
92 91 nrexdv ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B ∧ ∅ ∈ A → ¬ ∃ y ∈ On A ⋅ 𝑜 B = suc ⁡ y
93 ioran ⊢ ¬ A ⋅ 𝑜 B = ∅ ∨ ∃ y ∈ On A ⋅ 𝑜 B = suc ⁡ y ↔ ¬ A ⋅ 𝑜 B = ∅ ∧ ¬ ∃ y ∈ On A ⋅ 𝑜 B = suc ⁡ y
94 20 92 93 sylanbrc ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B ∧ ∅ ∈ A → ¬ A ⋅ 𝑜 B = ∅ ∨ ∃ y ∈ On A ⋅ 𝑜 B = suc ⁡ y
95 dflim3 ⊢ Lim ⁡ A ⋅ 𝑜 B ↔ Ord ⁡ A ⋅ 𝑜 B ∧ ¬ A ⋅ 𝑜 B = ∅ ∨ ∃ y ∈ On A ⋅ 𝑜 B = suc ⁡ y
96 6 94 95 sylanbrc ⊢ A ∈ On ∧ B ∈ C ∧ Lim ⁡ B ∧ ∅ ∈ A → Lim ⁡ A ⋅ 𝑜 B