mmtheorems38 - Metamath Proof Explorer

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

Statement List for Metamath Proof Explorer - 3701-3800 - Page 38 of 195

Type	Label	Description
Statement
Theorem	pwuni 3701	A class is a subclass of the power class of its union. Exercise 6(b) of [Enderton] p. 38.
|- A C_ ~PU.A
Theorem	pwel 3702	Membership of a power class. Exercise 10 of [Enderton] p. 26.
|- (A e. B -> ~PA e. ~P~PU.B)
Theorem	ssextss 3703	An extensionality-like principle defining subclass in terms of subsets.
|- (A C_ B <-> A.x(x C_ A -> x C_ B))
Theorem	ssext 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))
Theorem	nssss 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))
Theorem	pweqb 3706	Classes are equal if and only if their power classes are equal. Exercise 19 of [TakeutiZaring] p. 18.
|- (A = B <-> ~PA = ~PB)
Theorem	intid 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}
Theorem	moabex 3708	"At most one" existence implies a class abstraction exists.
|- (E*xph -> {x | ph} e. _V)
Theorem	euabex 3709	The abstraction of a wff with existential uniqueness exists.
|- (E!xph -> {x | ph} e. _V)
Theorem	nnullss 3710	A non-empty class (even if proper) has a non-empty subset.
|- (A =/= (/) -> E.x(x C_ A /\ x =/= (/)))
Theorem	exss 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))
Theorem	dtruALT 3712	A version of dtru 3694 ("two things exist") with a shorter proof using more axioms.
|- -. A.x x = y
Theorem	dtrucor 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
Theorem	dtrucor2 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)
Theorem	dvdemo1 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)
Theorem	dvdemo2 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
Theorem	zfpair 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
Theorem	axpr 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)
Axiom	ax-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)
Theorem	zfpair2 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
Theorem	prex 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
Theorem	opex 3722	An ordered pair of classes is a set. Exercise 7 of [TakeutiZaring] p. 16.
|- <.A, B>. e. _V
Theorem	elop 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}))
Theorem	opi1 3724	One of the two elements in an ordered pair.
|- {A} e. <.A, B>.
Theorem	opi2 3725	One of the two elements of an ordered pair.
|- {A, B} e. <.A, B>.
Ordered pair theorem
Theorem	opth1 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)
Theorem	opth 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))
Theorem	opthg 3728	Ordered pair theorem.
|- A e. _V   &   |- B e. _V   =>   |- (D e. R -> (<.A, B>. = <.C, D>. <-> (A = C /\ B = D)))
Theorem	opthgg 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)))
Theorem	otthg 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)))
Theorem	eqvinop 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>.))
Theorem	copsexg 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)))
Theorem	copsex2t 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))
Theorem	copsex2g 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))
Theorem	copsex4g 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))
Theorem	opnz 3736	An ordered pair is not empty.
|- -. <.A, B>. = (/)
Theorem	opprc1b 3737	A property of an ordered pair of proper classes (due to our particular definition of ordered pair).
|- (-. A e. _V <-> (/) e. <.A, B>.)
Theorem	opprc3 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>. = {(/)})
Theorem	opeqex 3739	Equivalence of existence implied by equality of ordered pairs.
|- (<.A, B>. = <.C, D>. -> (A e. _V <-> C e. _V))
Theorem	oteqex 3740	Equivalence of existence implied by equality of ordered triples.
|- (<.<.A, B>., C>. = <.<.R, S>., T>. -> (A e. _V <-> R e. _V))
Theorem	opth2 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)
Theorem	opcom 3742	An ordered pair commutes iff its members are equal.
|- A e. _V   =>   |- (<.A, B>. = <.B, A>. <-> A = B)
Theorem	moop2 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>.
Theorem	opeqsn 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}))
Theorem	opeqpr 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})))
Theorem	mosubopt 3746	"At most one" remains true inside ordered pair quantification.
|- (A.yA.zE*xph -> E*xE.yE.z(A = <.y, z>. /\ ph))
Theorem	mosubop 3747	"At most one" remains true inside ordered pair quantification.
|- E*xph   =>   |- E*xE.yE.z(A = <.y, z>. /\ ph)
Theorem	euop2 3748	Transfer existential uniqueness to second member of an ordered pair.
|- (E!xE.y(x = <.A, y>. /\ ph) <-> E!yph)
Theorem	opthwiener 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))
Theorem	uniop 3750	The union of an ordered pair. Theorem 65 of [Suppes] p. 39.
|- U.<.A, B>. = {A, B}
Theorem	uniopel 3751	Ordered pair membership is inherited by class union.
|- (<.A, B>. e. C -> U.<.A, B>. e. U.C)
Ordered-pair class abstractions (cont.)
Theorem	opabid 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)
Theorem	elopab 3753	Membership in a class abstraction of pairs.
|- (A e. {<.x, y>. | ph} <-> E.xE.y(A = <.x, y>. /\ ph))
Theorem	hbopab 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})
Theorem	hbopab1 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})
Theorem	hbopab2 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})
Theorem	opelopabsb 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)
Theorem	brabsb 3758	The law of concretion in terms of substitutions.
|- R = {<.x, y>. | ph}   =>   |- (zRw <-> [w / y][z / x]ph)
Theorem	opelopabt 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))
Theorem	opelopabg 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))
Theorem	brabg 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))
Theorem	opelopab2 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))
Theorem	opelopab 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)
Theorem	brab 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)
Theorem	opelopabf 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)
Theorem	ssopab2 3766	Equivalence of ordered pair abstraction subclass and implication.
|- ({<.x, y>. | ph} C_ {<.x, y>. | ps} <-> A.xA.y(ph -> ps))
Theorem	ssopab2i 3767	Inference of ordered pair abstraction subclass from implication.
|- (ph -> ps)   =>   |- {<.x, y>. | ph} C_ {<.x, y>. | ps}
Theorem	opabn0 3768	Non-empty ordered pair class abstraction.
|- ({<.x, y>. | ph} =/= (/) <-> E.xE.yph)
Power class of union and intersection
Theorem	pwin 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)
Theorem	pwunss 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)
Theorem	pwssun 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))
Theorem	pwundif 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)
Theorem	pwun 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
Syntax	cep 3774	Extend class notation to include the epsilon relation.
class _E
Syntax	cid 3775	Extend the definition of a class to include identity relation.
class _I
Definition	df-eprel 3776	Define the epsilon relation. Similar to Definition 6.22 of [TakeutiZaring] p. 30.
|- _E = {<.x, y>. | x e. y}
Theorem	epelc 3777	The epsilon relation and the membership relation are the same.
|- A e. _V   &   |- B e. _V   =>   |- (A _E B <-> A e. B)
Theorem	epel 3778	The epsilon relation and the membership relation are the same.
|- (x _E y <-> x e. y)
Definition	df-id 3779	Define the identity relation. Definition 9.15 of [Quine] p. 64.
|- _I = {<.x, y>. | x = y}
Theorem	dfid3 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}
Theorem	dfid2 3781	Alternate definition of the identity relation.
|- _I = {<.x, x>. | x = x}
Partial and complete ordering
Syntax	wpo 3782	Extend wff notation to include the strict partial ordering predicate. Read: ' R is a partial order on A.'
wff R Po A
Syntax	wor 3783	Extend wff notation to include the strict complete ordering predicate. Read: ' R orders A.'
wff R Or A
Definition	df-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)))
Theorem	poss 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))
Theorem	poeq1 3786	Equality theorem for partial ordering predicate.
|- (R = S -> (R Po A <-> S Po A))
Theorem	poeq2 3787	Equality theorem for partial ordering predicate.
|- (A = B -> (R Po A <-> R Po B))
Theorem	pocl 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))))
Theorem	poirr 3789	A partial order relation is irreflexive.
|- ((R Po A /\ B e. A) -> -. BRB)
Theorem	potr 3790	A partial order relation is a transitive relation.
|- ((R Po A /\ (B e. A /\ C e. A /\ D e. A)) -> ((BRC /\ CRD) -> BRD))
Theorem	po2nr 3791	A partial order relation has no 2-cycle loops.
|- ((R Po A /\ (B e. A /\ C e. A)) -> -. (BRC /\ CRB))
Theorem	po3nr 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))
Theorem	po0 3793	Any relation is a partial ordering of the empty set. (The proof was shortened by Andrew Salmon, 25-Jul-2011.)
|- R Po (/)
Theorem	posn 3794	Partial ordering of a singleton.
|- (R Po {x} <-> -. <.x, x>. e. R)
Theorem	pofun 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)
Definition	df-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)))
Theorem	sopo 3797	A strict linear order is a strict partial order.
|- (R Or A -> R Po A)
Theorem	soss 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))
Theorem	soeq1 3799	Equality theorem for the strict ordering predicate.
|- (R = S -> (R Or A <-> S Or A))
Theorem	soeq2 3800	Equality theorem for the strict ordering predicate.
|- (A = B -> (R Or A <-> R Or B))