Metamath Proof Explorer

Theorem pthdlem1

Description: Lemma 1 for pthd . (Contributed by Alexander van der Vekens, 13-Nov-2017) (Revised by AV, 9-Feb-2021)

Ref Expression
Hypotheses pthd.p ⊢ ( 𝜑 → 𝑃 ∈ Word V )
pthd.r ⊢ 𝑅 = ( ( ♯ ‘ 𝑃 ) − 1 )
pthd.s ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) )
Assertion pthdlem1 ( 𝜑 → Fun ◡ ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 pthd.p ⊢ ( 𝜑 → 𝑃 ∈ Word V )
2 pthd.r ⊢ 𝑅 = ( ( ♯ ‘ 𝑃 ) − 1 )
3 pthd.s ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) )
4 wrdf ⊢ ( 𝑃 ∈ Word V → 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ V )
5 1 4 syl ⊢ ( 𝜑 → 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ V )
6 fzo0ss1 ⊢ ( 1 ..^ 𝑅 ) ⊆ ( 0 ..^ 𝑅 )
7 2 a1i ⊢ ( 𝜑 → 𝑅 = ( ( ♯ ‘ 𝑃 ) − 1 ) )
8 7 oveq2d ⊢ ( 𝜑 → ( 0 ..^ 𝑅 ) = ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
9 6 8 sseqtrid ⊢ ( 𝜑 → ( 1 ..^ 𝑅 ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
10 lencl ⊢ ( 𝑃 ∈ Word V → ( ♯ ‘ 𝑃 ) ∈ ℕ0 )
11 nn0z ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ♯ ‘ 𝑃 ) ∈ ℤ )
12 1 10 11 3syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑃 ) ∈ ℤ )
13 fzossrbm1 ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℤ → ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) )
14 12 13 syl ⊢ ( 𝜑 → ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) )
15 9 14 sstrd ⊢ ( 𝜑 → ( 1 ..^ 𝑅 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) )
16 5 15 fssresd ⊢ ( 𝜑 → ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) : ( 1 ..^ 𝑅 ) ⟶ V )
17 16 adantr ⊢ ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) : ( 1 ..^ 𝑅 ) ⟶ V )
18 3 adantr ⊢ ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) )
19 1 10 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑃 ) ∈ ℕ0 )
20 nn0re ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ♯ ‘ 𝑃 ) ∈ ℝ )
21 20 ltm1d ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) − 1 ) < ( ♯ ‘ 𝑃 ) )
22 1re ⊢ 1 ∈ ℝ
23 peano2rem ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℝ → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℝ )
24 20 23 syl ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℝ )
25 lttr ⊢ ( ( 1 ∈ ℝ ∧ ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℝ ∧ ( ♯ ‘ 𝑃 ) ∈ ℝ ) → ( ( 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ∧ ( ( ♯ ‘ 𝑃 ) − 1 ) < ( ♯ ‘ 𝑃 ) ) → 1 < ( ♯ ‘ 𝑃 ) ) )
26 22 24 20 25 mp3an2i ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ∧ ( ( ♯ ‘ 𝑃 ) − 1 ) < ( ♯ ‘ 𝑃 ) ) → 1 < ( ♯ ‘ 𝑃 ) ) )
27 1red ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → 1 ∈ ℝ )
28 ltle ⊢ ( ( 1 ∈ ℝ ∧ ( ♯ ‘ 𝑃 ) ∈ ℝ ) → ( 1 < ( ♯ ‘ 𝑃 ) → 1 ≤ ( ♯ ‘ 𝑃 ) ) )
29 27 20 28 syl2anc ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( 1 < ( ♯ ‘ 𝑃 ) → 1 ≤ ( ♯ ‘ 𝑃 ) ) )
30 26 29 syld ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ∧ ( ( ♯ ‘ 𝑃 ) − 1 ) < ( ♯ ‘ 𝑃 ) ) → 1 ≤ ( ♯ ‘ 𝑃 ) ) )
31 21 30 mpan2d ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) → 1 ≤ ( ♯ ‘ 𝑃 ) ) )
32 31 imdistani ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) )
33 elnnnn0c ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) )
34 32 33 sylibr ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( ♯ ‘ 𝑃 ) ∈ ℕ )
35 19 34 sylan ⊢ ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( ♯ ‘ 𝑃 ) ∈ ℕ )
36 fzo0sn0fzo1 ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ → ( 0 ..^ ( ♯ ‘ 𝑃 ) ) = ( { 0 } ∪ ( 1 ..^ ( ♯ ‘ 𝑃 ) ) ) )
37 35 36 syl ⊢ ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( 0 ..^ ( ♯ ‘ 𝑃 ) ) = ( { 0 } ∪ ( 1 ..^ ( ♯ ‘ 𝑃 ) ) ) )
38 1zzd ⊢ ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → 1 ∈ ℤ )
39 1p1e2 ⊢ ( 1 + 1 ) = 2
40 2z ⊢ 2 ∈ ℤ
41 39 40 eqeltri ⊢ ( 1 + 1 ) ∈ ℤ
42 41 a1i ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( 1 + 1 ) ∈ ℤ )
43 11 adantr ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( ♯ ‘ 𝑃 ) ∈ ℤ )
44 ltaddsub ⊢ ( ( 1 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ♯ ‘ 𝑃 ) ∈ ℝ ) → ( ( 1 + 1 ) < ( ♯ ‘ 𝑃 ) ↔ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
45 44 bicomd ⊢ ( ( 1 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ♯ ‘ 𝑃 ) ∈ ℝ ) → ( 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ↔ ( 1 + 1 ) < ( ♯ ‘ 𝑃 ) ) )
46 22 27 20 45 mp3an2i ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ↔ ( 1 + 1 ) < ( ♯ ‘ 𝑃 ) ) )
47 2re ⊢ 2 ∈ ℝ
48 39 47 eqeltri ⊢ ( 1 + 1 ) ∈ ℝ
49 ltle ⊢ ( ( ( 1 + 1 ) ∈ ℝ ∧ ( ♯ ‘ 𝑃 ) ∈ ℝ ) → ( ( 1 + 1 ) < ( ♯ ‘ 𝑃 ) → ( 1 + 1 ) ≤ ( ♯ ‘ 𝑃 ) ) )
50 48 20 49 sylancr ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ( 1 + 1 ) < ( ♯ ‘ 𝑃 ) → ( 1 + 1 ) ≤ ( ♯ ‘ 𝑃 ) ) )
51 46 50 sylbid ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) → ( 1 + 1 ) ≤ ( ♯ ‘ 𝑃 ) ) )
52 51 imp ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( 1 + 1 ) ≤ ( ♯ ‘ 𝑃 ) )
53 eluz2 ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ↔ ( ( 1 + 1 ) ∈ ℤ ∧ ( ♯ ‘ 𝑃 ) ∈ ℤ ∧ ( 1 + 1 ) ≤ ( ♯ ‘ 𝑃 ) ) )
54 42 43 52 53 syl3anbrc ⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( ♯ ‘ 𝑃 ) ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) )
55 19 54 sylan ⊢ ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( ♯ ‘ 𝑃 ) ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) )
56 fzosplitsnm1 ⊢ ( ( 1 ∈ ℤ ∧ ( ♯ ‘ 𝑃 ) ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → ( 1 ..^ ( ♯ ‘ 𝑃 ) ) = ( ( 1 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑃 ) − 1 ) } ) )
57 38 55 56 syl2anc ⊢ ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( 1 ..^ ( ♯ ‘ 𝑃 ) ) = ( ( 1 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑃 ) − 1 ) } ) )
58 57 uneq2d ⊢ ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( { 0 } ∪ ( 1 ..^ ( ♯ ‘ 𝑃 ) ) ) = ( { 0 } ∪ ( ( 1 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑃 ) − 1 ) } ) ) )
59 37 58 eqtrd ⊢ ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( 0 ..^ ( ♯ ‘ 𝑃 ) ) = ( { 0 } ∪ ( ( 1 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑃 ) − 1 ) } ) ) )
60 59 raleqdv ⊢ ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ↔ ∀ 𝑖 ∈ ( { 0 } ∪ ( ( 1 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑃 ) − 1 ) } ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ) )
61 ralunb ⊢ ( ∀ 𝑖 ∈ ( { 0 } ∪ ( ( 1 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑃 ) − 1 ) } ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ↔ ( ∀ 𝑖 ∈ { 0 } ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ∧ ∀ 𝑖 ∈ ( ( 1 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑃 ) − 1 ) } ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ) )
62 ralunb ⊢ ( ∀ 𝑖 ∈ ( ( 1 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑃 ) − 1 ) } ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ↔ ( ∀ 𝑖 ∈ ( 1 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ∧ ∀ 𝑖 ∈ { ( ( ♯ ‘ 𝑃 ) − 1 ) } ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ) )
63 62 anbi2i ⊢ ( ( ∀ 𝑖 ∈ { 0 } ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ∧ ∀ 𝑖 ∈ ( ( 1 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑃 ) − 1 ) } ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ) ↔ ( ∀ 𝑖 ∈ { 0 } ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ∧ ∀ 𝑖 ∈ { ( ( ♯ ‘ 𝑃 ) − 1 ) } ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ) ) )
64 61 63 bitri ⊢ ( ∀ 𝑖 ∈ ( { 0 } ∪ ( ( 1 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑃 ) − 1 ) } ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ↔ ( ∀ 𝑖 ∈ { 0 } ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ∧ ∀ 𝑖 ∈ { ( ( ♯ ‘ 𝑃 ) − 1 ) } ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ) ) )
65 60 64 bitrdi ⊢ ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ↔ ( ∀ 𝑖 ∈ { 0 } ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ∧ ∀ 𝑖 ∈ { ( ( ♯ ‘ 𝑃 ) − 1 ) } ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ) ) ) )
66 2 eqcomi ⊢ ( ( ♯ ‘ 𝑃 ) − 1 ) = 𝑅
67 66 oveq2i ⊢ ( 1 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) = ( 1 ..^ 𝑅 )
68 67 raleqi ⊢ ( ∀ 𝑖 ∈ ( 1 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ↔ ∀ 𝑖 ∈ ( 1 ..^ 𝑅 ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) )
69 fvres ⊢ ( 𝑖 ∈ ( 1 ..^ 𝑅 ) → ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑖 ) = ( 𝑃 ‘ 𝑖 ) )
70 69 eqcomd ⊢ ( 𝑖 ∈ ( 1 ..^ 𝑅 ) → ( 𝑃 ‘ 𝑖 ) = ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑖 ) )
71 70 adantl ⊢ ( ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑅 ) ) → ( 𝑃 ‘ 𝑖 ) = ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑖 ) )
72 71 adantr ⊢ ( ( ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑅 ) ) ∧ 𝑗 ∈ ( 1 ..^ 𝑅 ) ) → ( 𝑃 ‘ 𝑖 ) = ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑖 ) )
73 fvres ⊢ ( 𝑗 ∈ ( 1 ..^ 𝑅 ) → ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑗 ) = ( 𝑃 ‘ 𝑗 ) )
74 73 eqcomd ⊢ ( 𝑗 ∈ ( 1 ..^ 𝑅 ) → ( 𝑃 ‘ 𝑗 ) = ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑗 ) )
75 74 adantl ⊢ ( ( ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑅 ) ) ∧ 𝑗 ∈ ( 1 ..^ 𝑅 ) ) → ( 𝑃 ‘ 𝑗 ) = ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑗 ) )
76 72 75 neeq12d ⊢ ( ( ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑅 ) ) ∧ 𝑗 ∈ ( 1 ..^ 𝑅 ) ) → ( ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ↔ ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑖 ) ≠ ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑗 ) ) )
77 76 biimpd ⊢ ( ( ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑅 ) ) ∧ 𝑗 ∈ ( 1 ..^ 𝑅 ) ) → ( ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) → ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑖 ) ≠ ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑗 ) ) )
78 77 imim2d ⊢ ( ( ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑅 ) ) ∧ 𝑗 ∈ ( 1 ..^ 𝑅 ) ) → ( ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) → ( 𝑖 ≠ 𝑗 → ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑖 ) ≠ ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑗 ) ) ) )
79 78 ralimdva ⊢ ( ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑅 ) ) → ( ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) → ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑖 ) ≠ ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑗 ) ) ) )
80 79 ralimdva ⊢ ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( ∀ 𝑖 ∈ ( 1 ..^ 𝑅 ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) → ∀ 𝑖 ∈ ( 1 ..^ 𝑅 ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑖 ) ≠ ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑗 ) ) ) )
81 68 80 syl5bi ⊢ ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( ∀ 𝑖 ∈ ( 1 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) → ∀ 𝑖 ∈ ( 1 ..^ 𝑅 ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑖 ) ≠ ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑗 ) ) ) )
82 81 adantrd ⊢ ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( ( ∀ 𝑖 ∈ ( 1 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ∧ ∀ 𝑖 ∈ { ( ( ♯ ‘ 𝑃 ) − 1 ) } ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ) → ∀ 𝑖 ∈ ( 1 ..^ 𝑅 ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑖 ) ≠ ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑗 ) ) ) )
83 82 adantld ⊢ ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( ( ∀ 𝑖 ∈ { 0 } ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ∧ ∀ 𝑖 ∈ { ( ( ♯ ‘ 𝑃 ) − 1 ) } ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ..^ 𝑅 ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑖 ) ≠ ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑗 ) ) ) )
84 65 83 sylbid ⊢ ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( 𝑃 ‘ 𝑖 ) ≠ ( 𝑃 ‘ 𝑗 ) ) → ∀ 𝑖 ∈ ( 1 ..^ 𝑅 ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑖 ) ≠ ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑗 ) ) ) )
85 18 84 mpd ⊢ ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ∀ 𝑖 ∈ ( 1 ..^ 𝑅 ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑖 ) ≠ ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑗 ) ) )
86 dff14a ⊢ ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) : ( 1 ..^ 𝑅 ) –1-1→ V ↔ ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) : ( 1 ..^ 𝑅 ) ⟶ V ∧ ∀ 𝑖 ∈ ( 1 ..^ 𝑅 ) ∀ 𝑗 ∈ ( 1 ..^ 𝑅 ) ( 𝑖 ≠ 𝑗 → ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑖 ) ≠ ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ‘ 𝑗 ) ) ) )
87 17 85 86 sylanbrc ⊢ ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) : ( 1 ..^ 𝑅 ) –1-1→ V )
88 df-f1 ⊢ ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) : ( 1 ..^ 𝑅 ) –1-1→ V ↔ ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) : ( 1 ..^ 𝑅 ) ⟶ V ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ) )
89 87 88 sylib ⊢ ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) : ( 1 ..^ 𝑅 ) ⟶ V ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ) )
90 89 simprd ⊢ ( ( 𝜑 ∧ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → Fun ◡ ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) )
91 funcnv0 ⊢ Fun ◡ ∅
92 19 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ 𝑃 ) ∈ ℤ )
93 peano2zm ⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℤ → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℤ )
94 92 93 syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℤ )
95 94 zred ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℝ )
96 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
97 95 96 lenltd ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝑃 ) − 1 ) ≤ 1 ↔ ¬ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) )
98 97 biimpar ⊢ ( ( 𝜑 ∧ ¬ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( ( ♯ ‘ 𝑃 ) − 1 ) ≤ 1 )
99 2 98 eqbrtrid ⊢ ( ( 𝜑 ∧ ¬ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → 𝑅 ≤ 1 )
100 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
101 2 94 eqeltrid ⊢ ( 𝜑 → 𝑅 ∈ ℤ )
102 100 101 jca ⊢ ( 𝜑 → ( 1 ∈ ℤ ∧ 𝑅 ∈ ℤ ) )
103 102 adantr ⊢ ( ( 𝜑 ∧ ¬ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( 1 ∈ ℤ ∧ 𝑅 ∈ ℤ ) )
104 fzon ⊢ ( ( 1 ∈ ℤ ∧ 𝑅 ∈ ℤ ) → ( 𝑅 ≤ 1 ↔ ( 1 ..^ 𝑅 ) = ∅ ) )
105 104 bicomd ⊢ ( ( 1 ∈ ℤ ∧ 𝑅 ∈ ℤ ) → ( ( 1 ..^ 𝑅 ) = ∅ ↔ 𝑅 ≤ 1 ) )
106 103 105 syl ⊢ ( ( 𝜑 ∧ ¬ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( ( 1 ..^ 𝑅 ) = ∅ ↔ 𝑅 ≤ 1 ) )
107 99 106 mpbird ⊢ ( ( 𝜑 ∧ ¬ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( 1 ..^ 𝑅 ) = ∅ )
108 107 reseq2d ⊢ ( ( 𝜑 ∧ ¬ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) = ( 𝑃 ↾ ∅ ) )
109 res0 ⊢ ( 𝑃 ↾ ∅ ) = ∅
110 108 109 eqtrdi ⊢ ( ( 𝜑 ∧ ¬ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) = ∅ )
111 110 cnveqd ⊢ ( ( 𝜑 ∧ ¬ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ◡ ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) = ◡ ∅ )
112 111 funeqd ⊢ ( ( 𝜑 ∧ ¬ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) ↔ Fun ◡ ∅ ) )
113 91 112 mpbiri ⊢ ( ( 𝜑 ∧ ¬ 1 < ( ( ♯ ‘ 𝑃 ) − 1 ) ) → Fun ◡ ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) )
114 90 113 pm2.61dan ⊢ ( 𝜑 → Fun ◡ ( 𝑃 ↾ ( 1 ..^ 𝑅 ) ) )