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 
|- ( ph -> I e. J )
Assertion fzo0pmtrlast 
|- ( ph -> E. 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 
 |-  ( ph -> I e. J )
3 1 ovexi 
 |-  J e. _V
4 3 a1i 
 |-  ( ( ph /\ I = ( N - 1 ) ) -> J e. _V )
5 4 resiexd 
 |-  ( ( ph /\ I = ( N - 1 ) ) -> ( _I |` J ) e. _V )
6 simpr 
 |-  ( ( ph /\ I = ( N - 1 ) ) -> I = ( N - 1 ) )
7 2 adantr 
 |-  ( ( ph /\ I = ( N - 1 ) ) -> I e. J )
8 6 7 eqeltrrd 
 |-  ( ( ph /\ I = ( N - 1 ) ) -> ( N - 1 ) e. J )
9 fvresi 
 |-  ( ( N - 1 ) e. J -> ( ( _I |` J ) ` ( N - 1 ) ) = ( N - 1 ) )
10 8 9 syl 
 |-  ( ( ph /\ I = ( N - 1 ) ) -> ( ( _I |` J ) ` ( N - 1 ) ) = ( N - 1 ) )
11 10 6 eqtr4d 
 |-  ( ( ph /\ I = ( N - 1 ) ) -> ( ( _I |` J ) ` ( N - 1 ) ) = I )
12 f1oi 
 |-  ( _I |` J ) : J -1-1-onto-> J
13 11 12 jctil 
 |-  ( ( ph /\ 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 
 |-  ( ( ph /\ I = ( N - 1 ) ) -> E. s ( s : J -1-1-onto-> J /\ ( s ` ( N - 1 ) ) = I ) )
19 fvexd 
 |-  ( ( ph /\ I =/= ( N - 1 ) ) -> ( ( pmTrsp ` J ) ` { I , ( N - 1 ) } ) e. _V )
20 3 a1i 
 |-  ( ( ph /\ I =/= ( N - 1 ) ) -> J e. _V )
21 2 adantr 
 |-  ( ( ph /\ I =/= ( N - 1 ) ) -> I e. J )
22 2 1 eleqtrdi 
 |-  ( ph -> I e. ( 0 ..^ N ) )
23 elfzo0 
 |-  ( I e. ( 0 ..^ N ) <-> ( I e. NN0 /\ N e. NN /\ I < N ) )
24 23 simp2bi 
 |-  ( I e. ( 0 ..^ N ) -> N e. NN )
25 fzo0end 
 |-  ( N e. NN -> ( N - 1 ) e. ( 0 ..^ N ) )
26 22 24 25 3syl 
 |-  ( ph -> ( N - 1 ) e. ( 0 ..^ N ) )
27 26 1 eleqtrrdi 
 |-  ( ph -> ( N - 1 ) e. J )
28 27 adantr 
 |-  ( ( ph /\ I =/= ( N - 1 ) ) -> ( N - 1 ) e. J )
29 21 28 prssd 
 |-  ( ( ph /\ I =/= ( N - 1 ) ) -> { I , ( N - 1 ) } C_ J )
30 simpr 
 |-  ( ( ph /\ I =/= ( N - 1 ) ) -> I =/= ( N - 1 ) )
31 enpr2 
 |-  ( ( I e. J /\ ( N - 1 ) e. J /\ I =/= ( N - 1 ) ) -> { I , ( N - 1 ) } ~~ 2o )
32 21 28 30 31 syl3anc 
 |-  ( ( ph /\ I =/= ( N - 1 ) ) -> { I , ( N - 1 ) } ~~ 2o )
33 eqid 
 |-  ( pmTrsp ` J ) = ( pmTrsp ` J )
34 eqid 
 |-  ran ( pmTrsp ` J ) = ran ( pmTrsp ` J )
35 33 34 pmtrrn 
 |-  ( ( J e. _V /\ { I , ( N - 1 ) } C_ J /\ { I , ( N - 1 ) } ~~ 2o ) -> ( ( pmTrsp ` J ) ` { I , ( N - 1 ) } ) e. ran ( pmTrsp ` J ) )
36 20 29 32 35 syl3anc 
 |-  ( ( ph /\ I =/= ( N - 1 ) ) -> ( ( pmTrsp ` J ) ` { I , ( N - 1 ) } ) e. ran ( pmTrsp ` J ) )
37 33 34 pmtrff1o 
 |-  ( ( ( pmTrsp ` J ) ` { I , ( N - 1 ) } ) e. ran ( pmTrsp ` J ) -> ( ( pmTrsp ` J ) ` { I , ( N - 1 ) } ) : J -1-1-onto-> J )
38 36 37 syl 
 |-  ( ( ph /\ I =/= ( N - 1 ) ) -> ( ( pmTrsp ` J ) ` { I , ( N - 1 ) } ) : J -1-1-onto-> J )
39 33 pmtrprfv2 
 |-  ( ( J e. _V /\ ( I e. J /\ ( N - 1 ) e. J /\ I =/= ( N - 1 ) ) ) -> ( ( ( pmTrsp ` J ) ` { I , ( N - 1 ) } ) ` ( N - 1 ) ) = I )
40 20 21 28 30 39 syl13anc 
 |-  ( ( ph /\ I =/= ( N - 1 ) ) -> ( ( ( pmTrsp ` J ) ` { I , ( N - 1 ) } ) ` ( N - 1 ) ) = I )
41 38 40 jca 
 |-  ( ( ph /\ 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 
 |-  ( ( ph /\ I =/= ( N - 1 ) ) -> E. s ( s : J -1-1-onto-> J /\ ( s ` ( N - 1 ) ) = I ) )
47 18 46 pm2.61dane 
 |-  ( ph -> E. s ( s : J -1-1-onto-> J /\ ( s ` ( N - 1 ) ) = I ) )