---

Step * 1 of Lemma stable-union-decomp


1. X : Type
2. T : Type
3. P : T ⟶ X ⟶ ℙ
4. S : T ⟶ Type
5. Q : i:T ⟶ S[i] ⟶ X ⟶ ℙ
6. ∀x:X. ∀i:T. ∀s:S[i].  (Q[i;s;x] ⇒ (¬¬P[i;x]))
7. ∀x:X. ∀i:T.  (P[i;x] ⇒ (¬¬(∃s:S[i]. Q[i;s;x])))
8. x : X
9. i : T
10. P[i;x]
⊢ ¬¬(∃p:i:T × S[i]. Q[fst(p);snd(p);x])
BY
{ ((FHyp (-4) [-1] THENA Auto) THEN RepeatFor 2 (ParallelLast) THEN ExRepD THEN D 0 With ⌜<i, s>⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  T  :  Type
3.  P  :  T  {}\mrightarrow{}  X  {}\mrightarrow{}  \mBbbP{}
4.  S  :  T  {}\mrightarrow{}  Type
5.  Q  :  i:T  {}\mrightarrow{}  S[i]  {}\mrightarrow{}  X  {}\mrightarrow{}  \mBbbP{}
6.  \mforall{}x:X.  \mforall{}i:T.  \mforall{}s:S[i].    (Q[i;s;x]  {}\mRightarrow{}  (\mneg{}\mneg{}P[i;x]))
7.  \mforall{}x:X.  \mforall{}i:T.    (P[i;x]  {}\mRightarrow{}  (\mneg{}\mneg{}(\mexists{}s:S[i].  Q[i;s;x])))
8.  x  :  X
9.  i  :  T
10.  P[i;x]
\mvdash{}  \mneg{}\mneg{}(\mexists{}p:i:T  \mtimes{}  S[i].  Q[fst(p);snd(p);x])


By

---

Latex:
((FHyp  (-4)  [-1]  THENA  Auto)  THEN  RepeatFor  2  (ParallelLast)  THEN  ExRepD  THEN  D  0  With  \mkleeneopen{}<i,  s>\mkleeneclose{}    THE\000CN  Auto)

---

Home Index