Metamath Proof Explorer - mmtheorems22

Jump to page: 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-5787

Statement List for Metamath Proof Explorer - 2101-2200 - Page 22 of 58

Type	Label	Description
Statement
Theorem	biopabd 2101	Equivalent wff's yield equal ordered-pair class abstractions (deduction rule).
|- (ph -> A.xph)   &   |- (ph -> A.yph)   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> {<.x, y>. | ps} = {<.x, y>. | ch})
Theorem	biopabdv 2102	Equivalent wff's yield equal ordered-pair class abstractions (deduction rule).
|- (ph -> (ps <-> ch))   =>   |- (ph -> {<.x, y>. | ps} = {<.x, y>. | ch})
Theorem	biopabi 2103	Equivalent wff's yield equal class abstractions.
|- (ph <-> ps)   =>   |- {<.x, y>. | ph} = {<.x, y>. | ps}
Theorem	cbvopab 2104	Rule used to change bound variables in an ordered pair abstraction, using implicit substitution.
|- (ph -> A.zph)   &   |- (ph -> A.wph)   &   |- (ps -> A.xps)   &   |- (ps -> A.yps)   &   |- ((x = z /\ y = w) -> (ph <-> ps))   =>   |- {<.x, y>. | ph} = {<.z, w>. | ps}
Theorem	cbvopabv 2105	Rule used to change bound variables in an ordered pair abstraction, using implicit substitution.
|- ((x = z /\ y = w) -> (ph <-> ps))   =>   |- {<.x, y>. | ph} = {<.z, w>. | ps}
Theorem	cbvopab1 2106	Change first bound variable in an ordered pair abstraction, using explicit substitution.
|- (ph -> A.zph)   &   |- (ps -> A.xps)   &   |- (x = z -> (ph <-> ps))   =>   |- {<.x, y>. | ph} = {<.z, y>. | ps}
Theorem	cbvopab1s 2107	Change first bound variable in an ordered pair abstraction, using explicit substitution.
|- {<.x, y>. | ph} = {<.z, y>. | [z / x]ph}
Theorem	cbvopab1v 2108	Rule used to change the first bound variable in an ordered pair abstraction, using implicit substitution.
|- (x = z -> (ph <-> ps))   =>   |- {<.x, y>. | ph} = {<.z, y>. | ps}
Theorem	cbvopab2v 2109	Rule used to change the second bound variable in an ordered pair abstraction, using implicit substitution.
|- (y = z -> (ph <-> ps))   =>   |- {<.x, y>. | ph} = {<.x, z>. | ps}
Theorem	elopab 2110	Membership in a class abstraction of pairs.
|- (A e. {<.x, y>. | ph} <-> E.xE.y(A = <.x, y>. /\ ph))
Theorem	hbopab 2111	Bound-variable hypothesis builder for class abstraction.
|- (ph -> A.zph)   =>   |- (w e. {<.x, y>. | ph} -> A.z w e. {<.x, y>. | ph})
Theorem	hbopab1 2112	The abstraction variables in a class abstraction of pairs are not free.
|- (z e. {<.x, y>. | ph} -> A.x z e. {<.x, y>. | ph})
Theorem	hbopab2 2113	The abstraction variables in a class abstraction of pairs are not free.
|- (z e. {<.x, y>. | ph} -> A.y z e. {<.x, y>. | ph})
Theorem	opabsb 2114	The law of concretion in terms of substitutions.
|- (<.z, w>. e. {<.x, y>. | ph} <-> [w / y][z / x]ph)
Theorem	opelopabg 2115	The law of concretion. Theorem 9.5 of [Quine] p. 61.
|- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   =>   |- ((A e. C /\ B e. D) -> (<.A, B>. e. {<.x, y>. | ph} <-> ch))
Theorem	brabg 2116	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	opelopab 2117	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 2118	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	ssopab2 2119	Equivalence of abstraction subclass and implication.
|- ({<.x, y>. | ph} (_ {<.x, y>. | ps} <-> A.xA.y(ph -> ps))
Theorem	ssopab2i 2120	Inference of abstraction subclass from implication.
|- (ph -> ps)   =>   |- {<.x, y>. | ph} (_ {<.x, y>. | ps}
Theorem	unopab 2121	Union of two ordered pair class abstractions.
|- ({<.x, y>. | ph} u. {<.x, y>. | ps}) = {<.x, y>. | (ph \/ ps)}
Definition	df-eprel 2122	Define the epsilon relation. Similar to Definition 6.22 of [TakeutiZaring] p. 30.
|- E = {<.x, y>. | x e. y}
Theorem	epelc 2123	The epsilon relation and the membership relation are the same.
|- A e. V   &   |- B e. V   =>   |- (AEB <-> A e. B)
Theorem	epel 2124	The epsilon relation and the membership relation are the same.
|- (xEy <-> x e. y)
Definition	df-id 2125	Define the identity relation. Definition 9.15 of [Quine] p. 64.
|- I = {<.x, y>. | x = y}
Theorem	ideqg 2126	For sets, the identity relation is the same as equality.
|- ((A e. C /\ B e. D) -> (AIB <-> A = B))
Theorem	ideq 2127	For sets, the identity relation is the same as equality.
|- A e. V   &   |- B e. V   =>   |- (AIB <-> A = B)
Definition	df-po 2128	Define a partial order relation. 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 2129	Subset theorem for the partial ordering predicate.
|- (A (_ B -> (R Po B -> R Po A))
Theorem	poeq1 2130	Equality theorem for partial ordering predicate.
|- (R = S -> (R Po A <-> S Po A))
Theorem	poeq2 2131	Equality theorem for partial ordering predicate.
|- (A = B -> (R Po A <-> R Po B))
Theorem	pocl 2132	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 2133	A partial order relation is irreflexive.
|- ((R Po A /\ B e. A) -> -. BRB)
Theorem	potr 2134	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 2135	A partial order relation has no 2-cycle loops.
|- ((R Po A /\ (B e. A /\ C e. A)) -> -. (BRC /\ CRB))
Theorem	po3nr 2136	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 2137	Any relation is a partial ordering of the empty set.
|- R Po (/)
Definition	df-so 2138	Define a strict or linear order relation.
|- (R Or A <-> (R Po A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)))
Theorem	sopo 2139	A strict order is a partial order.
|- (R Or A -> R Po A)
Theorem	soss 2140	Subset theorem for the strict ordering predicate.
|- (A (_ B -> (R Or B -> R Or A))
Theorem	soeq1 2141	Equality theorem for the strict ordering predicate.
|- (R = S -> (R Or A <-> S Or A))
Theorem	soeq2 2142	Equality theorem for the strict ordering predicate.
|- (A = B -> (R Or A <-> R Or B))
Theorem	sonr 2143	A strict order relation is irreflexive.
|- ((R Or A /\ B e. A) -> -. BRB)
Theorem	sotr 2144	A strict order relation is a transitive relation.
|- ((R Or A /\ (B e. A /\ C e. A /\ D e. A)) -> ((BRC /\ CRD) -> BRD))
Theorem	solin 2145	A strict order relation is linear (satisfies trichotomy).
|- ((R Or A /\ (B e. A /\ C e. A)) -> (BRC \/ B = C \/ CRB))
Theorem	so2nr 2146	A strict order relation has no 2-cycle loops.
|- ((R Or A /\ (B e. A /\ C e. A)) -> -. (BRC /\ CRB))
Theorem	so3nr 2147	A strict order relation has no 3-cycle loops.
|- ((R Or A /\ (B e. A /\ C e. A /\ D e. A)) -> -. (BRC /\ CRD /\ DRB))
Theorem	sotric 2148	A strict order relation satisfies strict trichotomy.
|- ((R Or A /\ (B e. A /\ C e. A)) -> (BRC <-> -. (B = C \/ CRB)))
Theorem	sotrieq 2149	Trichotomy law for strict order relation.
|- ((R Or A /\ (B e. A /\ C e. A)) -> (B = C <-> -. (BRC \/ CRB)))
Theorem	sotrieq2 2150	Trichotomy law for strict order relation.
|- ((R Or A /\ (B e. A /\ C e. A)) -> (B = C <-> (-. BRC /\ -. CRB)))
Theorem	itlso 2151	A irreflexive, transitive, linear relation is a strict ordering.
|- (x e. A -> -. xRx)   &   |- ((x e. A /\ y e. A /\ z e. A) -> ((xRy /\ yRz) -> xRz))   &   |- ((x e. A /\ y e. A) -> (xRy \/ x = y \/ yRx))   =>   |- R Or A
Theorem	so 2152	Deduce strict ordering from its properties.
|- ((x e. A /\ y e. A /\ z e. A) -> ((xRy <-> -. (x = y \/ yRx)) /\ ((xRy /\ yRz) -> xRz)))   =>   |- R Or A
Theorem	so0 2153	Any relation is a strict ordering of the empty set.
|- R Or (/)
Definition	df-sup 2154	Define the supremum of class B. It is meaningful when R is a relation that strictly orders A and when the supremum exists. For example, R could be 'less than', A could be the set of real numbers, and B could be the set of all positive reals whose square is less