Step | Hyp | Ref
| Expression |
1 | | wrdf 13165 |
. . . 4
⊢ (𝐹 ∈ Word dom 𝐸 → 𝐹:(0..^(#‘𝐹))⟶dom 𝐸) |
2 | 1 | 3ad2ant1 1075 |
. . 3
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → 𝐹:(0..^(#‘𝐹))⟶dom 𝐸) |
3 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑥 → (𝐹‘𝑘) = (𝐹‘𝑥)) |
4 | 3 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑥 → (𝐸‘(𝐹‘𝑘)) = (𝐸‘(𝐹‘𝑥))) |
5 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑥 → (𝑃‘𝑘) = (𝑃‘𝑥)) |
6 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑥 → (𝑘 + 1) = (𝑥 + 1)) |
7 | 6 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑥 → (𝑃‘(𝑘 + 1)) = (𝑃‘(𝑥 + 1))) |
8 | 5, 7 | preq12d 4220 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑥 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) |
9 | 4, 8 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑥 → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ (𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) |
10 | 9 | rspcva 3280 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (0..^(#‘𝐹)) ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) |
11 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 𝑦 → (𝐹‘𝑘) = (𝐹‘𝑦)) |
12 | 11 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑦 → (𝐸‘(𝐹‘𝑘)) = (𝐸‘(𝐹‘𝑦))) |
13 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 𝑦 → (𝑃‘𝑘) = (𝑃‘𝑦)) |
14 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = 𝑦 → (𝑘 + 1) = (𝑦 + 1)) |
15 | 14 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 𝑦 → (𝑃‘(𝑘 + 1)) = (𝑃‘(𝑦 + 1))) |
16 | 13, 15 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑦 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))}) |
17 | 12, 16 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑦 → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ (𝐸‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))})) |
18 | 17 | rspcva 3280 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ (0..^(#‘𝐹)) ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (𝐸‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))}) |
19 | | pm3.2 462 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐸‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} → ((𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} → ((𝐸‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} ∧ (𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ (0..^(#‘𝐹)) ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → ((𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} → ((𝐸‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} ∧ (𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))) |
21 | 20 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (0..^(#‘𝐹)) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → ((𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} → ((𝐸‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} ∧ (𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})))) |
22 | 21 | com3r 85 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} → (𝑦 ∈ (0..^(#‘𝐹)) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → ((𝐸‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} ∧ (𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})))) |
23 | 10, 22 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (0..^(#‘𝐹)) ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (𝑦 ∈ (0..^(#‘𝐹)) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → ((𝐸‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} ∧ (𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})))) |
24 | 23 | impancom 455 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → ((𝐸‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} ∧ (𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})))) |
25 | 24 | com3r 85 |
. . . . . . . . . . . . 13
⊢
(∀𝑘 ∈
(0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → ((𝐸‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} ∧ (𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})))) |
26 | 25 | pm2.43a 52 |
. . . . . . . . . . . 12
⊢
(∀𝑘 ∈
(0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ((𝐸‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} ∧ (𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))) |
27 | 26 | impcom 445 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → ((𝐸‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} ∧ (𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) |
28 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑥) = (𝐹‘𝑦) → (𝐸‘(𝐹‘𝑥)) = (𝐸‘(𝐹‘𝑦))) |
29 | | eqtr2 2630 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐸‘(𝐹‘𝑦)) = (𝐸‘(𝐹‘𝑥)) ∧ (𝐸‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))}) → (𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))}) |
30 | 29 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐸‘(𝐹‘𝑦)) = (𝐸‘(𝐹‘𝑥)) → ((𝐸‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} → (𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))})) |
31 | 30 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐸‘(𝐹‘𝑥)) = (𝐸‘(𝐹‘𝑦)) → ((𝐸‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} → (𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))})) |
32 | | eqtr2 2630 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} ∧ (𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) → {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) |
33 | 32 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} → ((𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} → {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) |
34 | 31, 33 | syl6com 36 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} → ((𝐸‘(𝐹‘𝑥)) = (𝐸‘(𝐹‘𝑦)) → ((𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} → {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))) |
35 | 34 | com23 84 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐸‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} → ((𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} → ((𝐸‘(𝐹‘𝑥)) = (𝐸‘(𝐹‘𝑦)) → {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}))) |
36 | 35 | imp 444 |
. . . . . . . . . . . . . . 15
⊢ (((𝐸‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} ∧ (𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) → ((𝐸‘(𝐹‘𝑥)) = (𝐸‘(𝐹‘𝑦)) → {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) |
37 | | elfzofz 12354 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 ∈ (0..^(#‘𝐹)) → 𝑥 ∈ (0...(#‘𝐹))) |
38 | | elfzofz 12354 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 ∈ (0..^(#‘𝐹)) → 𝑦 ∈ (0...(#‘𝐹))) |
39 | 37, 38 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (𝑥 ∈ (0...(#‘𝐹)) ∧ 𝑦 ∈ (0...(#‘𝐹)))) |
40 | 39 | anim2i 591 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ (𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → (𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ (𝑥 ∈ (0...(#‘𝐹)) ∧ 𝑦 ∈ (0...(#‘𝐹))))) |
41 | 40 | ancoms 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → (𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ (𝑥 ∈ (0...(#‘𝐹)) ∧ 𝑦 ∈ (0...(#‘𝐹))))) |
42 | | f1fveq 6420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ (𝑥 ∈ (0...(#‘𝐹)) ∧ 𝑦 ∈ (0...(#‘𝐹)))) → ((𝑃‘𝑥) = (𝑃‘𝑦) ↔ 𝑥 = 𝑦)) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → ((𝑃‘𝑥) = (𝑃‘𝑦) ↔ 𝑥 = 𝑦)) |
44 | 43 | notbid 307 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → (¬ (𝑃‘𝑥) = (𝑃‘𝑦) ↔ ¬ 𝑥 = 𝑦)) |
45 | 44 | biimparc 503 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((¬
𝑥 = 𝑦 ∧ ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉)) → ¬ (𝑃‘𝑥) = (𝑃‘𝑦)) |
46 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → 𝑃:(0...(#‘𝐹))–1-1→𝑉) |
47 | | fzofzp1 12431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑥 ∈ (0..^(#‘𝐹)) → (𝑥 + 1) ∈ (0...(#‘𝐹))) |
48 | | fzofzp1 12431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 ∈ (0..^(#‘𝐹)) → (𝑦 + 1) ∈ (0...(#‘𝐹))) |
49 | 47, 48 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ((𝑥 + 1) ∈ (0...(#‘𝐹)) ∧ (𝑦 + 1) ∈ (0...(#‘𝐹)))) |
50 | 49 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → ((𝑥 + 1) ∈ (0...(#‘𝐹)) ∧ (𝑦 + 1) ∈ (0...(#‘𝐹)))) |
51 | | f1fveq 6420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ ((𝑥 + 1) ∈ (0...(#‘𝐹)) ∧ (𝑦 + 1) ∈ (0...(#‘𝐹)))) → ((𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1)) ↔ (𝑥 + 1) = (𝑦 + 1))) |
52 | 46, 50, 51 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → ((𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1)) ↔ (𝑥 + 1) = (𝑦 + 1))) |
53 | | elfzoelz 12339 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑥 ∈ (0..^(#‘𝐹)) → 𝑥 ∈ ℤ) |
54 | 53 | zcnd 11359 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 ∈ (0..^(#‘𝐹)) → 𝑥 ∈ ℂ) |
55 | 54 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → 𝑥 ∈ ℂ) |
56 | | elfzoelz 12339 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 ∈ (0..^(#‘𝐹)) → 𝑦 ∈ ℤ) |
57 | 56 | zcnd 11359 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 ∈ (0..^(#‘𝐹)) → 𝑦 ∈ ℂ) |
58 | 57 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑦 ∈ ℂ) |
59 | 58 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → 𝑦 ∈ ℂ) |
60 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → 1 ∈ ℂ) |
61 | 55, 59, 60 | addcan2d 10119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → ((𝑥 + 1) = (𝑦 + 1) ↔ 𝑥 = 𝑦)) |
62 | 52, 61 | bitrd 267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → ((𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1)) ↔ 𝑥 = 𝑦)) |
63 | 62 | notbid 307 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → (¬ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1)) ↔ ¬ 𝑥 = 𝑦)) |
64 | | pm3.2 462 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (¬
(𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1)) → (¬ (𝑃‘𝑥) = (𝑃‘𝑦) → (¬ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1)) ∧ ¬ (𝑃‘𝑥) = (𝑃‘𝑦)))) |
65 | 63, 64 | syl6bir 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → (¬ 𝑥 = 𝑦 → (¬ (𝑃‘𝑥) = (𝑃‘𝑦) → (¬ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1)) ∧ ¬ (𝑃‘𝑥) = (𝑃‘𝑦))))) |
66 | 65 | com13 86 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
(𝑃‘𝑥) = (𝑃‘𝑦) → (¬ 𝑥 = 𝑦 → (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → (¬ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1)) ∧ ¬ (𝑃‘𝑥) = (𝑃‘𝑦))))) |
67 | 45, 66 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((¬
𝑥 = 𝑦 ∧ ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉)) → (¬ 𝑥 = 𝑦 → (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → (¬ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1)) ∧ ¬ (𝑃‘𝑥) = (𝑃‘𝑦))))) |
68 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃‘𝑦) ∈ V |
69 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃‘(𝑦 + 1)) ∈ V |
70 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃‘𝑥) ∈ V |
71 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑃‘(𝑥 + 1)) ∈ V |
72 | 68, 69, 70, 71 | preq12b 4322 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ({(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ↔ (((𝑃‘𝑦) = (𝑃‘𝑥) ∧ (𝑃‘(𝑦 + 1)) = (𝑃‘(𝑥 + 1))) ∨ ((𝑃‘𝑦) = (𝑃‘(𝑥 + 1)) ∧ (𝑃‘(𝑦 + 1)) = (𝑃‘𝑥)))) |
73 | | pm2.24 120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1)) → (¬ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1)) → (𝑃‘𝑦) = (𝑃‘(𝑥 + 1)))) |
74 | 73 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑃‘(𝑦 + 1)) = (𝑃‘(𝑥 + 1)) → (¬ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1)) → (𝑃‘𝑦) = (𝑃‘(𝑥 + 1)))) |
75 | | pm2.24 120 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑃‘𝑥) = (𝑃‘𝑦) → (¬ (𝑃‘𝑥) = (𝑃‘𝑦) → (𝑃‘(𝑦 + 1)) = (𝑃‘𝑥))) |
76 | 75 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑃‘𝑦) = (𝑃‘𝑥) → (¬ (𝑃‘𝑥) = (𝑃‘𝑦) → (𝑃‘(𝑦 + 1)) = (𝑃‘𝑥))) |
77 | 74, 76 | im2anan9r 877 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑃‘𝑦) = (𝑃‘𝑥) ∧ (𝑃‘(𝑦 + 1)) = (𝑃‘(𝑥 + 1))) → ((¬ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1)) ∧ ¬ (𝑃‘𝑥) = (𝑃‘𝑦)) → ((𝑃‘𝑦) = (𝑃‘(𝑥 + 1)) ∧ (𝑃‘(𝑦 + 1)) = (𝑃‘𝑥)))) |
78 | | ax-1 6 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑃‘𝑦) = (𝑃‘(𝑥 + 1)) ∧ (𝑃‘(𝑦 + 1)) = (𝑃‘𝑥)) → ((¬ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1)) ∧ ¬ (𝑃‘𝑥) = (𝑃‘𝑦)) → ((𝑃‘𝑦) = (𝑃‘(𝑥 + 1)) ∧ (𝑃‘(𝑦 + 1)) = (𝑃‘𝑥)))) |
79 | 77, 78 | jaoi 393 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑃‘𝑦) = (𝑃‘𝑥) ∧ (𝑃‘(𝑦 + 1)) = (𝑃‘(𝑥 + 1))) ∨ ((𝑃‘𝑦) = (𝑃‘(𝑥 + 1)) ∧ (𝑃‘(𝑦 + 1)) = (𝑃‘𝑥))) → ((¬ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1)) ∧ ¬ (𝑃‘𝑥) = (𝑃‘𝑦)) → ((𝑃‘𝑦) = (𝑃‘(𝑥 + 1)) ∧ (𝑃‘(𝑦 + 1)) = (𝑃‘𝑥)))) |
80 | 72, 79 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ({(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} → ((¬ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1)) ∧ ¬ (𝑃‘𝑥) = (𝑃‘𝑦)) → ((𝑃‘𝑦) = (𝑃‘(𝑥 + 1)) ∧ (𝑃‘(𝑦 + 1)) = (𝑃‘𝑥)))) |
81 | 37, 48 | anim12ci 589 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ((𝑦 + 1) ∈ (0...(#‘𝐹)) ∧ 𝑥 ∈ (0...(#‘𝐹)))) |
82 | | f1fveq 6420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ ((𝑦 + 1) ∈ (0...(#‘𝐹)) ∧ 𝑥 ∈ (0...(#‘𝐹)))) → ((𝑃‘(𝑦 + 1)) = (𝑃‘𝑥) ↔ (𝑦 + 1) = 𝑥)) |
83 | 81, 82 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ (𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → ((𝑃‘(𝑦 + 1)) = (𝑃‘𝑥) ↔ (𝑦 + 1) = 𝑥)) |
84 | 83 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ (𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → ((𝑃‘(𝑦 + 1)) = (𝑃‘𝑥) → (𝑦 + 1) = 𝑥)) |
85 | 84 | ancoms 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → ((𝑃‘(𝑦 + 1)) = (𝑃‘𝑥) → (𝑦 + 1) = 𝑥)) |
86 | 47, 38 | anim12ci 589 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (𝑦 ∈ (0...(#‘𝐹)) ∧ (𝑥 + 1) ∈ (0...(#‘𝐹)))) |
87 | | f1fveq 6420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ (𝑦 ∈ (0...(#‘𝐹)) ∧ (𝑥 + 1) ∈ (0...(#‘𝐹)))) → ((𝑃‘𝑦) = (𝑃‘(𝑥 + 1)) ↔ 𝑦 = (𝑥 + 1))) |
88 | 86, 87 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ (𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → ((𝑃‘𝑦) = (𝑃‘(𝑥 + 1)) ↔ 𝑦 = (𝑥 + 1))) |
89 | 88 | ancoms 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → ((𝑃‘𝑦) = (𝑃‘(𝑥 + 1)) ↔ 𝑦 = (𝑥 + 1))) |
90 | 89 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) ∧ (𝑃‘𝑦) = (𝑃‘(𝑥 + 1))) → 𝑦 = (𝑥 + 1)) |
91 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑦 = (𝑥 + 1) → (𝑦 + 1) = ((𝑥 + 1) + 1)) |
92 | 91 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑦 = (𝑥 + 1) → ((𝑦 + 1) = 𝑥 ↔ ((𝑥 + 1) + 1) = 𝑥)) |
93 | 92 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑦 = (𝑥 + 1)) → ((𝑦 + 1) = 𝑥 ↔ ((𝑥 + 1) + 1) = 𝑥)) |
94 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑥 ∈ (0..^(#‘𝐹)) → 1 ∈
ℂ) |
95 | 54, 94, 94 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑥 ∈ (0..^(#‘𝐹)) → (𝑥 ∈ ℂ ∧ 1 ∈ ℂ ∧
1 ∈ ℂ)) |
96 | 95 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑦 = (𝑥 + 1)) → (𝑥 ∈ ℂ ∧ 1 ∈ ℂ ∧
1 ∈ ℂ)) |
97 | | addass 9902 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑥 ∈ ℂ ∧ 1 ∈
ℂ ∧ 1 ∈ ℂ) → ((𝑥 + 1) + 1) = (𝑥 + (1 + 1))) |
98 | 97 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑥 ∈ ℂ ∧ 1 ∈
ℂ ∧ 1 ∈ ℂ) → (((𝑥 + 1) + 1) = 𝑥 ↔ (𝑥 + (1 + 1)) = 𝑥)) |
99 | 96, 98 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑦 = (𝑥 + 1)) → (((𝑥 + 1) + 1) = 𝑥 ↔ (𝑥 + (1 + 1)) = 𝑥)) |
100 | | 1p1e2 11011 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (1 + 1) =
2 |
101 | 100 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑥 + (1 + 1)) = (𝑥 + 2) |
102 | 101 | eqeq1i 2615 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑥 + (1 + 1)) = 𝑥 ↔ (𝑥 + 2) = 𝑥) |
103 | | zcn 11259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
104 | | 2cn 10968 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ 2 ∈
ℂ |
105 | 103, 104 | jctir 559 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝑥 ∈ ℤ → (𝑥 ∈ ℂ ∧ 2 ∈
ℂ)) |
106 | | addcl 9897 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑥 ∈ ℂ ∧ 2 ∈
ℂ) → (𝑥 + 2)
∈ ℂ) |
107 | 105, 106 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑥 ∈ ℤ → (𝑥 + 2) ∈
ℂ) |
108 | 107, 103,
103 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑥 ∈ ℤ → ((𝑥 + 2) ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑥 ∈
ℂ)) |
109 | | subcan2 10185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑥 + 2) ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (((𝑥 + 2) − 𝑥) = (𝑥 − 𝑥) ↔ (𝑥 + 2) = 𝑥)) |
110 | 109 | bicomd 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑥 + 2) ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((𝑥 + 2) = 𝑥 ↔ ((𝑥 + 2) − 𝑥) = (𝑥 − 𝑥))) |
111 | 53, 108, 110 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑥 ∈ (0..^(#‘𝐹)) → ((𝑥 + 2) = 𝑥 ↔ ((𝑥 + 2) − 𝑥) = (𝑥 − 𝑥))) |
112 | | pncan2 10167 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑥 ∈ ℂ ∧ 2 ∈
ℂ) → ((𝑥 + 2)
− 𝑥) =
2) |
113 | 53, 105, 112 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑥 ∈ (0..^(#‘𝐹)) → ((𝑥 + 2) − 𝑥) = 2) |
114 | 54 | subidd 10259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑥 ∈ (0..^(#‘𝐹)) → (𝑥 − 𝑥) = 0) |
115 | 113, 114 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑥 ∈ (0..^(#‘𝐹)) → (((𝑥 + 2) − 𝑥) = (𝑥 − 𝑥) ↔ 2 = 0)) |
116 | 111, 115 | bitrd 267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑥 ∈ (0..^(#‘𝐹)) → ((𝑥 + 2) = 𝑥 ↔ 2 = 0)) |
117 | 102, 116 | syl5bb 271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑥 ∈ (0..^(#‘𝐹)) → ((𝑥 + (1 + 1)) = 𝑥 ↔ 2 = 0)) |
118 | 117 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑦 = (𝑥 + 1)) → ((𝑥 + (1 + 1)) = 𝑥 ↔ 2 = 0)) |
119 | 93, 99, 118 | 3bitrd 293 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑦 = (𝑥 + 1)) → ((𝑦 + 1) = 𝑥 ↔ 2 = 0)) |
120 | | 2ne0 10990 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ 2 ≠
0 |
121 | | df-ne 2782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (2 ≠ 0
↔ ¬ 2 = 0) |
122 | | pm2.21 119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (¬ 2
= 0 → (2 = 0 → 𝑥
= 𝑦)) |
123 | 121, 122 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (2 ≠ 0
→ (2 = 0 → 𝑥 =
𝑦)) |
124 | 120, 123 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (2 = 0
→ 𝑥 = 𝑦) |
125 | 119, 124 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑦 = (𝑥 + 1)) → ((𝑦 + 1) = 𝑥 → 𝑥 = 𝑦)) |
126 | 125 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (𝑦 = (𝑥 + 1) → ((𝑦 + 1) = 𝑥 → 𝑥 = 𝑦))) |
127 | 126 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) ∧ (𝑃‘𝑦) = (𝑃‘(𝑥 + 1))) → (𝑦 = (𝑥 + 1) → ((𝑦 + 1) = 𝑥 → 𝑥 = 𝑦))) |
128 | 90, 127 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) ∧ (𝑃‘𝑦) = (𝑃‘(𝑥 + 1))) → ((𝑦 + 1) = 𝑥 → 𝑥 = 𝑦)) |
129 | 128 | expcom 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑃‘𝑦) = (𝑃‘(𝑥 + 1)) → (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → ((𝑦 + 1) = 𝑥 → 𝑥 = 𝑦))) |
130 | 129 | com13 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑦 + 1) = 𝑥 → (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → ((𝑃‘𝑦) = (𝑃‘(𝑥 + 1)) → 𝑥 = 𝑦))) |
131 | 85, 130 | syl6 34 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → ((𝑃‘(𝑦 + 1)) = (𝑃‘𝑥) → (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → ((𝑃‘𝑦) = (𝑃‘(𝑥 + 1)) → 𝑥 = 𝑦)))) |
132 | 131 | pm2.43a 52 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → ((𝑃‘(𝑦 + 1)) = (𝑃‘𝑥) → ((𝑃‘𝑦) = (𝑃‘(𝑥 + 1)) → 𝑥 = 𝑦))) |
133 | 132 | com13 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑃‘𝑦) = (𝑃‘(𝑥 + 1)) → ((𝑃‘(𝑦 + 1)) = (𝑃‘𝑥) → (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → 𝑥 = 𝑦))) |
134 | 133 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑃‘𝑦) = (𝑃‘(𝑥 + 1)) ∧ (𝑃‘(𝑦 + 1)) = (𝑃‘𝑥)) → (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → 𝑥 = 𝑦)) |
135 | 80, 134 | syl6com 36 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((¬
(𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1)) ∧ ¬ (𝑃‘𝑥) = (𝑃‘𝑦)) → ({(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} → (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → 𝑥 = 𝑦))) |
136 | 135 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((¬
(𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1)) ∧ ¬ (𝑃‘𝑥) = (𝑃‘𝑦)) → (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → ({(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} → 𝑥 = 𝑦))) |
137 | 67, 136 | syl8 74 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((¬
𝑥 = 𝑦 ∧ ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉)) → (¬ 𝑥 = 𝑦 → (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → ({(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} → 𝑥 = 𝑦))))) |
138 | 137 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
𝑥 = 𝑦 → (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → (¬ 𝑥 = 𝑦 → (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → ({(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} → 𝑥 = 𝑦)))))) |
139 | 138 | pm2.43a 52 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
𝑥 = 𝑦 → (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → ({(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} → 𝑥 = 𝑦))))) |
140 | 139 | com14 94 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → (¬ 𝑥 = 𝑦 → ({(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} → 𝑥 = 𝑦))))) |
141 | 140 | pm2.43a 52 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → (¬ 𝑥 = 𝑦 → ({(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} → 𝑥 = 𝑦)))) |
142 | 141 | pm2.43i 50 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉) → (¬ 𝑥 = 𝑦 → ({(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} → 𝑥 = 𝑦))) |
143 | 142 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (𝑃:(0...(#‘𝐹))–1-1→𝑉 → (¬ 𝑥 = 𝑦 → ({(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} → 𝑥 = 𝑦)))) |
144 | 143 | com23 84 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (¬ 𝑥 = 𝑦 → (𝑃:(0...(#‘𝐹))–1-1→𝑉 → ({(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} → 𝑥 = 𝑦)))) |
145 | 144 | com14 94 |
. . . . . . . . . . . . . . 15
⊢ ({(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} → (¬ 𝑥 = 𝑦 → (𝑃:(0...(#‘𝐹))–1-1→𝑉 → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑥 = 𝑦)))) |
146 | 36, 145 | syl6com 36 |
. . . . . . . . . . . . . 14
⊢ ((𝐸‘(𝐹‘𝑥)) = (𝐸‘(𝐹‘𝑦)) → (((𝐸‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} ∧ (𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) → (¬ 𝑥 = 𝑦 → (𝑃:(0...(#‘𝐹))–1-1→𝑉 → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑥 = 𝑦))))) |
147 | 28, 146 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑥) = (𝐹‘𝑦) → (((𝐸‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} ∧ (𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) → (¬ 𝑥 = 𝑦 → (𝑃:(0...(#‘𝐹))–1-1→𝑉 → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑥 = 𝑦))))) |
148 | 147 | com15 99 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (((𝐸‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} ∧ (𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) → (¬ 𝑥 = 𝑦 → (𝑃:(0...(#‘𝐹))–1-1→𝑉 → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))) |
149 | 148 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (((𝐸‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} ∧ (𝐸‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) → (¬ 𝑥 = 𝑦 → (𝑃:(0...(#‘𝐹))–1-1→𝑉 → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))) |
150 | 27, 149 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (¬ 𝑥 = 𝑦 → (𝑃:(0...(#‘𝐹))–1-1→𝑉 → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))) |
151 | 150 | ex 449 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (¬ 𝑥 = 𝑦 → (𝑃:(0...(#‘𝐹))–1-1→𝑉 → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))) |
152 | 151 | com14 94 |
. . . . . . . 8
⊢ (𝑃:(0...(#‘𝐹))–1-1→𝑉 → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (¬ 𝑥 = 𝑦 → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))) |
153 | 152 | a1i 11 |
. . . . . . 7
⊢ (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 → (𝑃:(0...(#‘𝐹))–1-1→𝑉 → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (¬ 𝑥 = 𝑦 → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))))) |
154 | 153 | 3imp 1249 |
. . . . . 6
⊢ ((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (¬ 𝑥 = 𝑦 → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))) |
155 | | 2a1 28 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
156 | 154, 155 | pm2.61d2 171 |
. . . . 5
⊢ ((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
157 | 156 | ralrimivv 2953 |
. . . 4
⊢ ((𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → ∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
158 | 1, 157 | syl3an1 1351 |
. . 3
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → ∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
159 | | dff13 6416 |
. . 3
⊢ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ↔ (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ ∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
160 | 2, 158, 159 | sylanbrc 695 |
. 2
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸) |
161 | 2 | biantrurd 528 |
. . 3
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (Fun ◡𝐹 ↔ (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ Fun ◡𝐹))) |
162 | | df-f1 5809 |
. . 3
⊢ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ↔ (𝐹:(0..^(#‘𝐹))⟶dom 𝐸 ∧ Fun ◡𝐹)) |
163 | 161, 162 | syl6bbr 277 |
. 2
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (Fun ◡𝐹 ↔ 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸)) |
164 | 160, 163 | mpbird 246 |
1
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → Fun ◡𝐹) |