HomeHome Intuitionistic Logic Explorer
Theorem List (p. 48 of 94)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 4701-4800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremssxp2 4701* Cross product subset cancellation. (Contributed by Jim Kingdon, 14-Dec-2018.)
 C  C  X.  C_  C  X.  C_
 
Theoremxp11m 4702* The cross product of inhabited classes is one-to-one. (Contributed by Jim Kingdon, 13-Dec-2018.)

 X.  C  X.  D  C  D
 
Theoremxpcanm 4703* Cancellation law for cross-product. (Contributed by Jim Kingdon, 14-Dec-2018.)
 C  C  X.  C  X.
 
Theoremxpcan2m 4704* Cancellation law for cross-product. (Contributed by Jim Kingdon, 14-Dec-2018.)
 C  X.  C  X.  C
 
Theoremxpexr2m 4705* If a nonempty cross product is a set, so are both of its components. (Contributed by Jim Kingdon, 14-Dec-2018.)

 X.  C  X.  _V  _V
 
Theoremssrnres 4706 Subset of the range of a restriction. (Contributed by NM, 16-Jan-2006.)
 C_  ran  C  |`  ran  C  i^i  X.
 
Theoremrninxp 4707* Range of the intersection with a cross product. (Contributed by NM, 17-Jan-2006.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
 ran  C  i^i  X.  C
 
Theoremdminxp 4708* Domain of the intersection with a cross product. (Contributed by NM, 17-Jan-2006.)
 dom  C  i^i  X.  C
 
Theoremimainrect 4709 Image of a relation restricted to a rectangular region. (Contributed by Stefan O'Rear, 19-Feb-2015.)
 G  i^i  X.  " Y  G
 " Y  i^i  i^i
 
Theoremxpima1 4710 The image by a cross product. (Contributed by Thierry Arnoux, 16-Dec-2017.)
 i^i  C  (/)  X. 
 " C  (/)
 
Theoremxpima2m 4711* The image by a cross product. (Contributed by Thierry Arnoux, 16-Dec-2017.)
 i^i  C 
 X.  " C
 
Theoremxpimasn 4712 The image of a singleton by a cross product. (Contributed by Thierry Arnoux, 14-Jan-2018.)
 X  X.  " { X }
 
Theoremcnvcnv3 4713* The set of all ordered pairs in a class is the same as the double converse. (Contributed by Mario Carneiro, 16-Aug-2015.)
 `' `' R  { <. ,  >.  |  R }
 
Theoremdfrel2 4714 Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 29-Dec-1996.)
 Rel  R  `' `' R  R
 
Theoremdfrel4v 4715* A relation can be expressed as the set of ordered pairs in it. (Contributed by Mario Carneiro, 16-Aug-2015.)
 Rel  R  R  {
 <. ,  >.  |  R }
 
Theoremcnvcnv 4716 The double converse of a class strips out all elements that are not ordered pairs. (Contributed by NM, 8-Dec-2003.)
 `' `'  i^i  _V  X.  _V
 
Theoremcnvcnv2 4717 The double converse of a class equals its restriction to the universe. (Contributed by NM, 8-Oct-2007.)
 `' `'  |`  _V
 
Theoremcnvcnvss 4718 The double converse of a class is a subclass. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 23-Jul-2004.)
 `' `'  C_
 
Theoremcnveqb 4719 Equality theorem for converse. (Contributed by FL, 19-Sep-2011.)
 Rel 
 Rel  `'  `'
 
Theoremcnveq0 4720 A relation empty iff its converse is empty. (Contributed by FL, 19-Sep-2011.)
 Rel  (/)  `'  (/)
 
Theoremdfrel3 4721 Alternate definition of relation. (Contributed by NM, 14-May-2008.)
 Rel  R  R  |`  _V  R
 
Theoremdmresv 4722 The domain of a universal restriction. (Contributed by NM, 14-May-2008.)

 dom  |`  _V  dom
 
Theoremrnresv 4723 The range of a universal restriction. (Contributed by NM, 14-May-2008.)

 ran  |`  _V  ran
 
Theoremdfrn4 4724 Range defined in terms of image. (Contributed by NM, 14-May-2008.)

 ran  " _V
 
Theoremcsbrng 4725 Distribute proper substitution through the range of a class. (Contributed by Alan Sare, 10-Nov-2012.)
 V  [_  ]_
 ran  ran  [_  ]_
 
Theoremrescnvcnv 4726 The restriction of the double converse of a class. (Contributed by NM, 8-Apr-2007.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
 `' `'  |`  |`
 
Theoremcnvcnvres 4727 The double converse of the restriction of a class. (Contributed by NM, 3-Jun-2007.)
 `' `'  |`  `' `'  |`
 
Theoremimacnvcnv 4728 The image of the double converse of a class. (Contributed by NM, 8-Apr-2007.)
 `' `' "  "
 
Theoremdmsnm 4729* The domain of a singleton is inhabited iff the singleton argument is an ordered pair. (Contributed by Jim Kingdon, 15-Dec-2018.)
 _V  X.  _V  dom  { }
 
Theoremrnsnm 4730* The range of a singleton is inhabited iff the singleton argument is an ordered pair. (Contributed by Jim Kingdon, 15-Dec-2018.)
 _V  X.  _V  ran  { }
 
Theoremdmsn0 4731 The domain of the singleton of the empty set is empty. (Contributed by NM, 30-Jan-2004.)

 dom  { (/) }  (/)
 
Theoremcnvsn0 4732 The converse of the singleton of the empty set is empty. (Contributed by Mario Carneiro, 30-Aug-2015.)
 `' { (/) }  (/)
 
Theoremdmsn0el 4733 The domain of a singleton is empty if the singleton's argument contains the empty set. (Contributed by NM, 15-Dec-2008.)
 (/)  dom  { }  (/)
 
Theoremrelsn2m 4734* A singleton is a relation iff it has an inhabited domain. (Contributed by Jim Kingdon, 16-Dec-2018.)
 _V   =>     Rel  { }  dom  { }
 
Theoremdmsnopg 4735 The domain of a singleton of an ordered pair is the singleton of the first member. (Contributed by Mario Carneiro, 26-Apr-2015.)
 V  dom  { <. ,  >. }  { }
 
Theoremdmpropg 4736 The domain of an unordered pair of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.)
 V  D  W  dom  { <. ,  >. ,  <. C ,  D >. }  { ,  C }
 
Theoremdmsnop 4737 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  { <. ,  >. }  { }
 
Theoremdmprop 4738 The domain of an unordered pair of ordered pairs. (Contributed by NM, 13-Sep-2011.)
 _V   &     D  _V   =>     dom  { <. ,  >. ,  <. C ,  D >. }  { ,  C }
 
Theoremdmtpop 4739 The domain of an unordered triple of ordered pairs. (Contributed by NM, 14-Sep-2011.)
 _V   &     D  _V   &     F  _V   =>    
 dom  { <. ,  >. ,  <. C ,  D >. ,  <. E ,  F >. }  { ,  C ,  E }
 
Theoremcnvcnvsn 4740 Double converse of a singleton of an ordered pair. (Unlike cnvsn 4746, this does not need any sethood assumptions on and .) (Contributed by Mario Carneiro, 26-Apr-2015.)
 `' `' { <. ,  >. }  `' { <. ,  >. }
 
Theoremdmsnsnsng 4741 The domain of the singleton of the singleton of a singleton. (Contributed by Jim Kingdon, 16-Dec-2018.)
 _V  dom  { { { } } }  { }
 
Theoremrnsnopg 4742 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.)
 V  ran  { <. ,  >. }  { }
 
Theoremrnpropg 4743 The range of a pair of ordered pairs is the pair of second members. (Contributed by Thierry Arnoux, 3-Jan-2017.)
 V  W  ran  { <. ,  C >. ,  <. ,  D >. }  { C ,  D }
 
Theoremrnsnop 4744 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  { <. ,  >. }  { }
 
Theoremop1sta 4745 Extract the first member of an ordered pair. (See op2nda 4748 to extract the second member and op1stb 4175 for an alternate version.) (Contributed by Raph Levien, 4-Dec-2003.)
 _V   &     _V   =>     U. dom  { <. ,  >. }
 
Theoremcnvsn 4746 Converse of a singleton of an ordered pair. (Contributed by NM, 11-May-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
 _V   &     _V   =>     `' { <. ,  >. }  { <. ,  >. }
 
Theoremop2ndb 4747 Extract the second member of an ordered pair. Theorem 5.12(ii) of [Monk1] p. 52. (See op1stb 4175 to extract the first member and op2nda 4748 for an alternate version.) (Contributed by NM, 25-Nov-2003.)
 _V   &     _V   =>     |^| |^| |^| `' { <. ,  >. }
 
Theoremop2nda 4748 Extract the second member of an ordered pair. (See op1sta 4745 to extract the first member and op2ndb 4747 for an alternate version.) (Contributed by NM, 17-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
 _V   &     _V   =>     U. ran  { <. ,  >. }
 
Theoremcnvsng 4749 Converse of a singleton of an ordered pair. (Contributed by NM, 23-Jan-2015.)
 V  W  `' { <. ,  >. }  {
 <. ,  >. }
 
Theoremopswapg 4750 Swap the members of an ordered pair. (Contributed by Jim Kingdon, 16-Dec-2018.)
 V  W  U. `' { <. ,  >. }  <. ,  >.
 
Theoremelxp4 4751 Membership in a cross product. This version requires no quantifiers or dummy variables. See also elxp5 4752. (Contributed by NM, 17-Feb-2004.)
 X.  C  <. U. dom  { } ,  U. ran  { } >.  U. dom  { }  U. ran  { }  C
 
Theoremelxp5 4752 Membership in a cross product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 4751 when the double intersection does not create class existence problems (caused by int0 3620). (Contributed by NM, 1-Aug-2004.)
 X.  C  <. |^| |^| ,  U. ran  { } >.  |^| |^|  U. ran  { }  C
 
Theoremcnvresima 4753 An image under the converse of a restriction. (Contributed by Jeff Hankins, 12-Jul-2009.)
 `' F  |`  "  `' F " 
 i^i
 
Theoremresdm2 4754 A class restricted to its domain equals its double converse. (Contributed by NM, 8-Apr-2007.)
 |`  dom  `' `'
 
Theoremresdmres 4755 Restriction to the domain of a restriction. (Contributed by NM, 8-Apr-2007.)
 |`  dom  |`  |`
 
Theoremimadmres 4756 The image of the domain of a restriction. (Contributed by NM, 8-Apr-2007.)
 " dom  |` 
 "
 
Theoremmptpreima 4757* The preimage of a function in maps-to notation. (Contributed by Stefan O'Rear, 25-Jan-2015.)
 F  |->    =>     `' F " C  {  |  C }
 
Theoremmptiniseg 4758* Converse singleton image of a function defined by maps-to. (Contributed by Stefan O'Rear, 25-Jan-2015.)
 F  |->    =>     C  V  `' F " { C } 
 {  |  C }
 
Theoremdmmpt 4759 The domain of the mapping operation in general. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 22-Mar-2015.)
 F  |->    =>     dom 
 F  {  |  _V
 }
 
Theoremdmmptss 4760* The domain of a mapping is a subset of its base class. (Contributed by Scott Fenton, 17-Jun-2013.)
 F  |->    =>     dom 
 F  C_
 
Theoremdmmptg 4761* 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.)
 V  dom  |->
 
Theoremrelco 4762 A composition is a relation. Exercise 24 of [TakeutiZaring] p. 25. (Contributed by NM, 26-Jan-1997.)

 Rel  o.
 
Theoremdfco2 4763* Alternate definition of a class composition, using only one bound variable. (Contributed by NM, 19-Dec-2008.)
 o.  U_  _V  `' " { }  X.  " { }
 
Theoremdfco2a 4764* Generalization of dfco2 4763, where  C can have any value between  dom  i^i  ran and  _V. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
 dom  i^i  ran  C_  C  o.  U_  C  `' " { }  X.  " { }
 
Theoremcoundi 4765 Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
 o.  u.  C  o.  u.  o.  C
 
Theoremcoundir 4766 Class composition distributes over union. (Contributed by NM, 21-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
 u.  o.  C  o.  C  u.  o.  C
 
Theoremcores 4767 Restricted first member of a class composition. (Contributed by NM, 12-Oct-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
 ran  C_  C  |`  C  o.  o.
 
Theoremresco 4768 Associative law for the restriction of a composition. (Contributed by NM, 12-Dec-2006.)
 o.  |`  C  o.  |`  C
 
Theoremimaco 4769 Image of the composition of two classes. (Contributed by Jason Orendorff, 12-Dec-2006.)
 o.  " C  " " C
 
Theoremrnco 4770 The range of the composition of two classes. (Contributed by NM, 12-Dec-2006.)

 ran  o.  ran  |`  ran
 
Theoremrnco2 4771 The range of the composition of two classes. (Contributed by NM, 27-Mar-2008.)

 ran  o.  " ran
 
Theoremdmco 4772 The domain of a composition. Exercise 27 of [Enderton] p. 53. (Contributed by NM, 4-Feb-2004.)

 dom  o.  `' " dom
 
Theoremcoiun 4773* Composition with an indexed union. (Contributed by NM, 21-Dec-2008.)
 o.  U_  C  U_  C  o.
 
Theoremcocnvcnv1 4774 A composition is not affected by a double converse of its first argument. (Contributed by NM, 8-Oct-2007.)
 `' `'  o.  o.
 
Theoremcocnvcnv2 4775 A composition is not affected by a double converse of its second argument. (Contributed by NM, 8-Oct-2007.)
 o.  `' `'  o.
 
Theoremcores2 4776 Absorption of a reverse (preimage) restriction of the second member of a class composition. (Contributed by NM, 11-Dec-2006.)
 dom  C_  C  o.  `' `'  |`  C  o.
 
Theoremco02 4777 Composition with the empty set. Theorem 20 of [Suppes] p. 63. (Contributed by NM, 24-Apr-2004.)
 o.  (/)  (/)
 
Theoremco01 4778 Composition with the empty set. (Contributed by NM, 24-Apr-2004.)
 (/)  o.  (/)
 
Theoremcoi1 4779 Composition with the identity relation. Part of Theorem 3.7(i) of [Monk1] p. 36. (Contributed by NM, 22-Apr-2004.)
 Rel  o.  _I
 
Theoremcoi2 4780 Composition with the identity relation. Part of Theorem 3.7(i) of [Monk1] p. 36. (Contributed by NM, 22-Apr-2004.)
 Rel  _I  o.
 
Theoremcoires1 4781 Composition with a restricted identity relation. (Contributed by FL, 19-Jun-2011.) (Revised by Stefan O'Rear, 7-Mar-2015.)
 o.  _I  |`  |`
 
Theoremcoass 4782 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.)
 o.  o.  C  o.  o.  C
 
Theoremrelcnvtr 4783 A relation is transitive iff its converse is transitive. (Contributed by FL, 19-Sep-2011.)
 Rel  R  R  o.  R  C_  R  `' R  o.  `' R  C_  `' R
 
Theoremrelssdmrn 4784 A relation is included in the cross product of its domain and range. Exercise 4.12(t) of [Mendelson] p. 235. (Contributed by NM, 3-Aug-1994.)
 Rel  C_  dom  X.  ran
 
Theoremcnvssrndm 4785 The converse is a subset of the cartesian product of range and domain. (Contributed by Mario Carneiro, 2-Jan-2017.)
 `'  C_  ran 
 X.  dom
 
Theoremcossxp 4786 Composition as a subset of the cross product of factors. (Contributed by Mario Carneiro, 12-Jan-2017.)
 o.  C_  dom  X.  ran
 
Theoremrelrelss 4787 Two ways to describe the structure of a two-place operation. (Contributed by NM, 17-Dec-2008.)
 Rel 
 Rel  dom  C_  _V  X.  _V  X.  _V
 
Theoremunielrel 4788 The membership relation for a relation is inherited by class union. (Contributed by NM, 17-Sep-2006.)
 Rel  R  R  U.  U. R
 
Theoremrelfld 4789 The double union of a relation is its field. (Contributed by NM, 17-Sep-2006.)
 Rel  R  U.
 U. R 
 dom  R  u.  ran  R
 
Theoremrelresfld 4790 Restriction of a relation to its field. (Contributed by FL, 15-Apr-2012.)
 Rel  R  R  |`  U. U. R  R
 
Theoremrelcoi2 4791 Composition with the identity relation restricted to a relation's field. (Contributed by FL, 2-May-2011.)
 Rel  R  _I  |`  U. U. R  o.  R  R
 
Theoremrelcoi1 4792 Composition with the identity relation restricted to a relation's field. (Contributed by FL, 8-May-2011.)
 Rel  R  R  o.  _I  |` 
 U. U. R  R
 
Theoremunidmrn 4793 The double union of the converse of a class is its field. (Contributed by NM, 4-Jun-2008.)

 U. U. `'  dom  u.  ran
 
Theoremrelcnvfld 4794 if  R is a relation, its double union equals the double union of its converse. (Contributed by FL, 5-Jan-2009.)
 Rel  R  U.
 U. R  U. U. `' R
 
Theoremdfdm2 4795 Alternate definition of domain df-dm 4298 that doesn't require dummy variables. (Contributed by NM, 2-Aug-2010.)

 dom  U. U. `'  o.
 
Theoremunixpm 4796* The double class union of an inhabited cross product is the union of its members. (Contributed by Jim Kingdon, 18-Dec-2018.)
 X.  U. U.  X.  u.
 
Theoremunixp0im 4797 The union of an empty cross product is empty. (Contributed by Jim Kingdon, 18-Dec-2018.)
 X.  (/)  U.  X.  (/)
 
Theoremcnvexg 4798 The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26. (Contributed by NM, 17-Mar-1998.)
 V  `'  _V
 
Theoremcnvex 4799 The converse of a set is a set. Corollary 6.8(1) of [TakeutiZaring] p. 26. (Contributed by NM, 19-Dec-2003.)
 _V   =>     `'  _V
 
Theoremrelcnvexb 4800 A relation is a set iff its converse is a set. (Contributed by FL, 3-Mar-2007.)
 Rel  R  R  _V  `' R  _V
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9381
  Copyright terms: Public domain < Previous  Next >