HomeHome New Foundations Explorer
Theorem List (p. 46 of 64)
< Previous  Next >
Bad symbols? Use Firefox
(or GIF version for IE).

Mirrors  >  Metamath Home Page  >  NFE Home Page  >  Theorem List Contents       This page: Page List

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 SSetkIns2k SIk SSetk ) “k 1111c)) ∩ Ins2k SSetk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SSetkIns2k SIk SSetk ) “k 111c) ∩ Ins2k SSetk ) “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 SSetkIns2k SIk SSetk ) “k 1111c)) ∩ Ins2k SSetk ) “k 111c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k SSetkIns2k SIk SSetk ) “k 111c) ∩ Ins2k SSetk ) “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))
 
Theoremaddccan1 4559 Cancellation law for natural addition. (Contributed by SF, 3-Feb-2015.)
((M Nn N Nn P Nn ) → ((M +c P) = (N +c P) ↔ M = N))
 
Theoremaddccan2 4560 Cancellation law for natural addition. (Contributed by SF, 3-Feb-2015.)
((M Nn N Nn P Nn ) → ((M +c N) = (M +c P) ↔ N = P))
 
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.
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.
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.
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.
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 SSetkIns2k SSetk ) “k 111c) (( Ins2k Ins2k SSetk ⊕ ( Ins2k Ins3k SSetkIns3k SIk SIk SSetk )) “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 SSetkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SSetkIns2k SSetk ) “k 111c) (( Ins2k Ins2k SSetk ⊕ ( Ins2k Ins3k SSetkIns3k SIk SIk SSetk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k SSetk ) ∪ ({{0c}} ×k V))) “k 111c) ↔ y = ( Phi x ∪ {0c}))
 
Theoremdfop2lem2 4574* Lemma for dfop2 4575 (Contributed by SF, 2-Jan-2015.)
( ∼ (( Ins2k SSetkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SSetkIns2k SSetk ) “k 111c) (( Ins2k Ins2k SSetk ⊕ ( Ins2k Ins3k SSetkIns3k SIk SIk SSetk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k SSetk ) ∪ ({{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 SSetkIns2k SSetk ) “k 111c) (( Ins2k Ins2k SSetk ⊕ ( Ins2k Ins3k SSetkIns3k SIk SIk SSetk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) “k A) ∪ ( ∼ (( Ins2k SSetkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SSetkIns2k SSetk ) “k 111c) (( Ins2k Ins2k SSetk ⊕ ( Ins2k Ins3k SSetkIns3k SIk SIk SSetk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k SSetk ) ∪ ({{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 SSetkIns2k SSetk ) “k 111c) (( Ins2k Ins2k SSetk ⊕ ( Ins2k Ins3k SSetkIns3k SIk SIk SSetk )) “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 SSetkIns3k ((kImagek((Imagek(( Ins3k ∼ (( Ins3k SSetkIns2k SSetk ) “k 111c) (( Ins2k Ins2k SSetk ⊕ ( Ins2k Ins3k SSetkIns3k SIk SIk SSetk )) “k 11111c)) “k 111c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) k SSetk ) ∪ ({{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)
 
Theoremphi11lem1 4593 Lemma for phi11 4594. (Contributed by SF, 3-Feb-2015.)
( Phi A = Phi BA B)
 
Theoremphi11 4594 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 4595 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 4596 Lemma for phi011 4597. (Contributed by SF, 3-Feb-2015.)
(( Phi A ∪ {0c}) = ( Phi B ∪ {0c}) → Phi A Phi B)
 
Theoremphi011 4597 ( 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 4598 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
 
Theoremproj2op 4599 The second projection operator applied to an ordered pair yields its second member. Theorem X.2.8 of [Rosser] p. 283. (Contributed by SF, 3-Feb-2015.)
Proj2 A, B = B
 
Theoremopth 4600 The ordered pair theorem. Two ordered pairs are equal iff their components are equal. (Contributed by SF, 2-Jan-2015.)
(A, B = C, D ↔ (A = C B = D))
    < Previous  Next >

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