Step |
Hyp |
Ref |
Expression |
1 |
|
om2uz.1 |
⊢ 𝐶 ∈ ℤ |
2 |
|
om2uz.2 |
⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω ) |
3 |
|
eleq2 |
⊢ ( 𝑧 = ∅ → ( 𝐴 ∈ 𝑧 ↔ 𝐴 ∈ ∅ ) ) |
4 |
|
fveq2 |
⊢ ( 𝑧 = ∅ → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ ∅ ) ) |
5 |
4
|
breq2d |
⊢ ( 𝑧 = ∅ → ( ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑧 ) ↔ ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ ∅ ) ) ) |
6 |
3 5
|
imbi12d |
⊢ ( 𝑧 = ∅ → ( ( 𝐴 ∈ 𝑧 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑧 ) ) ↔ ( 𝐴 ∈ ∅ → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ ∅ ) ) ) ) |
7 |
6
|
imbi2d |
⊢ ( 𝑧 = ∅ → ( ( 𝐴 ∈ ω → ( 𝐴 ∈ 𝑧 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑧 ) ) ) ↔ ( 𝐴 ∈ ω → ( 𝐴 ∈ ∅ → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ ∅ ) ) ) ) ) |
8 |
|
eleq2 |
⊢ ( 𝑧 = 𝑦 → ( 𝐴 ∈ 𝑧 ↔ 𝐴 ∈ 𝑦 ) ) |
9 |
|
fveq2 |
⊢ ( 𝑧 = 𝑦 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑦 ) ) |
10 |
9
|
breq2d |
⊢ ( 𝑧 = 𝑦 → ( ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑧 ) ↔ ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ) ) |
11 |
8 10
|
imbi12d |
⊢ ( 𝑧 = 𝑦 → ( ( 𝐴 ∈ 𝑧 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑧 ) ) ↔ ( 𝐴 ∈ 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ) ) ) |
12 |
11
|
imbi2d |
⊢ ( 𝑧 = 𝑦 → ( ( 𝐴 ∈ ω → ( 𝐴 ∈ 𝑧 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑧 ) ) ) ↔ ( 𝐴 ∈ ω → ( 𝐴 ∈ 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ) ) ) ) |
13 |
|
eleq2 |
⊢ ( 𝑧 = suc 𝑦 → ( 𝐴 ∈ 𝑧 ↔ 𝐴 ∈ suc 𝑦 ) ) |
14 |
|
fveq2 |
⊢ ( 𝑧 = suc 𝑦 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ suc 𝑦 ) ) |
15 |
14
|
breq2d |
⊢ ( 𝑧 = suc 𝑦 → ( ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑧 ) ↔ ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ suc 𝑦 ) ) ) |
16 |
13 15
|
imbi12d |
⊢ ( 𝑧 = suc 𝑦 → ( ( 𝐴 ∈ 𝑧 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑧 ) ) ↔ ( 𝐴 ∈ suc 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ suc 𝑦 ) ) ) ) |
17 |
16
|
imbi2d |
⊢ ( 𝑧 = suc 𝑦 → ( ( 𝐴 ∈ ω → ( 𝐴 ∈ 𝑧 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑧 ) ) ) ↔ ( 𝐴 ∈ ω → ( 𝐴 ∈ suc 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ suc 𝑦 ) ) ) ) ) |
18 |
|
eleq2 |
⊢ ( 𝑧 = 𝐵 → ( 𝐴 ∈ 𝑧 ↔ 𝐴 ∈ 𝐵 ) ) |
19 |
|
fveq2 |
⊢ ( 𝑧 = 𝐵 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐵 ) ) |
20 |
19
|
breq2d |
⊢ ( 𝑧 = 𝐵 → ( ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑧 ) ↔ ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝐵 ) ) ) |
21 |
18 20
|
imbi12d |
⊢ ( 𝑧 = 𝐵 → ( ( 𝐴 ∈ 𝑧 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑧 ) ) ↔ ( 𝐴 ∈ 𝐵 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝐵 ) ) ) ) |
22 |
21
|
imbi2d |
⊢ ( 𝑧 = 𝐵 → ( ( 𝐴 ∈ ω → ( 𝐴 ∈ 𝑧 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑧 ) ) ) ↔ ( 𝐴 ∈ ω → ( 𝐴 ∈ 𝐵 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝐵 ) ) ) ) ) |
23 |
|
noel |
⊢ ¬ 𝐴 ∈ ∅ |
24 |
23
|
pm2.21i |
⊢ ( 𝐴 ∈ ∅ → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ ∅ ) ) |
25 |
24
|
a1i |
⊢ ( 𝐴 ∈ ω → ( 𝐴 ∈ ∅ → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ ∅ ) ) ) |
26 |
|
id |
⊢ ( ( 𝐴 ∈ 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ) → ( 𝐴 ∈ 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ) ) |
27 |
|
fveq2 |
⊢ ( 𝐴 = 𝑦 → ( 𝐺 ‘ 𝐴 ) = ( 𝐺 ‘ 𝑦 ) ) |
28 |
27
|
a1i |
⊢ ( ( 𝐴 ∈ 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ) → ( 𝐴 = 𝑦 → ( 𝐺 ‘ 𝐴 ) = ( 𝐺 ‘ 𝑦 ) ) ) |
29 |
26 28
|
orim12d |
⊢ ( ( 𝐴 ∈ 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ) → ( ( 𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ) → ( ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ∨ ( 𝐺 ‘ 𝐴 ) = ( 𝐺 ‘ 𝑦 ) ) ) ) |
30 |
|
elsuc2g |
⊢ ( 𝑦 ∈ ω → ( 𝐴 ∈ suc 𝑦 ↔ ( 𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ) ) ) |
31 |
30
|
bicomd |
⊢ ( 𝑦 ∈ ω → ( ( 𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ) ↔ 𝐴 ∈ suc 𝑦 ) ) |
32 |
31
|
adantl |
⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ) ↔ 𝐴 ∈ suc 𝑦 ) ) |
33 |
1 2
|
om2uzsuci |
⊢ ( 𝑦 ∈ ω → ( 𝐺 ‘ suc 𝑦 ) = ( ( 𝐺 ‘ 𝑦 ) + 1 ) ) |
34 |
33
|
breq2d |
⊢ ( 𝑦 ∈ ω → ( ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ suc 𝑦 ) ↔ ( 𝐺 ‘ 𝐴 ) < ( ( 𝐺 ‘ 𝑦 ) + 1 ) ) ) |
35 |
34
|
adantl |
⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ suc 𝑦 ) ↔ ( 𝐺 ‘ 𝐴 ) < ( ( 𝐺 ‘ 𝑦 ) + 1 ) ) ) |
36 |
1 2
|
om2uzuzi |
⊢ ( 𝐴 ∈ ω → ( 𝐺 ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝐶 ) ) |
37 |
1 2
|
om2uzuzi |
⊢ ( 𝑦 ∈ ω → ( 𝐺 ‘ 𝑦 ) ∈ ( ℤ≥ ‘ 𝐶 ) ) |
38 |
|
eluzelz |
⊢ ( ( 𝐺 ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝐶 ) → ( 𝐺 ‘ 𝐴 ) ∈ ℤ ) |
39 |
|
eluzelz |
⊢ ( ( 𝐺 ‘ 𝑦 ) ∈ ( ℤ≥ ‘ 𝐶 ) → ( 𝐺 ‘ 𝑦 ) ∈ ℤ ) |
40 |
|
zleltp1 |
⊢ ( ( ( 𝐺 ‘ 𝐴 ) ∈ ℤ ∧ ( 𝐺 ‘ 𝑦 ) ∈ ℤ ) → ( ( 𝐺 ‘ 𝐴 ) ≤ ( 𝐺 ‘ 𝑦 ) ↔ ( 𝐺 ‘ 𝐴 ) < ( ( 𝐺 ‘ 𝑦 ) + 1 ) ) ) |
41 |
38 39 40
|
syl2an |
⊢ ( ( ( 𝐺 ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝐶 ) ∧ ( 𝐺 ‘ 𝑦 ) ∈ ( ℤ≥ ‘ 𝐶 ) ) → ( ( 𝐺 ‘ 𝐴 ) ≤ ( 𝐺 ‘ 𝑦 ) ↔ ( 𝐺 ‘ 𝐴 ) < ( ( 𝐺 ‘ 𝑦 ) + 1 ) ) ) |
42 |
36 37 41
|
syl2an |
⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐺 ‘ 𝐴 ) ≤ ( 𝐺 ‘ 𝑦 ) ↔ ( 𝐺 ‘ 𝐴 ) < ( ( 𝐺 ‘ 𝑦 ) + 1 ) ) ) |
43 |
36 38
|
syl |
⊢ ( 𝐴 ∈ ω → ( 𝐺 ‘ 𝐴 ) ∈ ℤ ) |
44 |
43
|
zred |
⊢ ( 𝐴 ∈ ω → ( 𝐺 ‘ 𝐴 ) ∈ ℝ ) |
45 |
37 39
|
syl |
⊢ ( 𝑦 ∈ ω → ( 𝐺 ‘ 𝑦 ) ∈ ℤ ) |
46 |
45
|
zred |
⊢ ( 𝑦 ∈ ω → ( 𝐺 ‘ 𝑦 ) ∈ ℝ ) |
47 |
|
leloe |
⊢ ( ( ( 𝐺 ‘ 𝐴 ) ∈ ℝ ∧ ( 𝐺 ‘ 𝑦 ) ∈ ℝ ) → ( ( 𝐺 ‘ 𝐴 ) ≤ ( 𝐺 ‘ 𝑦 ) ↔ ( ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ∨ ( 𝐺 ‘ 𝐴 ) = ( 𝐺 ‘ 𝑦 ) ) ) ) |
48 |
44 46 47
|
syl2an |
⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐺 ‘ 𝐴 ) ≤ ( 𝐺 ‘ 𝑦 ) ↔ ( ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ∨ ( 𝐺 ‘ 𝐴 ) = ( 𝐺 ‘ 𝑦 ) ) ) ) |
49 |
35 42 48
|
3bitr2rd |
⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ∨ ( 𝐺 ‘ 𝐴 ) = ( 𝐺 ‘ 𝑦 ) ) ↔ ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ suc 𝑦 ) ) ) |
50 |
32 49
|
imbi12d |
⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( ( 𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ) → ( ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ∨ ( 𝐺 ‘ 𝐴 ) = ( 𝐺 ‘ 𝑦 ) ) ) ↔ ( 𝐴 ∈ suc 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ suc 𝑦 ) ) ) ) |
51 |
29 50
|
syl5ib |
⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 ∈ 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ) → ( 𝐴 ∈ suc 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ suc 𝑦 ) ) ) ) |
52 |
51
|
expcom |
⊢ ( 𝑦 ∈ ω → ( 𝐴 ∈ ω → ( ( 𝐴 ∈ 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ) → ( 𝐴 ∈ suc 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ suc 𝑦 ) ) ) ) ) |
53 |
52
|
a2d |
⊢ ( 𝑦 ∈ ω → ( ( 𝐴 ∈ ω → ( 𝐴 ∈ 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝐴 ∈ ω → ( 𝐴 ∈ suc 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ suc 𝑦 ) ) ) ) ) |
54 |
7 12 17 22 25 53
|
finds |
⊢ ( 𝐵 ∈ ω → ( 𝐴 ∈ ω → ( 𝐴 ∈ 𝐵 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝐵 ) ) ) ) |
55 |
54
|
impcom |
⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ∈ 𝐵 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝐵 ) ) ) |