---

Step * 1 1 4 of Lemma union_functionality_wrt_equipollent


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


By

---

Latex:
TACTIC:OnMaybeHyp  8  (\mbackslash{}h.  (D  h
                                                    THEN  Unfold  `surject`  h+1
                                                    THEN  (InstHyp  [\mkleeneopen{}y\mkleeneclose{}]  (h+1)\mcdot{}  THENA  Auto)
                                                    THEN  D  -1
                                                    THEN  (InstConcl  [\mkleeneopen{}inr  a  \mkleeneclose{}]\mcdot{}  THENA  Auto)
                                                    THEN  Reduce  0
                                                    THEN  Auto))

---

Home Index