Metamath Proof Explorer

Theorem metakunt34

Description: D is a permutation. (Contributed by metakunt, 18-Jul-2024)

Ref Expression
Hypotheses metakunt34.1 
|- ( ph -> M e. NN )
metakunt34.2 
|- ( ph -> I e. NN )
metakunt34.3 
|- ( ph -> I <_ M )
metakunt34.4 
|- D = ( w e. ( 1 ... M ) |-> if ( w = I , w , if ( w < I , ( ( w + ( M - I ) ) + if ( I <_ ( w + ( M - I ) ) , 1 , 0 ) ) , ( ( w - I ) + if ( I <_ ( w - I ) , 1 , 0 ) ) ) ) )
Assertion metakunt34 
|- ( ph -> D : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )

Proof

Step Hyp Ref Expression
1 metakunt34.1 
 |-  ( ph -> M e. NN )
2 metakunt34.2 
 |-  ( ph -> I e. NN )
3 metakunt34.3 
 |-  ( ph -> I <_ M )
4 metakunt34.4 
 |-  D = ( w e. ( 1 ... M ) |-> if ( w = I , w , if ( w < I , ( ( w + ( M - I ) ) + if ( I <_ ( w + ( M - I ) ) , 1 , 0 ) ) , ( ( w - I ) + if ( I <_ ( w - I ) , 1 , 0 ) ) ) ) )
5 eqid 
 |-  ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) ) = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) )
6 eqid 
 |-  ( z e. ( 1 ... M ) |-> if ( z = M , I , if ( z < I , z , ( z + 1 ) ) ) ) = ( z e. ( 1 ... M ) |-> if ( z = M , I , if ( z < I , z , ( z + 1 ) ) ) )
7 1 2 3 5 6 metakunt14 
 |-  ( ph -> ( ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) /\ `' ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) ) = ( z e. ( 1 ... M ) |-> if ( z = M , I , if ( z < I , z , ( z + 1 ) ) ) ) ) )
8 7 simpld 
 |-  ( ph -> ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
9 f1ocnv 
 |-  ( ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) -> `' ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
10 8 9 syl 
 |-  ( ph -> `' ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
11 7 simprd 
 |-  ( ph -> `' ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) ) = ( z e. ( 1 ... M ) |-> if ( z = M , I , if ( z < I , z , ( z + 1 ) ) ) ) )
12 11 f1oeq1d 
 |-  ( ph -> ( `' ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) <-> ( z e. ( 1 ... M ) |-> if ( z = M , I , if ( z < I , z , ( z + 1 ) ) ) ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) ) )
13 10 12 mpbid 
 |-  ( ph -> ( z e. ( 1 ... M ) |-> if ( z = M , I , if ( z < I , z , ( z + 1 ) ) ) ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
14 eqid 
 |-  ( y e. ( 1 ... M ) |-> if ( y = M , M , if ( y < I , ( y + ( M - I ) ) , ( y + ( 1 - I ) ) ) ) ) = ( y e. ( 1 ... M ) |-> if ( y = M , M , if ( y < I , ( y + ( M - I ) ) , ( y + ( 1 - I ) ) ) ) )
15 1 2 3 14 metakunt25 
 |-  ( ph -> ( y e. ( 1 ... M ) |-> if ( y = M , M , if ( y < I , ( y + ( M - I ) ) , ( y + ( 1 - I ) ) ) ) ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
16 f1oco 
 |-  ( ( ( y e. ( 1 ... M ) |-> if ( y = M , M , if ( y < I , ( y + ( M - I ) ) , ( y + ( 1 - I ) ) ) ) ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) /\ ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) ) -> ( ( y e. ( 1 ... M ) |-> if ( y = M , M , if ( y < I , ( y + ( M - I ) ) , ( y + ( 1 - I ) ) ) ) ) o. ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) ) ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
17 15 8 16 syl2anc 
 |-  ( ph -> ( ( y e. ( 1 ... M ) |-> if ( y = M , M , if ( y < I , ( y + ( M - I ) ) , ( y + ( 1 - I ) ) ) ) ) o. ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) ) ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
18 f1oco 
 |-  ( ( ( z e. ( 1 ... M ) |-> if ( z = M , I , if ( z < I , z , ( z + 1 ) ) ) ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) /\ ( ( y e. ( 1 ... M ) |-> if ( y = M , M , if ( y < I , ( y + ( M - I ) ) , ( y + ( 1 - I ) ) ) ) ) o. ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) ) ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) ) -> ( ( z e. ( 1 ... M ) |-> if ( z = M , I , if ( z < I , z , ( z + 1 ) ) ) ) o. ( ( y e. ( 1 ... M ) |-> if ( y = M , M , if ( y < I , ( y + ( M - I ) ) , ( y + ( 1 - I ) ) ) ) ) o. ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) ) ) ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
19 13 17 18 syl2anc 
 |-  ( ph -> ( ( z e. ( 1 ... M ) |-> if ( z = M , I , if ( z < I , z , ( z + 1 ) ) ) ) o. ( ( y e. ( 1 ... M ) |-> if ( y = M , M , if ( y < I , ( y + ( M - I ) ) , ( y + ( 1 - I ) ) ) ) ) o. ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) ) ) ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
20 1 2 3 5 14 6 4 metakunt33 
 |-  ( ph -> ( ( z e. ( 1 ... M ) |-> if ( z = M , I , if ( z < I , z , ( z + 1 ) ) ) ) o. ( ( y e. ( 1 ... M ) |-> if ( y = M , M , if ( y < I , ( y + ( M - I ) ) , ( y + ( 1 - I ) ) ) ) ) o. ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) ) ) ) = D )
21 20 f1oeq1d 
 |-  ( ph -> ( ( ( z e. ( 1 ... M ) |-> if ( z = M , I , if ( z < I , z , ( z + 1 ) ) ) ) o. ( ( y e. ( 1 ... M ) |-> if ( y = M , M , if ( y < I , ( y + ( M - I ) ) , ( y + ( 1 - I ) ) ) ) ) o. ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) ) ) ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) <-> D : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) ) )
22 19 21 mpbid 
 |-  ( ph -> D : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )