Step * 1 1 3 of Lemma union_functionality_wrt_equipollent


1. [A] Type
2. [B] Type
3. [C] Type
4. [D] Type
5. A ⟶ B@i
6. Bij(A;B;f)
7. C ⟶ D@i
8. Bij(C;D;g)
9. B@i
⊢ ∃a:A C. (case of inl(a) => inl (f a) inr(c) => inr (g c)  (inl x) ∈ (B D))
BY
TACTIC:(OnMaybeHyp (\h. h)
          THEN OnMaybeHyp (\h. Unfold `surject` h)
          THEN OnMaybeHyp (\h. (InstHyp [⌜x⌝7⋅ THENA Auto))
          THEN -1
          THEN (InstConcl [⌜inl a⌝]⋅ THENA Auto)
          THEN Reduce 0
          THEN Auto) }


Latex:


Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  [C]  :  Type
4.  [D]  :  Type
5.  f  :  A  {}\mrightarrow{}  B@i
6.  Bij(A;B;f)
7.  g  :  C  {}\mrightarrow{}  D@i
8.  Bij(C;D;g)
9.  x  :  B@i
\mvdash{}  \mexists{}a:A  +  C.  (case  a  of  inl(a)  =>  inl  (f  a)  |  inr(c)  =>  inr  (g  c)    =  (inl  x))


By


Latex:
TACTIC:(OnMaybeHyp  6  (\mbackslash{}h.  D  h)
                THEN  OnMaybeHyp  7  (\mbackslash{}h.  Unfold  `surject`  h)
                THEN  OnMaybeHyp  7  (\mbackslash{}h.  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  7\mcdot{}  THENA  Auto))
                THEN  D  -1
                THEN  (InstConcl  [\mkleeneopen{}inl  a\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  Reduce  0
                THEN  Auto)




Home Index