---

Step * 2 1 1 1 of Lemma equiv-equipollent-iff-quotient-equipollent


1. [A] : Type
2. [B] : Type
3. E : A ⟶ A ⟶ ℙ
4. [%] : EquivRel(A;x,y.E[x;y])
5. ∀f:A ⟶ B. ∀b:B.  SqStable(∃a:A. ((f a) = b ∈ B))
6. f : (x,y:A//E[x;y]) ⟶ B
7. Inj(x,y:A//E[x;y];B;f)
8. ∀b:B. ∃a:x,y:A//E[x;y]. ((f a) = b ∈ B)
9. b : B
10. a : x,y:A//E[x;y]
11. (f a) = b ∈ B
⊢ ∃a:A. ((f a) = b ∈ B)
BY
{ Assert ⌜↓∃a:A. ((f a) = b ∈ B)⌝⋅ }

1
.....assertion..... 
1. [A] : Type
2. [B] : Type
3. E : A ⟶ A ⟶ ℙ
4. [%] : EquivRel(A;x,y.E[x;y])
5. ∀f:A ⟶ B. ∀b:B.  SqStable(∃a:A. ((f a) = b ∈ B))
6. f : (x,y:A//E[x;y]) ⟶ B
7. Inj(x,y:A//E[x;y];B;f)
8. ∀b:B. ∃a:x,y:A//E[x;y]. ((f a) = b ∈ B)
9. b : B
10. a : x,y:A//E[x;y]
11. (f a) = b ∈ B
⊢ ↓∃a:A. ((f a) = b ∈ B)

2
1. [A] : Type
2. [B] : Type
3. E : A ⟶ A ⟶ ℙ
4. [%] : EquivRel(A;x,y.E[x;y])
5. ∀f:A ⟶ B. ∀b:B.  SqStable(∃a:A. ((f a) = b ∈ B))
6. f : (x,y:A//E[x;y]) ⟶ B
7. Inj(x,y:A//E[x;y];B;f)
8. ∀b:B. ∃a:x,y:A//E[x;y]. ((f a) = b ∈ B)
9. b : B
10. a : x,y:A//E[x;y]
11. (f a) = b ∈ B
12. ↓∃a:A. ((f a) = b ∈ B)
⊢ ∃a:A. ((f a) = b ∈ B)

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  E  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
4.  [\%]  :  EquivRel(A;x,y.E[x;y])
5.  \mforall{}f:A  {}\mrightarrow{}  B.  \mforall{}b:B.    SqStable(\mexists{}a:A.  ((f  a)  =  b))
6.  f  :  (x,y:A//E[x;y])  {}\mrightarrow{}  B
7.  Inj(x,y:A//E[x;y];B;f)
8.  \mforall{}b:B.  \mexists{}a:x,y:A//E[x;y].  ((f  a)  =  b)
9.  b  :  B
10.  a  :  x,y:A//E[x;y]
11.  (f  a)  =  b
\mvdash{}  \mexists{}a:A.  ((f  a)  =  b)


By

---

Latex:
Assert  \mkleeneopen{}\mdownarrow{}\mexists{}a:A.  ((f  a)  =  b)\mkleeneclose{}\mcdot{}

---

Home Index