Proof of Theorem naddwordnexlem3
| Step | Hyp | Ref
| Expression |
| 1 | | naddwordnex.a |
. . . . . 6
⊢ (𝜑 → 𝐴 = ((ω ·o 𝐶) +o 𝑀)) |
| 2 | | omelon 9686 |
. . . . . . . 8
⊢ ω
∈ On |
| 3 | | naddwordnex.d |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ On) |
| 4 | | naddwordnex.c |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ 𝐷) |
| 5 | | onelon 6409 |
. . . . . . . . 9
⊢ ((𝐷 ∈ On ∧ 𝐶 ∈ 𝐷) → 𝐶 ∈ On) |
| 6 | 3, 4, 5 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ On) |
| 7 | | omcl 8574 |
. . . . . . . 8
⊢ ((ω
∈ On ∧ 𝐶 ∈
On) → (ω ·o 𝐶) ∈ On) |
| 8 | 2, 6, 7 | sylancr 587 |
. . . . . . 7
⊢ (𝜑 → (ω
·o 𝐶)
∈ On) |
| 9 | | naddwordnex.m |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ω) |
| 10 | | nnon 7893 |
. . . . . . . 8
⊢ (𝑀 ∈ ω → 𝑀 ∈ On) |
| 11 | 9, 10 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ On) |
| 12 | | oacl 8573 |
. . . . . . 7
⊢
(((ω ·o 𝐶) ∈ On ∧ 𝑀 ∈ On) → ((ω
·o 𝐶)
+o 𝑀) ∈
On) |
| 13 | 8, 11, 12 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ((ω
·o 𝐶)
+o 𝑀) ∈
On) |
| 14 | 1, 13 | eqeltrd 2841 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ On) |
| 15 | | naddonnn 43408 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ ω) → (𝐴 +o 𝑥) = (𝐴 +no 𝑥)) |
| 16 | 14, 15 | sylan 580 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (𝐴 +o 𝑥) = (𝐴 +no 𝑥)) |
| 17 | | naddwordnex.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 = ((ω ·o 𝐷) +o 𝑁)) |
| 18 | | naddwordnex.n |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ 𝑀) |
| 19 | 1, 17, 4, 3, 9, 18 | naddwordnexlem0 43409 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ∈ (ω ·o suc
𝐶) ∧ (ω
·o suc 𝐶)
⊆ 𝐵)) |
| 20 | 19 | simprd 495 |
. . . . . 6
⊢ (𝜑 → (ω
·o suc 𝐶)
⊆ 𝐵) |
| 21 | 20 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (ω
·o suc 𝐶)
⊆ 𝐵) |
| 22 | 8, 2 | jctil 519 |
. . . . . . . 8
⊢ (𝜑 → (ω ∈ On ∧
(ω ·o 𝐶) ∈ On)) |
| 23 | 22 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (ω ∈ On
∧ (ω ·o 𝐶) ∈ On)) |
| 24 | | nnacl 8649 |
. . . . . . . 8
⊢ ((𝑀 ∈ ω ∧ 𝑥 ∈ ω) → (𝑀 +o 𝑥) ∈
ω) |
| 25 | 9, 24 | sylan 580 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (𝑀 +o 𝑥) ∈ ω) |
| 26 | | oaordi 8584 |
. . . . . . 7
⊢ ((ω
∈ On ∧ (ω ·o 𝐶) ∈ On) → ((𝑀 +o 𝑥) ∈ ω → ((ω
·o 𝐶)
+o (𝑀
+o 𝑥)) ∈
((ω ·o 𝐶) +o ω))) |
| 27 | 23, 25, 26 | sylc 65 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → ((ω
·o 𝐶)
+o (𝑀
+o 𝑥)) ∈
((ω ·o 𝐶) +o ω)) |
| 28 | 1 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → 𝐴 = ((ω ·o 𝐶) +o 𝑀)) |
| 29 | 28 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (𝐴 +o 𝑥) = (((ω ·o 𝐶) +o 𝑀) +o 𝑥)) |
| 30 | | nnon 7893 |
. . . . . . . 8
⊢ (𝑥 ∈ ω → 𝑥 ∈ On) |
| 31 | | oaass 8599 |
. . . . . . . 8
⊢
(((ω ·o 𝐶) ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ On) → (((ω
·o 𝐶)
+o 𝑀)
+o 𝑥) =
((ω ·o 𝐶) +o (𝑀 +o 𝑥))) |
| 32 | 8, 11, 30, 31 | syl2an3an 1424 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (((ω
·o 𝐶)
+o 𝑀)
+o 𝑥) =
((ω ·o 𝐶) +o (𝑀 +o 𝑥))) |
| 33 | 29, 32 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (𝐴 +o 𝑥) = ((ω ·o 𝐶) +o (𝑀 +o 𝑥))) |
| 34 | 6 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → 𝐶 ∈ On) |
| 35 | | omsuc 8564 |
. . . . . . 7
⊢ ((ω
∈ On ∧ 𝐶 ∈
On) → (ω ·o suc 𝐶) = ((ω ·o 𝐶) +o
ω)) |
| 36 | 2, 34, 35 | sylancr 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (ω
·o suc 𝐶)
= ((ω ·o 𝐶) +o ω)) |
| 37 | 27, 33, 36 | 3eltr4d 2856 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (𝐴 +o 𝑥) ∈ (ω ·o suc
𝐶)) |
| 38 | 21, 37 | sseldd 3984 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (𝐴 +o 𝑥) ∈ 𝐵) |
| 39 | 16, 38 | eqeltrrd 2842 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (𝐴 +no 𝑥) ∈ 𝐵) |
| 40 | 39 | ex 412 |
. 2
⊢ (𝜑 → (𝑥 ∈ ω → (𝐴 +no 𝑥) ∈ 𝐵)) |
| 41 | 40 | ralrimiv 3145 |
1
⊢ (𝜑 → ∀𝑥 ∈ ω (𝐴 +no 𝑥) ∈ 𝐵) |