---

Step * 1 2 of Lemma isect2-b-union-subtype


1. A : Type
2. B : Type
3. C : Type
4. ¬B ⋂ C
5. x : A ⋂ B ⋃ C@i
6. ∃y:B ⋃ C. (y = x ∈ (B ⋃ C))
⊢ x ∈ A ⋂ B ⋃ A ⋂ C
BY
{ (D (-1) THEN D_b_union (-2) THEN All Reduce THEN All (Fold `b-union`)) }

1
1. A : Type
2. B : Type
3. C : Type
4. ¬B ⋂ C
5. x : A ⋂ B ⋃ C@i
6. a1 : B
7. a1 = x ∈ (B ⋃ C)
⊢ x ∈ A ⋂ B ⋃ A ⋂ C

2
1. A : Type
2. B : Type
3. C : Type
4. ¬B ⋂ C
5. x : A ⋂ B ⋃ C@i
6. a1 : C
7. a1 = x ∈ (B ⋃ C)
⊢ x ∈ A ⋂ B ⋃ A ⋂ C

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  \mneg{}B  \mcap{}  C
5.  x  :  A  \mcap{}  B  \mcup{}  C@i
6.  \mexists{}y:B  \mcup{}  C.  (y  =  x)
\mvdash{}  x  \mmember{}  A  \mcap{}  B  \mcup{}  A  \mcap{}  C


By

---

Latex:
(D  (-1)  THEN  D\_b\_union  (-2)  THEN  All  Reduce  THEN  All  (Fold  `b-union`))

---

Home Index