HomeHome Metamath Proof Explorer < Previous   Next >
Browser slow? Try the
Unicode version.

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-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17500 176 17501-17600 177 17601-17700 178 17701-17800 179 17801-17900 180 17901-18000 181 18001-18100 182 18101-18200 183 18201-18300 184 18301-18400 185 18401-18500 186 18501-18600 187 18601-18700 188 18701-18800 189 18801-18900 190 18901-19000 191 19001-19100 192 19101-19200 193 19201-19300 194 19301-19400 195 19401-19465

Color key:    Metamath Proof Explorer  Metamath Proof Explorer
(1-11415)
  Hilbert Space Explorer  Hilbert Space Explorer
(11416-13002)
  Users' Mathboxes  Users' Mathboxes
(13003-19465)
 

Statement List for Metamath Proof Explorer - 3701-3800 - Page 38 of 195
TypeLabelDescription
Statement
 
Theorempwuni 3701 A class is a subclass of the power class of its union. Exercise 6(b) of [Enderton] p. 38.
|- A C_ ~PU.A
 
Theorempwel 3702 Membership of a power class. Exercise 10 of [Enderton] p. 26.
|- (A e. B -> ~PA e. ~P~PU.B)
 
Theoremssextss 3703 An extensionality-like principle defining subclass in terms of subsets.
|- (A C_ B <-> A.x(x C_ A -> x C_ B))
 
Theoremssext 3704 An extensionality-like principle that uses the subset instead of the membership relation: two classes are equal iff they have the same subsets.
|- (A = B <-> A.x(x C_ A <-> x C_ B))
 
Theoremnssss 3705 Negation of subclass relationship. Compare nss 2930. (The proof was shortened by Andrew Salmon, 25-Jul-2011.)
|- (-. A C_ B <-> E.x(x C_ A /\ -. x C_ B))
 
Theorempweqb 3706 Classes are equal if and only if their power classes are equal. Exercise 19 of [TakeutiZaring] p. 18.
|- (A = B <-> ~PA = ~PB)
 
Theoremintid 3707 The intersection of all sets to which a set belongs is the singleton of that set.
|- A e. _V   =>   |- |^|{x | A e. x} = {A}
 
Theoremmoabex 3708 "At most one" existence implies a class abstraction exists.
|- (E*xph -> {x | ph} e. _V)
 
Theoremeuabex 3709 The abstraction of a wff with existential uniqueness exists.
|- (E!xph -> {x | ph} e. _V)
 
Theoremnnullss 3710 A non-empty class (even if proper) has a non-empty subset.
|- (A =/= (/) -> E.x(x C_ A /\ x =/= (/)))
 
Theoremexss 3711 Restricted existence in a class (even if proper) implies restricted existence in a subset.
|- (E.x e. A ph -> E.y(y C_ A /\ E.x e. y ph))
 
TheoremdtruALT 3712 A version of dtru 3694 ("two things exist") with a shorter proof using more axioms.
|- -. A.x x = y
 
Theoremdtrucor 3713 Corollary of dtru 3694. This example illustrates the danger of blindly trusting the standard Deduction Theorem without accounting for free variables: the theorem form of this deduction is not valid, as shown by dtrucor2 3714.
|- x = y   =>   |- x =/= y
 
Theoremdtrucor2 3714 The theorem form of the deduction dtrucor 3713 leads to a contradiction, as mentioned in the "Wrong!" example at http://us.metamath.org/mpegif/mmdeduction.html#bad.
|- (x = y -> x =/= y)   =>   |- (ph /\ -. ph)
 
Theoremdvdemo1 3715 Demonstration of a theorem (scheme) that requires (meta)variables x and y to be distinct, but no others. It bundles the theorem schemes E.x(x = y -> x e. x) and E.x(x = y -> y e. x). Compare dvdemo2 3716. ("Bundles" is a term introduced by Raph Levien.)
|- E.x(x = y -> z e. x)
 
Theoremdvdemo2 3716 Demonstration of a theorem (scheme) that requires (meta)variables x and z to be distinct, but no others. It bundles the theorem schemes E.x(x = x -> z e. x) and E.x(x = y -> y e. x). Compare dvdemo1 3715.
|- E.x(x = y -> z e. x)
 
Derive the Axiom of Pairing
 
Theoremzfpair 3717 The Axiom of Pairing of Zermelo-Fraenkel set theory. Axiom 2 of [TakeutiZaring] p. 15. In some textbooks this is stated as a separate axiom; here we show it is redundant since it can be derived from the other axioms.

This theorem should not be referenced by any proof other than axpr 3718. Instead, use zfpair2 3720 below so that the uses of the Axiom of Pairing can be more easily identified.

|- {x, y} e. _V
 
Theoremaxpr 3718 Unabbreviated version of the Axiom of Pairing of ZF set theory, derived as a theorem from the other axioms.

This theorem should not be referenced by any proof. Instead, use ax-pr 3719 below so that the uses of the Axiom of Pairing can be more easily identified.

|- E.zA.w((w = x \/ w = y) -> w e. z)
 
Axiomax-pr 3719 The Axiom of Pairing of ZF set theory. It was derived as theorem axpr 3718 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily.
|- E.zA.w((w = x \/ w = y) -> w e. z)
 
Theoremzfpair2 3720 Derive the abbreviated version of the Axiom of Pairing from ax-pr 3719. See zfpair 3717 for its derivation from the other axioms.
|- {x, y} e. _V
 
Theoremprex 3721 The Axiom of Pairing using class variables. Theorem 7.13 of [Quine] p. 51. By virtue of its definition, an unordered pair remains a set (even though no longer a pair) even when its components are proper classes (see prprc 3339), so we can dispense with hypotheses requiring them to be sets.
|- {A, B} e. _V
 
Theoremopex 3722 An ordered pair of classes is a set. Exercise 7 of [TakeutiZaring] p. 16.
|- <.A, B>. e. _V
 
Theoremelop 3723 An ordered pair has two elements. Exercise 3 of [TakeutiZaring] p. 15.
|- A e. _V   =>   |- (A e. <.B, C>. <-> (A = {B} \/ A = {B, C}))
 
Theoremopi1 3724 One of the two elements in an ordered pair.
|- {A} e. <.A, B>.
 
Theoremopi2 3725 One of the two elements of an ordered pair.
|- {A, B} e. <.A, B>.
 
Ordered pair theorem
 
Theoremopth1 3726 Equality of the first members of equal ordered pairs, which holds whether or not the second members are sets.
|- A e. _V   =>   |- (<.A, B>. = <.C, D>. -> A = C)
 
Theoremopth 3727 The ordered pair theorem. If two ordered pairs are equal, their first elements are equal and their second elements are equal. Exercise 6 of [TakeutiZaring] p. 16. Note that C is not required to be a set due to a peculiarity of our specific ordered pair definition.
|- A e. _V   &   |- B e. _V   &   |- D e. _V   =>   |- (<.A, B>. = <.C, D>. <-> (A = C /\ B = D))
 
Theoremopthg 3728 Ordered pair theorem.
|- A e. _V   &   |- B e. _V   =>   |- (D e. R -> (<.A, B>. = <.C, D>. <-> (A = C /\ B = D)))
 
Theoremopthgg 3729 Ordered pair theorem. C is not required to be a set under our specific ordered pair definition.
|- ((A e. V /\ B e. W /\ D e. X) -> (<.A, B>. = <.C, D>. <-> (A = C /\ B = D)))
 
Theoremotthg 3730 Ordered triple theorem.
|- A e. _V   &   |- B e. _V   &   |- R e. _V   =>   |- ((D e. F /\ S e. G) -> (<.<.A, B>., R>. = <.<.C, D>., S>. <-> (A = C /\ B = D /\ R = S)))
 
Theoremeqvinop 3731 A variable introduction law for ordered pairs. Analogue of Lemma 15 of [Monk2] p. 109.
|- B e. _V   &   |- C e. _V   =>   |- (A = <.B, C>. <-> E.xE.y(A = <.x, y>. /\ <.x, y>. = <.B, C>.))
 
Theoremcopsexg 3732 Substitution of class A for ordered pair <.x, y>.. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 11-Jul-2011.)
|- (A = <.x, y>. -> (ph <-> E.xE.y(A = <.x, y>. /\ ph)))
 
Theoremcopsex2t 3733 Closed theorem form of copsex2g 3734.
|- ((A.xA.y((x = A /\ y = B) -> (ph <-> ps)) /\ (A e. V /\ B e. W)) -> (E.xE.y(<.A, B>. = <.x, y>. /\ ph) <-> ps))
 
Theoremcopsex2g 3734 Implicit substitution inference for ordered pairs.
|- ((x = A /\ y = B) -> (ph <-> ps))   =>   |- ((A e. V /\ B e. W) -> (E.xE.y(<.A, B>. = <.x, y>. /\ ph) <-> ps))
 
Theoremcopsex4g 3735 An implicit substitution inference for 2 ordered pairs.
|- (((x = A /\ y = B) /\ (z = C /\ w = D)) -> (ph <-> ps))   =>   |- (((A e. R /\ B e. S) /\ (C e. R /\ D e. S)) -> (E.xE.yE.zE.w((<.A, B>. = <.x, y>. /\ <.C, D>. = <.z, w>.) /\ ph) <-> ps))
 
Theoremopnz 3736 An ordered pair is not empty.
|- -. <.A, B>. = (/)
 
Theoremopprc1b 3737 A property of an ordered pair of proper classes (due to our particular definition of ordered pair).
|- (-. A e. _V <-> (/) e. <.A, B>.)
 
Theoremopprc3 3738 A property of an ordered pair of proper classes (due to our particular definition of ordered pair).
|- ((-. A e. _V /\ -. B e. _V) <-> <.A, B>. = {(/)})
 
Theoremopeqex 3739 Equivalence of existence implied by equality of ordered pairs.
|- (<.A, B>. = <.C, D>. -> (A e. _V <-> C e. _V))
 
Theoremoteqex 3740 Equivalence of existence implied by equality of ordered triples.
|- (<.<.A, B>., C>. = <.<.R, S>., T>. -> (A e. _V <-> R e. _V))
 
Theoremopth2 3741 Equality of the second members of equal ordered pairs. Because of our particular ordered pair definition, equality holds whether or not the first members are sets.
|- B e. _V   &   |- D e. _V   =>   |- (<.A, B>. = <.C, D>. -> B = D)
 
Theoremopcom 3742 An ordered pair commutes iff its members are equal.
|- A e. _V   =>   |- (<.A, B>. = <.B, A>. <-> A = B)
 
Theoremmoop2 3743 "At most one" property of an ordered pair. The proof is a little tricky because we do not place any restrictions on class B.
|- E*x A = <.B, x>.
 
Theoremopeqsn 3744 Equivalence for an ordered pair equal to a singleton.
|- A e. _V   &   |- B e. _V   &   |- C e. _V   =>   |- (<.A, B>. = {C} <-> (A = B /\ C = {A}))
 
Theoremopeqpr 3745 Equivalence for an ordered pair equal to an unordered pair.
|- C e. _V   &   |- D e. _V   =>   |- (<.A, B>. = {C, D} <-> ((C = {A} /\ D = {A, B}) \/ (C = {A, B} /\ D = {A})))
 
Theoremmosubopt 3746 "At most one" remains true inside ordered pair quantification.
|- (A.yA.zE*xph -> E*xE.yE.z(A = <.y, z>. /\ ph))
 
Theoremmosubop 3747 "At most one" remains true inside ordered pair quantification.
|- E*xph   =>   |- E*xE.yE.z(A = <.y, z>. /\ ph)
 
Theoremeuop2 3748 Transfer existential uniqueness to second member of an ordered pair.
|- (E!xE.y(x = <.A, y>. /\ ph) <-> E!yph)
 
Theoremopthwiener 3749 Justification theorem for the ordered pair definition in Norbert Wiener, "A simplification of the logic of relations," Proc. of the Cambridge Philos. Soc., 1914, vol. 17, pp.387-390. It is also shown as a definition in [Enderton] p. 36 and as Exercise 4.8(b) of [Mendelson] p. 230. It is meaningful only for classes that exist as sets (i.e. are not proper classes). See df-op 3278 for other ordered pair definitions.
|- A e. _V   &   |- B e. _V   =>   |- ({{{A}, (/)}, {{B}}} = {{{C}, (/)}, {{D}}} <-> (A = C /\ B = D))
 
Theoremuniop 3750 The union of an ordered pair. Theorem 65 of [Suppes] p. 39.
|- U.<.A, B>. = {A, B}
 
Theoremuniopel 3751 Ordered pair membership is inherited by class union.
|- (<.A, B>. e. C -> U.<.A, B>. e. U.C)
 
Ordered-pair class abstractions (cont.)
 
Theoremopabid 3752 The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. (The proof was shortened by Andrew Salmon, 25-Jul-2011.)
|- (<.x, y>. e. {<.x, y>. | ph} <-> ph)
 
Theoremelopab 3753 Membership in a class abstraction of pairs.
|- (A e. {<.x, y>. | ph} <-> E.xE.y(A = <.x, y>. /\ ph))
 
Theoremhbopab 3754 Bound-variable hypothesis builder for class abstraction. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 11-Jul-2011.)
|- (ph -> A.zph)   =>   |- (w e. {<.x, y>. | ph} -> A.z w e. {<.x, y>. | ph})
 
Theoremhbopab1 3755 The first abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free.
|- (z e. {<.x, y>. | ph} -> A.x z e. {<.x, y>. | ph})
 
Theoremhbopab2 3756 The second abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free.
|- (z e. {<.x, y>. | ph} -> A.y z e. {<.x, y>. | ph})
 
Theoremopelopabsb 3757 The law of concretion in terms of substitutions. (The proof was shortened by Andrew Salmon, 25-Jul-2011.)
|- (<.z, w>. e. {<.x, y>. | ph} <-> [w / y][z / x]ph)
 
Theorembrabsb 3758 The law of concretion in terms of substitutions.
|- R = {<.x, y>. | ph}   =>   |- (zRw <-> [w / y][z / x]ph)
 
Theoremopelopabt 3759 Closed theorem form of opelopab 3763.
|- ((A.xA.y(x = A -> (ph <-> ps)) /\ A.xA.y(y = B -> (ps <-> ch)) /\ (A e. V /\ B e. W)) -> (<.A, B>. e. {<.x, y>. | ph} <-> ch))
 
Theoremopelopabg 3760 The law of concretion. Theorem 9.5 of [Quine] p. 61.
|- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   =>   |- ((A e. V /\ B e. W) -> (<.A, B>. e. {<.x, y>. | ph} <-> ch))
 
Theorembrabg 3761 The law of concretion for a binary relation.
|- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- R = {<.x, y>. | ph}   =>   |- ((A e. C /\ B e. D) -> (ARB <-> ch))
 
Theoremopelopab2 3762 Ordered pair membership in an ordered pair class abstraction.
|- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   =>   |- ((A e. C /\ B e. D) -> (<.A, B>. e. {<.x, y>. | ((x e. C /\ y e. D) /\ ph)} <-> ch))
 
Theoremopelopab 3763 The law of concretion. Theorem 9.5 of [Quine] p. 61.
|- A e. _V   &   |- B e. _V   &   |- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   =>   |- (<.A, B>. e. {<.x, y>. | ph} <-> ch)
 
Theorembrab 3764 The law of concretion for a binary relation.
|- A e. _V   &   |- B e. _V   &   |- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- R = {<.x, y>. | ph}   =>   |- (ARB <-> ch)
 
Theoremopelopabf 3765 The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 3763 uses bound-variable hypotheses in place of distinct variable conditions."
|- (ps -> A.xps)   &   |- (ch -> A.ych)   &   |- A e. _V   &   |- B e. _V   &   |- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   =>   |- (<.A, B>. e. {<.x, y>. | ph} <-> ch)
 
Theoremssopab2 3766 Equivalence of ordered pair abstraction subclass and implication.
|- ({<.x, y>. | ph} C_ {<.x, y>. | ps} <-> A.xA.y(ph -> ps))
 
Theoremssopab2i 3767 Inference of ordered pair abstraction subclass from implication.
|- (ph -> ps)   =>   |- {<.x, y>. | ph} C_ {<.x, y>. | ps}
 
Theoremopabn0 3768 Non-empty ordered pair class abstraction.
|- ({<.x, y>. | ph} =/= (/) <-> E.xE.yph)
 
Power class of union and intersection
 
Theorempwin 3769 The power class of the intersection of two classes is the intersection of their power classes. Exercise 4.12(j) of [Mendelson] p. 235.
|- ~P(A i^i B) = (~PA i^i ~PB)
 
Theorempwunss 3770 The power class of the union of two classes includes the union of their power classes. Exercise 4.12(k) of [Mendelson] p. 235.
|- (~PA u. ~PB) C_ ~P(A u. B)
 
Theorempwssun 3771 The power class of the union of two classes is a subset of the union of their power classes, iff one class is a subclass of the other. Exercise 4.12(l) of [Mendelson] p. 235.
|- ((A C_ B \/ B C_ A) <-> ~P(A u. B) C_ (~PA u. ~PB))
 
Theorempwundif 3772 Break up the power class of a union into a union of smaller classes.
|- ~P(A u. B) = ((~P(A u. B) \ ~PA) u. ~PA)
 
Theorempwun 3773 The power class of the union of two classes equals the union of their power classes, iff one class is a subclass of the other. Part of Exercise 7(b) of [Enderton] p. 28.
|- ((A C_ B \/ B C_ A) <-> ~P(A u. B) = (~PA u. ~PB))
 
Epsilon and identity relations
 
Syntaxcep 3774 Extend class notation to include the epsilon relation.
class _E
 
Syntaxcid 3775 Extend the definition of a class to include identity relation.
class _I
 
Definitiondf-eprel 3776 Define the epsilon relation. Similar to Definition 6.22 of [TakeutiZaring] p. 30.
|- _E = {<.x, y>. | x e. y}
 
Theoremepelc 3777 The epsilon relation and the membership relation are the same.
|- A e. _V   &   |- B e. _V   =>   |- (A _E B <-> A e. B)
 
Theoremepel 3778 The epsilon relation and the membership relation are the same.
|- (x _E y <-> x e. y)
 
Definitiondf-id 3779 Define the identity relation. Definition 9.15 of [Quine] p. 64.
|- _I = {<.x, y>. | x = y}
 
Theoremdfid3 3780 A stronger version of df-id 3779 that doesn't require x and y to be distinct. Ordinarily, we wouldn't use this as a definition, since non-distinct dummy variables would make soundness verification more difficult (as the proof here shows). The proof can be instructive in showing how distinct variable requirements may be eliminated, a task that is not necessarily obvious.
|- _I = {<.x, y>. | x = y}
 
Theoremdfid2 3781 Alternate definition of the identity relation.
|- _I = {<.x, x>. | x = x}
 
Partial and complete ordering
 
Syntaxwpo 3782 Extend wff notation to include the strict partial ordering predicate. Read: ' R is a partial order on A.'
wff R Po A
 
Syntaxwor 3783 Extend wff notation to include the strict complete ordering predicate. Read: ' R orders A.'
wff R Or A
 
Definitiondf-po 3784 Define the strict partial order predicate. Definition of [Enderton] p. 168.
|- (R Po A <-> A.x e. A A.y e. A A.z e. A (-. xRx /\ ((xRy /\ yRz) -> xRz)))
 
Theoremposs 3785 Subset theorem for the partial ordering predicate. (The proof was shortened by Andrew Salmon, 25-Jul-2011.)
|- (A C_ B -> (R Po B -> R Po A))
 
Theorempoeq1 3786 Equality theorem for partial ordering predicate.
|- (R = S -> (R Po A <-> S Po A))
 
Theorempoeq2 3787 Equality theorem for partial ordering predicate.
|- (A = B -> (R Po A <-> R Po B))
 
Theorempocl 3788 Properties of partial order relation in class notation.
|- (R Po A -> ((B e. A /\ C e. A /\ D e. A) -> (-. BRB /\ ((BRC /\ CRD) -> BRD))))
 
Theorempoirr 3789 A partial order relation is irreflexive.
|- ((R Po A /\ B e. A) -> -. BRB)
 
Theorempotr 3790 A partial order relation is a transitive relation.
|- ((R Po A /\ (B e. A /\ C e. A /\ D e. A)) -> ((BRC /\ CRD) -> BRD))
 
Theorempo2nr 3791 A partial order relation has no 2-cycle loops.
|- ((R Po A /\ (B e. A /\ C e. A)) -> -. (BRC /\ CRB))
 
Theorempo3nr 3792 A partial order relation has no 3-cycle loops.
|- ((R Po A /\ (B e. A /\ C e. A /\ D e. A)) -> -. (BRC /\ CRD /\ DRB))
 
Theorempo0 3793 Any relation is a partial ordering of the empty set. (The proof was shortened by Andrew Salmon, 25-Jul-2011.)
|- R Po (/)
 
Theoremposn 3794 Partial ordering of a singleton.
|- (R Po {x} <-> -. <.x, x>. e. R)
 
Theorempofun 3795 A function preserves a partial order relation. (Contributed by Jeff Madsen, 18-Jun-2011.)
|- S = {<.x, y>. | XRY}   &   |- (x = y -> X = Y)   =>   |- ((R Po B /\ A.x e. A X e. B) -> S Po A)
 
Definitiondf-so 3796 Define the strict complete (linear) order predicate.
|- (R Or A <-> (R Po A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)))
 
Theoremsopo 3797 A strict linear order is a strict partial order.
|- (R Or A -> R Po A)
 
Theoremsoss 3798 Subset theorem for the strict ordering predicate. (The proof was shortened by Andrew Salmon, 25-Jul-2011.)
|- (A C_ B -> (R Or B -> R Or A))
 
Theoremsoeq1 3799 Equality theorem for the strict ordering predicate.
|- (R = S -> (R Or A <-> S Or A))
 
Theoremsoeq2 3800 Equality theorem for the strict ordering predicate.
|- (A = B -> (R Or A <-> R Or B))

MPE Home   Contents Copyright terms: Public domain < Previous  Next >