---

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


1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. H : CubicalSet{j}
5. Gamma ⊢ ((phi ∧ psi) ⇒ 0(𝔽))
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)| (phi ∧ psi)(rho) = 1 ∈ Point(face_lattice(I))} 
⊢ False
BY
{ ((D -1 THEN UnfoldTopAb 5) THEN FHyp 5 [-1] THEN Auto THEN MoveToConcl (-1) THEN Fold `not` 0) }

1
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)))

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  phi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
3.  psi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
4.  H  :  CubicalSet\{j\}
5.  Gamma  \mvdash{}  ((phi  \mwedge{}  psi)  {}\mRightarrow{}  0(\mBbbF{}))
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)|  (phi  \mwedge{}  psi)(rho)  =  1\} 
\mvdash{}  False


By

---

Latex:
((D  -1  THEN  UnfoldTopAb  5)  THEN  FHyp  5  [-1]  THEN  Auto  THEN  MoveToConcl  (-1)  THEN  Fold  `not`  0)

---

Home Index