This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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