---

Step * 1 1 1 1 of Lemma es-le-linorder-interface


1. Info : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. j : Id@i
5. Connex({e:E| loc(e) = j ∈ Id} ;a,b.a ≤loc b )
6. Refl({e:E| loc(e) = j ∈ Id} ;a,b.a ≤loc b )
7. Trans({e:E| loc(e) = j ∈ Id} ;a,b.a ≤loc b )
8. ∀a,b:{e:E| loc(e) = j ∈ Id} .  (a ≤loc b  ⇒ b ≤loc a  ⇒ (a = b ∈ {e:E| loc(e) = j ∈ Id} ))
9. a : {e':E(X)| loc(e') = j ∈ Id} @i
10. ∀b:{e:E| loc(e) = j ∈ Id} . (a ≤loc b  ⇒ b ≤loc a  ⇒ (a = b ∈ {e:E| loc(e) = j ∈ Id} ))
11. b : {e':E(X)| loc(e') = j ∈ Id} @i
12. a ≤loc b @i
13. b ≤loc a @i
14. a = b ∈ {e:E| loc(e) = j ∈ Id} 
⊢ a = b ∈ {e':E(X)| loc(e') = j ∈ Id} 
BY
{ (EqTypeCD THEN Auto) }

---

Latex:



1.  Info  :  Type
2.  es  :  EO+(Info)@i'
3.  X  :  EClass(Top)@i'
4.  j  :  Id@i
5.  Connex(\{e:E|  loc(e)  =  j\}  ;a,b.a  \mleq{}loc  b  )
6.  Refl(\{e:E|  loc(e)  =  j\}  ;a,b.a  \mleq{}loc  b  )
7.  Trans(\{e:E|  loc(e)  =  j\}  ;a,b.a  \mleq{}loc  b  )
8.  \mforall{}a,b:\{e:E|  loc(e)  =  j\}  .    (a  \mleq{}loc  b    {}\mRightarrow{}  b  \mleq{}loc  a    {}\mRightarrow{}  (a  =  b))
9.  a  :  \{e':E(X)|  loc(e')  =  j\}  @i
10.  \mforall{}b:\{e:E|  loc(e)  =  j\}  .  (a  \mleq{}loc  b    {}\mRightarrow{}  b  \mleq{}loc  a    {}\mRightarrow{}  (a  =  b))
11.  b  :  \{e':E(X)|  loc(e')  =  j\}  @i
12.  a  \mleq{}loc  b  @i
13.  b  \mleq{}loc  a  @i
14.  a  =  b
\mvdash{}  a  =  b


By

(EqTypeCD  THEN  Auto)

---

Home Index