Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑝 = (𝑚 + 1) → (𝐹‘𝑝) = (𝐹‘(𝑚 + 1))) |
2 | 1 | breq2d 4665 |
. . . . . . . . 9
⊢ (𝑝 = (𝑚 + 1) → ((𝐹‘𝑚)𝑅(𝐹‘𝑝) ↔ (𝐹‘𝑚)𝑅(𝐹‘(𝑚 + 1)))) |
3 | 2 | imbi2d 330 |
. . . . . . . 8
⊢ (𝑝 = (𝑚 + 1) → ((((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) ∧ (∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)) ∧ 𝑚 ∈ ℕ)) → (𝐹‘𝑚)𝑅(𝐹‘𝑝)) ↔ (((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) ∧ (∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)) ∧ 𝑚 ∈ ℕ)) → (𝐹‘𝑚)𝑅(𝐹‘(𝑚 + 1))))) |
4 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑞 → (𝐹‘𝑝) = (𝐹‘𝑞)) |
5 | 4 | breq2d 4665 |
. . . . . . . . 9
⊢ (𝑝 = 𝑞 → ((𝐹‘𝑚)𝑅(𝐹‘𝑝) ↔ (𝐹‘𝑚)𝑅(𝐹‘𝑞))) |
6 | 5 | imbi2d 330 |
. . . . . . . 8
⊢ (𝑝 = 𝑞 → ((((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) ∧ (∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)) ∧ 𝑚 ∈ ℕ)) → (𝐹‘𝑚)𝑅(𝐹‘𝑝)) ↔ (((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) ∧ (∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)) ∧ 𝑚 ∈ ℕ)) → (𝐹‘𝑚)𝑅(𝐹‘𝑞)))) |
7 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑝 = (𝑞 + 1) → (𝐹‘𝑝) = (𝐹‘(𝑞 + 1))) |
8 | 7 | breq2d 4665 |
. . . . . . . . 9
⊢ (𝑝 = (𝑞 + 1) → ((𝐹‘𝑚)𝑅(𝐹‘𝑝) ↔ (𝐹‘𝑚)𝑅(𝐹‘(𝑞 + 1)))) |
9 | 8 | imbi2d 330 |
. . . . . . . 8
⊢ (𝑝 = (𝑞 + 1) → ((((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) ∧ (∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)) ∧ 𝑚 ∈ ℕ)) → (𝐹‘𝑚)𝑅(𝐹‘𝑝)) ↔ (((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) ∧ (∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)) ∧ 𝑚 ∈ ℕ)) → (𝐹‘𝑚)𝑅(𝐹‘(𝑞 + 1))))) |
10 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑛 → (𝐹‘𝑝) = (𝐹‘𝑛)) |
11 | 10 | breq2d 4665 |
. . . . . . . . 9
⊢ (𝑝 = 𝑛 → ((𝐹‘𝑚)𝑅(𝐹‘𝑝) ↔ (𝐹‘𝑚)𝑅(𝐹‘𝑛))) |
12 | 11 | imbi2d 330 |
. . . . . . . 8
⊢ (𝑝 = 𝑛 → ((((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) ∧ (∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)) ∧ 𝑚 ∈ ℕ)) → (𝐹‘𝑚)𝑅(𝐹‘𝑝)) ↔ (((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) ∧ (∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)) ∧ 𝑚 ∈ ℕ)) → (𝐹‘𝑚)𝑅(𝐹‘𝑛)))) |
13 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑚 → (𝐹‘𝑠) = (𝐹‘𝑚)) |
14 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝑠 = 𝑚 → (𝑠 + 1) = (𝑚 + 1)) |
15 | 14 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑚 → (𝐹‘(𝑠 + 1)) = (𝐹‘(𝑚 + 1))) |
16 | 13, 15 | breq12d 4666 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑚 → ((𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)) ↔ (𝐹‘𝑚)𝑅(𝐹‘(𝑚 + 1)))) |
17 | 16 | rspccva 3308 |
. . . . . . . . . 10
⊢
((∀𝑠 ∈
ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)) ∧ 𝑚 ∈ ℕ) → (𝐹‘𝑚)𝑅(𝐹‘(𝑚 + 1))) |
18 | 17 | adantl 482 |
. . . . . . . . 9
⊢ (((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) ∧ (∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)) ∧ 𝑚 ∈ ℕ)) → (𝐹‘𝑚)𝑅(𝐹‘(𝑚 + 1))) |
19 | 18 | a1i 11 |
. . . . . . . 8
⊢ ((𝑚 + 1) ∈ ℤ →
(((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) ∧ (∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)) ∧ 𝑚 ∈ ℕ)) → (𝐹‘𝑚)𝑅(𝐹‘(𝑚 + 1)))) |
20 | | peano2nn 11032 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ℕ → (𝑚 + 1) ∈
ℕ) |
21 | | elnnuz 11724 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 + 1) ∈ ℕ ↔
(𝑚 + 1) ∈
(ℤ≥‘1)) |
22 | 20, 21 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ → (𝑚 + 1) ∈
(ℤ≥‘1)) |
23 | | uztrn 11704 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑞 ∈
(ℤ≥‘(𝑚 + 1)) ∧ (𝑚 + 1) ∈
(ℤ≥‘1)) → 𝑞 ∈
(ℤ≥‘1)) |
24 | | elnnuz 11724 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑞 ∈ ℕ ↔ 𝑞 ∈
(ℤ≥‘1)) |
25 | 23, 24 | sylibr 224 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈
(ℤ≥‘(𝑚 + 1)) ∧ (𝑚 + 1) ∈
(ℤ≥‘1)) → 𝑞 ∈ ℕ) |
26 | 25 | expcom 451 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 + 1) ∈
(ℤ≥‘1) → (𝑞 ∈ (ℤ≥‘(𝑚 + 1)) → 𝑞 ∈ ℕ)) |
27 | 22, 26 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ → (𝑞 ∈
(ℤ≥‘(𝑚 + 1)) → 𝑞 ∈ ℕ)) |
28 | 27 | imdistani 726 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ ∧ 𝑞 ∈
(ℤ≥‘(𝑚 + 1))) → (𝑚 ∈ ℕ ∧ 𝑞 ∈ ℕ)) |
29 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 = 𝑞 → (𝐹‘𝑠) = (𝐹‘𝑞)) |
30 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = 𝑞 → (𝑠 + 1) = (𝑞 + 1)) |
31 | 30 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 = 𝑞 → (𝐹‘(𝑠 + 1)) = (𝐹‘(𝑞 + 1))) |
32 | 29, 31 | breq12d 4666 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = 𝑞 → ((𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)) ↔ (𝐹‘𝑞)𝑅(𝐹‘(𝑞 + 1)))) |
33 | 32 | rspccva 3308 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑠 ∈
ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)) ∧ 𝑞 ∈ ℕ) → (𝐹‘𝑞)𝑅(𝐹‘(𝑞 + 1))) |
34 | 33 | ad2ant2l 782 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) ∧ ∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1))) ∧ (𝑚 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (𝐹‘𝑞)𝑅(𝐹‘(𝑞 + 1))) |
35 | 34 | ex 450 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) ∧ ∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1))) → ((𝑚 ∈ ℕ ∧ 𝑞 ∈ ℕ) → (𝐹‘𝑞)𝑅(𝐹‘(𝑞 + 1)))) |
36 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹:ℕ⟶𝐴 ∧ 𝑚 ∈ ℕ) → (𝐹‘𝑚) ∈ 𝐴) |
37 | 36 | adantrr 753 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:ℕ⟶𝐴 ∧ (𝑚 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (𝐹‘𝑚) ∈ 𝐴) |
38 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹:ℕ⟶𝐴 ∧ 𝑞 ∈ ℕ) → (𝐹‘𝑞) ∈ 𝐴) |
39 | 38 | adantrl 752 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:ℕ⟶𝐴 ∧ (𝑚 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (𝐹‘𝑞) ∈ 𝐴) |
40 | | peano2nn 11032 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑞 ∈ ℕ → (𝑞 + 1) ∈
ℕ) |
41 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹:ℕ⟶𝐴 ∧ (𝑞 + 1) ∈ ℕ) → (𝐹‘(𝑞 + 1)) ∈ 𝐴) |
42 | 40, 41 | sylan2 491 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹:ℕ⟶𝐴 ∧ 𝑞 ∈ ℕ) → (𝐹‘(𝑞 + 1)) ∈ 𝐴) |
43 | 42 | adantrl 752 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹:ℕ⟶𝐴 ∧ (𝑚 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → (𝐹‘(𝑞 + 1)) ∈ 𝐴) |
44 | 37, 39, 43 | 3jca 1242 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹:ℕ⟶𝐴 ∧ (𝑚 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → ((𝐹‘𝑚) ∈ 𝐴 ∧ (𝐹‘𝑞) ∈ 𝐴 ∧ (𝐹‘(𝑞 + 1)) ∈ 𝐴)) |
45 | | potr 5047 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 Po 𝐴 ∧ ((𝐹‘𝑚) ∈ 𝐴 ∧ (𝐹‘𝑞) ∈ 𝐴 ∧ (𝐹‘(𝑞 + 1)) ∈ 𝐴)) → (((𝐹‘𝑚)𝑅(𝐹‘𝑞) ∧ (𝐹‘𝑞)𝑅(𝐹‘(𝑞 + 1))) → (𝐹‘𝑚)𝑅(𝐹‘(𝑞 + 1)))) |
46 | 45 | expcomd 454 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 Po 𝐴 ∧ ((𝐹‘𝑚) ∈ 𝐴 ∧ (𝐹‘𝑞) ∈ 𝐴 ∧ (𝐹‘(𝑞 + 1)) ∈ 𝐴)) → ((𝐹‘𝑞)𝑅(𝐹‘(𝑞 + 1)) → ((𝐹‘𝑚)𝑅(𝐹‘𝑞) → (𝐹‘𝑚)𝑅(𝐹‘(𝑞 + 1))))) |
47 | 46 | ex 450 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 Po 𝐴 → (((𝐹‘𝑚) ∈ 𝐴 ∧ (𝐹‘𝑞) ∈ 𝐴 ∧ (𝐹‘(𝑞 + 1)) ∈ 𝐴) → ((𝐹‘𝑞)𝑅(𝐹‘(𝑞 + 1)) → ((𝐹‘𝑚)𝑅(𝐹‘𝑞) → (𝐹‘𝑚)𝑅(𝐹‘(𝑞 + 1)))))) |
48 | 44, 47 | syl5 34 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 Po 𝐴 → ((𝐹:ℕ⟶𝐴 ∧ (𝑚 ∈ ℕ ∧ 𝑞 ∈ ℕ)) → ((𝐹‘𝑞)𝑅(𝐹‘(𝑞 + 1)) → ((𝐹‘𝑚)𝑅(𝐹‘𝑞) → (𝐹‘𝑚)𝑅(𝐹‘(𝑞 + 1)))))) |
49 | 48 | expdimp 453 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) → ((𝑚 ∈ ℕ ∧ 𝑞 ∈ ℕ) → ((𝐹‘𝑞)𝑅(𝐹‘(𝑞 + 1)) → ((𝐹‘𝑚)𝑅(𝐹‘𝑞) → (𝐹‘𝑚)𝑅(𝐹‘(𝑞 + 1)))))) |
50 | 49 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) ∧ ∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1))) → ((𝑚 ∈ ℕ ∧ 𝑞 ∈ ℕ) → ((𝐹‘𝑞)𝑅(𝐹‘(𝑞 + 1)) → ((𝐹‘𝑚)𝑅(𝐹‘𝑞) → (𝐹‘𝑚)𝑅(𝐹‘(𝑞 + 1)))))) |
51 | 35, 50 | mpdd 43 |
. . . . . . . . . . . . 13
⊢ (((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) ∧ ∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1))) → ((𝑚 ∈ ℕ ∧ 𝑞 ∈ ℕ) → ((𝐹‘𝑚)𝑅(𝐹‘𝑞) → (𝐹‘𝑚)𝑅(𝐹‘(𝑞 + 1))))) |
52 | 28, 51 | syl5 34 |
. . . . . . . . . . . 12
⊢ (((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) ∧ ∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1))) → ((𝑚 ∈ ℕ ∧ 𝑞 ∈ (ℤ≥‘(𝑚 + 1))) → ((𝐹‘𝑚)𝑅(𝐹‘𝑞) → (𝐹‘𝑚)𝑅(𝐹‘(𝑞 + 1))))) |
53 | 52 | expdimp 453 |
. . . . . . . . . . 11
⊢ ((((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) ∧ ∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1))) ∧ 𝑚 ∈ ℕ) → (𝑞 ∈ (ℤ≥‘(𝑚 + 1)) → ((𝐹‘𝑚)𝑅(𝐹‘𝑞) → (𝐹‘𝑚)𝑅(𝐹‘(𝑞 + 1))))) |
54 | 53 | anasss 679 |
. . . . . . . . . 10
⊢ (((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) ∧ (∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)) ∧ 𝑚 ∈ ℕ)) → (𝑞 ∈ (ℤ≥‘(𝑚 + 1)) → ((𝐹‘𝑚)𝑅(𝐹‘𝑞) → (𝐹‘𝑚)𝑅(𝐹‘(𝑞 + 1))))) |
55 | 54 | com12 32 |
. . . . . . . . 9
⊢ (𝑞 ∈
(ℤ≥‘(𝑚 + 1)) → (((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) ∧ (∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)) ∧ 𝑚 ∈ ℕ)) → ((𝐹‘𝑚)𝑅(𝐹‘𝑞) → (𝐹‘𝑚)𝑅(𝐹‘(𝑞 + 1))))) |
56 | 55 | a2d 29 |
. . . . . . . 8
⊢ (𝑞 ∈
(ℤ≥‘(𝑚 + 1)) → ((((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) ∧ (∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)) ∧ 𝑚 ∈ ℕ)) → (𝐹‘𝑚)𝑅(𝐹‘𝑞)) → (((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) ∧ (∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)) ∧ 𝑚 ∈ ℕ)) → (𝐹‘𝑚)𝑅(𝐹‘(𝑞 + 1))))) |
57 | 3, 6, 9, 12, 19, 56 | uzind4 11746 |
. . . . . . 7
⊢ (𝑛 ∈
(ℤ≥‘(𝑚 + 1)) → (((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) ∧ (∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)) ∧ 𝑚 ∈ ℕ)) → (𝐹‘𝑚)𝑅(𝐹‘𝑛))) |
58 | 57 | com12 32 |
. . . . . 6
⊢ (((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) ∧ (∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)) ∧ 𝑚 ∈ ℕ)) → (𝑛 ∈ (ℤ≥‘(𝑚 + 1)) → (𝐹‘𝑚)𝑅(𝐹‘𝑛))) |
59 | 58 | ralrimiv 2965 |
. . . . 5
⊢ (((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) ∧ (∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)) ∧ 𝑚 ∈ ℕ)) → ∀𝑛 ∈
(ℤ≥‘(𝑚 + 1))(𝐹‘𝑚)𝑅(𝐹‘𝑛)) |
60 | 59 | anassrs 680 |
. . . 4
⊢ ((((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) ∧ ∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1))) ∧ 𝑚 ∈ ℕ) → ∀𝑛 ∈
(ℤ≥‘(𝑚 + 1))(𝐹‘𝑚)𝑅(𝐹‘𝑛)) |
61 | 60 | ralrimiva 2966 |
. . 3
⊢ (((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) ∧ ∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1))) → ∀𝑚 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘(𝑚 + 1))(𝐹‘𝑚)𝑅(𝐹‘𝑛)) |
62 | 61 | ex 450 |
. 2
⊢ ((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) → (∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)) → ∀𝑚 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘(𝑚 + 1))(𝐹‘𝑚)𝑅(𝐹‘𝑛))) |
63 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑚 = 𝑠 → (𝑚 + 1) = (𝑠 + 1)) |
64 | 63 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑚 = 𝑠 → (ℤ≥‘(𝑚 + 1)) =
(ℤ≥‘(𝑠 + 1))) |
65 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑚 = 𝑠 → (𝐹‘𝑚) = (𝐹‘𝑠)) |
66 | 65 | breq1d 4663 |
. . . . . . 7
⊢ (𝑚 = 𝑠 → ((𝐹‘𝑚)𝑅(𝐹‘𝑛) ↔ (𝐹‘𝑠)𝑅(𝐹‘𝑛))) |
67 | 64, 66 | raleqbidv 3152 |
. . . . . 6
⊢ (𝑚 = 𝑠 → (∀𝑛 ∈ (ℤ≥‘(𝑚 + 1))(𝐹‘𝑚)𝑅(𝐹‘𝑛) ↔ ∀𝑛 ∈ (ℤ≥‘(𝑠 + 1))(𝐹‘𝑠)𝑅(𝐹‘𝑛))) |
68 | 67 | rspcv 3305 |
. . . . 5
⊢ (𝑠 ∈ ℕ →
(∀𝑚 ∈ ℕ
∀𝑛 ∈
(ℤ≥‘(𝑚 + 1))(𝐹‘𝑚)𝑅(𝐹‘𝑛) → ∀𝑛 ∈ (ℤ≥‘(𝑠 + 1))(𝐹‘𝑠)𝑅(𝐹‘𝑛))) |
69 | 68 | imdistanri 727 |
. . . 4
⊢
((∀𝑚 ∈
ℕ ∀𝑛 ∈
(ℤ≥‘(𝑚 + 1))(𝐹‘𝑚)𝑅(𝐹‘𝑛) ∧ 𝑠 ∈ ℕ) → (∀𝑛 ∈
(ℤ≥‘(𝑠 + 1))(𝐹‘𝑠)𝑅(𝐹‘𝑛) ∧ 𝑠 ∈ ℕ)) |
70 | | peano2nn 11032 |
. . . . . . 7
⊢ (𝑠 ∈ ℕ → (𝑠 + 1) ∈
ℕ) |
71 | 70 | nnzd 11481 |
. . . . . 6
⊢ (𝑠 ∈ ℕ → (𝑠 + 1) ∈
ℤ) |
72 | | uzid 11702 |
. . . . . 6
⊢ ((𝑠 + 1) ∈ ℤ →
(𝑠 + 1) ∈
(ℤ≥‘(𝑠 + 1))) |
73 | 71, 72 | syl 17 |
. . . . 5
⊢ (𝑠 ∈ ℕ → (𝑠 + 1) ∈
(ℤ≥‘(𝑠 + 1))) |
74 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑛 = (𝑠 + 1) → (𝐹‘𝑛) = (𝐹‘(𝑠 + 1))) |
75 | 74 | breq2d 4665 |
. . . . . 6
⊢ (𝑛 = (𝑠 + 1) → ((𝐹‘𝑠)𝑅(𝐹‘𝑛) ↔ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)))) |
76 | 75 | rspccva 3308 |
. . . . 5
⊢
((∀𝑛 ∈
(ℤ≥‘(𝑠 + 1))(𝐹‘𝑠)𝑅(𝐹‘𝑛) ∧ (𝑠 + 1) ∈
(ℤ≥‘(𝑠 + 1))) → (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1))) |
77 | 73, 76 | sylan2 491 |
. . . 4
⊢
((∀𝑛 ∈
(ℤ≥‘(𝑠 + 1))(𝐹‘𝑠)𝑅(𝐹‘𝑛) ∧ 𝑠 ∈ ℕ) → (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1))) |
78 | 69, 77 | syl 17 |
. . 3
⊢
((∀𝑚 ∈
ℕ ∀𝑛 ∈
(ℤ≥‘(𝑚 + 1))(𝐹‘𝑚)𝑅(𝐹‘𝑛) ∧ 𝑠 ∈ ℕ) → (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1))) |
79 | 78 | ralrimiva 2966 |
. 2
⊢
(∀𝑚 ∈
ℕ ∀𝑛 ∈
(ℤ≥‘(𝑚 + 1))(𝐹‘𝑚)𝑅(𝐹‘𝑛) → ∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1))) |
80 | 62, 79 | impbid1 215 |
1
⊢ ((𝑅 Po 𝐴 ∧ 𝐹:ℕ⟶𝐴) → (∀𝑠 ∈ ℕ (𝐹‘𝑠)𝑅(𝐹‘(𝑠 + 1)) ↔ ∀𝑚 ∈ ℕ ∀𝑛 ∈ (ℤ≥‘(𝑚 + 1))(𝐹‘𝑚)𝑅(𝐹‘𝑛))) |