| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | limord 6443 | . . . . 5
⊢ (Lim
𝐴 → Ord 𝐴) | 
| 2 |  | ordeleqon 7803 | . . . . . . 7
⊢ (Ord
𝐴 ↔ (𝐴 ∈ On ∨ 𝐴 = On)) | 
| 3 | 2 | biimpi 216 | . . . . . 6
⊢ (Ord
𝐴 → (𝐴 ∈ On ∨ 𝐴 = On)) | 
| 4 | 3 | orcomd 871 | . . . . 5
⊢ (Ord
𝐴 → (𝐴 = On ∨ 𝐴 ∈ On)) | 
| 5 | 1, 4 | syl 17 | . . . 4
⊢ (Lim
𝐴 → (𝐴 = On ∨ 𝐴 ∈ On)) | 
| 6 | 5 | pm4.71ri 560 | . . 3
⊢ (Lim
𝐴 ↔ ((𝐴 = On ∨ 𝐴 ∈ On) ∧ Lim 𝐴)) | 
| 7 |  | andir 1010 | . . 3
⊢ (((𝐴 = On ∨ 𝐴 ∈ On) ∧ Lim 𝐴) ↔ ((𝐴 = On ∧ Lim 𝐴) ∨ (𝐴 ∈ On ∧ Lim 𝐴))) | 
| 8 | 6, 7 | bitri 275 | . 2
⊢ (Lim
𝐴 ↔ ((𝐴 = On ∧ Lim 𝐴) ∨ (𝐴 ∈ On ∧ Lim 𝐴))) | 
| 9 |  | limon 7857 | . . . . 5
⊢ Lim
On | 
| 10 |  | limeq 6395 | . . . . 5
⊢ (𝐴 = On → (Lim 𝐴 ↔ Lim
On)) | 
| 11 | 9, 10 | mpbiri 258 | . . . 4
⊢ (𝐴 = On → Lim 𝐴) | 
| 12 | 11 | pm4.71i 559 | . . 3
⊢ (𝐴 = On ↔ (𝐴 = On ∧ Lim 𝐴)) | 
| 13 | 12 | orbi1i 913 | . 2
⊢ ((𝐴 = On ∨ (𝐴 ∈ On ∧ Lim 𝐴)) ↔ ((𝐴 = On ∧ Lim 𝐴) ∨ (𝐴 ∈ On ∧ Lim 𝐴))) | 
| 14 |  | simpl 482 | . . . . . 6
⊢ ((𝐴 ∈ On ∧ Lim 𝐴) → 𝐴 ∈ On) | 
| 15 |  | omelon 9687 | . . . . . . . 8
⊢ ω
∈ On | 
| 16 | 15 | a1i 11 | . . . . . . 7
⊢ (𝐴 ∈ On → ω ∈
On) | 
| 17 |  | id 22 | . . . . . . 7
⊢ (𝐴 ∈ On → 𝐴 ∈ On) | 
| 18 |  | peano1 7911 | . . . . . . . . 9
⊢ ∅
∈ ω | 
| 19 | 18 | ne0ii 4343 | . . . . . . . 8
⊢ ω
≠ ∅ | 
| 20 | 19 | a1i 11 | . . . . . . 7
⊢ (𝐴 ∈ On → ω ≠
∅) | 
| 21 | 16, 17, 20 | 3jca 1128 | . . . . . 6
⊢ (𝐴 ∈ On → (ω
∈ On ∧ 𝐴 ∈ On
∧ ω ≠ ∅)) | 
| 22 |  | omeulem1 8621 | . . . . . 6
⊢ ((ω
∈ On ∧ 𝐴 ∈ On
∧ ω ≠ ∅) → ∃𝑥 ∈ On ∃𝑦 ∈ ω ((ω
·o 𝑥)
+o 𝑦) = 𝐴) | 
| 23 | 14, 21, 22 | 3syl 18 | . . . . 5
⊢ ((𝐴 ∈ On ∧ Lim 𝐴) → ∃𝑥 ∈ On ∃𝑦 ∈ ω ((ω
·o 𝑥)
+o 𝑦) = 𝐴) | 
| 24 |  | limeq 6395 | . . . . . . . . . . . . . . . 16
⊢
(((ω ·o 𝑥) +o 𝑦) = 𝐴 → (Lim ((ω ·o
𝑥) +o 𝑦) ↔ Lim 𝐴)) | 
| 25 | 24 | biimprd 248 | . . . . . . . . . . . . . . 15
⊢
(((ω ·o 𝑥) +o 𝑦) = 𝐴 → (Lim 𝐴 → Lim ((ω ·o
𝑥) +o 𝑦))) | 
| 26 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ¬
∅ ∈ 𝑥) →
𝑦 ∈
ω) | 
| 27 |  | nnlim 7902 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ω → ¬ Lim
𝑦) | 
| 28 | 26, 27 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ¬
∅ ∈ 𝑥) →
¬ Lim 𝑦) | 
| 29 |  | on0eln0 6439 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ∈ On → (∅
∈ 𝑥 ↔ 𝑥 ≠ ∅)) | 
| 30 | 29 | biimprd 248 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ On → (𝑥 ≠ ∅ → ∅
∈ 𝑥)) | 
| 31 | 30 | necon1bd 2957 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ On → (¬ ∅
∈ 𝑥 → 𝑥 = ∅)) | 
| 32 | 31 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ ω) → (¬
∅ ∈ 𝑥 →
𝑥 =
∅)) | 
| 33 | 32 | imp 406 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ¬
∅ ∈ 𝑥) →
𝑥 =
∅) | 
| 34 | 33, 26 | jca 511 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ¬
∅ ∈ 𝑥) →
(𝑥 = ∅ ∧ 𝑦 ∈
ω)) | 
| 35 |  | simpl 482 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 = ∅ ∧ 𝑦 ∈ ω) → 𝑥 = ∅) | 
| 36 | 35 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 = ∅ ∧ 𝑦 ∈ ω) → (ω
·o 𝑥) =
(ω ·o ∅)) | 
| 37 |  | om0 8556 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ω
∈ On → (ω ·o ∅) =
∅) | 
| 38 | 15, 37 | mp1i 13 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 = ∅ ∧ 𝑦 ∈ ω) → (ω
·o ∅) = ∅) | 
| 39 | 36, 38 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 = ∅ ∧ 𝑦 ∈ ω) → (ω
·o 𝑥) =
∅) | 
| 40 | 39 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 = ∅ ∧ 𝑦 ∈ ω) →
((ω ·o 𝑥) +o 𝑦) = (∅ +o 𝑦)) | 
| 41 |  | nna0r 8648 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ ω → (∅
+o 𝑦) = 𝑦) | 
| 42 | 41 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 = ∅ ∧ 𝑦 ∈ ω) → (∅
+o 𝑦) = 𝑦) | 
| 43 | 40, 42 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 = ∅ ∧ 𝑦 ∈ ω) →
((ω ·o 𝑥) +o 𝑦) = 𝑦) | 
| 44 |  | limeq 6395 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((ω ·o 𝑥) +o 𝑦) = 𝑦 → (Lim ((ω ·o
𝑥) +o 𝑦) ↔ Lim 𝑦)) | 
| 45 | 34, 43, 44 | 3syl 18 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ¬
∅ ∈ 𝑥) →
(Lim ((ω ·o 𝑥) +o 𝑦) ↔ Lim 𝑦)) | 
| 46 | 28, 45 | mtbird 325 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ¬
∅ ∈ 𝑥) →
¬ Lim ((ω ·o 𝑥) +o 𝑦)) | 
| 47 | 46 | ex 412 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ ω) → (¬
∅ ∈ 𝑥 →
¬ Lim ((ω ·o 𝑥) +o 𝑦))) | 
| 48 |  | ovex 7465 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((ω
·o 𝑥)
+o ∪ 𝑦) ∈ V | 
| 49 |  | nlimsucg 7864 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((ω ·o 𝑥) +o ∪
𝑦) ∈ V → ¬
Lim suc ((ω ·o 𝑥) +o ∪
𝑦)) | 
| 50 | 48, 49 | mp1i 13 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ¬
𝑦 = ∅) → ¬
Lim suc ((ω ·o 𝑥) +o ∪
𝑦)) | 
| 51 |  | nnord 7896 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 ∈ ω → Ord 𝑦) | 
| 52 |  | orduniorsuc 7851 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (Ord
𝑦 → (𝑦 = ∪
𝑦 ∨ 𝑦 = suc ∪ 𝑦)) | 
| 53 | 51, 52 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ ω → (𝑦 = ∪
𝑦 ∨ 𝑦 = suc ∪ 𝑦)) | 
| 54 |  | 3ianor 1106 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (¬
(Ord 𝑦 ∧ 𝑦 ≠ ∅ ∧ 𝑦 = ∪
𝑦) ↔ (¬ Ord 𝑦 ∨ ¬ 𝑦 ≠ ∅ ∨ ¬ 𝑦 = ∪ 𝑦)) | 
| 55 |  | df-lim 6388 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (Lim
𝑦 ↔ (Ord 𝑦 ∧ 𝑦 ≠ ∅ ∧ 𝑦 = ∪ 𝑦)) | 
| 56 | 54, 55 | xchnxbir 333 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (¬
Lim 𝑦 ↔ (¬ Ord
𝑦 ∨ ¬ 𝑦 ≠ ∅ ∨ ¬ 𝑦 = ∪
𝑦)) | 
| 57 | 27, 56 | sylib 218 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ ω → (¬
Ord 𝑦 ∨ ¬ 𝑦 ≠ ∅ ∨ ¬ 𝑦 = ∪
𝑦)) | 
| 58 | 51 | pm2.24d 151 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 ∈ ω → (¬
Ord 𝑦 → (𝑦 = ∪
𝑦 → 𝑦 = ∅))) | 
| 59 |  | nne 2943 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (¬
𝑦 ≠ ∅ ↔ 𝑦 = ∅) | 
| 60 | 59 | biimpi 216 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (¬
𝑦 ≠ ∅ → 𝑦 = ∅) | 
| 61 | 60 | a1i13 27 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 ∈ ω → (¬
𝑦 ≠ ∅ →
(𝑦 = ∪ 𝑦
→ 𝑦 =
∅))) | 
| 62 |  | pm2.21 123 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (¬
𝑦 = ∪ 𝑦
→ (𝑦 = ∪ 𝑦
→ 𝑦 =
∅)) | 
| 63 | 62 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 ∈ ω → (¬
𝑦 = ∪ 𝑦
→ (𝑦 = ∪ 𝑦
→ 𝑦 =
∅))) | 
| 64 | 58, 61, 63 | 3jaod 1430 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ ω → ((¬
Ord 𝑦 ∨ ¬ 𝑦 ≠ ∅ ∨ ¬ 𝑦 = ∪
𝑦) → (𝑦 = ∪
𝑦 → 𝑦 = ∅))) | 
| 65 | 57, 64 | mpd 15 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 ∈ ω → (𝑦 = ∪
𝑦 → 𝑦 = ∅)) | 
| 66 | 65 | orim1d 967 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ ω → ((𝑦 = ∪
𝑦 ∨ 𝑦 = suc ∪ 𝑦) → (𝑦 = ∅ ∨ 𝑦 = suc ∪ 𝑦))) | 
| 67 | 53, 66 | mpd 15 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈ ω → (𝑦 = ∅ ∨ 𝑦 = suc ∪ 𝑦)) | 
| 68 | 67 | ord 864 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ω → (¬
𝑦 = ∅ → 𝑦 = suc ∪ 𝑦)) | 
| 69 | 68 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ ω) → (¬
𝑦 = ∅ → 𝑦 = suc ∪ 𝑦)) | 
| 70 | 69 | imp 406 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ¬
𝑦 = ∅) → 𝑦 = suc ∪ 𝑦) | 
| 71 | 70 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ¬
𝑦 = ∅) →
((ω ·o 𝑥) +o 𝑦) = ((ω ·o 𝑥) +o suc ∪ 𝑦)) | 
| 72 |  | simpl 482 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ ω) → 𝑥 ∈ On) | 
| 73 | 72 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ¬
𝑦 = ∅) → 𝑥 ∈ On) | 
| 74 |  | omcl 8575 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ω
∈ On ∧ 𝑥 ∈
On) → (ω ·o 𝑥) ∈ On) | 
| 75 | 15, 73, 74 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ¬
𝑦 = ∅) →
(ω ·o 𝑥) ∈ On) | 
| 76 |  | nnon 7894 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈ ω → 𝑦 ∈ On) | 
| 77 |  | onuni 7809 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈ On → ∪ 𝑦
∈ On) | 
| 78 | 76, 77 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ω → ∪ 𝑦
∈ On) | 
| 79 | 78 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ ω) → ∪ 𝑦
∈ On) | 
| 80 | 79 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ¬
𝑦 = ∅) → ∪ 𝑦
∈ On) | 
| 81 |  | oasuc 8563 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((ω ·o 𝑥) ∈ On ∧ ∪ 𝑦
∈ On) → ((ω ·o 𝑥) +o suc ∪ 𝑦) =
suc ((ω ·o 𝑥) +o ∪
𝑦)) | 
| 82 | 75, 80, 81 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ¬
𝑦 = ∅) →
((ω ·o 𝑥) +o suc ∪ 𝑦) =
suc ((ω ·o 𝑥) +o ∪
𝑦)) | 
| 83 | 71, 82 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ¬
𝑦 = ∅) →
((ω ·o 𝑥) +o 𝑦) = suc ((ω ·o 𝑥) +o ∪ 𝑦)) | 
| 84 |  | limeq 6395 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((ω ·o 𝑥) +o 𝑦) = suc ((ω ·o 𝑥) +o ∪ 𝑦)
→ (Lim ((ω ·o 𝑥) +o 𝑦) ↔ Lim suc ((ω
·o 𝑥)
+o ∪ 𝑦))) | 
| 85 | 83, 84 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ¬
𝑦 = ∅) → (Lim
((ω ·o 𝑥) +o 𝑦) ↔ Lim suc ((ω
·o 𝑥)
+o ∪ 𝑦))) | 
| 86 | 50, 85 | mtbird 325 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ¬
𝑦 = ∅) → ¬
Lim ((ω ·o 𝑥) +o 𝑦)) | 
| 87 | 86 | ex 412 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ ω) → (¬
𝑦 = ∅ → ¬
Lim ((ω ·o 𝑥) +o 𝑦))) | 
| 88 | 47, 87 | jaod 859 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ ω) → ((¬
∅ ∈ 𝑥 ∨ ¬
𝑦 = ∅) → ¬
Lim ((ω ·o 𝑥) +o 𝑦))) | 
| 89 | 88 | con2d 134 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ ω) → (Lim
((ω ·o 𝑥) +o 𝑦) → ¬ (¬ ∅ ∈ 𝑥 ∨ ¬ 𝑦 = ∅))) | 
| 90 |  | anor 984 | . . . . . . . . . . . . . . . 16
⊢ ((∅
∈ 𝑥 ∧ 𝑦 = ∅) ↔ ¬ (¬
∅ ∈ 𝑥 ∨ ¬
𝑦 =
∅)) | 
| 91 | 89, 90 | imbitrrdi 252 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ ω) → (Lim
((ω ·o 𝑥) +o 𝑦) → (∅ ∈ 𝑥 ∧ 𝑦 = ∅))) | 
| 92 | 25, 91 | syl9 77 | . . . . . . . . . . . . . 14
⊢
(((ω ·o 𝑥) +o 𝑦) = 𝐴 → ((𝑥 ∈ On ∧ 𝑦 ∈ ω) → (Lim 𝐴 → (∅ ∈ 𝑥 ∧ 𝑦 = ∅)))) | 
| 93 | 92 | com13 88 | . . . . . . . . . . . . 13
⊢ (Lim
𝐴 → ((𝑥 ∈ On ∧ 𝑦 ∈ ω) →
(((ω ·o 𝑥) +o 𝑦) = 𝐴 → (∅ ∈ 𝑥 ∧ 𝑦 = ∅)))) | 
| 94 | 93 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ Lim 𝐴) → ((𝑥 ∈ On ∧ 𝑦 ∈ ω) → (((ω
·o 𝑥)
+o 𝑦) = 𝐴 → (∅ ∈ 𝑥 ∧ 𝑦 = ∅)))) | 
| 95 | 94 | 3imp 1110 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ Lim 𝐴) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ((ω
·o 𝑥)
+o 𝑦) = 𝐴) → (∅ ∈ 𝑥 ∧ 𝑦 = ∅)) | 
| 96 |  | simp2 1137 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ On ∧ Lim 𝐴) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ((ω
·o 𝑥)
+o 𝑦) = 𝐴) → (𝑥 ∈ On ∧ 𝑦 ∈ ω)) | 
| 97 | 96, 72 | syl 17 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ On ∧ Lim 𝐴) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ((ω
·o 𝑥)
+o 𝑦) = 𝐴) → 𝑥 ∈ On) | 
| 98 |  | simpl 482 | . . . . . . . . . . . . . 14
⊢ ((∅
∈ 𝑥 ∧ 𝑦 = ∅) → ∅
∈ 𝑥) | 
| 99 | 97, 98 | anim12i 613 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ On ∧ Lim 𝐴) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ((ω
·o 𝑥)
+o 𝑦) = 𝐴) ∧ (∅ ∈ 𝑥 ∧ 𝑦 = ∅)) → (𝑥 ∈ On ∧ ∅ ∈ 𝑥)) | 
| 100 |  | ondif1 8540 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ (On ∖
1o) ↔ (𝑥
∈ On ∧ ∅ ∈ 𝑥)) | 
| 101 | 99, 100 | sylibr 234 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ On ∧ Lim 𝐴) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ((ω
·o 𝑥)
+o 𝑦) = 𝐴) ∧ (∅ ∈ 𝑥 ∧ 𝑦 = ∅)) → 𝑥 ∈ (On ∖
1o)) | 
| 102 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((∅
∈ 𝑥 ∧ 𝑦 = ∅) → 𝑦 = ∅) | 
| 103 | 102 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢ ((∅
∈ 𝑥 ∧ 𝑦 = ∅) → ((ω
·o 𝑥)
+o 𝑦) =
((ω ·o 𝑥) +o ∅)) | 
| 104 | 103 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ On ∧ Lim 𝐴) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ((ω
·o 𝑥)
+o 𝑦) = 𝐴) ∧ (∅ ∈ 𝑥 ∧ 𝑦 = ∅)) → ((ω
·o 𝑥)
+o 𝑦) =
((ω ·o 𝑥) +o ∅)) | 
| 105 |  | simpl3 1193 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ On ∧ Lim 𝐴) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ((ω
·o 𝑥)
+o 𝑦) = 𝐴) ∧ (∅ ∈ 𝑥 ∧ 𝑦 = ∅)) → ((ω
·o 𝑥)
+o 𝑦) = 𝐴) | 
| 106 | 15, 72, 74 | sylancr 587 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ ω) → (ω
·o 𝑥)
∈ On) | 
| 107 |  | oa0 8555 | . . . . . . . . . . . . . . 15
⊢ ((ω
·o 𝑥)
∈ On → ((ω ·o 𝑥) +o ∅) = (ω
·o 𝑥)) | 
| 108 | 96, 106, 107 | 3syl 18 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ On ∧ Lim 𝐴) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ((ω
·o 𝑥)
+o 𝑦) = 𝐴) → ((ω
·o 𝑥)
+o ∅) = (ω ·o 𝑥)) | 
| 109 | 108 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ On ∧ Lim 𝐴) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ((ω
·o 𝑥)
+o 𝑦) = 𝐴) ∧ (∅ ∈ 𝑥 ∧ 𝑦 = ∅)) → ((ω
·o 𝑥)
+o ∅) = (ω ·o 𝑥)) | 
| 110 | 104, 105,
109 | 3eqtr3d 2784 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ On ∧ Lim 𝐴) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ((ω
·o 𝑥)
+o 𝑦) = 𝐴) ∧ (∅ ∈ 𝑥 ∧ 𝑦 = ∅)) → 𝐴 = (ω ·o 𝑥)) | 
| 111 | 101, 110 | jca 511 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ On ∧ Lim 𝐴) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ((ω
·o 𝑥)
+o 𝑦) = 𝐴) ∧ (∅ ∈ 𝑥 ∧ 𝑦 = ∅)) → (𝑥 ∈ (On ∖ 1o) ∧
𝐴 = (ω
·o 𝑥))) | 
| 112 | 95, 111 | mpdan 687 | . . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ Lim 𝐴) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ ω) ∧ ((ω
·o 𝑥)
+o 𝑦) = 𝐴) → (𝑥 ∈ (On ∖ 1o) ∧
𝐴 = (ω
·o 𝑥))) | 
| 113 | 112 | 3exp 1119 | . . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ Lim 𝐴) → ((𝑥 ∈ On ∧ 𝑦 ∈ ω) → (((ω
·o 𝑥)
+o 𝑦) = 𝐴 → (𝑥 ∈ (On ∖ 1o) ∧
𝐴 = (ω
·o 𝑥))))) | 
| 114 | 113 | expdimp 452 | . . . . . . . 8
⊢ (((𝐴 ∈ On ∧ Lim 𝐴) ∧ 𝑥 ∈ On) → (𝑦 ∈ ω → (((ω
·o 𝑥)
+o 𝑦) = 𝐴 → (𝑥 ∈ (On ∖ 1o) ∧
𝐴 = (ω
·o 𝑥))))) | 
| 115 | 114 | rexlimdv 3152 | . . . . . . 7
⊢ (((𝐴 ∈ On ∧ Lim 𝐴) ∧ 𝑥 ∈ On) → (∃𝑦 ∈ ω ((ω
·o 𝑥)
+o 𝑦) = 𝐴 → (𝑥 ∈ (On ∖ 1o) ∧
𝐴 = (ω
·o 𝑥)))) | 
| 116 | 115 | expimpd 453 | . . . . . 6
⊢ ((𝐴 ∈ On ∧ Lim 𝐴) → ((𝑥 ∈ On ∧ ∃𝑦 ∈ ω ((ω
·o 𝑥)
+o 𝑦) = 𝐴) → (𝑥 ∈ (On ∖ 1o) ∧
𝐴 = (ω
·o 𝑥)))) | 
| 117 | 116 | reximdv2 3163 | . . . . 5
⊢ ((𝐴 ∈ On ∧ Lim 𝐴) → (∃𝑥 ∈ On ∃𝑦 ∈ ω ((ω
·o 𝑥)
+o 𝑦) = 𝐴 → ∃𝑥 ∈ (On ∖
1o)𝐴 = (ω
·o 𝑥))) | 
| 118 | 23, 117 | mpd 15 | . . . 4
⊢ ((𝐴 ∈ On ∧ Lim 𝐴) → ∃𝑥 ∈ (On ∖
1o)𝐴 = (ω
·o 𝑥)) | 
| 119 |  | simpr 484 | . . . . . . 7
⊢ ((𝑥 ∈ (On ∖
1o) ∧ 𝐴 =
(ω ·o 𝑥)) → 𝐴 = (ω ·o 𝑥)) | 
| 120 |  | eldifi 4130 | . . . . . . . . 9
⊢ (𝑥 ∈ (On ∖
1o) → 𝑥
∈ On) | 
| 121 | 15, 120, 74 | sylancr 587 | . . . . . . . 8
⊢ (𝑥 ∈ (On ∖
1o) → (ω ·o 𝑥) ∈ On) | 
| 122 | 121 | adantr 480 | . . . . . . 7
⊢ ((𝑥 ∈ (On ∖
1o) ∧ 𝐴 =
(ω ·o 𝑥)) → (ω ·o 𝑥) ∈ On) | 
| 123 | 119, 122 | eqeltrd 2840 | . . . . . 6
⊢ ((𝑥 ∈ (On ∖
1o) ∧ 𝐴 =
(ω ·o 𝑥)) → 𝐴 ∈ On) | 
| 124 |  | limom 7904 | . . . . . . . . . . 11
⊢ Lim
ω | 
| 125 | 15, 124 | pm3.2i 470 | . . . . . . . . . 10
⊢ (ω
∈ On ∧ Lim ω) | 
| 126 |  | omlimcl2 43259 | . . . . . . . . . 10
⊢ (((𝑥 ∈ On ∧ (ω ∈
On ∧ Lim ω)) ∧ ∅ ∈ 𝑥) → Lim (ω ·o
𝑥)) | 
| 127 | 125, 126 | mpanl2 701 | . . . . . . . . 9
⊢ ((𝑥 ∈ On ∧ ∅ ∈
𝑥) → Lim (ω
·o 𝑥)) | 
| 128 | 100, 127 | sylbi 217 | . . . . . . . 8
⊢ (𝑥 ∈ (On ∖
1o) → Lim (ω ·o 𝑥)) | 
| 129 | 128 | adantr 480 | . . . . . . 7
⊢ ((𝑥 ∈ (On ∖
1o) ∧ 𝐴 =
(ω ·o 𝑥)) → Lim (ω ·o
𝑥)) | 
| 130 |  | limeq 6395 | . . . . . . . 8
⊢ (𝐴 = (ω ·o
𝑥) → (Lim 𝐴 ↔ Lim (ω
·o 𝑥))) | 
| 131 | 130 | adantl 481 | . . . . . . 7
⊢ ((𝑥 ∈ (On ∖
1o) ∧ 𝐴 =
(ω ·o 𝑥)) → (Lim 𝐴 ↔ Lim (ω ·o
𝑥))) | 
| 132 | 129, 131 | mpbird 257 | . . . . . 6
⊢ ((𝑥 ∈ (On ∖
1o) ∧ 𝐴 =
(ω ·o 𝑥)) → Lim 𝐴) | 
| 133 | 123, 132 | jca 511 | . . . . 5
⊢ ((𝑥 ∈ (On ∖
1o) ∧ 𝐴 =
(ω ·o 𝑥)) → (𝐴 ∈ On ∧ Lim 𝐴)) | 
| 134 | 133 | rexlimiva 3146 | . . . 4
⊢
(∃𝑥 ∈ (On
∖ 1o)𝐴 =
(ω ·o 𝑥) → (𝐴 ∈ On ∧ Lim 𝐴)) | 
| 135 | 118, 134 | impbii 209 | . . 3
⊢ ((𝐴 ∈ On ∧ Lim 𝐴) ↔ ∃𝑥 ∈ (On ∖
1o)𝐴 = (ω
·o 𝑥)) | 
| 136 | 135 | orbi2i 912 | . 2
⊢ ((𝐴 = On ∨ (𝐴 ∈ On ∧ Lim 𝐴)) ↔ (𝐴 = On ∨ ∃𝑥 ∈ (On ∖ 1o)𝐴 = (ω ·o
𝑥))) | 
| 137 | 8, 13, 136 | 3bitr2i 299 | 1
⊢ (Lim
𝐴 ↔ (𝐴 = On ∨ ∃𝑥 ∈ (On ∖ 1o)𝐴 = (ω ·o
𝑥))) |