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	tfinltfinlem1 4501	Lemma for tfinltfin 4502. Prove the forward direction of the theorem. (Contributed by SF, 2-Feb-2015.)
⊢ ((M ∈ Nn ∧ N ∈ Nn ) → (⟪M, N⟫ ∈ <fin → ⟪ Tfin M, Tfin N⟫ ∈ <fin ))
Theorem	tfinltfin 4502	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 4503	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 4504	The set of all even naturals exists. (Contributed by SF, 20-Jan-2015.)
⊢ Evenfin ∈ V
Theorem	oddfinex 4505	The set of all odd naturals exists. (Contributed by SF, 20-Jan-2015.)
⊢ Oddfin ∈ V
Theorem	0ceven 4506	Cardinal zero is even. (Contributed by SF, 20-Jan-2015.)
⊢ 0c ∈ Evenfin
Theorem	evennn 4507	An even finite cardinal is a finite cardinal. (Contributed by SF, 20-Jan-2015.)
⊢ (A ∈ Evenfin → A ∈ Nn )
Theorem	oddnn 4508	An odd finite cardinal is a finite cardinal. (Contributed by SF, 20-Jan-2015.)
⊢ (A ∈ Oddfin → A ∈ Nn )
Theorem	evennnul 4509	An even number is nonempty. (Contributed by SF, 22-Jan-2015.)
⊢ (A ∈ Evenfin → A ≠ ∅)
Theorem	oddnnul 4510	An odd number is nonempty. (Contributed by SF, 22-Jan-2015.)
⊢ (A ∈ Oddfin → A ≠ ∅)
Theorem	sucevenodd 4511	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 4512	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 4513*	Alternate definition of even number. (Contributed by SF, 25-Jan-2015.)
⊢ Evenfin = {x ∣ ∃n ∈ Nn (x = (n +c n) ∧ (n +c n) ≠ ∅)}
Theorem	dfoddfin2 4514*	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 4515	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 4516*	Lemma for evenodddisj 4517. 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 4517	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 4518	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 4519	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 4520*	Lemma for nnadjoin 4521. Establish stratification. (Contributed by SF, 29-Jan-2015.)
⊢ {n ∣ ∀l ∈ n (y ∈ ∼ ∪l → {x ∣ ∃b ∈ l x = (b ∪ {y})} ∈ n)} ∈ V
Theorem	nnadjoin 4521*	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 4522	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 4523*	Lemma for nnpweq 4524. Establish stratification for induction. (Contributed by SF, 26-Jan-2015.)
⊢ {m ∣ ∀a ∈ m ∀b ∈ m ∃n ∈ Nn (℘a ∈ n ∧ ℘b ∈ n)} ∈ V
Theorem	nnpweq 4524*	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 4525	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 4526	The expression at the core of srelk 4525 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 4527	Equality theorem for the finite S relationship. (Contributed by SF, 27-Jan-2015.)
⊢ (A = B → ( Sfin (A, C) ↔ Sfin (B, C)))
Theorem	sfineq2 4528	Equality theorem for the finite S relationship. (Contributed by SF, 27-Jan-2015.)
⊢ (A = B → ( Sfin (C, A) ↔ Sfin (C, B)))
Theorem	sfin01 4529	Zero and one satisfy Sfin. Theorem X.1.42 of [Rosser] p. 530. (Contributed by SF, 30-Jan-2015.)
⊢ Sfin (0c, 1c)
Theorem	sfin112 4530	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 4531*	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 4532*	Lemma for sfintfin 4533. Set up induction stratification. (Contributed by SF, 31-Jan-2015.)
⊢ {m ∣ ∀n( Sfin (m, n) → Sfin ( Tfin m, Tfin n))} ∈ V
Theorem	sfintfin 4533	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 4534*	Lemma for tfinnn 4535. Establish stratification. (Contributed by SF, 30-Jan-2015.)
⊢ {n ∣ ∀y ∈ n (y ⊆ Nn → {a ∣ ∃x ∈ y a = Tfin x} ∈ Tfin n)} ∈ V
Theorem	tfinnn 4535*	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 4536	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 4537	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 4538	Spfin is a set. (Contributed by SF, 20-Jan-2015.)
⊢ Spfin ∈ V
Theorem	ncvspfin 4539	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 4540	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 4541*	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 4542	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 4543	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 4544	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 4545	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 4546	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 4547	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 4548	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 4549	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 4550*	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 4551*	Lemma for vfinspss 4552. 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 4552*	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 4553	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 4554*	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 4555	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 4556	The universe is infinite. Theorem X.1.63 of [Rosser] p. 536. (Contributed by SF, 20-Jan-2015.)
⊢ ¬ V ∈ Fin
Theorem	nulnnn 4557	The empty class is not a natural. Theorem X.1.65 of [Rosser] p. 536. (Contributed by SF, 20-Jan-2015.)
⊢ ¬ ∅ ∈ Nn
Theorem	peano4 4558	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 4559	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 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))
Theorem	addccan1 4561	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 4562	Declare the syntax for an ordered pair.
class ⟨A, B⟩
Syntax	cphi 4563	Declare the syntax for the Phi operation.
class Phi A
Syntax	cproj1 4564	Declare the syntax for the first projection operation.
class Proj1 A
Syntax	cproj2 4565	Declare the syntax for the second projection operation.
class Proj2 A
Definition	df-phi 4566*	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 4567*	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 4568*	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 4569*	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 4570	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 4571	Equality law for the Phi operation. (Contributed by SF, 3-Feb-2015.)
⊢ (A = B → Phi A = Phi B)
Theorem	phiexg 4572	The phi operator preserves sethood. (Contributed by SF, 3-Feb-2015.)
⊢ (A ∈ V → Phi A ∈ V)
Theorem	phiex 4573	The phi operator preserves sethood. (Contributed by SF, 3-Feb-2015.)
⊢ A ∈ V    ⇒   ⊢ Phi A ∈ V
Theorem	dfop2lem1 4574*	Lemma for dfop2 4576 and dfproj22 4578. (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 4575*	Lemma for dfop2 4576. (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 4576	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 4577	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 4578	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 4579	Equality theorem for ordered pairs. (Contributed by SF, 2-Jan-2015.)
⊢ (A = B → ⟨A, C⟩ = ⟨B, C⟩)
Theorem	opeq2 4580	Equality theorem for ordered pairs. (Contributed by SF, 2-Jan-2015.)
⊢ (A = B → ⟨C, A⟩ = ⟨C, B⟩)
Theorem	opeq12 4581	Equality theorem for ordered pairs. (Contributed by SF, 2-Jan-2015.)
⊢ ((A = B ∧ C = D) → ⟨A, C⟩ = ⟨B, D⟩)
Theorem	opeq1i 4582	Equality inference for ordered pairs. (Contributed by SF, 16-Dec-2006.)
⊢ A = B    ⇒   ⊢ ⟨A, C⟩ = ⟨B, C⟩
Theorem	opeq2i 4583	Equality inference for ordered pairs. (Contributed by SF, 16-Dec-2006.)
⊢ A = B    ⇒   ⊢ ⟨C, A⟩ = ⟨C, B⟩
Theorem	opeq12i 4584	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 4585	Equality deduction for ordered pairs. (Contributed by SF, 16-Dec-2006.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → ⟨A, C⟩ = ⟨B, C⟩)
Theorem	opeq2d 4586	Equality deduction for ordered pairs. (Contributed by SF, 16-Dec-2006.)
⊢ (φ → A = B)    ⇒   ⊢ (φ → ⟨C, A⟩ = ⟨C, B⟩)
Theorem	opeq12d 4587	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 4588	An ordered pair of two sets is a set. (Contributed by SF, 2-Jan-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → ⟨A, B⟩ ∈ V)
Theorem	opex 4589	An ordered pair of two sets is a set. (Contributed by SF, 5-Jan-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ⟨A, B⟩ ∈ V
Theorem	proj1eq 4590	Equality theorem for first projection operator. (Contributed by SF, 2-Jan-2015.)
⊢ (A = B → Proj1 A = Proj1 B)
Theorem	proj2eq 4591	Equality theorem for second projection operator. (Contributed by SF, 2-Jan-2015.)
⊢ (A = B → Proj2 A = Proj2 B)
Theorem	proj1exg 4592	The first projection of a set is a set. (Contributed by SF, 2-Jan-2015.)
⊢ (A ∈ V → Proj1 A ∈ V)
Theorem	proj2exg 4593	The second projection of a set is a set. (Contributed by SF, 2-Jan-2015.)
⊢ (A ∈ V → Proj2 A ∈ V)
Theorem	proj1ex 4594	The first projection of a set is a set. (Contributed by Scott Fenton, 16-Apr-2021.)
⊢ A ∈ V    ⇒   ⊢ Proj1 A ∈ V
Theorem	proj2ex 4595	The second projection of a set is a set. (Contributed by Scott Fenton, 16-Apr-2021.)
⊢ A ∈ V    ⇒   ⊢ Proj2 A ∈ V
Theorem	phi11lem1 4596	Lemma for phi11 4597. (Contributed by SF, 3-Feb-2015.)
⊢ ( Phi A = Phi B → A ⊆ B)
Theorem	phi11 4597	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 4598	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 4599	Lemma for phi011 4600. (Contributed by SF, 3-Feb-2015.)
⊢ (( Phi A ∪ {0c}) = ( Phi B ∪ {0c}) → Phi A ⊆ Phi B)
Theorem	phi011 4600	( 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}))