---

Step * of Lemma member-eclass-simple-loc-comb-1-iff

∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[F:Id ⟶ bag(A) ⟶ bag(B)]. ∀[X:EClass(A)].
  (uiff(↑e ∈b F(Loc, X);(↑e ∈b X) ∧ (¬↑bag-null(F loc(e) {X@e})))) supposing 
     (single-valued-classrel(es;X;A) and 
     lifting-like(A;F loc(e)))
BY
{ RepeatFor 11 ((D 0 THENA Auto)) }

1
1. Info : Type
2. A : Type
3. B : Type
4. es : EO+(Info)
5. e : E
6. F : Id ⟶ bag(A) ⟶ bag(B)
7. X : EClass(A)
8. lifting-like(A;F loc(e))
9. single-valued-classrel(es;X;A)
10. ↑e ∈b F(Loc, X)
⊢ (↑e ∈b X) ∧ (¬↑bag-null(F loc(e) {X@e}))

2
1. Info : Type
2. A : Type
3. B : Type
4. es : EO+(Info)
5. e : E
6. F : Id ⟶ bag(A) ⟶ bag(B)
7. X : EClass(A)
8. lifting-like(A;F loc(e))
9. single-valued-classrel(es;X;A)
10. (↑e ∈b X) ∧ (¬↑bag-null(F loc(e) {X@e}))
⊢ ↑e ∈b F(Loc, X)

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[F:Id  {}\mrightarrow{}  bag(A)  {}\mrightarrow{}  bag(B)].  \mforall{}[X:EClass(A)].
    (uiff(\muparrow{}e  \mmember{}\msubb{}  F(Loc,  X);(\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (\mneg{}\muparrow{}bag-null(F  loc(e)  \{X@e\}))))  supposing 
          (single-valued-classrel(es;X;A)  and 
          lifting-like(A;F  loc(e)))


By

---

Latex:
RepeatFor  11  ((D  0  THENA  Auto))

---

Home Index