P. 109 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 10801-10900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	grusn 10801	A Grothendieck universe contains the singletons of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈) → {𝐴} ∈ 𝑈)
Theorem	gruop 10802	A Grothendieck universe contains ordered pairs of its elements. (Contributed by Mario Carneiro, 10-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → ⟨𝐴, 𝐵⟩ ∈ 𝑈)
Theorem	gruun 10803	A Grothendieck universe contains binary unions of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 ∪ 𝐵) ∈ 𝑈)
Theorem	gruxp 10804	A Grothendieck universe contains binary cartesian products of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 × 𝐵) ∈ 𝑈)
Theorem	grumap 10805	A Grothendieck universe contains all powers of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈) → (𝐴 ↑m 𝐵) ∈ 𝑈)
Theorem	gruixp 10806*	A Grothendieck universe contains indexed cartesian products of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) → X𝑥 ∈ 𝐴 𝐵 ∈ 𝑈)
Theorem	gruiin 10807*	A Grothendieck universe contains indexed intersections of its elements. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ ∃𝑥 ∈ 𝐴 𝐵 ∈ 𝑈) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈)
Theorem	gruf 10808	A Grothendieck universe contains all functions on its elements. (Contributed by Mario Carneiro, 10-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹:𝐴⟶𝑈) → 𝐹 ∈ 𝑈)
Theorem	gruen 10809	A Grothendieck universe contains all subsets of itself that are equipotent to an element of the universe. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ⊆ 𝑈 ∧ (𝐵 ∈ 𝑈 ∧ 𝐵 ≈ 𝐴)) → 𝐴 ∈ 𝑈)
Theorem	gruwun 10810	A nonempty Grothendieck universe is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017.)
⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝑈 ∈ WUni)
Theorem	intgru 10811	The intersection of a family of universes is a universe. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ ((𝐴 ⊆ Univ ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ Univ)
Theorem	ingru 10812*	The intersection of a universe with a class that acts like a universe is another universe. (Contributed by Mario Carneiro, 10-Jun-2013.)
⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝒫 𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ 𝐴 {𝑥, 𝑦} ∈ 𝐴 ∧ ∀𝑦(𝑦:𝑥⟶𝐴 → ∪ ran 𝑦 ∈ 𝐴))) → (𝑈 ∈ Univ → (𝑈 ∩ 𝐴) ∈ Univ))
Theorem	wfgru 10813	The wellfounded part of a universe is another universe. (Contributed by Mario Carneiro, 17-Jun-2013.)
⊢ (𝑈 ∈ Univ → (𝑈 ∩ ∪ (𝑅1 “ On)) ∈ Univ)
Theorem	grudomon 10814	Each ordinal that is comparable with an element of the universe is in the universe. (Contributed by Mario Carneiro, 10-Jun-2013.)
⊢ ((𝑈 ∈ Univ ∧ 𝐴 ∈ On ∧ (𝐵 ∈ 𝑈 ∧ 𝐴 ≼ 𝐵)) → 𝐴 ∈ 𝑈)
Theorem	gruina 10815	If a Grothendieck universe 𝑈 is nonempty, then the height of the ordinals in 𝑈 is a strongly inaccessible cardinal. (Contributed by Mario Carneiro, 17-Jun-2013.)
⊢ 𝐴 = (𝑈 ∩ On)    ⇒   ⊢ ((𝑈 ∈ Univ ∧ 𝑈 ≠ ∅) → 𝐴 ∈ Inacc)
Theorem	grur1a 10816	A characterization of Grothendieck universes, part 1. (Contributed by Mario Carneiro, 23-Jun-2013.)
⊢ 𝐴 = (𝑈 ∩ On)    ⇒   ⊢ (𝑈 ∈ Univ → (𝑅1‘𝐴) ⊆ 𝑈)
Theorem	grur1 10817	A characterization of Grothendieck universes, part 2. (Contributed by Mario Carneiro, 24-Jun-2013.)
⊢ 𝐴 = (𝑈 ∩ On)    ⇒   ⊢ ((𝑈 ∈ Univ ∧ 𝑈 ∈ ∪ (𝑅1 “ On)) → 𝑈 = (𝑅1‘𝐴))
Theorem	grutsk1 10818	Grothendieck universes are the same as transitive Tarski classes, part one: a transitive Tarski class is a universe. (The hard work is in tskuni 10780.) (Contributed by Mario Carneiro, 17-Jun-2013.)
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇) → 𝑇 ∈ Univ)
Theorem	grutsk 10819	Grothendieck universes are the same as transitive Tarski classes. (The proof in the forward direction requires Foundation.) (Contributed by Mario Carneiro, 24-Jun-2013.)
⊢ Univ = {𝑥 ∈ Tarski ∣ Tr 𝑥}
4.2  ZFC Set Theory plus the Tarski-Grothendieck Axiom
4.2.1  Introduce the Tarski-Grothendieck Axiom
Axiom	ax-groth 10820*	The Tarski-Grothendieck Axiom. For every set 𝑥 there is an inaccessible cardinal 𝑦 such that 𝑦 is not in 𝑥. The addition of this axiom to ZFC set theory provides a framework for category theory, thus for all practical purposes giving us a complete foundation for "all of mathematics". This version of the axiom is used by the Mizar project (http://www.mizar.org/JFM/Axiomatics/tarski.html). Unlike the ZFC axioms, this axiom is very long when expressed in terms of primitive symbols (see grothprim 10831). An open problem is finding a shorter equivalent. (Contributed by NM, 18-Mar-2007.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → (𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦)))
Theorem	axgroth5 10821*	The Tarski-Grothendieck axiom using abbreviations. (Contributed by NM, 22-Jun-2009.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ ∃𝑤 ∈ 𝑦 𝒫 𝑧 ⊆ 𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≈ 𝑦 ∨ 𝑧 ∈ 𝑦))
Theorem	axgroth2 10822*	Alternate version of the Tarski-Grothendieck Axiom. (Contributed by NM, 18-Mar-2007.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → (𝑦 ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)))
4.2.2  Derive the Power Set, Infinity and Choice Axioms
Theorem	grothpw 10823*	Derive the Axiom of Power Sets ax-pow 5363 from the Tarski-Grothendieck axiom ax-groth 10820. That it follows is mentioned by Bob Solovay at http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html 10820. Note that ax-pow 5363 is not used by the proof. (Contributed by Gérard Lang, 22-Jun-2009.) (New usage is discouraged.)
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)
Theorem	grothpwex 10824	Derive the Axiom of Power Sets from the Tarski-Grothendieck axiom ax-groth 10820. Note that ax-pow 5363 is not used by the proof. Use axpweq 5348 to obtain ax-pow 5363. Use pwex 5378 or pwexg 5376 instead. (Contributed by Gérard Lang, 22-Jun-2009.) (New usage is discouraged.)
⊢ 𝒫 𝑥 ∈ V
Theorem	axgroth6 10825*	The Tarski-Grothendieck axiom using abbreviations. This version is called Tarski's axiom: given a set 𝑥, there exists a set 𝑦 containing 𝑥, the subsets of the members of 𝑦, the power sets of the members of 𝑦, and the subsets of 𝑦 of cardinality less than that of 𝑦. (Contributed by NM, 21-Jun-2009.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦))
Theorem	grothomex 10826	The Tarski-Grothendieck Axiom implies the Axiom of Infinity (in the form of omex 9640). Note that our proof depends on neither the Axiom of Infinity nor Regularity. (Contributed by Mario Carneiro, 19-Apr-2013.) (New usage is discouraged.)
⊢ ω ∈ V
Theorem	grothac 10827	The Tarski-Grothendieck Axiom implies the Axiom of Choice (in the form of cardeqv 10466). This can be put in a more conventional form via ween 10032 and dfac8 10132. Note that the mere existence of strongly inaccessible cardinals doesn't imply AC, but rather the particular form of the Tarski-Grothendieck axiom (see http://www.cs.nyu.edu/pipermail/fom/2008-March/012783.html 10132). (Contributed by Mario Carneiro, 19-Apr-2013.) (New usage is discouraged.)
⊢ dom card = V
Theorem	axgroth3 10828*	Alternate version of the Tarski-Grothendieck Axiom. ax-cc 10432 is used to derive this version. (Contributed by NM, 26-Mar-2007.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦) ∧ ∃𝑤 ∈ 𝑦 ∀𝑣(𝑣 ⊆ 𝑧 → 𝑣 ∈ 𝑤)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)))
Theorem	axgroth4 10829*	Alternate version of the Tarski-Grothendieck Axiom. ax-ac 10456 is used to derive this version. (Contributed by NM, 16-Apr-2007.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑣 ∈ 𝑦 ∀𝑤(𝑤 ⊆ 𝑧 → 𝑤 ∈ (𝑦 ∩ 𝑣)) ∧ ∀𝑧(𝑧 ⊆ 𝑦 → ((𝑦 ∖ 𝑧) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦)))
Theorem	grothprimlem 10830*	Lemma for grothprim 10831. Expand the membership of an unordered pair into primitives. (Contributed by NM, 29-Mar-2007.)
⊢ ({𝑢, 𝑣} ∈ 𝑤 ↔ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))
Theorem	grothprim 10831*	The Tarski-Grothendieck Axiom ax-groth 10820 expanded into set theory primitives using 163 symbols (allowing the defined symbols ∧, ∨, ↔, and ∃). An open problem is whether a shorter equivalent exists (when expanded to primitives). (Contributed by NM, 16-Apr-2007.)
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧((𝑧 ∈ 𝑦 → ∃𝑣(𝑣 ∈ 𝑦 ∧ ∀𝑤(∀𝑢(𝑢 ∈ 𝑤 → 𝑢 ∈ 𝑧) → (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣)))) ∧ ∃𝑤((𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦) → (∀𝑣((𝑣 ∈ 𝑧 → ∃𝑡∀𝑢(∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑣 ∨ ℎ = 𝑢))) → 𝑢 = 𝑡)) ∧ (𝑣 ∈ 𝑦 → (𝑣 ∈ 𝑧 ∨ ∃𝑢(𝑢 ∈ 𝑧 ∧ ∃𝑔(𝑔 ∈ 𝑤 ∧ ∀ℎ(ℎ ∈ 𝑔 ↔ (ℎ = 𝑢 ∨ ℎ = 𝑣))))))) ∨ 𝑧 ∈ 𝑦))))
Theorem	grothtsk 10832	The Tarski-Grothendieck Axiom, using abbreviations. (Contributed by Mario Carneiro, 28-May-2013.)
⊢ ∪ Tarski = V
Theorem	inaprc 10833	An equivalent to the Tarski-Grothendieck Axiom: there is a proper class of inaccessible cardinals. (Contributed by Mario Carneiro, 9-Jun-2013.)
⊢ Inacc ∉ V
4.2.3  Tarski map function
Syntax	ctskm 10834	Extend class definition to include the map whose value is the smallest Tarski class.
class tarskiMap
Definition	df-tskm 10835*	A function that maps a set 𝑥 to the smallest Tarski class that contains the set. (Contributed by FL, 30-Dec-2010.)
⊢ tarskiMap = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ Tarski ∣ 𝑥 ∈ 𝑦})
Theorem	tskmval 10836*	Value of our tarski map. (Contributed by FL, 30-Dec-2010.) (Revised by Mario Carneiro, 20-Sep-2014.)
⊢ (𝐴 ∈ 𝑉 → (tarskiMap‘𝐴) = ∩ {𝑥 ∈ Tarski ∣ 𝐴 ∈ 𝑥})
Theorem	tskmid 10837	The set 𝐴 is an element of the smallest Tarski class that contains 𝐴. CLASSES1 th. 5. (Contributed by FL, 30-Dec-2010.) (Proof shortened by Mario Carneiro, 21-Sep-2014.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ (tarskiMap‘𝐴))
Theorem	tskmcl 10838	A Tarski class that contains 𝐴 is a Tarski class. (Contributed by FL, 17-Apr-2011.) (Proof shortened by Mario Carneiro, 21-Sep-2014.)
⊢ (tarskiMap‘𝐴) ∈ Tarski
Theorem	sstskm 10839*	Being a part of (tarskiMap‘𝐴). (Contributed by FL, 17-Apr-2011.) (Proof shortened by Mario Carneiro, 20-Sep-2014.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ⊆ (tarskiMap‘𝐴) ↔ ∀𝑥 ∈ Tarski (𝐴 ∈ 𝑥 → 𝐵 ⊆ 𝑥)))
Theorem	eltskm 10840*	Belonging to (tarskiMap‘𝐴). (Contributed by FL, 17-Apr-2011.) (Proof shortened by Mario Carneiro, 21-Sep-2014.)
⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ (tarskiMap‘𝐴) ↔ ∀𝑥 ∈ Tarski (𝐴 ∈ 𝑥 → 𝐵 ∈ 𝑥)))
PART 5  REAL AND COMPLEX NUMBERS This section derives the basics of real and complex numbers. We first construct and axiomatize real and complex numbers (e.g., ax-resscn 11169). After that, we derive their basic properties, various operations like addition (df-add 11123) and sine (df-sin 16015), and subsets such as the integers (df-z 12561) and natural numbers (df-nn 12215).
5.1  Construction and axiomatization of real and complex numbers
5.1.1  Dedekind-cut construction of real and complex numbers
Syntax	cnpi 10841	The set of positive integers, which is the set of natural numbers ω with 0 removed. Note: This is the start of the Dedekind-cut construction of real and complex numbers. The last lemma of the construction is mulcnsrec 11141. The actual set of Dedekind cuts is defined by df-np 10978.
class N
Syntax	cpli 10842	Positive integer addition.
class +N
Syntax	cmi 10843	Positive integer multiplication.
class ·N
Syntax	clti 10844	Positive integer ordering relation.
class <N
Syntax	cplpq 10845	Positive pre-fraction addition.
class +pQ
Syntax	cmpq 10846	Positive pre-fraction multiplication.
class ·pQ
Syntax	cltpq 10847	Positive pre-fraction ordering relation.
class <pQ
Syntax	ceq 10848	Equivalence class used to construct positive fractions.
class ~Q
Syntax	cnq 10849	Set of positive fractions.
class Q
Syntax	c1q 10850	The positive fraction constant 1.
class 1Q
Syntax	cerq 10851	Positive fraction equivalence class.
class [Q]
Syntax	cplq 10852	Positive fraction addition.
class +Q
Syntax	cmq 10853	Positive fraction multiplication.
class ·Q
Syntax	crq 10854	Positive fraction reciprocal operation.
class *Q
Syntax	cltq 10855	Positive fraction ordering relation.
class <Q
Syntax	cnp 10856	Set of positive reals.
class P
Syntax	c1p 10857	Positive real constant 1.
class 1P
Syntax	cpp 10858	Positive real addition.
class +P
Syntax	cmp 10859	Positive real multiplication.
class ·P
Syntax	cltp 10860	Positive real ordering relation.
class <P
Syntax	cer 10861	Equivalence class used to construct signed reals.
class ~R
Syntax	cnr 10862	Set of signed reals.
class R
Syntax	c0r 10863	The signed real constant 0.
class 0R
Syntax	c1r 10864	The signed real constant 1.
class 1R
Syntax	cm1r 10865	The signed real constant -1.
class -1R
Syntax	cplr 10866	Signed real addition.
class +R
Syntax	cmr 10867	Signed real multiplication.
class ·R
Syntax	cltr 10868	Signed real ordering relation.
class <R
Definition	df-ni 10869	Define the class of positive integers. This is a "temporary" set used in the construction of complex numbers df-c 11118, and is intended to be used only by the construction. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
⊢ N = (ω ∖ {∅})
Definition	df-pli 10870	Define addition on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 11118, and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
⊢ +N = ( +o ↾ (N × N))
Definition	df-mi 10871	Define multiplication on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 11118, and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
⊢ ·N = ( ·o ↾ (N × N))
Definition	df-lti 10872	Define 'less than' on positive integers. This is a "temporary" set used in the construction of complex numbers df-c 11118, and is intended to be used only by the construction. (Contributed by NM, 6-Feb-1996.) (New usage is discouraged.)
⊢ <N = ( E ∩ (N × N))
Theorem	elni 10873	Membership in the class of positive integers. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ 𝐴 ≠ ∅))
Theorem	elni2 10874	Membership in the class of positive integers. (Contributed by NM, 27-Nov-1995.) (New usage is discouraged.)
⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ ∅ ∈ 𝐴))
Theorem	pinn 10875	A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
⊢ (𝐴 ∈ N → 𝐴 ∈ ω)
Theorem	pion 10876	A positive integer is an ordinal number. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ N → 𝐴 ∈ On)
Theorem	piord 10877	A positive integer is ordinal. (Contributed by NM, 29-Jan-1996.) (New usage is discouraged.)
⊢ (𝐴 ∈ N → Ord 𝐴)
Theorem	niex 10878	The class of positive integers is a set. (Contributed by NM, 15-Aug-1995.) (New usage is discouraged.)
⊢ N ∈ V
Theorem	0npi 10879	The empty set is not a positive integer. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
⊢ ¬ ∅ ∈ N
Theorem	1pi 10880	Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.) (New usage is discouraged.)
⊢ 1o ∈ N
Theorem	addpiord 10881	Positive integer addition in terms of ordinal addition. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 +N 𝐵) = (𝐴 +o 𝐵))
Theorem	mulpiord 10882	Positive integer multiplication in terms of ordinal multiplication. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 ·N 𝐵) = (𝐴 ·o 𝐵))
Theorem	mulidpi 10883	1 is an identity element for multiplication on positive integers. (Contributed by NM, 4-Mar-1996.) (Revised by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.)
⊢ (𝐴 ∈ N → (𝐴 ·N 1o) = 𝐴)
Theorem	ltpiord 10884	Positive integer 'less than' in terms of ordinal membership. (Contributed by NM, 6-Feb-1996.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 <N 𝐵 ↔ 𝐴 ∈ 𝐵))
Theorem	ltsopi 10885	Positive integer 'less than' is a strict ordering. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.)
⊢ <N Or N
Theorem	ltrelpi 10886	Positive integer 'less than' is a relation on positive integers. (Contributed by NM, 8-Feb-1996.) (New usage is discouraged.)
⊢ <N ⊆ (N × N)
Theorem	dmaddpi 10887	Domain of addition on positive integers. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
⊢ dom +N = (N × N)
Theorem	dmmulpi 10888	Domain of multiplication on positive integers. (Contributed by NM, 26-Aug-1995.) (New usage is discouraged.)
⊢ dom ·N = (N × N)
Theorem	addclpi 10889	Closure of addition of positive integers. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 +N 𝐵) ∈ N)
Theorem	mulclpi 10890	Closure of multiplication of positive integers. (Contributed by NM, 18-Oct-1995.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 ·N 𝐵) ∈ N)
Theorem	addcompi 10891	Addition of positive integers is commutative. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
⊢ (𝐴 +N 𝐵) = (𝐵 +N 𝐴)
Theorem	addasspi 10892	Addition of positive integers is associative. (Contributed by NM, 27-Aug-1995.) (New usage is discouraged.)
⊢ ((𝐴 +N 𝐵) +N 𝐶) = (𝐴 +N (𝐵 +N 𝐶))
Theorem	mulcompi 10893	Multiplication of positive integers is commutative. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.)
⊢ (𝐴 ·N 𝐵) = (𝐵 ·N 𝐴)
Theorem	mulasspi 10894	Multiplication of positive integers is associative. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.)
⊢ ((𝐴 ·N 𝐵) ·N 𝐶) = (𝐴 ·N (𝐵 ·N 𝐶))
Theorem	distrpi 10895	Multiplication of positive integers is distributive. (Contributed by NM, 21-Sep-1995.) (New usage is discouraged.)
⊢ (𝐴 ·N (𝐵 +N 𝐶)) = ((𝐴 ·N 𝐵) +N (𝐴 ·N 𝐶))
Theorem	addcanpi 10896	Addition cancellation law for positive integers. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → ((𝐴 +N 𝐵) = (𝐴 +N 𝐶) ↔ 𝐵 = 𝐶))
Theorem	mulcanpi 10897	Multiplication cancellation law for positive integers. (Contributed by NM, 4-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → ((𝐴 ·N 𝐵) = (𝐴 ·N 𝐶) ↔ 𝐵 = 𝐶))
Theorem	addnidpi 10898	There is no identity element for addition on positive integers. (Contributed by NM, 28-Nov-1995.) (New usage is discouraged.)
⊢ (𝐴 ∈ N → ¬ (𝐴 +N 𝐵) = 𝐴)
Theorem	ltexpi 10899*	Ordering on positive integers in terms of existence of sum. (Contributed by NM, 15-Mar-1996.) (Revised by Mario Carneiro, 14-Jun-2013.) (New usage is discouraged.)
⊢ ((𝐴 ∈ N ∧ 𝐵 ∈ N) → (𝐴 <N 𝐵 ↔ ∃𝑥 ∈ N (𝐴 +N 𝑥) = 𝐵))
Theorem	ltapi 10900	Ordering property of addition for positive integers. (Contributed by NM, 7-Mar-1996.) (New usage is discouraged.)
⊢ (𝐶 ∈ N → (𝐴 <N 𝐵 ↔ (𝐶 +N 𝐴) <N (𝐶 +N 𝐵)))