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
Theorem	opabm 4401*	Inhabited ordered pair class abstraction. (Contributed by Jim Kingdon, 29-Sep-2018.)
⊢ (∃𝑧 𝑧 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥∃𝑦𝜑)
Theorem	iunopab 4402*	Move indexed union inside an ordered-pair abstraction. (Contributed by Stefan O'Rear, 20-Feb-2015.)
⊢ ∪ 𝑧 ∈ 𝐴 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 𝜑}
Theorem	elopabr 4403*	Membership in an ordered-pair class abstraction defined by a binary relation. (Contributed by AV, 16-Feb-2021.) (Proof shortened by SN, 11-Dec-2024.)
⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑅𝑦} → 𝐴 ∈ 𝑅)
Theorem	elopabran 4404*	Membership in an ordered-pair class abstraction defined by a restricted binary relation. (Contributed by AV, 16-Feb-2021.)
⊢ (𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑅𝑦 ∧ 𝜓)} → 𝐴 ∈ 𝑅)
2.3.6  Power class of union and intersection
Theorem	pwin 4405	The power class of the intersection of two classes is the intersection of their power classes. Exercise 4.12(j) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.)
⊢ 𝒫 (𝐴 ∩ 𝐵) = (𝒫 𝐴 ∩ 𝒫 𝐵)
Theorem	pwunss 4406	The power class of the union of two classes includes the union of their power classes. Exercise 4.12(k) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.)
⊢ (𝒫 𝐴 ∪ 𝒫 𝐵) ⊆ 𝒫 (𝐴 ∪ 𝐵)
Theorem	pwssunim 4407	The power class of the union of two classes is a subset of the union of their power classes, if one class is a subclass of the other. One direction of Exercise 4.12(l) of [Mendelson] p. 235. (Contributed by Jim Kingdon, 30-Sep-2018.)
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴) → 𝒫 (𝐴 ∪ 𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵))
Theorem	pwundifss 4408	Break up the power class of a union into a union of smaller classes. (Contributed by Jim Kingdon, 30-Sep-2018.)
⊢ ((𝒫 (𝐴 ∪ 𝐵) ∖ 𝒫 𝐴) ∪ 𝒫 𝐴) ⊆ 𝒫 (𝐴 ∪ 𝐵)
Theorem	pwunim 4409	The power class of the union of two classes equals the union of their power classes, iff one class is a subclass of the other. Part of Exercise 7(b) of [Enderton] p. 28. (Contributed by Jim Kingdon, 30-Sep-2018.)
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴) → 𝒫 (𝐴 ∪ 𝐵) = (𝒫 𝐴 ∪ 𝒫 𝐵))
2.3.7  Epsilon and identity relations
Syntax	cep 4410	Extend class notation to include the epsilon relation.
class E
Syntax	cid 4411	Extend the definition of a class to include identity relation.
class I
Definition	df-eprel 4412*	Define the epsilon relation. Similar to Definition 6.22 of [TakeutiZaring] p. 30. The epsilon relation and set membership are the same, that is, (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵) when 𝐵 is a set by epelg 4413. Thus, 5 E { 1 , 5 }. (Contributed by NM, 13-Aug-1995.)
⊢ E = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ∈ 𝑦}
Theorem	epelg 4413	The epsilon relation and membership are the same. General version of epel 4415. (Contributed by Scott Fenton, 27-Mar-2011.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵))
Theorem	epelc 4414	The epsilon relationship and the membership relation are the same. (Contributed by Scott Fenton, 11-Apr-2012.)
⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)
Theorem	epel 4415	The epsilon relation and the membership relation are the same. (Contributed by NM, 13-Aug-1995.)
⊢ (𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦)
Definition	df-id 4416*	Define the identity relation. Definition 9.15 of [Quine] p. 64. For example, 5 I 5 and ¬ 4 I 5. (Contributed by NM, 13-Aug-1995.)
⊢ I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦}
2.3.8  Partial and total orderings We have not yet defined relations (df-rel 4758), but here we introduce a few related notions we will use to develop ordinals. The class variable 𝑅 is no different from other class variables, but it reminds us that typically it represents what we will later call a "relation".
Syntax	wpo 4417	Extend wff notation to include the strict partial ordering predicate. Read: ' 𝑅 is a partial order on 𝐴.'
wff 𝑅 Po 𝐴
Syntax	wor 4418	Extend wff notation to include the strict linear ordering predicate. Read: ' 𝑅 orders 𝐴.'
wff 𝑅 Or 𝐴
Definition	df-po 4419*	Define the strict partial order predicate. Definition of [Enderton] p. 168. The expression 𝑅 Po 𝐴 means 𝑅 is a partial order on 𝐴. (Contributed by NM, 16-Mar-1997.)
⊢ (𝑅 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
Definition	df-iso 4420*	Define the strict linear order predicate. The expression 𝑅 Or 𝐴 is true if relationship 𝑅 orders 𝐴. The property 𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦) is called weak linearity by Proposition 11.2.3 of [HoTT], p. (varies). If we assumed excluded middle, it would be equivalent to trichotomy, 𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥. (Contributed by NM, 21-Jan-1996.) (Revised by Jim Kingdon, 4-Oct-2018.)
⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))))
Theorem	poss 4421	Subset theorem for the partial ordering predicate. (Contributed by NM, 27-Mar-1997.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
⊢ (𝐴 ⊆ 𝐵 → (𝑅 Po 𝐵 → 𝑅 Po 𝐴))
Theorem	poeq1 4422	Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
⊢ (𝑅 = 𝑆 → (𝑅 Po 𝐴 ↔ 𝑆 Po 𝐴))
Theorem	poeq2 4423	Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
⊢ (𝐴 = 𝐵 → (𝑅 Po 𝐴 ↔ 𝑅 Po 𝐵))
Theorem	nfpo 4424	Bound-variable hypothesis builder for partial orders. (Contributed by Stefan O'Rear, 20-Jan-2015.)
⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝑅 Po 𝐴
Theorem	nfso 4425	Bound-variable hypothesis builder for total orders. (Contributed by Stefan O'Rear, 20-Jan-2015.)
⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝐴    ⇒   ⊢ Ⅎ𝑥 𝑅 Or 𝐴
Theorem	pocl 4426	Properties of partial order relation in class notation. (Contributed by NM, 27-Mar-1997.)
⊢ (𝑅 Po 𝐴 → ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴) → (¬ 𝐵𝑅𝐵 ∧ ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷))))
Theorem	ispod 4427*	Sufficient conditions for a partial order. (Contributed by NM, 9-Jul-2014.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥𝑅𝑥)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))    ⇒   ⊢ (𝜑 → 𝑅 Po 𝐴)
Theorem	swopolem 4428*	Perform the substitutions into the strict weak ordering law. (Contributed by Mario Carneiro, 31-Dec-2014.)
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦)))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴)) → (𝑋𝑅𝑌 → (𝑋𝑅𝑍 ∨ 𝑍𝑅𝑌)))
Theorem	swopo 4429*	A strict weak order is a partial order. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑦𝑅𝑧 → ¬ 𝑧𝑅𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦)))    ⇒   ⊢ (𝜑 → 𝑅 Po 𝐴)
Theorem	poirr 4430	A partial order relation is irreflexive. (Contributed by NM, 27-Mar-1997.)
⊢ ((𝑅 Po 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵)
Theorem	potr 4431	A partial order relation is a transitive relation. (Contributed by NM, 27-Mar-1997.)
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷))
Theorem	po2nr 4432	A partial order relation has no 2-cycle loops. (Contributed by NM, 27-Mar-1997.)
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵))
Theorem	po3nr 4433	A partial order relation has no 3-cycle loops. (Contributed by NM, 27-Mar-1997.)
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵))
Theorem	po0 4434	Any relation is a partial ordering of the empty set. (Contributed by NM, 28-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ 𝑅 Po ∅
Theorem	pofun 4435*	A function preserves a partial order relation. (Contributed by Jeff Madsen, 18-Jun-2011.)
⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌}    &   ⊢ (𝑥 = 𝑦 → 𝑋 = 𝑌)    ⇒   ⊢ ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) → 𝑆 Po 𝐴)
Theorem	sopo 4436	A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997.)
⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴)
Theorem	soss 4437	Subset theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴))
Theorem	soeq1 4438	Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
⊢ (𝑅 = 𝑆 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐴))
Theorem	soeq2 4439	Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
⊢ (𝐴 = 𝐵 → (𝑅 Or 𝐴 ↔ 𝑅 Or 𝐵))
Theorem	sonr 4440	A strict order relation is irreflexive. (Contributed by NM, 24-Nov-1995.)
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵)
Theorem	sotr 4441	A strict order relation is a transitive relation. (Contributed by NM, 21-Jan-1996.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷))
Theorem	issod 4442*	An irreflexive, transitive, trichotomous relation is a linear ordering (in the sense of df-iso 4420). (Contributed by NM, 21-Jan-1996.) (Revised by Mario Carneiro, 9-Jul-2014.)
⊢ (𝜑 → 𝑅 Po 𝐴)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))    ⇒   ⊢ (𝜑 → 𝑅 Or 𝐴)
Theorem	sowlin 4443	A strict order relation satisfies weak linearity. (Contributed by Jim Kingdon, 6-Oct-2018.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐵𝑅𝐶 → (𝐵𝑅𝐷 ∨ 𝐷𝑅𝐶)))
Theorem	so2nr 4444	A strict order relation has no 2-cycle loops. (Contributed by NM, 21-Jan-1996.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵))
Theorem	so3nr 4445	A strict order relation has no 3-cycle loops. (Contributed by NM, 21-Jan-1996.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵))
Theorem	sotricim 4446	One direction of sotritric 4447 holds for all weakly linear orders. (Contributed by Jim Kingdon, 28-Sep-2019.)
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 → ¬ (𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)))
Theorem	sotritric 4447	A trichotomy relationship, given a trichotomous order. (Contributed by Jim Kingdon, 28-Sep-2019.)
⊢ 𝑅 Or 𝐴    &   ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))    ⇒   ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵𝑅𝐶 ↔ ¬ (𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)))
Theorem	sotritrieq 4448	A trichotomy relationship, given a trichotomous order. (Contributed by Jim Kingdon, 13-Dec-2019.)
⊢ 𝑅 Or 𝐴    &   ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))    ⇒   ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵 = 𝐶 ↔ ¬ (𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵)))
Theorem	so0 4449	Any relation is a strict ordering of the empty set. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ 𝑅 Or ∅
2.3.9  Founded and set-like relations
Syntax	wfrfor 4450	Extend wff notation to include the well-founded predicate.
wff FrFor 𝑅𝐴𝑆
Syntax	wfr 4451	Extend wff notation to include the well-founded predicate. Read: ' 𝑅 is a well-founded relation on 𝐴.'
wff 𝑅 Fr 𝐴
Syntax	wse 4452	Extend wff notation to include the set-like predicate. Read: ' 𝑅 is set-like on 𝐴.'
wff 𝑅 Se 𝐴
Syntax	wwe 4453	Extend wff notation to include the well-ordering predicate. Read: ' 𝑅 well-orders 𝐴.'
wff 𝑅 We 𝐴
Definition	df-frfor 4454*	Define the well-founded relation predicate where 𝐴 might be a proper class. By passing in 𝑆 we allow it potentially to be a proper class rather than a set. (Contributed by Jim Kingdon and Mario Carneiro, 22-Sep-2021.)
⊢ ( FrFor 𝑅𝐴𝑆 ↔ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆) → 𝑥 ∈ 𝑆) → 𝐴 ⊆ 𝑆))
Definition	df-frind 4455*	Define the well-founded relation predicate. In the presence of excluded middle, there are a variety of equivalent ways to define this. In our case, this definition, in terms of an inductive principle, works better than one along the lines of "there is an element which is minimal when A is ordered by R". Because 𝑠 is constrained to be a set (not a proper class) here, sometimes it may be necessary to use FrFor directly rather than via Fr. (Contributed by Jim Kingdon and Mario Carneiro, 21-Sep-2021.)
⊢ (𝑅 Fr 𝐴 ↔ ∀𝑠 FrFor 𝑅𝐴𝑠)
Definition	df-se 4456*	Define the set-like predicate. (Contributed by Mario Carneiro, 19-Nov-2014.)
⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑥} ∈ V)
Definition	df-wetr 4457*	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 4645). 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 4458*	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 4459	Any relation on a set is set-like on it. (Contributed by Mario Carneiro, 22-Jun-2015.)
⊢ (𝐴 ∈ 𝑉 → 𝑅 Se 𝐴)
Theorem	sess1 4460	Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ (𝑅 ⊆ 𝑆 → (𝑆 Se 𝐴 → 𝑅 Se 𝐴))
Theorem	sess2 4461	Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ (𝐴 ⊆ 𝐵 → (𝑅 Se 𝐵 → 𝑅 Se 𝐴))
Theorem	seeq1 4462	Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ (𝑅 = 𝑆 → (𝑅 Se 𝐴 ↔ 𝑆 Se 𝐴))
Theorem	seeq2 4463	Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ (𝐴 = 𝐵 → (𝑅 Se 𝐴 ↔ 𝑅 Se 𝐵))
Theorem	nfse 4464	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 4465	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 4466	Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.)
⊢ (𝑅 = 𝑆 → ( FrFor 𝑅𝐴𝑇 ↔ FrFor 𝑆𝐴𝑇))
Theorem	freq1 4467	Equality theorem for the well-founded predicate. (Contributed by NM, 9-Mar-1997.)
⊢ (𝑅 = 𝑆 → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐴))
Theorem	frforeq2 4468	Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.)
⊢ (𝐴 = 𝐵 → ( FrFor 𝑅𝐴𝑇 ↔ FrFor 𝑅𝐵𝑇))
Theorem	freq2 4469	Equality theorem for the well-founded predicate. (Contributed by NM, 3-Apr-1994.)
⊢ (𝐴 = 𝐵 → (𝑅 Fr 𝐴 ↔ 𝑅 Fr 𝐵))
Theorem	frforeq3 4470	Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.)
⊢ (𝑆 = 𝑇 → ( FrFor 𝑅𝐴𝑆 ↔ FrFor 𝑅𝐴𝑇))
Theorem	nffrfor 4471	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 4472	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 4473	A well-founded relation is irreflexive. This is the case where 𝐴 exists. (Contributed by Jim Kingdon, 21-Sep-2021.)
⊢ ((𝑅 Fr 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵)
Theorem	fr0 4474	Any relation is well-founded on the empty set. (Contributed by NM, 17-Sep-1993.)
⊢ 𝑅 Fr ∅
Theorem	frind 4475*	Induction over a well-founded set. (Contributed by Jim Kingdon, 28-Sep-2021.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝜓) → 𝜑))    &   ⊢ (𝜒 → 𝑅 Fr 𝐴)    &   ⊢ (𝜒 → 𝐴 ∈ 𝑉)    ⇒   ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐴) → 𝜑)
Theorem	efrirr 4476	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 4477	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 4478	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 4479	Equality theorem for the well-ordering predicate. (Contributed by NM, 9-Mar-1997.)
⊢ (𝑅 = 𝑆 → (𝑅 We 𝐴 ↔ 𝑆 We 𝐴))
Theorem	weeq2 4480	Equality theorem for the well-ordering predicate. (Contributed by NM, 3-Apr-1994.)
⊢ (𝐴 = 𝐵 → (𝑅 We 𝐴 ↔ 𝑅 We 𝐵))
Theorem	wefr 4481	A well-ordering is well-founded. (Contributed by NM, 22-Apr-1994.)
⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴)
Theorem	wepo 4482	A well-ordering is a partial ordering. (Contributed by Jim Kingdon, 23-Sep-2021.)
⊢ ((𝑅 We 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝑅 Po 𝐴)
Theorem	wetrep 4483*	An epsilon well-ordering is a transitive relation. (Contributed by NM, 22-Apr-1994.)
⊢ (( E We 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧) → 𝑥 ∈ 𝑧))
Theorem	we0 4484	Any relation is a well-ordering of the empty set. (Contributed by NM, 16-Mar-1997.)
⊢ 𝑅 We ∅
2.3.10  Ordinals
Syntax	word 4485	Extend the definition of a wff to include the ordinal predicate.
wff Ord 𝐴
Syntax	con0 4486	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 4487	Extend the definition of a wff to include the limit ordinal predicate.
wff Lim 𝐴
Syntax	csuc 4488	Extend class notation to include the successor function.
class suc 𝐴
Definition	df-iord 4489*	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 4490 instead for naming consistency with set.mm. (New usage is discouraged.)
⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 Tr 𝑥))
Theorem	dford3 4490*	Alias for df-iord 4489. Use it instead of df-iord 4489 for naming consistency with set.mm. (Contributed by Jim Kingdon, 10-Oct-2018.)
⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 Tr 𝑥))
Definition	df-on 4491	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 4492	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 4493 instead for naming consistency with set.mm. (New usage is discouraged.)
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴))
Theorem	dflim2 4493	Alias for df-ilim 4492. Use it instead of df-ilim 4492 for naming consistency with set.mm. (Contributed by NM, 4-Nov-2004.)
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴))
Definition	df-suc 4494	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 4535). 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 4495	Equality theorem for the ordinal predicate. (Contributed by NM, 17-Sep-1993.)
⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
Theorem	elong 4496	An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ On ↔ Ord 𝐴))
Theorem	elon 4497	An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ On ↔ Ord 𝐴)
Theorem	eloni 4498	An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.)
⊢ (𝐴 ∈ On → Ord 𝐴)
Theorem	elon2 4499	An ordinal number is an ordinal set. (Contributed by NM, 8-Feb-2004.)
⊢ (𝐴 ∈ On ↔ (Ord 𝐴 ∧ 𝐴 ∈ V))
Theorem	limeq 4500	Equality theorem for the limit predicate. (Contributed by NM, 22-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))