Step
*
1
1
1
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)])
⊢ ∃f:t:set-dom(A) ⟶ set-dom(B[set-item(A;t)])
∀z:coSet{i:l}. ((z ∈ x) ⇐⇒ ∃t:set-dom(A). seteq(z;(set-item(A;t),set-item(B[set-item(A;t)];f t))))
BY
{ (D 0 With ⌜λt.(fst(((λt.(fst(snd((g set-item(A;t) (m t)))))) t)))⌝ THENA Auto) }
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)])
⊢ ∀z:coSet{i:l}
((z ∈ x)
⇐⇒ ∃t:set-dom(A)
seteq(z;(set-item(A;t),set-item(B[set-item(A;t)];(λt.(fst(((λt.(fst(snd((g set-item(A;t) (m t)))))) t)))) t))))
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)])
\mvdash{} \mexists{}f:t:set-dom(A) {}\mrightarrow{} set-dom(B[set-item(A;t)])
\mforall{}z:coSet\{i:l\}
((z \mmember{} x) \mLeftarrow{}{}\mRightarrow{} \mexists{}t:set-dom(A). seteq(z;(set-item(A;t),set-item(B[set-item(A;t)];f t))))
By
Latex:
(D 0 With \mkleeneopen{}\mlambda{}t.(fst(((\mlambda{}t.(fst(snd((g set-item(A;t) (m t)))))) t)))\mkleeneclose{} THENA Auto)
Home
Index