---

Step * of Lemma isect_functionality_wrt_equipollent_dependent

∀[A,B:Type]. ∀[C:A ⟶ Type]. ∀[D:B ⟶ Type].
  ∀f:A ⟶ B. (A ⇒ Bij(A;B;f) ⇒ (∀[a:A]. C[a] ~ D[f a]) ⇒ ⋂a:A. C[a] ~ ⋂b:B. D[b])
BY
{ (Auto
   THEN All (Unfold `equipollent`)
   THEN RenameVar `a' (-3)
   THEN RenameVar `h' (-1)
   THEN (InstConcl [⌜fst(h)⌝]⋅ THENA Auto)) }

1
.....wf..... 
1. A : Type
2. B : Type
3. C : A ⟶ Type
4. D : B ⟶ Type
5. f : A ⟶ B
6. a : A
7. Bij(A;B;f)
8. h : ∀[a:A]. ∃f@0:C[a] ⟶ D[f a]. Bij(C[a];D[f a];f@0)
⊢ fst(h) ∈ (⋂a:A. C[a]) ⟶ (⋂b:B. D[b])

2
1. [A] : Type
2. [B] : Type
3. [C] : A ⟶ Type
4. [D] : B ⟶ Type
5. f : A ⟶ B
6. a : A
7. Bij(A;B;f)
8. h : ∀[a:A]. ∃f@0:C[a] ⟶ D[f a]. Bij(C[a];D[f a];f@0)
⊢ Bij(⋂a:A. C[a];⋂b:B. D[b];fst(h))

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  All  (Unfold  `equipollent`)
  THEN  RenameVar  `a'  (-3)
  THEN  RenameVar  `h'  (-1)
  THEN  (InstConcl  [\mkleeneopen{}fst(h)\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index