---

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

∀[Info,A,B,C:Type]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[F:bag(A) ─→ bag(B) ─→ bag(C)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  (uiff(↑e ∈b F|X, Y|;(↑e ∈b X) ∧ (↑e ∈b Y) ∧ (¬↑bag-null(F {X@e} {Y@e})))) supposing 
     (single-valued-classrel(es;Y;B) and 
     single-valued-classrel(es;X;A) and 
     lifting2-like(A;B;F))
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 : bag(A) ─→ bag(B) ─→ bag(C)
8. X : EClass(A)
9. Y : EClass(B)
10. lifting2-like(A;B;F)
11. single-valued-classrel(es;X;A)
12. single-valued-classrel(es;Y;B)
13. ↑e ∈b F|X, Y|
⊢ (↑e ∈b X) ∧ (↑e ∈b Y) ∧ (¬↑bag-null(F {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 : bag(A) ─→ bag(B) ─→ bag(C)
8. X : EClass(A)
9. Y : EClass(B)
10. lifting2-like(A;B;F)
11. single-valued-classrel(es;X;A)
12. single-valued-classrel(es;Y;B)
13. (↑e ∈b X) ∧ (↑e ∈b Y) ∧ (¬↑bag-null(F {X@e} {Y@e}))
⊢ ↑e ∈b F|X, Y|

---

Latex:

---

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


By

---

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

---

Home Index