---

Step * 1 of Lemma finite'_functionality_wrt_equipollent


1. [A] : Type
2. [B] : Type
3. f : A ⟶ B
4. Inj(A;B;f)
5. Surj(A;B;f)
6. ∀f:A ⟶ A. (Inj(A;A;f) ⇒ Surj(A;A;f))
7. g : B ⟶ B
8. Inj(B;B;g)
⊢ Surj(B;B;g)
BY
{ (Unfold `surject` (-4)
   THEN (Skolemize (-4) `h' THENA Auto)
   THEN (InstHyp [⌜(h o g) o f⌝] (-5)⋅ THENA Auto)
   THEN Try ((ParallelLast
              THEN (RepUR ``compose`` -1 THEN Auto)
              THEN (InstHyp [⌜h b⌝] (-2)⋅ THENA Auto)
              THEN D -1
              THEN InstConcl [⌜f a⌝]⋅
              THEN Auto
              THEN (InstHyp [⌜g (f a)⌝] (-5)⋅ THENA Auto)
              THEN (InstHyp [⌜b⌝] (-6)⋅ THENA Auto)
              THEN HypSubst (-3) (-2)
              THEN Auto)⋅)) }

1
.....antecedent..... 
1. [A] : Type
2. [B] : Type
3. f : A ⟶ B
4. Inj(A;B;f)
5. ∀b:B. ∃a:A. ((f a) = b ∈ B)
6. ∀f:A ⟶ A. (Inj(A;A;f) ⇒ Surj(A;A;f))
7. g : B ⟶ B
8. Inj(B;B;g)
9. h : b:B ⟶ A
10. ∀b:B. ((f (h b)) = b ∈ B)
⊢ Inj(A;A;(h o g) o f)

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  f  :  A  {}\mrightarrow{}  B
4.  Inj(A;B;f)
5.  Surj(A;B;f)
6.  \mforall{}f:A  {}\mrightarrow{}  A.  (Inj(A;A;f)  {}\mRightarrow{}  Surj(A;A;f))
7.  g  :  B  {}\mrightarrow{}  B
8.  Inj(B;B;g)
\mvdash{}  Surj(B;B;g)


By

---

Latex:
(Unfold  `surject`  (-4)
  THEN  (Skolemize  (-4)  `h'  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}(h  o  g)  o  f\mkleeneclose{}]  (-5)\mcdot{}  THENA  Auto)
  THEN  Try  ((ParallelLast
                        THEN  (RepUR  ``compose``  -1  THEN  Auto)
                        THEN  (InstHyp  [\mkleeneopen{}h  b\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
                        THEN  D  -1
                        THEN  InstConcl  [\mkleeneopen{}f  a\mkleeneclose{}]\mcdot{}
                        THEN  Auto
                        THEN  (InstHyp  [\mkleeneopen{}g  (f  a)\mkleeneclose{}]  (-5)\mcdot{}  THENA  Auto)
                        THEN  (InstHyp  [\mkleeneopen{}b\mkleeneclose{}]  (-6)\mcdot{}  THENA  Auto)
                        THEN  HypSubst  (-3)  (-2)
                        THEN  Auto)\mcdot{}))

---

Home Index