MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  upgrwlkdvdelem Structured version   Visualization version   GIF version

Theorem upgrwlkdvdelem 26866
Description: Lemma for upgrwlkdvde 26867. (Contributed by Alexander van der Vekens, 27-Oct-2017.) (Proof shortened by AV, 17-Jan-2021.)
Assertion
Ref Expression
upgrwlkdvdelem ((𝑃:(0...(♯‘𝐹))–1-1𝑉𝐹 ∈ Word dom 𝐼) → (∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))} → Fun 𝐹))
Distinct variable groups:   𝑘,𝐹   𝑘,𝐼   𝑃,𝑘
Allowed substitution hint:   𝑉(𝑘)

Proof of Theorem upgrwlkdvdelem
Dummy variables 𝑎 𝑏 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wrdfin 13518 . . 3 (𝐹 ∈ Word dom 𝐼𝐹 ∈ Fin)
2 wrdf 13505 . . 3 (𝐹 ∈ Word dom 𝐼𝐹:(0..^(♯‘𝐹))⟶dom 𝐼)
3 simpr 471 . . . . . . . . 9 ((𝐹 ∈ Fin ∧ 𝐹:(0..^(♯‘𝐹))⟶dom 𝐼) → 𝐹:(0..^(♯‘𝐹))⟶dom 𝐼)
43adantr 466 . . . . . . . 8 (((𝐹 ∈ Fin ∧ 𝐹:(0..^(♯‘𝐹))⟶dom 𝐼) ∧ (𝑃:(0...(♯‘𝐹))–1-1𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))})) → 𝐹:(0..^(♯‘𝐹))⟶dom 𝐼)
5 fveq2 6332 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑥 → (𝐹𝑘) = (𝐹𝑥))
65fveq2d 6336 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑥 → (𝐼‘(𝐹𝑘)) = (𝐼‘(𝐹𝑥)))
7 fveq2 6332 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑥 → (𝑃𝑘) = (𝑃𝑥))
8 fvoveq1 6815 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑥 → (𝑃‘(𝑘 + 1)) = (𝑃‘(𝑥 + 1)))
97, 8preq12d 4410 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑥 → {(𝑃𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃𝑥), (𝑃‘(𝑥 + 1))})
106, 9eqeq12d 2785 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑥 → ((𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ↔ (𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))}))
1110rspcv 3454 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0..^(♯‘𝐹)) → (∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))} → (𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))}))
12 fveq2 6332 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑦 → (𝐹𝑘) = (𝐹𝑦))
1312fveq2d 6336 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑦 → (𝐼‘(𝐹𝑘)) = (𝐼‘(𝐹𝑦)))
14 fveq2 6332 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑦 → (𝑃𝑘) = (𝑃𝑦))
15 fvoveq1 6815 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑦 → (𝑃‘(𝑘 + 1)) = (𝑃‘(𝑦 + 1)))
1614, 15preq12d 4410 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑦 → {(𝑃𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃𝑦), (𝑃‘(𝑦 + 1))})
1713, 16eqeq12d 2785 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑦 → ((𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ↔ (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))}))
1817rspcv 3454 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0..^(♯‘𝐹)) → (∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))} → (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))}))
1911, 18anim12ii 596 . . . . . . . . . . . . . 14 ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))} → ((𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))})))
20 fveq2 6332 . . . . . . . . . . . . . . . 16 ((𝐹𝑥) = (𝐹𝑦) → (𝐼‘(𝐹𝑥)) = (𝐼‘(𝐹𝑦)))
21 simpl 468 . . . . . . . . . . . . . . . . . . . . 21 (((𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))}) → (𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))})
2221eqcomd 2776 . . . . . . . . . . . . . . . . . . . 20 (((𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))}) → {(𝑃𝑥), (𝑃‘(𝑥 + 1))} = (𝐼‘(𝐹𝑥)))
2322adantl 467 . . . . . . . . . . . . . . . . . . 19 (((𝐼‘(𝐹𝑥)) = (𝐼‘(𝐹𝑦)) ∧ ((𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))})) → {(𝑃𝑥), (𝑃‘(𝑥 + 1))} = (𝐼‘(𝐹𝑥)))
24 simpl 468 . . . . . . . . . . . . . . . . . . 19 (((𝐼‘(𝐹𝑥)) = (𝐼‘(𝐹𝑦)) ∧ ((𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))})) → (𝐼‘(𝐹𝑥)) = (𝐼‘(𝐹𝑦)))
25 simpr 471 . . . . . . . . . . . . . . . . . . . 20 (((𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))}) → (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))})
2625adantl 467 . . . . . . . . . . . . . . . . . . 19 (((𝐼‘(𝐹𝑥)) = (𝐼‘(𝐹𝑦)) ∧ ((𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))})) → (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))})
2723, 24, 263eqtrd 2808 . . . . . . . . . . . . . . . . . 18 (((𝐼‘(𝐹𝑥)) = (𝐼‘(𝐹𝑦)) ∧ ((𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))})) → {(𝑃𝑥), (𝑃‘(𝑥 + 1))} = {(𝑃𝑦), (𝑃‘(𝑦 + 1))})
28 fvex 6342 . . . . . . . . . . . . . . . . . . . 20 (𝑃𝑥) ∈ V
29 fvex 6342 . . . . . . . . . . . . . . . . . . . 20 (𝑃‘(𝑥 + 1)) ∈ V
30 fvex 6342 . . . . . . . . . . . . . . . . . . . 20 (𝑃𝑦) ∈ V
31 fvex 6342 . . . . . . . . . . . . . . . . . . . 20 (𝑃‘(𝑦 + 1)) ∈ V
3228, 29, 30, 31preq12b 4511 . . . . . . . . . . . . . . . . . . 19 ({(𝑃𝑥), (𝑃‘(𝑥 + 1))} = {(𝑃𝑦), (𝑃‘(𝑦 + 1))} ↔ (((𝑃𝑥) = (𝑃𝑦) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1))) ∨ ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦))))
33 dff13 6654 . . . . . . . . . . . . . . . . . . . . 21 (𝑃:(0...(♯‘𝐹))–1-1𝑉 ↔ (𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑎 ∈ (0...(♯‘𝐹))∀𝑏 ∈ (0...(♯‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏)))
34 elfzofz 12692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ (0..^(♯‘𝐹)) → 𝑥 ∈ (0...(♯‘𝐹)))
35 elfzofz 12692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ (0..^(♯‘𝐹)) → 𝑦 ∈ (0...(♯‘𝐹)))
36 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑎 = 𝑥 → (𝑃𝑎) = (𝑃𝑥))
3736eqeq1d 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 = 𝑥 → ((𝑃𝑎) = (𝑃𝑏) ↔ (𝑃𝑥) = (𝑃𝑏)))
38 eqeq1 2774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 = 𝑥 → (𝑎 = 𝑏𝑥 = 𝑏))
3937, 38imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 = 𝑥 → (((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) ↔ ((𝑃𝑥) = (𝑃𝑏) → 𝑥 = 𝑏)))
40 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑏 = 𝑦 → (𝑃𝑏) = (𝑃𝑦))
4140eqeq2d 2780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑏 = 𝑦 → ((𝑃𝑥) = (𝑃𝑏) ↔ (𝑃𝑥) = (𝑃𝑦)))
42 eqeq2 2781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑏 = 𝑦 → (𝑥 = 𝑏𝑥 = 𝑦))
4341, 42imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑏 = 𝑦 → (((𝑃𝑥) = (𝑃𝑏) → 𝑥 = 𝑏) ↔ ((𝑃𝑥) = (𝑃𝑦) → 𝑥 = 𝑦)))
4439, 43rspc2v 3470 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ (0...(♯‘𝐹)) ∧ 𝑦 ∈ (0...(♯‘𝐹))) → (∀𝑎 ∈ (0...(♯‘𝐹))∀𝑏 ∈ (0...(♯‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) → ((𝑃𝑥) = (𝑃𝑦) → 𝑥 = 𝑦)))
4534, 35, 44syl2an 575 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (∀𝑎 ∈ (0...(♯‘𝐹))∀𝑏 ∈ (0...(♯‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) → ((𝑃𝑥) = (𝑃𝑦) → 𝑥 = 𝑦)))
4645a1dd 50 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (∀𝑎 ∈ (0...(♯‘𝐹))∀𝑏 ∈ (0...(♯‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) → (𝐹 ∈ Fin → ((𝑃𝑥) = (𝑃𝑦) → 𝑥 = 𝑦))))
4746com14 96 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑃𝑥) = (𝑃𝑦) → (∀𝑎 ∈ (0...(♯‘𝐹))∀𝑏 ∈ (0...(♯‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) → (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → 𝑥 = 𝑦))))
4847adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃𝑥) = (𝑃𝑦) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1))) → (∀𝑎 ∈ (0...(♯‘𝐹))∀𝑏 ∈ (0...(♯‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) → (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → 𝑥 = 𝑦))))
49 hashcl 13348 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐹 ∈ Fin → (♯‘𝐹) ∈ ℕ0)
5034a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((♯‘𝐹) ∈ ℕ0 → (𝑥 ∈ (0..^(♯‘𝐹)) → 𝑥 ∈ (0...(♯‘𝐹))))
51 fzofzp1 12772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ (0..^(♯‘𝐹)) → (𝑦 + 1) ∈ (0...(♯‘𝐹)))
5250, 51anim12d1 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((♯‘𝐹) ∈ ℕ0 → ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (𝑥 ∈ (0...(♯‘𝐹)) ∧ (𝑦 + 1) ∈ (0...(♯‘𝐹)))))
5352imp 393 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((♯‘𝐹) ∈ ℕ0 ∧ (𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (𝑥 ∈ (0...(♯‘𝐹)) ∧ (𝑦 + 1) ∈ (0...(♯‘𝐹))))
54 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑏 = (𝑦 + 1) → (𝑃𝑏) = (𝑃‘(𝑦 + 1)))
5554eqeq2d 2780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑏 = (𝑦 + 1) → ((𝑃𝑥) = (𝑃𝑏) ↔ (𝑃𝑥) = (𝑃‘(𝑦 + 1))))
56 eqeq2 2781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑏 = (𝑦 + 1) → (𝑥 = 𝑏𝑥 = (𝑦 + 1)))
5755, 56imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑏 = (𝑦 + 1) → (((𝑃𝑥) = (𝑃𝑏) → 𝑥 = 𝑏) ↔ ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) → 𝑥 = (𝑦 + 1))))
5839, 57rspc2v 3470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑥 ∈ (0...(♯‘𝐹)) ∧ (𝑦 + 1) ∈ (0...(♯‘𝐹))) → (∀𝑎 ∈ (0...(♯‘𝐹))∀𝑏 ∈ (0...(♯‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) → ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) → 𝑥 = (𝑦 + 1))))
5953, 58syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((♯‘𝐹) ∈ ℕ0 ∧ (𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (∀𝑎 ∈ (0...(♯‘𝐹))∀𝑏 ∈ (0...(♯‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) → ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) → 𝑥 = (𝑦 + 1))))
6059imp 393 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((♯‘𝐹) ∈ ℕ0 ∧ (𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) ∧ ∀𝑎 ∈ (0...(♯‘𝐹))∀𝑏 ∈ (0...(♯‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏)) → ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) → 𝑥 = (𝑦 + 1)))
61 fzofzp1 12772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑥 ∈ (0..^(♯‘𝐹)) → (𝑥 + 1) ∈ (0...(♯‘𝐹)))
6261a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((♯‘𝐹) ∈ ℕ0 → (𝑥 ∈ (0..^(♯‘𝐹)) → (𝑥 + 1) ∈ (0...(♯‘𝐹))))
6362, 35anim12d1 589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((♯‘𝐹) ∈ ℕ0 → ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → ((𝑥 + 1) ∈ (0...(♯‘𝐹)) ∧ 𝑦 ∈ (0...(♯‘𝐹)))))
6463imp 393 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((♯‘𝐹) ∈ ℕ0 ∧ (𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → ((𝑥 + 1) ∈ (0...(♯‘𝐹)) ∧ 𝑦 ∈ (0...(♯‘𝐹))))
65 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑎 = (𝑥 + 1) → (𝑃𝑎) = (𝑃‘(𝑥 + 1)))
6665eqeq1d 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑎 = (𝑥 + 1) → ((𝑃𝑎) = (𝑃𝑏) ↔ (𝑃‘(𝑥 + 1)) = (𝑃𝑏)))
67 eqeq1 2774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑎 = (𝑥 + 1) → (𝑎 = 𝑏 ↔ (𝑥 + 1) = 𝑏))
6866, 67imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑎 = (𝑥 + 1) → (((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) ↔ ((𝑃‘(𝑥 + 1)) = (𝑃𝑏) → (𝑥 + 1) = 𝑏)))
6940eqeq2d 2780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑏 = 𝑦 → ((𝑃‘(𝑥 + 1)) = (𝑃𝑏) ↔ (𝑃‘(𝑥 + 1)) = (𝑃𝑦)))
70 eqeq2 2781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑏 = 𝑦 → ((𝑥 + 1) = 𝑏 ↔ (𝑥 + 1) = 𝑦))
7169, 70imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑏 = 𝑦 → (((𝑃‘(𝑥 + 1)) = (𝑃𝑏) → (𝑥 + 1) = 𝑏) ↔ ((𝑃‘(𝑥 + 1)) = (𝑃𝑦) → (𝑥 + 1) = 𝑦)))
7268, 71rspc2v 3470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑥 + 1) ∈ (0...(♯‘𝐹)) ∧ 𝑦 ∈ (0...(♯‘𝐹))) → (∀𝑎 ∈ (0...(♯‘𝐹))∀𝑏 ∈ (0...(♯‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) → ((𝑃‘(𝑥 + 1)) = (𝑃𝑦) → (𝑥 + 1) = 𝑦)))
7364, 72syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((♯‘𝐹) ∈ ℕ0 ∧ (𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → (∀𝑎 ∈ (0...(♯‘𝐹))∀𝑏 ∈ (0...(♯‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) → ((𝑃‘(𝑥 + 1)) = (𝑃𝑦) → (𝑥 + 1) = 𝑦)))
7473imp 393 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((♯‘𝐹) ∈ ℕ0 ∧ (𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) ∧ ∀𝑎 ∈ (0...(♯‘𝐹))∀𝑏 ∈ (0...(♯‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏)) → ((𝑃‘(𝑥 + 1)) = (𝑃𝑦) → (𝑥 + 1) = 𝑦))
7560, 74anim12d 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((♯‘𝐹) ∈ ℕ0 ∧ (𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) ∧ ∀𝑎 ∈ (0...(♯‘𝐹))∀𝑏 ∈ (0...(♯‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏)) → (((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦)) → (𝑥 = (𝑦 + 1) ∧ (𝑥 + 1) = 𝑦)))
7675expimpd 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((♯‘𝐹) ∈ ℕ0 ∧ (𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → ((∀𝑎 ∈ (0...(♯‘𝐹))∀𝑏 ∈ (0...(♯‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) ∧ ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦))) → (𝑥 = (𝑦 + 1) ∧ (𝑥 + 1) = 𝑦)))
77 oveq1 6799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 = (𝑦 + 1) → (𝑥 + 1) = ((𝑦 + 1) + 1))
7877eqeq1d 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 = (𝑦 + 1) → ((𝑥 + 1) = 𝑦 ↔ ((𝑦 + 1) + 1) = 𝑦))
7978adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑥 = (𝑦 + 1)) → ((𝑥 + 1) = 𝑦 ↔ ((𝑦 + 1) + 1) = 𝑦))
80 elfzonn0 12720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ (0..^(♯‘𝐹)) → 𝑦 ∈ ℕ0)
81 nn0cn 11503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑦 ∈ ℕ0𝑦 ∈ ℂ)
82 add1p1 11484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑦 ∈ ℂ → ((𝑦 + 1) + 1) = (𝑦 + 2))
8381, 82syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦 ∈ ℕ0 → ((𝑦 + 1) + 1) = (𝑦 + 2))
8483eqeq1d 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 ∈ ℕ0 → (((𝑦 + 1) + 1) = 𝑦 ↔ (𝑦 + 2) = 𝑦))
85 2cnd 11294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑦 ∈ ℕ0 → 2 ∈ ℂ)
86 2ne0 11314 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 2 ≠ 0
8786a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑦 ∈ ℕ0 → 2 ≠ 0)
88 addn0nid 10652 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑦 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (𝑦 + 2) ≠ 𝑦)
8981, 85, 87, 88syl3anc 1475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦 ∈ ℕ0 → (𝑦 + 2) ≠ 𝑦)
90 eqneqall 2953 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑦 + 2) = 𝑦 → ((𝑦 + 2) ≠ 𝑦𝑥 = 𝑦))
9189, 90syl5com 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 ∈ ℕ0 → ((𝑦 + 2) = 𝑦𝑥 = 𝑦))
9284, 91sylbid 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ ℕ0 → (((𝑦 + 1) + 1) = 𝑦𝑥 = 𝑦))
9380, 92syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 ∈ (0..^(♯‘𝐹)) → (((𝑦 + 1) + 1) = 𝑦𝑥 = 𝑦))
9493adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (((𝑦 + 1) + 1) = 𝑦𝑥 = 𝑦))
9594adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑥 = (𝑦 + 1)) → (((𝑦 + 1) + 1) = 𝑦𝑥 = 𝑦))
9679, 95sylbid 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑥 = (𝑦 + 1)) → ((𝑥 + 1) = 𝑦𝑥 = 𝑦))
9796expimpd 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → ((𝑥 = (𝑦 + 1) ∧ (𝑥 + 1) = 𝑦) → 𝑥 = 𝑦))
9897adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((♯‘𝐹) ∈ ℕ0 ∧ (𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → ((𝑥 = (𝑦 + 1) ∧ (𝑥 + 1) = 𝑦) → 𝑥 = 𝑦))
9976, 98syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((♯‘𝐹) ∈ ℕ0 ∧ (𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹)))) → ((∀𝑎 ∈ (0...(♯‘𝐹))∀𝑏 ∈ (0...(♯‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) ∧ ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦))) → 𝑥 = 𝑦))
10099ex 397 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((♯‘𝐹) ∈ ℕ0 → ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → ((∀𝑎 ∈ (0...(♯‘𝐹))∀𝑏 ∈ (0...(♯‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) ∧ ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦))) → 𝑥 = 𝑦)))
10149, 100syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → ((∀𝑎 ∈ (0...(♯‘𝐹))∀𝑏 ∈ (0...(♯‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) ∧ ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦))) → 𝑥 = 𝑦)))
102101com3l 89 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → ((∀𝑎 ∈ (0...(♯‘𝐹))∀𝑏 ∈ (0...(♯‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) ∧ ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦))) → (𝐹 ∈ Fin → 𝑥 = 𝑦)))
103102expd 400 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (∀𝑎 ∈ (0...(♯‘𝐹))∀𝑏 ∈ (0...(♯‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) → (((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦)) → (𝐹 ∈ Fin → 𝑥 = 𝑦))))
104103com34 91 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (∀𝑎 ∈ (0...(♯‘𝐹))∀𝑏 ∈ (0...(♯‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) → (𝐹 ∈ Fin → (((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦)) → 𝑥 = 𝑦))))
105104com14 96 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦)) → (∀𝑎 ∈ (0...(♯‘𝐹))∀𝑏 ∈ (0...(♯‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) → (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → 𝑥 = 𝑦))))
10648, 105jaoi 837 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑃𝑥) = (𝑃𝑦) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1))) ∨ ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦))) → (∀𝑎 ∈ (0...(♯‘𝐹))∀𝑏 ∈ (0...(♯‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) → (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → 𝑥 = 𝑦))))
107106adantld 474 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑃𝑥) = (𝑃𝑦) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1))) ∨ ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦))) → ((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑎 ∈ (0...(♯‘𝐹))∀𝑏 ∈ (0...(♯‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏)) → (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → 𝑥 = 𝑦))))
10833, 107syl5bi 232 . . . . . . . . . . . . . . . . . . . 20 ((((𝑃𝑥) = (𝑃𝑦) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1))) ∨ ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦))) → (𝑃:(0...(♯‘𝐹))–1-1𝑉 → (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → 𝑥 = 𝑦))))
109108com23 86 . . . . . . . . . . . . . . . . . . 19 ((((𝑃𝑥) = (𝑃𝑦) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1))) ∨ ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦))) → (𝐹 ∈ Fin → (𝑃:(0...(♯‘𝐹))–1-1𝑉 → ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → 𝑥 = 𝑦))))
11032, 109sylbi 207 . . . . . . . . . . . . . . . . . 18 ({(𝑃𝑥), (𝑃‘(𝑥 + 1))} = {(𝑃𝑦), (𝑃‘(𝑦 + 1))} → (𝐹 ∈ Fin → (𝑃:(0...(♯‘𝐹))–1-1𝑉 → ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → 𝑥 = 𝑦))))
11127, 110syl 17 . . . . . . . . . . . . . . . . 17 (((𝐼‘(𝐹𝑥)) = (𝐼‘(𝐹𝑦)) ∧ ((𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))})) → (𝐹 ∈ Fin → (𝑃:(0...(♯‘𝐹))–1-1𝑉 → ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → 𝑥 = 𝑦))))
112111ex 397 . . . . . . . . . . . . . . . 16 ((𝐼‘(𝐹𝑥)) = (𝐼‘(𝐹𝑦)) → (((𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))}) → (𝐹 ∈ Fin → (𝑃:(0...(♯‘𝐹))–1-1𝑉 → ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → 𝑥 = 𝑦)))))
11320, 112syl 17 . . . . . . . . . . . . . . 15 ((𝐹𝑥) = (𝐹𝑦) → (((𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))}) → (𝐹 ∈ Fin → (𝑃:(0...(♯‘𝐹))–1-1𝑉 → ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → 𝑥 = 𝑦)))))
114113com15 101 . . . . . . . . . . . . . 14 ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (((𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))}) → (𝐹 ∈ Fin → (𝑃:(0...(♯‘𝐹))–1-1𝑉 → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))))
11519, 114syld 47 . . . . . . . . . . . . 13 ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))} → (𝐹 ∈ Fin → (𝑃:(0...(♯‘𝐹))–1-1𝑉 → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))))
116115com14 96 . . . . . . . . . . . 12 (𝑃:(0...(♯‘𝐹))–1-1𝑉 → (∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))} → (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))))
117116imp 393 . . . . . . . . . . 11 ((𝑃:(0...(♯‘𝐹))–1-1𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))}) → (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))))
118117impcom 394 . . . . . . . . . 10 ((𝐹 ∈ Fin ∧ (𝑃:(0...(♯‘𝐹))–1-1𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))})) → ((𝑥 ∈ (0..^(♯‘𝐹)) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
119118ralrimivv 3118 . . . . . . . . 9 ((𝐹 ∈ Fin ∧ (𝑃:(0...(♯‘𝐹))–1-1𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))})) → ∀𝑥 ∈ (0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
120119adantlr 686 . . . . . . . 8 (((𝐹 ∈ Fin ∧ 𝐹:(0..^(♯‘𝐹))⟶dom 𝐼) ∧ (𝑃:(0...(♯‘𝐹))–1-1𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))})) → ∀𝑥 ∈ (0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
121 dff13 6654 . . . . . . . 8 (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼 ↔ (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 ∧ ∀𝑥 ∈ (0..^(♯‘𝐹))∀𝑦 ∈ (0..^(♯‘𝐹))((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
1224, 120, 121sylanbrc 564 . . . . . . 7 (((𝐹 ∈ Fin ∧ 𝐹:(0..^(♯‘𝐹))⟶dom 𝐼) ∧ (𝑃:(0...(♯‘𝐹))–1-1𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))})) → 𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼)
123 df-f1 6036 . . . . . . 7 (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼 ↔ (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 ∧ Fun 𝐹))
124122, 123sylib 208 . . . . . 6 (((𝐹 ∈ Fin ∧ 𝐹:(0..^(♯‘𝐹))⟶dom 𝐼) ∧ (𝑃:(0...(♯‘𝐹))–1-1𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))})) → (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 ∧ Fun 𝐹))
125 simpr 471 . . . . . 6 ((𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 ∧ Fun 𝐹) → Fun 𝐹)
126124, 125syl 17 . . . . 5 (((𝐹 ∈ Fin ∧ 𝐹:(0..^(♯‘𝐹))⟶dom 𝐼) ∧ (𝑃:(0...(♯‘𝐹))–1-1𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))})) → Fun 𝐹)
127126ex 397 . . . 4 ((𝐹 ∈ Fin ∧ 𝐹:(0..^(♯‘𝐹))⟶dom 𝐼) → ((𝑃:(0...(♯‘𝐹))–1-1𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))}) → Fun 𝐹))
128127expd 400 . . 3 ((𝐹 ∈ Fin ∧ 𝐹:(0..^(♯‘𝐹))⟶dom 𝐼) → (𝑃:(0...(♯‘𝐹))–1-1𝑉 → (∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))} → Fun 𝐹)))
1291, 2, 128syl2anc 565 . 2 (𝐹 ∈ Word dom 𝐼 → (𝑃:(0...(♯‘𝐹))–1-1𝑉 → (∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))} → Fun 𝐹)))
130129impcom 394 1 ((𝑃:(0...(♯‘𝐹))–1-1𝑉𝐹 ∈ Word dom 𝐼) → (∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))} → Fun 𝐹))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  wo 826   = wceq 1630  wcel 2144  wne 2942  wral 3060  {cpr 4316  ccnv 5248  dom cdm 5249  Fun wfun 6025  wf 6027  1-1wf1 6028  cfv 6031  (class class class)co 6792  Fincfn 8108  cc 10135  0cc0 10137  1c1 10138   + caddc 10140  2c2 11271  0cn0 11493  ...cfz 12532  ..^cfzo 12672  chash 13320  Word cword 13486
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-rep 4902  ax-sep 4912  ax-nul 4920  ax-pow 4971  ax-pr 5034  ax-un 7095  ax-cnex 10193  ax-resscn 10194  ax-1cn 10195  ax-icn 10196  ax-addcl 10197  ax-addrcl 10198  ax-mulcl 10199  ax-mulrcl 10200  ax-mulcom 10201  ax-addass 10202  ax-mulass 10203  ax-distr 10204  ax-i2m1 10205  ax-1ne0 10206  ax-1rid 10207  ax-rnegex 10208  ax-rrecex 10209  ax-cnre 10210  ax-pre-lttri 10211  ax-pre-lttrn 10212  ax-pre-ltadd 10213  ax-pre-mulgt0 10214
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1071  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-nel 3046  df-ral 3065  df-rex 3066  df-reu 3067  df-rab 3069  df-v 3351  df-sbc 3586  df-csb 3681  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-pss 3737  df-nul 4062  df-if 4224  df-pw 4297  df-sn 4315  df-pr 4317  df-tp 4319  df-op 4321  df-uni 4573  df-int 4610  df-iun 4654  df-br 4785  df-opab 4845  df-mpt 4862  df-tr 4885  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6753  df-ov 6795  df-oprab 6796  df-mpt2 6797  df-om 7212  df-1st 7314  df-2nd 7315  df-wrecs 7558  df-recs 7620  df-rdg 7658  df-1o 7712  df-oadd 7716  df-er 7895  df-en 8109  df-dom 8110  df-sdom 8111  df-fin 8112  df-card 8964  df-pnf 10277  df-mnf 10278  df-xr 10279  df-ltxr 10280  df-le 10281  df-sub 10469  df-neg 10470  df-nn 11222  df-2 11280  df-n0 11494  df-z 11579  df-uz 11888  df-fz 12533  df-fzo 12673  df-hash 13321  df-word 13494
This theorem is referenced by:  upgrwlkdvde  26867
  Copyright terms: Public domain W3C validator