---

Step * of Lemma squash-exists-is-union-squash

∀[T:Type]. ∀[P:T ⟶ ℙ].  ↓∃x:T. P[x] ≡ ⋃x:T.(↓P[x])
BY
{ (Auto THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
.....subterm..... T:t
1:n
1. T : Type
2. P : T ⟶ ℙ
3. x : ↓∃x:T. P[x]@i
⊢ x ∈ ⋃x:T.(↓P[x])

2
.....subterm..... T:t
1:n
1. T : Type
2. P : T ⟶ ℙ
3. x : ⋃x:T.(↓P[x])@i
⊢ x ∈ ↓∃x:T. P[x]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    \mdownarrow{}\mexists{}x:T.  P[x]  \mequiv{}  \mcup{}x:T.(\mdownarrow{}P[x])


By

---

Latex:
(Auto  THEN  (RepeatFor  2  (D  0)  THENA  Auto))

---

Home Index