Metamath Proof Explorer

Theorem pmtrto1cl

Description: Useful lemma for the following theorems. (Contributed by Thierry Arnoux, 21-Aug-2020)

Ref Expression
Hypotheses psgnfzto1st.d 
|- D = ( 1 ... N )
pmtrto1cl.t 
|- T = ( pmTrsp ` D )
Assertion pmtrto1cl 
|- ( ( K e. NN /\ ( K + 1 ) e. D ) -> ( T ` { K , ( K + 1 ) } ) e. ran T )

Proof

Step Hyp Ref Expression
1 psgnfzto1st.d 
 |-  D = ( 1 ... N )
2 pmtrto1cl.t 
 |-  T = ( pmTrsp ` D )
3 fzfi 
 |-  ( 1 ... N ) e. Fin
4 1 3 eqeltri 
 |-  D e. Fin
5 4 a1i 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> D e. Fin )
6 simpl 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> K e. NN )
7 simpr 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> ( K + 1 ) e. D )
8 7 1 eleqtrdi 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> ( K + 1 ) e. ( 1 ... N ) )
9 elfz1b 
 |-  ( ( K + 1 ) e. ( 1 ... N ) <-> ( ( K + 1 ) e. NN /\ N e. NN /\ ( K + 1 ) <_ N ) )
10 8 9 sylib 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> ( ( K + 1 ) e. NN /\ N e. NN /\ ( K + 1 ) <_ N ) )
11 10 simp2d 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> N e. NN )
12 6 nnred 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> K e. RR )
13 1red 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> 1 e. RR )
14 12 13 readdcld 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> ( K + 1 ) e. RR )
15 11 nnred 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> N e. RR )
16 12 lep1d 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> K <_ ( K + 1 ) )
17 10 simp3d 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> ( K + 1 ) <_ N )
18 12 14 15 16 17 letrd 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> K <_ N )
19 6 11 18 3jca 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> ( K e. NN /\ N e. NN /\ K <_ N ) )
20 elfz1b 
 |-  ( K e. ( 1 ... N ) <-> ( K e. NN /\ N e. NN /\ K <_ N ) )
21 19 20 sylibr 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> K e. ( 1 ... N ) )
22 21 1 eleqtrrdi 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> K e. D )
23 prssi 
 |-  ( ( K e. D /\ ( K + 1 ) e. D ) -> { K , ( K + 1 ) } C_ D )
24 22 7 23 syl2anc 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> { K , ( K + 1 ) } C_ D )
25 12 ltp1d 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> K < ( K + 1 ) )
26 12 25 ltned 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> K =/= ( K + 1 ) )
27 enpr2 
 |-  ( ( K e. D /\ ( K + 1 ) e. D /\ K =/= ( K + 1 ) ) -> { K , ( K + 1 ) } ~~ 2o )
28 22 7 26 27 syl3anc 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> { K , ( K + 1 ) } ~~ 2o )
29 eqid 
 |-  ran T = ran T
30 2 29 pmtrrn 
 |-  ( ( D e. Fin /\ { K , ( K + 1 ) } C_ D /\ { K , ( K + 1 ) } ~~ 2o ) -> ( T ` { K , ( K + 1 ) } ) e. ran T )
31 5 24 28 30 syl3anc 
 |-  ( ( K e. NN /\ ( K + 1 ) e. D ) -> ( T ` { K , ( K + 1 ) } ) e. ran T )