Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  upgrwlkdvdelem Structured version   Visualization version   GIF version

Theorem upgrwlkdvdelem 40942
 Description: Lemma for upgrwlkdvde 40943. Formerly wlkdvspthlem 26137. (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 13178 . . 3 (𝐹 ∈ Word dom 𝐼𝐹 ∈ Fin)
2 wrdf 13165 . . 3 (𝐹 ∈ Word dom 𝐼𝐹:(0..^(#‘𝐹))⟶dom 𝐼)
3 simpr 476 . . . . . . . . 9 ((𝐹 ∈ Fin ∧ 𝐹:(0..^(#‘𝐹))⟶dom 𝐼) → 𝐹:(0..^(#‘𝐹))⟶dom 𝐼)
43adantr 480 . . . . . . . 8 (((𝐹 ∈ Fin ∧ 𝐹:(0..^(#‘𝐹))⟶dom 𝐼) ∧ (𝑃:(0...(#‘𝐹))–1-1𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))})) → 𝐹:(0..^(#‘𝐹))⟶dom 𝐼)
5 fveq2 6103 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑥 → (𝐹𝑘) = (𝐹𝑥))
65fveq2d 6107 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑥 → (𝐼‘(𝐹𝑘)) = (𝐼‘(𝐹𝑥)))
7 fveq2 6103 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑥 → (𝑃𝑘) = (𝑃𝑥))
8 oveq1 6556 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑥 → (𝑘 + 1) = (𝑥 + 1))
98fveq2d 6107 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑥 → (𝑃‘(𝑘 + 1)) = (𝑃‘(𝑥 + 1)))
107, 9preq12d 4220 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑥 → {(𝑃𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃𝑥), (𝑃‘(𝑥 + 1))})
116, 10eqeq12d 2625 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑥 → ((𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ↔ (𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))}))
1211rspcv 3278 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0..^(#‘𝐹)) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))} → (𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))}))
13 fveq2 6103 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑦 → (𝐹𝑘) = (𝐹𝑦))
1413fveq2d 6107 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑦 → (𝐼‘(𝐹𝑘)) = (𝐼‘(𝐹𝑦)))
15 fveq2 6103 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑦 → (𝑃𝑘) = (𝑃𝑦))
16 oveq1 6556 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑦 → (𝑘 + 1) = (𝑦 + 1))
1716fveq2d 6107 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑦 → (𝑃‘(𝑘 + 1)) = (𝑃‘(𝑦 + 1)))
1815, 17preq12d 4220 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑦 → {(𝑃𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃𝑦), (𝑃‘(𝑦 + 1))})
1914, 18eqeq12d 2625 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑦 → ((𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ↔ (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))}))
2019rspcv 3278 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0..^(#‘𝐹)) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))} → (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))}))
2112, 20anim12ii 592 . . . . . . . . . . . . . 14 ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))} → ((𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))})))
22 fveq2 6103 . . . . . . . . . . . . . . . 16 ((𝐹𝑥) = (𝐹𝑦) → (𝐼‘(𝐹𝑥)) = (𝐼‘(𝐹𝑦)))
23 simpl 472 . . . . . . . . . . . . . . . . . . . . 21 (((𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))}) → (𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))})
2423eqcomd 2616 . . . . . . . . . . . . . . . . . . . 20 (((𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))}) → {(𝑃𝑥), (𝑃‘(𝑥 + 1))} = (𝐼‘(𝐹𝑥)))
2524adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝐼‘(𝐹𝑥)) = (𝐼‘(𝐹𝑦)) ∧ ((𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))})) → {(𝑃𝑥), (𝑃‘(𝑥 + 1))} = (𝐼‘(𝐹𝑥)))
26 simpl 472 . . . . . . . . . . . . . . . . . . 19 (((𝐼‘(𝐹𝑥)) = (𝐼‘(𝐹𝑦)) ∧ ((𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))})) → (𝐼‘(𝐹𝑥)) = (𝐼‘(𝐹𝑦)))
27 simpr 476 . . . . . . . . . . . . . . . . . . . 20 (((𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))}) → (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))})
2827adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝐼‘(𝐹𝑥)) = (𝐼‘(𝐹𝑦)) ∧ ((𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))})) → (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))})
2925, 26, 283eqtrd 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
3430, 31, 32, 33preq12b 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 (𝑎 = 𝑥 → (𝑃𝑎) = (𝑃𝑥))
3938eqeq1d 2612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 = 𝑥 → ((𝑃𝑎) = (𝑃𝑏) ↔ (𝑃𝑥) = (𝑃𝑏)))
40 eqeq1 2614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑎 = 𝑥 → (𝑎 = 𝑏𝑥 = 𝑏))
4139, 40imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 = 𝑥 → (((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) ↔ ((𝑃𝑥) = (𝑃𝑏) → 𝑥 = 𝑏)))
42 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑏 = 𝑦 → (𝑃𝑏) = (𝑃𝑦))
4342eqeq2d 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑏 = 𝑦 → ((𝑃𝑥) = (𝑃𝑏) ↔ (𝑃𝑥) = (𝑃𝑦)))
44 eqeq2 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑏 = 𝑦 → (𝑥 = 𝑏𝑥 = 𝑦))
4543, 44imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑏 = 𝑦 → (((𝑃𝑥) = (𝑃𝑏) → 𝑥 = 𝑏) ↔ ((𝑃𝑥) = (𝑃𝑦) → 𝑥 = 𝑦)))
4641, 45rspc2v 3293 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ (0...(#‘𝐹)) ∧ 𝑦 ∈ (0...(#‘𝐹))) → (∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) → ((𝑃𝑥) = (𝑃𝑦) → 𝑥 = 𝑦)))
4736, 37, 46syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) → ((𝑃𝑥) = (𝑃𝑦) → 𝑥 = 𝑦)))
4847a1dd 48 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) → (𝐹 ∈ Fin → ((𝑃𝑥) = (𝑃𝑦) → 𝑥 = 𝑦))))
4948com14 94 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑃𝑥) = (𝑃𝑦) → (∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) → (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑥 = 𝑦))))
5049adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃𝑥) = (𝑃𝑦) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1))) → (∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) → (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑥 = 𝑦))))
51 hashcl 13009 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐹 ∈ Fin → (#‘𝐹) ∈ ℕ0)
5236a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((#‘𝐹) ∈ ℕ0 → (𝑥 ∈ (0..^(#‘𝐹)) → 𝑥 ∈ (0...(#‘𝐹))))
53 fzofzp1 12431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ (0..^(#‘𝐹)) → (𝑦 + 1) ∈ (0...(#‘𝐹)))
5452, 53anim12d1 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((#‘𝐹) ∈ ℕ0 → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (𝑥 ∈ (0...(#‘𝐹)) ∧ (𝑦 + 1) ∈ (0...(#‘𝐹)))))
5554imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((#‘𝐹) ∈ ℕ0 ∧ (𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → (𝑥 ∈ (0...(#‘𝐹)) ∧ (𝑦 + 1) ∈ (0...(#‘𝐹))))
56 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑏 = (𝑦 + 1) → (𝑃𝑏) = (𝑃‘(𝑦 + 1)))
5756eqeq2d 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑏 = (𝑦 + 1) → ((𝑃𝑥) = (𝑃𝑏) ↔ (𝑃𝑥) = (𝑃‘(𝑦 + 1))))
58 eqeq2 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑏 = (𝑦 + 1) → (𝑥 = 𝑏𝑥 = (𝑦 + 1)))
5957, 58imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑏 = (𝑦 + 1) → (((𝑃𝑥) = (𝑃𝑏) → 𝑥 = 𝑏) ↔ ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) → 𝑥 = (𝑦 + 1))))
6041, 59rspc2v 3293 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑥 ∈ (0...(#‘𝐹)) ∧ (𝑦 + 1) ∈ (0...(#‘𝐹))) → (∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) → ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) → 𝑥 = (𝑦 + 1))))
6155, 60syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((#‘𝐹) ∈ ℕ0 ∧ (𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → (∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) → ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) → 𝑥 = (𝑦 + 1))))
6261imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((#‘𝐹) ∈ ℕ0 ∧ (𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) ∧ ∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏)) → ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) → 𝑥 = (𝑦 + 1)))
63 fzofzp1 12431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑥 ∈ (0..^(#‘𝐹)) → (𝑥 + 1) ∈ (0...(#‘𝐹)))
6463a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((#‘𝐹) ∈ ℕ0 → (𝑥 ∈ (0..^(#‘𝐹)) → (𝑥 + 1) ∈ (0...(#‘𝐹))))
6564, 37anim12d1 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((#‘𝐹) ∈ ℕ0 → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ((𝑥 + 1) ∈ (0...(#‘𝐹)) ∧ 𝑦 ∈ (0...(#‘𝐹)))))
6665imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((#‘𝐹) ∈ ℕ0 ∧ (𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → ((𝑥 + 1) ∈ (0...(#‘𝐹)) ∧ 𝑦 ∈ (0...(#‘𝐹))))
67 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑎 = (𝑥 + 1) → (𝑃𝑎) = (𝑃‘(𝑥 + 1)))
6867eqeq1d 2612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑎 = (𝑥 + 1) → ((𝑃𝑎) = (𝑃𝑏) ↔ (𝑃‘(𝑥 + 1)) = (𝑃𝑏)))
69 eqeq1 2614 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑎 = (𝑥 + 1) → (𝑎 = 𝑏 ↔ (𝑥 + 1) = 𝑏))
7068, 69imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑎 = (𝑥 + 1) → (((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) ↔ ((𝑃‘(𝑥 + 1)) = (𝑃𝑏) → (𝑥 + 1) = 𝑏)))
7142eqeq2d 2620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑏 = 𝑦 → ((𝑃‘(𝑥 + 1)) = (𝑃𝑏) ↔ (𝑃‘(𝑥 + 1)) = (𝑃𝑦)))
72 eqeq2 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑏 = 𝑦 → ((𝑥 + 1) = 𝑏 ↔ (𝑥 + 1) = 𝑦))
7371, 72imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑏 = 𝑦 → (((𝑃‘(𝑥 + 1)) = (𝑃𝑏) → (𝑥 + 1) = 𝑏) ↔ ((𝑃‘(𝑥 + 1)) = (𝑃𝑦) → (𝑥 + 1) = 𝑦)))
7470, 73rspc2v 3293 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑥 + 1) ∈ (0...(#‘𝐹)) ∧ 𝑦 ∈ (0...(#‘𝐹))) → (∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) → ((𝑃‘(𝑥 + 1)) = (𝑃𝑦) → (𝑥 + 1) = 𝑦)))
7566, 74syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((#‘𝐹) ∈ ℕ0 ∧ (𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → (∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) → ((𝑃‘(𝑥 + 1)) = (𝑃𝑦) → (𝑥 + 1) = 𝑦)))
7675imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((#‘𝐹) ∈ ℕ0 ∧ (𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) ∧ ∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏)) → ((𝑃‘(𝑥 + 1)) = (𝑃𝑦) → (𝑥 + 1) = 𝑦))
7762, 76anim12d 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((#‘𝐹) ∈ ℕ0 ∧ (𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) ∧ ∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏)) → (((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦)) → (𝑥 = (𝑦 + 1) ∧ (𝑥 + 1) = 𝑦)))
7877expimpd 627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((#‘𝐹) ∈ ℕ0 ∧ (𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → ((∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) ∧ ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦))) → (𝑥 = (𝑦 + 1) ∧ (𝑥 + 1) = 𝑦)))
79 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑥 = (𝑦 + 1) → (𝑥 + 1) = ((𝑦 + 1) + 1))
8079eqeq1d 2612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 = (𝑦 + 1) → ((𝑥 + 1) = 𝑦 ↔ ((𝑦 + 1) + 1) = 𝑦))
8180adantl 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))
8583, 84syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦 ∈ ℕ0 → ((𝑦 + 1) + 1) = (𝑦 + 2))
8685eqeq1d 2612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 ∈ ℕ0 → (((𝑦 + 1) + 1) = 𝑦 ↔ (𝑦 + 2) = 𝑦))
87 2cnd 10970 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑦 ∈ ℕ0 → 2 ∈ ℂ)
88 2ne0 10990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 2 ≠ 0
8988a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑦 ∈ ℕ0 → 2 ≠ 0)
90 addn0nid 10330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑦 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (𝑦 + 2) ≠ 𝑦)
9183, 87, 89, 90syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑦 ∈ ℕ0 → (𝑦 + 2) ≠ 𝑦)
92 eqneqall 2793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑦 + 2) = 𝑦 → ((𝑦 + 2) ≠ 𝑦𝑥 = 𝑦))
9391, 92syl5com 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑦 ∈ ℕ0 → ((𝑦 + 2) = 𝑦𝑥 = 𝑦))
9486, 93sylbid 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑦 ∈ ℕ0 → (((𝑦 + 1) + 1) = 𝑦𝑥 = 𝑦))
9582, 94syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 ∈ (0..^(#‘𝐹)) → (((𝑦 + 1) + 1) = 𝑦𝑥 = 𝑦))
9695adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (((𝑦 + 1) + 1) = 𝑦𝑥 = 𝑦))
9796adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑥 = (𝑦 + 1)) → (((𝑦 + 1) + 1) = 𝑦𝑥 = 𝑦))
9881, 97sylbid 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) ∧ 𝑥 = (𝑦 + 1)) → ((𝑥 + 1) = 𝑦𝑥 = 𝑦))
9998expimpd 627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ((𝑥 = (𝑦 + 1) ∧ (𝑥 + 1) = 𝑦) → 𝑥 = 𝑦))
10099adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((#‘𝐹) ∈ ℕ0 ∧ (𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → ((𝑥 = (𝑦 + 1) ∧ (𝑥 + 1) = 𝑦) → 𝑥 = 𝑦))
10178, 100syld 46 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((#‘𝐹) ∈ ℕ0 ∧ (𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹)))) → ((∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) ∧ ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦))) → 𝑥 = 𝑦))
102101ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((#‘𝐹) ∈ ℕ0 → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ((∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) ∧ ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦))) → 𝑥 = 𝑦)))
10351, 102syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ((∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) ∧ ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦))) → 𝑥 = 𝑦)))
104103com3l 87 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ((∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) ∧ ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦))) → (𝐹 ∈ Fin → 𝑥 = 𝑦)))
105104expd 451 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) → (((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦)) → (𝐹 ∈ Fin → 𝑥 = 𝑦))))
106105com34 89 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) → (𝐹 ∈ Fin → (((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦)) → 𝑥 = 𝑦))))
107106com14 94 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦)) → (∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) → (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑥 = 𝑦))))
10850, 107jaoi 393 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑃𝑥) = (𝑃𝑦) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1))) ∨ ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦))) → (∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏) → (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑥 = 𝑦))))
109108adantld 482 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑃𝑥) = (𝑃𝑦) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1))) ∨ ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦))) → ((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑎 ∈ (0...(#‘𝐹))∀𝑏 ∈ (0...(#‘𝐹))((𝑃𝑎) = (𝑃𝑏) → 𝑎 = 𝑏)) → (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑥 = 𝑦))))
11035, 109syl5bi 231 . . . . . . . . . . . . . . . . . . . 20 ((((𝑃𝑥) = (𝑃𝑦) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1))) ∨ ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦))) → (𝑃:(0...(#‘𝐹))–1-1𝑉 → (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑥 = 𝑦))))
111110com23 84 . . . . . . . . . . . . . . . . . . 19 ((((𝑃𝑥) = (𝑃𝑦) ∧ (𝑃‘(𝑥 + 1)) = (𝑃‘(𝑦 + 1))) ∨ ((𝑃𝑥) = (𝑃‘(𝑦 + 1)) ∧ (𝑃‘(𝑥 + 1)) = (𝑃𝑦))) → (𝐹 ∈ Fin → (𝑃:(0...(#‘𝐹))–1-1𝑉 → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑥 = 𝑦))))
11234, 111sylbi 206 . . . . . . . . . . . . . . . . . 18 ({(𝑃𝑥), (𝑃‘(𝑥 + 1))} = {(𝑃𝑦), (𝑃‘(𝑦 + 1))} → (𝐹 ∈ Fin → (𝑃:(0...(#‘𝐹))–1-1𝑉 → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑥 = 𝑦))))
11329, 112syl 17 . . . . . . . . . . . . . . . . 17 (((𝐼‘(𝐹𝑥)) = (𝐼‘(𝐹𝑦)) ∧ ((𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))})) → (𝐹 ∈ Fin → (𝑃:(0...(#‘𝐹))–1-1𝑉 → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑥 = 𝑦))))
114113ex 449 . . . . . . . . . . . . . . . 16 ((𝐼‘(𝐹𝑥)) = (𝐼‘(𝐹𝑦)) → (((𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))}) → (𝐹 ∈ Fin → (𝑃:(0...(#‘𝐹))–1-1𝑉 → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑥 = 𝑦)))))
11522, 114syl 17 . . . . . . . . . . . . . . 15 ((𝐹𝑥) = (𝐹𝑦) → (((𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))}) → (𝐹 ∈ Fin → (𝑃:(0...(#‘𝐹))–1-1𝑉 → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → 𝑥 = 𝑦)))))
116115com15 99 . . . . . . . . . . . . . 14 ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (((𝐼‘(𝐹𝑥)) = {(𝑃𝑥), (𝑃‘(𝑥 + 1))} ∧ (𝐼‘(𝐹𝑦)) = {(𝑃𝑦), (𝑃‘(𝑦 + 1))}) → (𝐹 ∈ Fin → (𝑃:(0...(#‘𝐹))–1-1𝑉 → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))))
11721, 116syld 46 . . . . . . . . . . . . 13 ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))} → (𝐹 ∈ Fin → (𝑃:(0...(#‘𝐹))–1-1𝑉 → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))))
118117com14 94 . . . . . . . . . . . 12 (𝑃:(0...(#‘𝐹))–1-1𝑉 → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))} → (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))))
119118imp 444 . . . . . . . . . . 11 ((𝑃:(0...(#‘𝐹))–1-1𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))}) → (𝐹 ∈ Fin → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))))
120119impcom 445 . . . . . . . . . 10 ((𝐹 ∈ Fin ∧ (𝑃:(0...(#‘𝐹))–1-1𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))})) → ((𝑥 ∈ (0..^(#‘𝐹)) ∧ 𝑦 ∈ (0..^(#‘𝐹))) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
121120ralrimivv 2953 . . . . . . . . 9 ((𝐹 ∈ Fin ∧ (𝑃:(0...(#‘𝐹))–1-1𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))})) → ∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
122121adantlr 747 . . . . . . . 8 (((𝐹 ∈ Fin ∧ 𝐹:(0..^(#‘𝐹))⟶dom 𝐼) ∧ (𝑃:(0...(#‘𝐹))–1-1𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))})) → ∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
123 dff13 6416 . . . . . . . 8 (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐼 ↔ (𝐹:(0..^(#‘𝐹))⟶dom 𝐼 ∧ ∀𝑥 ∈ (0..^(#‘𝐹))∀𝑦 ∈ (0..^(#‘𝐹))((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
1244, 122, 123sylanbrc 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 𝐹))
126124, 125sylib 207 . . . . . 6 (((𝐹 ∈ Fin ∧ 𝐹:(0..^(#‘𝐹))⟶dom 𝐼) ∧ (𝑃:(0...(#‘𝐹))–1-1𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))})) → (𝐹:(0..^(#‘𝐹))⟶dom 𝐼 ∧ Fun 𝐹))
127 simpr 476 . . . . . 6 ((𝐹:(0..^(#‘𝐹))⟶dom 𝐼 ∧ Fun 𝐹) → Fun 𝐹)
128126, 127syl 17 . . . . 5 (((𝐹 ∈ Fin ∧ 𝐹:(0..^(#‘𝐹))⟶dom 𝐼) ∧ (𝑃:(0...(#‘𝐹))–1-1𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))})) → Fun 𝐹)
129128ex 449 . . . 4 ((𝐹 ∈ Fin ∧ 𝐹:(0..^(#‘𝐹))⟶dom 𝐼) → ((𝑃:(0...(#‘𝐹))–1-1𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))}) → Fun 𝐹))
130129expd 451 . . 3 ((𝐹 ∈ Fin ∧ 𝐹:(0..^(#‘𝐹))⟶dom 𝐼) → (𝑃:(0...(#‘𝐹))–1-1𝑉 → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))} → Fun 𝐹)))
1311, 2, 130syl2anc 691 . 2 (𝐹 ∈ Word dom 𝐼 → (𝑃:(0...(#‘𝐹))–1-1𝑉 → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))} → Fun 𝐹)))
132131impcom 445 1 ((𝑃:(0...(#‘𝐹))–1-1𝑉𝐹 ∈ Word dom 𝐼) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))} → Fun 𝐹))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  {cpr 4127  ◡ccnv 5037  dom cdm 5038  Fun wfun 5798  ⟶wf 5800  –1-1→wf1 5801  ‘cfv 5804  (class class class)co 6549  Fincfn 7841  ℂcc 9813  0cc0 9815  1c1 9816   + caddc 9818  2c2 10947  ℕ0cn0 11169  ...cfz 12197  ..^cfzo 12334  #chash 12979  Word cword 13146 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-fzo 12335  df-hash 12980  df-word 13154 This theorem is referenced by:  upgrwlkdvde  40943
 Copyright terms: Public domain W3C validator