P. 45 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 4401-4500   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-se 4401*	Define the set-like predicate. (Contributed by Mario Carneiro, 19-Nov-2014.)
⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑥} ∈ V)
Definition	df-wetr 4402*	Define the well-ordering predicate. It is unusual to define "well-ordering" in the absence of excluded middle, but we mean an ordering which is like the ordering which we have for ordinals (for example, it does not entail trichotomy because ordinals do not have that as seen at ordtriexmid 4590). Given excluded middle, well-ordering is usually defined to require trichotomy (and the definition of Fr is typically also different). (Contributed by Mario Carneiro and Jim Kingdon, 23-Sep-2021.)
⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
Theorem	seex 4403*	The 𝑅-preimage of an element of the base set in a set-like relation is a set. (Contributed by Mario Carneiro, 19-Nov-2014.)
⊢ ((𝑅 Se 𝐴 ∧ 𝐵 ∈ 𝐴) → {𝑥 ∈ 𝐴 ∣ 𝑥𝑅𝐵} ∈ V)
Theorem	exse 4404	Any relation on a set is set-like on it. (Contributed by Mario Carneiro, 22-Jun-2015.)
⊢ (𝐴 ∈ 𝑉 → 𝑅 Se 𝐴)
Theorem	sess1 4405	Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ (𝑅 ⊆ 𝑆 → (𝑆 Se 𝐴 → 𝑅 Se 𝐴))
Theorem	sess2 4406	Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ (𝐴 ⊆ 𝐵 → (𝑅 Se 𝐵 → 𝑅 Se 𝐴))
Theorem	seeq1 4407	Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ (𝑅 = 𝑆 → (𝑅 Se 𝐴 ↔ 𝑆 Se 𝐴))
Theorem	seeq2 4408	Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ (𝐴 = 𝐵 → (𝑅 Se 𝐴 ↔ 𝑅 Se 𝐵))
Theorem	nfse 4409	Bound-variable hypothesis builder for set-like relations. (Contributed by Mario Carneiro, 24-Jun-2015.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝑅 Se 𝐴
Theorem	epse 4410	The epsilon relation is set-like on any class. (This is the origin of the term "set-like": a set-like relation "acts like" the epsilon relation of sets and their elements.) (Contributed by Mario Carneiro, 22-Jun-2015.)
⊢ E Se 𝐴
Theorem	frforeq1 4411	Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.)
⊢ (𝑅 = 𝑆 → ( FrFor 𝑅𝐴𝑇 ↔ FrFor 𝑆𝐴𝑇))
Theorem	freq1 4412	Equality theorem for the well-founded predicate. (Contributed by NM, 9-Mar-1997.)
⊢ (𝑅 = 𝑆 → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐴))
Theorem	frforeq2 4413	Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.)
⊢ (𝐴 = 𝐵 → ( FrFor 𝑅𝐴𝑇 ↔ FrFor 𝑅𝐵𝑇))
Theorem	freq2 4414	Equality theorem for the well-founded predicate. (Contributed by NM, 3-Apr-1994.)
⊢ (𝐴 = 𝐵 → (𝑅 Fr 𝐴 ↔ 𝑅 Fr 𝐵))
Theorem	frforeq3 4415	Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.)
⊢ (𝑆 = 𝑇 → ( FrFor 𝑅𝐴𝑆 ↔ FrFor 𝑅𝐴𝑇))
Theorem	nffrfor 4416	Bound-variable hypothesis builder for well-founded relations. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝑆    ⇒   ⊢ Ⅎ𝑥 FrFor 𝑅𝐴𝑆
Theorem	nffr 4417	Bound-variable hypothesis builder for well-founded relations. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝑅 Fr 𝐴
Theorem	frirrg 4418	A well-founded relation is irreflexive. This is the case where 𝐴 exists. (Contributed by Jim Kingdon, 21-Sep-2021.)
⊢ ((𝑅 Fr 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵)
Theorem	fr0 4419	Any relation is well-founded on the empty set. (Contributed by NM, 17-Sep-1993.)
⊢ 𝑅 Fr ∅
Theorem	frind 4420*	Induction over a well-founded set. (Contributed by Jim Kingdon, 28-Sep-2021.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝜓) → 𝜑))    &   ⊢ (𝜒 → 𝑅 Fr 𝐴)    &   ⊢ (𝜒 → 𝐴 ∈ 𝑉)    ⇒   ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐴) → 𝜑)
Theorem	efrirr 4421	Irreflexivity of the epsilon relation: a class founded by epsilon is not a member of itself. (Contributed by NM, 18-Apr-1994.) (Revised by Mario Carneiro, 22-Jun-2015.)
⊢ ( E Fr 𝐴 → ¬ 𝐴 ∈ 𝐴)
Theorem	tz7.2 4422	Similar to Theorem 7.2 of [TakeutiZaring] p. 35, of except that the Axiom of Regularity is not required due to antecedent E Fr 𝐴. (Contributed by NM, 4-May-1994.)
⊢ ((Tr 𝐴 ∧ E Fr 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ 𝐴))
Theorem	nfwe 4423	Bound-variable hypothesis builder for well-orderings. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro, 14-Oct-2016.)
⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝑅 We 𝐴
Theorem	weeq1 4424	Equality theorem for the well-ordering predicate. (Contributed by NM, 9-Mar-1997.)
⊢ (𝑅 = 𝑆 → (𝑅 We 𝐴 ↔ 𝑆 We 𝐴))
Theorem	weeq2 4425	Equality theorem for the well-ordering predicate. (Contributed by NM, 3-Apr-1994.)
⊢ (𝐴 = 𝐵 → (𝑅 We 𝐴 ↔ 𝑅 We 𝐵))
Theorem	wefr 4426	A well-ordering is well-founded. (Contributed by NM, 22-Apr-1994.)
⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴)
Theorem	wepo 4427	A well-ordering is a partial ordering. (Contributed by Jim Kingdon, 23-Sep-2021.)
⊢ ((𝑅 We 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝑅 Po 𝐴)
Theorem	wetrep 4428*	An epsilon well-ordering is a transitive relation. (Contributed by NM, 22-Apr-1994.)
⊢ (( E We 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧) → 𝑥 ∈ 𝑧))
Theorem	we0 4429	Any relation is a well-ordering of the empty set. (Contributed by NM, 16-Mar-1997.)
⊢ 𝑅 We ∅
2.3.10  Ordinals
Syntax	word 4430	Extend the definition of a wff to include the ordinal predicate.
wff Ord 𝐴
Syntax	con0 4431	Extend the definition of a class to include the class of all ordinal numbers. (The 0 in the name prevents creating a file called con.html, which causes problems in Windows.)
class On
Syntax	wlim 4432	Extend the definition of a wff to include the limit ordinal predicate.
wff Lim 𝐴
Syntax	csuc 4433	Extend class notation to include the successor function.
class suc 𝐴
Definition	df-iord 4434*	Define the ordinal predicate, which is true for a class that is transitive and whose elements are transitive. Definition of ordinal in [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic". Some sources will define a notation for ordinal order corresponding to < and ≤ but we just use ∈ and ⊆ respectively. (Contributed by Jim Kingdon, 10-Oct-2018.) Use its alias dford3 4435 instead for naming consistency with set.mm. (New usage is discouraged.)
⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 Tr 𝑥))
Theorem	dford3 4435*	Alias for df-iord 4434. Use it instead of df-iord 4434 for naming consistency with set.mm. (Contributed by Jim Kingdon, 10-Oct-2018.)
⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 Tr 𝑥))
Definition	df-on 4436	Define the class of all ordinal numbers. Definition 7.11 of [TakeutiZaring] p. 38. (Contributed by NM, 5-Jun-1994.)
⊢ On = {𝑥 ∣ Ord 𝑥}
Definition	df-ilim 4437	Define the limit ordinal predicate, which is true for an ordinal that has the empty set as an element and is not a successor (i.e. that is the union of itself). Our definition combines the definition of Lim of [BellMachover] p. 471 and Exercise 1 of [TakeutiZaring] p. 42, and then changes 𝐴 ≠ ∅ to ∅ ∈ 𝐴 (which would be equivalent given the law of the excluded middle, but which is not for us). (Contributed by Jim Kingdon, 11-Nov-2018.) Use its alias dflim2 4438 instead for naming consistency with set.mm. (New usage is discouraged.)
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴))
Theorem	dflim2 4438	Alias for df-ilim 4437. Use it instead of df-ilim 4437 for naming consistency with set.mm. (Contributed by NM, 4-Nov-2004.)
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴))
Definition	df-suc 4439	Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1". Definition 7.22 of [TakeutiZaring] p. 41, who use "+ 1" to denote this function. Our definition is a generalization to classes. Although it is not conventional to use it with proper classes, it has no effect on a proper class (sucprc 4480). Some authors denote the successor operation with a prime (apostrophe-like) symbol, such as Definition 6 of [Suppes] p. 134 and the definition of successor in [Mendelson] p. 246 (who uses the symbol "Suc" as a predicate to mean "is a successor ordinal"). The definition of successor of [Enderton] p. 68 denotes the operation with a plus-sign superscript. (Contributed by NM, 30-Aug-1993.)
⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
Theorem	ordeq 4440	Equality theorem for the ordinal predicate. (Contributed by NM, 17-Sep-1993.)
⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
Theorem	elong 4441	An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ On ↔ Ord 𝐴))
Theorem	elon 4442	An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ On ↔ Ord 𝐴)
Theorem	eloni 4443	An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.)
⊢ (𝐴 ∈ On → Ord 𝐴)
Theorem	elon2 4444	An ordinal number is an ordinal set. (Contributed by NM, 8-Feb-2004.)
⊢ (𝐴 ∈ On ↔ (Ord 𝐴 ∧ 𝐴 ∈ V))
Theorem	limeq 4445	Equality theorem for the limit predicate. (Contributed by NM, 22-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))
Theorem	ordtr 4446	An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.)
⊢ (Ord 𝐴 → Tr 𝐴)
Theorem	ordelss 4447	An element of an ordinal class is a subset of it. (Contributed by NM, 30-May-1994.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴)
Theorem	trssord 4448	A transitive subclass of an ordinal class is ordinal. (Contributed by NM, 29-May-1994.)
⊢ ((Tr 𝐴 ∧ 𝐴 ⊆ 𝐵 ∧ Ord 𝐵) → Ord 𝐴)
Theorem	ordelord 4449	An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. (Contributed by NM, 23-Apr-1994.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵)
Theorem	tron 4450	The class of all ordinal numbers is transitive. (Contributed by NM, 4-May-2009.)
⊢ Tr On
Theorem	ordelon 4451	An element of an ordinal class is an ordinal number. (Contributed by NM, 26-Oct-2003.)
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On)
Theorem	onelon 4452	An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of [BellMachover] p. 469. (Contributed by NM, 26-Oct-2003.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On)
Theorem	ordin 4453	The intersection of two ordinal classes is ordinal. Proposition 7.9 of [TakeutiZaring] p. 37. (Contributed by NM, 9-May-1994.)
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → Ord (𝐴 ∩ 𝐵))
Theorem	onin 4454	The intersection of two ordinal numbers is an ordinal number. (Contributed by NM, 7-Apr-1995.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∩ 𝐵) ∈ On)
Theorem	onelss 4455	An element of an ordinal number is a subset of the number. (Contributed by NM, 5-Jun-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
Theorem	ordtr1 4456	Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.)
⊢ (Ord 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))
Theorem	ontr1 4457	Transitive law for ordinal numbers. Theorem 7M(b) of [Enderton] p. 192. (Contributed by NM, 11-Aug-1994.)
⊢ (𝐶 ∈ On → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))
Theorem	onintss 4458*	If a property is true for an ordinal number, then the minimum ordinal number for which it is true is smaller or equal. Theorem Schema 61 of [Suppes] p. 228. (Contributed by NM, 3-Oct-2003.)
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝐴 ∈ On → (𝜓 → ∩ {𝑥 ∈ On ∣ 𝜑} ⊆ 𝐴))
Theorem	ord0 4459	The empty set is an ordinal class. (Contributed by NM, 11-May-1994.)
⊢ Ord ∅
Theorem	0elon 4460	The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193. (Contributed by NM, 17-Sep-1993.)
⊢ ∅ ∈ On
Theorem	inton 4461	The intersection of the class of ordinal numbers is the empty set. (Contributed by NM, 20-Oct-2003.)
⊢ ∩ On = ∅
Theorem	nlim0 4462	The empty set is not a limit ordinal. (Contributed by NM, 24-Mar-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ ¬ Lim ∅
Theorem	limord 4463	A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.)
⊢ (Lim 𝐴 → Ord 𝐴)
Theorem	limuni 4464	A limit ordinal is its own supremum (union). (Contributed by NM, 4-May-1995.)
⊢ (Lim 𝐴 → 𝐴 = ∪ 𝐴)
Theorem	limuni2 4465	The union of a limit ordinal is a limit ordinal. (Contributed by NM, 19-Sep-2006.)
⊢ (Lim 𝐴 → Lim ∪ 𝐴)
Theorem	0ellim 4466	A limit ordinal contains the empty set. (Contributed by NM, 15-May-1994.)
⊢ (Lim 𝐴 → ∅ ∈ 𝐴)
Theorem	limelon 4467	A limit ordinal class that is also a set is an ordinal number. (Contributed by NM, 26-Apr-2004.)
⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → 𝐴 ∈ On)
Theorem	onn0 4468	The class of all ordinal numbers is not empty. (Contributed by NM, 17-Sep-1995.)
⊢ On ≠ ∅
Theorem	onm 4469	The class of all ordinal numbers is inhabited. (Contributed by Jim Kingdon, 6-Mar-2019.)
⊢ ∃𝑥 𝑥 ∈ On
Theorem	suceq 4470	Equality of successors. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝐴 = 𝐵 → suc 𝐴 = suc 𝐵)
Theorem	elsuci 4471	Membership in a successor. This one-way implication does not require that either 𝐴 or 𝐵 be sets. (Contributed by NM, 6-Jun-1994.)
⊢ (𝐴 ∈ suc 𝐵 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))
Theorem	elsucg 4472	Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-1995.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
Theorem	elsuc2g 4473	Variant of membership in a successor, requiring that 𝐵 rather than 𝐴 be a set. (Contributed by NM, 28-Oct-2003.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
Theorem	elsuc 4474	Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))
Theorem	elsuc2 4475	Membership in a successor. (Contributed by NM, 15-Sep-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ∈ suc 𝐴 ↔ (𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴))
Theorem	nfsuc 4476	Bound-variable hypothesis builder for successor. (Contributed by NM, 15-Sep-2003.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 suc 𝐴
Theorem	elelsuc 4477	Membership in a successor. (Contributed by NM, 20-Jun-1998.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ suc 𝐵)
Theorem	sucel 4478*	Membership of a successor in another class. (Contributed by NM, 29-Jun-2004.)
⊢ (suc 𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐵 ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)))
Theorem	suc0 4479	The successor of the empty set. (Contributed by NM, 1-Feb-2005.)
⊢ suc ∅ = {∅}
Theorem	sucprc 4480	A proper class is its own successor. (Contributed by NM, 3-Apr-1995.)
⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴)
Theorem	unisuc 4481	A transitive class is equal to the union of its successor. Combines Theorem 4E of [Enderton] p. 72 and Exercise 6 of [Enderton] p. 73. (Contributed by NM, 30-Aug-1993.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (Tr 𝐴 ↔ ∪ suc 𝐴 = 𝐴)
Theorem	unisucg 4482	A transitive class is equal to the union of its successor. Combines Theorem 4E of [Enderton] p. 72 and Exercise 6 of [Enderton] p. 73. (Contributed by Jim Kingdon, 18-Aug-2019.)
⊢ (𝐴 ∈ 𝑉 → (Tr 𝐴 ↔ ∪ suc 𝐴 = 𝐴))
Theorem	sssucid 4483	A class is included in its own successor. Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized to arbitrary classes). (Contributed by NM, 31-May-1994.)
⊢ 𝐴 ⊆ suc 𝐴
Theorem	sucidg 4484	Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized). (Contributed by NM, 25-Mar-1995.) (Proof shortened by Scott Fenton, 20-Feb-2012.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ suc 𝐴)
Theorem	sucid 4485	A set belongs to its successor. (Contributed by NM, 22-Jun-1994.) (Proof shortened by Alan Sare, 18-Feb-2012.) (Proof shortened by Scott Fenton, 20-Feb-2012.)
⊢ 𝐴 ∈ V    ⇒   ⊢ 𝐴 ∈ suc 𝐴
Theorem	nsuceq0g 4486	No successor is empty. (Contributed by Jim Kingdon, 14-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → suc 𝐴 ≠ ∅)
Theorem	eqelsuc 4487	A set belongs to the successor of an equal set. (Contributed by NM, 18-Aug-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 = 𝐵 → 𝐴 ∈ suc 𝐵)
Theorem	iunsuc 4488*	Inductive definition for the indexed union at a successor. (Contributed by Mario Carneiro, 4-Feb-2013.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
⊢ 𝐴 ∈ V    &   ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)    ⇒   ⊢ ∪ 𝑥 ∈ suc 𝐴𝐵 = (∪ 𝑥 ∈ 𝐴 𝐵 ∪ 𝐶)
Theorem	suctr 4489	The successor of a transitive class is transitive. (Contributed by Alan Sare, 11-Apr-2009.)
⊢ (Tr 𝐴 → Tr suc 𝐴)
Theorem	trsuc 4490	A set whose successor belongs to a transitive class also belongs. (Contributed by NM, 5-Sep-2003.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
⊢ ((Tr 𝐴 ∧ suc 𝐵 ∈ 𝐴) → 𝐵 ∈ 𝐴)
Theorem	trsucss 4491	A member of the successor of a transitive class is a subclass of it. (Contributed by NM, 4-Oct-2003.)
⊢ (Tr 𝐴 → (𝐵 ∈ suc 𝐴 → 𝐵 ⊆ 𝐴))
Theorem	sucssel 4492	A set whose successor is a subset of another class is a member of that class. (Contributed by NM, 16-Sep-1995.)
⊢ (𝐴 ∈ 𝑉 → (suc 𝐴 ⊆ 𝐵 → 𝐴 ∈ 𝐵))
Theorem	orduniss 4493	An ordinal class includes its union. (Contributed by NM, 13-Sep-2003.)
⊢ (Ord 𝐴 → ∪ 𝐴 ⊆ 𝐴)
Theorem	onordi 4494	An ordinal number is an ordinal class. (Contributed by NM, 11-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ Ord 𝐴
Theorem	ontrci 4495	An ordinal number is a transitive class. (Contributed by NM, 11-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ Tr 𝐴
Theorem	oneli 4496	A member of an ordinal number is an ordinal number. Theorem 7M(a) of [Enderton] p. 192. (Contributed by NM, 11-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐵 ∈ 𝐴 → 𝐵 ∈ On)
Theorem	onelssi 4497	A member of an ordinal number is a subset of it. (Contributed by NM, 11-Aug-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)
Theorem	onelini 4498	An element of an ordinal number equals the intersection with it. (Contributed by NM, 11-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐵 ∈ 𝐴 → 𝐵 = (𝐵 ∩ 𝐴))
Theorem	oneluni 4499	An ordinal number equals its union with any element. (Contributed by NM, 13-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐵 ∈ 𝐴 → (𝐴 ∪ 𝐵) = 𝐴)
Theorem	onunisuci 4500	An ordinal number is equal to the union of its successor. (Contributed by NM, 12-Jun-1994.)
⊢ 𝐴 ∈ On    ⇒   ⊢ ∪ suc 𝐴 = 𝐴