Metamath Proof Explorer

Theorem fzo0pmtrlast

Description: Reorder a half-open integer range based at 0, so that the given index I is at the end. (Contributed by Thierry Arnoux, 27-May-2025)

Ref Expression
Hypotheses fzo0pmtrlast.j ⊢ J = 0 ..^ N
fzo0pmtrlast.i ⊢ φ → I ∈ J
Assertion fzo0pmtrlast ⊢ φ → ∃ s s : J ⟶ 1-1 onto J ∧ s ⁡ N − 1 = I

Proof

Step Hyp Ref Expression
1 fzo0pmtrlast.j ⊢ J = 0 ..^ N
2 fzo0pmtrlast.i ⊢ φ → I ∈ J
3 1 ovexi ⊢ J ∈ V
4 3 a1i ⊢ φ ∧ I = N − 1 → J ∈ V
5 4 resiexd ⊢ φ ∧ I = N − 1 → I ↾ J ∈ V
6 simpr ⊢ φ ∧ I = N − 1 → I = N − 1
7 2 adantr ⊢ φ ∧ I = N − 1 → I ∈ J
8 6 7 eqeltrrd ⊢ φ ∧ I = N − 1 → N − 1 ∈ J
9 fvresi ⊢ N − 1 ∈ J → I ↾ J ⁡ N − 1 = N − 1
10 8 9 syl ⊢ φ ∧ I = N − 1 → I ↾ J ⁡ N − 1 = N − 1
11 10 6 eqtr4d ⊢ φ ∧ I = N − 1 → I ↾ J ⁡ N − 1 = I
12 f1oi ⊢ I ↾ J : J ⟶ 1-1 onto J
13 11 12 jctil ⊢ φ ∧ I = N − 1 → I ↾ J : J ⟶ 1-1 onto J ∧ I ↾ J ⁡ N − 1 = I
14 f1oeq1 ⊢ s = I ↾ J → s : J ⟶ 1-1 onto J ↔ I ↾ J : J ⟶ 1-1 onto J
15 fveq1 ⊢ s = I ↾ J → s ⁡ N − 1 = I ↾ J ⁡ N − 1
16 15 eqeq1d ⊢ s = I ↾ J → s ⁡ N − 1 = I ↔ I ↾ J ⁡ N − 1 = I
17 14 16 anbi12d ⊢ s = I ↾ J → s : J ⟶ 1-1 onto J ∧ s ⁡ N − 1 = I ↔ I ↾ J : J ⟶ 1-1 onto J ∧ I ↾ J ⁡ N − 1 = I
18 5 13 17 spcedv ⊢ φ ∧ I = N − 1 → ∃ s s : J ⟶ 1-1 onto J ∧ s ⁡ N − 1 = I
19 fvexd ⊢ φ ∧ I ≠ N − 1 → pmTrsp ⁡ J ⁡ I N − 1 ∈ V
20 3 a1i ⊢ φ ∧ I ≠ N − 1 → J ∈ V
21 2 adantr ⊢ φ ∧ I ≠ N − 1 → I ∈ J
22 2 1 eleqtrdi ⊢ φ → I ∈ 0 ..^ N
23 elfzo0 ⊢ I ∈ 0 ..^ N ↔ I ∈ ℕ 0 ∧ N ∈ ℕ ∧ I < N
24 23 simp2bi ⊢ I ∈ 0 ..^ N → N ∈ ℕ
25 fzo0end ⊢ N ∈ ℕ → N − 1 ∈ 0 ..^ N
26 22 24 25 3syl ⊢ φ → N − 1 ∈ 0 ..^ N
27 26 1 eleqtrrdi ⊢ φ → N − 1 ∈ J
28 27 adantr ⊢ φ ∧ I ≠ N − 1 → N − 1 ∈ J
29 21 28 prssd ⊢ φ ∧ I ≠ N − 1 → I N − 1 ⊆ J
30 simpr ⊢ φ ∧ I ≠ N − 1 → I ≠ N − 1
31 enpr2 ⊢ I ∈ J ∧ N − 1 ∈ J ∧ I ≠ N − 1 → I N − 1 ≈ 2 𝑜
32 21 28 30 31 syl3anc ⊢ φ ∧ I ≠ N − 1 → I N − 1 ≈ 2 𝑜
33 eqid ⊢ pmTrsp ⁡ J = pmTrsp ⁡ J
34 eqid ⊢ ran ⁡ pmTrsp ⁡ J = ran ⁡ pmTrsp ⁡ J
35 33 34 pmtrrn ⊢ J ∈ V ∧ I N − 1 ⊆ J ∧ I N − 1 ≈ 2 𝑜 → pmTrsp ⁡ J ⁡ I N − 1 ∈ ran ⁡ pmTrsp ⁡ J
36 20 29 32 35 syl3anc ⊢ φ ∧ I ≠ N − 1 → pmTrsp ⁡ J ⁡ I N − 1 ∈ ran ⁡ pmTrsp ⁡ J
37 33 34 pmtrff1o ⊢ pmTrsp ⁡ J ⁡ I N − 1 ∈ ran ⁡ pmTrsp ⁡ J → pmTrsp ⁡ J ⁡ I N − 1 : J ⟶ 1-1 onto J
38 36 37 syl ⊢ φ ∧ I ≠ N − 1 → pmTrsp ⁡ J ⁡ I N − 1 : J ⟶ 1-1 onto J
39 33 pmtrprfv2 ⊢ J ∈ V ∧ I ∈ J ∧ N − 1 ∈ J ∧ I ≠ N − 1 → pmTrsp ⁡ J ⁡ I N − 1 ⁡ N − 1 = I
40 20 21 28 30 39 syl13anc ⊢ φ ∧ I ≠ N − 1 → pmTrsp ⁡ J ⁡ I N − 1 ⁡ N − 1 = I
41 38 40 jca ⊢ φ ∧ I ≠ N − 1 → pmTrsp ⁡ J ⁡ I N − 1 : J ⟶ 1-1 onto J ∧ pmTrsp ⁡ J ⁡ I N − 1 ⁡ N − 1 = I
42 f1oeq1 ⊢ s = pmTrsp ⁡ J ⁡ I N − 1 → s : J ⟶ 1-1 onto J ↔ pmTrsp ⁡ J ⁡ I N − 1 : J ⟶ 1-1 onto J
43 fveq1 ⊢ s = pmTrsp ⁡ J ⁡ I N − 1 → s ⁡ N − 1 = pmTrsp ⁡ J ⁡ I N − 1 ⁡ N − 1
44 43 eqeq1d ⊢ s = pmTrsp ⁡ J ⁡ I N − 1 → s ⁡ N − 1 = I ↔ pmTrsp ⁡ J ⁡ I N − 1 ⁡ N − 1 = I
45 42 44 anbi12d ⊢ s = pmTrsp ⁡ J ⁡ I N − 1 → s : J ⟶ 1-1 onto J ∧ s ⁡ N − 1 = I ↔ pmTrsp ⁡ J ⁡ I N − 1 : J ⟶ 1-1 onto J ∧ pmTrsp ⁡ J ⁡ I N − 1 ⁡ N − 1 = I
46 19 41 45 spcedv ⊢ φ ∧ I ≠ N − 1 → ∃ s s : J ⟶ 1-1 onto J ∧ s ⁡ N − 1 = I
47 18 46 pm2.61dane ⊢ φ → ∃ s s : J ⟶ 1-1 onto J ∧ s ⁡ N − 1 = I