Proof of Theorem naddwordnexlem3
Step | Hyp | Ref
| Expression |
1 | | naddwordnex.a |
. . . . . 6
⊢ (𝜑 → 𝐴 = ((ω ·o 𝐶) +o 𝑀)) |
2 | | omelon 9637 |
. . . . . . . 8
⊢ ω
∈ On |
3 | | naddwordnex.d |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ On) |
4 | | naddwordnex.c |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ 𝐷) |
5 | | onelon 6379 |
. . . . . . . . 9
⊢ ((𝐷 ∈ On ∧ 𝐶 ∈ 𝐷) → 𝐶 ∈ On) |
6 | 3, 4, 5 | syl2anc 583 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ On) |
7 | | omcl 8531 |
. . . . . . . 8
⊢ ((ω
∈ On ∧ 𝐶 ∈
On) → (ω ·o 𝐶) ∈ On) |
8 | 2, 6, 7 | sylancr 586 |
. . . . . . 7
⊢ (𝜑 → (ω
·o 𝐶)
∈ On) |
9 | | naddwordnex.m |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ω) |
10 | | nnon 7854 |
. . . . . . . 8
⊢ (𝑀 ∈ ω → 𝑀 ∈ On) |
11 | 9, 10 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ On) |
12 | | oacl 8530 |
. . . . . . 7
⊢
(((ω ·o 𝐶) ∈ On ∧ 𝑀 ∈ On) → ((ω
·o 𝐶)
+o 𝑀) ∈
On) |
13 | 8, 11, 12 | syl2anc 583 |
. . . . . 6
⊢ (𝜑 → ((ω
·o 𝐶)
+o 𝑀) ∈
On) |
14 | 1, 13 | eqeltrd 2825 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ On) |
15 | | naddonnn 42635 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ ω) → (𝐴 +o 𝑥) = (𝐴 +no 𝑥)) |
16 | 14, 15 | sylan 579 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (𝐴 +o 𝑥) = (𝐴 +no 𝑥)) |
17 | | naddwordnex.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 = ((ω ·o 𝐷) +o 𝑁)) |
18 | | naddwordnex.n |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ 𝑀) |
19 | 1, 17, 4, 3, 9, 18 | naddwordnexlem0 42636 |
. . . . . . 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 8606 |
. . . . . . . 8
⊢ ((𝑀 ∈ ω ∧ 𝑥 ∈ ω) → (𝑀 +o 𝑥) ∈
ω) |
25 | 9, 24 | sylan 579 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (𝑀 +o 𝑥) ∈ ω) |
26 | | oaordi 8541 |
. . . . . . 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 7416 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (𝐴 +o 𝑥) = (((ω ·o 𝐶) +o 𝑀) +o 𝑥)) |
30 | | nnon 7854 |
. . . . . . . 8
⊢ (𝑥 ∈ ω → 𝑥 ∈ On) |
31 | | oaass 8556 |
. . . . . . . 8
⊢
(((ω ·o 𝐶) ∈ On ∧ 𝑀 ∈ On ∧ 𝑥 ∈ On) → (((ω
·o 𝐶)
+o 𝑀)
+o 𝑥) =
((ω ·o 𝐶) +o (𝑀 +o 𝑥))) |
32 | 8, 11, 30, 31 | syl2an3an 1419 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (((ω
·o 𝐶)
+o 𝑀)
+o 𝑥) =
((ω ·o 𝐶) +o (𝑀 +o 𝑥))) |
33 | 29, 32 | eqtrd 2764 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (𝐴 +o 𝑥) = ((ω ·o 𝐶) +o (𝑀 +o 𝑥))) |
34 | 6 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → 𝐶 ∈ On) |
35 | | omsuc 8521 |
. . . . . . 7
⊢ ((ω
∈ On ∧ 𝐶 ∈
On) → (ω ·o suc 𝐶) = ((ω ·o 𝐶) +o
ω)) |
36 | 2, 34, 35 | sylancr 586 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (ω
·o suc 𝐶)
= ((ω ·o 𝐶) +o ω)) |
37 | 27, 33, 36 | 3eltr4d 2840 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (𝐴 +o 𝑥) ∈ (ω ·o suc
𝐶)) |
38 | 21, 37 | sseldd 3975 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (𝐴 +o 𝑥) ∈ 𝐵) |
39 | 16, 38 | eqeltrrd 2826 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (𝐴 +no 𝑥) ∈ 𝐵) |
40 | 39 | ex 412 |
. 2
⊢ (𝜑 → (𝑥 ∈ ω → (𝐴 +no 𝑥) ∈ 𝐵)) |
41 | 40 | ralrimiv 3137 |
1
⊢ (𝜑 → ∀𝑥 ∈ ω (𝐴 +no 𝑥) ∈ 𝐵) |