Step
*
1
1
of Lemma
id-fun-subtype
.....set predicate.....
1. A : Type
2. B : Type
3. ∀b:B. ∀a:A. ((b = a ∈ B)
⇒ (b = a ∈ A))
4. A ⊆r B
5. {b:B| ∃a:A. (b = a ∈ B)} ⊆r A
6. x : x:B ⟶ {y:B| x = y ∈ B}
7. a : A
⊢ a = (x a) ∈ A
BY
{ (GenConclAtAddr [3] THEN Auto)⋅ }
Latex:
Latex:
.....set predicate.....
1. A : Type
2. B : Type
3. \mforall{}b:B. \mforall{}a:A. ((b = a) {}\mRightarrow{} (b = a))
4. A \msubseteq{}r B
5. \{b:B| \mexists{}a:A. (b = a)\} \msubseteq{}r A
6. x : x:B {}\mrightarrow{} \{y:B| x = y\}
7. a : A
\mvdash{} a = (x a)
By
Latex:
(GenConclAtAddr [3] THEN Auto)\mcdot{}
Home
Index