Home | Metamath
Proof Explorer Theorem List (p. 56 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 | cnvcnv3 5501* | 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 5502 | Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 29-Dec-1996.) |
⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅) | ||
Theorem | dfrel4v 5503* | A relation can be expressed as the set of ordered pairs in it. An analogue of dffn5 6151 for relations. (Contributed by Mario Carneiro, 16-Aug-2015.) |
⊢ (Rel 𝑅 ↔ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦}) | ||
Theorem | dfrel4 5504* | A relation can be expressed as the set of ordered pairs in it. An analogue of dffn5 6151 for relations. (Contributed by Mario Carneiro, 16-Aug-2015.) (Revised by Thierry Arnoux, 11-May-2017.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑦𝑅 ⇒ ⊢ (Rel 𝑅 ↔ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦}) | ||
Theorem | cnvcnv 5505 | The double converse of a class strips out all elements that are not ordered pairs. (Contributed by NM, 8-Dec-2003.) |
⊢ ◡◡𝐴 = (𝐴 ∩ (V × V)) | ||
Theorem | cnvcnv2 5506 | The double converse of a class equals its restriction to the universe. (Contributed by NM, 8-Oct-2007.) |
⊢ ◡◡𝐴 = (𝐴 ↾ V) | ||
Theorem | cnvcnvss 5507 | The double converse of a class is a subclass. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 23-Jul-2004.) |
⊢ ◡◡𝐴 ⊆ 𝐴 | ||
Theorem | cnveqb 5508 | Equality theorem for converse. (Contributed by FL, 19-Sep-2011.) |
⊢ ((Rel 𝐴 ∧ Rel 𝐵) → (𝐴 = 𝐵 ↔ ◡𝐴 = ◡𝐵)) | ||
Theorem | cnveq0 5509 | A relation empty iff its converse is empty. (Contributed by FL, 19-Sep-2011.) |
⊢ (Rel 𝐴 → (𝐴 = ∅ ↔ ◡𝐴 = ∅)) | ||
Theorem | dfrel3 5510 | Alternate definition of relation. (Contributed by NM, 14-May-2008.) |
⊢ (Rel 𝑅 ↔ (𝑅 ↾ V) = 𝑅) | ||
Theorem | dmresv 5511 | The domain of a universal restriction. (Contributed by NM, 14-May-2008.) |
⊢ dom (𝐴 ↾ V) = dom 𝐴 | ||
Theorem | rnresv 5512 | The range of a universal restriction. (Contributed by NM, 14-May-2008.) |
⊢ ran (𝐴 ↾ V) = ran 𝐴 | ||
Theorem | dfrn4 5513 | Range defined in terms of image. (Contributed by NM, 14-May-2008.) |
⊢ ran 𝐴 = (𝐴 “ V) | ||
Theorem | csbrn 5514 | Distribute proper substitution through the range of a class. (Contributed by Alan Sare, 10-Nov-2012.) |
⊢ ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵 | ||
Theorem | rescnvcnv 5515 | The restriction of the double converse of a class. (Contributed by NM, 8-Apr-2007.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (◡◡𝐴 ↾ 𝐵) = (𝐴 ↾ 𝐵) | ||
Theorem | cnvcnvres 5516 | The double converse of the restriction of a class. (Contributed by NM, 3-Jun-2007.) |
⊢ ◡◡(𝐴 ↾ 𝐵) = (◡◡𝐴 ↾ 𝐵) | ||
Theorem | imacnvcnv 5517 | The image of the double converse of a class. (Contributed by NM, 8-Apr-2007.) |
⊢ (◡◡𝐴 “ 𝐵) = (𝐴 “ 𝐵) | ||
Theorem | dmsnn0 5518 | The domain of a singleton is nonzero iff the singleton argument is an ordered pair. (Contributed by NM, 14-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (𝐴 ∈ (V × V) ↔ dom {𝐴} ≠ ∅) | ||
Theorem | rnsnn0 5519 | The range of a singleton is nonzero iff the singleton argument is an ordered pair. (Contributed by NM, 14-Dec-2008.) |
⊢ (𝐴 ∈ (V × V) ↔ ran {𝐴} ≠ ∅) | ||
Theorem | dmsn0 5520 | The domain of the singleton of the empty set is empty. (Contributed by NM, 30-Jan-2004.) |
⊢ dom {∅} = ∅ | ||
Theorem | cnvsn0 5521 | The converse of the singleton of the empty set is empty. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ ◡{∅} = ∅ | ||
Theorem | dmsn0el 5522 | The domain of a singleton is empty if the singleton's argument contains the empty set. (Contributed by NM, 15-Dec-2008.) |
⊢ (∅ ∈ 𝐴 → dom {𝐴} = ∅) | ||
Theorem | relsn2 5523 | A singleton is a relation iff it has a nonempty domain. (Contributed by NM, 25-Sep-2013.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (Rel {𝐴} ↔ dom {𝐴} ≠ ∅) | ||
Theorem | dmsnopg 5524 | The domain of a singleton of an ordered pair is the singleton of the first member. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ (𝐵 ∈ 𝑉 → dom {〈𝐴, 𝐵〉} = {𝐴}) | ||
Theorem | dmsnopss 5525 | The domain of a singleton of an ordered pair is a subset of the singleton of the first member (with no sethood assumptions on 𝐵). (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ dom {〈𝐴, 𝐵〉} ⊆ {𝐴} | ||
Theorem | dmpropg 5526 | The domain of an unordered pair of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) → dom {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {𝐴, 𝐶}) | ||
Theorem | dmsnop 5527 | The domain of a singleton of an ordered pair is the singleton of the first member. (Contributed by NM, 30-Jan-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐵 ∈ V ⇒ ⊢ dom {〈𝐴, 𝐵〉} = {𝐴} | ||
Theorem | dmprop 5528 | The domain of an unordered pair of ordered pairs. (Contributed by NM, 13-Sep-2011.) |
⊢ 𝐵 ∈ V & ⊢ 𝐷 ∈ V ⇒ ⊢ dom {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {𝐴, 𝐶} | ||
Theorem | dmtpop 5529 | The domain of an unordered triple of ordered pairs. (Contributed by NM, 14-Sep-2011.) |
⊢ 𝐵 ∈ V & ⊢ 𝐷 ∈ V & ⊢ 𝐹 ∈ V ⇒ ⊢ dom {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉, 〈𝐸, 𝐹〉} = {𝐴, 𝐶, 𝐸} | ||
Theorem | cnvcnvsn 5530 | Double converse of a singleton of an ordered pair. (Unlike cnvsn 5536, this does not need any sethood assumptions on 𝐴 and 𝐵.) (Contributed by Mario Carneiro, 26-Apr-2015.) |
⊢ ◡◡{〈𝐴, 𝐵〉} = ◡{〈𝐵, 𝐴〉} | ||
Theorem | dmsnsnsn 5531 | The domain of the singleton of the singleton of a singleton. (Contributed by NM, 15-Sep-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ dom {{{𝐴}}} = {𝐴} | ||
Theorem | rnsnopg 5532 | The range of a singleton of an ordered pair is the singleton of the second member. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ (𝐴 ∈ 𝑉 → ran {〈𝐴, 𝐵〉} = {𝐵}) | ||
Theorem | rnpropg 5533 | The range of a pair of ordered pairs is the pair of second members. (Contributed by Thierry Arnoux, 3-Jan-2017.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ran {〈𝐴, 𝐶〉, 〈𝐵, 𝐷〉} = {𝐶, 𝐷}) | ||
Theorem | rnsnop 5534 | The range of a singleton of an ordered pair is the singleton of the second member. (Contributed by NM, 24-Jul-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ran {〈𝐴, 𝐵〉} = {𝐵} | ||
Theorem | op1sta 5535 | Extract the first member of an ordered pair. (See op2nda 5538 to extract the second member, op1stb 4867 for an alternate version, and op1st 7067 for the preferred version.) (Contributed by Raph Levien, 4-Dec-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∪ dom {〈𝐴, 𝐵〉} = 𝐴 | ||
Theorem | cnvsn 5536 | Converse of a singleton of an ordered pair. (Contributed by NM, 11-May-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ◡{〈𝐴, 𝐵〉} = {〈𝐵, 𝐴〉} | ||
Theorem | op2ndb 5537 | Extract the second member of an ordered pair. Theorem 5.12(ii) of [Monk1] p. 52. (See op1stb 4867 to extract the first member, op2nda 5538 for an alternate version, and op2nd 7068 for the preferred version.) (Contributed by NM, 25-Nov-2003.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∩ ∩ ∩ ◡{〈𝐴, 𝐵〉} = 𝐵 | ||
Theorem | op2nda 5538 | Extract the second member of an ordered pair. (See op1sta 5535 to extract the first member, op2ndb 5537 for an alternate version, and op2nd 7068 for the preferred version.) (Contributed by NM, 17-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ∪ ran {〈𝐴, 𝐵〉} = 𝐵 | ||
Theorem | cnvsng 5539 | Converse of a singleton of an ordered pair. (Contributed by NM, 23-Jan-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ◡{〈𝐴, 𝐵〉} = {〈𝐵, 𝐴〉}) | ||
Theorem | opswap 5540 | Swap the members of an ordered pair. (Contributed by NM, 14-Dec-2008.) (Revised by Mario Carneiro, 30-Aug-2015.) |
⊢ ∪ ◡{〈𝐴, 𝐵〉} = 〈𝐵, 𝐴〉 | ||
Theorem | cnvresima 5541 | An image under the converse of a restriction. (Contributed by Jeff Hankins, 12-Jul-2009.) |
⊢ (◡(𝐹 ↾ 𝐴) “ 𝐵) = ((◡𝐹 “ 𝐵) ∩ 𝐴) | ||
Theorem | resdm2 5542 | A class restricted to its domain equals its double converse. (Contributed by NM, 8-Apr-2007.) |
⊢ (𝐴 ↾ dom 𝐴) = ◡◡𝐴 | ||
Theorem | resdmres 5543 | Restriction to the domain of a restriction. (Contributed by NM, 8-Apr-2007.) |
⊢ (𝐴 ↾ dom (𝐴 ↾ 𝐵)) = (𝐴 ↾ 𝐵) | ||
Theorem | imadmres 5544 | The image of the domain of a restriction. (Contributed by NM, 8-Apr-2007.) |
⊢ (𝐴 “ dom (𝐴 ↾ 𝐵)) = (𝐴 “ 𝐵) | ||
Theorem | mptpreima 5545* | The preimage of a function in maps-to notation. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (◡𝐹 “ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶} | ||
Theorem | mptiniseg 5546* | Converse singleton image of a function defined by maps-to. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ (𝐶 ∈ 𝑉 → (◡𝐹 “ {𝐶}) = {𝑥 ∈ 𝐴 ∣ 𝐵 = 𝐶}) | ||
Theorem | dmmpt 5547 | The domain of the mapping operation in general. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 22-Mar-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ dom 𝐹 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} | ||
Theorem | dmmptss 5548* | The domain of a mapping is a subset of its base class. (Contributed by Scott Fenton, 17-Jun-2013.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) ⇒ ⊢ dom 𝐹 ⊆ 𝐴 | ||
Theorem | dmmptg 5549* | The domain of the mapping operation is the stated domain, if the function value is always a set. (Contributed by Mario Carneiro, 9-Feb-2013.) (Revised by Mario Carneiro, 14-Sep-2013.) |
⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴) | ||
Theorem | relco 5550 | A composition is a relation. Exercise 24 of [TakeutiZaring] p. 25. (Contributed by NM, 26-Jan-1997.) |
⊢ Rel (𝐴 ∘ 𝐵) | ||
Theorem | dfco2 5551* | Alternate definition of a class composition, using only one bound variable. (Contributed by NM, 19-Dec-2008.) |
⊢ (𝐴 ∘ 𝐵) = ∪ 𝑥 ∈ V ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥})) | ||
Theorem | dfco2a 5552* | Generalization of dfco2 5551, where 𝐶 can have any value between dom 𝐴 ∩ ran 𝐵 and V. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ((dom 𝐴 ∩ ran 𝐵) ⊆ 𝐶 → (𝐴 ∘ 𝐵) = ∪ 𝑥 ∈ 𝐶 ((◡𝐵 “ {𝑥}) × (𝐴 “ {𝑥}))) | ||
Theorem | coundi 5553 | Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (𝐴 ∘ (𝐵 ∪ 𝐶)) = ((𝐴 ∘ 𝐵) ∪ (𝐴 ∘ 𝐶)) | ||
Theorem | coundir 5554 | Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ ((𝐴 ∪ 𝐵) ∘ 𝐶) = ((𝐴 ∘ 𝐶) ∪ (𝐵 ∘ 𝐶)) | ||
Theorem | cores 5555 | Restricted first member of a class composition. (Contributed by NM, 12-Oct-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
⊢ (ran 𝐵 ⊆ 𝐶 → ((𝐴 ↾ 𝐶) ∘ 𝐵) = (𝐴 ∘ 𝐵)) | ||
Theorem | resco 5556 | Associative law for the restriction of a composition. (Contributed by NM, 12-Dec-2006.) |
⊢ ((𝐴 ∘ 𝐵) ↾ 𝐶) = (𝐴 ∘ (𝐵 ↾ 𝐶)) | ||
Theorem | imaco 5557 | Image of the composition of two classes. (Contributed by Jason Orendorff, 12-Dec-2006.) |
⊢ ((𝐴 ∘ 𝐵) “ 𝐶) = (𝐴 “ (𝐵 “ 𝐶)) | ||
Theorem | rnco 5558 | The range of the composition of two classes. (Contributed by NM, 12-Dec-2006.) |
⊢ ran (𝐴 ∘ 𝐵) = ran (𝐴 ↾ ran 𝐵) | ||
Theorem | rnco2 5559 | The range of the composition of two classes. (Contributed by NM, 27-Mar-2008.) |
⊢ ran (𝐴 ∘ 𝐵) = (𝐴 “ ran 𝐵) | ||
Theorem | dmco 5560 | The domain of a composition. Exercise 27 of [Enderton] p. 53. (Contributed by NM, 4-Feb-2004.) |
⊢ dom (𝐴 ∘ 𝐵) = (◡𝐵 “ dom 𝐴) | ||
Theorem | coeq0 5561 | A composition of two relations is empty iff there is no overlap between the range of the second and the domain of the first. Useful in combination with coundi 5553 and coundir 5554 to prune meaningless terms in the result. (Contributed by Stefan O'Rear, 8-Oct-2014.) |
⊢ ((𝐴 ∘ 𝐵) = ∅ ↔ (dom 𝐴 ∩ ran 𝐵) = ∅) | ||
Theorem | coiun 5562* | Composition with an indexed union. (Contributed by NM, 21-Dec-2008.) |
⊢ (𝐴 ∘ ∪ 𝑥 ∈ 𝐶 𝐵) = ∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵) | ||
Theorem | cocnvcnv1 5563 | A composition is not affected by a double converse of its first argument. (Contributed by NM, 8-Oct-2007.) |
⊢ (◡◡𝐴 ∘ 𝐵) = (𝐴 ∘ 𝐵) | ||
Theorem | cocnvcnv2 5564 | A composition is not affected by a double converse of its second argument. (Contributed by NM, 8-Oct-2007.) |
⊢ (𝐴 ∘ ◡◡𝐵) = (𝐴 ∘ 𝐵) | ||
Theorem | cores2 5565 | Absorption of a reverse (preimage) restriction of the second member of a class composition. (Contributed by NM, 11-Dec-2006.) |
⊢ (dom 𝐴 ⊆ 𝐶 → (𝐴 ∘ ◡(◡𝐵 ↾ 𝐶)) = (𝐴 ∘ 𝐵)) | ||
Theorem | co02 5566 | Composition with the empty set. Theorem 20 of [Suppes] p. 63. (Contributed by NM, 24-Apr-2004.) |
⊢ (𝐴 ∘ ∅) = ∅ | ||
Theorem | co01 5567 | Composition with the empty set. (Contributed by NM, 24-Apr-2004.) |
⊢ (∅ ∘ 𝐴) = ∅ | ||
Theorem | coi1 5568 | Composition with the identity relation. Part of Theorem 3.7(i) of [Monk1] p. 36. (Contributed by NM, 22-Apr-2004.) |
⊢ (Rel 𝐴 → (𝐴 ∘ I ) = 𝐴) | ||
Theorem | coi2 5569 | Composition with the identity relation. Part of Theorem 3.7(i) of [Monk1] p. 36. (Contributed by NM, 22-Apr-2004.) |
⊢ (Rel 𝐴 → ( I ∘ 𝐴) = 𝐴) | ||
Theorem | coires1 5570 | Composition with a restricted identity relation. (Contributed by FL, 19-Jun-2011.) (Revised by Stefan O'Rear, 7-Mar-2015.) |
⊢ (𝐴 ∘ ( I ↾ 𝐵)) = (𝐴 ↾ 𝐵) | ||
Theorem | coass 5571 | Associative law for class composition. Theorem 27 of [Suppes] p. 64. Also Exercise 21 of [Enderton] p. 53. Interestingly, this law holds for any classes whatsoever, not just functions or even relations. (Contributed by NM, 27-Jan-1997.) |
⊢ ((𝐴 ∘ 𝐵) ∘ 𝐶) = (𝐴 ∘ (𝐵 ∘ 𝐶)) | ||
Theorem | relcnvtr 5572 | A relation is transitive iff its converse is transitive. (Contributed by FL, 19-Sep-2011.) |
⊢ (Rel 𝑅 → ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ (◡𝑅 ∘ ◡𝑅) ⊆ ◡𝑅)) | ||
Theorem | relssdmrn 5573 | A relation is included in the Cartesian product of its domain and range. Exercise 4.12(t) of [Mendelson] p. 235. (Contributed by NM, 3-Aug-1994.) |
⊢ (Rel 𝐴 → 𝐴 ⊆ (dom 𝐴 × ran 𝐴)) | ||
Theorem | cnvssrndm 5574 | The converse is a subset of the cartesian product of range and domain. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ ◡𝐴 ⊆ (ran 𝐴 × dom 𝐴) | ||
Theorem | cossxp 5575 | Composition as a subset of the Cartesian product of factors. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ (𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴) | ||
Theorem | relrelss 5576 | Two ways to describe the structure of a two-place operation. (Contributed by NM, 17-Dec-2008.) |
⊢ ((Rel 𝐴 ∧ Rel dom 𝐴) ↔ 𝐴 ⊆ ((V × V) × V)) | ||
Theorem | unielrel 5577 | The membership relation for a relation is inherited by class union. (Contributed by NM, 17-Sep-2006.) |
⊢ ((Rel 𝑅 ∧ 𝐴 ∈ 𝑅) → ∪ 𝐴 ∈ ∪ 𝑅) | ||
Theorem | relfld 5578 | The double union of a relation is its field. (Contributed by NM, 17-Sep-2006.) |
⊢ (Rel 𝑅 → ∪ ∪ 𝑅 = (dom 𝑅 ∪ ran 𝑅)) | ||
Theorem | relresfld 5579 | Restriction of a relation to its field. (Contributed by FL, 15-Apr-2012.) |
⊢ (Rel 𝑅 → (𝑅 ↾ ∪ ∪ 𝑅) = 𝑅) | ||
Theorem | relcoi2 5580 | Composition with the identity relation restricted to a relation's field. (Contributed by FL, 2-May-2011.) |
⊢ (Rel 𝑅 → (( I ↾ ∪ ∪ 𝑅) ∘ 𝑅) = 𝑅) | ||
Theorem | relcoi1 5581 | Composition with the identity relation restricted to a relation's field. (Contributed by FL, 8-May-2011.) (Proof shortened by OpenAI, 3-Jul-2020.) |
⊢ (Rel 𝑅 → (𝑅 ∘ ( I ↾ ∪ ∪ 𝑅)) = 𝑅) | ||
Theorem | unidmrn 5582 | The double union of the converse of a class is its field. (Contributed by NM, 4-Jun-2008.) |
⊢ ∪ ∪ ◡𝐴 = (dom 𝐴 ∪ ran 𝐴) | ||
Theorem | relcnvfld 5583 | if 𝑅 is a relation, its double union equals the double union of its converse. (Contributed by FL, 5-Jan-2009.) |
⊢ (Rel 𝑅 → ∪ ∪ 𝑅 = ∪ ∪ ◡𝑅) | ||
Theorem | dfdm2 5584 | Alternate definition of domain df-dm 5048 that doesn't require dummy variables. (Contributed by NM, 2-Aug-2010.) |
⊢ dom 𝐴 = ∪ ∪ (◡𝐴 ∘ 𝐴) | ||
Theorem | unixp 5585 | The double class union of a nonempty Cartesian product is the union of it members. (Contributed by NM, 17-Sep-2006.) |
⊢ ((𝐴 × 𝐵) ≠ ∅ → ∪ ∪ (𝐴 × 𝐵) = (𝐴 ∪ 𝐵)) | ||
Theorem | unixp0 5586 | A Cartesian product is empty iff its union is empty. (Contributed by NM, 20-Sep-2006.) |
⊢ ((𝐴 × 𝐵) = ∅ ↔ ∪ (𝐴 × 𝐵) = ∅) | ||
Theorem | unixpid 5587 | Field of a square Cartesian product. (Contributed by FL, 10-Oct-2009.) |
⊢ ∪ ∪ (𝐴 × 𝐴) = 𝐴 | ||
Theorem | ressn 5588 | Restriction of a class to a singleton. (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ (𝐴 ↾ {𝐵}) = ({𝐵} × (𝐴 “ {𝐵})) | ||
Theorem | cnviin 5589* | The converse of an intersection is the intersection of the converse. (Contributed by FL, 15-Oct-2012.) |
⊢ (𝐴 ≠ ∅ → ◡∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 ◡𝐵) | ||
Theorem | cnvpo 5590 | The converse of a partial order relation is a partial order relation. (Contributed by NM, 15-Jun-2005.) |
⊢ (𝑅 Po 𝐴 ↔ ◡𝑅 Po 𝐴) | ||
Theorem | cnvso 5591 | The converse of a strict order relation is a strict order relation. (Contributed by NM, 15-Jun-2005.) |
⊢ (𝑅 Or 𝐴 ↔ ◡𝑅 Or 𝐴) | ||
Theorem | xpco 5592 | Composition of two Cartesian products. (Contributed by Thierry Arnoux, 17-Nov-2017.) |
⊢ (𝐵 ≠ ∅ → ((𝐵 × 𝐶) ∘ (𝐴 × 𝐵)) = (𝐴 × 𝐶)) | ||
Theorem | xpcoid 5593 | Composition of two square Cartesian products. (Contributed by Thierry Arnoux, 14-Jan-2018.) |
⊢ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)) = (𝐴 × 𝐴) | ||
Theorem | elsnxp 5594* | Elementhood to a cartesian product with a singleton. (Contributed by Thierry Arnoux, 10-Apr-2020.) (Proof shortened by JJ, 14-Jul-2021.) |
⊢ (𝑋 ∈ 𝑉 → (𝑍 ∈ ({𝑋} × 𝐴) ↔ ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉)) | ||
Theorem | elsnxpOLD 5595* | Obsolete proof of elsnxp 5594 as of 14-Jul-2021. (Contributed by Thierry Arnoux, 10-Apr-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑋 ∈ 𝑉 → (𝑍 ∈ ({𝑋} × 𝐴) ↔ ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉)) | ||
Syntax | cpred 5596 | The predecessors symbol. |
class Pred(𝑅, 𝐴, 𝑋) | ||
Definition | df-pred 5597 | Define the predecessor class of a relationship. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 5610) . (Contributed by Scott Fenton, 29-Jan-2011.) |
⊢ Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋})) | ||
Theorem | predeq123 5598 | Equality theorem for the predecessor class. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌) → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑆, 𝐵, 𝑌)) | ||
Theorem | predeq1 5599 | Equality theorem for the predecessor class. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝑅 = 𝑆 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑆, 𝐴, 𝑋)) | ||
Theorem | predeq2 5600 | Equality theorem for the predecessor class. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝐴 = 𝐵 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐵, 𝑋)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |