---

Step * 1 1 of Lemma order-type-less-maximal


1. A : Type
2. < : A ⟶ A ⟶ ℙ
3. x3 : DCC(A;<)
4. x4 : Trans(A;x,y.x < y)
⊢ ∃f:A ⟶ (A:Type × <:A ⟶ A ⟶ ℙ × DCC(A;<))
   ∃b:A:Type × <:A ⟶ A ⟶ ℙ × DCC(A;<)
    (order-preserving(A;A:Type × <:A ⟶ A ⟶ ℙ × DCC(A;<);a1,a2.a1 < a2;b1,b2.let A,R,wf1 = b1 in 
    let B,S,wf2 = b2 in 
    ∃f:A ⟶ B. ∃b:B. (order-preserving(A;B;a1,a2.a1 R a2;b1,b2.b1 S b2;f) ∧ (∀a:A. ((f a) S b)));f)
    ∧ (∀a:A
         let A,R,wf1 = f a in 
         let B,S,wf2 = b in 
         ∃f:A ⟶ B. ∃b:B. (order-preserving(A;B;a1,a2.a1 R a2;b1,b2.b1 S b2;f) ∧ (∀a:A. ((f a) S b)))))
BY
{ xxxAssert ⌜∀a:A. DCC(b:A × (b < a);λp1,p2. ((fst(p1)) < (fst(p2))))⌝⋅xxx }

1
.....assertion..... 
1. A : Type
2. < : A ⟶ A ⟶ ℙ
3. x3 : DCC(A;<)
4. x4 : Trans(A;x,y.x < y)
⊢ ∀a:A. DCC(b:A × (b < a);λp1,p2. ((fst(p1)) < (fst(p2))))

2
1. A : Type
2. < : A ⟶ A ⟶ ℙ
3. x3 : DCC(A;<)
4. x4 : Trans(A;x,y.x < y)
5. ∀a:A. DCC(b:A × (b < a);λp1,p2. ((fst(p1)) < (fst(p2))))
⊢ ∃f:A ⟶ (A:Type × <:A ⟶ A ⟶ ℙ × DCC(A;<))
   ∃b:A:Type × <:A ⟶ A ⟶ ℙ × DCC(A;<)
    (order-preserving(A;A:Type × <:A ⟶ A ⟶ ℙ × DCC(A;<);a1,a2.a1 < a2;b1,b2.let A,R,wf1 = b1 in 
    let B,S,wf2 = b2 in 
    ∃f:A ⟶ B. ∃b:B. (order-preserving(A;B;a1,a2.a1 R a2;b1,b2.b1 S b2;f) ∧ (∀a:A. ((f a) S b)));f)
    ∧ (∀a:A
         let A,R,wf1 = f a in 
         let B,S,wf2 = b in 
         ∃f:A ⟶ B. ∃b:B. (order-preserving(A;B;a1,a2.a1 R a2;b1,b2.b1 S b2;f) ∧ (∀a:A. ((f a) S b)))))

---

Latex:

---

Latex:

1.  A  :  Type
2.  <  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  x3  :  DCC(A;<)
4.  x4  :  Trans(A;x,y.x  <  y)
\mvdash{}  \mexists{}f:A  {}\mrightarrow{}  (A:Type  \mtimes{}  <:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}  \mtimes{}  DCC(A;<))
      \mexists{}b:A:Type  \mtimes{}  <:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}  \mtimes{}  DCC(A;<)
        (order-preserving(A;A:Type  \mtimes{}  <:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}  \mtimes{}  DCC(A;<);a1,a2.a1  <  a2;b1,b2.let  A,R,wf1  =  b1  in 
        let  B,S,wf2  =  b2  in 
        \mexists{}f:A  {}\mrightarrow{}  B.  \mexists{}b:B.  (order-preserving(A;B;a1,a2.a1  R  a2;b1,b2.b1  S  b2;f)  \mwedge{}  (\mforall{}a:A.  ((f  a)  S  b)));f)
        \mwedge{}  (\mforall{}a:A
                  let  A,R,wf1  =  f  a  in 
                  let  B,S,wf2  =  b  in 
                  \mexists{}f:A  {}\mrightarrow{}  B
                    \mexists{}b:B.  (order-preserving(A;B;a1,a2.a1  R  a2;b1,b2.b1  S  b2;f)  \mwedge{}  (\mforall{}a:A.  ((f  a)  S  b)))))


By

---

Latex:
xxxAssert  \mkleeneopen{}\mforall{}a:A.  DCC(b:A  \mtimes{}  (b  <  a);\mlambda{}p1,p2.  ((fst(p1))  <  (fst(p2))))\mkleeneclose{}\mcdot{}xxx

---

Home Index