Metamath Proof Explorer

Theorem psgnfzto1stlem

Description: Lemma for psgnfzto1st . Our permutation of rank ( n + 1 ) can be written as a permutation of rank n composed with a transposition. (Contributed by Thierry Arnoux, 21-Aug-2020)

Ref Expression
Hypothesis psgnfzto1st.d ⊢ 𝐷 = ( 1 ... 𝑁 )
Assertion psgnfzto1stlem ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , ( 𝐾 + 1 ) , if ( 𝑖 ≤ ( 𝐾 + 1 ) , ( 𝑖 − 1 ) , 𝑖 ) ) ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ∘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 psgnfzto1st.d ⊢ 𝐷 = ( 1 ... 𝑁 )
2 ovex ⊢ ( 𝐾 + 1 ) ∈ V
3 ovex ⊢ ( 𝑖 − 1 ) ∈ V
4 vex ⊢ 𝑖 ∈ V
5 3 4 ifex ⊢ if ( 𝑖 ≤ ( 𝐾 + 1 ) , ( 𝑖 − 1 ) , 𝑖 ) ∈ V
6 2 5 ifex ⊢ if ( 𝑖 = 1 , ( 𝐾 + 1 ) , if ( 𝑖 ≤ ( 𝐾 + 1 ) , ( 𝑖 − 1 ) , 𝑖 ) ) ∈ V
7 eqid ⊢ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , ( 𝐾 + 1 ) , if ( 𝑖 ≤ ( 𝐾 + 1 ) , ( 𝑖 − 1 ) , 𝑖 ) ) ) = ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , ( 𝐾 + 1 ) , if ( 𝑖 ≤ ( 𝐾 + 1 ) , ( 𝑖 − 1 ) , 𝑖 ) ) )
8 6 7 fnmpti ⊢ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , ( 𝐾 + 1 ) , if ( 𝑖 ≤ ( 𝐾 + 1 ) , ( 𝑖 − 1 ) , 𝑖 ) ) ) Fn 𝐷
9 8 a1i ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , ( 𝐾 + 1 ) , if ( 𝑖 ≤ ( 𝐾 + 1 ) , ( 𝑖 − 1 ) , 𝑖 ) ) ) Fn 𝐷 )
10 eqid ⊢ ( pmTrsp ‘ 𝐷 ) = ( pmTrsp ‘ 𝐷 )
11 1 10 pmtrto1cl ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ∈ ran ( pmTrsp ‘ 𝐷 ) )
12 eqid ⊢ ran ( pmTrsp ‘ 𝐷 ) = ran ( pmTrsp ‘ 𝐷 )
13 10 12 pmtrff1o ⊢ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ∈ ran ( pmTrsp ‘ 𝐷 ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) : 𝐷 –1-1-onto→ 𝐷 )
14 f1ofn ⊢ ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) : 𝐷 –1-1-onto→ 𝐷 → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) Fn 𝐷 )
15 11 13 14 3syl ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) Fn 𝐷 )
16 simpr ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ 𝑖 = 1 ) → 𝑖 = 1 )
17 16 iftrued ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ 𝑖 = 1 ) → if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) = 𝐾 )
18 simpl ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → 𝐾 ∈ ℕ )
19 18 nnred ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → 𝐾 ∈ ℝ )
20 fz1ssnn ⊢ ( 1 ... 𝑁 ) ⊆ ℕ
21 1 eleq2i ⊢ ( ( 𝐾 + 1 ) ∈ 𝐷 ↔ ( 𝐾 + 1 ) ∈ ( 1 ... 𝑁 ) )
22 21 biimpi ⊢ ( ( 𝐾 + 1 ) ∈ 𝐷 → ( 𝐾 + 1 ) ∈ ( 1 ... 𝑁 ) )
23 22 adantl ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → ( 𝐾 + 1 ) ∈ ( 1 ... 𝑁 ) )
24 20 23 sselid ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → ( 𝐾 + 1 ) ∈ ℕ )
25 24 nnred ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → ( 𝐾 + 1 ) ∈ ℝ )
26 elfz1b ⊢ ( ( 𝐾 + 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝐾 + 1 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝐾 + 1 ) ≤ 𝑁 ) )
27 26 simp2bi ⊢ ( ( 𝐾 + 1 ) ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ℕ )
28 22 27 syl ⊢ ( ( 𝐾 + 1 ) ∈ 𝐷 → 𝑁 ∈ ℕ )
29 28 adantl ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → 𝑁 ∈ ℕ )
30 29 nnred ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → 𝑁 ∈ ℝ )
31 19 lep1d ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → 𝐾 ≤ ( 𝐾 + 1 ) )
32 elfzle2 ⊢ ( ( 𝐾 + 1 ) ∈ ( 1 ... 𝑁 ) → ( 𝐾 + 1 ) ≤ 𝑁 )
33 23 32 syl ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → ( 𝐾 + 1 ) ≤ 𝑁 )
34 19 25 30 31 33 letrd ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → 𝐾 ≤ 𝑁 )
35 29 nnzd ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → 𝑁 ∈ ℤ )
36 fznn ⊢ ( 𝑁 ∈ ℤ → ( 𝐾 ∈ ( 1 ... 𝑁 ) ↔ ( 𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁 ) ) )
37 35 36 syl ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → ( 𝐾 ∈ ( 1 ... 𝑁 ) ↔ ( 𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁 ) ) )
38 18 34 37 mpbir2and ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → 𝐾 ∈ ( 1 ... 𝑁 ) )
39 38 1 eleqtrrdi ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → 𝐾 ∈ 𝐷 )
40 39 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ 𝑖 = 1 ) → 𝐾 ∈ 𝐷 )
41 17 40 eqeltrd ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ 𝑖 = 1 ) → if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ∈ 𝐷 )
42 simpr ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) → ¬ 𝑖 = 1 )
43 42 iffalsed ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) → if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) = if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) )
44 simpr ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐾 ) → 𝑖 ≤ 𝐾 )
45 44 iftrued ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐾 ) → if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) = ( 𝑖 − 1 ) )
46 42 adantr ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐾 ) → ¬ 𝑖 = 1 )
47 1 20 eqsstri ⊢ 𝐷 ⊆ ℕ
48 simpllr ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐾 ) → 𝑖 ∈ 𝐷 )
49 47 48 sselid ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐾 ) → 𝑖 ∈ ℕ )
50 nn1m1nn ⊢ ( 𝑖 ∈ ℕ → ( 𝑖 = 1 ∨ ( 𝑖 − 1 ) ∈ ℕ ) )
51 49 50 syl ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐾 ) → ( 𝑖 = 1 ∨ ( 𝑖 − 1 ) ∈ ℕ ) )
52 51 ord ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐾 ) → ( ¬ 𝑖 = 1 → ( 𝑖 − 1 ) ∈ ℕ ) )
53 46 52 mpd ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐾 ) → ( 𝑖 − 1 ) ∈ ℕ )
54 53 nnred ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐾 ) → ( 𝑖 − 1 ) ∈ ℝ )
55 49 nnred ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐾 ) → 𝑖 ∈ ℝ )
56 30 ad3antrrr ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐾 ) → 𝑁 ∈ ℝ )
57 55 lem1d ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐾 ) → ( 𝑖 − 1 ) ≤ 𝑖 )
58 48 1 eleqtrdi ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐾 ) → 𝑖 ∈ ( 1 ... 𝑁 ) )
59 elfzle2 ⊢ ( 𝑖 ∈ ( 1 ... 𝑁 ) → 𝑖 ≤ 𝑁 )
60 58 59 syl ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐾 ) → 𝑖 ≤ 𝑁 )
61 54 55 56 57 60 letrd ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐾 ) → ( 𝑖 − 1 ) ≤ 𝑁 )
62 53 61 jca ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐾 ) → ( ( 𝑖 − 1 ) ∈ ℕ ∧ ( 𝑖 − 1 ) ≤ 𝑁 ) )
63 fznn ⊢ ( 𝑁 ∈ ℤ → ( ( 𝑖 − 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝑖 − 1 ) ∈ ℕ ∧ ( 𝑖 − 1 ) ≤ 𝑁 ) ) )
64 35 63 syl ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → ( ( 𝑖 − 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝑖 − 1 ) ∈ ℕ ∧ ( 𝑖 − 1 ) ≤ 𝑁 ) ) )
65 64 ad3antrrr ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐾 ) → ( ( 𝑖 − 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝑖 − 1 ) ∈ ℕ ∧ ( 𝑖 − 1 ) ≤ 𝑁 ) ) )
66 62 65 mpbird ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐾 ) → ( 𝑖 − 1 ) ∈ ( 1 ... 𝑁 ) )
67 66 1 eleqtrrdi ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐾 ) → ( 𝑖 − 1 ) ∈ 𝐷 )
68 45 67 eqeltrd ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ 𝑖 ≤ 𝐾 ) → if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ∈ 𝐷 )
69 simpr ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ ¬ 𝑖 ≤ 𝐾 ) → ¬ 𝑖 ≤ 𝐾 )
70 69 iffalsed ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ ¬ 𝑖 ≤ 𝐾 ) → if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) = 𝑖 )
71 simpllr ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ ¬ 𝑖 ≤ 𝐾 ) → 𝑖 ∈ 𝐷 )
72 70 71 eqeltrd ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) ∧ ¬ 𝑖 ≤ 𝐾 ) → if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ∈ 𝐷 )
73 68 72 pm2.61dan ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) → if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ∈ 𝐷 )
74 43 73 eqeltrd ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) ∧ ¬ 𝑖 = 1 ) → if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ∈ 𝐷 )
75 41 74 pm2.61dan ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑖 ∈ 𝐷 ) → if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ∈ 𝐷 )
76 75 ralrimiva ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → ∀ 𝑖 ∈ 𝐷 if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ∈ 𝐷 )
77 eqid ⊢ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) = ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) )
78 77 fnmpt ⊢ ( ∀ 𝑖 ∈ 𝐷 if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ∈ 𝐷 → ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) Fn 𝐷 )
79 76 78 syl ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) Fn 𝐷 )
80 77 rnmptss ⊢ ( ∀ 𝑖 ∈ 𝐷 if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ∈ 𝐷 → ran ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ⊆ 𝐷 )
81 76 80 syl ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → ran ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ⊆ 𝐷 )
82 fnco ⊢ ( ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) Fn 𝐷 ∧ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) Fn 𝐷 ∧ ran ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ⊆ 𝐷 ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ∘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) Fn 𝐷 )
83 15 79 81 82 syl3anc ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ∘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) Fn 𝐷 )
84 simpr ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 = 1 ) → 𝑥 = 1 )
85 84 iftrued ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 = 1 ) → if ( 𝑥 = 1 , 𝐾 , if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) ) = 𝐾 )
86 85 fveq2d ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 = 1 ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ if ( 𝑥 = 1 , 𝐾 , if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) ) ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ 𝐾 ) )
87 fzfi ⊢ ( 1 ... 𝑁 ) ∈ Fin
88 1 87 eqeltri ⊢ 𝐷 ∈ Fin
89 88 a1i ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → 𝐷 ∈ Fin )
90 23 21 sylibr ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → ( 𝐾 + 1 ) ∈ 𝐷 )
91 19 ltp1d ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → 𝐾 < ( 𝐾 + 1 ) )
92 19 91 ltned ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → 𝐾 ≠ ( 𝐾 + 1 ) )
93 10 pmtrprfv ⊢ ( ( 𝐷 ∈ Fin ∧ ( 𝐾 ∈ 𝐷 ∧ ( 𝐾 + 1 ) ∈ 𝐷 ∧ 𝐾 ≠ ( 𝐾 + 1 ) ) ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ 𝐾 ) = ( 𝐾 + 1 ) )
94 89 39 90 92 93 syl13anc ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ 𝐾 ) = ( 𝐾 + 1 ) )
95 94 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 = 1 ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ 𝐾 ) = ( 𝐾 + 1 ) )
96 86 95 eqtr2d ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑥 = 1 ) → ( 𝐾 + 1 ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ if ( 𝑥 = 1 , 𝐾 , if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) ) ) )
97 88 a1i ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 = ( 𝐾 + 1 ) ) → 𝐷 ∈ Fin )
98 39 ad4antr ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 = ( 𝐾 + 1 ) ) → 𝐾 ∈ 𝐷 )
99 90 ad4antr ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 = ( 𝐾 + 1 ) ) → ( 𝐾 + 1 ) ∈ 𝐷 )
100 92 ad4antr ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 = ( 𝐾 + 1 ) ) → 𝐾 ≠ ( 𝐾 + 1 ) )
101 10 pmtrprfv2 ⊢ ( ( 𝐷 ∈ Fin ∧ ( 𝐾 ∈ 𝐷 ∧ ( 𝐾 + 1 ) ∈ 𝐷 ∧ 𝐾 ≠ ( 𝐾 + 1 ) ) ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ ( 𝐾 + 1 ) ) = 𝐾 )
102 97 98 99 100 101 syl13anc ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 = ( 𝐾 + 1 ) ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ ( 𝐾 + 1 ) ) = 𝐾 )
103 91 ad4antr ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 = ( 𝐾 + 1 ) ) → 𝐾 < ( 𝐾 + 1 ) )
104 simpr ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 = ( 𝐾 + 1 ) ) → 𝑥 = ( 𝐾 + 1 ) )
105 103 104 breqtrrd ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 = ( 𝐾 + 1 ) ) → 𝐾 < 𝑥 )
106 19 ad4antr ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 = ( 𝐾 + 1 ) ) → 𝐾 ∈ ℝ )
107 simpr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ 𝐷 )
108 47 107 sselid ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ ℕ )
109 108 nnred ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ ℝ )
110 109 ad3antrrr ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 = ( 𝐾 + 1 ) ) → 𝑥 ∈ ℝ )
111 106 110 ltnled ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 = ( 𝐾 + 1 ) ) → ( 𝐾 < 𝑥 ↔ ¬ 𝑥 ≤ 𝐾 ) )
112 105 111 mpbid ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 = ( 𝐾 + 1 ) ) → ¬ 𝑥 ≤ 𝐾 )
113 112 iffalsed ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 = ( 𝐾 + 1 ) ) → if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) = 𝑥 )
114 113 104 eqtrd ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 = ( 𝐾 + 1 ) ) → if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) = ( 𝐾 + 1 ) )
115 114 fveq2d ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 = ( 𝐾 + 1 ) ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ ( 𝐾 + 1 ) ) )
116 104 oveq1d ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 = ( 𝐾 + 1 ) ) → ( 𝑥 − 1 ) = ( ( 𝐾 + 1 ) − 1 ) )
117 106 recnd ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 = ( 𝐾 + 1 ) ) → 𝐾 ∈ ℂ )
118 1cnd ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 = ( 𝐾 + 1 ) ) → 1 ∈ ℂ )
119 117 118 pncand ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 = ( 𝐾 + 1 ) ) → ( ( 𝐾 + 1 ) − 1 ) = 𝐾 )
120 116 119 eqtrd ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 = ( 𝐾 + 1 ) ) → ( 𝑥 − 1 ) = 𝐾 )
121 102 115 120 3eqtr4rd ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 = ( 𝐾 + 1 ) ) → ( 𝑥 − 1 ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) ) )
122 simplr ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → 𝑥 ≤ ( 𝐾 + 1 ) )
123 simpr ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → 𝑥 ≠ ( 𝐾 + 1 ) )
124 123 necomd ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → ( 𝐾 + 1 ) ≠ 𝑥 )
125 109 ad3antrrr ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → 𝑥 ∈ ℝ )
126 25 ad4antr ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → ( 𝐾 + 1 ) ∈ ℝ )
127 125 126 ltlend ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → ( 𝑥 < ( 𝐾 + 1 ) ↔ ( 𝑥 ≤ ( 𝐾 + 1 ) ∧ ( 𝐾 + 1 ) ≠ 𝑥 ) ) )
128 122 124 127 mpbir2and ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → 𝑥 < ( 𝐾 + 1 ) )
129 108 ad3antrrr ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → 𝑥 ∈ ℕ )
130 simpll ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → 𝐾 ∈ ℕ )
131 130 ad3antrrr ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → 𝐾 ∈ ℕ )
132 nnleltp1 ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( 𝑥 ≤ 𝐾 ↔ 𝑥 < ( 𝐾 + 1 ) ) )
133 129 131 132 syl2anc ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → ( 𝑥 ≤ 𝐾 ↔ 𝑥 < ( 𝐾 + 1 ) ) )
134 128 133 mpbird ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → 𝑥 ≤ 𝐾 )
135 134 iftrued ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) = ( 𝑥 − 1 ) )
136 135 fveq2d ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ ( 𝑥 − 1 ) ) )
137 88 a1i ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → 𝐷 ∈ Fin )
138 39 ad4antr ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → 𝐾 ∈ 𝐷 )
139 simp-5r ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → ( 𝐾 + 1 ) ∈ 𝐷 )
140 simpr ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) → ¬ 𝑥 = 1 )
141 140 ad2antrr ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → ¬ 𝑥 = 1 )
142 elnn1uz2 ⊢ ( 𝑥 ∈ ℕ ↔ ( 𝑥 = 1 ∨ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) )
143 129 142 sylib ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → ( 𝑥 = 1 ∨ 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) )
144 143 ord ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → ( ¬ 𝑥 = 1 → 𝑥 ∈ ( ℤ≥ ‘ 2 ) ) )
145 141 144 mpd ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → 𝑥 ∈ ( ℤ≥ ‘ 2 ) )
146 uz2m1nn ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑥 − 1 ) ∈ ℕ )
147 145 146 syl ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → ( 𝑥 − 1 ) ∈ ℕ )
148 139 28 syl ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → 𝑁 ∈ ℕ )
149 147 nnred ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → ( 𝑥 − 1 ) ∈ ℝ )
150 131 139 30 syl2anc ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → 𝑁 ∈ ℝ )
151 125 lem1d ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → ( 𝑥 − 1 ) ≤ 𝑥 )
152 107 ad3antrrr ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → 𝑥 ∈ 𝐷 )
153 152 1 eleqtrdi ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → 𝑥 ∈ ( 1 ... 𝑁 ) )
154 elfzle2 ⊢ ( 𝑥 ∈ ( 1 ... 𝑁 ) → 𝑥 ≤ 𝑁 )
155 153 154 syl ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → 𝑥 ≤ 𝑁 )
156 149 125 150 151 155 letrd ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → ( 𝑥 − 1 ) ≤ 𝑁 )
157 147 148 156 3jca ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → ( ( 𝑥 − 1 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑥 − 1 ) ≤ 𝑁 ) )
158 elfz1b ⊢ ( ( 𝑥 − 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( ( 𝑥 − 1 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ ( 𝑥 − 1 ) ≤ 𝑁 ) )
159 157 158 sylibr ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → ( 𝑥 − 1 ) ∈ ( 1 ... 𝑁 ) )
160 159 1 eleqtrrdi ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → ( 𝑥 − 1 ) ∈ 𝐷 )
161 138 139 160 3jca ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → ( 𝐾 ∈ 𝐷 ∧ ( 𝐾 + 1 ) ∈ 𝐷 ∧ ( 𝑥 − 1 ) ∈ 𝐷 ) )
162 131 139 92 syl2anc ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → 𝐾 ≠ ( 𝐾 + 1 ) )
163 simpr ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝐾 = ( 𝑥 − 1 ) ) → 𝐾 = ( 𝑥 − 1 ) )
164 163 oveq1d ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝐾 = ( 𝑥 − 1 ) ) → ( 𝐾 + 1 ) = ( ( 𝑥 − 1 ) + 1 ) )
165 109 recnd ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ ℂ )
166 165 ad3antrrr ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝐾 = ( 𝑥 − 1 ) ) → 𝑥 ∈ ℂ )
167 1cnd ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝐾 = ( 𝑥 − 1 ) ) → 1 ∈ ℂ )
168 166 167 npcand ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝐾 = ( 𝑥 − 1 ) ) → ( ( 𝑥 − 1 ) + 1 ) = 𝑥 )
169 164 168 eqtr2d ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝐾 = ( 𝑥 − 1 ) ) → 𝑥 = ( 𝐾 + 1 ) )
170 169 ex ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) → ( 𝐾 = ( 𝑥 − 1 ) → 𝑥 = ( 𝐾 + 1 ) ) )
171 170 necon3d ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) → ( 𝑥 ≠ ( 𝐾 + 1 ) → 𝐾 ≠ ( 𝑥 − 1 ) ) )
172 171 imp ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → 𝐾 ≠ ( 𝑥 − 1 ) )
173 149 125 126 151 128 lelttrd ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → ( 𝑥 − 1 ) < ( 𝐾 + 1 ) )
174 149 173 ltned ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → ( 𝑥 − 1 ) ≠ ( 𝐾 + 1 ) )
175 174 necomd ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → ( 𝐾 + 1 ) ≠ ( 𝑥 − 1 ) )
176 162 172 175 3jca ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → ( 𝐾 ≠ ( 𝐾 + 1 ) ∧ 𝐾 ≠ ( 𝑥 − 1 ) ∧ ( 𝐾 + 1 ) ≠ ( 𝑥 − 1 ) ) )
177 10 pmtrprfv3 ⊢ ( ( 𝐷 ∈ Fin ∧ ( 𝐾 ∈ 𝐷 ∧ ( 𝐾 + 1 ) ∈ 𝐷 ∧ ( 𝑥 − 1 ) ∈ 𝐷 ) ∧ ( 𝐾 ≠ ( 𝐾 + 1 ) ∧ 𝐾 ≠ ( 𝑥 − 1 ) ∧ ( 𝐾 + 1 ) ≠ ( 𝑥 − 1 ) ) ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ ( 𝑥 − 1 ) ) = ( 𝑥 − 1 ) )
178 137 161 176 177 syl3anc ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ ( 𝑥 − 1 ) ) = ( 𝑥 − 1 ) )
179 136 178 eqtr2d ⊢ ( ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) ∧ 𝑥 ≠ ( 𝐾 + 1 ) ) → ( 𝑥 − 1 ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) ) )
180 121 179 pm2.61dane ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ ( 𝐾 + 1 ) ) → ( 𝑥 − 1 ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) ) )
181 109 ad2antrr ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ 𝐾 ) → 𝑥 ∈ ℝ )
182 19 ad3antrrr ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ 𝐾 ) → 𝐾 ∈ ℝ )
183 25 ad3antrrr ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ 𝐾 ) → ( 𝐾 + 1 ) ∈ ℝ )
184 simpr ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ 𝐾 ) → 𝑥 ≤ 𝐾 )
185 31 ad3antrrr ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ 𝐾 ) → 𝐾 ≤ ( 𝐾 + 1 ) )
186 181 182 183 184 185 letrd ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ 𝑥 ≤ 𝐾 ) → 𝑥 ≤ ( 𝐾 + 1 ) )
187 186 ex ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) → ( 𝑥 ≤ 𝐾 → 𝑥 ≤ ( 𝐾 + 1 ) ) )
188 187 con3d ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) → ( ¬ 𝑥 ≤ ( 𝐾 + 1 ) → ¬ 𝑥 ≤ 𝐾 ) )
189 188 imp ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ ¬ 𝑥 ≤ ( 𝐾 + 1 ) ) → ¬ 𝑥 ≤ 𝐾 )
190 189 iffalsed ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ ¬ 𝑥 ≤ ( 𝐾 + 1 ) ) → if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) = 𝑥 )
191 190 fveq2d ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ ¬ 𝑥 ≤ ( 𝐾 + 1 ) ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ 𝑥 ) )
192 88 a1i ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ ¬ 𝑥 ≤ ( 𝐾 + 1 ) ) → 𝐷 ∈ Fin )
193 39 ad3antrrr ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ ¬ 𝑥 ≤ ( 𝐾 + 1 ) ) → 𝐾 ∈ 𝐷 )
194 90 ad3antrrr ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ ¬ 𝑥 ≤ ( 𝐾 + 1 ) ) → ( 𝐾 + 1 ) ∈ 𝐷 )
195 107 ad2antrr ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ ¬ 𝑥 ≤ ( 𝐾 + 1 ) ) → 𝑥 ∈ 𝐷 )
196 193 194 195 3jca ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ ¬ 𝑥 ≤ ( 𝐾 + 1 ) ) → ( 𝐾 ∈ 𝐷 ∧ ( 𝐾 + 1 ) ∈ 𝐷 ∧ 𝑥 ∈ 𝐷 ) )
197 92 ad3antrrr ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ ¬ 𝑥 ≤ ( 𝐾 + 1 ) ) → 𝐾 ≠ ( 𝐾 + 1 ) )
198 19 ad3antrrr ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ ¬ 𝑥 ≤ ( 𝐾 + 1 ) ) → 𝐾 ∈ ℝ )
199 25 ad3antrrr ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ ¬ 𝑥 ≤ ( 𝐾 + 1 ) ) → ( 𝐾 + 1 ) ∈ ℝ )
200 109 ad2antrr ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ ¬ 𝑥 ≤ ( 𝐾 + 1 ) ) → 𝑥 ∈ ℝ )
201 91 ad3antrrr ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ ¬ 𝑥 ≤ ( 𝐾 + 1 ) ) → 𝐾 < ( 𝐾 + 1 ) )
202 simpr ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ ¬ 𝑥 ≤ ( 𝐾 + 1 ) ) → ¬ 𝑥 ≤ ( 𝐾 + 1 ) )
203 199 200 ltnled ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ ¬ 𝑥 ≤ ( 𝐾 + 1 ) ) → ( ( 𝐾 + 1 ) < 𝑥 ↔ ¬ 𝑥 ≤ ( 𝐾 + 1 ) ) )
204 202 203 mpbird ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ ¬ 𝑥 ≤ ( 𝐾 + 1 ) ) → ( 𝐾 + 1 ) < 𝑥 )
205 198 199 200 201 204 lttrd ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ ¬ 𝑥 ≤ ( 𝐾 + 1 ) ) → 𝐾 < 𝑥 )
206 198 205 ltned ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ ¬ 𝑥 ≤ ( 𝐾 + 1 ) ) → 𝐾 ≠ 𝑥 )
207 199 204 ltned ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ ¬ 𝑥 ≤ ( 𝐾 + 1 ) ) → ( 𝐾 + 1 ) ≠ 𝑥 )
208 197 206 207 3jca ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ ¬ 𝑥 ≤ ( 𝐾 + 1 ) ) → ( 𝐾 ≠ ( 𝐾 + 1 ) ∧ 𝐾 ≠ 𝑥 ∧ ( 𝐾 + 1 ) ≠ 𝑥 ) )
209 10 pmtrprfv3 ⊢ ( ( 𝐷 ∈ Fin ∧ ( 𝐾 ∈ 𝐷 ∧ ( 𝐾 + 1 ) ∈ 𝐷 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐾 ≠ ( 𝐾 + 1 ) ∧ 𝐾 ≠ 𝑥 ∧ ( 𝐾 + 1 ) ≠ 𝑥 ) ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ 𝑥 ) = 𝑥 )
210 192 196 208 209 syl3anc ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ ¬ 𝑥 ≤ ( 𝐾 + 1 ) ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ 𝑥 ) = 𝑥 )
211 191 210 eqtr2d ⊢ ( ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) ∧ ¬ 𝑥 ≤ ( 𝐾 + 1 ) ) → 𝑥 = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) ) )
212 180 211 ifeqda ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) → if ( 𝑥 ≤ ( 𝐾 + 1 ) , ( 𝑥 − 1 ) , 𝑥 ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) ) )
213 140 iffalsed ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) → if ( 𝑥 = 1 , 𝐾 , if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) ) = if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) )
214 213 fveq2d ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ if ( 𝑥 = 1 , 𝐾 , if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) ) ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) ) )
215 212 214 eqtr4d ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ¬ 𝑥 = 1 ) → if ( 𝑥 ≤ ( 𝐾 + 1 ) , ( 𝑥 − 1 ) , 𝑥 ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ if ( 𝑥 = 1 , 𝐾 , if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) ) ) )
216 96 215 ifeqda ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → if ( 𝑥 = 1 , ( 𝐾 + 1 ) , if ( 𝑥 ≤ ( 𝐾 + 1 ) , ( 𝑥 − 1 ) , 𝑥 ) ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ if ( 𝑥 = 1 , 𝐾 , if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) ) ) )
217 eqidd ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) = ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) )
218 eqeq1 ⊢ ( 𝑖 = 𝑥 → ( 𝑖 = 1 ↔ 𝑥 = 1 ) )
219 breq1 ⊢ ( 𝑖 = 𝑥 → ( 𝑖 ≤ 𝐾 ↔ 𝑥 ≤ 𝐾 ) )
220 oveq1 ⊢ ( 𝑖 = 𝑥 → ( 𝑖 − 1 ) = ( 𝑥 − 1 ) )
221 id ⊢ ( 𝑖 = 𝑥 → 𝑖 = 𝑥 )
222 219 220 221 ifbieq12d ⊢ ( 𝑖 = 𝑥 → if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) = if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) )
223 218 222 ifbieq2d ⊢ ( 𝑖 = 𝑥 → if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) = if ( 𝑥 = 1 , 𝐾 , if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) ) )
224 223 adantl ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) ∧ 𝑖 = 𝑥 ) → if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) = if ( 𝑥 = 1 , 𝐾 , if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) ) )
225 ovex ⊢ ( 𝑥 − 1 ) ∈ V
226 vex ⊢ 𝑥 ∈ V
227 225 226 ifcli ⊢ if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) ∈ V
228 227 a1i ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) ∈ V )
229 130 228 ifexd ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → if ( 𝑥 = 1 , 𝐾 , if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) ) ∈ V )
230 217 224 107 229 fvmptd ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ‘ 𝑥 ) = if ( 𝑥 = 1 , 𝐾 , if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) ) )
231 230 fveq2d ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ ( ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ‘ 𝑥 ) ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ if ( 𝑥 = 1 , 𝐾 , if ( 𝑥 ≤ 𝐾 , ( 𝑥 − 1 ) , 𝑥 ) ) ) )
232 216 231 eqtr4d ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → if ( 𝑥 = 1 , ( 𝐾 + 1 ) , if ( 𝑥 ≤ ( 𝐾 + 1 ) , ( 𝑥 − 1 ) , 𝑥 ) ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ ( ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ‘ 𝑥 ) ) )
233 breq1 ⊢ ( 𝑖 = 𝑥 → ( 𝑖 ≤ ( 𝐾 + 1 ) ↔ 𝑥 ≤ ( 𝐾 + 1 ) ) )
234 233 220 221 ifbieq12d ⊢ ( 𝑖 = 𝑥 → if ( 𝑖 ≤ ( 𝐾 + 1 ) , ( 𝑖 − 1 ) , 𝑖 ) = if ( 𝑥 ≤ ( 𝐾 + 1 ) , ( 𝑥 − 1 ) , 𝑥 ) )
235 218 234 ifbieq2d ⊢ ( 𝑖 = 𝑥 → if ( 𝑖 = 1 , ( 𝐾 + 1 ) , if ( 𝑖 ≤ ( 𝐾 + 1 ) , ( 𝑖 − 1 ) , 𝑖 ) ) = if ( 𝑥 = 1 , ( 𝐾 + 1 ) , if ( 𝑥 ≤ ( 𝐾 + 1 ) , ( 𝑥 − 1 ) , 𝑥 ) ) )
236 225 226 ifex ⊢ if ( 𝑥 ≤ ( 𝐾 + 1 ) , ( 𝑥 − 1 ) , 𝑥 ) ∈ V
237 2 236 ifex ⊢ if ( 𝑥 = 1 , ( 𝐾 + 1 ) , if ( 𝑥 ≤ ( 𝐾 + 1 ) , ( 𝑥 − 1 ) , 𝑥 ) ) ∈ V
238 235 7 237 fvmpt ⊢ ( 𝑥 ∈ 𝐷 → ( ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , ( 𝐾 + 1 ) , if ( 𝑖 ≤ ( 𝐾 + 1 ) , ( 𝑖 − 1 ) , 𝑖 ) ) ) ‘ 𝑥 ) = if ( 𝑥 = 1 , ( 𝐾 + 1 ) , if ( 𝑥 ≤ ( 𝐾 + 1 ) , ( 𝑥 − 1 ) , 𝑥 ) ) )
239 238 adantl ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , ( 𝐾 + 1 ) , if ( 𝑖 ≤ ( 𝐾 + 1 ) , ( 𝑖 − 1 ) , 𝑖 ) ) ) ‘ 𝑥 ) = if ( 𝑥 = 1 , ( 𝐾 + 1 ) , if ( 𝑥 ≤ ( 𝐾 + 1 ) , ( 𝑥 − 1 ) , 𝑥 ) ) )
240 funmpt ⊢ Fun ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) )
241 240 a1i ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → Fun ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) )
242 76 adantr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → ∀ 𝑖 ∈ 𝐷 if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ∈ 𝐷 )
243 dmmptg ⊢ ( ∀ 𝑖 ∈ 𝐷 if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ∈ 𝐷 → dom ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) = 𝐷 )
244 242 243 syl ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → dom ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) = 𝐷 )
245 107 244 eleqtrrd ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ dom ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) )
246 fvco ⊢ ( ( Fun ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ∧ 𝑥 ∈ dom ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) → ( ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ∘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) ‘ 𝑥 ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ ( ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ‘ 𝑥 ) ) )
247 241 245 246 syl2anc ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ∘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) ‘ 𝑥 ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ‘ ( ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ‘ 𝑥 ) ) )
248 232 239 247 3eqtr4d ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , ( 𝐾 + 1 ) , if ( 𝑖 ≤ ( 𝐾 + 1 ) , ( 𝑖 − 1 ) , 𝑖 ) ) ) ‘ 𝑥 ) = ( ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ∘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) ‘ 𝑥 ) )
249 9 83 248 eqfnfvd ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝐾 + 1 ) ∈ 𝐷 ) → ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , ( 𝐾 + 1 ) , if ( 𝑖 ≤ ( 𝐾 + 1 ) , ( 𝑖 − 1 ) , 𝑖 ) ) ) = ( ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝐾 , ( 𝐾 + 1 ) } ) ∘ ( 𝑖 ∈ 𝐷 ↦ if ( 𝑖 = 1 , 𝐾 , if ( 𝑖 ≤ 𝐾 , ( 𝑖 − 1 ) , 𝑖 ) ) ) ) )