---

Step * 1 of Lemma no_repeats-length-equal-by-relation

.....antecedent..... 
1. A : Type
2. B : Type
3. as : A List
4. bs : B List
5. no_repeats(B;bs)
6. no_repeats(A;as)
7. ∃R:A ⟶ B ⟶ ℙ
    ((∀a1,a2:A. ∀b:B.  ((a1 ∈ as) ⇒ (a2 ∈ as) ⇒ (b ∈ bs) ⇒ (R a1 b) ⇒ (R a2 b) ⇒ (a1 = a2 ∈ A)))
    ∧ (∀b1,b2:B. ∀a:A.  ((b1 ∈ bs) ⇒ (b2 ∈ bs) ⇒ (a ∈ as) ⇒ (R a b1) ⇒ (R a b2) ⇒ (b1 = b2 ∈ B)))
    ∧ (∀a∈as.(∃b∈bs. R a b))
    ∧ (∀b∈bs.(∃a∈as. R a b)))
⊢ ∃R:A ⟶ B ⟶ ℙ
   ((∀a1,a2:A. ∀b:B.  ((R a1 b) ⇒ (R a2 b) ⇒ (a1 = a2 ∈ A)))
   ∧ (∀b1,b2:B. ∀a:A.  ((R a b1) ⇒ (R a b2) ⇒ (b1 = b2 ∈ B)))
   ∧ (∀a∈as.(∃b∈bs. R a b))
   ∧ (∀b∈bs.(∃a∈as. R a b)))
BY
{ ((ExRepD THEN D 0 With ⌜λa,b. (((a ∈ as) ∧ (b ∈ bs)) ∧ (R a b))⌝ )
   THEN Reduce 0
   THEN Auto
   THEN RepeatFor 2 (ParallelOp -4)
   THEN RepeatFor 2 (ParallelLast)
   THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  A  :  Type
2.  B  :  Type
3.  as  :  A  List
4.  bs  :  B  List
5.  no\_repeats(B;bs)
6.  no\_repeats(A;as)
7.  \mexists{}R:A  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}
        ((\mforall{}a1,a2:A.  \mforall{}b:B.    ((a1  \mmember{}  as)  {}\mRightarrow{}  (a2  \mmember{}  as)  {}\mRightarrow{}  (b  \mmember{}  bs)  {}\mRightarrow{}  (R  a1  b)  {}\mRightarrow{}  (R  a2  b)  {}\mRightarrow{}  (a1  =  a2)))
        \mwedge{}  (\mforall{}b1,b2:B.  \mforall{}a:A.    ((b1  \mmember{}  bs)  {}\mRightarrow{}  (b2  \mmember{}  bs)  {}\mRightarrow{}  (a  \mmember{}  as)  {}\mRightarrow{}  (R  a  b1)  {}\mRightarrow{}  (R  a  b2)  {}\mRightarrow{}  (b1  =  b2)))
        \mwedge{}  (\mforall{}a\mmember{}as.(\mexists{}b\mmember{}bs.  R  a  b))
        \mwedge{}  (\mforall{}b\mmember{}bs.(\mexists{}a\mmember{}as.  R  a  b)))
\mvdash{}  \mexists{}R:A  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}
      ((\mforall{}a1,a2:A.  \mforall{}b:B.    ((R  a1  b)  {}\mRightarrow{}  (R  a2  b)  {}\mRightarrow{}  (a1  =  a2)))
      \mwedge{}  (\mforall{}b1,b2:B.  \mforall{}a:A.    ((R  a  b1)  {}\mRightarrow{}  (R  a  b2)  {}\mRightarrow{}  (b1  =  b2)))
      \mwedge{}  (\mforall{}a\mmember{}as.(\mexists{}b\mmember{}bs.  R  a  b))
      \mwedge{}  (\mforall{}b\mmember{}bs.(\mexists{}a\mmember{}as.  R  a  b)))


By

---

Latex:
((ExRepD  THEN  D  0  With  \mkleeneopen{}\mlambda{}a,b.  (((a  \mmember{}  as)  \mwedge{}  (b  \mmember{}  bs))  \mwedge{}  (R  a  b))\mkleeneclose{}  )
  THEN  Reduce  0
  THEN  Auto
  THEN  RepeatFor  2  (ParallelOp  -4)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  Auto)

---

Home Index