Step
*
1
1
1
1
1
2
1
of Lemma
implies-setmem-piset
1. A : coSet{i:l}
2. ∀t:set-dom(A). (set-item(A;t) ∈ {a:coSet{i:l}| (a ∈ A)} )
3. B : {a:coSet{i:l}| (a ∈ A)} ⟶ coSet{i:l}
4. x : coSet{i:l}
5. ∀a1,a2:coSet{i:l}. ((a1 ∈ A) ⇒ (a2 ∈ A) ⇒ seteq(a1;a2) ⇒ seteq(B[a1];B[a2]))
6. (x ⊆ Σa:A.B[a])
7. g : ∀a:coSet{i:l}. ((a ∈ A) ⇒ (∃b:coSet{i:l}. ((b ∈ B[a]) ∧ ((a,b) ∈ x))))
8. ∀a,b1,b2:coSet{i:l}. ((a ∈ A) ⇒ (b1 ∈ B[a]) ⇒ (b2 ∈ B[a]) ⇒ ((a,b1) ∈ x) ⇒ ((a,b2) ∈ x) ⇒ seteq(b1;b2))
9. m : ∀t:set-dom(A). (set-item(A;t) ∈ A)
10. λt.(fst((g set-item(A;t) (m t)))) ∈ t:set-dom(A) ⟶ coSet{i:l}
11. λt.(snd((g set-item(A;t) (m t)))) ∈ t:set-dom(A) ⟶ ((fst((g set-item(A;t) (m t))) ∈ B[set-item(A;t)])
∧ ((set-item(A;t),fst((g set-item(A;t) (m t)))) ∈ x))
12. λt.(fst(snd((g set-item(A;t) (m t))))) ∈ t:set-dom(A) ⟶ (fst((g set-item(A;t) (m t))) ∈ B[set-item(A;t)])
13. λt.(fst(((λt.(fst(snd((g set-item(A;t) (m t)))))) t))) ∈ t:set-dom(A) ⟶ set-dom(B[set-item(A;t)])
14. z : coSet{i:l}
15. t : set-dom(A)
16. b : coSet{i:l}
17. v2 : (b ∈ B[set-item(A;t)])
18. v3 : ((set-item(A;t),b) ∈ x)
⊢ seteq(z;(set-item(A;t),set-item(B[set-item(A;t)];fst(v2)))) ⇒ (z ∈ x)
BY
{ (MoveToConcl (-2)
THEN (GenConclTerm ⌜B[set-item(A;t)]⌝⋅ THENA Auto)
THEN coSetD (-2)
THEN D -2
THEN All (Fold `mk-coset`)) }
1
1. A : coSet{i:l}
2. ∀t:set-dom(A). (set-item(A;t) ∈ {a:coSet{i:l}| (a ∈ A)} )
3. B : {a:coSet{i:l}| (a ∈ A)} ⟶ coSet{i:l}
4. x : coSet{i:l}
5. ∀a1,a2:coSet{i:l}. ((a1 ∈ A) ⇒ (a2 ∈ A) ⇒ seteq(a1;a2) ⇒ seteq(B[a1];B[a2]))
6. (x ⊆ Σa:A.B[a])
7. g : ∀a:coSet{i:l}. ((a ∈ A) ⇒ (∃b:coSet{i:l}. ((b ∈ B[a]) ∧ ((a,b) ∈ x))))
8. ∀a,b1,b2:coSet{i:l}. ((a ∈ A) ⇒ (b1 ∈ B[a]) ⇒ (b2 ∈ B[a]) ⇒ ((a,b1) ∈ x) ⇒ ((a,b2) ∈ x) ⇒ seteq(b1;b2))
9. m : ∀t:set-dom(A). (set-item(A;t) ∈ A)
10. λt.(fst((g set-item(A;t) (m t)))) ∈ t:set-dom(A) ⟶ coSet{i:l}
11. λt.(snd((g set-item(A;t) (m t)))) ∈ t:set-dom(A) ⟶ ((fst((g set-item(A;t) (m t))) ∈ B[set-item(A;t)])
∧ ((set-item(A;t),fst((g set-item(A;t) (m t)))) ∈ x))
12. λt.(fst(snd((g set-item(A;t) (m t))))) ∈ t:set-dom(A) ⟶ (fst((g set-item(A;t) (m t))) ∈ B[set-item(A;t)])
13. λt.(fst(((λt.(fst(snd((g set-item(A;t) (m t)))))) t))) ∈ t:set-dom(A) ⟶ set-dom(B[set-item(A;t)])
14. z : coSet{i:l}
15. t : set-dom(A)
16. b : coSet{i:l}
17. v3 : ((set-item(A;t),b) ∈ x)
18. T : Type
19. v4 : T ⟶ coSet{i:l}
20. B[set-item(A;t)] = mk-coset(T;v4) ∈ coSet{i:l}
⊢ ∀v2:(b ∈ mk-coset(T;v4)). (seteq(z;(set-item(A;t),set-item(mk-coset(T;v4);fst(v2)))) ⇒ (z ∈ x))
Latex:
Latex:
1. A : coSet\{i:l\}
2. \mforall{}t:set-dom(A). (set-item(A;t) \mmember{} \{a:coSet\{i:l\}| (a \mmember{} A)\} )
3. B : \{a:coSet\{i:l\}| (a \mmember{} A)\} {}\mrightarrow{} coSet\{i:l\}
4. x : coSet\{i:l\}
5. \mforall{}a1,a2:coSet\{i:l\}. ((a1 \mmember{} A) {}\mRightarrow{} (a2 \mmember{} A) {}\mRightarrow{} seteq(a1;a2) {}\mRightarrow{} seteq(B[a1];B[a2]))
6. (x \msubseteq{} \mSigma{}a:A.B[a])
7. g : \mforall{}a:coSet\{i:l\}. ((a \mmember{} A) {}\mRightarrow{} (\mexists{}b:coSet\{i:l\}. ((b \mmember{} B[a]) \mwedge{} ((a,b) \mmember{} x))))
8. \mforall{}a,b1,b2:coSet\{i:l\}.
((a \mmember{} A) {}\mRightarrow{} (b1 \mmember{} B[a]) {}\mRightarrow{} (b2 \mmember{} B[a]) {}\mRightarrow{} ((a,b1) \mmember{} x) {}\mRightarrow{} ((a,b2) \mmember{} x) {}\mRightarrow{} seteq(b1;b2))
9. m : \mforall{}t:set-dom(A). (set-item(A;t) \mmember{} A)
10. \mlambda{}t.(fst((g set-item(A;t) (m t)))) \mmember{} t:set-dom(A) {}\mrightarrow{} coSet\{i:l\}
11. \mlambda{}t.(snd((g set-item(A;t) (m t)))) \mmember{} t:set-dom(A)
{}\mrightarrow{} ((fst((g set-item(A;t) (m t))) \mmember{} B[set-item(A;t)])
\mwedge{} ((set-item(A;t),fst((g set-item(A;t) (m t)))) \mmember{} x))
12. \mlambda{}t.(fst(snd((g set-item(A;t) (m t))))) \mmember{} t:set-dom(A)
{}\mrightarrow{} (fst((g set-item(A;t) (m t))) \mmember{} B[set-item(A;t)])
13. \mlambda{}t.(fst(((\mlambda{}t.(fst(snd((g set-item(A;t) (m t)))))) t))) \mmember{} t:set-dom(A)
{}\mrightarrow{} set-dom(B[set-item(A;t)])
14. z : coSet\{i:l\}
15. t : set-dom(A)
16. b : coSet\{i:l\}
17. v2 : (b \mmember{} B[set-item(A;t)])
18. v3 : ((set-item(A;t),b) \mmember{} x)
\mvdash{} seteq(z;(set-item(A;t),set-item(B[set-item(A;t)];fst(v2)))) {}\mRightarrow{} (z \mmember{} x)
By
Latex:
(MoveToConcl (-2)
THEN (GenConclTerm \mkleeneopen{}B[set-item(A;t)]\mkleeneclose{}\mcdot{} THENA Auto)
THEN coSetD (-2)
THEN D -2
THEN All (Fold `mk-coset`))
Home
Index