---

Step * of Lemma isect-mono

∀A:Type. ∀B:A ⟶ Type.  ((∀a:A. mono(B[a])) ⇒ mono(⋂a:A. B[a]))
BY
{ (Auto THEN D 0 THEN Auto THEN EqTypeCD THEN Auto THEN BackThruHyp' 3 THEN Auto) }

1
1. A : Type@i'
2. B : A ⟶ Type@i'
3. ∀a:A. ∀a@0:B[a]. ∀b:Base.  (is-above(B[a];a@0;b) ⇒ (a@0 = b ∈ B[a]))@i
4. a : ⋂a:A. B[a]@i
5. b : Base@i
6. is-above(⋂a:A. B[a];a;b)@i
7. a1 : A
⊢ is-above(B[a1];a;b)

---

Latex:

---

Latex:
\mforall{}A:Type.  \mforall{}B:A  {}\mrightarrow{}  Type.    ((\mforall{}a:A.  mono(B[a]))  {}\mRightarrow{}  mono(\mcap{}a:A.  B[a]))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  EqTypeCD  THEN  Auto  THEN  BackThruHyp'  3  THEN  Auto)

---

Home Index