---

Step * 1 1 of Lemma goes-thru-goes-thru-last


1. [Info] : Type
2. es : EO+(Info)@i'
3. Sys : EClass(Top)@i'
4. f : sys-antecedent(es;Sys)@i
5. x : E(Sys)@i
6. y : E(Sys)@i
7. i : Id@i
8. ¬(loc(x) = i ∈ Id)
9. e : E(Sys)@i
10. loc(e) = i ∈ Id@i
11. e is f*(y)@i
12. x is f*(e)@i
⊢ ∃e:E(Sys). (((loc(e) = i ∈ Id) ∧ (¬(loc(f e) = loc(e) ∈ Id))) ∧ e is f*(y) ∧ x is f*(e))
BY
{ (FLemma `chain-pullback` [-1] THEN Auto) }

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  Sys  :  EClass(Top)@i'
4.  f  :  sys-antecedent(es;Sys)@i
5.  x  :  E(Sys)@i
6.  y  :  E(Sys)@i
7.  i  :  Id@i
8.  \mneg{}(loc(x)  =  i)
9.  e  :  E(Sys)@i
10.  loc(e)  =  i@i
11.  e  is  f*(y)@i
12.  x  is  f*(e)@i
\mvdash{}  \mexists{}e:E(Sys).  (((loc(e)  =  i)  \mwedge{}  (\mneg{}(loc(f  e)  =  loc(e))))  \mwedge{}  e  is  f*(y)  \mwedge{}  x  is  f*(e))


By

---

Latex:
(FLemma  `chain-pullback`  [-1]  THEN  Auto)

---

Home Index