---

Step * 1 3 of Lemma prior-or-latest


1. Info : Type
2. A : Type
3. B : Type
4. X : EClass(A)
5. Y : EClass(B)
6. Singlevalued(X)
7. Singlevalued(Y)
8. ∀es:EO+(Info). ∀e:E.  (↑e ∈b ((X |- Y))' ⇐⇒ ↑e ∈b ((X)' | (Y)'))
9. es : EO+(Info)@i'
10. e : E@i
11. ↑e ∈b ((X |- Y))'@i
12. ↑e ∈b ((X)' | (Y)')@i
⊢ ((X |- Y))'(e) = ((X)' | (Y)')(e) ∈ one_or_both(A;B)
BY
{ ((FHyp (-5) [-1] THENA Auto)
   THEN (FLemma `prior-val-val` [-3] THENA Auto)
        THEN (ExRepD THEN (HypSubst' -1 0 THENA Auto))
   )⋅ }

1
1. Info : Type
2. A : Type
3. B : Type
4. X : EClass(A)
5. Y : EClass(B)
6. Singlevalued(X)
7. Singlevalued(Y)
8. ∀es:EO+(Info). ∀e:E.  (↑e ∈b ((X |- Y))' ⇐⇒ ↑e ∈b ((X)' | (Y)'))
9. es : EO+(Info)@i'
10. e : E@i
11. ↑e ∈b ((X |- Y))'@i
12. ↑e ∈b ((X)' | (Y)')@i
13. ↑e ∈b ((X |- Y))'
14. e' : E
15. (e' <loc e)
16. ↑e' ∈b (X |- Y)
17. ∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑e'' ∈b (X |- Y)))
18. ((X |- Y))'(e) = (X |- Y)(e') ∈ one_or_both(A;B)
⊢ (X |- Y)(e') = ((X)' | (Y)')(e) ∈ one_or_both(A;B)

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  X  :  EClass(A)
5.  Y  :  EClass(B)
6.  Singlevalued(X)
7.  Singlevalued(Y)
8.  \mforall{}es:EO+(Info).  \mforall{}e:E.    (\muparrow{}e  \mmember{}\msubb{}  ((X  |\msupminus{}  Y))'  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}e  \mmember{}\msubb{}  ((X)'  |  (Y)'))
9.  es  :  EO+(Info)@i'
10.  e  :  E@i
11.  \muparrow{}e  \mmember{}\msubb{}  ((X  |\msupminus{}  Y))'@i
12.  \muparrow{}e  \mmember{}\msubb{}  ((X)'  |  (Y)')@i
\mvdash{}  ((X  |\msupminus{}  Y))'(e)  =  ((X)'  |  (Y)')(e)


By

---

Latex:
((FHyp  (-5)  [-1]  THENA  Auto)
  THEN  (FLemma  `prior-val-val`  [-3]  THENA  Auto)
            THEN  (ExRepD  THEN  (HypSubst'  -1  0  THENA  Auto))
  )\mcdot{}

---

Home Index