Home | Metamath
Proof Explorer Theorem List (p. 55 of 424) | < 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: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 0ima 5401 | Image under the empty relation. (Contributed by FL, 11-Jan-2007.) |
⊢ (∅ “ 𝐴) = ∅ | ||
Theorem | csbima12 5402 | 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 5403 | A class whose image under another is empty is disjoint with the other's domain. (Contributed by FL, 24-Jan-2007.) |
⊢ ((𝐴 “ 𝐵) = ∅ ↔ (dom 𝐴 ∩ 𝐵) = ∅) | ||
Theorem | cnvimass 5404 | A preimage under any class is included in the domain of the class. (Contributed by FL, 29-Jan-2007.) |
⊢ (◡𝐴 “ 𝐵) ⊆ dom 𝐴 | ||
Theorem | cnvimarndm 5405 | 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 5406* | The image of a singleton. (Contributed by NM, 8-May-2005.) |
⊢ (𝐴 ∈ 𝐵 → (𝑅 “ {𝐴}) = {𝑦 ∣ 𝐴𝑅𝑦}) | ||
Theorem | relimasn 5407* | The image of a singleton. (Contributed by NM, 20-May-1998.) |
⊢ (Rel 𝑅 → (𝑅 “ {𝐴}) = {𝑦 ∣ 𝐴𝑅𝑦}) | ||
Theorem | elrelimasn 5408 | Elementhood in the image of a singleton. (Contributed by Mario Carneiro, 3-Nov-2015.) |
⊢ (Rel 𝑅 → (𝐵 ∈ (𝑅 “ {𝐴}) ↔ 𝐴𝑅𝐵)) | ||
Theorem | elimasn 5409 | 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 5410 | Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐶 ∈ (𝐴 “ {𝐵}) ↔ 〈𝐵, 𝐶〉 ∈ 𝐴)) | ||
Theorem | elimasni 5411 | Membership in an image of a singleton. (Contributed by NM, 5-Aug-2010.) |
⊢ (𝐶 ∈ (𝐴 “ {𝐵}) → 𝐵𝐴𝐶) | ||
Theorem | args 5412* | 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 6100 of function value, which is based on the idea in Quine's definition. (Contributed by NM, 8-May-2005.) |
⊢ {𝑥 ∣ ∃𝑦(𝐹 “ {𝑥}) = {𝑦}} = {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦} | ||
Theorem | eliniseg 5413 | 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 5414 | Any set is equal to its preimage under the converse epsilon relation. (Contributed by Mario Carneiro, 9-Mar-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (◡ E “ {𝐴}) = 𝐴 | ||
Theorem | iniseg 5415* | 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 5416 | Nonemptyness of an initial segment in terms of range. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ (𝐴 ∈ ran 𝐹 ↔ (◡𝐹 “ {𝐴}) ≠ ∅) | ||
Theorem | dffr3 5417* | 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 5418* | Alternate definition of set-like relation. (Contributed by Mario Carneiro, 23-Jun-2015.) |
⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 (𝐴 ∩ (◡𝑅 “ {𝑥})) ∈ V) | ||
Theorem | imass1 5419 | Subset theorem for image. (Contributed by NM, 16-Mar-2004.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐴 “ 𝐶) ⊆ (𝐵 “ 𝐶)) | ||
Theorem | imass2 5420 | Subset theorem for image. Exercise 22(a) of [Enderton] p. 53. (Contributed by NM, 22-Mar-1998.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵)) | ||
Theorem | ndmima 5421 | 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 5422 | A converse is a relation. Theorem 12 of [Suppes] p. 62. (Contributed by NM, 29-Oct-1996.) |
⊢ Rel ◡𝐴 | ||
Theorem | relbrcnvg 5423 | When 𝑅 is a relation, the sethood assumptions on brcnv 5227 can be omitted. (Contributed by Mario Carneiro, 28-Apr-2015.) |
⊢ (Rel 𝑅 → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)) | ||
Theorem | eliniseg2 5424 | Eliminate the class existence constraint in eliniseg 5413. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 17-Nov-2015.) |
⊢ (Rel 𝐴 → (𝐶 ∈ (◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵)) | ||
Theorem | relbrcnv 5425 | When 𝑅 is a relation, the sethood assumptions on brcnv 5227 can be omitted. (Contributed by Mario Carneiro, 28-Apr-2015.) |
⊢ Rel 𝑅 ⇒ ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴) | ||
Theorem | cotrg 5426* | Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr 5427 for the main application. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Generalized from its special instance cotr 5427. (Revised by Richard Penner, 24-Dec-2019.) |
⊢ ((𝐴 ∘ 𝐵) ⊆ 𝐶 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)) | ||
Theorem | cotr 5427* | Two ways of saying a relation is transitive. Definition of transitivity in [Schechter] p. 51. Special instance of cotrg 5426. (Contributed by NM, 27-Dec-1996.) |
⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) | ||
Theorem | issref 5428* | Two ways to state a relation is reflexive. Adapted from Tarski. (Contributed by FL, 15-Jan-2012.) (Revised by NM, 30-Mar-2016.) |
⊢ (( I ↾ 𝐴) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 𝑥𝑅𝑥) | ||
Theorem | cnvsym 5429* | 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 5430* | 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 5431* | Two ways of saying a relation is antisymmetric and reflexive. ∪ ∪ 𝑅 is the field of a relation by relfld 5578. (Contributed by NM, 6-May-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ((𝑅 ∩ ◡𝑅) = ( I ↾ ∪ ∪ 𝑅) ↔ ∀𝑥 ∈ ∪ ∪ 𝑅∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ 𝑥 = 𝑦)) | ||
Theorem | asymref2 5432* | 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 5433* | 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 5434* | Two ways of saying that two elements have an upper bound. (Contributed by Mario Carneiro, 3-Nov-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(◡𝑅 ∘ 𝑅)𝐵 ↔ ∃𝑧(𝐴𝑅𝑧 ∧ 𝐵𝑅𝑧))) | ||
Theorem | codir 5435* | Two ways of saying a relation is directed. (Contributed by Mario Carneiro, 22-Nov-2013.) |
⊢ ((𝐴 × 𝐵) ⊆ (◡𝑅 ∘ 𝑅) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∃𝑧(𝑥𝑅𝑧 ∧ 𝑦𝑅𝑧)) | ||
Theorem | qfto 5436* | A quantifier-free way of expressing the total order predicate. (Contributed by Mario Carneiro, 22-Nov-2013.) |
⊢ ((𝐴 × 𝐵) ⊆ (𝑅 ∪ ◡𝑅) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥)) | ||
Theorem | xpidtr 5437 | A square Cartesian product (𝐴 × 𝐴) is a transitive relation. (Contributed by FL, 31-Jul-2009.) |
⊢ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) | ||
Theorem | trin2 5438 | The intersection of two transitive classes is transitive. (Contributed by FL, 31-Jul-2009.) |
⊢ (((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ((𝑅 ∩ 𝑆) ∘ (𝑅 ∩ 𝑆)) ⊆ (𝑅 ∩ 𝑆)) | ||
Theorem | poirr2 5439 | A partial order relation is irreflexive. (Contributed by Mario Carneiro, 2-Nov-2015.) |
⊢ (𝑅 Po 𝐴 → (𝑅 ∩ ( I ↾ 𝐴)) = ∅) | ||
Theorem | trinxp 5440 | The relation induced by a transitive relation on a part of its field is transitive. (Taking the intersection of a relation with a square Cartesian product is a way to restrict it to a subset of its field.) (Contributed by FL, 31-Jul-2009.) |
⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 → ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ (𝑅 ∩ (𝐴 × 𝐴))) | ||
Theorem | soirri 5441 | A strict order relation is irreflexive. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.) |
⊢ 𝑅 Or 𝑆 & ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ¬ 𝐴𝑅𝐴 | ||
Theorem | sotri 5442 | A strict order relation is a transitive relation. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.) |
⊢ 𝑅 Or 𝑆 & ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) | ||
Theorem | son2lpi 5443 | 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 5444 | A transitivity relation. (Read 𝐴 ≤ 𝐵 and 𝐵 < 𝐶 implies 𝐴 < 𝐶.) (Contributed by Mario Carneiro, 10-May-2013.) |
⊢ 𝑅 Or 𝑆 & ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ ¬ 𝐵𝑅𝐴 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) | ||
Theorem | sotri3 5445 | A transitivity relation. (Read 𝐴 < 𝐵 and 𝐵 ≤ 𝐶 implies 𝐴 < 𝐶.) (Contributed by Mario Carneiro, 10-May-2013.) |
⊢ 𝑅 Or 𝑆 & ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐴𝑅𝐵 ∧ ¬ 𝐶𝑅𝐵) → 𝐴𝑅𝐶) | ||
Theorem | poleloe 5446 | Express "less than or equals" for general strict orders. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴(𝑅 ∪ I )𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵))) | ||
Theorem | poltletr 5447 | Transitive law for general strict orders. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝑅 Po 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑅𝐵 ∧ 𝐵(𝑅 ∪ I )𝐶) → 𝐴𝑅𝐶)) | ||
Theorem | somin1 5448 | Property of a minimum in a strict order. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝑅 Or 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → if(𝐴𝑅𝐵, 𝐴, 𝐵)(𝑅 ∪ I )𝐴) | ||
Theorem | somincom 5449 | Commutativity of minimum in a total order. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝑅 Or 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → if(𝐴𝑅𝐵, 𝐴, 𝐵) = if(𝐵𝑅𝐴, 𝐵, 𝐴)) | ||
Theorem | somin2 5450 | Property of a minimum in a strict order. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝑅 Or 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → if(𝐴𝑅𝐵, 𝐴, 𝐵)(𝑅 ∪ I )𝐵) | ||
Theorem | soltmin 5451 | Being less than a minimum, for a general total order. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝑅 Or 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶) ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑅𝐶))) | ||
Theorem | cnvopab 5452* | 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 5453* | The converse of a mapping function. (Contributed by Thierry Arnoux, 16-Jan-2017.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐷))) ⇒ ⊢ (𝜑 → ◡(𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | cnv0 5454 | The converse of the empty set. (Contributed by NM, 6-Apr-1998.) Remove dependency on ax-sep 4709, ax-nul 4717, ax-pr 4833. (Revised by KP, 25-Oct-2021.) |
⊢ ◡∅ = ∅ | ||
Theorem | cnv0OLD 5455 | Obsolete version of cnv0 5454 as of 25-Oct-2021. (Contributed by NM, 6-Apr-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ◡∅ = ∅ | ||
Theorem | cnvi 5456 | 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 5457 | 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 5458 | Distributive law for converse over class difference. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ ◡(𝐴 ∖ 𝐵) = (◡𝐴 ∖ ◡𝐵) | ||
Theorem | cnvin 5459 | 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 5460 | Distributive law for range over union. Theorem 8 of [Suppes] p. 60. (Contributed by NM, 24-Mar-1998.) |
⊢ ran (𝐴 ∪ 𝐵) = (ran 𝐴 ∪ ran 𝐵) | ||
Theorem | rnin 5461 | 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 5462 | The range of an indexed union. (Contributed by Mario Carneiro, 29-May-2015.) |
⊢ ran ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ran 𝐵 | ||
Theorem | rnuni 5463* | 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 5464 | Distributive law for image over union. Theorem 35 of [Suppes] p. 65. (Contributed by NM, 30-Sep-2002.) |
⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶)) | ||
Theorem | imaundir 5465 | The image of a union. (Contributed by Jeff Hoffman, 17-Feb-2008.) |
⊢ ((𝐴 ∪ 𝐵) “ 𝐶) = ((𝐴 “ 𝐶) ∪ (𝐵 “ 𝐶)) | ||
Theorem | dminss 5466 | 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 5467 | An upper bound for intersection with an image. Theorem 41 of [Suppes] p. 66. (Contributed by NM, 11-Aug-2004.) |
⊢ ((𝑅 “ 𝐴) ∩ 𝐵) ⊆ (𝑅 “ (𝐴 ∩ (◡𝑅 “ 𝐵))) | ||
Theorem | inimass 5468 | The image of an intersection. (Contributed by Thierry Arnoux, 16-Dec-2017.) |
⊢ ((𝐴 ∩ 𝐵) “ 𝐶) ⊆ ((𝐴 “ 𝐶) ∩ (𝐵 “ 𝐶)) | ||
Theorem | inimasn 5469 | The intersection of the image of singleton. (Contributed by Thierry Arnoux, 16-Dec-2017.) |
⊢ (𝐶 ∈ 𝑉 → ((𝐴 ∩ 𝐵) “ {𝐶}) = ((𝐴 “ {𝐶}) ∩ (𝐵 “ {𝐶}))) | ||
Theorem | cnvxp 5470 | 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 5471 | 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 5472 | 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 5473 | At least one member of an empty Cartesian product is empty. (Contributed by NM, 27-Aug-2006.) |
⊢ ((𝐴 × 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅)) | ||
Theorem | xpdisj1 5474 | Cartesian products with disjoint sets are disjoint. (Contributed by NM, 13-Sep-2004.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 × 𝐶) ∩ (𝐵 × 𝐷)) = ∅) | ||
Theorem | xpdisj2 5475 | Cartesian products with disjoint sets are disjoint. (Contributed by NM, 13-Sep-2004.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐶 × 𝐴) ∩ (𝐷 × 𝐵)) = ∅) | ||
Theorem | xpsndisj 5476 | Cartesian products with two different singletons are disjoint. (Contributed by NM, 28-Jul-2004.) |
⊢ (𝐵 ≠ 𝐷 → ((𝐴 × {𝐵}) ∩ (𝐶 × {𝐷})) = ∅) | ||
Theorem | difxp 5477 | 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 5478 | Difference law for Cartesian product. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 26-Jun-2014.) |
⊢ ((𝐴 ∖ 𝐵) × 𝐶) = ((𝐴 × 𝐶) ∖ (𝐵 × 𝐶)) | ||
Theorem | difxp2 5479 | Difference law for Cartesian product. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 26-Jun-2014.) |
⊢ (𝐴 × (𝐵 ∖ 𝐶)) = ((𝐴 × 𝐵) ∖ (𝐴 × 𝐶)) | ||
Theorem | djudisj 5480* | Disjoint unions with disjoint index sets are disjoint. (Contributed by Stefan O'Rear, 21-Nov-2014.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → (∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐶) ∩ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝐷)) = ∅) | ||
Theorem | xpdifid 5481* | The set of distinct couples in a Cartesian product. (Contributed by Thierry Arnoux, 25-May-2019.) |
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ {𝑥})) = ((𝐴 × 𝐵) ∖ I ) | ||
Theorem | resdisj 5482 | 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 5483 | 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 5484 | The domain of a Cartesian product is a subclass of the first factor. (Contributed by NM, 19-Mar-2007.) |
⊢ dom (𝐴 × 𝐵) ⊆ 𝐴 | ||
Theorem | rnxpss 5485 | The range of a Cartesian product is a subclass of the second factor. (Contributed by NM, 16-Jan-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ran (𝐴 × 𝐵) ⊆ 𝐵 | ||
Theorem | rnxpid 5486 | The range of a square Cartesian product. (Contributed by FL, 17-May-2010.) |
⊢ ran (𝐴 × 𝐴) = 𝐴 | ||
Theorem | ssxpb 5487 | A Cartesian product subclass relationship is equivalent to the relationship for it components. (Contributed by NM, 17-Dec-2008.) |
⊢ ((𝐴 × 𝐵) ≠ ∅ → ((𝐴 × 𝐵) ⊆ (𝐶 × 𝐷) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷))) | ||
Theorem | xp11 5488 | The Cartesian product of nonempty classes is one-to-one. (Contributed by NM, 31-May-2008.) |
⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ((𝐴 × 𝐵) = (𝐶 × 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | xpcan 5489 | Cancellation law for Cartesian product. (Contributed by NM, 30-Aug-2011.) |
⊢ (𝐶 ≠ ∅ → ((𝐶 × 𝐴) = (𝐶 × 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | xpcan2 5490 | Cancellation law for Cartesian product. (Contributed by NM, 30-Aug-2011.) |
⊢ (𝐶 ≠ ∅ → ((𝐴 × 𝐶) = (𝐵 × 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | ssrnres 5491 | Subset of the range of a restriction. (Contributed by NM, 16-Jan-2006.) |
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) ↔ ran (𝐶 ∩ (𝐴 × 𝐵)) = 𝐵) | ||
Theorem | rninxp 5492* | Range of the intersection with a Cartesian product. (Contributed by NM, 17-Jan-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (ran (𝐶 ∩ (𝐴 × 𝐵)) = 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑥𝐶𝑦) | ||
Theorem | dminxp 5493* | Domain of the intersection with a Cartesian product. (Contributed by NM, 17-Jan-2006.) |
⊢ (dom (𝐶 ∩ (𝐴 × 𝐵)) = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥𝐶𝑦) | ||
Theorem | imainrect 5494 | Image of a relation restricted to a rectangular region. (Contributed by Stefan O'Rear, 19-Feb-2015.) |
⊢ ((𝐺 ∩ (𝐴 × 𝐵)) “ 𝑌) = ((𝐺 “ (𝑌 ∩ 𝐴)) ∩ 𝐵) | ||
Theorem | xpima 5495 | The image by a constant function (or other Cartesian product). (Contributed by Thierry Arnoux, 4-Feb-2017.) |
⊢ ((𝐴 × 𝐵) “ 𝐶) = if((𝐴 ∩ 𝐶) = ∅, ∅, 𝐵) | ||
Theorem | xpima1 5496 | The image by a Cartesian product. (Contributed by Thierry Arnoux, 16-Dec-2017.) |
⊢ ((𝐴 ∩ 𝐶) = ∅ → ((𝐴 × 𝐵) “ 𝐶) = ∅) | ||
Theorem | xpima2 5497 | The image by a Cartesian product. (Contributed by Thierry Arnoux, 16-Dec-2017.) |
⊢ ((𝐴 ∩ 𝐶) ≠ ∅ → ((𝐴 × 𝐵) “ 𝐶) = 𝐵) | ||
Theorem | xpimasn 5498 | The image of a singleton by a Cartesian product. (Contributed by Thierry Arnoux, 14-Jan-2018.) (Proof shortened by BJ, 6-Apr-2019.) |
⊢ (𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = 𝐵) | ||
Theorem | sossfld 5499 | The base set of a strict order is contained in the field of the relation, except possibly for one element (note that ∅ Or {𝐵}). (Contributed by Mario Carneiro, 27-Apr-2015.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐴 ∖ {𝐵}) ⊆ (dom 𝑅 ∪ ran 𝑅)) | ||
Theorem | sofld 5500 | The base set of a nonempty strict order is the same as the field of the relation. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝑅 ⊆ (𝐴 × 𝐴) ∧ 𝑅 ≠ ∅) → 𝐴 = (dom 𝑅 ∪ ran 𝑅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |