---

Step * 2 1 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)
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))
BY
{ (ThinVar `h'
   THEN ExRepD
   THEN Reduce 0
   THEN (D 0 THEN Auto)
   THEN (FLemma `biject-inverse` [7] THENA Auto)
   THEN ExRepD
   THEN (InstHyp [⌜b⌝] (-2)⋅ THENA Auto)
   THEN (With ⌜g1 b⌝ (D 8)⋅ THENA Auto)
   THEN Try (Complete (((With ⌜g1 b⌝ (D 10)⋅ THENA Auto) THEN Assert ⌜y y1 ∈ D[b]⌝⋅ THEN Auto)))
   THEN Try (Complete (((With ⌜g1 b⌝ (D 11)⋅ THENA Auto) THEN Assert ⌜y y1 ∈ D[b]⌝⋅ 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.  h  \mmember{}  \mexists{}g:\mcap{}a:A.  (C[a]  {}\mrightarrow{}  D[f  a]).  \mforall{}[a:A].  Bij(C[a];D[f  a];g)
10.  v  :  \mexists{}g:\mcap{}a:A.  (C[a]  {}\mrightarrow{}  D[f  a]).  \mforall{}[a:A].  Bij(C[a];D[f  a];g)
11.  h  =  v
\mvdash{}  Inj(\mcap{}a:A.  C[a];\mcap{}b:B.  D[b];fst(v))


By

---

Latex:
(ThinVar  `h'
  THEN  ExRepD
  THEN  Reduce  0
  THEN  (D  0  THEN  Auto)
  THEN  (FLemma  `biject-inverse`  [7]  THENA  Auto)
  THEN  ExRepD
  THEN  (InstHyp  [\mkleeneopen{}b\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  (With  \mkleeneopen{}g1  b\mkleeneclose{}  (D  8)\mcdot{}  THENA  Auto)
  THEN  Try  (Complete  (((With  \mkleeneopen{}g1  b\mkleeneclose{}  (D  10)\mcdot{}  THENA  Auto)  THEN  Assert  \mkleeneopen{}y  y1  \mmember{}  D[b]\mkleeneclose{}\mcdot{}  THEN  Auto)))
  THEN  Try  (Complete  (((With  \mkleeneopen{}g1  b\mkleeneclose{}  (D  11)\mcdot{}  THENA  Auto)  THEN  Assert  \mkleeneopen{}y  y1  \mmember{}  D[b]\mkleeneclose{}\mcdot{}  THEN  Auto))))

---

Home Index