 Home Intuitionistic Logic ExplorerTheorem List (p. 41 of 95) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 4001-4100   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremopelopabaf 4001* The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 3999 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by Mario Carneiro, 19-Dec-2013.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
xψ    &   yψ    &   A V    &   B V    &   ((x = A y = B) → (φψ))       (⟨A, B {⟨x, y⟩ ∣ φ} ↔ ψ)

Theoremopelopabf 4002* The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 3999 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by NM, 19-Dec-2008.)
xψ    &   yχ    &   A V    &   B V    &   (x = A → (φψ))    &   (y = B → (ψχ))       (⟨A, B {⟨x, y⟩ ∣ φ} ↔ χ)

Theoremssopab2 4003 Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 19-May-2013.)
(xy(φψ) → {⟨x, y⟩ ∣ φ} ⊆ {⟨x, y⟩ ∣ ψ})

Theoremssopab2b 4004 Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
({⟨x, y⟩ ∣ φ} ⊆ {⟨x, y⟩ ∣ ψ} ↔ xy(φψ))

Theoremssopab2i 4005 Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 5-Apr-1995.)
(φψ)       {⟨x, y⟩ ∣ φ} ⊆ {⟨x, y⟩ ∣ ψ}

Theoremssopab2dv 4006* Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 19-Jan-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
(φ → (ψχ))       (φ → {⟨x, y⟩ ∣ ψ} ⊆ {⟨x, y⟩ ∣ χ})

Theoremeqopab2b 4007 Equivalence of ordered pair abstraction equality and biconditional. (Contributed by Mario Carneiro, 4-Jan-2017.)
({⟨x, y⟩ ∣ φ} = {⟨x, y⟩ ∣ ψ} ↔ xy(φψ))

Theoremopabm 4008* Inhabited ordered pair class abstraction. (Contributed by Jim Kingdon, 29-Sep-2018.)
(z z {⟨x, y⟩ ∣ φ} ↔ xyφ)

Theoremiunopab 4009* Move indexed union inside an ordered-pair abstraction. (Contributed by Stefan O'Rear, 20-Feb-2015.)
z A {⟨x, y⟩ ∣ φ} = {⟨x, y⟩ ∣ z A φ}

2.3.5  Power class of union and intersection

Theorempwin 4010 The power class of the intersection of two classes is the intersection of their power classes. Exercise 4.12(j) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.)
𝒫 (AB) = (𝒫 A ∩ 𝒫 B)

Theorempwunss 4011 The power class of the union of two classes includes the union of their power classes. Exercise 4.12(k) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.)
(𝒫 A ∪ 𝒫 B) ⊆ 𝒫 (AB)

Theorempwssunim 4012 The power class of the union of two classes is a subset of the union of their power classes, if one class is a subclass of the other. One direction of Exercise 4.12(l) of [Mendelson] p. 235. (Contributed by Jim Kingdon, 30-Sep-2018.)
((AB BA) → 𝒫 (AB) ⊆ (𝒫 A ∪ 𝒫 B))

Theorempwundifss 4013 Break up the power class of a union into a union of smaller classes. (Contributed by Jim Kingdon, 30-Sep-2018.)
((𝒫 (AB) ∖ 𝒫 A) ∪ 𝒫 A) ⊆ 𝒫 (AB)

Theorempwunim 4014 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. (Contributed by Jim Kingdon, 30-Sep-2018.)
((AB BA) → 𝒫 (AB) = (𝒫 A ∪ 𝒫 B))

2.3.6  Epsilon and identity relations

Syntaxcep 4015 Extend class notation to include the epsilon relation.
class E

Syntaxcid 4016 Extend the definition of a class to include identity relation.
class I

Definitiondf-eprel 4017* Define the epsilon relation. Similar to Definition 6.22 of [TakeutiZaring] p. 30. The epsilon relation and set membership are the same, that is, (A E BA B) when B is a set by epelg 4018. Thus, 5 E { 1 , 5 }. (Contributed by NM, 13-Aug-1995.)
E = {⟨x, y⟩ ∣ x y}

Theoremepelg 4018 The epsilon relation and membership are the same. General version of epel 4020. (Contributed by Scott Fenton, 27-Mar-2011.) (Revised by Mario Carneiro, 28-Apr-2015.)
(B 𝑉 → (A E BA B))

Theoremepelc 4019 The epsilon relationship and the membership relation are the same. (Contributed by Scott Fenton, 11-Apr-2012.)
B V       (A E BA B)

Theoremepel 4020 The epsilon relation and the membership relation are the same. (Contributed by NM, 13-Aug-1995.)
(x E yx y)

Definitiondf-id 4021* Define the identity relation. Definition 9.15 of [Quine] p. 64. For example, 5 I 5 and ¬ 4 I 5. (Contributed by NM, 13-Aug-1995.)
I = {⟨x, y⟩ ∣ x = y}

2.3.7  Partial and complete ordering

Syntaxwpo 4022 Extend wff notation to include the strict partial ordering predicate. Read: ' 𝑅 is a partial order on A.'
wff 𝑅 Po A

Syntaxwor 4023 Extend wff notation to include the strict linear ordering predicate. Read: ' 𝑅 orders A.'
wff 𝑅 Or A

Definitiondf-po 4024* Define the strict partial order predicate. Definition of [Enderton] p. 168. The expression 𝑅 Po A means 𝑅 is a partial order on A. (Contributed by NM, 16-Mar-1997.)
(𝑅 Po Ax A y A z Ax𝑅x ((x𝑅y y𝑅z) → x𝑅z)))

Definitiondf-iso 4025* Define the strict linear order predicate. The expression 𝑅 Or A is true if relationship 𝑅 orders A. The property x𝑅y → (x𝑅z z𝑅y) is called weak linearity by Proposition 11.2.3 of [HoTT], p. (varies). If we assumed excluded middle, it would be equivalent to trichotomy, x𝑅y x = y y𝑅x. (Contributed by NM, 21-Jan-1996.) (Revised by Jim Kingdon, 4-Oct-2018.)
(𝑅 Or A ↔ (𝑅 Po A x A y A z A (x𝑅y → (x𝑅z z𝑅y))))

Theoremposs 4026 Subset theorem for the partial ordering predicate. (Contributed by NM, 27-Mar-1997.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
(AB → (𝑅 Po B𝑅 Po A))

Theorempoeq1 4027 Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
(𝑅 = 𝑆 → (𝑅 Po A𝑆 Po A))

Theorempoeq2 4028 Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
(A = B → (𝑅 Po A𝑅 Po B))

Theoremnfpo 4029 Bound-variable hypothesis builder for partial orders. (Contributed by Stefan O'Rear, 20-Jan-2015.)
x𝑅    &   xA       x 𝑅 Po A

Theoremnfso 4030 Bound-variable hypothesis builder for total orders. (Contributed by Stefan O'Rear, 20-Jan-2015.)
x𝑅    &   xA       x 𝑅 Or A

Theorempocl 4031 Properties of partial order relation in class notation. (Contributed by NM, 27-Mar-1997.)
(𝑅 Po A → ((B A 𝐶 A 𝐷 A) → (¬ B𝑅B ((B𝑅𝐶 𝐶𝑅𝐷) → B𝑅𝐷))))

Theoremispod 4032* Sufficient conditions for a partial order. (Contributed by NM, 9-Jul-2014.)
((φ x A) → ¬ x𝑅x)    &   ((φ (x A y A z A)) → ((x𝑅y y𝑅z) → x𝑅z))       (φ𝑅 Po A)

Theoremswopolem 4033* Perform the substitutions into the strict weak ordering law. (Contributed by Mario Carneiro, 31-Dec-2014.)
((φ (x A y A z A)) → (x𝑅y → (x𝑅z z𝑅y)))       ((φ (𝑋 A 𝑌 A 𝑍 A)) → (𝑋𝑅𝑌 → (𝑋𝑅𝑍 𝑍𝑅𝑌)))

Theoremswopo 4034* A strict weak order is a partial order. (Contributed by Mario Carneiro, 9-Jul-2014.)
((φ (y A z A)) → (y𝑅z → ¬ z𝑅y))    &   ((φ (x A y A z A)) → (x𝑅y → (x𝑅z z𝑅y)))       (φ𝑅 Po A)

Theorempoirr 4035 A partial order relation is irreflexive. (Contributed by NM, 27-Mar-1997.)
((𝑅 Po A B A) → ¬ B𝑅B)

Theorempotr 4036 A partial order relation is a transitive relation. (Contributed by NM, 27-Mar-1997.)
((𝑅 Po A (B A 𝐶 A 𝐷 A)) → ((B𝑅𝐶 𝐶𝑅𝐷) → B𝑅𝐷))

Theorempo2nr 4037 A partial order relation has no 2-cycle loops. (Contributed by NM, 27-Mar-1997.)
((𝑅 Po A (B A 𝐶 A)) → ¬ (B𝑅𝐶 𝐶𝑅B))

Theorempo3nr 4038 A partial order relation has no 3-cycle loops. (Contributed by NM, 27-Mar-1997.)
((𝑅 Po A (B A 𝐶 A 𝐷 A)) → ¬ (B𝑅𝐶 𝐶𝑅𝐷 𝐷𝑅B))

Theorempo0 4039 Any relation is a partial ordering of the empty set. (Contributed by NM, 28-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
𝑅 Po ∅

Theorempofun 4040* A function preserves a partial order relation. (Contributed by Jeff Madsen, 18-Jun-2011.)
𝑆 = {⟨x, y⟩ ∣ 𝑋𝑅𝑌}    &   (x = y𝑋 = 𝑌)       ((𝑅 Po B x A 𝑋 B) → 𝑆 Po A)

Theoremsopo 4041 A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997.)
(𝑅 Or A𝑅 Po A)

Theoremsoss 4042 Subset theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(AB → (𝑅 Or B𝑅 Or A))

Theoremsoeq1 4043 Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
(𝑅 = 𝑆 → (𝑅 Or A𝑆 Or A))

Theoremsoeq2 4044 Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
(A = B → (𝑅 Or A𝑅 Or B))

Theoremsonr 4045 A strict order relation is irreflexive. (Contributed by NM, 24-Nov-1995.)
((𝑅 Or A B A) → ¬ B𝑅B)

Theoremsotr 4046 A strict order relation is a transitive relation. (Contributed by NM, 21-Jan-1996.)
((𝑅 Or A (B A 𝐶 A 𝐷 A)) → ((B𝑅𝐶 𝐶𝑅𝐷) → B𝑅𝐷))

Theoremissod 4047* An irreflexive, transitive, trichotomous relation is a linear ordering (in the sense of df-iso 4025). (Contributed by NM, 21-Jan-1996.) (Revised by Mario Carneiro, 9-Jul-2014.)
(φ𝑅 Po A)    &   ((φ (x A y A)) → (x𝑅y x = y y𝑅x))       (φ𝑅 Or A)

Theoremsowlin 4048 A strict order relation satisfies weak linearity. (Contributed by Jim Kingdon, 6-Oct-2018.)
((𝑅 Or A (B A 𝐶 A 𝐷 A)) → (B𝑅𝐶 → (B𝑅𝐷 𝐷𝑅𝐶)))

Theoremso2nr 4049 A strict order relation has no 2-cycle loops. (Contributed by NM, 21-Jan-1996.)
((𝑅 Or A (B A 𝐶 A)) → ¬ (B𝑅𝐶 𝐶𝑅B))

Theoremso3nr 4050 A strict order relation has no 3-cycle loops. (Contributed by NM, 21-Jan-1996.)
((𝑅 Or A (B A 𝐶 A 𝐷 A)) → ¬ (B𝑅𝐶 𝐶𝑅𝐷 𝐷𝑅B))

Theoremsotricim 4051 One direction of sotritric 4052 holds for all weakly linear orders. (Contributed by Jim Kingdon, 28-Sep-2019.)
((𝑅 Or A (B A 𝐶 A)) → (B𝑅𝐶 → ¬ (B = 𝐶 𝐶𝑅B)))

Theoremsotritric 4052 A trichotomy relationship, given a trichotomous order. (Contributed by Jim Kingdon, 28-Sep-2019.)
𝑅 Or A    &   ((B A 𝐶 A) → (B𝑅𝐶 B = 𝐶 𝐶𝑅B))       ((B A 𝐶 A) → (B𝑅𝐶 ↔ ¬ (B = 𝐶 𝐶𝑅B)))

Theoremsotritrieq 4053 A trichotomy relationship, given a trichotomous order. (Contributed by Jim Kingdon, 13-Dec-2019.)
𝑅 Or A    &   ((B A 𝐶 A) → (B𝑅𝐶 B = 𝐶 𝐶𝑅B))       ((B A 𝐶 A) → (B = 𝐶 ↔ ¬ (B𝑅𝐶 𝐶𝑅B)))

Theoremso0 4054 Any relation is a strict ordering of the empty set. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
𝑅 Or ∅

2.3.8  Set-like relations

Syntaxwse 4055 Extend wff notation to include the set-like predicate. Read: ' 𝑅 is set-like on A.'
wff 𝑅 Se A

Definitiondf-se 4056* Define the set-like predicate. (Contributed by Mario Carneiro, 19-Nov-2014.)
(𝑅 Se Ax A {y Ay𝑅x} V)

Theoremseex 4057* The 𝑅-preimage of an element of the base set in a set-like relation is a set. (Contributed by Mario Carneiro, 19-Nov-2014.)
((𝑅 Se A B A) → {x Ax𝑅B} V)

Theoremexse 4058 Any relation on a set is set-like on it. (Contributed by Mario Carneiro, 22-Jun-2015.)
(A 𝑉𝑅 Se A)

Theoremsess1 4059 Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
(𝑅𝑆 → (𝑆 Se A𝑅 Se A))

Theoremsess2 4060 Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
(AB → (𝑅 Se B𝑅 Se A))

Theoremseeq1 4061 Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
(𝑅 = 𝑆 → (𝑅 Se A𝑆 Se A))

Theoremseeq2 4062 Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
(A = B → (𝑅 Se A𝑅 Se B))

Theoremnfse 4063 Bound-variable hypothesis builder for set-like relations. (Contributed by Mario Carneiro, 24-Jun-2015.) (Revised by Mario Carneiro, 14-Oct-2016.)
x𝑅    &   xA       x 𝑅 Se A

Theoremepse 4064 The epsilon relation is set-like on any class. (This is the origin of the term "set-like": a set-like relation "acts like" the epsilon relation of sets and their elements.) (Contributed by Mario Carneiro, 22-Jun-2015.)
E Se A

2.3.9  Ordinals

Syntaxword 4065 Extend the definition of a wff to include the ordinal predicate.
wff Ord A

Syntaxcon0 4066 Extend the definition of a class to include the class of all ordinal numbers. (The 0 in the name prevents creating a file called con.html, which causes problems in Windows.)
class On

Syntaxwlim 4067 Extend the definition of a wff to include the limit ordinal predicate.
wff Lim A

Syntaxcsuc 4068 Extend class notation to include the successor function.
class suc A

Definitiondf-iord 4069* Define the ordinal predicate, which is true for a class that is transitive and whose elements are transitive. Definition of ordinal in [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic". (Contributed by Jim Kingdon, 10-Oct-2018.) Use its alias dford3 4070 instead for naming consistency with set.mm. (New usage is discouraged.)
(Ord A ↔ (Tr A x A Tr x))

Theoremdford3 4070* Alias for df-iord 4069. Use it instead of df-iord 4069 for naming consistency with set.mm. (Contributed by Jim Kingdon, 10-Oct-2018.)
(Ord A ↔ (Tr A x A Tr x))

Definitiondf-on 4071 Define the class of all ordinal numbers. Definition 7.11 of [TakeutiZaring] p. 38. (Contributed by NM, 5-Jun-1994.)
On = {x ∣ Ord x}

Definitiondf-ilim 4072 Define the limit ordinal predicate, which is true for an ordinal that has the empty set as an element and is not a successor (i.e. that is the union of itself). Our definition combines the definition of Lim of [BellMachover] p. 471 and Exercise 1 of [TakeutiZaring] p. 42, and then changes A ≠ ∅ to A (which would be equivalent given the law of the excluded middle, but which is not for us). (Contributed by Jim Kingdon, 11-Nov-2018.) Use its alias dflim2 4073 instead for naming consistency with set.mm. (New usage is discouraged.)
(Lim A ↔ (Ord A A A = A))

Theoremdflim2 4073 Alias for df-ilim 4072. Use it instead of df-ilim 4072 for naming consistency with set.mm. (Contributed by NM, 4-Nov-2004.)
(Lim A ↔ (Ord A A A = A))

Definitiondf-suc 4074 Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1". Definition 7.22 of [TakeutiZaring] p. 41, who use "+ 1" to denote this function. Our definition is a generalization to classes. Although it is not conventional to use it with proper classes, it has no effect on a proper class (sucprc 4115). Some authors denote the successor operation with a prime (apostrophe-like) symbol, such as Definition 6 of [Suppes] p. 134 and the definition of successor in [Mendelson] p. 246 (who uses the symbol "Suc" as a predicate to mean "is a successor ordinal"). The definition of successor of [Enderton] p. 68 denotes the operation with a plus-sign superscript. (Contributed by NM, 30-Aug-1993.)
suc A = (A ∪ {A})

Theoremordeq 4075 Equality theorem for the ordinal predicate. (Contributed by NM, 17-Sep-1993.)
(A = B → (Ord A ↔ Ord B))

Theoremelong 4076 An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
(A 𝑉 → (A On ↔ Ord A))

Theoremelon 4077 An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
A V       (A On ↔ Ord A)

Theoremeloni 4078 An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.)
(A On → Ord A)

Theoremelon2 4079 An ordinal number is an ordinal set. (Contributed by NM, 8-Feb-2004.)
(A On ↔ (Ord A A V))

Theoremlimeq 4080 Equality theorem for the limit predicate. (Contributed by NM, 22-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(A = B → (Lim A ↔ Lim B))

Theoremordtr 4081 An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.)
(Ord A → Tr A)

Theoremordelss 4082 An element of an ordinal class is a subset of it. (Contributed by NM, 30-May-1994.)
((Ord A B A) → BA)

Theoremtrssord 4083 A transitive subclass of an ordinal class is ordinal. (Contributed by NM, 29-May-1994.)
((Tr A AB Ord B) → Ord A)

Theoremordelord 4084 An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. (Contributed by NM, 23-Apr-1994.)
((Ord A B A) → Ord B)

Theoremtron 4085 The class of all ordinal numbers is transitive. (Contributed by NM, 4-May-2009.)
Tr On

Theoremordelon 4086 An element of an ordinal class is an ordinal number. (Contributed by NM, 26-Oct-2003.)
((Ord A B A) → B On)

Theoremonelon 4087 An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of [BellMachover] p. 469. (Contributed by NM, 26-Oct-2003.)
((A On B A) → B On)

Theoremordin 4088 The intersection of two ordinal classes is ordinal. Proposition 7.9 of [TakeutiZaring] p. 37. (Contributed by NM, 9-May-1994.)
((Ord A Ord B) → Ord (AB))

Theoremonin 4089 The intersection of two ordinal numbers is an ordinal number. (Contributed by NM, 7-Apr-1995.)
((A On B On) → (AB) On)

Theoremonelss 4090 An element of an ordinal number is a subset of the number. (Contributed by NM, 5-Jun-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(A On → (B ABA))

Theoremordtr1 4091 Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.)
(Ord 𝐶 → ((A B B 𝐶) → A 𝐶))

Theoremontr1 4092 Transitive law for ordinal numbers. Theorem 7M(b) of [Enderton] p. 192. (Contributed by NM, 11-Aug-1994.)
(𝐶 On → ((A B B 𝐶) → A 𝐶))

Theoremonintss 4093* If a property is true for an ordinal number, then the minimum ordinal number for which it is true is smaller or equal. Theorem Schema 61 of [Suppes] p. 228. (Contributed by NM, 3-Oct-2003.)
(x = A → (φψ))       (A On → (ψ {x On ∣ φ} ⊆ A))

Theoremord0 4094 The empty set is an ordinal class. (Contributed by NM, 11-May-1994.)
Ord ∅

Theorem0elon 4095 The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193. (Contributed by NM, 17-Sep-1993.)
On

Theoreminton 4096 The intersection of the class of ordinal numbers is the empty set. (Contributed by NM, 20-Oct-2003.)
On = ∅

Theoremnlim0 4097 The empty set is not a limit ordinal. (Contributed by NM, 24-Mar-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
¬ Lim ∅

Theoremlimord 4098 A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.)
(Lim A → Ord A)

Theoremlimuni 4099 A limit ordinal is its own supremum (union). (Contributed by NM, 4-May-1995.)
(Lim AA = A)

Theoremlimuni2 4100 The union of a limit ordinal is a limit ordinal. (Contributed by NM, 19-Sep-2006.)
(Lim A → Lim A)

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-9427
 Copyright terms: Public domain < Previous  Next >