---

Step * 1 1 1 of Lemma permutation-generators4

.....equality..... 
1. n : ℕ
2. P : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⟶ ℙ
3. P[λx.x]
4. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ∀j:ℕ+n.  (P[f] ⇒ P[f o (0, j)])
5. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
6. (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ∀i,j:ℕn.  P[f] ⇒ P[f o (i, j)] supposing i < j)
⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . P[f])
7. f1 : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
8. i : ℕn
9. j : ℕn
10. i < j
11. P[f1]
12. ¬(i = 0 ∈ ℤ)
13. ¬(j = 0 ∈ ℤ)
⊢ (f1 o (i, j)) = (((f1 o (0, i)) o (0, j)) o (0, i)) ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
BY
{ (EqTypeCD THENA EAuto 1) }

1
1. n : ℕ
2. P : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⟶ ℙ
3. P[λx.x]
4. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ∀j:ℕ+n.  (P[f] ⇒ P[f o (0, j)])
5. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
6. (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ∀i,j:ℕn.  P[f] ⇒ P[f o (i, j)] supposing i < j)
⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . P[f])
7. f1 : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
8. i : ℕn
9. j : ℕn
10. i < j
11. P[f1]
12. ¬(i = 0 ∈ ℤ)
13. ¬(j = 0 ∈ ℤ)
⊢ (f1 o (i, j)) = (((f1 o (0, i)) o (0, j)) o (0, i)) ∈ (ℕn ⟶ ℕn)

---

Latex:

---

Latex:
.....equality..... 
1.  n  :  \mBbbN{}
2.  P  :  \{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}    {}\mrightarrow{}  \mBbbP{}
3.  P[\mlambda{}x.x]
4.  \mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .  \mforall{}j:\mBbbN{}\msupplus{}n.    (P[f]  {}\mRightarrow{}  P[f  o  (0,  j)])
5.  f  :  \{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\} 
6.  (\mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .  \mforall{}i,j:\mBbbN{}n.    P[f]  {}\mRightarrow{}  P[f  o  (i,  j)]  supposing  i  <  j)
{}\mRightarrow{}  (\mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\}  .  P[f])
7.  f1  :  \{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\} 
8.  i  :  \mBbbN{}n
9.  j  :  \mBbbN{}n
10.  i  <  j
11.  P[f1]
12.  \mneg{}(i  =  0)
13.  \mneg{}(j  =  0)
\mvdash{}  (f1  o  (i,  j))  =  (((f1  o  (0,  i))  o  (0,  j))  o  (0,  i))


By

---

Latex:
(EqTypeCD  THENA  EAuto  1)

---

Home Index