---

Step * 1 2 of Lemma continuous'-monotone-bunion


1. F : Type ⟶ Type
2. G : Type ⟶ Type
3. ∀[A,B:Type].  (F A) ⊆r (F B) supposing A ⊆r B
4. ∀[X:type-incr-chain{i:l}()]. ((F ⋃n:ℕ.(X n)) ⊆r ⋃n:ℕ.(F (X n)))
5. ∀[A,B:Type].  (G A) ⊆r (G B) supposing A ⊆r B
6. ∀[X:type-incr-chain{i:l}()]. ((G ⋃n:ℕ.(X n)) ⊆r ⋃n:ℕ.(G (X n)))
7. ∀[A,B:Type].  ((F A) ⋃ (G A)) ⊆r ((F B) ⋃ (G B)) supposing A ⊆r B
8. X : type-incr-chain{i:l}()
9. a1 : G ⋃n:ℕ.(X n)@i
⊢ a1 ∈ ⋃n:ℕ.((F (X n)) ⋃ (G (X n)))
BY
{ (RenameVar `z' (-1)
   THEN (Assert ⌜z ∈ ⋃n:ℕ.(G (X n))⌝⋅ THENA Auto)
   THEN Assert ⌜⋃n:ℕ.(G (X n)) ⊆r ⋃n:ℕ.((F (X n)) ⋃ (G (X n)))⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  F  :  Type  {}\mrightarrow{}  Type
2.  G  :  Type  {}\mrightarrow{}  Type
3.  \mforall{}[A,B:Type].    (F  A)  \msubseteq{}r  (F  B)  supposing  A  \msubseteq{}r  B
4.  \mforall{}[X:type-incr-chain\{i:l\}()].  ((F  \mcup{}n:\mBbbN{}.(X  n))  \msubseteq{}r  \mcup{}n:\mBbbN{}.(F  (X  n)))
5.  \mforall{}[A,B:Type].    (G  A)  \msubseteq{}r  (G  B)  supposing  A  \msubseteq{}r  B
6.  \mforall{}[X:type-incr-chain\{i:l\}()].  ((G  \mcup{}n:\mBbbN{}.(X  n))  \msubseteq{}r  \mcup{}n:\mBbbN{}.(G  (X  n)))
7.  \mforall{}[A,B:Type].    ((F  A)  \mcup{}  (G  A))  \msubseteq{}r  ((F  B)  \mcup{}  (G  B))  supposing  A  \msubseteq{}r  B
8.  X  :  type-incr-chain\{i:l\}()
9.  a1  :  G  \mcup{}n:\mBbbN{}.(X  n)@i
\mvdash{}  a1  \mmember{}  \mcup{}n:\mBbbN{}.((F  (X  n))  \mcup{}  (G  (X  n)))


By

---

Latex:
(RenameVar  `z'  (-1)
  THEN  (Assert  \mkleeneopen{}z  \mmember{}  \mcup{}n:\mBbbN{}.(G  (X  n))\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Assert  \mkleeneopen{}\mcup{}n:\mBbbN{}.(G  (X  n))  \msubseteq{}r  \mcup{}n:\mBbbN{}.((F  (X  n))  \mcup{}  (G  (X  n)))\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index