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 ⊢ 𝐽 = ( 0 ..^ 𝑁 )
fzo0pmtrlast.i ⊢ ( 𝜑 → 𝐼 ∈ 𝐽 )
Assertion fzo0pmtrlast ( 𝜑 → ∃ 𝑠 ( 𝑠 : 𝐽 –1-1-onto→ 𝐽 ∧ ( 𝑠 ‘ ( 𝑁 − 1 ) ) = 𝐼 ) )

Proof

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