---

Step * 2 2 1 2 of Lemma isect_functionality_wrt_equipollent_dependent


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)
9. d : ⋂b:B. D[b]
⊢ ((fst(h)) (fst(((snd(snd(h))) d)))) = d ∈ (⋂b:B. D[b])
BY
{ ((EqCD THENA Auto)
   THEN (FLemma `biject-inverse` [-4] THENA Auto)
   THEN ExRepD
   THEN (InstHyp [⌜b⌝] (-2)⋅ THENA Auto)
   THEN (With ⌜g b⌝ (D (-7))⋅ THENA Auto)
   THEN All(RepUR ``exists biject and surject``)
   THEN Repeat (SimpEqPairs)
   THEN (With ⌜b⌝ (D (-10))⋅ THENA Auto)
   THEN (GenConclAtAddrType ⌜∀b@0:D[f (g b)]. (a:C[g b] × (((fst(y)) a) = b@0 ∈ D[f (g b)]))⌝ [2;2;1;1]⋅ THENA Auto)
   THEN (GenConclAtAddrType ⌜a:C[g b] × (((fst(y)) a) = d ∈ D[f (g b)])⌝ [2;2;1]⋅ THENA Auto)
   THEN D (-2)
   THEN Reduce 0
   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.  a  :  A
7.  Bij(A;B;f)
8.  h  :  \mforall{}[a:A].  \mexists{}f@0:C[a]  {}\mrightarrow{}  D[f  a].  Bij(C[a];D[f  a];f@0)
9.  d  :  \mcap{}b:B.  D[b]
\mvdash{}  ((fst(h))  (fst(((snd(snd(h)))  d))))  =  d


By

---

Latex:
((EqCD  THENA  Auto)
  THEN  (FLemma  `biject-inverse`  [-4]  THENA  Auto)
  THEN  ExRepD
  THEN  (InstHyp  [\mkleeneopen{}b\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  (With  \mkleeneopen{}g  b\mkleeneclose{}  (D  (-7))\mcdot{}  THENA  Auto)
  THEN  All(RepUR  ``exists  biject  and  surject``)
  THEN  Repeat  (SimpEqPairs)
  THEN  (With  \mkleeneopen{}b\mkleeneclose{}  (D  (-10))\mcdot{}  THENA  Auto)
  THEN  (GenConclAtAddrType  \mkleeneopen{}\mforall{}b@0:D[f  (g  b)].  (a:C[g  b]  \mtimes{}  (((fst(y))  a)  =  b@0))\mkleeneclose{}  [2;2;1;1]\mcdot{}
              THENA  Auto
              )
  THEN  (GenConclAtAddrType  \mkleeneopen{}a:C[g  b]  \mtimes{}  (((fst(y))  a)  =  d)\mkleeneclose{}  [2;2;1]\mcdot{}  THENA  Auto)
  THEN  D  (-2)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index