Home(or GIF version for IE).
| Home |
Metamath Proof Explorer | < Previous Next > |
| Bad symbols?
Use Mozilla (or GIF version for IE). |
| Color key: | Metamath Proof
Explorer
(1-4957)
|
Hilbert Space Explorer
(4958-5787)
|
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | er2 3201 | Alternate definition of equivalence predicate. |
| ⊢ (Er R ↔ ∀x∀y∀z((xRy → yRx) ∧ ((xRy ∧ yRz) → xRz))) | ||
| Definition | df-ec 3202 | Define the R -coset of A. Exercise 35 of [Enderton] p. 61. This is called the equivalence class of A modulo R when R is an equivalence relation. The Definition of [Enderton] p. 57 uses the notation [A] (subscript) R, although we simply follow the brackets by R since we don't have subscripts. For an alternate definition, see ec2 3203. |
| ⊢ [A]R = (R “ {A}) | ||
| Theorem | ec2 3203 | Alternate definition of R-coset of A. Definition 34 of [Suppes] p. 81. |
| ⊢ A ∈ V ⇒ ⊢ [A]R = {y∣ARy} | ||
| Theorem | ecexg 3204 | An equivalence class modulo a set is a set. |
| ⊢ (R ∈ B → [A]R ∈ V) | ||
| Definition | df-qs 3205 | Define quotient set. R is usually an equivalence relation. Definition of [Enderton] p. 58. |
| ⊢ (A / R) = {y∣∃x ∈ A y = [x]R} | ||
| Theorem | ereq 3206 | Equality theorem for equivalence predicate. |
| ⊢ (R = S → (Er R ↔ Er S)) | ||
| Theorem | ster 3207 | A symmetric, transitive relation is an equivalence relation. |
| ⊢ (xRy → yRx) & ⊢ ((xRy ∧ yRz) → xRz) ⇒ ⊢ Er R | ||
| Theorem | ider 3208 | The identity relation is an equivalence relation. |
| ⊢ Er I | ||
| Theorem | ersym 3209 | An equivalence relation is symmetric. |
| ⊢ A ∈ V & ⊢ B ∈ V & ⊢ Er R ⇒ ⊢ (ARB → BRA) | ||
| Theorem | ersymb 3210 | An equivalence relation is symmetric. |
| ⊢ A ∈ V & ⊢ B ∈ V & ⊢ Er R ⇒ ⊢ (ARB ↔ BRA) | ||
| Theorem | ertr 3211 | An equivalence relation is transitive. |
| ⊢ A ∈ V & ⊢ B ∈ V & ⊢ C ∈ V & ⊢ Er R ⇒ ⊢ ((ARB ∧ BRC) → ARC) | ||
| Theorem | erref 3212 | An equivalence relation is reflexive on its field. Compare Theorem 3M of [Enderton] p. 56. |
| ⊢ Er R ⇒ ⊢ (A ∈ (dom R ∪ ran R) → ARA) | ||
| Theorem | erdmrn 3213 | The range and domain of an equivalence relation are equal. |
| ⊢ Er R ⇒ ⊢ dom R = ran R | ||
| Theorem | eceq1 3214 | Equality theorem for equivalence class. |
| ⊢ (A = B → [C]A = [C]B) | ||
| Theorem | eceq2 3215 | Equality theorem for equivalence class. |
| ⊢ (A = B → [A]C = [B]C) | ||
| Theorem | elec 3216 | Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. |
| ⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (A ∈ [B]R ↔ BRA) | ||
| Theorem | ecdmn0 3217 | An equivalence class is not empty in its domain. |
| ⊢ A ∈ V ⇒ ⊢ (A ∈ dom R ↔ ¬ [A]R = ∅) | ||
| Theorem | erthi 3218 | Basic property of equivalence relations. Part of Lemma 3N of [Enderton] p. 57. |
| ⊢ A ∈ V & ⊢ B ∈ V & ⊢ Er R ⇒ ⊢ (ARB → [A]R = [B]R) | ||
| Theorem | erth 3219 | Basic property of equivalence relations. Theorem 73 of [Suppes] p. 82. |
| ⊢ B ∈ V & ⊢ Er R ⇒ ⊢ (A ∈ (dom R ∪ ran R) → ([A]R = [B]R ↔ ARB)) | ||
| Theorem | erthdm 3220 | Basic property of equivalence relations. Compare Theorem 73 of [Suppes] p. 82. Assumes membership in the domain instead of just the field. |
| ⊢ B ∈ V & ⊢ Er R ⇒ ⊢ (A ∈ dom R → ([A]R = [B]R ↔ ARB)) | ||
| Theorem | erthdmr 3221 | Basic property of equivalence relations. Compare Theorem 73 of [Suppes] p. 82. Assumes membership of the second argument in the domain. |
| ⊢ A ∈ V & ⊢ B ∈ V & ⊢ Er R ⇒ ⊢ (B ∈ dom R → ([A]R = [B]R ↔ ARB)) | ||
| Theorem | ereldm 3222 | Equality of equivalence classes implies equivalence of domain membership. |
| ⊢ A ∈ V & ⊢ B ∈ V & ⊢ Er R & ⊢ dom R = D ⇒ ⊢ ([A]R = [B]R → (A ∈ D ↔ B ∈ D)) | ||
| Theorem | erdisj 3223 | Equivalence classes do not overlap. In other words, two equivalence classes are either equal or disjoint. Theorem 74 of [Suppes] p. 83. |
| ⊢ A ∈ V & ⊢ B ∈ V & ⊢ Er R ⇒ ⊢ ([A]R = [B]R ∨ ([A]R ∩ [B]R) = ∅) | ||
| Theorem | ecidsn 3224 | An equivalence class modulo the identity relation is a singleton. |
| ⊢ [A]I = {A} | ||
| Theorem | qseq1 3225 | Equality theorem for quotient set. |
| ⊢ (A = B → (A / C) = (B / C)) | ||
| Theorem | qseq2 3226 | Equality theorem for quotient set. |
| ⊢ (A = B → (C / A) = (C / B)) | ||
| Theorem | elqs 3227 | Membership in a quotient set. |
| ⊢ B ∈ V ⇒ ⊢ (B ∈ (A / R) ↔ ∃x(x ∈ A ∧ B = [x]R)) | ||
| Theorem | elqsi 3228 | Membership in a quotient set. |
| ⊢ (B ∈ (A / R) → ∃x(x ∈ A ∧ B = [x]R)) | ||
| Theorem | ecelqsi 3229 | Membership of an equivalence class in a quotient set. |
| ⊢ R ∈ V ⇒ ⊢ (B ∈ A → [B]R ∈ (A / R)) | ||
| Theorem | ecopqsi 3230 | "Closure" law for equivalence class of ordered pairs. |
| ⊢ R ∈ V & ⊢ S = ((A × A) / R) ⇒ ⊢ ((B ∈ A ∧ C ∈ A) → [⟨B, C⟩]R ∈ S) | ||
| Theorem | qsex 3231 | A quotient set exists. |
| ⊢ A ∈ V ⇒ ⊢ (A / R) ∈ V | ||
| Theorem | snec 3232 | The singleton of an equivalence class. |
| ⊢ A ∈ V ⇒ ⊢ {[A]R} = ({A} / R) | ||
| Theorem | ecqs 3233 | Equivalence class in terms of quotient set. |
| ⊢ A ∈ V & ⊢ R ∈ V ⇒ ⊢ [A]R = ∪({A} / R) | ||
| Theorem | 0nelqs 3234 | A quotient set doesn't contain the empty set. |
| ⊢ Er R & ⊢ dom R = A ⇒ ⊢ ¬ ∅ ∈ (A / R) | ||
| Theorem | ecelqsdm 3235 | Membership of an equivalence class in a quotient set. |
| ⊢ B ∈ V & ⊢ Er R & ⊢ dom R = A ⇒ ⊢ ([B]R ∈ (A / R) → B ∈ A) | ||
| Theorem | ecid 3236 | A set is equal to its converse epsilon coset. (Note: converse epsilon is not an equivalence relation.) |
| ⊢ A ∈ V ⇒ ⊢ [A]◡E = A | ||
| Theorem | qsid 3237 | A set is equal to its quotient set mod converse epsilon. (Note: converse epsilon is not an equivalence relation.) |
| ⊢ A ∈ V ⇒ ⊢ (A / ◡E) = A | ||
| Theorem | ectocl 3238 | Implicit substitution of class for equivalence class. |
| ⊢ S = (B / R) & ⊢ ([x]R = A → (φ ↔ ψ)) & ⊢ (x ∈ B → φ) ⇒ ⊢ (A ∈ S → ψ) | ||
| Theorem | ecoptocl 3239 | Implicit substitution of class for equivalence class of ordered pair. |
| ⊢ S = ((B × C) / R) & ⊢ ([⟨x, y⟩]R = A → (φ ↔ ψ)) & ⊢ ((x ∈ B ∧ y ∈ C) → φ) ⇒ ⊢ (A ∈ S → ψ) | ||
| Theorem | 2ecoptocl 3240 | Implicit substitution of classes for equivalence classes of ordered pairs. |
| ⊢ S = ((C × D) / R) & ⊢ ([⟨x, y⟩]R = A → (φ ↔ ψ)) & ⊢ ([⟨z, w⟩]R = B → (ψ ↔ χ)) & ⊢ (((x ∈ C ∧ y ∈ D) ∧ (z ∈ C ∧ w ∈ D)) → φ) ⇒ ⊢ ((A ∈ S ∧ B ∈ S) → χ) | ||
| Theorem | 3ecoptocl 3241 | Implicit substitution of classes for equivalence classes of ordered pairs. |
| ⊢ S = ((D × D) / R) & ⊢ ([⟨x, y⟩]R = A → (φ ↔ ψ)) & ⊢ ([⟨z, w⟩]R = B → (ψ ↔ χ)) & ⊢ ([⟨v, u⟩]R = C → (χ ↔ θ)) & ⊢ (((x ∈ D ∧ y ∈ D) ∧ (z ∈ D ∧ w ∈ D) ∧ (v ∈ D ∧ u ∈ D)) → φ) ⇒ ⊢ ((A ∈ S ∧ B ∈ S ∧ C ∈ S) → θ) | ||
| Theorem | brecop 3242 | Binary relation on a quotient set. Lemma for real number construction. |
| ⊢ S ∈ V & ⊢ Er S & ⊢ dom S = (G × G) & ⊢ H = ((G × G) / S) & ⊢ R = {⟨x, y⟩∣((x ∈ H ∧ y ∈ H) ∧ ∃z∃w∃v∃u((x = [⟨z, w⟩]S ∧ y = [⟨v, u⟩]S) ∧ φ))} & ⊢ ((((z ∈ G ∧ w ∈ G) ∧ (A ∈ G ∧ B ∈ G)) ∧ ((v ∈ G ∧ u ∈ G) ∧ (C ∈ G ∧ D ∈ G))) → (([⟨z, w⟩]S = [⟨A, B⟩]S ∧ [⟨v, u⟩]S = [⟨C, D⟩]S) → (φ ↔ ψ))) ⇒ ⊢ (((A ∈ G ∧ B ∈ G) ∧ (C ∈ G ∧ D ∈ G)) → ([⟨A, B⟩]SR[⟨C, D⟩]S ↔ ψ)) | ||
| Theorem | brecop2 3243 | Binary relation on a quotient set. Lemma for real number construction. Eliminates antecedent from last hypothesis. |
| ⊢ S ∈ V & ⊢ B ∈ V & ⊢ C ∈ V & ⊢ D ∈ V & ⊢ Er S & ⊢ dom S = (G × G) & ⊢ H = ((G × G) / S) & ⊢ R ⊆ (H × H) & ⊢ Q ⊆ (G × G) & ⊢ ¬ ∅ ∈ G & ⊢ dom F = (G × G) & ⊢ (((A ∈ G ∧ B ∈ G) ∧ (C ∈ G ∧ D ∈ G)) → ([⟨A, B⟩]SR[⟨C, D⟩]S ↔ (AFD)Q(BFC))) ⇒ ⊢ ([⟨A, B⟩]SR[⟨C, D⟩]S ↔ (AFD)Q(BFC)) | ||
| Theorem | ecopopreq 3244 | Express the relation R (specified by the hypothesis) in terms of its operation F. |
| ⊢ R = {⟨x, y⟩∣((x ∈ (S × S) ∧ y ∈ (S × S)) ∧ ∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (zFu) = (wFv)))} ⇒ ⊢ (((A ∈ S ∧ B ∈ S) ∧ (C ∈ S ∧ D ∈ S)) → (⟨A, B⟩R⟨C, D⟩ ↔ (AFD) = (BFC))) | ||
| Theorem | ecopoprdm 3245 | Assuming the operation F is commutative, compute the domain the relation R specified by the first hypothesis. |
| ⊢ R = {⟨x, y⟩∣((x ∈ (S × S) ∧ y ∈ (S × S)) ∧ ∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (zFu) = (wFv)))} & ⊢ (xFy) = (yFx) ⇒ ⊢ dom R = (S × S) | ||
| Theorem | ecopoprsym 3246 | Assuming the operation F is commutative, show that the relation R, specified by the first hypothesis, is symmetric. |
| ⊢ R = {⟨x, y⟩∣((x ∈ (S × S) ∧ y ∈ (S × S)) ∧ ∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (zFu) = (wFv)))} & ⊢ (xFy) = (yFx) & ⊢ B ∈ V ⇒ ⊢ (ARB → BRA) | ||
| Theorem | ecopoprtrn 3247 | Assuming that operation F is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation R, specified by the first hypothesis, is transitive. |
| ⊢ R = {⟨x, y⟩∣((x ∈ (S × S) ∧ y ∈ (S × S)) ∧ ∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (zFu) = (wFv)))} & ⊢ (xFy) = (yFx) & ⊢ ((x ∈ S ∧ y ∈ S) → (xFy) ∈ S) & ⊢ ((xFy)Fz) = (xF(yFz)) & ⊢ ((x ∈ S ∧ y ∈ S) → ((xFy) = (xFz) → y = z)) & ⊢ B ∈ V & ⊢ C ∈ V ⇒ ⊢ ((ARB ∧ BRC) → ARC) | ||
| Theorem | ecopoprer 3248 | Assuming that operation F is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation R, specified by the first hypothesis, is an equivalence relation. |
| ⊢ R = {⟨x, y⟩∣((x ∈ (S × S) ∧ y ∈ (S × S)) ∧ ∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ (zFu) = (wFv)))} & ⊢ (xFy) = (yFx) & ⊢ ((x ∈ S ∧ y ∈ S) → (xFy) ∈ S) & ⊢ ((xFy)Fz) = (xF(yFz)) & ⊢ ((x ∈ S ∧ y ∈ S) → ((xFy) = (xFz) → y = z)) ⇒ ⊢ Er R | ||
| Theorem | eceqopreq 3249 | Equality of equivalence relation in terms of an operation. |
| ⊢ B ∈ V & ⊢ C ∈ V & ⊢ D ∈ V & ⊢ Er R & ⊢ dom R = (S × S) & ⊢ dom F = (S × S) & ⊢ ¬ ∅ ∈ S & ⊢ ((x ∈ S ∧ y ∈ S) → (xFy) ∈ S) & ⊢ (((A ∈ S ∧ B ∈ S) ∧ (C ∈ S ∧ D ∈ S)) → (⟨A, B⟩R⟨C, D⟩ ↔ (AFD) = (BFC))) ⇒ ⊢ ((A ∈ S ∧ C ∈ S) → ([⟨A, B⟩]R = [⟨C, D⟩]R ↔ (AFD) = (BFC))) | ||
| Theorem | th3qlem1 3250 | Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60. The third hypothesis is the compatibility assumption. |
| ⊢ Er R & ⊢ dom R = S & ⊢ (((y ∈ S ∧ w ∈ S) ∧ (z ∈ S ∧ v ∈ S)) → ((yRw ∧ zRv) → (yFz)R(wFv))) ⇒ ⊢ ((A ∈ (S / R) ∧ B ∈ (S / R)) → ∃*x∃y∃z((A = [y]R ∧ B = [z]R) ∧ x = [(yFz)]R)) | ||
| Theorem | th3qlem2 3251 | Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60, extended to operations on ordered pairs. The fourth hypothesis is the compatibility assumption. |
| ⊢ R ∈ V & ⊢ Er R & ⊢ dom R = (S × S) & ⊢ ((((w ∈ S ∧ v ∈ S) ∧ (u ∈ S ∧ t ∈ S)) ∧ ((s ∈ S ∧ f ∈ S) ∧ (g ∈ S ∧ h ∈ S))) → ((⟨w, v⟩R⟨u, t⟩ ∧ ⟨s, f⟩R⟨g, h⟩) → (⟨w, v⟩F⟨s, f⟩)R(⟨u, t⟩F⟨g, h⟩))) ⇒ ⊢ ((A ∈ ((S × S) / R) ∧ B ∈ ((S × S) / R)) → ∃*z∃w∃v∃u∃t((A = [⟨w, v⟩]R ∧ B = [⟨u, t⟩]R) ∧ z = [(⟨w, v⟩F⟨u, t⟩)]R)) | ||
| Theorem | th3qcor 3252 | Corollary of Theorem 3Q of [Enderton] p. 60. |
| ⊢ R ∈ V & ⊢ Er R & ⊢ dom R = (S × S) & ⊢ ((((w ∈ S ∧ v ∈ S) ∧ (u ∈ S ∧ t ∈ S)) ∧ ((s ∈ S ∧ f ∈ S) ∧ (g ∈ S ∧ h ∈ S))) → ((⟨w, v⟩R⟨u, t⟩ ∧ ⟨s, f⟩R⟨g, h⟩) → (⟨w, v⟩F⟨s, f⟩)R(⟨u, t⟩F⟨g, h⟩))) & ⊢ G = {⟨⟨x, y⟩, z⟩∣((x ∈ ((S × S) / R) ∧ y ∈ ((S × S) / R)) ∧ ∃w∃v∃u∃t((x = [⟨w, v⟩]R ∧ y = [⟨u, t⟩]R) ∧ z = [(⟨w, v⟩F⟨u, t⟩)]R))} ⇒ ⊢ Fun G | ||
| Theorem | th3q 3253 | Theorem 3Q of [Enderton] p. 60, extended to operations on ordered pairs. |
| ⊢ R ∈ V & ⊢ Er R & ⊢ dom R = (S × S) & ⊢ ((((w ∈ S ∧ v ∈ S) ∧ (u ∈ S ∧ t ∈ S)) ∧ ((s ∈ S ∧ f ∈ S) ∧ (g ∈ S ∧ h ∈ S))) → ((⟨w, v⟩R⟨u, t⟩ ∧ ⟨s, f⟩R⟨g, h⟩) → (⟨w, v⟩F⟨s, f⟩)R(⟨u, t⟩F⟨g, h⟩))) & ⊢ G = {⟨⟨x, y⟩, z⟩∣((x ∈ ((S × S) / R) ∧ y ∈ ((S × S) / R)) ∧ ∃w∃v∃u∃t((x = [⟨w, v⟩]R ∧ y = [⟨u, t⟩]R) ∧ z = [(⟨w, v⟩F⟨u, t⟩)]R))} ⇒ ⊢ (((A ∈ S ∧ B ∈ S) ∧ (C ∈ S ∧ D ∈ S)) → ([⟨A, B⟩]RG[⟨C, D⟩]R) = [(⟨A, B⟩F⟨C, D⟩)]R) | ||
| Theorem | oprec 3254 | Express an operation on equivalence classes of ordered pairs in terms of equivalence class of operations on ordered pairs. |
| ⊢ H ∈ V & ⊢ K ∈ V & ⊢ L ∈ V & ⊢ R ∈ V & ⊢ Er R & ⊢ dom R = (S × S) & ⊢ R = {⟨x, y⟩∣((x ∈ (S × S) ∧ y ∈ (S × S)) ∧ ∃z∃w∃v∃u((x = ⟨z, w⟩ ∧ y = ⟨v, u⟩) ∧ φ))} & ⊢ (((z = a ∧ w = b) ∧ (v = c ∧ u = d)) → (φ ↔ ψ)) & ⊢ (((z = g ∧ w = h) ∧ (v = t ∧ u = s)) → (φ ↔ χ)) & ⊢ G = {⟨⟨x, y⟩, z⟩∣((x ∈ (S × S) ∧ y ∈ (S × S)) ∧ ∃w∃v∃u∃f((x = ⟨w, v⟩ ∧ y = ⟨u, f⟩) ∧ z = J))} & ⊢ (((w = a ∧ v = b) ∧ (u = g ∧ f = h)) → J = K) & ⊢ (((w = c ∧ v = d) ∧ (u = t ∧ f = s)) → J = L) & ⊢ (((w = A ∧ v = B) ∧ (u = C ∧ f = D)) → J = H) & ⊢ F = {⟨⟨x, y⟩, z⟩∣((x ∈ Q ∧ y ∈ Q) ∧ ∃a∃b∃c∃d((x = [⟨a, b⟩]R ∧ y = [⟨c, d⟩]R) ∧ z = [(⟨a, b⟩G⟨c, d⟩)]R))} & ⊢ Q = ((S × S) / R) & ⊢ ((((a ∈ S ∧ b ∈ S) ∧ (c ∈ S ∧ d ∈ S)) ∧ ((g ∈ S ∧ h ∈ S) ∧ (t ∈ S ∧ s ∈ S))) → ((ψ ∧ χ) → KRL)) ⇒ ⊢ (((A ∈ S ∧ B ∈ S) ∧ (C ∈ S ∧ D ∈ S)) → ([⟨A, B⟩]RF[⟨C, D⟩]R) = [H]R) | ||
| Theorem | ecoprcom 3255 | Lemma used in proving commutative laws via equivalence classes. |
| ⊢ C = ((S × S) / R) & ⊢ (((x ∈ S ∧ y ∈ S) ∧ (z ∈ S ∧ w ∈ S)) → ([⟨x, y⟩]RF[⟨z, w⟩]R) = [⟨D, G⟩]R) & ⊢ (((z ∈ S ∧ w ∈ S) ∧ (x ∈ S ∧ y ∈ S)) → ([⟨z, w⟩]RF[⟨x, y⟩]R) = [⟨H, J⟩]R) & ⊢ D = H & ⊢ G = J ⇒ ⊢ ((A ∈ C ∧ B ∈ C) → (AFB) = (BFA)) | ||
| Theorem | ecoprass 3256 | Lemma used in proving associative laws via equivalence classes. |
| ⊢ D = ((S × S) / R) & ⊢ (((x ∈ S ∧ y ∈ S) ∧ (z ∈ S ∧ w ∈ S)) → ([⟨x, y⟩]RF[⟨z, w⟩]R) = [⟨G, H⟩]R) & ⊢ (((z ∈ S ∧ w ∈ S) ∧ (v ∈ S ∧ u ∈ S)) → ([⟨z, w⟩]RF[⟨v, u⟩]R) = [⟨N, Q⟩]R) & ⊢ (((G ∈ S ∧ H ∈ S) ∧ (v ∈ S ∧ u ∈ S)) → ([⟨G, H⟩]RF[⟨v, u⟩]R) = [⟨J, K⟩]R) & ⊢ (((x ∈ S ∧ y ∈ S) ∧ (N ∈ S ∧ Q ∈ S)) → ([⟨x, y⟩]RF[⟨N, Q⟩]R) = [⟨L, M⟩]R) & ⊢ (((x ∈ S ∧ y ∈ S) ∧ (z ∈ S ∧ w ∈ S)) → (G ∈ S ∧ H ∈ S)) & ⊢ (((z ∈ S ∧ w ∈ S) ∧ (v ∈ S ∧ u ∈ S)) → (N ∈ S ∧ Q ∈ S)) & ⊢ J = L & ⊢ K = M ⇒ ⊢ ((A ∈ D ∧ B ∈ D ∧ C ∈ D) → ((AFB)FC) = (AF(BFC))) | ||
| Theorem | ecoprdi 3257 | Lemma used in proving distributive laws via equivalence classes. |
| ⊢ D = ((S × S) / R) & ⊢ (((z ∈ S ∧ w ∈ S) ∧ (v ∈ S ∧ u ∈ S)) → ([⟨z, w⟩]RF[⟨v, u⟩]R) = [⟨M, N⟩]R) & ⊢ (((x ∈ S ∧ y ∈ S) ∧ (M ∈ S ∧ N ∈ S)) → ([⟨x, y⟩]RG[⟨M, N⟩]R) = [⟨H, J⟩]R) & ⊢ (((x ∈ S ∧ y ∈ S) ∧ (z ∈ S ∧ w ∈ S)) → ([⟨x, y⟩]RG[⟨z, w⟩]R) = [⟨W, X⟩]R) & ⊢ (((x ∈ S ∧ y ∈ S) ∧ (v ∈ S ∧ u ∈ S)) → ([⟨x, y⟩]RG[⟨v, u⟩]R) = [⟨Y, Z⟩]R) & ⊢ (((W ∈ S ∧ X ∈ S) ∧ (Y ∈ S ∧ Z ∈ S)) → ([⟨W, X⟩]RF[⟨Y, Z⟩]R) = [⟨K, L⟩]R) & ⊢ (((z ∈ S ∧ w ∈ S) ∧ (v ∈ S ∧ u ∈ S)) → (M ∈ S ∧ N ∈ S)) & ⊢ (((x ∈ S ∧ y ∈ S) ∧ (z ∈ S ∧ w ∈ S)) → (W ∈ S ∧ X ∈ S)) & ⊢ (((x ∈ S ∧ y ∈ S) ∧ (v ∈ S ∧ u ∈ S)) → (Y ∈ S ∧ Z ∈ S)) & ⊢ H = K & ⊢ J = L ⇒ ⊢ ((A ∈ D ∧ B ∈ D ∧ C ∈ D) → (AG(BFC)) = ((AGB)F(AGC))) | ||
| Syntax | cm 3258 | Extend the definition of a class to include the mapping operation. (Read for A ↑m B, "the set of all functions that map from B to A.) |
| class ↑m | ||
| Definition | df-map 3259 | Define the mapping operation or set exponentiation. The set of all functions that map from B to A is written (A ↑m B) (see mapval 3264). Many authors write A followed by B as a superscript for this operation and rely on context to avoid confusion other exponentiation operations (e.g. Definition 10.42 of [TakeutiZaring] p. 95). Other authors show B as a prefixed superscript, which is read "A pre B" (e.g. definition of [Enderton] p. 52). Definition 8.21 of [Eisenberg] p. 125 uses the notation Map(B, A) for our (A ↑m B). The up-arrow is used by Donald Knuth for iterated exponentiation (Science 194, 1235-1242, 1976). We adopt the first case of his notation (simple exponentiation) and subscript it with m to distinguish it from other kinds of exponentiation. |
| ⊢ ↑m = {⟨⟨x, y⟩, z⟩∣z = {f∣f:y–→x}} | ||
| Theorem | mapprc 3260 | When A is a proper class, the class of all functions mapping A to B is empty. Exercise 4.41 of [Mendelson] p. 255. |
| ⊢ (¬ A ∈ V → {f∣f:A–→B} = ∅) | ||
| Theorem | mapex 3261 | The class of all functions mapping one set to another is a set. Remark after Definition 10.24 of [Kunen] p. 31. (Contributed by Raph Levien, 4-Dec-03.) |
| ⊢ ((A ∈ C ∧ B ∈ D) → {f∣f:A–→B} ∈ V) | ||
| Theorem | fnmap 3262 | Set exponentiation has a universal domain. |
| ⊢ ↑m Fn (V × V) | ||
| Theorem | mapvalg 3263 | The value of set exponentiation. (A ↑m B) is the set of all functions that map from B to A. Definition 10.24 of [Kunen] p. 24. |
| ⊢ ((A ∈ C ∧ B ∈ D) → (A ↑m B) = {f∣f:B–→A}) | ||
| Theorem | mapval 3264 | The value of set exponentiation (inference version). (A ↑m B) is the set of all functions that map from B to A. Definition 10.24 of [Kunen] p. 24. |
| ⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (A ↑m B) = {f∣f:B–→A} | ||
| Theorem | elmap 3265 | Membership relation for set exponentiation. |
| ⊢ A ∈ V & ⊢ B ∈ V ⇒ ⊢ (C ∈ (A ↑m B) ↔ C:B–→A) | ||
| Theorem | map0e 3266 | Set exponentiation with an empty exponent (ordinal number 0) is ordinal number 1. Exercise 4.42(a) of [Mendelson] p. 255. |
| ⊢ A ∈ V ⇒ ⊢ (A ↑m ∅) = 1o | ||
| Theorem | map0b 3267 | Set exponentiation with an empty base is the empty set, provided the exponent is non-empty. Theorem 96 of [Suppes] p. 89. |
| ⊢ A ∈ V ⇒ ⊢ (¬ A = ∅ → (∅ ↑m A) = ∅) | ||
| Theorem | map0 3268 | Set exponentiation is empty iff the base is empty and the exponent is not empty. Theorem 97 of [Suppes] p. 89. |
| ⊢ A ∈ V & ⊢ B ∈ V | ||