---

Step * 1 of Lemma function_functionality_wrt_equipollent_left


1. [A] : Type
2. [B] : Type
3. [C] : Type
4. f : A ⟶ B
5. Inj(A;B;f)
6. Surj(A;B;f)
7. g : B ⟶ A
8. ∀x:B. ((f (g x)) = x ∈ B)
⊢ ∃f:(A ⟶ C) ⟶ B ⟶ C. Bij(A ⟶ C;B ⟶ C;f)
BY
{ (InstConcl [⌜λh.(h o g)⌝]⋅ THEN Auto THEN D 0 THEN Auto THEN All (Unfolds ``inject surject``) THEN Reduce 0) }

1
1. [A] : Type
2. [B] : Type
3. [C] : Type
4. f : A ⟶ B
5. ∀a1,a2:A.  (((f a1) = (f a2) ∈ B) ⇒ (a1 = a2 ∈ A))
6. ∀b:B. ∃a:A. ((f a) = b ∈ B)
7. g : B ⟶ A
8. ∀x:B. ((f (g x)) = x ∈ B)
⊢ ∀a1,a2:A ⟶ C.  (((a1 o g) = (a2 o g) ∈ (B ⟶ C)) ⇒ (a1 = a2 ∈ (A ⟶ C)))

2
1. [A] : Type
2. [B] : Type
3. [C] : Type
4. f : A ⟶ B
5. ∀a1,a2:A.  (((f a1) = (f a2) ∈ B) ⇒ (a1 = a2 ∈ A))
6. ∀b:B. ∃a:A. ((f a) = b ∈ B)
7. g : B ⟶ A
8. ∀x:B. ((f (g x)) = x ∈ B)
⊢ ∀b:B ⟶ C. ∃a:A ⟶ C. ((a o g) = b ∈ (B ⟶ C))

---

Latex:

---

Latex:

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


By

---

Latex:
(InstConcl  [\mkleeneopen{}\mlambda{}h.(h  o  g)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  All  (Unfolds  ``inject  surject``)
  THEN  Reduce  0)

---

Home Index