---

Step * 1 1 1 of Lemma product_functionality_wrt_equipollent_dependent


1. A : Type
2. B : Type
3. C : A ⟶ Type
4. D : B ⟶ Type
5. f : A ⟶ B
6. Bij(A;B;f)
7. ∀a:A. ∃f@0:C[a] ⟶ D[f a]. Bij(C[a];D[f a];f@0)
8. g : a:A ⟶ C[a] ⟶ D[f a]
9. ∀a:A. Bij(C[a];D[f a];g a)
10. a : A
11. a3 : C[a]
12. a4 : A
13. a5 : C[a4]
14. (f a) = (f a4) ∈ B
15. (g a a3) = (g a4 a5) ∈ D[f a]
⊢ <a, a3> = <a4, a5> ∈ (a:A × C[a])
BY
{ ((Assert a = a4 ∈ A BY Auto) THEN EqCD THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  C  :  A  {}\mrightarrow{}  Type
4.  D  :  B  {}\mrightarrow{}  Type
5.  f  :  A  {}\mrightarrow{}  B
6.  Bij(A;B;f)
7.  \mforall{}a:A.  \mexists{}f@0:C[a]  {}\mrightarrow{}  D[f  a].  Bij(C[a];D[f  a];f@0)
8.  g  :  a:A  {}\mrightarrow{}  C[a]  {}\mrightarrow{}  D[f  a]
9.  \mforall{}a:A.  Bij(C[a];D[f  a];g  a)
10.  a  :  A
11.  a3  :  C[a]
12.  a4  :  A
13.  a5  :  C[a4]
14.  (f  a)  =  (f  a4)
15.  (g  a  a3)  =  (g  a4  a5)
\mvdash{}  <a,  a3>  =  <a4,  a5>


By

---

Latex:
((Assert  a  =  a4  BY  Auto)  THEN  EqCD  THEN  Auto)\mcdot{}

---

Home Index