---

Step * 1 1 1 1 of Lemma pairwise-mapl


1. [T] : Type
2. [T'] : Type
3. u : T@i
4. v : T List@i
5. ∀f:{x:T| (x ∈ v)}  ⟶ T'
     ∀[P:T' ⟶ T' ⟶ ℙ']. ((∀x,y:T.  ((x ∈ v) ⇒ (y ∈ v) ⇒ P[f x;f y])) ⇒ (∀x,y∈mapl(f;v).  P[x;y]))
6. f : {x:T| (x ∈ [u / v])}  ⟶ T'@i
7. [P] : T' ⟶ T' ⟶ ℙ'
8. ∀x,y:T.  ((x ∈ [u / v]) ⇒ (y ∈ [u / v]) ⇒ P[f x;f y])
9. f ∈ {x:T| (x ∈ v)}  ⟶ T'
10. (∀x,y∈mapl(f;v).  P[x;y])
11. z : T'@i
12. (f u) = z ∈ T'
13. ∀y:T. ((y ∈ v) ⇒ P[z;f y])
⊢ (∀y∈mapl(f;v).P[z;y])
BY
{ (InstLemma `l_all_iff` [⌜parm{i'}⌝]⋅ THEN (BHyp -1 THENA Auto) THEN Thin (-1) THEN Auto) }

1
1. [T] : Type
2. [T'] : Type
3. u : T@i
4. v : T List@i
5. ∀f:{x:T| (x ∈ v)}  ⟶ T'
     ∀[P:T' ⟶ T' ⟶ ℙ']. ((∀x,y:T.  ((x ∈ v) ⇒ (y ∈ v) ⇒ P[f x;f y])) ⇒ (∀x,y∈mapl(f;v).  P[x;y]))
6. f : {x:T| (x ∈ [u / v])}  ⟶ T'@i
7. [P] : T' ⟶ T' ⟶ ℙ'
8. ∀x,y:T.  ((x ∈ [u / v]) ⇒ (y ∈ [u / v]) ⇒ P[f x;f y])
9. f ∈ {x:T| (x ∈ v)}  ⟶ T'
10. (∀x,y∈mapl(f;v).  P[x;y])
11. z : T'@i
12. (f u) = z ∈ T'
13. ∀y:T. ((y ∈ v) ⇒ P[z;f y])
14. y : T'
15. (y ∈ mapl(f;v))
⊢ P[z;y]

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [T']  :  Type
3.  u  :  T@i
4.  v  :  T  List@i
5.  \mforall{}f:\{x:T|  (x  \mmember{}  v)\}    {}\mrightarrow{}  T'
          \mforall{}[P:T'  {}\mrightarrow{}  T'  {}\mrightarrow{}  \mBbbP{}']
              ((\mforall{}x,y:T.    ((x  \mmember{}  v)  {}\mRightarrow{}  (y  \mmember{}  v)  {}\mRightarrow{}  P[f  x;f  y]))  {}\mRightarrow{}  (\mforall{}x,y\mmember{}mapl(f;v).    P[x;y]))
6.  f  :  \{x:T|  (x  \mmember{}  [u  /  v])\}    {}\mrightarrow{}  T'@i
7.  [P]  :  T'  {}\mrightarrow{}  T'  {}\mrightarrow{}  \mBbbP{}'
8.  \mforall{}x,y:T.    ((x  \mmember{}  [u  /  v])  {}\mRightarrow{}  (y  \mmember{}  [u  /  v])  {}\mRightarrow{}  P[f  x;f  y])
9.  f  \mmember{}  \{x:T|  (x  \mmember{}  v)\}    {}\mrightarrow{}  T'
10.  (\mforall{}x,y\mmember{}mapl(f;v).    P[x;y])
11.  z  :  T'@i
12.  (f  u)  =  z
13.  \mforall{}y:T.  ((y  \mmember{}  v)  {}\mRightarrow{}  P[z;f  y])
\mvdash{}  (\mforall{}y\mmember{}mapl(f;v).P[z;y])


By

---

Latex:
(InstLemma  `l\_all\_iff`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{}]\mcdot{}  THEN  (BHyp  -1  THENA  Auto)  THEN  Thin  (-1)  THEN  Auto)

---

Home Index