---

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


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|
BY
{ ((RepUR ``member-eclass simple-comb-2 simple-comb`` 0)⋅
   THEN ((RW assert_pushdownC 0)⋅ THENA Auto)
   THEN Unfold `lifting2-like` 10
   THEN ((D 10 THEN InstHyp [⌈X es e⌉; ⌈Y es e⌉;⌈X@e⌉;⌈Y@e⌉] 10⋅) 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. ∀as:bag(A). ∀bs:bag(B). ∀a:A. ∀b:B.
      (single-valued-bag(as;A)
      ⇒ single-valued-bag(bs;B)
      ⇒ a ↓∈ as
      ⇒ b ↓∈ bs
      ⇒ (↑bag-null(F as bs) ⇐⇒ ↑bag-null(F {a} {b})))
11. ∀as:bag(A). (↑bag-null(F as {}))
12. ∀bs:bag(B). (↑bag-null(F {} bs))
13. single-valued-classrel(es;X;A)
14. single-valued-classrel(es;Y;B)
15. ↑e ∈b X
16. ↑e ∈b Y
17. ¬↑bag-null(F {X@e} {Y@e})
⊢ single-valued-bag(X es e;A)

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. ∀as:bag(A). ∀bs:bag(B). ∀a:A. ∀b:B.
      (single-valued-bag(as;A)
      ⇒ single-valued-bag(bs;B)
      ⇒ a ↓∈ as
      ⇒ b ↓∈ bs
      ⇒ (↑bag-null(F as bs) ⇐⇒ ↑bag-null(F {a} {b})))
11. ∀as:bag(A). (↑bag-null(F as {}))
12. ∀bs:bag(B). (↑bag-null(F {} bs))
13. single-valued-classrel(es;X;A)
14. single-valued-classrel(es;Y;B)
15. ↑e ∈b X
16. ↑e ∈b Y
17. ¬↑bag-null(F {X@e} {Y@e})
⊢ single-valued-bag(Y es e;B)

3
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. ∀as:bag(A). ∀bs:bag(B). ∀a:A. ∀b:B.
      (single-valued-bag(as;A)
      ⇒ single-valued-bag(bs;B)
      ⇒ a ↓∈ as
      ⇒ b ↓∈ bs
      ⇒ (↑bag-null(F as bs) ⇐⇒ ↑bag-null(F {a} {b})))
11. ∀as:bag(A). (↑bag-null(F as {}))
12. ∀bs:bag(B). (↑bag-null(F {} bs))
13. single-valued-classrel(es;X;A)
14. single-valued-classrel(es;Y;B)
15. ↑e ∈b X
16. ↑e ∈b Y
17. ¬↑bag-null(F {X@e} {Y@e})
⊢ X@e ↓∈ X es e

4
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. ∀as:bag(A). ∀bs:bag(B). ∀a:A. ∀b:B.
      (single-valued-bag(as;A)
      ⇒ single-valued-bag(bs;B)
      ⇒ a ↓∈ as
      ⇒ b ↓∈ bs
      ⇒ (↑bag-null(F as bs) ⇐⇒ ↑bag-null(F {a} {b})))
11. ∀as:bag(A). (↑bag-null(F as {}))
12. ∀bs:bag(B). (↑bag-null(F {} bs))
13. single-valued-classrel(es;X;A)
14. single-valued-classrel(es;Y;B)
15. ↑e ∈b X
16. ↑e ∈b Y
17. ¬↑bag-null(F {X@e} {Y@e})
⊢ Y@e ↓∈ Y es e

5
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. ∀as:bag(A). ∀bs:bag(B). ∀a:A. ∀b:B.
      (single-valued-bag(as;A)
      ⇒ single-valued-bag(bs;B)
      ⇒ a ↓∈ as
      ⇒ b ↓∈ bs
      ⇒ (↑bag-null(F as bs) ⇐⇒ ↑bag-null(F {a} {b})))
11. (∀as:bag(A). (↑bag-null(F as {}))) ∧ (∀bs:bag(B). (↑bag-null(F {} bs)))
12. single-valued-classrel(es;X;A)
13. single-valued-classrel(es;Y;B)
14. (↑e ∈b X) ∧ (↑e ∈b Y) ∧ (¬↑bag-null(F {X@e} {Y@e}))
15. ↑bag-null(F (X es e) (Y es e)) ⇐⇒ ↑bag-null(F {X@e} {Y@e})
⊢ ¬(#(F (X es e) (Y es e)) = 0 ∈ ℤ)

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  C  :  Type
5.  es  :  EO+(Info)
6.  e  :  E
7.  F  :  bag(A)  {}\mrightarrow{}  bag(B)  {}\mrightarrow{}  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.  (\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (\muparrow{}e  \mmember{}\msubb{}  Y)  \mwedge{}  (\mneg{}\muparrow{}bag-null(F  \{X@e\}  \{Y@e\}))
\mvdash{}  \muparrow{}e  \mmember{}\msubb{}  F|X,  Y|


By

---

Latex:
((RepUR  ``member-eclass  simple-comb-2  simple-comb``  0)\mcdot{}
  THEN  ((RW  assert\_pushdownC  0)\mcdot{}  THENA  Auto)
  THEN  Unfold  `lifting2-like`  10
  THEN  ((D  10  THEN  InstHyp  [\mkleeneopen{}X  es  e\mkleeneclose{};  \mkleeneopen{}Y  es  e\mkleeneclose{};\mkleeneopen{}X@e\mkleeneclose{};\mkleeneopen{}Y@e\mkleeneclose{}]  10\mcdot{})  THENA  Auto))

---

Home Index