---

Step * 1 of Lemma fpf-sub-val3


1. [A] : Type
2. [B] : A ─→ Type
3. [C] : A ─→ Type
4. eq : EqDecider(A)@i
5. f : a:A fp-> B[a]@i
6. g : a:A fp-> C[a]@i
7. x : A@i
8. [P] : a:A ─→ B[a] ─→ ℙ
9. [Q] : a:A ─→ C[a] ─→ ℙ
10. ∀x:A. ((C[x] ⊆r B[x]) c∧ (P[x;g(x)] ⇒ Q[x;g(x)])) supposing ((↑x ∈ dom(f)) and (↑x ∈ dom(g)))@i
11. ∀x:A. ((↑x ∈ dom(g)) ⇒ ((↑x ∈ dom(f)) c∧ (g(x) = f(x) ∈ B[x])))
12. ↑x ∈ dom(g)@i
13. ↑x ∈ dom(f)
14. g(x) = f(x) ∈ B[x]
15. P[x;f(x)]@i
⊢ P[x;g(x)]
BY
{ ((HypSubst (-2) 0) THEN Auto) }

---

Latex:



1.  [A]  :  Type
2.  [B]  :  A  {}\mrightarrow{}  Type
3.  [C]  :  A  {}\mrightarrow{}  Type
4.  eq  :  EqDecider(A)@i
5.  f  :  a:A  fp->  B[a]@i
6.  g  :  a:A  fp->  C[a]@i
7.  x  :  A@i
8.  [P]  :  a:A  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  \mBbbP{}
9.  [Q]  :  a:A  {}\mrightarrow{}  C[a]  {}\mrightarrow{}  \mBbbP{}
10.  \mforall{}x:A.  ((C[x]  \msubseteq{}r  B[x])  c\mwedge{}  (P[x;g(x)]  {}\mRightarrow{}  Q[x;g(x)]))  supposing  ((\muparrow{}x  \mmember{}  dom(f))  and  (\muparrow{}x  \mmember{}  dom(g)))@i
11.  \mforall{}x:A.  ((\muparrow{}x  \mmember{}  dom(g))  {}\mRightarrow{}  ((\muparrow{}x  \mmember{}  dom(f))  c\mwedge{}  (g(x)  =  f(x))))
12.  \muparrow{}x  \mmember{}  dom(g)@i
13.  \muparrow{}x  \mmember{}  dom(f)
14.  g(x)  =  f(x)
15.  P[x;f(x)]@i
\mvdash{}  P[x;g(x)]


By

((HypSubst  (-2)  0)  THEN  Auto)

---

Home Index