---

Step * 1 1 of Lemma map-to-context-subset-disjoint


1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. H : CubicalSet{j}
5. ∀I:fset(ℕ). ∀rho:Gamma(I).
     (((phi ∧ psi)(rho) = 1 ∈ Point(face_lattice(I))) ⇒ (0(𝔽)(rho) = 1 ∈ Point(face_lattice(I))))
6. sigma : ∀A:fset(ℕ). (H(A) ⇒ {rho:Gamma(A)| (phi ∧ psi)(rho) = 1 ∈ Point(face_lattice(A))} )
7. I : fset(ℕ)
8. H(I)
9. rho : Gamma(I)
10. (phi ∧ psi)(rho) = 1 ∈ Point(face_lattice(I))
⊢ ¬(0(𝔽)(rho) = 1 ∈ Point(face_lattice(I)))
BY
{ ((Subst' 0(𝔽)(rho) ~ 0 0 THEN Auto) THEN Computation⋅) }

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  phi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
3.  psi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
4.  H  :  CubicalSet\{j\}
5.  \mforall{}I:fset(\mBbbN{}).  \mforall{}rho:Gamma(I).    (((phi  \mwedge{}  psi)(rho)  =  1)  {}\mRightarrow{}  (0(\mBbbF{})(rho)  =  1))
6.  sigma  :  \mforall{}A:fset(\mBbbN{}).  (H(A)  {}\mRightarrow{}  \{rho:Gamma(A)|  (phi  \mwedge{}  psi)(rho)  =  1\}  )
7.  I  :  fset(\mBbbN{})
8.  H(I)
9.  rho  :  Gamma(I)
10.  (phi  \mwedge{}  psi)(rho)  =  1
\mvdash{}  \mneg{}(0(\mBbbF{})(rho)  =  1)


By

---

Latex:
((Subst'  0(\mBbbF{})(rho)  \msim{}  0  0  THEN  Auto)  THEN  Computation\mcdot{})

---

Home Index