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).
⊢ (φ → ∀xφ)    &   ⊢ (φ → ∀yφ)    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → {⟨x, y⟩∣ψ} = {⟨x, y⟩∣χ})
Theorem	biopabdv 2102	Equivalent wff's yield equal ordered-pair class abstractions (deduction rule).
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → {⟨x, y⟩∣ψ} = {⟨x, y⟩∣χ})
Theorem	biopabi 2103	Equivalent wff's yield equal class abstractions.
⊢ (φ ↔ ψ)    ⇒   ⊢ {⟨x, y⟩∣φ} = {⟨x, y⟩∣ψ}
Theorem	cbvopab 2104	Rule used to change bound variables in an ordered pair abstraction, using implicit substitution.
⊢ (φ → ∀zφ)    &   ⊢ (φ → ∀wφ)    &   ⊢ (ψ → ∀xψ)    &   ⊢ (ψ → ∀yψ)    &   ⊢ ((x = z ∧ y = w) → (φ ↔ ψ))    ⇒   ⊢ {⟨x, y⟩∣φ} = {⟨z, w⟩∣ψ}
Theorem	cbvopabv 2105	Rule used to change bound variables in an ordered pair abstraction, using implicit substitution.
⊢ ((x = z ∧ y = w) → (φ ↔ ψ))    ⇒   ⊢ {⟨x, y⟩∣φ} = {⟨z, w⟩∣ψ}
Theorem	cbvopab1 2106	Change first bound variable in an ordered pair abstraction, using explicit substitution.
⊢ (φ → ∀zφ)    &   ⊢ (ψ → ∀xψ)    &   ⊢ (x = z → (φ ↔ ψ))    ⇒   ⊢ {⟨x, y⟩∣φ} = {⟨z, y⟩∣ψ}
Theorem	cbvopab1s 2107	Change first bound variable in an ordered pair abstraction, using explicit substitution.
⊢ {⟨x, y⟩∣φ} = {⟨z, y⟩∣[z / x]φ}
Theorem	cbvopab1v 2108	Rule used to change the first bound variable in an ordered pair abstraction, using implicit substitution.
⊢ (x = z → (φ ↔ ψ))    ⇒   ⊢ {⟨x, y⟩∣φ} = {⟨z, y⟩∣ψ}
Theorem	cbvopab2v 2109	Rule used to change the second bound variable in an ordered pair abstraction, using implicit substitution.
⊢ (y = z → (φ ↔ ψ))    ⇒   ⊢ {⟨x, y⟩∣φ} = {⟨x, z⟩∣ψ}
Theorem	elopab 2110	Membership in a class abstraction of pairs.
⊢ (A ∈ {⟨x, y⟩∣φ} ↔ ∃x∃y(A = ⟨x, y⟩ ∧ φ))
Theorem	hbopab 2111	Bound-variable hypothesis builder for class abstraction.
⊢ (φ → ∀zφ)    ⇒   ⊢ (w ∈ {⟨x, y⟩∣φ} → ∀z w ∈ {⟨x, y⟩∣φ})
Theorem	hbopab1 2112	The abstraction variables in a class abstraction of pairs are not free.
⊢ (z ∈ {⟨x, y⟩∣φ} → ∀x z ∈ {⟨x, y⟩∣φ})
Theorem	hbopab2 2113	The abstraction variables in a class abstraction of pairs are not free.
⊢ (z ∈ {⟨x, y⟩∣φ} → ∀y z ∈ {⟨x, y⟩∣φ})
Theorem	opabsb 2114	The law of concretion in terms of substitutions.
⊢ (⟨z, w⟩ ∈ {⟨x, y⟩∣φ} ↔ [w / y][z / x]φ)
Theorem	opelopabg 2115	The law of concretion. Theorem 9.5 of [Quine] p. 61.
⊢ (x = A → (φ ↔ ψ))    &   ⊢ (y = B → (ψ ↔ χ))    ⇒   ⊢ ((A ∈ C ∧ B ∈ D) → (⟨A, B⟩ ∈ {⟨x, y⟩∣φ} ↔ χ))
Theorem	brabg 2116	The law of concretion for a binary relation.
⊢ (x = A → (φ ↔ ψ))    &   ⊢ (y = B → (ψ ↔ χ))    &   ⊢ R = {⟨x, y⟩∣φ}    ⇒   ⊢ ((A ∈ C ∧ B ∈ D) → (ARB ↔ χ))
Theorem	opelopab 2117	The law of concretion. Theorem 9.5 of [Quine] p. 61.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ (x = A → (φ ↔ ψ))    &   ⊢ (y = B → (ψ ↔ χ))    ⇒   ⊢ (⟨A, B⟩ ∈ {⟨x, y⟩∣φ} ↔ χ)
Theorem	brab 2118	The law of concretion for a binary relation.
⊢ A ∈ V    &   ⊢ B ∈ V    &   ⊢ (x = A → (φ ↔ ψ))    &   ⊢ (y = B → (ψ ↔ χ))    &   ⊢ R = {⟨x, y⟩∣φ}    ⇒   ⊢ (ARB ↔ χ)
Theorem	ssopab2 2119	Equivalence of abstraction subclass and implication.
⊢ ({⟨x, y⟩∣φ} ⊆ {⟨x, y⟩∣ψ} ↔ ∀x∀y(φ → ψ))
Theorem	ssopab2i 2120	Inference of abstraction subclass from implication.
⊢ (φ → ψ)    ⇒   ⊢ {⟨x, y⟩∣φ} ⊆ {⟨x, y⟩∣ψ}
Theorem	unopab 2121	Union of two ordered pair class abstractions.
⊢ ({⟨x, y⟩∣φ} ∪ {⟨x, y⟩∣ψ}) = {⟨x, y⟩∣(φ ∨ ψ)}
Definition	df-eprel 2122	Define the epsilon relation. Similar to Definition 6.22 of [TakeutiZaring] p. 30.
⊢ E = {⟨x, y⟩∣x ∈ y}
Theorem	epelc 2123	The epsilon relation and the membership relation are the same.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (AEB ↔ A ∈ B)
Theorem	epel 2124	The epsilon relation and the membership relation are the same.
⊢ (xEy ↔ x ∈ 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 ∈ C ∧ B ∈ D) → (AIB ↔ A = B))
Theorem	ideq 2127	For sets, the identity relation is the same as equality.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (AIB ↔ A = B)
Definition	df-po 2128	Define a partial order relation. Definition of [Enderton] p. 168.
⊢ (R Po A ↔ ∀x ∈ A ∀y ∈ A ∀z ∈ 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 ∈ A ∧ C ∈ A ∧ D ∈ A) → (¬ BRB ∧ ((BRC ∧ CRD) → BRD))))
Theorem	poirr 2133	A partial order relation is irreflexive.
⊢ ((R Po A ∧ B ∈ A) → ¬ BRB)
Theorem	potr 2134	A partial order relation is a transitive relation.
⊢ ((R Po A ∧ (B ∈ A ∧ C ∈ A ∧ D ∈ A)) → ((BRC ∧ CRD) → BRD))
Theorem	po2nr 2135	A partial order relation has no 2-cycle loops.
⊢ ((R Po A ∧ (B ∈ A ∧ C ∈ A)) → ¬ (BRC ∧ CRB))
Theorem	po3nr 2136	A partial order relation has no 3-cycle loops.
⊢ ((R Po A ∧ (B ∈ A ∧ C ∈ A ∧ D ∈ 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 ∧ ∀x ∈ A ∀y ∈ 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 ∈ A) → ¬ BRB)
Theorem	sotr 2144	A strict order relation is a transitive relation.
⊢ ((R Or A ∧ (B ∈ A ∧ C ∈ A ∧ D ∈ A)) → ((BRC ∧ CRD) → BRD))
Theorem	solin 2145	A strict order relation is linear (satisfies trichotomy).
⊢ ((R Or A ∧ (B ∈ A ∧ C ∈ A)) → (BRC ∨ B = C ∨ CRB))
Theorem	so2nr 2146	A strict order relation has no 2-cycle loops.
⊢ ((R Or A ∧ (B ∈ A ∧ C ∈ A)) → ¬ (BRC ∧ CRB))
Theorem	so3nr 2147	A strict order relation has no 3-cycle loops.
⊢ ((R Or A ∧ (B ∈ A ∧ C ∈ A ∧ D ∈ A)) → ¬ (BRC ∧ CRD ∧ DRB))
Theorem	sotric 2148	A strict order relation satisfies strict trichotomy.
⊢ ((R Or A ∧ (B ∈ A ∧ C ∈ A)) → (BRC ↔ ¬ (B = C ∨ CRB)))
Theorem	sotrieq 2149	Trichotomy law for strict order relation.
⊢ ((R Or A ∧ (B ∈ A ∧ C ∈ A)) → (B = C ↔ ¬ (BRC ∨ CRB)))
Theorem	sotrieq2 2150	Trichotomy law for strict order relation.
⊢ ((R Or A ∧ (B ∈ A ∧ C ∈ A)) → (B = C ↔ (¬ BRC ∧ ¬ CRB)))
Theorem	itlso 2151	A irreflexive, transitive, linear relation is a strict ordering.
⊢ (x ∈ A → ¬ xRx)    &   ⊢ ((x ∈ A ∧ y ∈ A ∧ z ∈ A) → ((xRy ∧ yRz) → xRz))    &   ⊢ ((x ∈ A ∧ y ∈ A) → (xRy ∨ x = y ∨ yRx))    ⇒   ⊢ R Or A
Theorem	so 2152	Deduce strict ordering from its properties.
⊢ ((x ∈ A ∧ y ∈ A ∧ z ∈ 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 than 2; in this case the supremum is defined as the square root of 2 per sqrval 4729.
⊢ sup(B, A, R) = ∪{x ∈ A∣(∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ B yRz))}
Theorem	supeq1 2155	Equality theorem for supremum.
⊢ (B = C → sup(B, A, R) = sup(C, A, R))
Theorem	supmo 2156	Any class B has at most one supremum in A (where R is interpreted as 'less than').
⊢ R Or A    ⇒   ⊢ ∃*x(x ∈ A ∧ (∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ B yRz)))
Theorem	supex 2157	A supremum is a set.
⊢ R Or A    ⇒   ⊢ sup(B, A, R) ∈ V
Theorem	supeu 2158	A supremum is unique. Similar to Theorem I.26 of [Apostol] p. 24 (but for supremums in general).
⊢ R Or A    ⇒   ⊢ (∃x ∈ A (∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ B yRz)) → ∃!x ∈ A (∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ B yRz)))
Theorem	supcl 2159	A supremum belongs to its base class (closure law).
⊢ R Or A    ⇒   ⊢ (∃x ∈ A (∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ B yRz)) → sup(B, A, R) ∈ A)
Theorem	supub 2160	A supremum is an upper bound.
⊢ R Or A    ⇒   ⊢ (∃x ∈ A (∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ B yRz)) → (C ∈ B → ¬ sup(B, A, R)RC))
Theorem	suplub 2161	A supremum is the least upper bound.
⊢ R Or A    ⇒   ⊢ (∃x ∈ A (∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ B yRz)) → ((C ∈ A ∧ CRsup(B, A, R)) → ∃z ∈ B CRz))
Theorem	supnub 2162	An upper bound is not less than the supremum.
⊢ R Or A    ⇒   ⊢ (∃x ∈ A (∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ B yRz)) → ((C ∈ A ∧ ∀z ∈ B ¬ CRz) → ¬ CRsup(B, A, R)))
Theorem	supeui 2163	A supremum is unique. Similar to Theorem I.26 of [Apostol] p. 24 (but for supremums in general).
⊢ R Or A    &   ⊢ ∃x ∈ A (∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ B yRz))    ⇒   ⊢ ∃!x ∈ A (∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ B yRz))
Theorem	supcli 2164	A supremum belongs to its base class (closure law).
⊢ R Or A    &   ⊢ ∃x ∈ A (∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ B yRz))    ⇒   ⊢ sup(B, A, R) ∈ A
Theorem	supubi 2165	A supremum is an upper bound.
⊢ R Or A    &   ⊢ ∃x ∈ A (∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ B yRz))    ⇒   ⊢ (C ∈ B → ¬ sup(B, A, R)RC)
Theorem	suplubi 2166	A supremum is the least upper bound.
⊢ R Or A    &   ⊢ ∃x ∈ A (∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ B yRz))    ⇒   ⊢ ((C ∈ A ∧ CRsup(B, A, R)) → ∃z ∈ B CRz)
Theorem	supnubi 2167	An upper bound is not less than the supremum.
⊢ R Or A    &   ⊢ ∃x ∈ A (∀y ∈ B ¬ xRy ∧ ∀y ∈ A (yRx → ∃z ∈ B yRz))    ⇒   ⊢ ((C ∈ A ∧ ∀z ∈ B ¬ CRz) → ¬ CRsup(B, A, R))
Theorem	supsn 2168	The supremum of a singleton.
⊢ R Or A    ⇒   ⊢ (B ∈ A → sup({B}, A, R) = B)
Definition	df-fr 2169	Define a founded relation. For alternate definitions, see dffr2 2171 and dffr3 2620.
⊢ (R Fr A ↔ ∀x((x ⊆ A ∧ ¬ x = ∅) → ∃y ∈ x ∀z ∈ x ¬ zRy))
Theorem	fri 2170	Property of founded relation (one direction of definition).
⊢ B ∈ V    ⇒   ⊢ ((R Fr A ∧ (B ⊆ A ∧ ¬ B = ∅)) → ∃x ∈ B ∀y ∈ B ¬ yRx)
Theorem	dffr2 2171	Alternate definition of founded relation. Similar to Definition 6.21 of [TakeutiZaring] p. 30.
⊢ (R Fr A ↔ ∀x((x ⊆ A ∧ ¬ x = ∅) → ∃y ∈ x (x ∩ {z∣zRy}) = ∅))
Theorem	frc 2172	Property of founded relation (one direction of definition using class variables).
⊢ B ∈ V    ⇒   ⊢ (R Fr A → ((B ⊆ A ∧ ¬ B = ∅) → ∃x ∈ B (B ∩ {y∣yRx}) = ∅))
Theorem	frss 2173	Subset theorem for the founded predicate. Exercise 1 of [TakeutiZaring] p. 31.
⊢ (A ⊆ B → (R Fr B → R Fr A))
Theorem	freq1 2174	Equality theorem for the founded predicate.
⊢ (R = S → (R Fr A ↔ S Fr A))
Theorem	freq2 2175	Equality theorem for the founded predicate.
⊢ (A = B → (R Fr A ↔ R Fr B))
Theorem	frirr 2176	A founded relation is irreflexive. Special case of Proposition 6.23 of [TakeutiZaring] p. 30.
⊢ ((R Fr A ∧ x ∈ A) → ¬ xRx)
Theorem	fr2nr 2177	A founded relation has no 2-cycle loops. Special case of Proposition 6.23 of [TakeutiZaring] p. 30.
⊢ ((R Fr A ∧ (x ∈ A ∧ y ∈ A)) → ¬ (xRy ∧ yRx))
Theorem	fr3nr 2178	A founded relation has no 3-cycle loops. Special case of Proposition 6.23 of [TakeutiZaring] p. 30.
⊢ ((R Fr A ∧ (x ∈ A ∧ y ∈ A ∧ z ∈ A)) → ¬ (xRy ∧ yRz ∧ zRx))
Theorem	fr0 2179	Any relation is founded on the empty set.
⊢ R Fr ∅
Theorem	efrirr 2180	Irreflexivitiy of the epsilon relation: a class founded by epsilon is not a member of itself.
⊢ (E Fr A → ¬ A ∈ A)
Theorem	efrn2lp 2181	A set founded by epsilon contains no 2-cycle loops.
⊢ ((E Fr A ∧ (x ∈ A ∧ y ∈ A)) → ¬ (x ∈ y ∧ y ∈ x))
Theorem	epne3 2182	A set founded by epsilon contains no 3-cycle loops.
⊢ ((E Fr A ∧ (x ∈ A ∧ y ∈ A ∧ z ∈ A)) → ¬ (x ∈ y ∧ y ∈ z ∧ z ∈ x))
Theorem	tz7.2 2183	Similar to Theorem 7.2 of [TakeutiZaring] p. 35, of except that the Axiom of Regularity is not required due to antecedent E Fr A.
⊢ (((Tr A ∧ E Fr A) ∧ B ∈ A) → (B ⊆ A ∧ ¬ B = A))
Theorem	dfepfr 2184	A simpler way of saying that the epsilon relation is founded.
⊢ (E Fr A ↔ ∀x((x ⊆ A ∧ ¬ x = ∅) → ∃y ∈ x (x ∩ y) = ∅))
Theorem	epfrc 2185	A subset of an epsilon-founded class has a minimal element.
⊢ B ∈ V    ⇒   ⊢ ((E Fr A ∧ (B ⊆ A ∧ ¬ B = ∅)) → ∃x ∈ B (B ∩ x) = ∅)
Definition	df-we 2186	Define a well-ordering. For an alternate definition see dfwe2 2187.
⊢ (R We A ↔ (R Fr A ∧ R Or A))
Theorem	dfwe2 2187	Alternate definition of well-ordering. Definition 6.24(2) of [TakeutiZaring] p. 30.
⊢ (R We A ↔ (R Fr A ∧ ∀x ∈ A ∀y ∈ A (xRy ∨ x = y ∨ yRx)))
Theorem	wess 2188	Subset theorem for the well-ordering predicate. Exercise 4 of [TakeutiZaring] p. 31.
⊢ (A ⊆ B → (R We B → R We A))
Theorem	weeq1 2189	Equality theorem for the well-ordering predicate.
⊢ (R = S → (R We A ↔ S We A))
Theorem	weeq2 2190	Equality theorem for the well-ordering predicate.
⊢ (A = B → (R We A ↔ R We B))
Theorem	wefr 2191	A well-ordering is founded.
⊢ (R We A → R Fr A)
Theorem	weso 2192	A well-ordering is a strict ordering.
⊢ (R We A → R Or A)
Theorem	wecmpep 2193	The elements of an epsilon well-ordering are comparable.
⊢ ((E We A ∧ (x ∈ A ∧ y ∈ A)) → (x ∈ y ∨ x = y ∨ y ∈ x))
Theorem	wetrep 2194	An epsilon well-ordering is a transitive relation.
⊢ ((E We A ∧ (x ∈ A ∧ y ∈ A ∧ z ∈ A)) → ((x ∈ y ∧ y ∈ z) → x ∈ z))
Theorem	wefrc 2195	A non-empty (possibly proper) subclass of a class well-ordered by E has a minimal element. Special case of Proposition 6.26 of [TakeutiZaring] p. 31.
⊢ ((E We A ∧ (B ⊆ A ∧ ¬ B = ∅)) → ∃x ∈ B (B ∩ x) = ∅)
Theorem	we0 2196	Any relation is a well-ordering of the empty set.
⊢ R We ∅
Theorem	wereu 2197	A subset of a well-ordered set has a unique minimal element.
⊢ B ∈ V    ⇒   ⊢ ((R We A ∧ (B ⊆ A ∧ ¬ B = ∅)) → ∃!x ∈ B ∀y ∈ B ¬ yRx)
Syntax	word 2198	Extend the definition of a wff to include the ordinal predicate.
wff Ord A
Syntax	con0 2199	Extend the definition of a class to include the class of all ordinals. (The 0 in the name prevents creating a file called con.html, which causes problems in Windows.)
class On
Syntax	wlim 2200	Extend the definition of a wff to include the limit ordinal predicate.
wff Lim A