 Home Intuitionistic Logic ExplorerTheorem List (p. 44 of 73) < 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 - 4301-4400   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremopelxp 4301 Ordered pair membership in a cross product. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
(⟨A, B (𝐶 × 𝐷) ↔ (A 𝐶 B 𝐷))

Theorembrxp 4302 Binary relation on a cross product. (Contributed by NM, 22-Apr-2004.)
(A(𝐶 × 𝐷)B ↔ (A 𝐶 B 𝐷))

Theoremopelxpi 4303 Ordered pair membership in a cross product (implication). (Contributed by NM, 28-May-1995.)
((A 𝐶 B 𝐷) → ⟨A, B (𝐶 × 𝐷))

Theoremopelxp1 4304 The first member of an ordered pair of classes in a cross product belongs to first cross product argument. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
(⟨A, B (𝐶 × 𝐷) → A 𝐶)

Theoremopelxp2 4305 The second member of an ordered pair of classes in a cross product belongs to second cross product argument. (Contributed by Mario Carneiro, 26-Apr-2015.)
(⟨A, B (𝐶 × 𝐷) → B 𝐷)

Theoremotelxp1 4306 The first member of an ordered triple of classes in a cross product belongs to first cross product argument. (Contributed by NM, 28-May-2008.)
(⟨⟨A, B⟩, 𝐶 ((𝑅 × 𝑆) × 𝑇) → A 𝑅)

Theoremrabxp 4307* Membership in a class builder restricted to a cross product. (Contributed by NM, 20-Feb-2014.)
(x = ⟨y, z⟩ → (φψ))       {x (A × B) ∣ φ} = {⟨y, z⟩ ∣ (y A z B ψ)}

Theorembrrelex12 4308 A true binary relation on a relation implies the arguments are sets. (This is a property of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015.)
((Rel 𝑅 A𝑅B) → (A V B V))

Theorembrrelex 4309 A true binary relation on a relation implies the first argument is a set. (This is a property of our ordered pair definition.) (Contributed by NM, 18-May-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
((Rel 𝑅 A𝑅B) → A V)

Theorembrrelex2 4310 A true binary relation on a relation implies the second argument is a set. (This is a property of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015.)
((Rel 𝑅 A𝑅B) → B V)

Theorembrrelexi 4311 The first argument of a binary relation exists. (An artifact of our ordered pair definition.) (Contributed by NM, 4-Jun-1998.)
Rel 𝑅       (A𝑅BA V)

Theorembrrelex2i 4312 The second argument of a binary relation exists. (An artifact of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015.)
Rel 𝑅       (A𝑅BB V)

Theoremnprrel 4313 No proper class is related to anything via any relation. (Contributed by Roy F. Longton, 30-Jul-2005.)
Rel 𝑅    &    ¬ A V        ¬ A𝑅B

Theoremfconstmpt 4314* Representation of a constant function using the mapping operation. (Note that x cannot appear free in B.) (Contributed by NM, 12-Oct-1999.) (Revised by Mario Carneiro, 16-Nov-2013.)
(A × {B}) = (x AB)

Theoremvtoclr 4315* Variable to class conversion of transitive relation. (Contributed by NM, 9-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
Rel 𝑅    &   ((x𝑅y y𝑅z) → x𝑅z)       ((A𝑅B B𝑅𝐶) → A𝑅𝐶)

Theoremopelvvg 4316 Ordered pair membership in the universal class of ordered pairs. (Contributed by Mario Carneiro, 3-May-2015.)
((A 𝑉 B 𝑊) → ⟨A, B (V × V))

Theoremopelvv 4317 Ordered pair membership in the universal class of ordered pairs. (Contributed by NM, 22-Aug-2013.) (Revised by Mario Carneiro, 26-Apr-2015.)
A V    &   B V       A, B (V × V)

Theoremopthprc 4318 Justification theorem for an ordered pair definition that works for any classes, including proper classes. This is a possible definition implied by the footnote in [Jech] p. 78, which says, "The sophisticated reader will not object to our use of a pair of classes." (Contributed by NM, 28-Sep-2003.)
(((A × {∅}) ∪ (B × {{∅}})) = ((𝐶 × {∅}) ∪ (𝐷 × {{∅}})) ↔ (A = 𝐶 B = 𝐷))

Theorembrel 4319 Two things in a binary relation belong to the relation's domain. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 26-Apr-2015.)
𝑅 ⊆ (𝐶 × 𝐷)       (A𝑅B → (A 𝐶 B 𝐷))

Theorembrab2a 4320* Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 9-Nov-2015.)
((x = A y = B) → (φψ))    &   𝑅 = {⟨x, y⟩ ∣ ((x 𝐶 y 𝐷) φ)}       (A𝑅B ↔ ((A 𝐶 B 𝐷) ψ))

Theoremelxp3 4321* Membership in a cross product. (Contributed by NM, 5-Mar-1995.)
(A (B × 𝐶) ↔ xy(⟨x, y⟩ = A x, y (B × 𝐶)))

Theoremopeliunxp 4322 Membership in a union of cross products. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by Mario Carneiro, 1-Jan-2017.)
(⟨x, 𝐶 x A ({x} × B) ↔ (x A 𝐶 B))

Theoremxpundi 4323 Distributive law for cross product over union. Theorem 103 of [Suppes] p. 52. (Contributed by NM, 12-Aug-2004.)
(A × (B𝐶)) = ((A × B) ∪ (A × 𝐶))

Theoremxpundir 4324 Distributive law for cross product over union. Similar to Theorem 103 of [Suppes] p. 52. (Contributed by NM, 30-Sep-2002.)
((AB) × 𝐶) = ((A × 𝐶) ∪ (B × 𝐶))

Theoremxpiundi 4325* Distributive law for cross product over indexed union. (Contributed by Mario Carneiro, 27-Apr-2014.)
(𝐶 × x A B) = x A (𝐶 × B)

Theoremxpiundir 4326* Distributive law for cross product over indexed union. (Contributed by Mario Carneiro, 27-Apr-2014.)
( x A B × 𝐶) = x A (B × 𝐶)

Theoremiunxpconst 4327* Membership in a union of cross products when the second factor is constant. (Contributed by Mario Carneiro, 29-Dec-2014.)
x A ({x} × B) = (A × B)

Theoremxpun 4328 The cross product of two unions. (Contributed by NM, 12-Aug-2004.)
((AB) × (𝐶𝐷)) = (((A × 𝐶) ∪ (A × 𝐷)) ∪ ((B × 𝐶) ∪ (B × 𝐷)))

Theoremelvv 4329* Membership in universal class of ordered pairs. (Contributed by NM, 4-Jul-1994.)
(A (V × V) ↔ xy A = ⟨x, y⟩)

Theoremelvvv 4330* Membership in universal class of ordered triples. (Contributed by NM, 17-Dec-2008.)
(A ((V × V) × V) ↔ xyz A = ⟨⟨x, y⟩, z⟩)

Theoremelvvuni 4331 An ordered pair contains its union. (Contributed by NM, 16-Sep-2006.)
(A (V × V) → A A)

Theoremmosubopt 4332* "At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-Aug-2007.)
(yz∃*xφ∃*xyz(A = ⟨y, z φ))

Theoremmosubop 4333* "At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-May-1995.)
∃*xφ       ∃*xyz(A = ⟨y, z φ)

Theorembrinxp2 4334 Intersection of binary relation with cross product. (Contributed by NM, 3-Mar-2007.) (Revised by Mario Carneiro, 26-Apr-2015.)
(A(𝑅 ∩ (𝐶 × 𝐷))B ↔ (A 𝐶 B 𝐷 A𝑅B))

Theorembrinxp 4335 Intersection of binary relation with cross product. (Contributed by NM, 9-Mar-1997.)
((A 𝐶 B 𝐷) → (A𝑅BA(𝑅 ∩ (𝐶 × 𝐷))B))

Theorempoinxp 4336 Intersection of partial order with cross product of its field. (Contributed by Mario Carneiro, 10-Jul-2014.)
(𝑅 Po A ↔ (𝑅 ∩ (A × A)) Po A)

Theoremsoinxp 4337 Intersection of linear order with cross product of its field. (Contributed by Mario Carneiro, 10-Jul-2014.)
(𝑅 Or A ↔ (𝑅 ∩ (A × A)) Or A)

Theoremseinxp 4338 Intersection of set-like relation with cross product of its field. (Contributed by Mario Carneiro, 22-Jun-2015.)
(𝑅 Se A ↔ (𝑅 ∩ (A × A)) Se A)

Theoremposng 4339 Partial ordering of a singleton. (Contributed by Jim Kingdon, 5-Dec-2018.)
((Rel 𝑅 A V) → (𝑅 Po {A} ↔ ¬ A𝑅A))

Theoremsosng 4340 Strict linear ordering on a singleton. (Contributed by Jim Kingdon, 5-Dec-2018.)
((Rel 𝑅 A V) → (𝑅 Or {A} ↔ ¬ A𝑅A))

Theoremopabssxp 4341* An abstraction relation is a subset of a related cross product. (Contributed by NM, 16-Jul-1995.)
{⟨x, y⟩ ∣ ((x A y B) φ)} ⊆ (A × B)

Theorembrab2ga 4342* The law of concretion for a binary relation. See brab2a 4320 for alternate proof. TODO: should one of them be deleted? (Contributed by Mario Carneiro, 28-Apr-2015.) (Proof modification is discouraged.)
((x = A y = B) → (φψ))    &   𝑅 = {⟨x, y⟩ ∣ ((x 𝐶 y 𝐷) φ)}       (A𝑅B ↔ ((A 𝐶 B 𝐷) ψ))

Theoremoptocl 4343* Implicit substitution of class for ordered pair. (Contributed by NM, 5-Mar-1995.)
𝐷 = (B × 𝐶)    &   (⟨x, y⟩ = A → (φψ))    &   ((x B y 𝐶) → φ)       (A 𝐷ψ)

Theorem2optocl 4344* Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995.)
𝑅 = (𝐶 × 𝐷)    &   (⟨x, y⟩ = A → (φψ))    &   (⟨z, w⟩ = B → (ψχ))    &   (((x 𝐶 y 𝐷) (z 𝐶 w 𝐷)) → φ)       ((A 𝑅 B 𝑅) → χ)

Theorem3optocl 4345* Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995.)
𝑅 = (𝐷 × 𝐹)    &   (⟨x, y⟩ = A → (φψ))    &   (⟨z, w⟩ = B → (ψχ))    &   (⟨v, u⟩ = 𝐶 → (χθ))    &   (((x 𝐷 y 𝐹) (z 𝐷 w 𝐹) (v 𝐷 u 𝐹)) → φ)       ((A 𝑅 B 𝑅 𝐶 𝑅) → θ)

Theoremopbrop 4346* Ordered pair membership in a relation. Special case. (Contributed by NM, 5-Aug-1995.)
(((z = A w = B) (v = 𝐶 u = 𝐷)) → (φψ))    &   𝑅 = {⟨x, y⟩ ∣ ((x (𝑆 × 𝑆) y (𝑆 × 𝑆)) zwvu((x = ⟨z, w y = ⟨v, u⟩) φ))}       (((A 𝑆 B 𝑆) (𝐶 𝑆 𝐷 𝑆)) → (⟨A, B𝑅𝐶, 𝐷⟩ ↔ ψ))

Theorem0xp 4347 The cross product with the empty set is empty. Part of Theorem 3.13(ii) of [Monk1] p. 37. (Contributed by NM, 4-Jul-1994.)
(∅ × A) = ∅

Theoremcsbxpg 4348 Distribute proper substitution through the cross product of two classes. (Contributed by Alan Sare, 10-Nov-2012.)
(A 𝐷A / x(B × 𝐶) = (A / xB × A / x𝐶))

Theoremreleq 4349 Equality theorem for the relation predicate. (Contributed by NM, 1-Aug-1994.)
(A = B → (Rel A ↔ Rel B))

Theoremreleqi 4350 Equality inference for the relation predicate. (Contributed by NM, 8-Dec-2006.)
A = B       (Rel A ↔ Rel B)

Theoremreleqd 4351 Equality deduction for the relation predicate. (Contributed by NM, 8-Mar-2014.)
(φA = B)       (φ → (Rel A ↔ Rel B))

Theoremnfrel 4352 Bound-variable hypothesis builder for a relation. (Contributed by NM, 31-Jan-2004.) (Revised by Mario Carneiro, 15-Oct-2016.)
xA       xRel A

Theoremsbcrel 4353 Distribute proper substitution through a relation predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
(A 𝑉 → ([A / x]Rel 𝑅 ↔ Rel A / x𝑅))

Theoremrelss 4354 Subclass theorem for relation predicate. Theorem 2 of [Suppes] p. 58. (Contributed by NM, 15-Aug-1994.)
(AB → (Rel B → Rel A))

Theoremssrel 4355* A subclass relationship depends only on a relation's ordered pairs. Theorem 3.2(i) of [Monk1] p. 33. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
(Rel A → (ABxy(⟨x, y A → ⟨x, y B)))

Theoremeqrel 4356* Extensionality principle for relations. Theorem 3.2(ii) of [Monk1] p. 33. (Contributed by NM, 2-Aug-1994.)
((Rel A Rel B) → (A = Bxy(⟨x, y A ↔ ⟨x, y B)))

Theoremssrel2 4357* A subclass relationship depends only on a relation's ordered pairs. This version of ssrel 4355 is restricted to the relation's domain. (Contributed by Thierry Arnoux, 25-Jan-2018.)
(𝑅 ⊆ (A × B) → (𝑅𝑆x A y B (⟨x, y 𝑅 → ⟨x, y 𝑆)))

Theoremrelssi 4358* Inference from subclass principle for relations. (Contributed by NM, 31-Mar-1998.)
Rel A    &   (⟨x, y A → ⟨x, y B)       AB

Theoremrelssdv 4359* Deduction from subclass principle for relations. (Contributed by NM, 11-Sep-2004.)
(φ → Rel A)    &   (φ → (⟨x, y A → ⟨x, y B))       (φAB)

Theoremeqrelriv 4360* Inference from extensionality principle for relations. (Contributed by FL, 15-Oct-2012.)
(⟨x, y A ↔ ⟨x, y B)       ((Rel A Rel B) → A = B)

Theoremeqrelriiv 4361* Inference from extensionality principle for relations. (Contributed by NM, 17-Mar-1995.)
Rel A    &   Rel B    &   (⟨x, y A ↔ ⟨x, y B)       A = B

Theoremeqbrriv 4362* Inference from extensionality principle for relations. (Contributed by NM, 12-Dec-2006.)
Rel A    &   Rel B    &   (xAyxBy)       A = B

Theoremeqrelrdv 4363* Deduce equality of relations from equivalence of membership. (Contributed by Rodolfo Medina, 10-Oct-2010.)
Rel A    &   Rel B    &   (φ → (⟨x, y A ↔ ⟨x, y B))       (φA = B)

Theoremeqbrrdv 4364* Deduction from extensionality principle for relations. (Contributed by Mario Carneiro, 3-Jan-2017.)
(φ → Rel A)    &   (φ → Rel B)    &   (φ → (xAyxBy))       (φA = B)

Theoremeqbrrdiv 4365* Deduction from extensionality principle for relations. (Contributed by Rodolfo Medina, 10-Oct-2010.)
Rel A    &   Rel B    &   (φ → (xAyxBy))       (φA = B)

Theoremeqrelrdv2 4366* A version of eqrelrdv 4363. (Contributed by Rodolfo Medina, 10-Oct-2010.)
(φ → (⟨x, y A ↔ ⟨x, y B))       (((Rel A Rel B) φ) → A = B)

Theoremssrelrel 4367* A subclass relationship determined by ordered triples. Use relrelss 4771 to express the antecedent in terms of the relation predicate. (Contributed by NM, 17-Dec-2008.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
(A ⊆ ((V × V) × V) → (ABxyz(⟨⟨x, y⟩, z A → ⟨⟨x, y⟩, z B)))

Theoremeqrelrel 4368* Extensionality principle for ordered triples, analogous to eqrel 4356. Use relrelss 4771 to express the antecedent in terms of the relation predicate. (Contributed by NM, 17-Dec-2008.)
((AB) ⊆ ((V × V) × V) → (A = Bxyz(⟨⟨x, y⟩, z A ↔ ⟨⟨x, y⟩, z B)))

Theoremelrel 4369* A member of a relation is an ordered pair. (Contributed by NM, 17-Sep-2006.)
((Rel 𝑅 A 𝑅) → xy A = ⟨x, y⟩)

Theoremrelsn 4370 A singleton is a relation iff it is an ordered pair. (Contributed by NM, 24-Sep-2013.)
A V       (Rel {A} ↔ A (V × V))

Theoremrelsnop 4371 A singleton of an ordered pair is a relation. (Contributed by NM, 17-May-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
A V    &   B V       Rel {⟨A, B⟩}

Theoremxpss12 4372 Subset theorem for cross product. Generalization of Theorem 101 of [Suppes] p. 52. (Contributed by NM, 26-Aug-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
((AB 𝐶𝐷) → (A × 𝐶) ⊆ (B × 𝐷))

Theoremxpss 4373 A cross product is included in the ordered pair universe. Exercise 3 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.)
(A × B) ⊆ (V × V)

Theoremrelxp 4374 A cross product is a relation. Theorem 3.13(i) of [Monk1] p. 37. (Contributed by NM, 2-Aug-1994.)
Rel (A × B)

Theoremxpss1 4375 Subset relation for cross product. (Contributed by Jeff Hankins, 30-Aug-2009.)
(AB → (A × 𝐶) ⊆ (B × 𝐶))

Theoremxpss2 4376 Subset relation for cross product. (Contributed by Jeff Hankins, 30-Aug-2009.)
(AB → (𝐶 × A) ⊆ (𝐶 × B))

Theoremxpsspw 4377 A cross product is included in the power of the power of the union of its arguments. (Contributed by NM, 13-Sep-2006.)
(A × B) ⊆ 𝒫 𝒫 (AB)

Theoremunixpss 4378 The double class union of a cross product is included in the union of its arguments. (Contributed by NM, 16-Sep-2006.)
(A × B) ⊆ (AB)

Theoremxpexg 4379 The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. (Contributed by NM, 14-Aug-1994.)
((A 𝑉 B 𝑊) → (A × B) V)

Theoremxpex 4380 The cross product of two sets is a set. Proposition 6.2 of [TakeutiZaring] p. 23. (Contributed by NM, 14-Aug-1994.)
A V    &   B V       (A × B) V

Theoremrelun 4381 The union of two relations is a relation. Compare Exercise 5 of [TakeutiZaring] p. 25. (Contributed by NM, 12-Aug-1994.)
(Rel (AB) ↔ (Rel A Rel B))

Theoremrelin1 4382 The intersection with a relation is a relation. (Contributed by NM, 16-Aug-1994.)
(Rel A → Rel (AB))

Theoremrelin2 4383 The intersection with a relation is a relation. (Contributed by NM, 17-Jan-2006.)
(Rel B → Rel (AB))

Theoremreldif 4384 A difference cutting down a relation is a relation. (Contributed by NM, 31-Mar-1998.)
(Rel A → Rel (AB))

Theoremreliun 4385 An indexed union is a relation iff each member of its indexed family is a relation. (Contributed by NM, 19-Dec-2008.)
(Rel x A Bx A Rel B)

Theoremreliin 4386 An indexed intersection is a relation if at least one of the member of the indexed family is a relation. (Contributed by NM, 8-Mar-2014.)
(x A Rel B → Rel x A B)

Theoremreluni 4387* The union of a class is a relation iff any member is a relation. Exercise 6 of [TakeutiZaring] p. 25 and its converse. (Contributed by NM, 13-Aug-2004.)
(Rel Ax A Rel x)

Theoremrelint 4388* The intersection of a class is a relation if at least one member is a relation. (Contributed by NM, 8-Mar-2014.)
(x A Rel x → Rel A)

Theoremrel0 4389 The empty set is a relation. (Contributed by NM, 26-Apr-1998.)
Rel ∅

Theoremrelopabi 4390 A class of ordered pairs is a relation. (Contributed by Mario Carneiro, 21-Dec-2013.)
A = {⟨x, y⟩ ∣ φ}       Rel A

Theoremrelopab 4391 A class of ordered pairs is a relation. (Contributed by NM, 8-Mar-1995.) (Unnecessary distinct variable restrictions were removed by Alan Sare, 9-Jul-2013.) (Proof shortened by Mario Carneiro, 21-Dec-2013.)
Rel {⟨x, y⟩ ∣ φ}

Theoremreli 4392 The identity relation is a relation. Part of Exercise 4.12(p) of [Mendelson] p. 235. (Contributed by NM, 26-Apr-1998.) (Revised by Mario Carneiro, 21-Dec-2013.)
Rel I

Theoremrele 4393 The membership relation is a relation. (Contributed by NM, 26-Apr-1998.) (Revised by Mario Carneiro, 21-Dec-2013.)
Rel E

Theoremopabid2 4394* A relation expressed as an ordered pair abstraction. (Contributed by NM, 11-Dec-2006.)
(Rel A → {⟨x, y⟩ ∣ ⟨x, y A} = A)

Theoreminopab 4395* Intersection of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.)
({⟨x, y⟩ ∣ φ} ∩ {⟨x, y⟩ ∣ ψ}) = {⟨x, y⟩ ∣ (φ ψ)}

Theoremdifopab 4396* The difference of two ordered-pair abstractions. (Contributed by Stefan O'Rear, 17-Jan-2015.)
({⟨x, y⟩ ∣ φ} ∖ {⟨x, y⟩ ∣ ψ}) = {⟨x, y⟩ ∣ (φ ¬ ψ)}

Theoreminxp 4397 The intersection of two cross products. Exercise 9 of [TakeutiZaring] p. 25. (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
((A × B) ∩ (𝐶 × 𝐷)) = ((A𝐶) × (B𝐷))

Theoremxpindi 4398 Distributive law for cross product over intersection. Theorem 102 of [Suppes] p. 52. (Contributed by NM, 26-Sep-2004.)
(A × (B𝐶)) = ((A × B) ∩ (A × 𝐶))

Theoremxpindir 4399 Distributive law for cross product over intersection. Similar to Theorem 102 of [Suppes] p. 52. (Contributed by NM, 26-Sep-2004.)
((AB) × 𝐶) = ((A × 𝐶) ∩ (B × 𝐶))

Theoremxpiindim 4400* Distributive law for cross product over indexed intersection. (Contributed by Jim Kingdon, 7-Dec-2018.)
(y y A → (𝐶 × x A B) = x A (𝐶 × B))

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