---

Step * 1 1 of Lemma Q-R-glued-first


1. [Info] : Type
2. es : EO+(Info)@i'
3. [Q] : E ─→ E ─→ ℙ
4. [R] : E ─→ E ─→ ℙ
5. [A] : Type
6. [B] : Type
7. f : E(first-class([])) ─→ B@i
8. ∀i:ℕ0. ∀j:ℕi.  ⊥ ∩ ⊥ = 0
9. ∀i:ℕ0. ∀j:ℕi.  ⊥ ∩ ⊥ = 0
10. 0 = 0 ∈ ℤ
11. ∀i:ℕ0. ⊥:Q →─f─→  ⊥:R@i
12. ∀i:ℕ0. ∀j:ℕi. ∀e,e':E.  ((¬(Q e e')) ∧ (¬(Q e' e))) supposing ((↑e' ∈b ⊥) and (↑e ∈b ⊥))
⊢ first-class([]):Q →─f─→  first-class([]):R
BY
{ (RepUR ``first-class`` 0 THEN BLemma `Q-R-glued-empty` THEN Auto) }

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  [Q]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
4.  [R]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
5.  [A]  :  Type
6.  [B]  :  Type
7.  f  :  E(first-class([]))  {}\mrightarrow{}  B@i
8.  \mforall{}i:\mBbbN{}0.  \mforall{}j:\mBbbN{}i.    \mbot{}  \mcap{}  \mbot{}  =  0
9.  \mforall{}i:\mBbbN{}0.  \mforall{}j:\mBbbN{}i.    \mbot{}  \mcap{}  \mbot{}  =  0
10.  0  =  0
11.  \mforall{}i:\mBbbN{}0.  \mbot{}:Q  \mrightarrow{}{}f{}\mrightarrow{}    \mbot{}:R@i
12.  \mforall{}i:\mBbbN{}0.  \mforall{}j:\mBbbN{}i.  \mforall{}e,e':E.    ((\mneg{}(Q  e  e'))  \mwedge{}  (\mneg{}(Q  e'  e)))  supposing  ((\muparrow{}e'  \mmember{}\msubb{}  \mbot{})  and  (\muparrow{}e  \mmember{}\msubb{}  \mbot{}))
\mvdash{}  first-class([]):Q  \mrightarrow{}{}f{}\mrightarrow{}    first-class([]):R


By

---

Latex:
(RepUR  ``first-class``  0  THEN  BLemma  `Q-R-glued-empty`  THEN  Auto)

---

Home Index