P. 46 of Theorem List - New Foundations Explorer

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

Type	Label	Description
Statement
Theorem	tfinltfin 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 ))
Theorem	tfinlefin 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, N⟫ ∈ ≤fin ↔ ⟪ Tfin M, Tfin N⟫ ∈ ≤fin ))
Theorem	evenfinex 4503	The set of all even naturals exists. (Contributed by SF, 20-Jan-2015.)
⊢ Evenfin ∈ V
Theorem	oddfinex 4504	The set of all odd naturals exists. (Contributed by SF, 20-Jan-2015.)
⊢ Oddfin ∈ V
Theorem	0ceven 4505	Cardinal zero is even. (Contributed by SF, 20-Jan-2015.)
⊢ 0c ∈ Evenfin
Theorem	evennn 4506	An even finite cardinal is a finite cardinal. (Contributed by SF, 20-Jan-2015.)
⊢ (A ∈ Evenfin → A ∈ Nn )
Theorem	oddnn 4507	An odd finite cardinal is a finite cardinal. (Contributed by SF, 20-Jan-2015.)
⊢ (A ∈ Oddfin → A ∈ Nn )
Theorem	evennnul 4508	An even number is nonempty. (Contributed by SF, 22-Jan-2015.)
⊢ (A ∈ Evenfin → A ≠ ∅)
Theorem	oddnnul 4509	An odd number is nonempty. (Contributed by SF, 22-Jan-2015.)
⊢ (A ∈ Oddfin → A ≠ ∅)
Theorem	sucevenodd 4510	The successor of an even natural is odd. (Contributed by SF, 20-Jan-2015.)
⊢ ((A ∈ Evenfin ∧ (A +c 1c) ≠ ∅) → (A +c 1c) ∈ Oddfin )
Theorem	sucoddeven 4511	The successor of an odd natural is even. (Contributed by SF, 22-Jan-2015.)
⊢ ((A ∈ Oddfin ∧ (A +c 1c) ≠ ∅) → (A +c 1c) ∈ Evenfin )
Theorem	dfevenfin2 4512*	Alternate definition of even number. (Contributed by SF, 25-Jan-2015.)
⊢ Evenfin = {x ∣ ∃n ∈ Nn (x = (n +c n) ∧ (n +c n) ≠ ∅)}
Theorem	dfoddfin2 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) ≠ ∅)}
Theorem	evenoddnnnul 4514	Every nonempty finite cardinal is either even or odd. Theorem X.1.35 of [Rosser] p. 529. (Contributed by SF, 20-Jan-2015.)
⊢ ( Evenfin ∪ Oddfin ) = ( Nn ∖ {∅})
Theorem	evenodddisjlem1 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
Theorem	evenodddisj 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.)
⊢ ( Evenfin ∩ Oddfin ) = ∅
Theorem	eventfin 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 ∈ Evenfin → Tfin M ∈ Evenfin )
Theorem	oddtfin 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 ∈ Oddfin → Tfin M ∈ Oddfin )
Theorem	nnadjoinlem1 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
Theorem	nnadjoin 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)
Theorem	nnadjoinpw 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))
Theorem	nnpweqlem1 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
Theorem	nnpweq 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))
Theorem	srelk 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 Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ↔ Sfin (A, B))
Theorem	srelkex 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 Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c) ∩ Ins2k (( Ins3k SIk ∼ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘11c) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ∈ V
Theorem	sfineq1 4526	Equality theorem for the finite S relationship. (Contributed by SF, 27-Jan-2015.)
⊢ (A = B → ( Sfin (A, C) ↔ Sfin (B, C)))
Theorem	sfineq2 4527	Equality theorem for the finite S relationship. (Contributed by SF, 27-Jan-2015.)
⊢ (A = B → ( Sfin (C, A) ↔ Sfin (C, B)))
Theorem	sfin01 4528	Zero and one satisfy Sfin. Theorem X.1.42 of [Rosser] p. 530. (Contributed by SF, 30-Jan-2015.)
⊢ Sfin (0c, 1c)
Theorem	sfin112 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)
Theorem	sfindbl 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))))
Theorem	sfintfinlem1 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
Theorem	sfintfin 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))
Theorem	tfinnnlem1 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
Theorem	tfinnn 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)
Theorem	sfinltfin 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 )
Theorem	sfin111 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)
Theorem	spfinex 4537	Spfin is a set. (Contributed by SF, 20-Jan-2015.)
⊢ Spfin ∈ V
Theorem	ncvspfin 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
Theorem	spfinsfincl 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 )
Theorem	spfininduct 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)
Theorem	vfinspnn 4541	If the universe is finite, then Spfin is a subset of the nonempty naturals. Theorem X.1.53 of [Rosser] p. 534. (Contributed by SF, 27-Jan-2015.)
⊢ (V ∈ Fin → Spfin ⊆ ( Nn ∖ {∅}))
Theorem	1cvsfin 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 ∈ Fin → Sfin ( Ncfin 1c, Ncfin V))
Theorem	1cspfin 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 ∈ Fin → Ncfin 1c ∈ Spfin )
Theorem	tncveqnc1fin 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 ∈ Fin → Tfin Ncfin V = Ncfin 1c)
Theorem	t1csfin1c 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 ∈ Fin → Sfin ( Tfin Ncfin 1c, Ncfin 1c))
Theorem	vfintle 4546	If the universe is finite, then the T-raising of all nonempty 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 1c⟫ ∈ ≤fin )
Theorem	vfin1cltv 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 )
Theorem	vfinncvntnn 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 N ≠ Ncfin V)
Theorem	vfinncvntsp 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})
Theorem	vfinspsslem1 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)
Theorem	vfinspss 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 ∈ Fin → Spfin ⊆ ({a ∣ ∃x ∈ Spfin a = Tfin x} ∪ { Ncfin V}))
Theorem	vfinspclt 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 )
Theorem	vfinspeqtncv 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 ∈ Fin → Spfin = ({a ∣ ∃x ∈ Spfin a = Tfin x} ∪ { Ncfin V}))
Theorem	vfinncsp 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 ∈ Fin → Ncfin Spfin = ( Tfin Ncfin Spfin +c 1c))
Theorem	vinf 4555	The universe is infinite. Theorem X.1.63 of [Rosser] p. 536. (Contributed by SF, 20-Jan-2015.)
⊢ ¬ V ∈ Fin
Theorem	nulnnn 4556	The empty class is not a natural. Theorem X.1.65 of [Rosser] p. 536. (Contributed by SF, 20-Jan-2015.)
⊢ ¬ ∅ ∈ Nn
Theorem	peano4 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)
Theorem	suc11nnc 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))
Theorem	addccan2 4559	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))
Theorem	addccan1 4560	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))
2.3  Ordered Pairs, Relationships, and Functions
2.3.1  Ordered Pairs
Syntax	cop 4561	Declare the syntax for an ordered pair.
class ⟨A, B⟩
Syntax	cphi 4562	Declare the syntax for the Phi operation.
class Phi A
Syntax	cproj1 4563	Declare the syntax for the first projection operation.
class Proj1 A
Syntax	cproj2 4564	Declare the syntax for the second projection operation.
class Proj2 A
Definition	df-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)}
Definition	df-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})})
Definition	df-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}
Definition	df-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}
Theorem	dfphi2 4569	Express the phi operator in terms of the Kuratowski set construction functions. (Contributed by SF, 3-Feb-2015.)
⊢ Phi A = (((Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) “k A)
Theorem	phieq 4570	Equality law for the Phi operation. (Contributed by SF, 3-Feb-2015.)
⊢ (A = B → Phi A = Phi B)
Theorem	phiexg 4571	The phi operator preserves sethood. (Contributed by SF, 3-Feb-2015.)
⊢ (A ∈ V → Phi A ∈ V)
Theorem	phiex 4572	The phi operator preserves sethood. (Contributed by SF, 3-Feb-2015.)
⊢ A ∈ V    ⇒   ⊢ Phi A ∈ V
Theorem	dfop2lem1 4573*	Lemma for dfop2 4575 and dfproj22 4577. (Contributed by SF, 2-Jan-2015.)
⊢ (⟪x, y⟫ ∈ ∼ (( Ins2k Sk ⊕ Ins3k ((◡kImagek((Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) ∘k Sk ) ∪ ({{0c}} ×k V))) “k ℘1℘11c) ↔ y = ( Phi x ∪ {0c}))
Theorem	dfop2lem2 4574*	Lemma for dfop2 4575. (Contributed by SF, 2-Jan-2015.)
⊢ ( ∼ (( Ins2k Sk ⊕ Ins3k ((◡kImagek((Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) ∘k Sk ) ∪ ({{0c}} ×k V))) “k ℘1℘11c) “k B) = {x ∣ ∃y ∈ B x = ( Phi y ∪ {0c})}
Theorem	dfop2 4575	Express the ordered pair via the set construction functors. (Contributed by SF, 2-Jan-2015.)
⊢ ⟨A, B⟩ = ((Imagek((Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) “k A) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k ((◡kImagek((Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) ∘k Sk ) ∪ ({{0c}} ×k V))) “k ℘1℘11c) “k B))
Theorem	dfproj12 4576	Express the first projection operator via the set construction functors. (Contributed by SF, 2-Jan-2015.)
⊢ Proj1 A = (◡kImagek((Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) “k A)
Theorem	dfproj22 4577	Express the second projection operator via the set construction functors. (Contributed by SF, 2-Jan-2015.)
⊢ Proj2 A = (◡k ∼ (( Ins2k Sk ⊕ Ins3k ((◡kImagek((Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c)) “k ℘1℘11c) ∩ ( Nn ×k V)) ∪ ( Ik ∩ ( ∼ Nn ×k V))) ∘k Sk ) ∪ ({{0c}} ×k V))) “k ℘1℘11c) “k A)
Theorem	opeq1 4578	Equality theorem for ordered pairs. (Contributed by SF, 2-Jan-2015.)
⊢ (A = B → ⟨A, C⟩ = ⟨B, C⟩)
Theorem	opeq2 4579	Equality theorem for ordered pairs. (Contributed by SF, 2-Jan-2015.)
⊢ (A = B → ⟨C, A⟩ = ⟨C, B⟩)
Theorem	opeq12 4580	Equality theorem for ordered pairs. (Contributed by SF, 2-Jan-2015.)
⊢ ((A = B ∧ C = D) → ⟨A, C⟩ = ⟨B, D⟩)
Theorem	opeq1i 4581	Equality inference for ordered pairs. (Contributed by SF, 16-Dec-2006.)
⊢ A = B    ⇒   ⊢ ⟨A, C⟩ = ⟨B, C⟩
Theorem	opeq2i 4582	Equality inference for ordered pairs. (Contributed by SF, 16-Dec-2006.)
⊢ A = B    ⇒   ⊢ ⟨C, A⟩ = ⟨C, B⟩
Theorem	opeq12i 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⟩
Theorem	opeq1d 4584	Equality deduction for ordered pairs. (Contributed by SF, 16-Dec-2006.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → ⟨A, C⟩ = ⟨B, C⟩)
Theorem	opeq2d 4585	Equality deduction for ordered pairs. (Contributed by SF, 16-Dec-2006.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → ⟨C, A⟩ = ⟨C, B⟩)
Theorem	opeq12d 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⟩)
Theorem	opexg 4587	An ordered pair of two sets is a set. (Contributed by SF, 2-Jan-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → ⟨A, B⟩ ∈ V)
Theorem	opex 4588	An ordered pair of two sets is a set. (Contributed by SF, 5-Jan-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ⟨A, B⟩ ∈ V
Theorem	proj1eq 4589	Equality theorem for first projection operator. (Contributed by SF, 2-Jan-2015.)
⊢ (A = B → Proj1 A = Proj1 B)
Theorem	proj2eq 4590	Equality theorem for second projection operator. (Contributed by SF, 2-Jan-2015.)
⊢ (A = B → Proj2 A = Proj2 B)
Theorem	proj1exg 4591	The first projection of a set is a set. (Contributed by SF, 2-Jan-2015.)
⊢ (A ∈ V → Proj1 A ∈ V)
Theorem	proj2exg 4592	The second projection of a set is a set. (Contributed by SF, 2-Jan-2015.)
⊢ (A ∈ V → Proj2 A ∈ V)
Theorem	proj1ex 4593	The first projection of a set is a set. (Contributed by Scott Fenton, 16-Apr-2021.)
⊢ A ∈ V    ⇒   ⊢ Proj1 A ∈ V
Theorem	proj2ex 4594	The second projection of a set is a set. (Contributed by Scott Fenton, 16-Apr-2021.)
⊢ A ∈ V    ⇒   ⊢ Proj2 A ∈ V
Theorem	phi11lem1 4595	Lemma for phi11 4596. (Contributed by SF, 3-Feb-2015.)
⊢ ( Phi A = Phi B → A ⊆ B)
Theorem	phi11 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)
Theorem	0cnelphi 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
Theorem	phi011lem1 4598	Lemma for phi011 4599. (Contributed by SF, 3-Feb-2015.)
⊢ (( Phi A ∪ {0c}) = ( Phi B ∪ {0c}) → Phi A ⊆ Phi B)
Theorem	phi011 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}))
Theorem	proj1op 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