---

Step * 1 of Lemma es-class-causal-rel-iff-bijection


1. [Info] : Type
2. [A] : Type
3. [B] : Type
4. es : EO+(Info)@i'
5. X : EClass(A)@i'
6. Y : EClass(B)@i'
7. [R] : E(X) ─→ A ─→ B ─→ ℙ
8. ∀b:B. ∀a1,a2:E(X).  (R[a1;X(a1);b] ⇒ R[a2;X(a2);b] ⇒ (a1 = a2 ∈ E(X)))
9. ∀b1,b2:E(Y). ∀e:E(X).  (R[e;X(e);Y(b1)] ⇒ R[e;X(e);Y(b2)] ⇒ (b1 = b2 ∈ E(Y)))
10. e∈X(x) ⇐c⇒ Y(y) such that
     R[e;x;y]@i
⊢ ∃f:E(X) ─→ E(Y). (Bij(E(X);E(Y);f) ∧ (∀e:E(X). (e c≤ f e ∧ R[e;X(e);Y(f e)])))
BY
{ ((D (-1)
    THEN (Skolemize (-1) `f'  THENM (With ⌈f⌉ (D 0)⋅ THENM (D 0 THEN Try (Trivial) THEN D 0 THEN D 0 THEN Auto)))
    )
   THENA Auto
   ) }

1
1. Info : Type
2. A : Type
3. B : Type
4. es : EO+(Info)@i'
5. X : EClass(A)@i'
6. Y : EClass(B)@i'
7. R : E(X) ─→ A ─→ B ─→ ℙ
8. ∀b:B. ∀a1,a2:E(X).  (R[a1;X(a1);b] ⇒ R[a2;X(a2);b] ⇒ (a1 = a2 ∈ E(X)))
9. ∀b1,b2:E(Y). ∀e:E(X).  (R[e;X(e);Y(b1)] ⇒ R[e;X(e);Y(b2)] ⇒ (b1 = b2 ∈ E(Y)))
10. ∀e:E(Y). ∃e':E(X). (e' c≤ e ∧ R[e';X(e');Y(e)])@i
11. ∀e':E(X). ∃e:E(Y). (e' c≤ e ∧ R[e';X(e');Y(e)])
12. f : e':E(X) ─→ E(Y)
13. ∀e':E(X). (e' c≤ f e' ∧ R[e';X(e');Y(f e')])
14. a1 : E(X)@i
15. a2 : E(X)@i
16. (f a1) = (f a2) ∈ E(Y)@i
⊢ a1 = a2 ∈ E(X)

2
1. [Info] : Type
2. [A] : Type
3. [B] : Type
4. es : EO+(Info)@i'
5. X : EClass(A)@i'
6. Y : EClass(B)@i'
7. [R] : E(X) ─→ A ─→ B ─→ ℙ
8. ∀b:B. ∀a1,a2:E(X).  (R[a1;X(a1);b] ⇒ R[a2;X(a2);b] ⇒ (a1 = a2 ∈ E(X)))
9. ∀b1,b2:E(Y). ∀e:E(X).  (R[e;X(e);Y(b1)] ⇒ R[e;X(e);Y(b2)] ⇒ (b1 = b2 ∈ E(Y)))
10. ∀e:E(Y). ∃e':E(X). (e' c≤ e ∧ R[e';X(e');Y(e)])@i
11. ∀e':E(X). ∃e:E(Y). (e' c≤ e ∧ R[e';X(e');Y(e)])
12. f : e':E(X) ─→ E(Y)
13. ∀e':E(X). (e' c≤ f e' ∧ R[e';X(e');Y(f e')])
14. b : E(Y)@i
⊢ ∃a:E(X). ((f a) = b ∈ E(Y))

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  [A]  :  Type
3.  [B]  :  Type
4.  es  :  EO+(Info)@i'
5.  X  :  EClass(A)@i'
6.  Y  :  EClass(B)@i'
7.  [R]  :  E(X)  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}
8.  \mforall{}b:B.  \mforall{}a1,a2:E(X).    (R[a1;X(a1);b]  {}\mRightarrow{}  R[a2;X(a2);b]  {}\mRightarrow{}  (a1  =  a2))
9.  \mforall{}b1,b2:E(Y).  \mforall{}e:E(X).    (R[e;X(e);Y(b1)]  {}\mRightarrow{}  R[e;X(e);Y(b2)]  {}\mRightarrow{}  (b1  =  b2))
10.  e\mmember{}X(x)  \mLeftarrow{}c\mRightarrow{}  Y(y)  such  that
          R[e;x;y]@i
\mvdash{}  \mexists{}f:E(X)  {}\mrightarrow{}  E(Y).  (Bij(E(X);E(Y);f)  \mwedge{}  (\mforall{}e:E(X).  (e  c\mleq{}  f  e  \mwedge{}  R[e;X(e);Y(f  e)])))


By

---

Latex:
((D  (-1)
    THEN  (Skolemize  (-1)  `f' 
              THENM  (With  \mkleeneopen{}f\mkleeneclose{}  (D  0)\mcdot{}  THENM  (D  0  THEN  Try  (Trivial)  THEN  D  0  THEN  D  0  THEN  Auto))
              )
    )
  THENA  Auto
  )

---

Home Index