![]() |
Metamath
Proof Explorer Theorem List (p. 62 of 480) | < 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-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | imass2 6101 | Subset theorem for image. Exercise 22(a) of [Enderton] p. 53. (Contributed by NM, 22-Mar-1998.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵)) | ||
Theorem | ndmima 6102 | 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 6103 | A converse is a relation. Theorem 12 of [Suppes] p. 62. (Contributed by NM, 29-Oct-1996.) |
⊢ Rel ◡𝐴 | ||
Theorem | relbrcnvg 6104 | When 𝑅 is a relation, the sethood assumptions on brcnv 5882 can be omitted. (Contributed by Mario Carneiro, 28-Apr-2015.) |
⊢ (Rel 𝑅 → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)) | ||
Theorem | eliniseg2 6105 | Eliminate the class existence constraint in eliniseg 6093. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 17-Nov-2015.) |
⊢ (Rel 𝐴 → (𝐶 ∈ (◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵)) | ||
Theorem | relbrcnv 6106 | When 𝑅 is a relation, the sethood assumptions on brcnv 5882 can be omitted. (Contributed by Mario Carneiro, 28-Apr-2015.) |
⊢ Rel 𝑅 ⇒ ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴) | ||
Theorem | relco 6107 | A composition is a relation. Exercise 24 of [TakeutiZaring] p. 25. (Contributed by NM, 26-Jan-1997.) |
⊢ Rel (𝐴 ∘ 𝐵) | ||
Theorem | cotrg 6108* | Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr 6111 for the main application. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Generalized from its special instance cotr 6111. (Revised by Richard Penner, 24-Dec-2019.) (Proof shortened by SN, 19-Dec-2024.) Avoid ax-11 2154. (Revised by BTernaryTau, 29-Dec-2024.) |
⊢ ((𝐴 ∘ 𝐵) ⊆ 𝐶 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)) | ||
Theorem | cotrgOLD 6109* | Obsolete version of cotrg 6108 as of 29-Dec-2024. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Generalized from its special instance cotr 6111. (Revised by Richard Penner, 24-Dec-2019.) (Proof shortened by SN, 19-Dec-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∘ 𝐵) ⊆ 𝐶 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)) | ||
Theorem | cotrgOLDOLD 6110* | Obsolete version of cotrg 6108 as of 19-Dec-2024. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Generalized from its special instance cotr 6111. (Revised by Richard Penner, 24-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∘ 𝐵) ⊆ 𝐶 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)) | ||
Theorem | cotr 6111* | Two ways of saying a relation is transitive. Definition of transitivity in [Schechter] p. 51. Special instance of cotrg 6108. (Contributed by NM, 27-Dec-1996.) |
⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) | ||
Theorem | idrefALT 6112* | Alternate proof of idref 7146 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 6113* | 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.) (Proof shortened by SN, 23-Dec-2024.) Avoid ax-11 2154. (Revised by BTernaryTau, 29-Dec-2024.) |
⊢ (◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) | ||
Theorem | cnvsymOLD 6114* | Obsolete proof of cnvsym 6113 as of 29-Dec-2024. (Contributed by NM, 28-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof shortened by SN, 23-Dec-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) | ||
Theorem | cnvsymOLDOLD 6115* | Obsolete proof of cnvsym 6113 as of 23-Dec-2024. (Contributed by NM, 28-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) | ||
Theorem | intasym 6116* | 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 6117* | Two ways of saying a relation is antisymmetric and reflexive. ∪ ∪ 𝑅 is the field of a relation by relfld 6274. (Contributed by NM, 6-May-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ((𝑅 ∩ ◡𝑅) = ( I ↾ ∪ ∪ 𝑅) ↔ ∀𝑥 ∈ ∪ ∪ 𝑅∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ 𝑥 = 𝑦)) | ||
Theorem | asymref2 6118* | 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 6119* | 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 6120* | Two ways of saying that two elements have an upper bound. (Contributed by Mario Carneiro, 3-Nov-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(◡𝑅 ∘ 𝑅)𝐵 ↔ ∃𝑧(𝐴𝑅𝑧 ∧ 𝐵𝑅𝑧))) | ||
Theorem | codir 6121* | Two ways of saying a relation is directed. (Contributed by Mario Carneiro, 22-Nov-2013.) |
⊢ ((𝐴 × 𝐵) ⊆ (◡𝑅 ∘ 𝑅) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∃𝑧(𝑥𝑅𝑧 ∧ 𝑦𝑅𝑧)) | ||
Theorem | qfto 6122* | A quantifier-free way of expressing the total order predicate. (Contributed by Mario Carneiro, 22-Nov-2013.) |
⊢ ((𝐴 × 𝐵) ⊆ (𝑅 ∪ ◡𝑅) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥)) | ||
Theorem | xpidtr 6123 | A Cartesian square is a transitive relation. (Contributed by FL, 31-Jul-2009.) |
⊢ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) | ||
Theorem | trin2 6124 | The intersection of two transitive classes is transitive. (Contributed by FL, 31-Jul-2009.) |
⊢ (((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ((𝑅 ∩ 𝑆) ∘ (𝑅 ∩ 𝑆)) ⊆ (𝑅 ∩ 𝑆)) | ||
Theorem | poirr2 6125 | A partial order is irreflexive. (Contributed by Mario Carneiro, 2-Nov-2015.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ (𝑅 Po 𝐴 → (𝑅 ∩ ( I ↾ 𝐴)) = ∅) | ||
Theorem | trinxp 6126 | 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 6127 | A strict order relation is irreflexive. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.) |
⊢ 𝑅 Or 𝑆 & ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ¬ 𝐴𝑅𝐴 | ||
Theorem | sotri 6128 | A strict order relation is a transitive relation. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.) |
⊢ 𝑅 Or 𝑆 & ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) | ||
Theorem | son2lpi 6129 | 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 6130 | A transitivity relation. (Read 𝐴 ≤ 𝐵 and 𝐵 < 𝐶 implies 𝐴 < 𝐶.) (Contributed by Mario Carneiro, 10-May-2013.) |
⊢ 𝑅 Or 𝑆 & ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ ¬ 𝐵𝑅𝐴 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) | ||
Theorem | sotri3 6131 | A transitivity relation. (Read 𝐴 < 𝐵 and 𝐵 ≤ 𝐶 implies 𝐴 < 𝐶.) (Contributed by Mario Carneiro, 10-May-2013.) |
⊢ 𝑅 Or 𝑆 & ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐴𝑅𝐵 ∧ ¬ 𝐶𝑅𝐵) → 𝐴𝑅𝐶) | ||
Theorem | poleloe 6132 | Express "less than or equals" for general strict orders. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴(𝑅 ∪ I )𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵))) | ||
Theorem | poltletr 6133 | Transitive law for general strict orders. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝑅 Po 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑅𝐵 ∧ 𝐵(𝑅 ∪ I )𝐶) → 𝐴𝑅𝐶)) | ||
Theorem | somin1 6134 | Property of a minimum in a strict order. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝑅 Or 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → if(𝐴𝑅𝐵, 𝐴, 𝐵)(𝑅 ∪ I )𝐴) | ||
Theorem | somincom 6135 | Commutativity of minimum in a total order. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝑅 Or 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → if(𝐴𝑅𝐵, 𝐴, 𝐵) = if(𝐵𝑅𝐴, 𝐵, 𝐴)) | ||
Theorem | somin2 6136 | Property of a minimum in a strict order. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝑅 Or 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → if(𝐴𝑅𝐵, 𝐴, 𝐵)(𝑅 ∪ I )𝐵) | ||
Theorem | soltmin 6137 | Being less than a minimum, for a general total order. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝑅 Or 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶) ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑅𝐶))) | ||
Theorem | cnvopab 6138* | 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 6139* | The converse of a mapping function. (Contributed by Thierry Arnoux, 16-Jan-2017.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐷))) ⇒ ⊢ (𝜑 → ◡(𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | cnv0 6140 | The converse of the empty set. (Contributed by NM, 6-Apr-1998.) Remove dependency on ax-sep 5299, ax-nul 5306, ax-pr 5427. (Revised by KP, 25-Oct-2021.) |
⊢ ◡∅ = ∅ | ||
Theorem | cnvi 6141 | 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 6142 | 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 6143 | Distributive law for converse over class difference. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ ◡(𝐴 ∖ 𝐵) = (◡𝐴 ∖ ◡𝐵) | ||
Theorem | cnvin 6144 | 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 6145 | Distributive law for range over union. Theorem 8 of [Suppes] p. 60. (Contributed by NM, 24-Mar-1998.) |
⊢ ran (𝐴 ∪ 𝐵) = (ran 𝐴 ∪ ran 𝐵) | ||
Theorem | rnin 6146 | 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 6147 | The range of an indexed union. (Contributed by Mario Carneiro, 29-May-2015.) |
⊢ ran ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ran 𝐵 | ||
Theorem | rnuni 6148* | 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 6149 | Distributive law for image over union. Theorem 35 of [Suppes] p. 65. (Contributed by NM, 30-Sep-2002.) |
⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶)) | ||
Theorem | imaundir 6150 | The image of a union. (Contributed by Jeff Hoffman, 17-Feb-2008.) |
⊢ ((𝐴 ∪ 𝐵) “ 𝐶) = ((𝐴 “ 𝐶) ∪ (𝐵 “ 𝐶)) | ||
Theorem | cnvimassrndm 6151 | The preimage of a superset of the range of a class is the domain of the class. Generalization of cnvimarndm 6081 for subsets. (Contributed by AV, 18-Sep-2024.) |
⊢ (ran 𝐹 ⊆ 𝐴 → (◡𝐹 “ 𝐴) = dom 𝐹) | ||
Theorem | dminss 6152 | 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 6153 | An upper bound for intersection with an image. Theorem 41 of [Suppes] p. 66. (Contributed by NM, 11-Aug-2004.) |
⊢ ((𝑅 “ 𝐴) ∩ 𝐵) ⊆ (𝑅 “ (𝐴 ∩ (◡𝑅 “ 𝐵))) | ||
Theorem | inimass 6154 | The image of an intersection. (Contributed by Thierry Arnoux, 16-Dec-2017.) |
⊢ ((𝐴 ∩ 𝐵) “ 𝐶) ⊆ ((𝐴 “ 𝐶) ∩ (𝐵 “ 𝐶)) | ||
Theorem | inimasn 6155 | The intersection of the image of singleton. (Contributed by Thierry Arnoux, 16-Dec-2017.) |
⊢ (𝐶 ∈ 𝑉 → ((𝐴 ∩ 𝐵) “ {𝐶}) = ((𝐴 “ {𝐶}) ∩ (𝐵 “ {𝐶}))) | ||
Theorem | cnvxp 6156 | 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 6157 | 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 6158 | 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 6159 | At least one member of an empty Cartesian product is empty. (Contributed by NM, 27-Aug-2006.) |
⊢ ((𝐴 × 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅)) | ||
Theorem | xpdisj1 6160 | Cartesian products with disjoint sets are disjoint. (Contributed by NM, 13-Sep-2004.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 × 𝐶) ∩ (𝐵 × 𝐷)) = ∅) | ||
Theorem | xpdisj2 6161 | Cartesian products with disjoint sets are disjoint. (Contributed by NM, 13-Sep-2004.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐶 × 𝐴) ∩ (𝐷 × 𝐵)) = ∅) | ||
Theorem | xpsndisj 6162 | Cartesian products with two different singletons are disjoint. (Contributed by NM, 28-Jul-2004.) |
⊢ (𝐵 ≠ 𝐷 → ((𝐴 × {𝐵}) ∩ (𝐶 × {𝐷})) = ∅) | ||
Theorem | difxp 6163 | 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 6164 | Difference law for Cartesian product. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 26-Jun-2014.) |
⊢ ((𝐴 ∖ 𝐵) × 𝐶) = ((𝐴 × 𝐶) ∖ (𝐵 × 𝐶)) | ||
Theorem | difxp2 6165 | Difference law for Cartesian product. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 26-Jun-2014.) |
⊢ (𝐴 × (𝐵 ∖ 𝐶)) = ((𝐴 × 𝐵) ∖ (𝐴 × 𝐶)) | ||
Theorem | djudisj 6166* | Disjoint unions with disjoint index sets are disjoint. (Contributed by Stefan O'Rear, 21-Nov-2014.) |
⊢ ((𝐴 ∩ 𝐵) = ∅ → (∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐶) ∩ ∪ 𝑦 ∈ 𝐵 ({𝑦} × 𝐷)) = ∅) | ||
Theorem | xpdifid 6167* | The set of distinct couples in a Cartesian product. (Contributed by Thierry Arnoux, 25-May-2019.) |
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ {𝑥})) = ((𝐴 × 𝐵) ∖ I ) | ||
Theorem | resdisj 6168 | 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 6169 | 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 6170 | The domain of a Cartesian product is included in its first factor. (Contributed by NM, 19-Mar-2007.) |
⊢ dom (𝐴 × 𝐵) ⊆ 𝐴 | ||
Theorem | rnxpss 6171 | 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 6172 | The range of a Cartesian square. (Contributed by FL, 17-May-2010.) |
⊢ ran (𝐴 × 𝐴) = 𝐴 | ||
Theorem | ssxpb 6173 | 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 6174 | 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 6175 | Cancellation law for Cartesian product. (Contributed by NM, 30-Aug-2011.) |
⊢ (𝐶 ≠ ∅ → ((𝐶 × 𝐴) = (𝐶 × 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | xpcan2 6176 | Cancellation law for Cartesian product. (Contributed by NM, 30-Aug-2011.) |
⊢ (𝐶 ≠ ∅ → ((𝐴 × 𝐶) = (𝐵 × 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | ssrnres 6177 | Two ways to express surjectivity of a restricted and corestricted binary relation (intersection of a binary relation with a Cartesian product): the LHS expresses inclusion in the range of the restricted relation, while the RHS expresses equality with the range of the restricted and corestricted relation. (Contributed by NM, 16-Jan-2006.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) ↔ ran (𝐶 ∩ (𝐴 × 𝐵)) = 𝐵) | ||
Theorem | rninxp 6178* | Two ways to express surjectivity of a restricted and corestricted binary relation (intersection of a binary relation with a Cartesian product). (Contributed by NM, 17-Jan-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (ran (𝐶 ∩ (𝐴 × 𝐵)) = 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑥𝐶𝑦) | ||
Theorem | dminxp 6179* | Two ways to express totality of a restricted and corestricted binary relation (intersection of a binary relation with a Cartesian product). (Contributed by NM, 17-Jan-2006.) |
⊢ (dom (𝐶 ∩ (𝐴 × 𝐵)) = 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥𝐶𝑦) | ||
Theorem | imainrect 6180 | Image by a restricted and corestricted binary relation (intersection of a binary relation with a Cartesian product). (Contributed by Stefan O'Rear, 19-Feb-2015.) |
⊢ ((𝐺 ∩ (𝐴 × 𝐵)) “ 𝑌) = ((𝐺 “ (𝑌 ∩ 𝐴)) ∩ 𝐵) | ||
Theorem | xpima 6181 | Direct image by a Cartesian product. (Contributed by Thierry Arnoux, 4-Feb-2017.) |
⊢ ((𝐴 × 𝐵) “ 𝐶) = if((𝐴 ∩ 𝐶) = ∅, ∅, 𝐵) | ||
Theorem | xpima1 6182 | Direct image by a Cartesian product (case of empty intersection with the domain). (Contributed by Thierry Arnoux, 16-Dec-2017.) |
⊢ ((𝐴 ∩ 𝐶) = ∅ → ((𝐴 × 𝐵) “ 𝐶) = ∅) | ||
Theorem | xpima2 6183 | Direct image by a Cartesian product (case of nonempty intersection with the domain). (Contributed by Thierry Arnoux, 16-Dec-2017.) |
⊢ ((𝐴 ∩ 𝐶) ≠ ∅ → ((𝐴 × 𝐵) “ 𝐶) = 𝐵) | ||
Theorem | xpimasn 6184 | Direct image of a singleton by a Cartesian product. (Contributed by Thierry Arnoux, 14-Jan-2018.) (Proof shortened by BJ, 6-Apr-2019.) |
⊢ (𝑋 ∈ 𝐴 → ((𝐴 × 𝐵) “ {𝑋}) = 𝐵) | ||
Theorem | sossfld 6185 | 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 6186 | 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 𝑅)) | ||
Theorem | cnvcnv3 6187* | The set of all ordered pairs in a class is the same as the double converse. (Contributed by Mario Carneiro, 16-Aug-2015.) |
⊢ ◡◡𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑅𝑦} | ||
Theorem | dfrel2 6188 | Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 29-Dec-1996.) |
⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅) | ||
Theorem | dfrel4v 6189* | A relation can be expressed as the set of ordered pairs in it. An analogue of dffn5 6950 for relations. (Contributed by Mario Carneiro, 16-Aug-2015.) |
⊢ (Rel 𝑅 ↔ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑅𝑦}) | ||
Theorem | dfrel4 6190* | A relation can be expressed as the set of ordered pairs in it. An analogue of dffn5 6950 for relations. (Contributed by Mario Carneiro, 16-Aug-2015.) (Revised by Thierry Arnoux, 11-May-2017.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑦𝑅 ⇒ ⊢ (Rel 𝑅 ↔ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑅𝑦}) | ||
Theorem | cnvcnv 6191 | The double converse of a class strips out all elements that are not ordered pairs. (Contributed by NM, 8-Dec-2003.) (Proof shortened by BJ, 26-Nov-2021.) |
⊢ ◡◡𝐴 = (𝐴 ∩ (V × V)) | ||
Theorem | cnvcnv2 6192 | The double converse of a class equals its restriction to the universe. (Contributed by NM, 8-Oct-2007.) |
⊢ ◡◡𝐴 = (𝐴 ↾ V) | ||
Theorem | cnvcnvss 6193 | The double converse of a class is a subclass. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 23-Jul-2004.) |
⊢ ◡◡𝐴 ⊆ 𝐴 | ||
Theorem | cnvrescnv 6194 | Two ways to express the corestriction of a class. (Contributed by BJ, 28-Dec-2023.) |
⊢ ◡(◡𝑅 ↾ 𝐵) = (𝑅 ∩ (V × 𝐵)) | ||
Theorem | cnveqb 6195 | Equality theorem for converse. (Contributed by FL, 19-Sep-2011.) |
⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ◡𝐴 = ◡𝐵)) | ||
Theorem | cnveq0 6196 | A relation empty iff its converse is empty. (Contributed by FL, 19-Sep-2011.) |
⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ ◡𝐴 = ∅)) | ||
Theorem | dfrel3 6197 | Alternate definition of relation. (Contributed by NM, 14-May-2008.) |
⊢ (Rel 𝑅 ↔ (𝑅 ↾ V) = 𝑅) | ||
Theorem | elid 6198* | Characterization of the elements of the identity relation. TODO: reorder theorems to move this theorem and dfrel3 6197 after elrid 6045. (Contributed by BJ, 28-Aug-2022.) |
⊢ (𝐴 ∈ I ↔ ∃𝑥 𝐴 = ⟨𝑥, 𝑥⟩) | ||
Theorem | dmresv 6199 | The domain of a universal restriction. (Contributed by NM, 14-May-2008.) |
⊢ dom (𝐴 ↾ V) = dom 𝐴 | ||
Theorem | rnresv 6200 | The range of a universal restriction. (Contributed by NM, 14-May-2008.) |
⊢ ran (𝐴 ↾ V) = ran 𝐴 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |