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

[Info,A,B:Type].
  ∀es:EO+(Info). ∀X:EClass(A). ∀Y:EClass(B).
    ∀[R:E(X) ─→ A ─→ B ─→ ℙ]
      (e∈X(x) c Y(y) such that
        R[e;x;y]
         ⇐⇒ ∃f:E(X) ─→ E(Y). (Bij(E(X);E(Y);f) ∧ (∀e:E(X). (e c≤ e ∧ R[e;X(e);Y(f e)])))) supposing 
         ((∀b1,b2:E(Y). ∀e:E(X).  (R[e;X(e);Y(b1)]  R[e;X(e);Y(b2)]  (b1 b2 ∈ E(Y)))) and 
         (∀b:B. ∀a1,a2:E(X).  (R[a1;X(a1);b]  R[a2;X(a2);b]  (a1 a2 ∈ E(X)))))
BY
Auto }

1
1. [Info] Type
2. [A] Type
3. [B] Type
4. es EO+(Info)@i'
5. EClass(A)@i'
6. 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≤ e ∧ R[e;X(e);Y(f e)])))

2
1. [Info] Type
2. [A] Type
3. [B] Type
4. es EO+(Info)@i'
5. EClass(A)@i'
6. 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. ∃f:E(X) ─→ E(Y). (Bij(E(X);E(Y);f) ∧ (∀e:E(X). (e c≤ e ∧ R[e;X(e);Y(f e)])))@i
⊢ e∈X(x) c Y(y) such that
   R[e;x;y]


Latex:



Latex:
\mforall{}[Info,A,B:Type].
    \mforall{}es:EO+(Info).  \mforall{}X:EClass(A).  \mforall{}Y:EClass(B).
        \mforall{}[R:E(X)  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}]
            (e\mmember{}X(x)  \mLeftarrow{}c\mRightarrow{}  Y(y)  such  that
                R[e;x;y]
                  \mLeftarrow{}{}\mRightarrow{}  \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)]))))  supposing 
                  ((\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)))  and 
                  (\mforall{}b:B.  \mforall{}a1,a2:E(X).    (R[a1;X(a1);b]  {}\mRightarrow{}  R[a2;X(a2);b]  {}\mRightarrow{}  (a1  =  a2))))


By


Latex:
Auto




Home Index