---

Step * 2 1 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)
⊢ Inj(⋂a:A. C[a];⋂b:B. D[b];fst(h))
BY
{ ((Assert ⌜h ∈ ∃g:⋂a:A. (C[a] ⟶ D[f a]). ∀[a:A]. Bij(C[a];D[f a];g)⌝⋅
    THENA ((InstLemma `pair-eta` [⌜h⌝]⋅ THENA (With ⌜a⌝ (D (-1))⋅ THEN Auto))
           THEN RepUR ``uall`` 0
           THEN HypSubst (-1) 0
           THEN MemCD
           THEN Auto
           THEN (With ⌜a1⌝ (D (-3))⋅ THENA Auto)
           THEN All(RepUR ``exists``)
           THEN DProdsAndUnions
           THEN SimpEqPairs
           THEN Auto)
    )
   THEN (GenConclAtAddrType ⌜∃g:⋂a:A. (C[a] ⟶ D[f a]). ∀[a:A]. Bij(C[a];D[f a];g)⌝ [3;1]⋅ THENA Auto)
   ) }

1
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. h ∈ ∃g:⋂a:A. (C[a] ⟶ D[f a]). ∀[a:A]. Bij(C[a];D[f a];g)
10. v : ∃g:⋂a:A. (C[a] ⟶ D[f a]). ∀[a:A]. Bij(C[a];D[f a];g)
11. h = v ∈ (∃g:⋂a:A. (C[a] ⟶ D[f a]). ∀[a:A]. Bij(C[a];D[f a];g))
⊢ Inj(⋂a:A. C[a];⋂b:B. D[b];fst(v))

---

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)
\mvdash{}  Inj(\mcap{}a:A.  C[a];\mcap{}b:B.  D[b];fst(h))


By

---

Latex:
((Assert  \mkleeneopen{}h  \mmember{}  \mexists{}g:\mcap{}a:A.  (C[a]  {}\mrightarrow{}  D[f  a]).  \mforall{}[a:A].  Bij(C[a];D[f  a];g)\mkleeneclose{}\mcdot{}
    THENA  ((InstLemma  `pair-eta`  [\mkleeneopen{}h\mkleeneclose{}]\mcdot{}  THENA  (With  \mkleeneopen{}a\mkleeneclose{}  (D  (-1))\mcdot{}  THEN  Auto))
                  THEN  RepUR  ``uall``  0
                  THEN  HypSubst  (-1)  0
                  THEN  MemCD
                  THEN  Auto
                  THEN  (With  \mkleeneopen{}a1\mkleeneclose{}  (D  (-3))\mcdot{}  THENA  Auto)
                  THEN  All(RepUR  ``exists``)
                  THEN  DProdsAndUnions
                  THEN  SimpEqPairs
                  THEN  Auto)
    )
  THEN  (GenConclAtAddrType  \mkleeneopen{}\mexists{}g:\mcap{}a:A.  (C[a]  {}\mrightarrow{}  D[f  a]).  \mforall{}[a:A].  Bij(C[a];D[f  a];g)\mkleeneclose{}  [3;1]\mcdot{}  THENA  Auto)
  )

---

Home Index