---

Step * 1 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)'))
⊢ ((X |- Y))' = ((X)' | (Y)') ∈ EClass(one_or_both(A;B))
BY
{ (BLemma `es-interface-extensionality`⋅ THEN 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)'))
⊢ Singlevalued(((X)' | (Y)'))

2
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)'))
⊢ Singlevalued(((X |- Y))')

3
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)

---

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)'))
\mvdash{}  ((X  |\msupminus{}  Y))'  =  ((X)'  |  (Y)')


By

---

Latex:
(BLemma  `es-interface-extensionality`\mcdot{}  THEN  Auto)

---

Home Index