---

Step * 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. AntiSym({e:E| loc(e) = j ∈ Id} ;a,b.a ≤loc b )
⊢ AntiSym({e':E(X)| loc(e') = j ∈ Id} ;a,b.a ≤loc b )
BY
{ RepeatFor 5 (ParallelLast⋅) }

1
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} 

---

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.  AntiSym(\{e:E|  loc(e)  =  j\}  ;a,b.a  \mleq{}loc  b  )
\mvdash{}  AntiSym(\{e':E(X)|  loc(e')  =  j\}  ;a,b.a  \mleq{}loc  b  )


By

RepeatFor  5  (ParallelLast\mcdot{})

---

Home Index