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