Step * of Lemma pairwise-iff

No Annotations
[T:Type]
  ∀L:T List
    ∀[P:T ⟶ T ⟶ ℙ']
      ((∀x,y:T.  (P[x;y]  P[y;x]))
       (∀x:T. P[x;x])
       ((∀x,y∈L.  P[x;y]) ⇐⇒ ∀x,y:T.  ((x ∈ L)  (y ∈ L)  P[x;y])))
BY
Auto }

1
1. [T] Type
2. List
3. [P] T ⟶ T ⟶ ℙ'
4. ∀x,y:T.  (P[x;y]  P[y;x])
5. ∀x:T. P[x;x]
6. (∀x,y∈L.  P[x;y])
7. T
8. T
9. (x ∈ L)
10. (y ∈ L)
⊢ P[x;y]

2
1. [T] Type
2. List
3. [P] T ⟶ T ⟶ ℙ'
4. ∀x,y:T.  (P[x;y]  P[y;x])
5. ∀x:T. P[x;x]
6. ∀x,y:T.  ((x ∈ L)  (y ∈ L)  P[x;y])
⊢ (∀x,y∈L.  P[x;y])


Latex:


Latex:
No  Annotations
\mforall{}[T:Type]
    \mforall{}L:T  List
        \mforall{}[P:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}']
            ((\mforall{}x,y:T.    (P[x;y]  {}\mRightarrow{}  P[y;x]))
            {}\mRightarrow{}  (\mforall{}x:T.  P[x;x])
            {}\mRightarrow{}  ((\mforall{}x,y\mmember{}L.    P[x;y])  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x,y:T.    ((x  \mmember{}  L)  {}\mRightarrow{}  (y  \mmember{}  L)  {}\mRightarrow{}  P[x;y])))


By


Latex:
Auto




Home Index