![]() |
Metamath
Proof Explorer Theorem List (p. 90 of 491) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fsetcdmex 8901* | The class of all functions from a nonempty set 𝐴 into a class 𝐵 is a set iff 𝐵 is a set . (Contributed by AV, 15-Sep-2024.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅) → (𝐵 ∈ V ↔ {𝑓 ∣ 𝑓:𝐴⟶𝐵} ∈ V)) | ||
Theorem | fsetexb 8902* | The class of all functions from a class 𝐴 into a class 𝐵 is a set iff 𝐵 is a set or 𝐴 is not a set or 𝐴 is empty. (Contributed by AV, 15-Sep-2024.) |
⊢ ({𝑓 ∣ 𝑓:𝐴⟶𝐵} ∈ V ↔ (𝐴 ∉ V ∨ 𝐴 = ∅ ∨ 𝐵 ∈ V)) | ||
Theorem | elmapfn 8903 | A mapping is a function with the appropriate domain. (Contributed by AV, 6-Apr-2019.) |
⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → 𝐴 Fn 𝐶) | ||
Theorem | elmapfun 8904 | A mapping is always a function. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.) |
⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → Fun 𝐴) | ||
Theorem | elmapssres 8905 | A restricted mapping is a mapping. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Mario Carneiro, 5-May-2015.) |
⊢ ((𝐴 ∈ (𝐵 ↑m 𝐶) ∧ 𝐷 ⊆ 𝐶) → (𝐴 ↾ 𝐷) ∈ (𝐵 ↑m 𝐷)) | ||
Theorem | fpmg 8906 | A total function is a partial function. (Contributed by Mario Carneiro, 31-Dec-2013.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴⟶𝐵) → 𝐹 ∈ (𝐵 ↑pm 𝐴)) | ||
Theorem | pmss12g 8907 | Subset relation for the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013.) |
⊢ (((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊)) → (𝐴 ↑pm 𝐵) ⊆ (𝐶 ↑pm 𝐷)) | ||
Theorem | pmresg 8908 | Elementhood of a restricted function in the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐹 ∈ (𝐴 ↑pm 𝐶)) → (𝐹 ↾ 𝐵) ∈ (𝐴 ↑pm 𝐵)) | ||
Theorem | elmap 8909 | Membership relation for set exponentiation. (Contributed by NM, 8-Dec-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹 ∈ (𝐴 ↑m 𝐵) ↔ 𝐹:𝐵⟶𝐴) | ||
Theorem | mapval2 8910* | Alternate expression for the value of set exponentiation. (Contributed by NM, 3-Nov-2007.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ↑m 𝐵) = (𝒫 (𝐵 × 𝐴) ∩ {𝑓 ∣ 𝑓 Fn 𝐵}) | ||
Theorem | elpm 8911 | The predicate "is a partial function". (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) ↔ (Fun 𝐹 ∧ 𝐹 ⊆ (𝐵 × 𝐴))) | ||
Theorem | elpm2 8912 | The predicate "is a partial function". (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 31-Dec-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹 ∈ (𝐴 ↑pm 𝐵) ↔ (𝐹:dom 𝐹⟶𝐴 ∧ dom 𝐹 ⊆ 𝐵)) | ||
Theorem | fpm 8913 | A total function is a partial function. (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 31-Dec-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ∈ (𝐵 ↑pm 𝐴)) | ||
Theorem | mapsspm 8914 | Set exponentiation is a subset of partial maps. (Contributed by NM, 15-Nov-2007.) (Revised by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝐴 ↑m 𝐵) ⊆ (𝐴 ↑pm 𝐵) | ||
Theorem | pmsspw 8915 | Partial maps are a subset of the power set of the Cartesian product of its arguments. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ (𝐴 ↑pm 𝐵) ⊆ 𝒫 (𝐵 × 𝐴) | ||
Theorem | mapsspw 8916 | Set exponentiation is a subset of the power set of the Cartesian product of its arguments. (Contributed by NM, 8-Dec-2006.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐴 ↑m 𝐵) ⊆ 𝒫 (𝐵 × 𝐴) | ||
Theorem | mapfvd 8917 | The value of a function that maps from 𝐵 to 𝐴. (Contributed by AV, 2-Feb-2023.) |
⊢ 𝑀 = (𝐴 ↑m 𝐵) & ⊢ (𝜑 → 𝐹 ∈ 𝑀) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹‘𝑋) ∈ 𝐴) | ||
Theorem | elmapresaun 8918 | fresaun 6779 transposed to mappings. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.) |
⊢ ((𝐹 ∈ (𝐶 ↑m 𝐴) ∧ 𝐺 ∈ (𝐶 ↑m 𝐵) ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → (𝐹 ∪ 𝐺) ∈ (𝐶 ↑m (𝐴 ∪ 𝐵))) | ||
Theorem | fvmptmap 8919* | Special case of fvmpt 7015 for operator theorems. (Contributed by NM, 27-Nov-2007.) |
⊢ 𝐶 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝑅 ∈ V & ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) & ⊢ 𝐹 = (𝑥 ∈ (𝑅 ↑m 𝐷) ↦ 𝐵) ⇒ ⊢ (𝐴:𝐷⟶𝑅 → (𝐹‘𝐴) = 𝐶) | ||
Theorem | map0e 8920 | Set exponentiation with an empty exponent (ordinal number 0) is ordinal number 1. Exercise 4.42(a) of [Mendelson] p. 255. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 30-Apr-2015.) (Proof shortened by AV, 14-Jul-2022.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ↑m ∅) = 1o) | ||
Theorem | map0b 8921 | Set exponentiation with an empty base is the empty set, provided the exponent is nonempty. Theorem 96 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐴 ≠ ∅ → (∅ ↑m 𝐴) = ∅) | ||
Theorem | map0g 8922 | Set exponentiation is empty iff the base is empty and the exponent is not empty. Theorem 97 of [Suppes] p. 89. (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ↑m 𝐵) = ∅ ↔ (𝐴 = ∅ ∧ 𝐵 ≠ ∅))) | ||
Theorem | 0map0sn0 8923 | The set of mappings of the empty set to the empty set is the singleton containing the empty set. (Contributed by AV, 31-Mar-2024.) |
⊢ (∅ ↑m ∅) = {∅} | ||
Theorem | mapsnd 8924* | The value of set exponentiation with a singleton exponent. Theorem 98 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Revised by Glauco Siliprandi, 24-Dec-2020.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐴 ↑m {𝐵}) = {𝑓 ∣ ∃𝑦 ∈ 𝐴 𝑓 = {〈𝐵, 𝑦〉}}) | ||
Theorem | map0 8925 | Set exponentiation is empty iff the base is empty and the exponent is not empty. Theorem 97 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐴 ↑m 𝐵) = ∅ ↔ (𝐴 = ∅ ∧ 𝐵 ≠ ∅)) | ||
Theorem | mapsn 8926* | The value of set exponentiation with a singleton exponent. Theorem 98 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Proof shortened by AV, 17-Jul-2022.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ↑m {𝐵}) = {𝑓 ∣ ∃𝑦 ∈ 𝐴 𝑓 = {〈𝐵, 𝑦〉}} | ||
Theorem | mapss 8927 | Subset inheritance for set exponentiation. Theorem 99 of [Suppes] p. 89. (Contributed by NM, 10-Dec-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → (𝐴 ↑m 𝐶) ⊆ (𝐵 ↑m 𝐶)) | ||
Theorem | fdiagfn 8928* | Functionality of the diagonal map. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) ⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐵⟶(𝐵 ↑m 𝐼)) | ||
Theorem | fvdiagfn 8929* | Functionality of the diagonal map. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) ⇒ ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) = (𝐼 × {𝑋})) | ||
Theorem | mapsnconst 8930 | Every singleton map is a constant function. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
⊢ 𝑆 = {𝑋} & ⊢ 𝐵 ∈ V & ⊢ 𝑋 ∈ V ⇒ ⊢ (𝐹 ∈ (𝐵 ↑m 𝑆) → 𝐹 = (𝑆 × {(𝐹‘𝑋)})) | ||
Theorem | mapsncnv 8931* | Expression for the inverse of the canonical map between a set and its set of singleton functions. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
⊢ 𝑆 = {𝑋} & ⊢ 𝐵 ∈ V & ⊢ 𝑋 ∈ V & ⊢ 𝐹 = (𝑥 ∈ (𝐵 ↑m 𝑆) ↦ (𝑥‘𝑋)) ⇒ ⊢ ◡𝐹 = (𝑦 ∈ 𝐵 ↦ (𝑆 × {𝑦})) | ||
Theorem | mapsnf1o2 8932* | Explicit bijection between a set and its singleton functions. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
⊢ 𝑆 = {𝑋} & ⊢ 𝐵 ∈ V & ⊢ 𝑋 ∈ V & ⊢ 𝐹 = (𝑥 ∈ (𝐵 ↑m 𝑆) ↦ (𝑥‘𝑋)) ⇒ ⊢ 𝐹:(𝐵 ↑m 𝑆)–1-1-onto→𝐵 | ||
Theorem | mapsnf1o3 8933* | Explicit bijection in the reverse of mapsnf1o2 8932. (Contributed by Stefan O'Rear, 24-Mar-2015.) |
⊢ 𝑆 = {𝑋} & ⊢ 𝐵 ∈ V & ⊢ 𝑋 ∈ V & ⊢ 𝐹 = (𝑦 ∈ 𝐵 ↦ (𝑆 × {𝑦})) ⇒ ⊢ 𝐹:𝐵–1-1-onto→(𝐵 ↑m 𝑆) | ||
Theorem | ralxpmap 8934* | Quantification over functions in terms of quantification over values and punctured functions. (Contributed by Stefan O'Rear, 27-Feb-2015.) (Revised by Stefan O'Rear, 5-May-2015.) |
⊢ (𝑓 = (𝑔 ∪ {〈𝐽, 𝑦〉}) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝐽 ∈ 𝑇 → (∀𝑓 ∈ (𝑆 ↑m 𝑇)𝜑 ↔ ∀𝑦 ∈ 𝑆 ∀𝑔 ∈ (𝑆 ↑m (𝑇 ∖ {𝐽}))𝜓)) | ||
Syntax | cixp 8935 | Extend class notation to include infinite Cartesian products. |
class X𝑥 ∈ 𝐴 𝐵 | ||
Definition | df-ixp 8936* | Definition of infinite Cartesian product of [Enderton] p. 54. Enderton uses a bold "X" with 𝑥 ∈ 𝐴 written underneath or as a subscript, as does Stoll p. 47. Some books use a capital pi, but we will reserve that notation for products of numbers. Usually 𝐵 represents a class expression containing 𝑥 free and thus can be thought of as 𝐵(𝑥). Normally, 𝑥 is not free in 𝐴, although this is not a requirement of the definition. (Contributed by NM, 28-Sep-2006.) |
⊢ X𝑥 ∈ 𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn {𝑥 ∣ 𝑥 ∈ 𝐴} ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)} | ||
Theorem | dfixp 8937* | Eliminate the expression {𝑥 ∣ 𝑥 ∈ 𝐴} in df-ixp 8936, under the assumption that 𝐴 and 𝑥 are disjoint. This way, we can say that 𝑥 is bound in X𝑥 ∈ 𝐴𝐵 even if it appears free in 𝐴. (Contributed by Mario Carneiro, 12-Aug-2016.) |
⊢ X𝑥 ∈ 𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)} | ||
Theorem | ixpsnval 8938* | The value of an infinite Cartesian product with a singleton. (Contributed by AV, 3-Dec-2018.) |
⊢ (𝑋 ∈ 𝑉 → X𝑥 ∈ {𝑋}𝐵 = {𝑓 ∣ (𝑓 Fn {𝑋} ∧ (𝑓‘𝑋) ∈ ⦋𝑋 / 𝑥⦌𝐵)}) | ||
Theorem | elixp2 8939* | Membership in an infinite Cartesian product. See df-ixp 8936 for discussion of the notation. (Contributed by NM, 28-Sep-2006.) |
⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) | ||
Theorem | fvixp 8940* | Projection of a factor of an indexed Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.) |
⊢ (𝑥 = 𝐶 → 𝐵 = 𝐷) ⇒ ⊢ ((𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐷) | ||
Theorem | ixpfn 8941* | A nuple is a function. (Contributed by FL, 6-Jun-2011.) (Revised by Mario Carneiro, 31-May-2014.) |
⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 → 𝐹 Fn 𝐴) | ||
Theorem | elixp 8942* | Membership in an infinite Cartesian product. (Contributed by NM, 28-Sep-2006.) |
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) | ||
Theorem | elixpconst 8943* | Membership in an infinite Cartesian product of a constant 𝐵. (Contributed by NM, 12-Apr-2008.) |
⊢ 𝐹 ∈ V ⇒ ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ 𝐹:𝐴⟶𝐵) | ||
Theorem | ixpconstg 8944* | Infinite Cartesian product of a constant 𝐵. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → X𝑥 ∈ 𝐴 𝐵 = (𝐵 ↑m 𝐴)) | ||
Theorem | ixpconst 8945* | Infinite Cartesian product of a constant 𝐵. (Contributed by NM, 28-Sep-2006.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ X𝑥 ∈ 𝐴 𝐵 = (𝐵 ↑m 𝐴) | ||
Theorem | ixpeq1 8946* | Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.) |
⊢ (𝐴 = 𝐵 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶) | ||
Theorem | ixpeq1d 8947* | Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐶 = X𝑥 ∈ 𝐵 𝐶) | ||
Theorem | ss2ixp 8948 | Subclass theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.) (Revised by Mario Carneiro, 12-Aug-2016.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → X𝑥 ∈ 𝐴 𝐵 ⊆ X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | ixpeq2 8949 | Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | ixpeq2dva 8950* | Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | ixpeq2dv 8951* | Equality theorem for infinite Cartesian product. (Contributed by Mario Carneiro, 11-Jun-2016.) |
⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐴 𝐵 = X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | cbvixp 8952* | Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 20-Jun-2011.) |
⊢ Ⅎ𝑦𝐵 & ⊢ Ⅎ𝑥𝐶 & ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶 | ||
Theorem | cbvixpv 8953* | Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) ⇒ ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶 | ||
Theorem | nfixpw 8954* | Bound-variable hypothesis builder for indexed Cartesian product. Version of nfixp 8955 with a disjoint variable condition, which does not require ax-13 2374. (Contributed by Mario Carneiro, 15-Oct-2016.) Avoid ax-13 2374. (Revised by GG, 26-Jan-2024.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦X𝑥 ∈ 𝐴 𝐵 | ||
Theorem | nfixp 8955 | Bound-variable hypothesis builder for indexed Cartesian product. Usage of this theorem is discouraged because it depends on ax-13 2374. Use the weaker nfixpw 8954 when possible. (Contributed by Mario Carneiro, 15-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝐴 & ⊢ Ⅎ𝑦𝐵 ⇒ ⊢ Ⅎ𝑦X𝑥 ∈ 𝐴 𝐵 | ||
Theorem | nfixp1 8956 | The index variable in an indexed Cartesian product is not free. (Contributed by Jeff Madsen, 19-Jun-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥X𝑥 ∈ 𝐴 𝐵 | ||
Theorem | ixpprc 8957* | A cartesian product of proper-class many sets is empty, because any function in the cartesian product has to be a set with domain 𝐴, which is not possible for a proper class domain. (Contributed by Mario Carneiro, 25-Jan-2015.) |
⊢ (¬ 𝐴 ∈ V → X𝑥 ∈ 𝐴 𝐵 = ∅) | ||
Theorem | ixpf 8958* | A member of an infinite Cartesian product maps to the indexed union of the product argument. Remark in [Enderton] p. 54. (Contributed by NM, 28-Sep-2006.) |
⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 → 𝐹:𝐴⟶∪ 𝑥 ∈ 𝐴 𝐵) | ||
Theorem | uniixp 8959* | The union of an infinite Cartesian product is included in a Cartesian product. (Contributed by NM, 28-Sep-2006.) (Revised by Mario Carneiro, 24-Jun-2015.) |
⊢ ∪ X𝑥 ∈ 𝐴 𝐵 ⊆ (𝐴 × ∪ 𝑥 ∈ 𝐴 𝐵) | ||
Theorem | ixpexg 8960* | The existence of an infinite Cartesian product. 𝑥 is normally a free-variable parameter in 𝐵. Remark in Enderton p. 54. (Contributed by NM, 28-Sep-2006.) (Revised by Mario Carneiro, 25-Jan-2015.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X𝑥 ∈ 𝐴 𝐵 ∈ V) | ||
Theorem | ixpin 8961* | The intersection of two infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ X𝑥 ∈ 𝐴 (𝐵 ∩ 𝐶) = (X𝑥 ∈ 𝐴 𝐵 ∩ X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | ixpiin 8962* | The indexed intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 6-Feb-2015.) |
⊢ (𝐵 ≠ ∅ → X𝑥 ∈ 𝐴 ∩ 𝑦 ∈ 𝐵 𝐶 = ∩ 𝑦 ∈ 𝐵 X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | ixpint 8963* | The intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ (𝐵 ≠ ∅ → X𝑥 ∈ 𝐴 ∩ 𝐵 = ∩ 𝑦 ∈ 𝐵 X𝑥 ∈ 𝐴 𝑦) | ||
Theorem | ixp0x 8964 | An infinite Cartesian product with an empty index set. (Contributed by NM, 21-Sep-2007.) |
⊢ X𝑥 ∈ ∅ 𝐴 = {∅} | ||
Theorem | ixpssmap2g 8965* | An infinite Cartesian product is a subset of set exponentiation. This version of ixpssmapg 8966 avoids ax-rep 5284. (Contributed by Mario Carneiro, 16-Nov-2014.) |
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴)) | ||
Theorem | ixpssmapg 8966* | An infinite Cartesian product is a subset of set exponentiation. (Contributed by Jeff Madsen, 19-Jun-2011.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴)) | ||
Theorem | 0elixp 8967 | Membership of the empty set in an infinite Cartesian product. (Contributed by Steve Rodriguez, 29-Sep-2006.) |
⊢ ∅ ∈ X𝑥 ∈ ∅ 𝐴 | ||
Theorem | ixpn0 8968 | The infinite Cartesian product of a family 𝐵(𝑥) with an empty member is empty. The converse of this theorem is equivalent to the Axiom of Choice, see ac9 10520. (Contributed by Mario Carneiro, 22-Jun-2016.) |
⊢ (X𝑥 ∈ 𝐴 𝐵 ≠ ∅ → ∀𝑥 ∈ 𝐴 𝐵 ≠ ∅) | ||
Theorem | ixp0 8969 | The infinite Cartesian product of a family 𝐵(𝑥) with an empty member is empty. The converse of this theorem is equivalent to the Axiom of Choice, see ac9 10520. (Contributed by NM, 1-Oct-2006.) (Proof shortened by Mario Carneiro, 22-Jun-2016.) |
⊢ (∃𝑥 ∈ 𝐴 𝐵 = ∅ → X𝑥 ∈ 𝐴 𝐵 = ∅) | ||
Theorem | ixpssmap 8970* | An infinite Cartesian product is a subset of set exponentiation. Remark in [Enderton] p. 54. (Contributed by NM, 28-Sep-2006.) |
⊢ 𝐵 ∈ V ⇒ ⊢ X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴) | ||
Theorem | resixp 8971* | Restriction of an element of an infinite Cartesian product. (Contributed by FL, 7-Nov-2011.) (Proof shortened by Mario Carneiro, 31-May-2014.) |
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐹 ∈ X𝑥 ∈ 𝐴 𝐶) → (𝐹 ↾ 𝐵) ∈ X𝑥 ∈ 𝐵 𝐶) | ||
Theorem | undifixp 8972* | Union of two projections of a cartesian product. (Contributed by FL, 7-Nov-2011.) |
⊢ ((𝐹 ∈ X𝑥 ∈ 𝐵 𝐶 ∧ 𝐺 ∈ X𝑥 ∈ (𝐴 ∖ 𝐵)𝐶 ∧ 𝐵 ⊆ 𝐴) → (𝐹 ∪ 𝐺) ∈ X𝑥 ∈ 𝐴 𝐶) | ||
Theorem | mptelixpg 8973* | Condition for an explicit member of an indexed product. (Contributed by Stefan O'Rear, 4-Jan-2015.) |
⊢ (𝐼 ∈ 𝑉 → ((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ X𝑥 ∈ 𝐼 𝐾 ↔ ∀𝑥 ∈ 𝐼 𝐽 ∈ 𝐾)) | ||
Theorem | resixpfo 8974* | Restriction of elements of an infinite Cartesian product creates a surjection, if the original Cartesian product is nonempty. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ 𝐹 = (𝑓 ∈ X𝑥 ∈ 𝐴 𝐶 ↦ (𝑓 ↾ 𝐵)) ⇒ ⊢ ((𝐵 ⊆ 𝐴 ∧ X𝑥 ∈ 𝐴 𝐶 ≠ ∅) → 𝐹:X𝑥 ∈ 𝐴 𝐶–onto→X𝑥 ∈ 𝐵 𝐶) | ||
Theorem | elixpsn 8975* | Membership in a class of singleton functions. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐹 ∈ X𝑥 ∈ {𝐴}𝐵 ↔ ∃𝑦 ∈ 𝐵 𝐹 = {〈𝐴, 𝑦〉})) | ||
Theorem | ixpsnf1o 8976* | A bijection between a class and single-point functions to it. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ ({𝐼} × {𝑥})) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐹:𝐴–1-1-onto→X𝑦 ∈ {𝐼}𝐴) | ||
Theorem | mapsnf1o 8977* | A bijection between a set and single-point functions to it. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ ({𝐼} × {𝑥})) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊) → 𝐹:𝐴–1-1-onto→(𝐴 ↑m {𝐼})) | ||
Theorem | boxriin 8978* | A rectangular subset of a rectangular set can be recovered as the relative intersection of single-axis restrictions. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ (∀𝑥 ∈ 𝐼 𝐴 ⊆ 𝐵 → X𝑥 ∈ 𝐼 𝐴 = (X𝑥 ∈ 𝐼 𝐵 ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐴, 𝐵))) | ||
Theorem | boxcutc 8979* | The relative complement of a box set restricted on one axis. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ ((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) → (X𝑘 ∈ 𝐴 𝐵 ∖ X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, 𝐶, 𝐵)) = X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵)) | ||
Syntax | cen 8980 | Extend class definition to include the equinumerosity relation ("approximately equals" symbol) |
class ≈ | ||
Syntax | cdom 8981 | Extend class definition to include the dominance relation (curly "less than or equal to") |
class ≼ | ||
Syntax | csdm 8982 | Extend class definition to include the strict dominance relation (curly less-than) |
class ≺ | ||
Syntax | cfn 8983 | Extend class definition to include the class of all finite sets. |
class Fin | ||
Definition | df-en 8984* | Define the equinumerosity relation. Definition of [Enderton] p. 129. We define ≈ to be a binary relation rather than a connective, so its arguments must be sets to be meaningful. This is acceptable because we do not consider equinumerosity for proper classes. We derive the usual definition as bren 8993. (Contributed by NM, 28-Mar-1998.) |
⊢ ≈ = {〈𝑥, 𝑦〉 ∣ ∃𝑓 𝑓:𝑥–1-1-onto→𝑦} | ||
Definition | df-dom 8985* | Define the dominance relation. For an alternate definition see dfdom2 9016. Compare Definition of [Enderton] p. 145. Typical textbook definitions are derived as brdom 8999 and domen 9000. (Contributed by NM, 28-Mar-1998.) |
⊢ ≼ = {〈𝑥, 𝑦〉 ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦} | ||
Definition | df-sdom 8986 | Define the strict dominance relation. Alternate possible definitions are derived as brsdom 9013 and brsdom2 9135. Definition 3 of [Suppes] p. 97. (Contributed by NM, 31-Mar-1998.) |
⊢ ≺ = ( ≼ ∖ ≈ ) | ||
Definition | df-fin 8987* | Define the (proper) class of all finite sets. Similar to Definition 10.29 of [TakeutiZaring] p. 91, whose "Fin(a)" corresponds to our "𝑎 ∈ Fin". This definition is meaningful whether or not we accept the Axiom of Infinity ax-inf2 9678. If we accept Infinity, we can also express 𝐴 ∈ Fin by 𝐴 ≺ ω (Theorem isfinite 9689.) (Contributed by NM, 22-Aug-2008.) |
⊢ Fin = {𝑥 ∣ ∃𝑦 ∈ ω 𝑥 ≈ 𝑦} | ||
Theorem | relen 8988 | Equinumerosity is a relation. (Contributed by NM, 28-Mar-1998.) |
⊢ Rel ≈ | ||
Theorem | reldom 8989 | Dominance is a relation. (Contributed by NM, 28-Mar-1998.) |
⊢ Rel ≼ | ||
Theorem | relsdom 8990 | Strict dominance is a relation. (Contributed by NM, 31-Mar-1998.) |
⊢ Rel ≺ | ||
Theorem | encv 8991 | If two classes are equinumerous, both classes are sets. (Contributed by AV, 21-Mar-2019.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | ||
Theorem | breng 8992* | Equinumerosity relation. This variation of bren 8993 does not require the Axiom of Union. (Contributed by NM, 15-Jun-1998.) Extract from a subproof of bren 8993. (Revised by BTernaryTau, 23-Sep-2024.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)) | ||
Theorem | bren 8993* | Equinumerosity relation. (Contributed by NM, 15-Jun-1998.) Extract breng 8992 as an intermediate result. (Revised by BTernaryTau, 23-Sep-2024.) |
⊢ (𝐴 ≈ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵) | ||
Theorem | brdom2g 8994* | Dominance relation. This variation of brdomg 8995 does not require the Axiom of Union. (Contributed by NM, 15-Jun-1998.) Extract from a subproof of brdomg 8995. (Revised by BTernaryTau, 29-Nov-2024.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵)) | ||
Theorem | brdomg 8995* | Dominance relation. (Contributed by NM, 15-Jun-1998.) Extract brdom2g 8994 as an intermediate result. (Revised by BTernaryTau, 29-Nov-2024.) |
⊢ (𝐵 ∈ 𝐶 → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵)) | ||
Theorem | brdomgOLD 8996* | Obsolete version of brdomg 8995 as of 29-Nov-2024. (Contributed by NM, 15-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐵 ∈ 𝐶 → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵)) | ||
Theorem | brdomi 8997* | Dominance relation. (Contributed by Mario Carneiro, 26-Apr-2015.) Avoid ax-un 7753. (Revised by BTernaryTau, 29-Nov-2024.) |
⊢ (𝐴 ≼ 𝐵 → ∃𝑓 𝑓:𝐴–1-1→𝐵) | ||
Theorem | brdomiOLD 8998* | Obsolete version of brdomi 8997 as of 29-Nov-2024. (Contributed by Mario Carneiro, 26-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ≼ 𝐵 → ∃𝑓 𝑓:𝐴–1-1→𝐵) | ||
Theorem | brdom 8999* | Dominance relation. (Contributed by NM, 15-Jun-1998.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵) | ||
Theorem | domen 9000* | Dominance in terms of equinumerosity. Example 1 of [Enderton] p. 146. (Contributed by NM, 15-Jun-1998.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑥(𝐴 ≈ 𝑥 ∧ 𝑥 ⊆ 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |