---

Step * 1 1 of Lemma dMpair-eq-meet


1. I : fset(ℕ)
2. i : ℕ
3. j : ℕ
4. i ∈ I
5. j ∈ I
⊢ {{inl i,inl j}}
= fset-ac-glb(union-deq(names(I);names(I);NamesDeq;NamesDeq);<i>;<j>)
∈ fset(fset(names(I) + names(I)))
BY
{ ((RepUR ``dminc free-dl-inc`` 0
    THEN (GenConcl ⌜(inl i) = x ∈ (names(I) + names(I))⌝⋅ THENA Auto)
    THEN (GenConcl ⌜(inl j) = y ∈ (names(I) + names(I))⌝⋅ THENA Auto))
   THEN RepUR ``fset-ac-glb`` 0
   THEN RepUR ``f-union`` 0
   THEN ((RWO "fset-image-singleton" 0 THENM RepUR ``fset-singleton`` 0) THENA Auto)
   THEN Fold `fset-singleton` 0
   THEN Fold `empty-fset` 0
   THEN (RWO "empty-fset-union" 0 THENA Auto)) }

1
1. I : fset(ℕ)
2. i : ℕ
3. j : ℕ
4. i ∈ I
5. j ∈ I
6. x : names(I) + names(I)
7. (inl i) = x ∈ (names(I) + names(I))
8. y : names(I) + names(I)
9. (inl j) = y ∈ (names(I) + names(I))
⊢ {{x,y}}
= fset-minimals(xs,ys.f-proper-subset-dec(union-deq(names(I);names(I);NamesDeq;NamesDeq);xs;ys); {{x} ⋃ {y}})
∈ fset(fset(names(I) + names(I)))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  i  :  \mBbbN{}
3.  j  :  \mBbbN{}
4.  i  \mmember{}  I
5.  j  \mmember{}  I
\mvdash{}  \{\{inl  i,inl  j\}\}  =  fset-ac-glb(union-deq(names(I);names(I);NamesDeq;NamesDeq);<i><j>)


By

---

Latex:
((RepUR  ``dminc  free-dl-inc``  0
    THEN  (GenConcl  \mkleeneopen{}(inl  i)  =  x\mkleeneclose{}\mcdot{}  THENA  Auto)
    THEN  (GenConcl  \mkleeneopen{}(inl  j)  =  y\mkleeneclose{}\mcdot{}  THENA  Auto))
  THEN  RepUR  ``fset-ac-glb``  0
  THEN  RepUR  ``f-union``  0
  THEN  ((RWO  "fset-image-singleton"  0  THENM  RepUR  ``fset-singleton``  0)  THENA  Auto)
  THEN  Fold  `fset-singleton`  0
  THEN  Fold  `empty-fset`  0
  THEN  (RWO  "empty-fset-union"  0  THENA  Auto))

---

Home Index