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