---

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

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

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

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

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepeatFor  2  ((D  0  THENA  Auto)))

---

Home Index