---

Step * 2 1 of Lemma set-elim


1. A : Type
2. B : A ⟶ Type
3. a : A
4. B[a]
5. (λp.(fst(p))) <a, %2> ∈ A
⊢ Ax ∈ ↓B[fst(<a, %2>)]
BY
{ TACTIC:(RenameVar `a2' (-2) THEN Assert ⌜((λp.Ax) a2) = ((λp.Ax) a2) ∈ Image(B[fst(<a, a2>)],(λp.Ax))⌝⋅) }

1
.....assertion..... 
1. A : Type
2. B : A ⟶ Type
3. a : A
4. a2 : B[a]
5. (λp.(fst(p))) <a, a2> ∈ A
⊢ ((λp.Ax) a2) = ((λp.Ax) a2) ∈ Image(B[fst(<a, a2>)],(λp.Ax))

2
1. A : Type
2. B : A ⟶ Type
3. a : A
4. a2 : B[a]
5. (λp.(fst(p))) <a, a2> ∈ A
6. ((λp.Ax) a2) = ((λp.Ax) a2) ∈ Image(B[fst(<a, a2>)],(λp.Ax))
⊢ Ax ∈ ↓B[fst(<a, a2>)]

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  a  :  A
4.  B[a]
5.  (\mlambda{}p.(fst(p)))  <a,  \%2>  \mmember{}  A
\mvdash{}  Ax  \mmember{}  \mdownarrow{}B[fst(<a,  \%2>)]


By

---

Latex:
TACTIC:(RenameVar  `a2'  (-2)  THEN  Assert  \mkleeneopen{}((\mlambda{}p.Ax)  a2)  =  ((\mlambda{}p.Ax)  a2)\mkleeneclose{}\mcdot{})

---

Home Index