Step * of Lemma dMpair-eq-meet

∀[I:fset(ℕ)]. ∀[i,j:ℕ].  (dMpair(i;j) = <i> ∧ <j> ∈ Point(dM(I))) supposing (j ∈ I and i ∈ I)
BY
{ Intros }

1
1. I : fset(ℕ)
2. i : ℕ
3. j : ℕ
4. i ∈ I
5. j ∈ I
⊢ dMpair(i;j) = <i> ∧ <j> ∈ Point(dM(I))


Latex:


Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[i,j:\mBbbN{}].    (dMpair(i;j)  =  <i>  \mwedge{}  <j>)  supposing  (j  \mmember{}  I  and  i  \mmember{}  I)


By


Latex:
Intros




Home Index