HomeHome Intuitionistic Logic Explorer
Theorem List (p. 44 of 95)
< 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 - 4301-4400   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Definitiondf-ima 4301 Define the image of a class (as restricted by another class). Definition 6.6(2) of [TakeutiZaring] p. 24. For example, ( F = {  <. 2 , 6  >.,  <. 3 , 9  >. } /\ B = { 1 , 2 } ) -> ( F  " B ) = { 6 } . Contrast with restriction (df-res 4300) and range (df-rn 4299). For an alternate definition, see dfima2 4613. (Contributed by NM, 2-Aug-1994.)
 "  ran  |`
 
Theoremxpeq1 4302 Equality theorem for cross product. (Contributed by NM, 4-Jul-1994.)
 X.  C  X.  C
 
Theoremxpeq2 4303 Equality theorem for cross product. (Contributed by NM, 5-Jul-1994.)
 C  X.  C  X.
 
Theoremelxpi 4304* Membership in a cross product. Uses fewer axioms than elxp 4305. (Contributed by NM, 4-Jul-1994.)
 X.  C  <. ,  >.  C
 
Theoremelxp 4305* Membership in a cross product. (Contributed by NM, 4-Jul-1994.)
 X.  C  <. ,  >.  C
 
Theoremelxp2 4306* Membership in a cross product. (Contributed by NM, 23-Feb-2004.)
 X.  C  C  <. ,  >.
 
Theoremxpeq12 4307 Equality theorem for cross product. (Contributed by FL, 31-Aug-2009.)
 C  D  X.  C  X.  D
 
Theoremxpeq1i 4308 Equality inference for cross product. (Contributed by NM, 21-Dec-2008.)
   =>     X.  C  X.  C
 
Theoremxpeq2i 4309 Equality inference for cross product. (Contributed by NM, 21-Dec-2008.)
   =>     C  X.  C  X.
 
Theoremxpeq12i 4310 Equality inference for cross product. (Contributed by FL, 31-Aug-2009.)
   &     C  D   =>     X.  C  X.  D
 
Theoremxpeq1d 4311 Equality deduction for cross product. (Contributed by Jeff Madsen, 17-Jun-2010.)
   =>     X.  C  X.  C
 
Theoremxpeq2d 4312 Equality deduction for cross product. (Contributed by Jeff Madsen, 17-Jun-2010.)
   =>     C  X.  C  X.
 
Theoremxpeq12d 4313 Equality deduction for cross product. (Contributed by NM, 8-Dec-2013.)
   &     C  D   =>     X.  C  X.  D
 
Theoremnfxp 4314 Bound-variable hypothesis builder for cross product. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 15-Oct-2016.)
 F/_   &     F/_   =>     F/_ 
 X.
 
Theorem0nelxp 4315 The empty set is not a member of a cross product. (Contributed by NM, 2-May-1996.) (Revised by Mario Carneiro, 26-Apr-2015.)
 (/) 
 X.
 
Theorem0nelelxp 4316 A member of a cross product (ordered pair) doesn't contain the empty set. (Contributed by NM, 15-Dec-2008.)
 C  X.  (/)  C
 
Theoremopelxp 4317 Ordered pair membership in a cross product. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
 <. ,  >.  C  X.  D  C  D
 
Theorembrxp 4318 Binary relation on a cross product. (Contributed by NM, 22-Apr-2004.)
 C  X.  D  C  D
 
Theoremopelxpi 4319 Ordered pair membership in a cross product (implication). (Contributed by NM, 28-May-1995.)
 C  D  <. ,  >.  C  X.  D
 
Theoremopelxp1 4320 The first member of an ordered pair of classes in a cross product belongs to first cross product argument. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
 <. ,  >.  C  X.  D  C
 
Theoremopelxp2 4321 The second member of an ordered pair of classes in a cross product belongs to second cross product argument. (Contributed by Mario Carneiro, 26-Apr-2015.)
 <. ,  >.  C  X.  D  D
 
Theoremotelxp1 4322 The first member of an ordered triple of classes in a cross product belongs to first cross product argument. (Contributed by NM, 28-May-2008.)
 <. <. ,  >. ,  C >.  R  X.  S 
 X.  T  R
 
Theoremrabxp 4323* Membership in a class builder restricted to a cross product. (Contributed by NM, 20-Feb-2014.)
 <. ,  >.    =>    
 {  X.  | 
 }  { <. ,  >.  |  }
 
Theorembrrelex12 4324 A true binary relation on a relation implies the arguments are sets. (This is a property of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015.)
 Rel  R  R  _V  _V
 
Theorembrrelex 4325 A true binary relation on a relation implies the first argument is a set. (This is a property of our ordered pair definition.) (Contributed by NM, 18-May-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
 Rel  R  R  _V
 
Theorembrrelex2 4326 A true binary relation on a relation implies the second argument is a set. (This is a property of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015.)
 Rel  R  R  _V
 
Theorembrrelexi 4327 The first argument of a binary relation exists. (An artifact of our ordered pair definition.) (Contributed by NM, 4-Jun-1998.)

 Rel  R   =>     R  _V
 
Theorembrrelex2i 4328 The second argument of a binary relation exists. (An artifact of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015.)

 Rel  R   =>     R  _V
 
Theoremnprrel 4329 No proper class is related to anything via any relation. (Contributed by Roy F. Longton, 30-Jul-2005.)

 Rel  R   &     _V   =>     R
 
Theoremfconstmpt 4330* Representation of a constant function using the mapping operation. (Note that cannot appear free in .) (Contributed by NM, 12-Oct-1999.) (Revised by Mario Carneiro, 16-Nov-2013.)
 X.  { }  |->
 
Theoremvtoclr 4331* Variable to class conversion of transitive relation. (Contributed by NM, 9-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)

 Rel  R   &     R  R  R   =>     R  R C  R C
 
Theoremopelvvg 4332 Ordered pair membership in the universal class of ordered pairs. (Contributed by Mario Carneiro, 3-May-2015.)
 V  W  <. ,  >.  _V  X.  _V
 
Theoremopelvv 4333 Ordered pair membership in the universal class of ordered pairs. (Contributed by NM, 22-Aug-2013.) (Revised by Mario Carneiro, 26-Apr-2015.)
 _V   &     _V   =>     <. ,  >.  _V  X.  _V
 
Theoremopthprc 4334 Justification theorem for an ordered pair definition that works for any classes, including proper classes. This is a possible definition implied by the footnote in [Jech] p. 78, which says, "The sophisticated reader will not object to our use of a pair of classes." (Contributed by NM, 28-Sep-2003.)

 X.  { (/) }  u.  X.  { { (/)
 } }  C  X.  { (/) }  u.  D  X.  { { (/) } }  C  D
 
Theorembrel 4335 Two things in a binary relation belong to the relation's domain. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 26-Apr-2015.)
 R  C_  C  X.  D   =>     R  C  D
 
Theorembrab2a 4336* Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 9-Nov-2015.)
   &     R  { <. ,  >.  |  C  D  }   =>     R  C  D
 
Theoremelxp3 4337* Membership in a cross product. (Contributed by NM, 5-Mar-1995.)
 X.  C  <. ,  >.  <. ,  >.  X.  C
 
Theoremopeliunxp 4338 Membership in a union of cross products. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by Mario Carneiro, 1-Jan-2017.)
 <. ,  C >.  U_  { }  X.  C
 
Theoremxpundi 4339 Distributive law for cross product over union. Theorem 103 of [Suppes] p. 52. (Contributed by NM, 12-Aug-2004.)
 X.  u.  C 
 X.  u.  X.  C
 
Theoremxpundir 4340 Distributive law for cross product over union. Similar to Theorem 103 of [Suppes] p. 52. (Contributed by NM, 30-Sep-2002.)
 u.  X.  C 
 X.  C  u.  X.  C
 
Theoremxpiundi 4341* Distributive law for cross product over indexed union. (Contributed by Mario Carneiro, 27-Apr-2014.)
 C  X.  U_  U_  C  X.
 
Theoremxpiundir 4342* Distributive law for cross product over indexed union. (Contributed by Mario Carneiro, 27-Apr-2014.)
 U_  X.  C  U_  X.  C
 
Theoremiunxpconst 4343* Membership in a union of cross products when the second factor is constant. (Contributed by Mario Carneiro, 29-Dec-2014.)
 U_  { }  X.  X.
 
Theoremxpun 4344 The cross product of two unions. (Contributed by NM, 12-Aug-2004.)
 u.  X.  C  u.  D  X.  C  u.  X.  D  u.  X.  C  u.  X.  D
 
Theoremelvv 4345* Membership in universal class of ordered pairs. (Contributed by NM, 4-Jul-1994.)
 _V  X.  _V  <. ,  >.
 
Theoremelvvv 4346* Membership in universal class of ordered triples. (Contributed by NM, 17-Dec-2008.)
 _V  X.  _V  X.  _V  <. <. ,  >. ,  >.
 
Theoremelvvuni 4347 An ordered pair contains its union. (Contributed by NM, 16-Sep-2006.)
 _V  X.  _V  U.
 
Theoremmosubopt 4348* "At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-Aug-2007.)
 <. ,  >.
 
Theoremmosubop 4349* "At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-May-1995.)
   =>     <. ,  >.
 
Theorembrinxp2 4350 Intersection of binary relation with cross product. (Contributed by NM, 3-Mar-2007.) (Revised by Mario Carneiro, 26-Apr-2015.)
 R  i^i  C  X.  D  C  D  R
 
Theorembrinxp 4351 Intersection of binary relation with cross product. (Contributed by NM, 9-Mar-1997.)
 C  D  R  R  i^i  C  X.  D
 
Theorempoinxp 4352 Intersection of partial order with cross product of its field. (Contributed by Mario Carneiro, 10-Jul-2014.)
 R  Po  R  i^i 
 X.  Po
 
Theoremsoinxp 4353 Intersection of linear order with cross product of its field. (Contributed by Mario Carneiro, 10-Jul-2014.)
 R  Or  R  i^i 
 X.  Or
 
Theoremseinxp 4354 Intersection of set-like relation with cross product of its field. (Contributed by Mario Carneiro, 22-Jun-2015.)
 R Se  R  i^i  X. Se
 
Theoremposng 4355 Partial ordering of a singleton. (Contributed by Jim Kingdon, 5-Dec-2018.)
 Rel  R  _V  R  Po  { }  R
 
Theoremsosng 4356 Strict linear ordering on a singleton. (Contributed by Jim Kingdon, 5-Dec-2018.)
 Rel  R  _V  R  Or  { }  R
 
Theoremopabssxp 4357* An abstraction relation is a subset of a related cross product. (Contributed by NM, 16-Jul-1995.)

 { <. ,  >.  |  }  C_  X.
 
Theorembrab2ga 4358* The law of concretion for a binary relation. See brab2a 4336 for alternate proof. TODO: should one of them be deleted? (Contributed by Mario Carneiro, 28-Apr-2015.) (Proof modification is discouraged.)
   &     R  { <. ,  >.  |  C  D  }   =>     R  C  D
 
Theoremoptocl 4359* Implicit substitution of class for ordered pair. (Contributed by NM, 5-Mar-1995.)
 D 
 X.  C   &     <. ,  >.    &     C    =>     D
 
Theorem2optocl 4360* Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995.)
 R  C  X.  D   &     <. ,  >.    &     <. ,  >.    &     C  D  C  D    =>     R  R
 
Theorem3optocl 4361* Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995.)
 R  D  X.  F   &     <. ,  >.    &     <. ,  >.    &     <. ,  >.  C    &     D  F  D  F  D  F    =>     R  R  C  R
 
Theoremopbrop 4362* Ordered pair membership in a relation. Special case. (Contributed by NM, 5-Aug-1995.)
 C  D    &     R  { <. ,  >.  |  S  X.  S  S  X.  S  <. ,  >.  <. ,  >.  }   =>     S  S  C  S  D  S  <. ,  >. R <. C ,  D >.
 
Theorem0xp 4363 The cross product with the empty set is empty. Part of Theorem 3.13(ii) of [Monk1] p. 37. (Contributed by NM, 4-Jul-1994.)
 (/)  X.  (/)
 
Theoremcsbxpg 4364 Distribute proper substitution through the cross product of two classes. (Contributed by Alan Sare, 10-Nov-2012.)
 D  [_  ]_  X.  C  [_  ]_  X.  [_  ]_ C
 
Theoremreleq 4365 Equality theorem for the relation predicate. (Contributed by NM, 1-Aug-1994.)
 Rel  Rel
 
Theoremreleqi 4366 Equality inference for the relation predicate. (Contributed by NM, 8-Dec-2006.)
   =>     Rel  Rel
 
Theoremreleqd 4367 Equality deduction for the relation predicate. (Contributed by NM, 8-Mar-2014.)
   =>     Rel  Rel
 
Theoremnfrel 4368 Bound-variable hypothesis builder for a relation. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
 F/_   =>    
 F/ Rel
 
Theoremsbcrel 4369 Distribute proper substitution through a relation predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
 V  [.  ]. Rel  R  Rel  [_  ]_ R
 
Theoremrelss 4370 Subclass theorem for relation predicate. Theorem 2 of [Suppes] p. 58. (Contributed by NM, 15-Aug-1994.)
 C_  Rel  Rel
 
Theoremssrel 4371* A subclass relationship depends only on a relation's ordered pairs. Theorem 3.2(i) of [Monk1] p. 33. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
 Rel  C_  <. ,  >.  <. ,  >.
 
Theoremeqrel 4372* Extensionality principle for relations. Theorem 3.2(ii) of [Monk1] p. 33. (Contributed by NM, 2-Aug-1994.)
 Rel 
 Rel  <. ,  >.  <. ,  >.
 
Theoremssrel2 4373* A subclass relationship depends only on a relation's ordered pairs. This version of ssrel 4371 is restricted to the relation's domain. (Contributed by Thierry Arnoux, 25-Jan-2018.)
 R  C_  X.  R  C_  S  <. ,  >.  R  <. ,  >.  S
 
Theoremrelssi 4374* Inference from subclass principle for relations. (Contributed by NM, 31-Mar-1998.)

 Rel    &     <. ,  >.  <. ,  >.    =>     C_
 
Theoremrelssdv 4375* Deduction from subclass principle for relations. (Contributed by NM, 11-Sep-2004.)
 Rel    &     <. ,  >.  <. ,  >.    =>     C_
 
Theoremeqrelriv 4376* Inference from extensionality principle for relations. (Contributed by FL, 15-Oct-2012.)
 <. ,  >.  <. ,  >.    =>     Rel  Rel
 
Theoremeqrelriiv 4377* Inference from extensionality principle for relations. (Contributed by NM, 17-Mar-1995.)

 Rel    &     Rel    &     <. ,  >.  <. ,  >.    =>   
 
Theoremeqbrriv 4378* Inference from extensionality principle for relations. (Contributed by NM, 12-Dec-2006.)

 Rel    &     Rel    &       =>   
 
Theoremeqrelrdv 4379* Deduce equality of relations from equivalence of membership. (Contributed by Rodolfo Medina, 10-Oct-2010.)

 Rel    &     Rel    &     <. ,  >. 
 <. ,  >.    =>   
 
Theoremeqbrrdv 4380* Deduction from extensionality principle for relations. (Contributed by Mario Carneiro, 3-Jan-2017.)
 Rel    &     Rel    &       =>   
 
Theoremeqbrrdiv 4381* Deduction from extensionality principle for relations. (Contributed by Rodolfo Medina, 10-Oct-2010.)

 Rel    &     Rel    &       =>   
 
Theoremeqrelrdv2 4382* A version of eqrelrdv 4379. (Contributed by Rodolfo Medina, 10-Oct-2010.)
 <. ,  >. 
 <. ,  >.    =>     Rel  Rel
 
Theoremssrelrel 4383* A subclass relationship determined by ordered triples. Use relrelss 4787 to express the antecedent in terms of the relation predicate. (Contributed by NM, 17-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
 C_  _V  X.  _V  X.  _V  C_ 
 <. <. ,  >. ,  >.  <. <. ,  >. ,  >.
 
Theoremeqrelrel 4384* Extensionality principle for ordered triples, analogous to eqrel 4372. Use relrelss 4787 to express the antecedent in terms of the relation predicate. (Contributed by NM, 17-Dec-2008.)
 u.  C_  _V  X.  _V  X.  _V 
 <. <. ,  >. ,  >.  <.
 <. ,  >. ,  >.
 
Theoremelrel 4385* A member of a relation is an ordered pair. (Contributed by NM, 17-Sep-2006.)
 Rel  R  R  <. ,  >.
 
Theoremrelsn 4386 A singleton is a relation iff it is an ordered pair. (Contributed by NM, 24-Sep-2013.)
 _V   =>     Rel  { }  _V  X. 
 _V
 
Theoremrelsnop 4387 A singleton of an ordered pair is a relation. (Contributed by NM, 17-May-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
 _V   &     _V   =>     Rel  { <. ,  >. }
 
Theoremxpss12 4388 Subset theorem for cross product. Generalization of Theorem 101 of [Suppes] p. 52. (Contributed by NM, 26-Aug-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
 C_  C  C_  D  X.  C  C_ 
 X.  D
 
Theoremxpss 4389 A cross product is included in the ordered pair universe. Exercise 3 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.)
 X.  C_  _V  X.  _V
 
Theoremrelxp 4390 A cross product is a relation. Theorem 3.13(i) of [Monk1] p. 37. (Contributed by NM, 2-Aug-1994.)

 Rel  X.
 
Theoremxpss1 4391 Subset relation for cross product. (Contributed by Jeff Hankins, 30-Aug-2009.)
 C_  X.  C  C_  X.  C
 
Theoremxpss2 4392 Subset relation for cross product. (Contributed by Jeff Hankins, 30-Aug-2009.)
 C_  C  X.  C_  C  X.
 
Theoremxpsspw 4393 A cross product is included in the power of the power of the union of its arguments. (Contributed by NM, 13-Sep-2006.)
 X.  C_  ~P ~P  u.
 
Theoremunixpss 4394 The double class union of a cross product is included in the union of its arguments. (Contributed by NM, 16-Sep-2006.)

 U. U.  X.  C_  u.
 
Theoremxpexg 4395 The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. (Contributed by NM, 14-Aug-1994.)
 V  W  X.  _V
 
Theoremxpex 4396 The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. (Contributed by NM, 14-Aug-1994.)
 _V   &     _V   =>     X.  _V
 
Theoremrelun 4397 The union of two relations is a relation. Compare Exercise 5 of [TakeutiZaring] p. 25. (Contributed by NM, 12-Aug-1994.)
 Rel  u.  Rel  Rel
 
Theoremrelin1 4398 The intersection with a relation is a relation. (Contributed by NM, 16-Aug-1994.)
 Rel  Rel  i^i
 
Theoremrelin2 4399 The intersection with a relation is a relation. (Contributed by NM, 17-Jan-2006.)
 Rel  Rel  i^i
 
Theoremreldif 4400 A difference cutting down a relation is a relation. (Contributed by NM, 31-Mar-1998.)
 Rel  Rel  \
    < 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-9400 95 9401-9457
  Copyright terms: Public domain < Previous  Next >