![]() |
Metamath
Proof Explorer Theorem List (p. 60 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | elima 5901* | Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 19-Apr-2004.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥 ∈ 𝐶 𝑥𝐵𝐴) | ||
Theorem | elima2 5902* | Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 11-Aug-2004.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥(𝑥 ∈ 𝐶 ∧ 𝑥𝐵𝐴)) | ||
Theorem | elima3 5903* | Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 14-Aug-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥(𝑥 ∈ 𝐶 ∧ 〈𝑥, 𝐴〉 ∈ 𝐵)) | ||
Theorem | nfima 5904 | Bound-variable hypothesis builder for image. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 “ 𝐵) | ||
Theorem | nfimad 5905 | Deduction version of bound-variable hypothesis builder nfima 5904. (Contributed by FL, 15-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥(𝐴 “ 𝐵)) | ||
Theorem | imadmrn 5906 | The image of the domain of a class is the range of the class. (Contributed by NM, 14-Aug-1994.) |
⊢ (𝐴 “ dom 𝐴) = ran 𝐴 | ||
Theorem | imassrn 5907 | The image of a class is a subset of its range. Theorem 3.16(xi) of [Monk1] p. 39. (Contributed by NM, 31-Mar-1995.) |
⊢ (𝐴 “ 𝐵) ⊆ ran 𝐴 | ||
Theorem | mptima 5908* | Image of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) “ 𝐶) = ran (𝑥 ∈ (𝐴 ∩ 𝐶) ↦ 𝐵) | ||
Theorem | imai 5909 | Image under the identity relation. Theorem 3.16(viii) of [Monk1] p. 38. (Contributed by NM, 30-Apr-1998.) |
⊢ ( I “ 𝐴) = 𝐴 | ||
Theorem | rnresi 5910 | The range of the restricted identity function. (Contributed by NM, 27-Aug-2004.) |
⊢ ran ( I ↾ 𝐴) = 𝐴 | ||
Theorem | resiima 5911 | The image of a restriction of the identity function. (Contributed by FL, 31-Dec-2006.) |
⊢ (𝐵 ⊆ 𝐴 → (( I ↾ 𝐴) “ 𝐵) = 𝐵) | ||
Theorem | ima0 5912 | Image of the empty set. Theorem 3.16(ii) of [Monk1] p. 38. (Contributed by NM, 20-May-1998.) |
⊢ (𝐴 “ ∅) = ∅ | ||
Theorem | 0ima 5913 | Image under the empty relation. (Contributed by FL, 11-Jan-2007.) |
⊢ (∅ “ 𝐴) = ∅ | ||
Theorem | csbima12 5914 | Move class substitution in and out of the image of a function. (Contributed by FL, 15-Dec-2006.) (Revised by NM, 20-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵) | ||
Theorem | imadisj 5915 | A class whose image under another is empty is disjoint with the other's domain. (Contributed by FL, 24-Jan-2007.) |
⊢ ((𝐴 “ 𝐵) = ∅ ↔ (dom 𝐴 ∩ 𝐵) = ∅) | ||
Theorem | cnvimass 5916 | A preimage under any class is included in the domain of the class. (Contributed by FL, 29-Jan-2007.) |
⊢ (◡𝐴 “ 𝐵) ⊆ dom 𝐴 | ||
Theorem | cnvimarndm 5917 | The preimage of the range of a class is the domain of the class. (Contributed by Jeff Hankins, 15-Jul-2009.) |
⊢ (◡𝐴 “ ran 𝐴) = dom 𝐴 | ||
Theorem | imasng 5918* | The image of a singleton. (Contributed by NM, 8-May-2005.) |
⊢ (𝐴 ∈ 𝐵 → (𝑅 “ {𝐴}) = {𝑦 ∣ 𝐴𝑅𝑦}) | ||
Theorem | relimasn 5919* | The image of a singleton. (Contributed by NM, 20-May-1998.) |
⊢ (Rel 𝑅 → (𝑅 “ {𝐴}) = {𝑦 ∣ 𝐴𝑅𝑦}) | ||
Theorem | elrelimasn 5920 | Elementhood in the image of a singleton. (Contributed by Mario Carneiro, 3-Nov-2015.) |
⊢ (Rel 𝑅 → (𝐵 ∈ (𝑅 “ {𝐴}) ↔ 𝐴𝑅𝐵)) | ||
Theorem | elimasn 5921 | Membership in an image of a singleton. (Contributed by NM, 15-Mar-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐶 ∈ (𝐴 “ {𝐵}) ↔ 〈𝐵, 𝐶〉 ∈ 𝐴) | ||
Theorem | elimasng 5922 | Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐶 ∈ (𝐴 “ {𝐵}) ↔ 〈𝐵, 𝐶〉 ∈ 𝐴)) | ||
Theorem | elimasni 5923 | Membership in an image of a singleton. (Contributed by NM, 5-Aug-2010.) |
⊢ (𝐶 ∈ (𝐴 “ {𝐵}) → 𝐵𝐴𝐶) | ||
Theorem | args 5924* | Two ways to express the class of unique-valued arguments of 𝐹, which is the same as the domain of 𝐹 whenever 𝐹 is a function. The left-hand side of the equality is from Definition 10.2 of [Quine] p. 65. Quine uses the notation "arg 𝐹 " for this class (for which we have no separate notation). Observe the resemblance to the alternate definition dffv4 6642 of function value, which is based on the idea in Quine's definition. (Contributed by NM, 8-May-2005.) |
⊢ {𝑥 ∣ ∃𝑦(𝐹 “ {𝑥}) = {𝑦}} = {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦} | ||
Theorem | eliniseg 5925 | Membership in an initial segment. The idiom (◡𝐴 “ {𝐵}), meaning {𝑥 ∣ 𝑥𝐴𝐵}, is used to specify an initial segment in (for example) Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by NM, 28-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ 𝐶 ∈ V ⇒ ⊢ (𝐵 ∈ 𝑉 → (𝐶 ∈ (◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵)) | ||
Theorem | epini 5926 | Any set is equal to its preimage under the converse membership relation. (Contributed by Mario Carneiro, 9-Mar-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (◡ E “ {𝐴}) = 𝐴 | ||
Theorem | iniseg 5927* | An idiom that signifies an initial segment of an ordering, used, for example, in Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by NM, 28-Apr-2004.) |
⊢ (𝐵 ∈ 𝑉 → (◡𝐴 “ {𝐵}) = {𝑥 ∣ 𝑥𝐴𝐵}) | ||
Theorem | inisegn0 5928 | Nonemptiness of an initial segment in terms of range. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ (𝐴 ∈ ran 𝐹 ↔ (◡𝐹 “ {𝐴}) ≠ ∅) | ||
Theorem | dffr3 5929* | Alternate definition of well-founded relation. Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by NM, 23-Apr-2004.) (Revised by Mario Carneiro, 23-Jun-2015.) |
⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 (𝑥 ∩ (◡𝑅 “ {𝑦})) = ∅)) | ||
Theorem | dfse2 5930* | Alternate definition of set-like relation. (Contributed by Mario Carneiro, 23-Jun-2015.) |
⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 (𝐴 ∩ (◡𝑅 “ {𝑥})) ∈ V) | ||
Theorem | imass1 5931 | Subset theorem for image. (Contributed by NM, 16-Mar-2004.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐴 “ 𝐶) ⊆ (𝐵 “ 𝐶)) | ||
Theorem | imass2 5932 | Subset theorem for image. Exercise 22(a) of [Enderton] p. 53. (Contributed by NM, 22-Mar-1998.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵)) | ||
Theorem | ndmima 5933 | The image of a singleton outside the domain is empty. (Contributed by NM, 22-May-1998.) (Proof shortened by OpenAI, 3-Jul-2020.) |
⊢ (¬ 𝐴 ∈ dom 𝐵 → (𝐵 “ {𝐴}) = ∅) | ||
Theorem | relcnv 5934 | A converse is a relation. Theorem 12 of [Suppes] p. 62. (Contributed by NM, 29-Oct-1996.) |
⊢ Rel ◡𝐴 | ||
Theorem | relbrcnvg 5935 | When 𝑅 is a relation, the sethood assumptions on brcnv 5717 can be omitted. (Contributed by Mario Carneiro, 28-Apr-2015.) |
⊢ (Rel 𝑅 → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)) | ||
Theorem | eliniseg2 5936 | Eliminate the class existence constraint in eliniseg 5925. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 17-Nov-2015.) |
⊢ (Rel 𝐴 → (𝐶 ∈ (◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵)) | ||
Theorem | relbrcnv 5937 | When 𝑅 is a relation, the sethood assumptions on brcnv 5717 can be omitted. (Contributed by Mario Carneiro, 28-Apr-2015.) |
⊢ Rel 𝑅 ⇒ ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴) | ||
Theorem | cotrg 5938* | Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr 5939 for the main application. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Generalized from its special instance cotr 5939. (Revised by Richard Penner, 24-Dec-2019.) |
⊢ ((𝐴 ∘ 𝐵) ⊆ 𝐶 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)) | ||
Theorem | cotr 5939* | Two ways of saying a relation is transitive. Definition of transitivity in [Schechter] p. 51. Special instance of cotrg 5938. (Contributed by NM, 27-Dec-1996.) |
⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) | ||
Theorem | idrefALT 5940* | Alternate proof of idref 6885 not relying on definitions related to functions. Two ways to state that a relation is reflexive on a class. (Contributed by FL, 15-Jan-2012.) (Proof shortened by Mario Carneiro, 3-Nov-2015.) (Revised by NM, 30-Mar-2016.) (Proof shortened by BJ, 28-Aug-2022.) The "proof modification is discouraged" tag is here only because this is an *ALT result. (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (( I ↾ 𝐴) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 𝑥𝑅𝑥) | ||
Theorem | cnvsym 5941* | Two ways of saying a relation is symmetric. Similar to definition of symmetry in [Schechter] p. 51. (Contributed by NM, 28-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) | ||
Theorem | intasym 5942* | Two ways of saying a relation is antisymmetric. Definition of antisymmetry in [Schechter] p. 51. (Contributed by NM, 9-Sep-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ((𝑅 ∩ ◡𝑅) ⊆ I ↔ ∀𝑥∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦)) | ||
Theorem | asymref 5943* | Two ways of saying a relation is antisymmetric and reflexive. ∪ ∪ 𝑅 is the field of a relation by relfld 6094. (Contributed by NM, 6-May-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ((𝑅 ∩ ◡𝑅) = ( I ↾ ∪ ∪ 𝑅) ↔ ∀𝑥 ∈ ∪ ∪ 𝑅∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ 𝑥 = 𝑦)) | ||
Theorem | asymref2 5944* | Two ways of saying a relation is antisymmetric and reflexive. (Contributed by NM, 6-May-2008.) (Proof shortened by Mario Carneiro, 4-Dec-2016.) |
⊢ ((𝑅 ∩ ◡𝑅) = ( I ↾ ∪ ∪ 𝑅) ↔ (∀𝑥 ∈ ∪ ∪ 𝑅𝑥𝑅𝑥 ∧ ∀𝑥∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) → 𝑥 = 𝑦))) | ||
Theorem | intirr 5945* | Two ways of saying a relation is irreflexive. Definition of irreflexivity in [Schechter] p. 51. (Contributed by NM, 9-Sep-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ((𝑅 ∩ I ) = ∅ ↔ ∀𝑥 ¬ 𝑥𝑅𝑥) | ||
Theorem | brcodir 5946* | Two ways of saying that two elements have an upper bound. (Contributed by Mario Carneiro, 3-Nov-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(◡𝑅 ∘ 𝑅)𝐵 ↔ ∃𝑧(𝐴𝑅𝑧 ∧ 𝐵𝑅𝑧))) | ||
Theorem | codir 5947* | Two ways of saying a relation is directed. (Contributed by Mario Carneiro, 22-Nov-2013.) |
⊢ ((𝐴 × 𝐵) ⊆ (◡𝑅 ∘ 𝑅) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∃𝑧(𝑥𝑅𝑧 ∧ 𝑦𝑅𝑧)) | ||
Theorem | qfto 5948* | A quantifier-free way of expressing the total order predicate. (Contributed by Mario Carneiro, 22-Nov-2013.) |
⊢ ((𝐴 × 𝐵) ⊆ (𝑅 ∪ ◡𝑅) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥)) | ||
Theorem | xpidtr 5949 | A Cartesian square is a transitive relation. (Contributed by FL, 31-Jul-2009.) |
⊢ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) | ||
Theorem | trin2 5950 | The intersection of two transitive classes is transitive. (Contributed by FL, 31-Jul-2009.) |
⊢ (((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ((𝑅 ∩ 𝑆) ∘ (𝑅 ∩ 𝑆)) ⊆ (𝑅 ∩ 𝑆)) | ||
Theorem | poirr2 5951 | A partial order relation is irreflexive. (Contributed by Mario Carneiro, 2-Nov-2015.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ (𝑅 Po 𝐴 → (𝑅 ∩ ( I ↾ 𝐴)) = ∅) | ||
Theorem | trinxp 5952 | The relation induced by a transitive relation on a part of its field is transitive. (Taking the intersection of a relation with a Cartesian square is a way to restrict it to a subset of its field.) (Contributed by FL, 31-Jul-2009.) |
⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 → ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ (𝑅 ∩ (𝐴 × 𝐴))) | ||
Theorem | soirri 5953 | A strict order relation is irreflexive. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.) |
⊢ 𝑅 Or 𝑆 & ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ¬ 𝐴𝑅𝐴 | ||
Theorem | sotri 5954 | A strict order relation is a transitive relation. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.) |
⊢ 𝑅 Or 𝑆 & ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) | ||
Theorem | son2lpi 5955 | A strict order relation has no 2-cycle loops. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.) |
⊢ 𝑅 Or 𝑆 & ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ¬ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴) | ||
Theorem | sotri2 5956 | A transitivity relation. (Read 𝐴 ≤ 𝐵 and 𝐵 < 𝐶 implies 𝐴 < 𝐶.) (Contributed by Mario Carneiro, 10-May-2013.) |
⊢ 𝑅 Or 𝑆 & ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ ¬ 𝐵𝑅𝐴 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) | ||
Theorem | sotri3 5957 | A transitivity relation. (Read 𝐴 < 𝐵 and 𝐵 ≤ 𝐶 implies 𝐴 < 𝐶.) (Contributed by Mario Carneiro, 10-May-2013.) |
⊢ 𝑅 Or 𝑆 & ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐴𝑅𝐵 ∧ ¬ 𝐶𝑅𝐵) → 𝐴𝑅𝐶) | ||
Theorem | poleloe 5958 | Express "less than or equals" for general strict orders. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴(𝑅 ∪ I )𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵))) | ||
Theorem | poltletr 5959 | Transitive law for general strict orders. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝑅 Po 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑅𝐵 ∧ 𝐵(𝑅 ∪ I )𝐶) → 𝐴𝑅𝐶)) | ||
Theorem | somin1 5960 | Property of a minimum in a strict order. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝑅 Or 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → if(𝐴𝑅𝐵, 𝐴, 𝐵)(𝑅 ∪ I )𝐴) | ||
Theorem | somincom 5961 | Commutativity of minimum in a total order. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝑅 Or 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → if(𝐴𝑅𝐵, 𝐴, 𝐵) = if(𝐵𝑅𝐴, 𝐵, 𝐴)) | ||
Theorem | somin2 5962 | Property of a minimum in a strict order. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝑅 Or 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → if(𝐴𝑅𝐵, 𝐴, 𝐵)(𝑅 ∪ I )𝐵) | ||
Theorem | soltmin 5963 | Being less than a minimum, for a general total order. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝑅 Or 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶) ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑅𝐶))) | ||
Theorem | cnvopab 5964* | The converse of a class abstraction of ordered pairs. (Contributed by NM, 11-Dec-2003.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ◡{〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑦, 𝑥〉 ∣ 𝜑} | ||
Theorem | mptcnv 5965* | The converse of a mapping function. (Contributed by Thierry Arnoux, 16-Jan-2017.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐷))) ⇒ ⊢ (𝜑 → ◡(𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | cnv0 5966 | The converse of the empty set. (Contributed by NM, 6-Apr-1998.) Remove dependency on ax-sep 5167, ax-nul 5174, ax-pr 5295. (Revised by KP, 25-Oct-2021.) |
⊢ ◡∅ = ∅ | ||
Theorem | cnvi 5967 | The converse of the identity relation. Theorem 3.7(ii) of [Monk1] p. 36. (Contributed by NM, 26-Apr-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ◡ I = I | ||
Theorem | cnvun 5968 | The converse of a union is the union of converses. Theorem 16 of [Suppes] p. 62. (Contributed by NM, 25-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵) | ||
Theorem | cnvdif 5969 | Distributive law for converse over class difference. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ ◡(𝐴 ∖ 𝐵) = (◡𝐴 ∖ ◡𝐵) | ||
Theorem | cnvin 5970 | Distributive law for converse over intersection. Theorem 15 of [Suppes] p. 62. (Contributed by NM, 25-Mar-1998.) (Revised by Mario Carneiro, 26-Jun-2014.) |
⊢ ◡(𝐴 ∩ 𝐵) = (◡𝐴 ∩ ◡𝐵) | ||
Theorem | rnun 5971 | Distributive law for range over union. Theorem 8 of [Suppes] p. 60. (Contributed by NM, 24-Mar-1998.) |
⊢ ran (𝐴 ∪ 𝐵) = (ran 𝐴 ∪ ran 𝐵) | ||
Theorem | rnin 5972 | The range of an intersection belongs the intersection of ranges. Theorem 9 of [Suppes] p. 60. (Contributed by NM, 15-Sep-2004.) |
⊢ ran (𝐴 ∩ 𝐵) ⊆ (ran 𝐴 ∩ ran 𝐵) | ||
Theorem | rniun 5973 | The range of an indexed union. (Contributed by Mario Carneiro, 29-May-2015.) |
⊢ ran ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ran 𝐵 | ||
Theorem | rnuni 5974* | The range of a union. Part of Exercise 8 of [Enderton] p. 41. (Contributed by NM, 17-Mar-2004.) (Revised by Mario Carneiro, 29-May-2015.) |
⊢ ran ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 ran 𝑥 | ||
Theorem | imaundi 5975 | Distributive law for image over union. Theorem 35 of [Suppes] p. 65. (Contributed by NM, 30-Sep-2002.) |
⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶)) | ||
Theorem | imaundir 5976 | The image of a union. (Contributed by Jeff Hoffman, 17-Feb-2008.) |
⊢ ((𝐴 ∪ 𝐵) “ 𝐶) = ((𝐴 “ 𝐶) ∪ (𝐵 “ 𝐶)) | ||
Theorem | dminss 5977 | An upper bound for intersection with a domain. Theorem 40 of [Suppes] p. 66, who calls it "somewhat surprising." (Contributed by NM, 11-Aug-2004.) |
⊢ (dom 𝑅 ∩ 𝐴) ⊆ (◡𝑅 “ (𝑅 “ 𝐴)) | ||
Theorem | imainss 5978 | An upper bound for intersection with an image. Theorem 41 of [Suppes] p. 66. (Contributed by NM, 11-Aug-2004.) |
⊢ ((𝑅 “ 𝐴) ∩ 𝐵) ⊆ (𝑅 “ (𝐴 ∩ (◡𝑅 “ 𝐵))) | ||
Theorem | inimass 5979 | The image of an intersection. (Contributed by Thierry Arnoux, 16-Dec-2017.) |
⊢ ((𝐴 ∩ 𝐵) “ 𝐶) ⊆ ((𝐴 “ 𝐶) ∩ (𝐵 “ 𝐶)) | ||
Theorem | inimasn 5980 | The intersection of the image of singleton. (Contributed by Thierry Arnoux, 16-Dec-2017.) |
⊢ (𝐶 ∈ 𝑉 → ((𝐴 ∩ 𝐵) “ {𝐶}) = ((𝐴 “ {𝐶}) ∩ (𝐵 “ {𝐶}))) | ||
Theorem | cnvxp 5981 | The converse of a Cartesian product. Exercise 11 of [Suppes] p. 67. (Contributed by NM, 14-Aug-1999.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ◡(𝐴 × 𝐵) = (𝐵 × 𝐴) | ||
Theorem | xp0 5982 | The Cartesian product with the empty set is empty. Part of Theorem 3.13(ii) of [Monk1] p. 37. (Contributed by NM, 12-Apr-2004.) |
⊢ (𝐴 × ∅) = ∅ | ||
Theorem | xpnz 5983 | The Cartesian product of nonempty classes is nonempty. (Variation of a theorem contributed by Raph Levien, 30-Jun-2006.) (Contributed by NM, 30-Jun-2006.) |
⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ↔ (𝐴 × 𝐵) ≠ ∅) | ||
Theorem | xpeq0 5984 | At least one member of an empty Cartesian product is empty. (Contributed by NM, 27-Aug-2006.) |
⊢ ((𝐴 × 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅)) | ||
Theorem | xpdisj1 5985 | Cartesian products with disjoint sets are disjoint. (Contributed by NM, 13-Sep-2004.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 × 𝐶) ∩ (𝐵 × 𝐷)) = ∅) | ||
Theorem | xpdisj2 5986 | Cartesian products with disjoint sets are disjoint. (Contributed by NM, 13-Sep-2004.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐶 × 𝐴) ∩ (𝐷 × 𝐵)) = ∅) | ||
Theorem | xpsndisj 5987 | Cartesian products with two different singletons are disjoint. (Contributed by NM, 28-Jul-2004.) |
⊢ (𝐵 ≠ 𝐷 → ((𝐴 × {𝐵}) ∩ (𝐶 × {𝐷})) = ∅) | ||
Theorem | difxp 5988 | Difference of Cartesian products, expressed in terms of a union of Cartesian products of differences. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 26-Jun-2014.) |
⊢ ((𝐶 × 𝐷) ∖ (𝐴 × 𝐵)) = (((𝐶 ∖ 𝐴) × 𝐷) ∪ (𝐶 × (𝐷 ∖ 𝐵))) | ||
Theorem | difxp1 5989 | Difference law for Cartesian product. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 26-Jun-2014.) |
⊢ ((𝐴 ∖ 𝐵) × 𝐶) = ((𝐴 × 𝐶) ∖ (𝐵 × 𝐶)) | ||
Theorem | difxp2 5990 | Difference law for Cartesian product. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 26-Jun-2014.) |
⊢ (𝐴 × (𝐵 ∖ 𝐶)) = ((𝐴 × 𝐵) ∖ (𝐴 × 𝐶)) | ||
Theorem | djudisj 5991* | Disjoint unions with disjoint index sets are disjoint. (Contributed by Stefan O'Rear, 21-Nov-2014.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → (∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐶) ∩ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝐷)) = ∅) | ||
Theorem | xpdifid 5992* | The set of distinct couples in a Cartesian product. (Contributed by Thierry Arnoux, 25-May-2019.) |
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ {𝑥})) = ((𝐴 × 𝐵) ∖ I ) | ||
Theorem | resdisj 5993 | A double restriction to disjoint classes is the empty set. (Contributed by NM, 7-Oct-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐶 ↾ 𝐴) ↾ 𝐵) = ∅) | ||
Theorem | rnxp 5994 | The range of a Cartesian product. Part of Theorem 3.13(x) of [Monk1] p. 37. (Contributed by NM, 12-Apr-2004.) |
⊢ (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵) | ||
Theorem | dmxpss 5995 | The domain of a Cartesian product is included in its first factor. (Contributed by NM, 19-Mar-2007.) |
⊢ dom (𝐴 × 𝐵) ⊆ 𝐴 | ||
Theorem | rnxpss 5996 | The range of a Cartesian product is included in its second factor. (Contributed by NM, 16-Jan-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ran (𝐴 × 𝐵) ⊆ 𝐵 | ||
Theorem | rnxpid 5997 | The range of a Cartesian square. (Contributed by FL, 17-May-2010.) |
⊢ ran (𝐴 × 𝐴) = 𝐴 | ||
Theorem | ssxpb 5998 | A Cartesian product subclass relationship is equivalent to the conjunction of the analogous relationships for the factors. (Contributed by NM, 17-Dec-2008.) |
⊢ ((𝐴 × 𝐵) ≠ ∅ → ((𝐴 × 𝐵) ⊆ (𝐶 × 𝐷) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷))) | ||
Theorem | xp11 5999 | The Cartesian product of nonempty classes is a one-to-one "function" of its two "arguments". In other words, two Cartesian products, at least one with nonempty factors, are equal if and only if their respective factors are equal. (Contributed by NM, 31-May-2008.) |
⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((𝐴 × 𝐵) = (𝐶 × 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | xpcan 6000 | Cancellation law for Cartesian product. (Contributed by NM, 30-Aug-2011.) |
⊢ (𝐶 ≠ ∅ → ((𝐶 × 𝐴) = (𝐶 × 𝐵) ↔ 𝐴 = 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |