---

Step * of Lemma product_functionality_wrt_equipollent_dependent

∀[A,B:Type]. ∀[C:A ⟶ Type]. ∀[D:B ⟶ Type].
  ∀f:A ⟶ B. (Bij(A;B;f) ⇒ (∀a:A. C[a] ~ D[f a]) ⇒ a:A × C[a] ~ b:B × D[b])
BY
{ TACTIC:(Auto THEN All (Unfold `equipollent`) THEN (Skolemize (-1) `g' THENA Auto)) }

1
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)
⊢ ∃f:(a:A × C[a]) ⟶ (b:B × D[b]). Bij(a:A × C[a];b:B × D[b];f)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[C:A  {}\mrightarrow{}  Type].  \mforall{}[D:B  {}\mrightarrow{}  Type].
    \mforall{}f:A  {}\mrightarrow{}  B.  (Bij(A;B;f)  {}\mRightarrow{}  (\mforall{}a:A.  C[a]  \msim{}  D[f  a])  {}\mRightarrow{}  a:A  \mtimes{}  C[a]  \msim{}  b:B  \mtimes{}  D[b])


By

---

Latex:
TACTIC:(Auto  THEN  All  (Unfold  `equipollent`)  THEN  (Skolemize  (-1)  `g'  THENA  Auto))

---

Home Index