Home | Metamath
Proof Explorer Theorem List (p. 61 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mptresid 6001* | The restricted identity relation expressed in maps-to notation. (Contributed by FL, 25-Apr-2012.) |
⊢ ( I ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ 𝑥) | ||
Theorem | dmresi 6002 | The domain of a restricted identity function. (Contributed by NM, 27-Aug-2004.) |
⊢ dom ( I ↾ 𝐴) = 𝐴 | ||
Theorem | restidsing 6003 | Restriction of the identity to a singleton. (Contributed by FL, 2-Aug-2009.) (Proof shortened by JJ, 25-Aug-2021.) (Proof shortened by Peter Mazsa, 6-Oct-2022.) |
⊢ ( I ↾ {𝐴}) = ({𝐴} × {𝐴}) | ||
Theorem | iresn0n0 6004 | The identity function restricted to a class 𝐴 is empty iff the class 𝐴 is empty. (Contributed by AV, 30-Jan-2024.) |
⊢ (𝐴 = ∅ ↔ ( I ↾ 𝐴) = ∅) | ||
Theorem | imaeq1 6005 | Equality theorem for image. (Contributed by NM, 14-Aug-1994.) |
⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶)) | ||
Theorem | imaeq2 6006 | Equality theorem for image. (Contributed by NM, 14-Aug-1994.) |
⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵)) | ||
Theorem | imaeq1i 6007 | Equality theorem for image. (Contributed by NM, 21-Dec-2008.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 “ 𝐶) = (𝐵 “ 𝐶) | ||
Theorem | imaeq2i 6008 | Equality theorem for image. (Contributed by NM, 21-Dec-2008.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 “ 𝐴) = (𝐶 “ 𝐵) | ||
Theorem | imaeq1d 6009 | Equality theorem for image. (Contributed by FL, 15-Dec-2006.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶)) | ||
Theorem | imaeq2d 6010 | Equality theorem for image. (Contributed by FL, 15-Dec-2006.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵)) | ||
Theorem | imaeq12d 6011 | Equality theorem for image. (Contributed by Mario Carneiro, 4-Dec-2016.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐷)) | ||
Theorem | dfima2 6012* | Alternate definition of image. Compare definition (d) of [Enderton] p. 44. (Contributed by NM, 19-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑥𝐴𝑦} | ||
Theorem | dfima3 6013* | Alternate definition of image. Compare definition (d) of [Enderton] p. 44. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (𝐴 “ 𝐵) = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐴)} | ||
Theorem | elimag 6014* | Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 20-Jan-2007.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥 ∈ 𝐶 𝑥𝐵𝐴)) | ||
Theorem | elima 6015* | Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 19-Apr-2004.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥 ∈ 𝐶 𝑥𝐵𝐴) | ||
Theorem | elima2 6016* | Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 11-Aug-2004.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥(𝑥 ∈ 𝐶 ∧ 𝑥𝐵𝐴)) | ||
Theorem | elima3 6017* | Membership in an image. Theorem 34 of [Suppes] p. 65. (Contributed by NM, 14-Aug-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ (𝐵 “ 𝐶) ↔ ∃𝑥(𝑥 ∈ 𝐶 ∧ ⟨𝑥, 𝐴⟩ ∈ 𝐵)) | ||
Theorem | nfima 6018 | Bound-variable hypothesis builder for image. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥(𝐴 “ 𝐵) | ||
Theorem | nfimad 6019 | Deduction version of bound-variable hypothesis builder nfima 6018. (Contributed by FL, 15-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝐴) & ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥(𝐴 “ 𝐵)) | ||
Theorem | imadmrn 6020 | The image of the domain of a class is the range of the class. (Contributed by NM, 14-Aug-1994.) |
⊢ (𝐴 “ dom 𝐴) = ran 𝐴 | ||
Theorem | imassrn 6021 | 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 6022* | Image of a function in maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021.) |
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) “ 𝐶) = ran (𝑥 ∈ (𝐴 ∩ 𝐶) ↦ 𝐵) | ||
Theorem | imai 6023 | Image under the identity relation. Theorem 3.16(viii) of [Monk1] p. 38. (Contributed by NM, 30-Apr-1998.) |
⊢ ( I “ 𝐴) = 𝐴 | ||
Theorem | rnresi 6024 | The range of the restricted identity function. (Contributed by NM, 27-Aug-2004.) |
⊢ ran ( I ↾ 𝐴) = 𝐴 | ||
Theorem | resiima 6025 | The image of a restriction of the identity function. (Contributed by FL, 31-Dec-2006.) |
⊢ (𝐵 ⊆ 𝐴 → (( I ↾ 𝐴) “ 𝐵) = 𝐵) | ||
Theorem | ima0 6026 | Image of the empty set. Theorem 3.16(ii) of [Monk1] p. 38. (Contributed by NM, 20-May-1998.) |
⊢ (𝐴 “ ∅) = ∅ | ||
Theorem | 0ima 6027 | Image under the empty relation. (Contributed by FL, 11-Jan-2007.) |
⊢ (∅ “ 𝐴) = ∅ | ||
Theorem | csbima12 6028 | 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 6029 | A class whose image under another is empty is disjoint with the other's domain. (Contributed by FL, 24-Jan-2007.) |
⊢ ((𝐴 “ 𝐵) = ∅ ↔ (dom 𝐴 ∩ 𝐵) = ∅) | ||
Theorem | cnvimass 6030 | A preimage under any class is included in the domain of the class. (Contributed by FL, 29-Jan-2007.) |
⊢ (◡𝐴 “ 𝐵) ⊆ dom 𝐴 | ||
Theorem | cnvimarndm 6031 | 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 6032* | The image of a singleton. (Contributed by NM, 8-May-2005.) |
⊢ (𝐴 ∈ 𝐵 → (𝑅 “ {𝐴}) = {𝑦 ∣ 𝐴𝑅𝑦}) | ||
Theorem | relimasn 6033* | The image of a singleton. (Contributed by NM, 20-May-1998.) |
⊢ (Rel 𝑅 → (𝑅 “ {𝐴}) = {𝑦 ∣ 𝐴𝑅𝑦}) | ||
Theorem | elrelimasn 6034 | Elementhood in the image of a singleton. (Contributed by Mario Carneiro, 3-Nov-2015.) |
⊢ (Rel 𝑅 → (𝐵 ∈ (𝑅 “ {𝐴}) ↔ 𝐴𝑅𝐵)) | ||
Theorem | elimasng1 6035 | Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006.) Revise to use df-br 5105 and to prove elimasn1 6036 from it. (Revised by BJ, 16-Oct-2024.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐶 ∈ (𝐴 “ {𝐵}) ↔ 𝐵𝐴𝐶)) | ||
Theorem | elimasn1 6036 | Membership in an image of a singleton. (Contributed by NM, 15-Mar-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Use df-br 5105 and shorten proof. (Revised by BJ, 16-Oct-2024.) |
⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐶 ∈ (𝐴 “ {𝐵}) ↔ 𝐵𝐴𝐶) | ||
Theorem | elimasng 6037 | Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006.) TODO: replace existing usages by usages of elimasng1 6035, remove, and relabel elimasng1 6035 to "elimasng". |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴)) | ||
Theorem | elimasn 6038 | Membership in an image of a singleton. (Contributed by NM, 15-Mar-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof shortened by BJ, 16-Oct-2024.) TODO: replace existing usages by usages of elimasn1 6036, remove, and relabel elimasn1 6036 to "elimasn". |
⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴) | ||
Theorem | elimasngOLD 6039 | Obsolete version of elimasng 6037 as of 16-Oct-2024. (Contributed by Raph Levien, 21-Oct-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴)) | ||
Theorem | elimasni 6040 | Membership in an image of a singleton. (Contributed by NM, 5-Aug-2010.) |
⊢ (𝐶 ∈ (𝐴 “ {𝐵}) → 𝐵𝐴𝐶) | ||
Theorem | args 6041* | 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 6835 of function value, which is based on the idea in Quine's definition. (Contributed by NM, 8-May-2005.) |
⊢ {𝑥 ∣ ∃𝑦(𝐹 “ {𝑥}) = {𝑦}} = {𝑥 ∣ ∃!𝑦 𝑥𝐹𝑦} | ||
Theorem | elinisegg 6042 | Membership in the inverse image of a singleton. (Contributed by NM, 28-Apr-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Put in closed form and shorten proof. (Revised by BJ, 16-Oct-2024.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐶 ∈ (◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵)) | ||
Theorem | eliniseg 6043 | Membership in the inverse image of a singleton. An application is to express initial segments for an order relation. See 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 | epin 6044 | Any set is equal to its preimage under the converse membership relation. (Contributed by Mario Carneiro, 9-Mar-2013.) Put in closed form. (Revised by BJ, 16-Oct-2024.) |
⊢ (𝐴 ∈ 𝑉 → (◡ E “ {𝐴}) = 𝐴) | ||
Theorem | epini 6045 | Any set is equal to its preimage under the converse membership relation. (Contributed by Mario Carneiro, 9-Mar-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (◡ E “ {𝐴}) = 𝐴 | ||
Theorem | iniseg 6046* | 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 6047 | Nonemptiness of an initial segment in terms of range. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ (𝐴 ∈ ran 𝐹 ↔ (◡𝐹 “ {𝐴}) ≠ ∅) | ||
Theorem | dffr3 6048* | 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 6049* | Alternate definition of set-like relation. (Contributed by Mario Carneiro, 23-Jun-2015.) |
⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 (𝐴 ∩ (◡𝑅 “ {𝑥})) ∈ V) | ||
Theorem | imass1 6050 | Subset theorem for image. (Contributed by NM, 16-Mar-2004.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐴 “ 𝐶) ⊆ (𝐵 “ 𝐶)) | ||
Theorem | imass2 6051 | Subset theorem for image. Exercise 22(a) of [Enderton] p. 53. (Contributed by NM, 22-Mar-1998.) |
⊢ (𝐴 ⊆ 𝐵 → (𝐶 “ 𝐴) ⊆ (𝐶 “ 𝐵)) | ||
Theorem | ndmima 6052 | 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 6053 | A converse is a relation. Theorem 12 of [Suppes] p. 62. (Contributed by NM, 29-Oct-1996.) |
⊢ Rel ◡𝐴 | ||
Theorem | relbrcnvg 6054 | When 𝑅 is a relation, the sethood assumptions on brcnv 5835 can be omitted. (Contributed by Mario Carneiro, 28-Apr-2015.) |
⊢ (Rel 𝑅 → (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴)) | ||
Theorem | eliniseg2 6055 | Eliminate the class existence constraint in eliniseg 6043. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 17-Nov-2015.) |
⊢ (Rel 𝐴 → (𝐶 ∈ (◡𝐴 “ {𝐵}) ↔ 𝐶𝐴𝐵)) | ||
Theorem | relbrcnv 6056 | When 𝑅 is a relation, the sethood assumptions on brcnv 5835 can be omitted. (Contributed by Mario Carneiro, 28-Apr-2015.) |
⊢ Rel 𝑅 ⇒ ⊢ (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴) | ||
Theorem | relco 6057 | A composition is a relation. Exercise 24 of [TakeutiZaring] p. 25. (Contributed by NM, 26-Jan-1997.) |
⊢ Rel (𝐴 ∘ 𝐵) | ||
Theorem | cotrg 6058* | Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr 6061 for the main application. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Generalized from its special instance cotr 6061. (Revised by Richard Penner, 24-Dec-2019.) (Proof shortened by SN, 19-Dec-2024.) Avoid ax-11 2155. (Revised by BTernaryTau, 29-Dec-2024.) |
⊢ ((𝐴 ∘ 𝐵) ⊆ 𝐶 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)) | ||
Theorem | cotrgOLD 6059* | Obsolete version of cotrg 6058 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 6061. (Revised by Richard Penner, 24-Dec-2019.) (Proof shortened by SN, 19-Dec-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∘ 𝐵) ⊆ 𝐶 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)) | ||
Theorem | cotrgOLDOLD 6060* | Obsolete version of cotrg 6058 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 6061. (Revised by Richard Penner, 24-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∘ 𝐵) ⊆ 𝐶 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐵𝑦 ∧ 𝑦𝐴𝑧) → 𝑥𝐶𝑧)) | ||
Theorem | cotr 6061* | Two ways of saying a relation is transitive. Definition of transitivity in [Schechter] p. 51. Special instance of cotrg 6058. (Contributed by NM, 27-Dec-1996.) |
⊢ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) | ||
Theorem | idrefALT 6062* | Alternate proof of idref 7087 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 6063* | 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 2155. (Revised by BTernaryTau, 29-Dec-2024.) |
⊢ (◡𝑅 ⊆ 𝑅 ↔ ∀𝑥∀𝑦(𝑥𝑅𝑦 → 𝑦𝑅𝑥)) | ||
Theorem | cnvsymOLD 6064* | Obsolete proof of cnvsym 6063 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 6065* | Obsolete proof of cnvsym 6063 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 6066* | 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 6067* | Two ways of saying a relation is antisymmetric and reflexive. ∪ ∪ 𝑅 is the field of a relation by relfld 6224. (Contributed by NM, 6-May-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ((𝑅 ∩ ◡𝑅) = ( I ↾ ∪ ∪ 𝑅) ↔ ∀𝑥 ∈ ∪ ∪ 𝑅∀𝑦((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑥) ↔ 𝑥 = 𝑦)) | ||
Theorem | asymref2 6068* | 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 6069* | 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 6070* | Two ways of saying that two elements have an upper bound. (Contributed by Mario Carneiro, 3-Nov-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴(◡𝑅 ∘ 𝑅)𝐵 ↔ ∃𝑧(𝐴𝑅𝑧 ∧ 𝐵𝑅𝑧))) | ||
Theorem | codir 6071* | Two ways of saying a relation is directed. (Contributed by Mario Carneiro, 22-Nov-2013.) |
⊢ ((𝐴 × 𝐵) ⊆ (◡𝑅 ∘ 𝑅) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∃𝑧(𝑥𝑅𝑧 ∧ 𝑦𝑅𝑧)) | ||
Theorem | qfto 6072* | A quantifier-free way of expressing the total order predicate. (Contributed by Mario Carneiro, 22-Nov-2013.) |
⊢ ((𝐴 × 𝐵) ⊆ (𝑅 ∪ ◡𝑅) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥)) | ||
Theorem | xpidtr 6073 | A Cartesian square is a transitive relation. (Contributed by FL, 31-Jul-2009.) |
⊢ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)) ⊆ (𝐴 × 𝐴) | ||
Theorem | trin2 6074 | The intersection of two transitive classes is transitive. (Contributed by FL, 31-Jul-2009.) |
⊢ (((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → ((𝑅 ∩ 𝑆) ∘ (𝑅 ∩ 𝑆)) ⊆ (𝑅 ∩ 𝑆)) | ||
Theorem | poirr2 6075 | A partial order is irreflexive. (Contributed by Mario Carneiro, 2-Nov-2015.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ (𝑅 Po 𝐴 → (𝑅 ∩ ( I ↾ 𝐴)) = ∅) | ||
Theorem | trinxp 6076 | 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 6077 | A strict order relation is irreflexive. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.) |
⊢ 𝑅 Or 𝑆 & ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ¬ 𝐴𝑅𝐴 | ||
Theorem | sotri 6078 | A strict order relation is a transitive relation. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.) |
⊢ 𝑅 Or 𝑆 & ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) | ||
Theorem | son2lpi 6079 | 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 6080 | A transitivity relation. (Read 𝐴 ≤ 𝐵 and 𝐵 < 𝐶 implies 𝐴 < 𝐶.) (Contributed by Mario Carneiro, 10-May-2013.) |
⊢ 𝑅 Or 𝑆 & ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ ¬ 𝐵𝑅𝐴 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) | ||
Theorem | sotri3 6081 | A transitivity relation. (Read 𝐴 < 𝐵 and 𝐵 ≤ 𝐶 implies 𝐴 < 𝐶.) (Contributed by Mario Carneiro, 10-May-2013.) |
⊢ 𝑅 Or 𝑆 & ⊢ 𝑅 ⊆ (𝑆 × 𝑆) ⇒ ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐴𝑅𝐵 ∧ ¬ 𝐶𝑅𝐵) → 𝐴𝑅𝐶) | ||
Theorem | poleloe 6082 | Express "less than or equals" for general strict orders. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴(𝑅 ∪ I )𝐵 ↔ (𝐴𝑅𝐵 ∨ 𝐴 = 𝐵))) | ||
Theorem | poltletr 6083 | Transitive law for general strict orders. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝑅 Po 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑅𝐵 ∧ 𝐵(𝑅 ∪ I )𝐶) → 𝐴𝑅𝐶)) | ||
Theorem | somin1 6084 | Property of a minimum in a strict order. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝑅 Or 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → if(𝐴𝑅𝐵, 𝐴, 𝐵)(𝑅 ∪ I )𝐴) | ||
Theorem | somincom 6085 | Commutativity of minimum in a total order. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝑅 Or 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → if(𝐴𝑅𝐵, 𝐴, 𝐵) = if(𝐵𝑅𝐴, 𝐵, 𝐴)) | ||
Theorem | somin2 6086 | Property of a minimum in a strict order. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝑅 Or 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → if(𝐴𝑅𝐵, 𝐴, 𝐵)(𝑅 ∪ I )𝐵) | ||
Theorem | soltmin 6087 | Being less than a minimum, for a general total order. (Contributed by Stefan O'Rear, 17-Jan-2015.) |
⊢ ((𝑅 Or 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑅if(𝐵𝑅𝐶, 𝐵, 𝐶) ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑅𝐶))) | ||
Theorem | cnvopab 6088* | 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 6089* | The converse of a mapping function. (Contributed by Thierry Arnoux, 16-Jan-2017.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐷))) ⇒ ⊢ (𝜑 → ◡(𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | cnv0 6090 | The converse of the empty set. (Contributed by NM, 6-Apr-1998.) Remove dependency on ax-sep 5255, ax-nul 5262, ax-pr 5383. (Revised by KP, 25-Oct-2021.) |
⊢ ◡∅ = ∅ | ||
Theorem | cnvi 6091 | 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 6092 | 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 6093 | Distributive law for converse over class difference. (Contributed by Mario Carneiro, 26-Jun-2014.) |
⊢ ◡(𝐴 ∖ 𝐵) = (◡𝐴 ∖ ◡𝐵) | ||
Theorem | cnvin 6094 | 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 6095 | Distributive law for range over union. Theorem 8 of [Suppes] p. 60. (Contributed by NM, 24-Mar-1998.) |
⊢ ran (𝐴 ∪ 𝐵) = (ran 𝐴 ∪ ran 𝐵) | ||
Theorem | rnin 6096 | 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 6097 | The range of an indexed union. (Contributed by Mario Carneiro, 29-May-2015.) |
⊢ ran ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ran 𝐵 | ||
Theorem | rnuni 6098* | 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 6099 | Distributive law for image over union. Theorem 35 of [Suppes] p. 65. (Contributed by NM, 30-Sep-2002.) |
⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶)) | ||
Theorem | imaundir 6100 | The image of a union. (Contributed by Jeff Hoffman, 17-Feb-2008.) |
⊢ ((𝐴 ∪ 𝐵) “ 𝐶) = ((𝐴 “ 𝐶) ∪ (𝐵 “ 𝐶)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |