Metamath Proof Explorer

Theorem pmtrto1cl

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

Ref Expression
Hypotheses psgnfzto1st.d ⊢ 𝐷 = ( 1 ... 𝑁 )
pmtrto1cl.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
Assertion pmtrto1cl ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → ( 𝑇 ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ∈ ran 𝑇 )

Proof

Step Hyp Ref Expression
1 psgnfzto1st.d ⊢ 𝐷 = ( 1 ... 𝑁 )
2 pmtrto1cl.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
3 fzfi ⊢ ( 1 ... 𝑁 ) ∈ Fin
4 1 3 eqeltri ⊢ 𝐷 ∈ Fin
5 4 a1i ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → 𝐷 ∈ Fin )
6 simpl ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → 𝐾 ∈ ℕ )
7 simpr ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → ( 𝐾 + 1 ) ∈ 𝐷 )
8 7 1 eleqtrdi ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → ( 𝐾 + 1 ) ∈ ( 1 ... 𝑁 ) )
9 elfz1b ⊢ ( ( 𝐾 + 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝐾 + 1 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝐾 + 1 ) ≤ 𝑁 ) )
10 8 9 sylib ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → ( ( 𝐾 + 1 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝐾 + 1 ) ≤ 𝑁 ) )
11 10 simp2d ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → 𝑁 ∈ ℕ )
12 6 nnred ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → 𝐾 ∈ ℝ )
13 1red ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → 1 ∈ ℝ )
14 12 13 readdcld ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → ( 𝐾 + 1 ) ∈ ℝ )
15 11 nnred ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → 𝑁 ∈ ℝ )
16 12 lep1d ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → 𝐾 ≤ ( 𝐾 + 1 ) )
17 10 simp3d ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → ( 𝐾 + 1 ) ≤ 𝑁 )
18 12 14 15 16 17 letrd ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → 𝐾 ≤ 𝑁 )
19 6 11 18 3jca ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → ( 𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ≤ 𝑁 ) )
20 elfz1b ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) ↔ ( 𝐾 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ≤ 𝑁 ) )
21 19 20 sylibr ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → 𝐾 ∈ ( 1 ... 𝑁 ) )
22 21 1 eleqtrrdi ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → 𝐾 ∈ 𝐷 )
23 prssi ⊢ ( ( 𝐾 ∈ 𝐷 ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → { 𝐾 , ( 𝐾 + 1 ) } ⊆ 𝐷 )
24 22 7 23 syl2anc ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → { 𝐾 , ( 𝐾 + 1 ) } ⊆ 𝐷 )
25 12 ltp1d ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → 𝐾 < ( 𝐾 + 1 ) )
26 12 25 ltned ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → 𝐾 ≠ ( 𝐾 + 1 ) )
27 pr2nelem ⊢ ( ( 𝐾 ∈ 𝐷 ∧ ( 𝐾 + 1 ) ∈ 𝐷 ∧ 𝐾 ≠ ( 𝐾 + 1 ) ) → { 𝐾 , ( 𝐾 + 1 ) } ≈ 2o )
28 22 7 26 27 syl3anc ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → { 𝐾 , ( 𝐾 + 1 ) } ≈ 2o )
29 eqid ⊢ ran 𝑇 = ran 𝑇
30 2 29 pmtrrn ⊢ ( ( 𝐷 ∈ Fin ∧ { 𝐾 , ( 𝐾 + 1 ) } ⊆ 𝐷 ∧ { 𝐾 , ( 𝐾 + 1 ) } ≈ 2o ) → ( 𝑇 ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ∈ ran 𝑇 )
31 5 24 28 30 syl3anc ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → ( 𝑇 ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ∈ ran 𝑇 )