Step
*
1
of Lemma
glued-first
1. [Info] : Type
2. es : EO+(Info)@i'
3. [A] : Type
4. [B] : Type
5. Ias : EClass(A) List@i'
6. Ibs : EClass(B) List@i'
7. f : E(first-class(Ias)) ─→ B@i
8. ((∀i:ℕ||Ias||. Ias[i]:λe,e'. e ≤loc e' →─f─→ Ibs[i]:λe,e'. e ≤loc e' )
⇒ first-class(Ias):λe,e'. e ≤loc e' →─f─→ first-class(Ibs):λe,e'. e ≤loc e'
supposing (∀Ia1,Ia2∈Ias. ∀e,e':E.
((¬((λe,e'. e ≤loc e' ) e e')) ∧ (¬((λe,e'. e ≤loc e' ) e' e))) supposing
((↑e' ∈b Ia2) and
(↑e ∈b Ia1)))) supposing
((||Ias|| = ||Ibs|| ∈ ℤ) and
(∀Ib1,Ib2∈Ibs. Ib1 ∩ Ib2 = 0) and
(∀Ia1,Ia2∈Ias. Ia1 ∩ Ia2 = 0))
9. (∀Ia1,Ia2∈Ias. ∀es:EO+(Info). ∀e,e':E. (¬(loc(e) = loc(e') ∈ Id)) supposing ((↑e' ∈b Ia2) and (↑e ∈b Ia1)))
10. (∀Ib1,Ib2∈Ibs. Ib1 ∩ Ib2 = 0)
11. ||Ias|| = ||Ibs|| ∈ ℤ
12. ∀i:ℕ||Ias||. glued(es;B;f;Ias[i];Ibs[i])@i
⊢ glued(es;B;f;first-class(Ias);first-class(Ibs))
BY
{ ((Using [`A',⌈A⌉] (BLemma `glued-Q-R-glued`)⋅ THENA Auto) THEN BackThruSomeHyp THEN Try (Trivial)) }
1
1. Info : Type
2. es : EO+(Info)@i'
3. A : Type
4. B : Type
5. Ias : EClass(A) List@i'
6. Ibs : EClass(B) List@i'
7. f : E(first-class(Ias)) ─→ B@i
8. ((∀i:ℕ||Ias||. Ias[i]:λe,e'. e ≤loc e' →─f─→ Ibs[i]:λe,e'. e ≤loc e' )
⇒ first-class(Ias):λe,e'. e ≤loc e' →─f─→ first-class(Ibs):λe,e'. e ≤loc e'
supposing (∀Ia1,Ia2∈Ias. ∀e,e':E.
((¬((λe,e'. e ≤loc e' ) e e')) ∧ (¬((λe,e'. e ≤loc e' ) e' e))) supposing
((↑e' ∈b Ia2) and
(↑e ∈b Ia1)))) supposing
((||Ias|| = ||Ibs|| ∈ ℤ) and
(∀Ib1,Ib2∈Ibs. Ib1 ∩ Ib2 = 0) and
(∀Ia1,Ia2∈Ias. Ia1 ∩ Ia2 = 0))
9. (∀Ia1,Ia2∈Ias. ∀es:EO+(Info). ∀e,e':E. (¬(loc(e) = loc(e') ∈ Id)) supposing ((↑e' ∈b Ia2) and (↑e ∈b Ia1)))
10. (∀Ib1,Ib2∈Ibs. Ib1 ∩ Ib2 = 0)
11. ||Ias|| = ||Ibs|| ∈ ℤ
12. ∀i:ℕ||Ias||. glued(es;B;f;Ias[i];Ibs[i])@i
⊢ (∀Ia1,Ia2∈Ias. Ia1 ∩ Ia2 = 0)
2
1. [Info] : Type
2. es : EO+(Info)@i'
3. [A] : Type
4. [B] : Type
5. Ias : EClass(A) List@i'
6. Ibs : EClass(B) List@i'
7. f : E(first-class(Ias)) ─→ B@i
8. ((∀i:ℕ||Ias||. Ias[i]:λe,e'. e ≤loc e' →─f─→ Ibs[i]:λe,e'. e ≤loc e' )
⇒ first-class(Ias):λe,e'. e ≤loc e' →─f─→ first-class(Ibs):λe,e'. e ≤loc e'
supposing (∀Ia1,Ia2∈Ias. ∀e,e':E.
((¬((λe,e'. e ≤loc e' ) e e')) ∧ (¬((λe,e'. e ≤loc e' ) e' e))) supposing
((↑e' ∈b Ia2) and
(↑e ∈b Ia1)))) supposing
((||Ias|| = ||Ibs|| ∈ ℤ) and
(∀Ib1,Ib2∈Ibs. Ib1 ∩ Ib2 = 0) and
(∀Ia1,Ia2∈Ias. Ia1 ∩ Ia2 = 0))
9. (∀Ia1,Ia2∈Ias. ∀es:EO+(Info). ∀e,e':E. (¬(loc(e) = loc(e') ∈ Id)) supposing ((↑e' ∈b Ia2) and (↑e ∈b Ia1)))
10. (∀Ib1,Ib2∈Ibs. Ib1 ∩ Ib2 = 0)
11. ||Ias|| = ||Ibs|| ∈ ℤ
12. ∀i:ℕ||Ias||. glued(es;B;f;Ias[i];Ibs[i])@i
⊢ ∀i:ℕ||Ias||. Ias[i]:λe,e'. e ≤loc e' →─f─→ Ibs[i]:λe,e'. e ≤loc e'
3
1. Info : Type
2. es : EO+(Info)@i'
3. A : Type
4. B : Type
5. Ias : EClass(A) List@i'
6. Ibs : EClass(B) List@i'
7. f : E(first-class(Ias)) ─→ B@i
8. ((∀i:ℕ||Ias||. Ias[i]:λe,e'. e ≤loc e' →─f─→ Ibs[i]:λe,e'. e ≤loc e' )
⇒ first-class(Ias):λe,e'. e ≤loc e' →─f─→ first-class(Ibs):λe,e'. e ≤loc e'
supposing (∀Ia1,Ia2∈Ias. ∀e,e':E.
((¬((λe,e'. e ≤loc e' ) e e')) ∧ (¬((λe,e'. e ≤loc e' ) e' e))) supposing
((↑e' ∈b Ia2) and
(↑e ∈b Ia1)))) supposing
((||Ias|| = ||Ibs|| ∈ ℤ) and
(∀Ib1,Ib2∈Ibs. Ib1 ∩ Ib2 = 0) and
(∀Ia1,Ia2∈Ias. Ia1 ∩ Ia2 = 0))
9. (∀Ia1,Ia2∈Ias. ∀es:EO+(Info). ∀e,e':E. (¬(loc(e) = loc(e') ∈ Id)) supposing ((↑e' ∈b Ia2) and (↑e ∈b Ia1)))
10. (∀Ib1,Ib2∈Ibs. Ib1 ∩ Ib2 = 0)
11. ||Ias|| = ||Ibs|| ∈ ℤ
12. ∀i:ℕ||Ias||. glued(es;B;f;Ias[i];Ibs[i])@i
⊢ (∀Ia1,Ia2∈Ias. ∀e,e':E.
((¬((λe,e'. e ≤loc e' ) e e')) ∧ (¬((λe,e'. e ≤loc e' ) e' e))) supposing ((↑e' ∈b Ia2) and (↑e ∈b I\000Ca1)))
Latex:
Latex:
1. [Info] : Type
2. es : EO+(Info)@i'
3. [A] : Type
4. [B] : Type
5. Ias : EClass(A) List@i'
6. Ibs : EClass(B) List@i'
7. f : E(first-class(Ias)) {}\mrightarrow{} B@i
8. ((\mforall{}i:\mBbbN{}||Ias||. Ias[i]:\mlambda{}e,e'. e \mleq{}loc e' \mrightarrow{}{}f{}\mrightarrow{} Ibs[i]:\mlambda{}e,e'. e \mleq{}loc e' )
{}\mRightarrow{} first-class(Ias):\mlambda{}e,e'. e \mleq{}loc e' \mrightarrow{}{}f{}\mrightarrow{} first-class(Ibs):\mlambda{}e,e'. e \mleq{}loc e'
supposing (\mforall{}Ia1,Ia2\mmember{}Ias. \mforall{}e,e':E.
((\mneg{}((\mlambda{}e,e'. e \mleq{}loc e' ) e e'))
\mwedge{} (\mneg{}((\mlambda{}e,e'. e \mleq{}loc e' ) e' e))) supposing
((\muparrow{}e' \mmember{}\msubb{} Ia2) and
(\muparrow{}e \mmember{}\msubb{} Ia1)))) supposing
((||Ias|| = ||Ibs||) and
(\mforall{}Ib1,Ib2\mmember{}Ibs. Ib1 \mcap{} Ib2 = 0) and
(\mforall{}Ia1,Ia2\mmember{}Ias. Ia1 \mcap{} Ia2 = 0))
9. (\mforall{}Ia1,Ia2\mmember{}Ias. \mforall{}es:EO+(Info). \mforall{}e,e':E.
(\mneg{}(loc(e) = loc(e'))) supposing ((\muparrow{}e' \mmember{}\msubb{} Ia2) and (\muparrow{}e \mmember{}\msubb{} Ia1)))
10. (\mforall{}Ib1,Ib2\mmember{}Ibs. Ib1 \mcap{} Ib2 = 0)
11. ||Ias|| = ||Ibs||
12. \mforall{}i:\mBbbN{}||Ias||. glued(es;B;f;Ias[i];Ibs[i])@i
\mvdash{} glued(es;B;f;first-class(Ias);first-class(Ibs))
By
Latex:
((Using [`A',\mkleeneopen{}A\mkleeneclose{}] (BLemma `glued-Q-R-glued`)\mcdot{} THENA Auto) THEN BackThruSomeHyp THEN Try (Trivial))
Home
Index