---

Step * 2 of Lemma equipollent-iff-inverse-funs


1. [A] : Type
2. [B] : Type
3. p : A ⟶ B × (B ⟶ A)@i
4. InvFuns(A;B;fst(p);snd(p))
⊢ ∃f:A ⟶ B. Bij(A;B;f)
BY
{ ((D (-2) THEN Reduce (-1)) THEN With ⌜p1⌝ (D 0)⋅ THEN Auto) }

1
1. [A] : Type
2. [B] : Type
3. p1 : A ⟶ B@i
4. p2 : B ⟶ A@i
5. InvFuns(A;B;p1;p2)
⊢ Bij(A;B;p1)

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  p  :  A  {}\mrightarrow{}  B  \mtimes{}  (B  {}\mrightarrow{}  A)@i
4.  InvFuns(A;B;fst(p);snd(p))
\mvdash{}  \mexists{}f:A  {}\mrightarrow{}  B.  Bij(A;B;f)


By

---

Latex:
((D  (-2)  THEN  Reduce  (-1))  THEN  With  \mkleeneopen{}p1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index