Step |
Hyp |
Ref |
Expression |
1 |
|
oveq2 |
⊢ ( 𝑥 = 𝑦 → ( 2o ·o 𝑥 ) = ( 2o ·o 𝑦 ) ) |
2 |
1
|
eqeq2d |
⊢ ( 𝑥 = 𝑦 → ( 𝐴 = ( 2o ·o 𝑥 ) ↔ 𝐴 = ( 2o ·o 𝑦 ) ) ) |
3 |
2
|
cbvrexvw |
⊢ ( ∃ 𝑥 ∈ ω 𝐴 = ( 2o ·o 𝑥 ) ↔ ∃ 𝑦 ∈ ω 𝐴 = ( 2o ·o 𝑦 ) ) |
4 |
|
nnneo |
⊢ ( ( 𝑦 ∈ ω ∧ 𝑥 ∈ ω ∧ 𝐴 = ( 2o ·o 𝑦 ) ) → ¬ suc 𝐴 = ( 2o ·o 𝑥 ) ) |
5 |
4
|
3com23 |
⊢ ( ( 𝑦 ∈ ω ∧ 𝐴 = ( 2o ·o 𝑦 ) ∧ 𝑥 ∈ ω ) → ¬ suc 𝐴 = ( 2o ·o 𝑥 ) ) |
6 |
5
|
3expa |
⊢ ( ( ( 𝑦 ∈ ω ∧ 𝐴 = ( 2o ·o 𝑦 ) ) ∧ 𝑥 ∈ ω ) → ¬ suc 𝐴 = ( 2o ·o 𝑥 ) ) |
7 |
6
|
nrexdv |
⊢ ( ( 𝑦 ∈ ω ∧ 𝐴 = ( 2o ·o 𝑦 ) ) → ¬ ∃ 𝑥 ∈ ω suc 𝐴 = ( 2o ·o 𝑥 ) ) |
8 |
7
|
rexlimiva |
⊢ ( ∃ 𝑦 ∈ ω 𝐴 = ( 2o ·o 𝑦 ) → ¬ ∃ 𝑥 ∈ ω suc 𝐴 = ( 2o ·o 𝑥 ) ) |
9 |
3 8
|
sylbi |
⊢ ( ∃ 𝑥 ∈ ω 𝐴 = ( 2o ·o 𝑥 ) → ¬ ∃ 𝑥 ∈ ω suc 𝐴 = ( 2o ·o 𝑥 ) ) |
10 |
|
suceq |
⊢ ( 𝑦 = ∅ → suc 𝑦 = suc ∅ ) |
11 |
10
|
eqeq1d |
⊢ ( 𝑦 = ∅ → ( suc 𝑦 = ( 2o ·o 𝑥 ) ↔ suc ∅ = ( 2o ·o 𝑥 ) ) ) |
12 |
11
|
rexbidv |
⊢ ( 𝑦 = ∅ → ( ∃ 𝑥 ∈ ω suc 𝑦 = ( 2o ·o 𝑥 ) ↔ ∃ 𝑥 ∈ ω suc ∅ = ( 2o ·o 𝑥 ) ) ) |
13 |
12
|
notbid |
⊢ ( 𝑦 = ∅ → ( ¬ ∃ 𝑥 ∈ ω suc 𝑦 = ( 2o ·o 𝑥 ) ↔ ¬ ∃ 𝑥 ∈ ω suc ∅ = ( 2o ·o 𝑥 ) ) ) |
14 |
|
eqeq1 |
⊢ ( 𝑦 = ∅ → ( 𝑦 = ( 2o ·o 𝑥 ) ↔ ∅ = ( 2o ·o 𝑥 ) ) ) |
15 |
14
|
rexbidv |
⊢ ( 𝑦 = ∅ → ( ∃ 𝑥 ∈ ω 𝑦 = ( 2o ·o 𝑥 ) ↔ ∃ 𝑥 ∈ ω ∅ = ( 2o ·o 𝑥 ) ) ) |
16 |
13 15
|
imbi12d |
⊢ ( 𝑦 = ∅ → ( ( ¬ ∃ 𝑥 ∈ ω suc 𝑦 = ( 2o ·o 𝑥 ) → ∃ 𝑥 ∈ ω 𝑦 = ( 2o ·o 𝑥 ) ) ↔ ( ¬ ∃ 𝑥 ∈ ω suc ∅ = ( 2o ·o 𝑥 ) → ∃ 𝑥 ∈ ω ∅ = ( 2o ·o 𝑥 ) ) ) ) |
17 |
|
suceq |
⊢ ( 𝑦 = 𝑧 → suc 𝑦 = suc 𝑧 ) |
18 |
17
|
eqeq1d |
⊢ ( 𝑦 = 𝑧 → ( suc 𝑦 = ( 2o ·o 𝑥 ) ↔ suc 𝑧 = ( 2o ·o 𝑥 ) ) ) |
19 |
18
|
rexbidv |
⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑥 ∈ ω suc 𝑦 = ( 2o ·o 𝑥 ) ↔ ∃ 𝑥 ∈ ω suc 𝑧 = ( 2o ·o 𝑥 ) ) ) |
20 |
19
|
notbid |
⊢ ( 𝑦 = 𝑧 → ( ¬ ∃ 𝑥 ∈ ω suc 𝑦 = ( 2o ·o 𝑥 ) ↔ ¬ ∃ 𝑥 ∈ ω suc 𝑧 = ( 2o ·o 𝑥 ) ) ) |
21 |
|
eqeq1 |
⊢ ( 𝑦 = 𝑧 → ( 𝑦 = ( 2o ·o 𝑥 ) ↔ 𝑧 = ( 2o ·o 𝑥 ) ) ) |
22 |
21
|
rexbidv |
⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑥 ∈ ω 𝑦 = ( 2o ·o 𝑥 ) ↔ ∃ 𝑥 ∈ ω 𝑧 = ( 2o ·o 𝑥 ) ) ) |
23 |
20 22
|
imbi12d |
⊢ ( 𝑦 = 𝑧 → ( ( ¬ ∃ 𝑥 ∈ ω suc 𝑦 = ( 2o ·o 𝑥 ) → ∃ 𝑥 ∈ ω 𝑦 = ( 2o ·o 𝑥 ) ) ↔ ( ¬ ∃ 𝑥 ∈ ω suc 𝑧 = ( 2o ·o 𝑥 ) → ∃ 𝑥 ∈ ω 𝑧 = ( 2o ·o 𝑥 ) ) ) ) |
24 |
|
suceq |
⊢ ( 𝑦 = suc 𝑧 → suc 𝑦 = suc suc 𝑧 ) |
25 |
24
|
eqeq1d |
⊢ ( 𝑦 = suc 𝑧 → ( suc 𝑦 = ( 2o ·o 𝑥 ) ↔ suc suc 𝑧 = ( 2o ·o 𝑥 ) ) ) |
26 |
25
|
rexbidv |
⊢ ( 𝑦 = suc 𝑧 → ( ∃ 𝑥 ∈ ω suc 𝑦 = ( 2o ·o 𝑥 ) ↔ ∃ 𝑥 ∈ ω suc suc 𝑧 = ( 2o ·o 𝑥 ) ) ) |
27 |
26
|
notbid |
⊢ ( 𝑦 = suc 𝑧 → ( ¬ ∃ 𝑥 ∈ ω suc 𝑦 = ( 2o ·o 𝑥 ) ↔ ¬ ∃ 𝑥 ∈ ω suc suc 𝑧 = ( 2o ·o 𝑥 ) ) ) |
28 |
|
eqeq1 |
⊢ ( 𝑦 = suc 𝑧 → ( 𝑦 = ( 2o ·o 𝑥 ) ↔ suc 𝑧 = ( 2o ·o 𝑥 ) ) ) |
29 |
28
|
rexbidv |
⊢ ( 𝑦 = suc 𝑧 → ( ∃ 𝑥 ∈ ω 𝑦 = ( 2o ·o 𝑥 ) ↔ ∃ 𝑥 ∈ ω suc 𝑧 = ( 2o ·o 𝑥 ) ) ) |
30 |
27 29
|
imbi12d |
⊢ ( 𝑦 = suc 𝑧 → ( ( ¬ ∃ 𝑥 ∈ ω suc 𝑦 = ( 2o ·o 𝑥 ) → ∃ 𝑥 ∈ ω 𝑦 = ( 2o ·o 𝑥 ) ) ↔ ( ¬ ∃ 𝑥 ∈ ω suc suc 𝑧 = ( 2o ·o 𝑥 ) → ∃ 𝑥 ∈ ω suc 𝑧 = ( 2o ·o 𝑥 ) ) ) ) |
31 |
|
suceq |
⊢ ( 𝑦 = 𝐴 → suc 𝑦 = suc 𝐴 ) |
32 |
31
|
eqeq1d |
⊢ ( 𝑦 = 𝐴 → ( suc 𝑦 = ( 2o ·o 𝑥 ) ↔ suc 𝐴 = ( 2o ·o 𝑥 ) ) ) |
33 |
32
|
rexbidv |
⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 ∈ ω suc 𝑦 = ( 2o ·o 𝑥 ) ↔ ∃ 𝑥 ∈ ω suc 𝐴 = ( 2o ·o 𝑥 ) ) ) |
34 |
33
|
notbid |
⊢ ( 𝑦 = 𝐴 → ( ¬ ∃ 𝑥 ∈ ω suc 𝑦 = ( 2o ·o 𝑥 ) ↔ ¬ ∃ 𝑥 ∈ ω suc 𝐴 = ( 2o ·o 𝑥 ) ) ) |
35 |
|
eqeq1 |
⊢ ( 𝑦 = 𝐴 → ( 𝑦 = ( 2o ·o 𝑥 ) ↔ 𝐴 = ( 2o ·o 𝑥 ) ) ) |
36 |
35
|
rexbidv |
⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 ∈ ω 𝑦 = ( 2o ·o 𝑥 ) ↔ ∃ 𝑥 ∈ ω 𝐴 = ( 2o ·o 𝑥 ) ) ) |
37 |
34 36
|
imbi12d |
⊢ ( 𝑦 = 𝐴 → ( ( ¬ ∃ 𝑥 ∈ ω suc 𝑦 = ( 2o ·o 𝑥 ) → ∃ 𝑥 ∈ ω 𝑦 = ( 2o ·o 𝑥 ) ) ↔ ( ¬ ∃ 𝑥 ∈ ω suc 𝐴 = ( 2o ·o 𝑥 ) → ∃ 𝑥 ∈ ω 𝐴 = ( 2o ·o 𝑥 ) ) ) ) |
38 |
|
peano1 |
⊢ ∅ ∈ ω |
39 |
|
eqid |
⊢ ∅ = ∅ |
40 |
|
oveq2 |
⊢ ( 𝑥 = ∅ → ( 2o ·o 𝑥 ) = ( 2o ·o ∅ ) ) |
41 |
|
2on |
⊢ 2o ∈ On |
42 |
|
om0 |
⊢ ( 2o ∈ On → ( 2o ·o ∅ ) = ∅ ) |
43 |
41 42
|
ax-mp |
⊢ ( 2o ·o ∅ ) = ∅ |
44 |
40 43
|
eqtrdi |
⊢ ( 𝑥 = ∅ → ( 2o ·o 𝑥 ) = ∅ ) |
45 |
44
|
rspceeqv |
⊢ ( ( ∅ ∈ ω ∧ ∅ = ∅ ) → ∃ 𝑥 ∈ ω ∅ = ( 2o ·o 𝑥 ) ) |
46 |
38 39 45
|
mp2an |
⊢ ∃ 𝑥 ∈ ω ∅ = ( 2o ·o 𝑥 ) |
47 |
46
|
a1i |
⊢ ( ¬ ∃ 𝑥 ∈ ω suc ∅ = ( 2o ·o 𝑥 ) → ∃ 𝑥 ∈ ω ∅ = ( 2o ·o 𝑥 ) ) |
48 |
1
|
eqeq2d |
⊢ ( 𝑥 = 𝑦 → ( 𝑧 = ( 2o ·o 𝑥 ) ↔ 𝑧 = ( 2o ·o 𝑦 ) ) ) |
49 |
48
|
cbvrexvw |
⊢ ( ∃ 𝑥 ∈ ω 𝑧 = ( 2o ·o 𝑥 ) ↔ ∃ 𝑦 ∈ ω 𝑧 = ( 2o ·o 𝑦 ) ) |
50 |
|
peano2 |
⊢ ( 𝑦 ∈ ω → suc 𝑦 ∈ ω ) |
51 |
|
2onn |
⊢ 2o ∈ ω |
52 |
|
nnmsuc |
⊢ ( ( 2o ∈ ω ∧ 𝑦 ∈ ω ) → ( 2o ·o suc 𝑦 ) = ( ( 2o ·o 𝑦 ) +o 2o ) ) |
53 |
51 52
|
mpan |
⊢ ( 𝑦 ∈ ω → ( 2o ·o suc 𝑦 ) = ( ( 2o ·o 𝑦 ) +o 2o ) ) |
54 |
|
df-2o |
⊢ 2o = suc 1o |
55 |
54
|
oveq2i |
⊢ ( ( 2o ·o 𝑦 ) +o 2o ) = ( ( 2o ·o 𝑦 ) +o suc 1o ) |
56 |
|
nnmcl |
⊢ ( ( 2o ∈ ω ∧ 𝑦 ∈ ω ) → ( 2o ·o 𝑦 ) ∈ ω ) |
57 |
51 56
|
mpan |
⊢ ( 𝑦 ∈ ω → ( 2o ·o 𝑦 ) ∈ ω ) |
58 |
|
1onn |
⊢ 1o ∈ ω |
59 |
|
nnasuc |
⊢ ( ( ( 2o ·o 𝑦 ) ∈ ω ∧ 1o ∈ ω ) → ( ( 2o ·o 𝑦 ) +o suc 1o ) = suc ( ( 2o ·o 𝑦 ) +o 1o ) ) |
60 |
57 58 59
|
sylancl |
⊢ ( 𝑦 ∈ ω → ( ( 2o ·o 𝑦 ) +o suc 1o ) = suc ( ( 2o ·o 𝑦 ) +o 1o ) ) |
61 |
55 60
|
eqtr2id |
⊢ ( 𝑦 ∈ ω → suc ( ( 2o ·o 𝑦 ) +o 1o ) = ( ( 2o ·o 𝑦 ) +o 2o ) ) |
62 |
|
nnon |
⊢ ( ( 2o ·o 𝑦 ) ∈ ω → ( 2o ·o 𝑦 ) ∈ On ) |
63 |
|
oa1suc |
⊢ ( ( 2o ·o 𝑦 ) ∈ On → ( ( 2o ·o 𝑦 ) +o 1o ) = suc ( 2o ·o 𝑦 ) ) |
64 |
|
suceq |
⊢ ( ( ( 2o ·o 𝑦 ) +o 1o ) = suc ( 2o ·o 𝑦 ) → suc ( ( 2o ·o 𝑦 ) +o 1o ) = suc suc ( 2o ·o 𝑦 ) ) |
65 |
57 62 63 64
|
4syl |
⊢ ( 𝑦 ∈ ω → suc ( ( 2o ·o 𝑦 ) +o 1o ) = suc suc ( 2o ·o 𝑦 ) ) |
66 |
53 61 65
|
3eqtr2rd |
⊢ ( 𝑦 ∈ ω → suc suc ( 2o ·o 𝑦 ) = ( 2o ·o suc 𝑦 ) ) |
67 |
|
oveq2 |
⊢ ( 𝑥 = suc 𝑦 → ( 2o ·o 𝑥 ) = ( 2o ·o suc 𝑦 ) ) |
68 |
67
|
rspceeqv |
⊢ ( ( suc 𝑦 ∈ ω ∧ suc suc ( 2o ·o 𝑦 ) = ( 2o ·o suc 𝑦 ) ) → ∃ 𝑥 ∈ ω suc suc ( 2o ·o 𝑦 ) = ( 2o ·o 𝑥 ) ) |
69 |
50 66 68
|
syl2anc |
⊢ ( 𝑦 ∈ ω → ∃ 𝑥 ∈ ω suc suc ( 2o ·o 𝑦 ) = ( 2o ·o 𝑥 ) ) |
70 |
|
suceq |
⊢ ( 𝑧 = ( 2o ·o 𝑦 ) → suc 𝑧 = suc ( 2o ·o 𝑦 ) ) |
71 |
|
suceq |
⊢ ( suc 𝑧 = suc ( 2o ·o 𝑦 ) → suc suc 𝑧 = suc suc ( 2o ·o 𝑦 ) ) |
72 |
70 71
|
syl |
⊢ ( 𝑧 = ( 2o ·o 𝑦 ) → suc suc 𝑧 = suc suc ( 2o ·o 𝑦 ) ) |
73 |
72
|
eqeq1d |
⊢ ( 𝑧 = ( 2o ·o 𝑦 ) → ( suc suc 𝑧 = ( 2o ·o 𝑥 ) ↔ suc suc ( 2o ·o 𝑦 ) = ( 2o ·o 𝑥 ) ) ) |
74 |
73
|
rexbidv |
⊢ ( 𝑧 = ( 2o ·o 𝑦 ) → ( ∃ 𝑥 ∈ ω suc suc 𝑧 = ( 2o ·o 𝑥 ) ↔ ∃ 𝑥 ∈ ω suc suc ( 2o ·o 𝑦 ) = ( 2o ·o 𝑥 ) ) ) |
75 |
69 74
|
syl5ibrcom |
⊢ ( 𝑦 ∈ ω → ( 𝑧 = ( 2o ·o 𝑦 ) → ∃ 𝑥 ∈ ω suc suc 𝑧 = ( 2o ·o 𝑥 ) ) ) |
76 |
75
|
rexlimiv |
⊢ ( ∃ 𝑦 ∈ ω 𝑧 = ( 2o ·o 𝑦 ) → ∃ 𝑥 ∈ ω suc suc 𝑧 = ( 2o ·o 𝑥 ) ) |
77 |
76
|
a1i |
⊢ ( 𝑧 ∈ ω → ( ∃ 𝑦 ∈ ω 𝑧 = ( 2o ·o 𝑦 ) → ∃ 𝑥 ∈ ω suc suc 𝑧 = ( 2o ·o 𝑥 ) ) ) |
78 |
49 77
|
syl5bi |
⊢ ( 𝑧 ∈ ω → ( ∃ 𝑥 ∈ ω 𝑧 = ( 2o ·o 𝑥 ) → ∃ 𝑥 ∈ ω suc suc 𝑧 = ( 2o ·o 𝑥 ) ) ) |
79 |
78
|
con3d |
⊢ ( 𝑧 ∈ ω → ( ¬ ∃ 𝑥 ∈ ω suc suc 𝑧 = ( 2o ·o 𝑥 ) → ¬ ∃ 𝑥 ∈ ω 𝑧 = ( 2o ·o 𝑥 ) ) ) |
80 |
|
con1 |
⊢ ( ( ¬ ∃ 𝑥 ∈ ω suc 𝑧 = ( 2o ·o 𝑥 ) → ∃ 𝑥 ∈ ω 𝑧 = ( 2o ·o 𝑥 ) ) → ( ¬ ∃ 𝑥 ∈ ω 𝑧 = ( 2o ·o 𝑥 ) → ∃ 𝑥 ∈ ω suc 𝑧 = ( 2o ·o 𝑥 ) ) ) |
81 |
79 80
|
syl9 |
⊢ ( 𝑧 ∈ ω → ( ( ¬ ∃ 𝑥 ∈ ω suc 𝑧 = ( 2o ·o 𝑥 ) → ∃ 𝑥 ∈ ω 𝑧 = ( 2o ·o 𝑥 ) ) → ( ¬ ∃ 𝑥 ∈ ω suc suc 𝑧 = ( 2o ·o 𝑥 ) → ∃ 𝑥 ∈ ω suc 𝑧 = ( 2o ·o 𝑥 ) ) ) ) |
82 |
16 23 30 37 47 81
|
finds |
⊢ ( 𝐴 ∈ ω → ( ¬ ∃ 𝑥 ∈ ω suc 𝐴 = ( 2o ·o 𝑥 ) → ∃ 𝑥 ∈ ω 𝐴 = ( 2o ·o 𝑥 ) ) ) |
83 |
9 82
|
impbid2 |
⊢ ( 𝐴 ∈ ω → ( ∃ 𝑥 ∈ ω 𝐴 = ( 2o ·o 𝑥 ) ↔ ¬ ∃ 𝑥 ∈ ω suc 𝐴 = ( 2o ·o 𝑥 ) ) ) |