Step | Hyp | Ref
| Expression |
1 | | wrdfin 13178 |
. . 3
⊢ (𝐹 ∈ Word dom 𝐼 → 𝐹 ∈ Fin) |
2 | | wrdf 13165 |
. . 3
⊢ (𝐹 ∈ Word dom 𝐼 → 𝐹:(0..^(#‘𝐹))⟶dom 𝐼) |
3 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Fin ∧ 𝐹:(0..^(#‘𝐹))⟶dom 𝐼) → 𝐹:(0..^(#‘𝐹))⟶dom 𝐼) |
4 | 3 | adantr 480 |
. . . . . . . 8
⊢ (((𝐹 ∈ Fin ∧ 𝐹:(0..^(#‘𝐹))⟶dom 𝐼) ∧ (𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) → 𝐹:(0..^(#‘𝐹))⟶dom 𝐼) |
5 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑥 → (𝐹‘𝑘) = (𝐹‘𝑥)) |
6 | 5 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑥 → (𝐼‘(𝐹‘𝑘)) = (𝐼‘(𝐹‘𝑥))) |
7 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑥 → (𝑃‘𝑘) = (𝑃‘𝑥)) |
8 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑥 → (𝑘 + 1) = (𝑥 + 1)) |
9 | 8 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑥 → (𝑃‘(𝑘 + 1)) = (𝑃‘(𝑥 + 1))) |
10 | 7, 9 | preq12d 4220 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑥 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) |
11 | 6, 10 | eqeq12d 2625 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑥 → ((𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ (𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) |
12 | 11 | rspcv 3278 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (0..^(#‘𝐹)) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) |
13 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑦 → (𝐹‘𝑘) = (𝐹‘𝑦)) |
14 | 13 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑦 → (𝐼‘(𝐹‘𝑘)) = (𝐼‘(𝐹‘𝑦))) |
15 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑦 → (𝑃‘𝑘) = (𝑃‘𝑦)) |
16 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑦 → (𝑘 + 1) = (𝑦 + 1)) |
17 | 16 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑦 → (𝑃‘(𝑘 + 1)) = (𝑃‘(𝑦 + 1))) |
18 | 15, 17 | preq12d 4220 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑦 → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))}) |
19 | 14, 18 | eqeq12d 2625 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑦 → ((𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ (𝐼‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))})) |
20 | 19 | rspcv 3278 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (0..^(#‘𝐹)) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝐼‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))})) |
21 | 12, 20 | anim12ii 592 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → ((𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))}))) |
22 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑥) = (𝐹‘𝑦) → (𝐼‘(𝐹‘𝑥)) = (𝐼‘(𝐹‘𝑦))) |
23 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))}) → (𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) |
24 | 23 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))}) → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} = (𝐼‘(𝐹‘𝑥))) |
25 | 24 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼‘(𝐹‘𝑥)) = (𝐼‘(𝐹‘𝑦)) ∧ ((𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))})) → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} = (𝐼‘(𝐹‘𝑥))) |
26 | | simpl 472 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼‘(𝐹‘𝑥)) = (𝐼‘(𝐹‘𝑦)) ∧ ((𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))})) → (𝐼‘(𝐹‘𝑥)) = (𝐼‘(𝐹‘𝑦))) |
27 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))}) → (𝐼‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))}) |
28 | 27 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼‘(𝐹‘𝑥)) = (𝐼‘(𝐹‘𝑦)) ∧ ((𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))})) → (𝐼‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))}) |
29 | 25, 26, 28 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐼‘(𝐹‘𝑥)) = (𝐼‘(𝐹‘𝑦)) ∧ ((𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))})) → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))}) |
30 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃‘𝑥) ∈ V |
31 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃‘(𝑥 + 1)) ∈ V |
32 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃‘𝑦) ∈ V |
33 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃‘(𝑦 + 1)) ∈ V |
34 | 30, 31, 32, 33 | preq12b 4322 |
. . . . . . . . . . . . . . . . . . 19
⊢ ({(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} ↔ (((𝑃‘𝑥) = (𝑃‘𝑦) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1))) ∨ ((𝑃‘𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘𝑦)))) |
35 | | dff13 6416 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃:(0...(#‘𝐹))–1-1→𝑉 ↔ (𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃‘𝑎) = (𝑃‘𝑏) → 𝑎 = 𝑏))) |
36 | | elfzofz 12354 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 ∈ (0..^(#‘𝐹)) → 𝑥 ∈ (0...(#‘𝐹))) |
37 | | elfzofz 12354 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ (0..^(#‘𝐹)) → 𝑦 ∈ (0...(#‘𝐹))) |
38 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑎 = 𝑥 → (𝑃‘𝑎) = (𝑃‘𝑥)) |
39 | 38 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑎 = 𝑥 → ((𝑃‘𝑎) = (𝑃‘𝑏) ↔ (𝑃‘𝑥) = (𝑃‘𝑏))) |
40 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑎 = 𝑥 → (𝑎 = 𝑏 ↔ 𝑥 = 𝑏)) |
41 | 39, 40 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑎 = 𝑥 → (((𝑃‘𝑎) = (𝑃‘𝑏) → 𝑎 = 𝑏) ↔ ((𝑃‘𝑥) = (𝑃‘𝑏) → 𝑥 = 𝑏))) |
42 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑏 = 𝑦 → (𝑃‘𝑏) = (𝑃‘𝑦)) |
43 | 42 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑏 = 𝑦 → ((𝑃‘𝑥) = (𝑃‘𝑏) ↔ (𝑃‘𝑥) = (𝑃‘𝑦))) |
44 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑏 = 𝑦 → (𝑥 = 𝑏 ↔ 𝑥 = 𝑦)) |
45 | 43, 44 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑏 = 𝑦 → (((𝑃‘𝑥) = (𝑃‘𝑏) → 𝑥 = 𝑏) ↔ ((𝑃‘𝑥) = (𝑃‘𝑦) → 𝑥 = 𝑦))) |
46 | 41, 45 | rspc2v 3293 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ (0...(#‘𝐹)) ∧ 𝑦 ∈ (0...(#‘𝐹))) → (∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃‘𝑎) = (𝑃‘𝑏) → 𝑎 = 𝑏) → ((𝑃‘𝑥) = (𝑃‘𝑦) → 𝑥 = 𝑦))) |
47 | 36, 37, 46 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃‘𝑎) = (𝑃‘𝑏) → 𝑎 = 𝑏) → ((𝑃‘𝑥) = (𝑃‘𝑦) → 𝑥 = 𝑦))) |
48 | 47 | a1dd 48 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃‘𝑎) = (𝑃‘𝑏) → 𝑎 = 𝑏) → (𝐹 ∈ Fin → ((𝑃‘𝑥) = (𝑃‘𝑦) → 𝑥 = 𝑦)))) |
49 | 48 | com14 94 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑃‘𝑥) = (𝑃‘𝑦) → (∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃‘𝑎) = (𝑃‘𝑏) → 𝑎 = 𝑏) → (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑥 = 𝑦)))) |
50 | 49 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃‘𝑥) = (𝑃‘𝑦) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1))) → (∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃‘𝑎) = (𝑃‘𝑏) → 𝑎 = 𝑏) → (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑥 = 𝑦)))) |
51 | | hashcl 13009 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐹 ∈ Fin →
(#‘𝐹) ∈
ℕ0) |
52 | 36 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((#‘𝐹) ∈
ℕ0 → (𝑥 ∈ (0..^(#‘𝐹)) → 𝑥 ∈ (0...(#‘𝐹)))) |
53 | | fzofzp1 12431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑦 ∈ (0..^(#‘𝐹)) → (𝑦 + 1) ∈ (0...(#‘𝐹))) |
54 | 52, 53 | anim12d1 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((#‘𝐹) ∈
ℕ0 → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (𝑥 ∈ (0...(#‘𝐹)) ∧ (𝑦 + 1) ∈ (0...(#‘𝐹))))) |
55 | 54 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → (𝑥 ∈ (0...(#‘𝐹)) ∧ (𝑦 + 1) ∈ (0...(#‘𝐹)))) |
56 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑏 = (𝑦 + 1) → (𝑃‘𝑏) = (𝑃‘(𝑦 + 1))) |
57 | 56 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑏 = (𝑦 + 1) → ((𝑃‘𝑥) = (𝑃‘𝑏) ↔ (𝑃‘𝑥) = (𝑃‘(𝑦 + 1)))) |
58 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑏 = (𝑦 + 1) → (𝑥 = 𝑏 ↔ 𝑥 = (𝑦 + 1))) |
59 | 57, 58 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑏 = (𝑦 + 1) → (((𝑃‘𝑥) = (𝑃‘𝑏) → 𝑥 = 𝑏) ↔ ((𝑃‘𝑥) = (𝑃‘(𝑦 + 1)) → 𝑥 = (𝑦 + 1)))) |
60 | 41, 59 | rspc2v 3293 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑥 ∈ (0...(#‘𝐹)) ∧ (𝑦 + 1) ∈ (0...(#‘𝐹))) → (∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃‘𝑎) = (𝑃‘𝑏) → 𝑎 = 𝑏) → ((𝑃‘𝑥) = (𝑃‘(𝑦 + 1)) → 𝑥 = (𝑦 + 1)))) |
61 | 55, 60 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → (∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃‘𝑎) = (𝑃‘𝑏) → 𝑎 = 𝑏) → ((𝑃‘𝑥) = (𝑃‘(𝑦 + 1)) → 𝑥 = (𝑦 + 1)))) |
62 | 61 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((#‘𝐹)
∈ ℕ0 ∧ (𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) ∧ ∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃‘𝑎) = (𝑃‘𝑏) → 𝑎 = 𝑏)) → ((𝑃‘𝑥) = (𝑃‘(𝑦 + 1)) → 𝑥 = (𝑦 + 1))) |
63 | | fzofzp1 12431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑥 ∈ (0..^(#‘𝐹)) → (𝑥 + 1) ∈ (0...(#‘𝐹))) |
64 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((#‘𝐹) ∈
ℕ0 → (𝑥 ∈ (0..^(#‘𝐹)) → (𝑥 + 1) ∈ (0...(#‘𝐹)))) |
65 | 64, 37 | anim12d1 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((#‘𝐹) ∈
ℕ0 → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ((𝑥 + 1) ∈ (0...(#‘𝐹)) ∧ 𝑦 ∈ (0...(#‘𝐹))))) |
66 | 65 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → ((𝑥 + 1) ∈ (0...(#‘𝐹)) ∧ 𝑦 ∈ (0...(#‘𝐹)))) |
67 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑎 = (𝑥 + 1) → (𝑃‘𝑎) = (𝑃‘(𝑥 + 1))) |
68 | 67 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑎 = (𝑥 + 1) → ((𝑃‘𝑎) = (𝑃‘𝑏) ↔ (𝑃‘(𝑥 + 1)) = (𝑃‘𝑏))) |
69 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑎 = (𝑥 + 1) → (𝑎 = 𝑏 ↔ (𝑥 + 1) = 𝑏)) |
70 | 68, 69 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑎 = (𝑥 + 1) → (((𝑃‘𝑎) = (𝑃‘𝑏) → 𝑎 = 𝑏) ↔ ((𝑃‘(𝑥 + 1)) = (𝑃‘𝑏) → (𝑥 + 1) = 𝑏))) |
71 | 42 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑏 = 𝑦 → ((𝑃‘(𝑥 + 1)) = (𝑃‘𝑏) ↔ (𝑃‘(𝑥 + 1)) = (𝑃‘𝑦))) |
72 | | eqeq2 2621 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑏 = 𝑦 → ((𝑥 + 1) = 𝑏 ↔ (𝑥 + 1) = 𝑦)) |
73 | 71, 72 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑏 = 𝑦 → (((𝑃‘(𝑥 + 1)) = (𝑃‘𝑏) → (𝑥 + 1) = 𝑏) ↔ ((𝑃‘(𝑥 + 1)) = (𝑃‘𝑦) → (𝑥 + 1) = 𝑦))) |
74 | 70, 73 | rspc2v 3293 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑥 + 1) ∈ (0...(#‘𝐹)) ∧ 𝑦 ∈ (0...(#‘𝐹))) → (∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃‘𝑎) = (𝑃‘𝑏) → 𝑎 = 𝑏) → ((𝑃‘(𝑥 + 1)) = (𝑃‘𝑦) → (𝑥 + 1) = 𝑦))) |
75 | 66, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → (∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃‘𝑎) = (𝑃‘𝑏) → 𝑎 = 𝑏) → ((𝑃‘(𝑥 + 1)) = (𝑃‘𝑦) → (𝑥 + 1) = 𝑦))) |
76 | 75 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((#‘𝐹)
∈ ℕ0 ∧ (𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) ∧ ∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃‘𝑎) = (𝑃‘𝑏) → 𝑎 = 𝑏)) → ((𝑃‘(𝑥 + 1)) = (𝑃‘𝑦) → (𝑥 + 1) = 𝑦)) |
77 | 62, 76 | anim12d 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((#‘𝐹)
∈ ℕ0 ∧ (𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) ∧ ∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃‘𝑎) = (𝑃‘𝑏) → 𝑎 = 𝑏)) → (((𝑃‘𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘𝑦)) → (𝑥 = (𝑦 + 1) ∧ (𝑥 + 1) = 𝑦))) |
78 | 77 | expimpd 627 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → ((∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃‘𝑎) = (𝑃‘𝑏) → 𝑎 = 𝑏) ∧ ((𝑃‘𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘𝑦))) → (𝑥 = (𝑦 + 1) ∧ (𝑥 + 1) = 𝑦))) |
79 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑥 = (𝑦 + 1) → (𝑥 + 1) = ((𝑦 + 1) + 1)) |
80 | 79 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑥 = (𝑦 + 1) → ((𝑥 + 1) = 𝑦 ↔ ((𝑦 + 1) + 1) = 𝑦)) |
81 | 80 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑥 = (𝑦 + 1)) → ((𝑥 + 1) = 𝑦 ↔ ((𝑦 + 1) + 1) = 𝑦)) |
82 | | elfzonn0 12380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑦 ∈ (0..^(#‘𝐹)) → 𝑦 ∈ ℕ0) |
83 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℂ) |
84 | | add1p1 11160 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑦 ∈ ℂ → ((𝑦 + 1) + 1) = (𝑦 + 2)) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑦 ∈ ℕ0
→ ((𝑦 + 1) + 1) =
(𝑦 + 2)) |
86 | 85 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑦 ∈ ℕ0
→ (((𝑦 + 1) + 1) =
𝑦 ↔ (𝑦 + 2) = 𝑦)) |
87 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑦 ∈ ℕ0
→ 2 ∈ ℂ) |
88 | | 2ne0 10990 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ 2 ≠
0 |
89 | 88 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑦 ∈ ℕ0
→ 2 ≠ 0) |
90 | | addn0nid 10330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑦 ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 ≠ 0) → (𝑦 + 2) ≠ 𝑦) |
91 | 83, 87, 89, 90 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑦 ∈ ℕ0
→ (𝑦 + 2) ≠ 𝑦) |
92 | | eqneqall 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑦 + 2) = 𝑦 → ((𝑦 + 2) ≠ 𝑦 → 𝑥 = 𝑦)) |
93 | 91, 92 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑦 ∈ ℕ0
→ ((𝑦 + 2) = 𝑦 → 𝑥 = 𝑦)) |
94 | 86, 93 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑦 ∈ ℕ0
→ (((𝑦 + 1) + 1) =
𝑦 → 𝑥 = 𝑦)) |
95 | 82, 94 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑦 ∈ (0..^(#‘𝐹)) → (((𝑦 + 1) + 1) = 𝑦 → 𝑥 = 𝑦)) |
96 | 95 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (((𝑦 + 1) + 1) = 𝑦 → 𝑥 = 𝑦)) |
97 | 96 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑥 = (𝑦 + 1)) → (((𝑦 + 1) + 1) = 𝑦 → 𝑥 = 𝑦)) |
98 | 81, 97 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑥 = (𝑦 + 1)) → ((𝑥 + 1) = 𝑦 → 𝑥 = 𝑦)) |
99 | 98 | expimpd 627 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ((𝑥 = (𝑦 + 1) ∧ (𝑥 + 1) = 𝑦) → 𝑥 = 𝑦)) |
100 | 99 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → ((𝑥 = (𝑦 + 1) ∧ (𝑥 + 1) = 𝑦) → 𝑥 = 𝑦)) |
101 | 78, 100 | syld 46 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → ((∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃‘𝑎) = (𝑃‘𝑏) → 𝑎 = 𝑏) ∧ ((𝑃‘𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘𝑦))) → 𝑥 = 𝑦)) |
102 | 101 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((#‘𝐹) ∈
ℕ0 → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ((∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃‘𝑎) = (𝑃‘𝑏) → 𝑎 = 𝑏) ∧ ((𝑃‘𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘𝑦))) → 𝑥 = 𝑦))) |
103 | 51, 102 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ((∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃‘𝑎) = (𝑃‘𝑏) → 𝑎 = 𝑏) ∧ ((𝑃‘𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘𝑦))) → 𝑥 = 𝑦))) |
104 | 103 | com3l 87 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ((∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃‘𝑎) = (𝑃‘𝑏) → 𝑎 = 𝑏) ∧ ((𝑃‘𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘𝑦))) → (𝐹 ∈ Fin → 𝑥 = 𝑦))) |
105 | 104 | expd 451 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃‘𝑎) = (𝑃‘𝑏) → 𝑎 = 𝑏) → (((𝑃‘𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘𝑦)) → (𝐹 ∈ Fin → 𝑥 = 𝑦)))) |
106 | 105 | com34 89 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃‘𝑎) = (𝑃‘𝑏) → 𝑎 = 𝑏) → (𝐹 ∈ Fin → (((𝑃‘𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘𝑦)) → 𝑥 = 𝑦)))) |
107 | 106 | com14 94 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃‘𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘𝑦)) → (∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃‘𝑎) = (𝑃‘𝑏) → 𝑎 = 𝑏) → (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑥 = 𝑦)))) |
108 | 50, 107 | jaoi 393 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑃‘𝑥) = (𝑃‘𝑦) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1))) ∨ ((𝑃‘𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘𝑦))) → (∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃‘𝑎) = (𝑃‘𝑏) → 𝑎 = 𝑏) → (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑥 = 𝑦)))) |
109 | 108 | adantld 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑃‘𝑥) = (𝑃‘𝑦) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1))) ∨ ((𝑃‘𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘𝑦))) → ((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃‘𝑎) = (𝑃‘𝑏) → 𝑎 = 𝑏)) → (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑥 = 𝑦)))) |
110 | 35, 109 | syl5bi 231 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑃‘𝑥) = (𝑃‘𝑦) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1))) ∨ ((𝑃‘𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘𝑦))) → (𝑃:(0...(#‘𝐹))–1-1→𝑉 → (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑥 = 𝑦)))) |
111 | 110 | com23 84 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑃‘𝑥) = (𝑃‘𝑦) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1))) ∨ ((𝑃‘𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘𝑦))) → (𝐹 ∈ Fin → (𝑃:(0...(#‘𝐹))–1-1→𝑉 → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑥 = 𝑦)))) |
112 | 34, 111 | sylbi 206 |
. . . . . . . . . . . . . . . . . 18
⊢ ({(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))} → (𝐹 ∈ Fin → (𝑃:(0...(#‘𝐹))–1-1→𝑉 → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑥 = 𝑦)))) |
113 | 29, 112 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐼‘(𝐹‘𝑥)) = (𝐼‘(𝐹‘𝑦)) ∧ ((𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))})) → (𝐹 ∈ Fin → (𝑃:(0...(#‘𝐹))–1-1→𝑉 → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑥 = 𝑦)))) |
114 | 113 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼‘(𝐹‘𝑥)) = (𝐼‘(𝐹‘𝑦)) → (((𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))}) → (𝐹 ∈ Fin → (𝑃:(0...(#‘𝐹))–1-1→𝑉 → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑥 = 𝑦))))) |
115 | 22, 114 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑥) = (𝐹‘𝑦) → (((𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))}) → (𝐹 ∈ Fin → (𝑃:(0...(#‘𝐹))–1-1→𝑉 → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑥 = 𝑦))))) |
116 | 115 | com15 99 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (((𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹‘𝑦)) = {(𝑃‘𝑦), (𝑃‘(𝑦 + 1))}) → (𝐹 ∈ Fin → (𝑃:(0...(#‘𝐹))–1-1→𝑉 → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))) |
117 | 21, 116 | syld 46 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝐹 ∈ Fin → (𝑃:(0...(#‘𝐹))–1-1→𝑉 → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))) |
118 | 117 | com14 94 |
. . . . . . . . . . . 12
⊢ (𝑃:(0...(#‘𝐹))–1-1→𝑉 → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))))) |
119 | 118 | imp 444 |
. . . . . . . . . . 11
⊢ ((𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))) |
120 | 119 | impcom 445 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ Fin ∧ (𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
121 | 120 | ralrimivv 2953 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Fin ∧ (𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) → ∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
122 | 121 | adantlr 747 |
. . . . . . . 8
⊢ (((𝐹 ∈ Fin ∧ 𝐹:(0..^(#‘𝐹))⟶dom 𝐼) ∧ (𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) → ∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
123 | | dff13 6416 |
. . . . . . . 8
⊢ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼 ↔ (𝐹:(0..^(#‘𝐹))⟶dom 𝐼 ∧ ∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
124 | 4, 122, 123 | sylanbrc 695 |
. . . . . . 7
⊢ (((𝐹 ∈ Fin ∧ 𝐹:(0..^(#‘𝐹))⟶dom 𝐼) ∧ (𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) → 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼) |
125 | | df-f1 5809 |
. . . . . . 7
⊢ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼 ↔ (𝐹:(0..^(#‘𝐹))⟶dom 𝐼 ∧ Fun ◡𝐹)) |
126 | 124, 125 | sylib 207 |
. . . . . 6
⊢ (((𝐹 ∈ Fin ∧ 𝐹:(0..^(#‘𝐹))⟶dom 𝐼) ∧ (𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) → (𝐹:(0..^(#‘𝐹))⟶dom 𝐼 ∧ Fun ◡𝐹)) |
127 | | simpr 476 |
. . . . . 6
⊢ ((𝐹:(0..^(#‘𝐹))⟶dom 𝐼 ∧ Fun ◡𝐹) → Fun ◡𝐹) |
128 | 126, 127 | syl 17 |
. . . . 5
⊢ (((𝐹 ∈ Fin ∧ 𝐹:(0..^(#‘𝐹))⟶dom 𝐼) ∧ (𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) → Fun ◡𝐹) |
129 | 128 | ex 449 |
. . . 4
⊢ ((𝐹 ∈ Fin ∧ 𝐹:(0..^(#‘𝐹))⟶dom 𝐼) → ((𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) → Fun ◡𝐹)) |
130 | 129 | expd 451 |
. . 3
⊢ ((𝐹 ∈ Fin ∧ 𝐹:(0..^(#‘𝐹))⟶dom 𝐼) → (𝑃:(0...(#‘𝐹))–1-1→𝑉 → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → Fun ◡𝐹))) |
131 | 1, 2, 130 | syl2anc 691 |
. 2
⊢ (𝐹 ∈ Word dom 𝐼 → (𝑃:(0...(#‘𝐹))–1-1→𝑉 → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → Fun ◡𝐹))) |
132 | 131 | impcom 445 |
1
⊢ ((𝑃:(0...(#‘𝐹))–1-1→𝑉 ∧ 𝐹 ∈ Word dom 𝐼) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → Fun ◡𝐹)) |