---

Step * of Lemma face_lattice-fset-join-eq-1

∀I:fset(ℕ). ∀s:fset(Point(face_lattice(I))).
  (\/(s) = 1 ∈ Point(face_lattice(I)) ⇐⇒ ∃x:Point(face_lattice(I)). (x ∈ s ∧ (x = 1 ∈ Point(face_lattice(I)))))
BY
{ ((D 0 THENA Auto) THEN Using [`eq',⌜face_lattice-deq()⌝] (BLemma `fset-induction`)⋅ THEN Auto) }

1
1. I : fset(ℕ)
2. s : fset(Point(face_lattice(I)))
⊢ SqStable(∃x:Point(face_lattice(I)). (x ∈ s ∧ (x = 1 ∈ Point(face_lattice(I)))))

2
1. I : fset(ℕ)
2. \/({}) = 1 ∈ Point(face_lattice(I))
⊢ ∃x:Point(face_lattice(I)). (x ∈ {} ∧ (x = 1 ∈ Point(face_lattice(I))))

3
1. I : fset(ℕ)
2. ∃x:Point(face_lattice(I)). (x ∈ {} ∧ (x = 1 ∈ Point(face_lattice(I))))
⊢ \/({}) = 1 ∈ Point(face_lattice(I))

4
1. I : fset(ℕ)
2. s : fset(Point(face_lattice(I)))
3. x : Point(face_lattice(I))
4. (\/(s) = 1 ∈ Point(face_lattice(I))) ⇒ (∃x:Point(face_lattice(I)). (x ∈ s ∧ (x = 1 ∈ Point(face_lattice(I)))))
5. (\/(s) = 1 ∈ Point(face_lattice(I))) ⇐ ∃x:Point(face_lattice(I)). (x ∈ s ∧ (x = 1 ∈ Point(face_lattice(I))))
6. ¬x ∈ s
7. \/(fset-add(face_lattice-deq();x;s)) = 1 ∈ Point(face_lattice(I))
⊢ ∃x@0:Point(face_lattice(I)). (x@0 ∈ fset-add(face_lattice-deq();x;s) ∧ (x@0 = 1 ∈ Point(face_lattice(I))))

5
1. I : fset(ℕ)
2. s : fset(Point(face_lattice(I)))
3. x : Point(face_lattice(I))
4. (\/(s) = 1 ∈ Point(face_lattice(I))) ⇒ (∃x:Point(face_lattice(I)). (x ∈ s ∧ (x = 1 ∈ Point(face_lattice(I)))))
5. (\/(s) = 1 ∈ Point(face_lattice(I))) ⇐ ∃x:Point(face_lattice(I)). (x ∈ s ∧ (x = 1 ∈ Point(face_lattice(I))))
6. ¬x ∈ s
7. ∃x@0:Point(face_lattice(I)). (x@0 ∈ fset-add(face_lattice-deq();x;s) ∧ (x@0 = 1 ∈ Point(face_lattice(I))))
⊢ \/(fset-add(face_lattice-deq();x;s)) = 1 ∈ Point(face_lattice(I))

---

Latex:

---

Latex:
\mforall{}I:fset(\mBbbN{}).  \mforall{}s:fset(Point(face\_lattice(I))).
    (\mbackslash{}/(s)  =  1  \mLeftarrow{}{}\mRightarrow{}  \mexists{}x:Point(face\_lattice(I)).  (x  \mmember{}  s  \mwedge{}  (x  =  1)))


By

---

Latex:
((D  0  THENA  Auto)  THEN  Using  [`eq',\mkleeneopen{}face\_lattice-deq()\mkleeneclose{}]  (BLemma  `fset-induction`)\mcdot{}  THEN  Auto)

---

Home Index