Theorem List for New Foundations Explorer - 4501-4600   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremtfinltfin 4501 Ordering rule for the finite T operation. Corollary to theorem X.1.33 of [Rosser] p. 529. (Contributed by SF, 1-Feb-2015.)
((M Nn N Nn ) → (⟪M, N <fin ↔ ⟪ Tfin M, Tfin N <fin ))

Theoremtfinlefin 4502 Ordering rule for the finite T operation. Theorem X.1.33 of [Rosser] p. 529. (Contributed by SF, 2-Feb-2015.)
((M Nn N Nn ) → (⟪M, Nfin ↔ ⟪ Tfin M, Tfin Nfin ))

Theoremevenfinex 4503 The set of all even naturals exists. (Contributed by SF, 20-Jan-2015.)
Evenfin V

Theoremoddfinex 4504 The set of all odd naturals exists. (Contributed by SF, 20-Jan-2015.)
Oddfin V

Theorem0ceven 4505 Cardinal zero is even. (Contributed by SF, 20-Jan-2015.)
0c Evenfin

Theoremevennn 4506 An even finite cardinal is a finite cardinal. (Contributed by SF, 20-Jan-2015.)
(A EvenfinA Nn )

Theoremoddnn 4507 An odd finite cardinal is a finite cardinal. (Contributed by SF, 20-Jan-2015.)
(A OddfinA Nn )

Theoremevennnul 4508 An even number is non-empty. (Contributed by SF, 22-Jan-2015.)
(A EvenfinA)

Theoremoddnnul 4509 An odd number is non-empty. (Contributed by SF, 22-Jan-2015.)
(A OddfinA)

Theoremsucevenodd 4510 The successor of an even natural is odd. (Contributed by SF, 20-Jan-2015.)
((A Evenfin (A +c 1c) ≠ ) → (A +c 1c) Oddfin )

Theoremsucoddeven 4511 The successor of an odd natural is even. (Contributed by SF, 22-Jan-2015.)
((A Oddfin (A +c 1c) ≠ ) → (A +c 1c) Evenfin )

Theoremdfevenfin2 4512* Alternate definition of even number. (Contributed by SF, 25-Jan-2015.)
Evenfin = {x n Nn (x = (n +c n) (n +c n) ≠ )}

Theoremdfoddfin2 4513* Alternate definition of odd number. (Contributed by SF, 25-Jan-2015.)
Oddfin = {x n Nn (x = ((n +c n) +c 1c) ((n +c n) +c 1c) ≠ )}

Theoremevenoddnnnul 4514 Every non-empty finite cardinal is either even or odd. Theorem X.1.35 of [Rosser] p. 529. (Contributed by SF, 20-Jan-2015.)
( EvenfinOddfin ) = ( Nn {})

Theoremevenodddisjlem1 4515* Lemma for evenodddisj 4516. Establish stratification for induction. (Contributed by SF, 25-Jan-2015.)
{j ((j +c j) ≠ n Nn (((n +c n) +c 1c) ≠ → (j +c j) ≠ ((n +c n) +c 1c)))} V

Theoremevenodddisj 4516 The even finite cardinals and the odd ones are disjoint. Theorem X.1.36 of [Rosser] p. 529. (Contributed by SF, 22-Jan-2015.)
( EvenfinOddfin ) =

Theoremeventfin 4517 If M is even , then so is Tfin M. Theorem X.1.37 of [Rosser] p. 530. (Contributed by SF, 26-Jan-2015.)
(M EvenfinTfin M Evenfin )

Theoremoddtfin 4518 If M is odd , then so is Tfin M. Theorem X.1.38 of [Rosser] p. 530. (Contributed by SF, 26-Jan-2015.)
(M OddfinTfin M Oddfin )

Theoremnnadjoinlem1 4519* Lemma for nnadjoin 4520. Establish stratification. (Contributed by SF, 29-Jan-2015.)
{n l n (y l → {x b l x = (b ∪ {y})} n)} V

Theoremnnadjoin 4520* Adjoining a new element to every member of L does not change its size. Theorem X.1.39 of [Rosser] p. 530. (Contributed by SF, 29-Jan-2015.)
((N Nn L N X L) → {x b L x = (b ∪ {X})} N)

Theoremnnadjoinpw 4521 Adjoining an element to a power class. Theorem X.1.40 of [Rosser] p. 530. (Contributed by SF, 27-Jan-2015.)
(((M Nn N Nn ) (A M X A) A N) → (A ∪ {X}) (N +c N))

Theoremnnpweqlem1 4522* Lemma for nnpweq 4523. Establish stratification for induction. (Contributed by SF, 26-Jan-2015.)
{m a m b m n Nn (a n b n)} V

Theoremnnpweq 4523* If two sets are the same finite size, then so are their power classes. Theorem X.1.41 of [Rosser] p. 530. (Contributed by SF, 26-Jan-2015.)
((M Nn A M B M) → n Nn (A n B n))

Theoremsrelk 4524 Binary relationship form of the Sfin relationship. (Contributed by SF, 23-Jan-2015.)
A V    &   B V       (⟪A, B (( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ↔ Sfin (A, B))

Theoremsrelkex 4525 The expression at the core of srelk 4524 exists. (Contributed by SF, 30-Jan-2015.)
(( Nn ×k Nn ) ∩ (( Ins3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SkIns2k SIk Sk ) “k 111c) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) V

Theoremsfineq1 4526 Equality theorem for the finite S relationship. (Contributed by SF, 27-Jan-2015.)
(A = B → ( Sfin (A, C) ↔ Sfin (B, C)))

Theoremsfineq2 4527 Equality theorem for the finite S relationship. (Contributed by SF, 27-Jan-2015.)
(A = B → ( Sfin (C, A) ↔ Sfin (C, B)))

Theoremsfin01 4528 Zero and one satisfy Sfin. Theorem X.1.42 of [Rosser] p. 530. (Contributed by SF, 30-Jan-2015.)
Sfin (0c, 1c)

Theoremsfin112 4529 Equality law for the finite S operator. Theorem X.1.43 of [Rosser] p. 530. (Contributed by SF, 27-Jan-2015.)
(( Sfin (M, N) Sfin (M, P)) → N = P)

Theoremsfindbl 4530* If the unit power set of a set is in the successor of a finite cardinal, then there is a natural that is smaller than the finite cardinal and whose double is smaller than the successor of the cardinal. Theorem X.1.44 of [Rosser] p. 531. (Contributed by SF, 30-Jan-2015.)
((M Nn 1A (M +c 1c)) → n Nn ( Sfin (M, n) Sfin ((M +c 1c), (n +c n))))

Theoremsfintfinlem1 4531* Lemma for sfintfin 4532. Set up induction stratification. (Contributed by SF, 31-Jan-2015.)
{m n( Sfin (m, n) → Sfin ( Tfin m, Tfin n))} V

Theoremsfintfin 4532 If two numbers obey Sfin, then do their T raisings. Theorem X.1.45 of [Rosser] p. 532. (Contributed by SF, 30-Jan-2015.)
( Sfin (M, N) → Sfin ( Tfin M, Tfin N))

Theoremtfinnnlem1 4533* Lemma for tfinnn 4534. Establish stratification. (Contributed by SF, 30-Jan-2015.)
{n y n (y Nn → {a x y a = Tfin x} Tfin n)} V

Theoremtfinnn 4534* T-raising of a set of naturals. Theorem X.1.46 of [Rosser] p. 532. (Contributed by SF, 30-Jan-2015.)
((N Nn A Nn A N) → {a x A a = Tfin x} Tfin N)

Theoremsfinltfin 4535 Ordering law for finite smaller than. Theorem X.1.47 of [Rosser] p. 532. (Contributed by SF, 30-Jan-2015.)
((( Sfin (M, N) Sfin (P, Q)) M, P <fin ) → ⟪N, Q <fin )

Theoremsfin111 4536 The finite smaller relationship is one-to-one in its first argument. Theorem X.1.48 of [Rosser] p. 533. (Contributed by SF, 29-Jan-2015.)
(( Sfin (M, P) Sfin (N, P)) → M = N)

Theoremspfinex 4537 Spfin is a set. (Contributed by SF, 20-Jan-2015.)
Spfin V

Theoremncvspfin 4538 The cardinality of the universe is in the finite Sp set. Theorem X.1.49 of [Rosser] p. 534. (Contributed by SF, 27-Jan-2015.)
Ncfin V Spfin

Theoremspfinsfincl 4539 If X is in Spfin and Z is smaller than X, then Z is also in Spfin. Theorem X.1.50 of [Rosser] p. 534. (Contributed by SF, 27-Jan-2015.)
((X Spfin Sfin (Z, X)) → Z Spfin )

Theoremspfininduct 4540* Inductive principle for Spfin. Theorem X.1.51 of [Rosser] p. 534. (Contributed by SF, 27-Jan-2015.)
((B V Ncfin V B x Spfin z((x B Sfin (z, x)) → z B)) → Spfin B)

Theoremvfinspnn 4541 If the universe is finite, then Spfin is a subset of the non-empty naturals. Theorem X.1.53 of [Rosser] p. 534. (Contributed by SF, 27-Jan-2015.)
(V FinSpfin ( Nn {}))

Theorem1cvsfin 4542 If the universe is finite, then Ncfin 1c is the base two log of Ncfin V. Theorem X.1.54 of [Rosser] p. 534. (Contributed by SF, 29-Jan-2015.)
(V FinSfin ( Ncfin 1c, Ncfin V))

Theorem1cspfin 4543 If the universe is finite, then the size of 1c is in Spfin. Corollary of Theorem X.1.54 of [Rosser] p. 534. (Contributed by SF, 29-Jan-2015.)
(V FinNcfin 1c Spfin )

Theoremtncveqnc1fin 4544 If the universe is finite, then the T-raising of the size of the universe is equal to the size of 1c. Theorem X.1.55 of [Rosser] p. 534. (Contributed by SF, 29-Jan-2015.)
(V FinTfin Ncfin V = Ncfin 1c)

Theoremt1csfin1c 4545 If the universe is finite, then the T-raising of the size of 1c is smaller than the size itself. Corollary of theorem X.1.56 of [Rosser] p. 534. (Contributed by SF, 29-Jan-2015.)
(V FinSfin ( Tfin Ncfin 1c, Ncfin 1c))

Theoremvfintle 4546 If the universe is finite, then the T-raising of all non-empty naturals are no greater than the size of 1c. Theorem X.1.56 of [Rosser] p. 534. (Contributed by SF, 30-Jan-2015.)
((V Fin N Nn N) → ⟪ Tfin N, Ncfin 1cfin )

Theoremvfin1cltv 4547 If the universe is finite, then 1c is strictly smaller than the universe. Theorem X.1.57 of [Rosser] p. 534. (Contributed by SF, 30-Jan-2015.)
(V Fin → ⟪ Ncfin 1c, Ncfin V⟫ <fin )

Theoremvfinncvntnn 4548 If the universe is finite, then the size of the universe is not the T-raising of a natural. Theorem X.1.58 of [Rosser] p. 534. (Contributed by SF, 29-Jan-2015.)
((V Fin N Nn ) → Tfin NNcfin V)

Theoremvfinncvntsp 4549* If the universe is finite, then its size is not a T raising of an element of Spfin. Corollary of theorem X.1.58 of [Rosser] p. 534. (Contributed by SF, 27-Jan-2015.)
(V Fin → ¬ Ncfin V {a x Spfin a = Tfin x})

Theoremvfinspsslem1 4550* Lemma for vfinspss 4551. Establish part of the inductive step. (Contributed by SF, 3-Feb-2015.)
(((V Fin Tfin n Spfin ) (n Spfin Sfin (z, Tfin n))) → x Spfin z = Tfin x)

Theoremvfinspss 4551* If the universe is finite, then Spfin is a subset of its T raisings and the cardinality of the universe. Theorem X.1.59 of [Rosser] p. 534. (Contributed by SF, 29-Jan-2015.)
(V FinSpfin ({a x Spfin a = Tfin x} ∪ { Ncfin V}))

Theoremvfinspclt 4552 If the universe is finite, then Spfin is closed under T-raising. Theorem X.1.60 of [Rosser] p. 536. (Contributed by SF, 30-Jan-2015.)
((V Fin X Spfin ) → Tfin X Spfin )

Theoremvfinspeqtncv 4553* If the universe is finite, then Spfin is equal to its T raisings and the cardinality of the universe. Theorem X.1.61 of [Rosser] p. 536. (Contributed by SF, 29-Jan-2015.)
(V FinSpfin = ({a x Spfin a = Tfin x} ∪ { Ncfin V}))

Theoremvfinncsp 4554 If the universe is finite, then the size of Spfin is equal to the successor of its T-raising. Theorem X.1.62 of [Rosser] p. 536. (Contributed by SF, 20-Jan-2015.)
(V FinNcfin Spfin = ( Tfin Ncfin Spfin +c 1c))

Theoremvinf 4555 The universe is infinite. Theorem X.1.63 of [Rosser] p. 536. (Contributed by SF, 20-Jan-2015.)
¬ V Fin

Theoremnulnnn 4556 The empty class is not a natural. Theorem X.1.65 of [Rosser] p. 536. (Contributed by SF, 20-Jan-2015.)
¬ Nn

Theorempeano4 4557 The successor operation is one-to-one over the finite cardinals. Theorem X.1.66 of [Rosser] p. 537. (Contributed by SF, 20-Jan-2015.)
((M Nn N Nn (M +c 1c) = (N +c 1c)) → M = N)

Theoremsuc11nnc 4558 Successor cancellation law for finite cardinals. (Contributed by SF, 3-Feb-2015.)
((M Nn N Nn ) → ((M +c 1c) = (N +c 1c) ↔ M = N))

((M Nn N Nn P Nn ) → ((M +c N) = (M +c P) ↔ N = P))

((M Nn N Nn P Nn ) → ((M +c P) = (N +c P) ↔ M = N))

2.3  Ordered Pairs, Relationships, and Functions

2.3.1  Ordered Pairs

Syntaxcop 4561 Declare the syntax for an ordered pair.
class A, B

Syntaxcphi 4562 Declare the syntax for the Phi operation.
class Phi A

Syntaxcproj1 4563 Declare the syntax for the first projection operation.
class Proj1 A

Syntaxcproj2 4564 Declare the syntax for the second projection operation.
class Proj2 A

Definitiondf-phi 4565* Define the phi operator. This operation increments all the naturals in A and leaves all its other members the same. (Contributed by SF, 3-Feb-2015.)
Phi A = {y x A y = if(x Nn , (x +c 1c), x)}

Definitiondf-op 4566* Define the type-level ordered pair. Definition from [Rosser] p. 281. (Contributed by SF, 3-Feb-2015.)
A, B = ({x y A x = Phi y} ∪ {x y B x = ( Phi y ∪ {0c})})

Definitiondf-proj1 4567* Define the first projection operation. This operation recovers the first element of an ordered pair. Definition from [Rosser] p. 281. (Contributed by SF, 3-Feb-2015.)
Proj1 A = {x Phi x A}

Definitiondf-proj2 4568* Define the second projection operation. This operation recovers the second element of an ordered pair. Definition from [Rosser] p. 281. (Contributed by SF, 3-Feb-2015.)
Proj2 A = {x ( Phi x ∪ {0c}) A}

Theoremdfphi2 4569 Express the phi operator in terms of the Kuratowski set construction functions. (Contributed by SF, 3-Feb-2015.)
Phi A = (((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) “k A)

Theoremphieq 4570 Equality law for the Phi operation. (Contributed by SF, 3-Feb-2015.)
(A = B Phi A = Phi B)

Theoremphiexg 4571 The phi operator preserves sethood. (Contributed by SF, 3-Feb-2015.)
(A V Phi A V)

Theoremphiex 4572 The phi operator preserves sethood. (Contributed by SF, 3-Feb-2015.)
A V        Phi A V

Theoremdfop2lem1 4573* Lemma for dfop2 4575 and dfproj22 4577. (Contributed by SF, 2-Jan-2015.)
(⟪x, y ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c) ↔ y = ( Phi x ∪ {0c}))

Theoremdfop2lem2 4574* Lemma for dfop2 4575 (Contributed by SF, 2-Jan-2015.)
( ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c) “k B) = {x y B x = ( Phi y ∪ {0c})}

Theoremdfop2 4575 Express the ordered pair via the set construction functors. (Contributed by SF, 2-Jan-2015.)
A, B = ((Imagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) “k A) ∪ ( ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c) “k B))

Theoremdfproj12 4576 Express the first projection operator via the set construction functors. (Contributed by SF, 2-Jan-2015.)
Proj1 A = (kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) “k A)

Theoremdfproj22 4577 Express the second projection operator via the set construction functors. (Contributed by SF, 2-Jan-2015.)
Proj2 A = (k ∼ (( Ins2k SkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SkIns2k Sk ) “k 111c) (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k SkIns3k SIk SIk Sk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k Sk ) ∪ ({{0c}} ×k V))) “k 111c) “k A)

Theoremopeq1 4578 Equality theorem for ordered pairs. (Contributed by SF, 2-Jan-2015.)
(A = BA, C = B, C)

Theoremopeq2 4579 Equality theorem for ordered pairs. (Contributed by SF, 2-Jan-2015.)
(A = BC, A = C, B)

Theoremopeq12 4580 Equality theorem for ordered pairs. (Contributed by SF, 2-Jan-2015.)
((A = B C = D) → A, C = B, D)

Theoremopeq1i 4581 Equality inference for ordered pairs. (Contributed by SF, 16-Dec-2006.)
A = B       A, C = B, C

Theoremopeq2i 4582 Equality inference for ordered pairs. (Contributed by SF, 16-Dec-2006.)
A = B       C, A = C, B

Theoremopeq12i 4583 Equality inference for ordered pairs. (The proof was shortened by Eric Schmidt, 4-Apr-2007.) (Contributed by SF, 16-Dec-2006.)
A = B    &   C = D       A, C = B, D

Theoremopeq1d 4584 Equality deduction for ordered pairs. (Contributed by SF, 16-Dec-2006.)
(φA = B)       (φA, C = B, C)

Theoremopeq2d 4585 Equality deduction for ordered pairs. (Contributed by SF, 16-Dec-2006.)
(φA = B)       (φC, A = C, B)

Theoremopeq12d 4586 Equality deduction for ordered pairs. (The proof was shortened by Andrew Salmon, 29-Jun-2011.) (Contributed by SF, 16-Dec-2006.) (Revised by SF, 29-Jun-2011.)
(φA = B)    &   (φC = D)       (φA, C = B, D)

Theoremopexg 4587 An ordered pair of two sets is a set. (Contributed by SF, 2-Jan-2015.)
((A V B W) → A, B V)

Theoremopex 4588 An ordered pair of two sets is a set. (Contributed by SF, 5-Jan-2015.)
A V    &   B V       A, B V

Theoremproj1eq 4589 Equality theorem for first projection operator. (Contributed by SF, 2-Jan-2015.)
(A = B Proj1 A = Proj1 B)

Theoremproj2eq 4590 Equality theorem for second projection operator. (Contributed by SF, 2-Jan-2015.)
(A = B Proj2 A = Proj2 B)

Theoremproj1exg 4591 The first projection of a set is a set. (Contributed by SF, 2-Jan-2015.)
(A V Proj1 A V)

Theoremproj2exg 4592 The second projection of a set is a set. (Contributed by SF, 2-Jan-2015.)
(A V Proj2 A V)

Theoremproj1ex 4593 The first projection of a set is a set. (Contributed by Scott Fenton, 16-Apr-2021.)
A V        Proj1 A V

Theoremproj2ex 4594 The second projection of a set is a set. (Contributed by Scott Fenton, 16-Apr-2021.)
A V        Proj2 A V

Theoremphi11lem1 4595 Lemma for phi11 4596. (Contributed by SF, 3-Feb-2015.)
( Phi A = Phi BA B)

Theoremphi11 4596 The phi operator is one-to-one. Theorem X.2.2 of [Rosser] p. 282. (Contributed by SF, 3-Feb-2015.)
(A = B Phi A = Phi B)

Theorem0cnelphi 4597 Cardinal zero is not a member of a phi operation. Theorem X.2.3 of [Rosser] p. 282. (Contributed by SF, 3-Feb-2015.)
¬ 0c Phi A

Theoremphi011lem1 4598 Lemma for phi011 4599. (Contributed by SF, 3-Feb-2015.)
(( Phi A ∪ {0c}) = ( Phi B ∪ {0c}) → Phi A Phi B)

Theoremphi011 4599 ( Phi A ∪ {0c}) is one-to-one. Theorem X.2.4 of [Rosser] p. 282. (Contributed by SF, 3-Feb-2015.)
(A = B ↔ ( Phi A ∪ {0c}) = ( Phi B ∪ {0c}))

Theoremproj1op 4600 The first projection operator applied to an ordered pair yields its first member. Theorem X.2.7 of [Rosser] p. 282. (Contributed by SF, 3-Feb-2015.)
Proj1 A, B = 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-6337
 Copyright terms: Public domain < Previous  Next >