---

Step * 1 of Lemma continuous'-monotone-bunion

.....subterm..... T:t
1:n
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. x : (F ⋃n:ℕ.(X n)) ⋃ (G ⋃n:ℕ.(X n))@i
⊢ x ∈ ⋃n:ℕ.((F (X n)) ⋃ (G (X n)))
BY
{ D_b_union (-1) }

1
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 : F ⋃n:ℕ.(X n)@i
⊢ a1 ∈ ⋃n:ℕ.((F (X n)) ⋃ (G (X n)))

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

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
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.  x  :  (F  \mcup{}n:\mBbbN{}.(X  n))  \mcup{}  (G  \mcup{}n:\mBbbN{}.(X  n))@i
\mvdash{}  x  \mmember{}  \mcup{}n:\mBbbN{}.((F  (X  n))  \mcup{}  (G  (X  n)))


By

---

Latex:
D\_b\_union  (-1)

---

Home Index