---

Step * 1 1 1 1 of Lemma fdl-is-1_wf


1. X : Type
2. as : X List List@i
3. bs : X List List@i
4. (∀b∈as.(∃a∈bs. a ⊆ b))
⊢ (∃a∈as. ↑isaxiom(a)) ⇒ (∃a∈bs. ↑isaxiom(a))
BY
{ ((RWW "l_all_iff l_exists_iff" (-1) THENA Auto)
   THEN (RWW "l_all_iff l_exists_iff" 0 THENA Auto)
   THEN (D 0 THENA Auto)
   THEN ExRepD
   THEN (FHyp (-4) [-2] THENA Auto)
   THEN ParallelLast
   THEN Auto) }

1
1. X : Type
2. as : X List List@i
3. bs : X List List@i
4. ∀b:X List. ((b ∈ as) ⇒ (∃a:X List. ((a ∈ bs) ∧ a ⊆ b)))
5. a : X List@i
6. (a ∈ as)
7. ↑isaxiom(a)
8. a1 : X List
9. (a1 ∈ bs)
10. a1 ⊆ a
11. (a1 ∈ bs)
⊢ ↑isaxiom(a1)

---

Latex:

---

Latex:

1.  X  :  Type
2.  as  :  X  List  List@i
3.  bs  :  X  List  List@i
4.  (\mforall{}b\mmember{}as.(\mexists{}a\mmember{}bs.  a  \msubseteq{}  b))
\mvdash{}  (\mexists{}a\mmember{}as.  \muparrow{}isaxiom(a))  {}\mRightarrow{}  (\mexists{}a\mmember{}bs.  \muparrow{}isaxiom(a))


By

---

Latex:
((RWW  "l\_all\_iff  l\_exists\_iff"  (-1)  THENA  Auto)
  THEN  (RWW  "l\_all\_iff  l\_exists\_iff"  0  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  ExRepD
  THEN  (FHyp  (-4)  [-2]  THENA  Auto)
  THEN  ParallelLast
  THEN  Auto)

---

Home Index