P. 98 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9701-9800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cnfcom3c 9701*	Wrap the construction of cnfcom3 9699 into an existential quantifier. For any ω ⊆ 𝑏, there is a bijection from 𝑏 to some power of ω. Furthermore, this bijection is canonical , which means that we can find a single function 𝑔 which will give such bijections for every 𝑏 less than some arbitrarily large bound 𝐴. (Contributed by Mario Carneiro, 30-May-2015.)
⊢ (𝐴 ∈ On → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑔‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)))
2.6.4  Transitive closure of a relation
Syntax	cttrcl 9702	Declare the syntax for the transitive closure of a class.
class t++𝑅
Definition	df-ttrcl 9703*	Define the transitive closure of a class. This is the smallest relation containing 𝑅 (or more precisely, the relation (𝑅 ↾ V) induced by 𝑅) and having the transitive property. Definition from [Levy] p. 59, who denotes it as 𝑅∗ and calls it the "ancestral" of 𝑅. (Contributed by Scott Fenton, 17-Oct-2024.)
⊢ t++𝑅 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝑥 ∧ (𝑓‘𝑛) = 𝑦) ∧ ∀𝑚 ∈ 𝑛 (𝑓‘𝑚)𝑅(𝑓‘suc 𝑚))}
Theorem	ttrcleq 9704	Equality theorem for transitive closure. (Contributed by Scott Fenton, 17-Oct-2024.)
⊢ (𝑅 = 𝑆 → t++𝑅 = t++𝑆)
Theorem	nfttrcld 9705	Bound variable hypothesis builder for transitive closure. Deduction form. (Contributed by Scott Fenton, 26-Oct-2024.)
⊢ (𝜑 → Ⅎ𝑥𝑅)    ⇒   ⊢ (𝜑 → Ⅎ𝑥t++𝑅)
Theorem	nfttrcl 9706	Bound variable hypothesis builder for transitive closure. (Contributed by Scott Fenton, 17-Oct-2024.)
⊢ Ⅎ𝑥𝑅    ⇒   ⊢ Ⅎ𝑥t++𝑅
Theorem	relttrcl 9707	The transitive closure of a class is a relation. (Contributed by Scott Fenton, 17-Oct-2024.)
⊢ Rel t++𝑅
Theorem	brttrcl 9708*	Characterization of elements of the transitive closure of a relation. (Contributed by Scott Fenton, 18-Aug-2024.)
⊢ (𝐴t++𝑅𝐵 ↔ ∃𝑛 ∈ (ω ∖ 1o)∃𝑓(𝑓 Fn suc 𝑛 ∧ ((𝑓‘∅) = 𝐴 ∧ (𝑓‘𝑛) = 𝐵) ∧ ∀𝑎 ∈ 𝑛 (𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
Theorem	brttrcl2 9709*	Characterization of elements of the transitive closure of a relation. (Contributed by Scott Fenton, 24-Aug-2024.)
⊢ (𝐴t++𝑅𝐵 ↔ ∃𝑛 ∈ ω ∃𝑓(𝑓 Fn suc suc 𝑛 ∧ ((𝑓‘∅) = 𝐴 ∧ (𝑓‘suc 𝑛) = 𝐵) ∧ ∀𝑎 ∈ suc 𝑛(𝑓‘𝑎)𝑅(𝑓‘suc 𝑎)))
Theorem	ssttrcl 9710	If 𝑅 is a relation, then it is a subclass of its transitive closure. (Contributed by Scott Fenton, 17-Oct-2024.)
⊢ (Rel 𝑅 → 𝑅 ⊆ t++𝑅)
Theorem	ttrcltr 9711	The transitive closure of a class is transitive. (Contributed by Scott Fenton, 17-Oct-2024.)
⊢ (t++𝑅 ∘ t++𝑅) ⊆ t++𝑅
Theorem	ttrclresv 9712	The transitive closure of 𝑅 restricted to V is the same as the transitive closure of 𝑅 itself. (Contributed by Scott Fenton, 20-Oct-2024.)
⊢ t++(𝑅 ↾ V) = t++𝑅
Theorem	ttrclco 9713	Composition law for the transitive closure of a relation. (Contributed by Scott Fenton, 20-Oct-2024.)
⊢ (t++𝑅 ∘ 𝑅) ⊆ t++𝑅
Theorem	cottrcl 9714	Composition law for the transitive closure of a relation. (Contributed by Scott Fenton, 20-Oct-2024.)
⊢ (𝑅 ∘ t++𝑅) ⊆ t++𝑅
Theorem	ttrclss 9715	If 𝑅 is a subclass of 𝑆 and 𝑆 is transitive, then the transitive closure of 𝑅 is a subclass of 𝑆. (Contributed by Scott Fenton, 20-Oct-2024.)
⊢ ((𝑅 ⊆ 𝑆 ∧ (𝑆 ∘ 𝑆) ⊆ 𝑆) → t++𝑅 ⊆ 𝑆)
Theorem	dmttrcl 9716	The domain of a transitive closure is the same as the domain of the original class. (Contributed by Scott Fenton, 26-Oct-2024.)
⊢ dom t++𝑅 = dom 𝑅
Theorem	rnttrcl 9717	The range of a transitive closure is the same as the range of the original class. (Contributed by Scott Fenton, 26-Oct-2024.)
⊢ ran t++𝑅 = ran 𝑅
Theorem	ttrclexg 9718	If 𝑅 is a set, then so is t++𝑅. (Contributed by Scott Fenton, 26-Oct-2024.)
⊢ (𝑅 ∈ 𝑉 → t++𝑅 ∈ V)
Theorem	dfttrcl2 9719*	When 𝑅 is a set and a relation, then its transitive closure can be defined by an intersection. (Contributed by Scott Fenton, 26-Oct-2024.)
⊢ ((𝑅 ∈ 𝑉 ∧ Rel 𝑅) → t++𝑅 = ∩ {𝑧 ∣ (𝑅 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})
Theorem	ttrclselem1 9720*	Lemma for ttrclse 9722. Show that all finite ordinal function values of 𝐹 are subsets of 𝐴. (Contributed by Scott Fenton, 31-Oct-2024.)
⊢ 𝐹 = rec((𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))    ⇒   ⊢ (𝑁 ∈ ω → (𝐹‘𝑁) ⊆ 𝐴)
Theorem	ttrclselem2 9721*	Lemma for ttrclse 9722. Show that a suc 𝑁 element long chain gives membership in the 𝑁-th predecessor class and vice-versa. (Contributed by Scott Fenton, 31-Oct-2024.)
⊢ 𝐹 = rec((𝑏 ∈ V ↦ ∪ 𝑤 ∈ 𝑏 Pred(𝑅, 𝐴, 𝑤)), Pred(𝑅, 𝐴, 𝑋))    ⇒   ⊢ ((𝑁 ∈ ω ∧ 𝑅 Se 𝐴 ∧ 𝑋 ∈ 𝐴) → (∃𝑓(𝑓 Fn suc suc 𝑁 ∧ ((𝑓‘∅) = 𝑦 ∧ (𝑓‘suc 𝑁) = 𝑋) ∧ ∀𝑎 ∈ suc 𝑁(𝑓‘𝑎)(𝑅 ↾ 𝐴)(𝑓‘suc 𝑎)) ↔ 𝑦 ∈ (𝐹‘𝑁)))
Theorem	ttrclse 9722	If 𝑅 is set-like over 𝐴, then the transitive closure of the restriction of 𝑅 to 𝐴 is set-like over 𝐴. This theorem requires the axioms of infinity and replacement for its proof. (Contributed by Scott Fenton, 31-Oct-2024.)
⊢ (𝑅 Se 𝐴 → t++(𝑅 ↾ 𝐴) Se 𝐴)
2.6.5  Transitive closure
Theorem	trcl 9723*	For any set 𝐴, show the properties of its transitive closure 𝐶. Similar to Theorem 9.1 of [TakeutiZaring] p. 73 except that we show an explicit expression for the transitive closure rather than just its existence. See tz9.1 9724 for an abbreviated version showing existence. (Contributed by NM, 14-Sep-2003.) (Revised by Mario Carneiro, 11-Sep-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐹 = (rec((𝑧 ∈ V ↦ (𝑧 ∪ ∪ 𝑧)), 𝐴) ↾ ω)    &   ⊢ 𝐶 = ∪ 𝑦 ∈ ω (𝐹‘𝑦)    ⇒   ⊢ (𝐴 ⊆ 𝐶 ∧ Tr 𝐶 ∧ ∀𝑥((𝐴 ⊆ 𝑥 ∧ Tr 𝑥) → 𝐶 ⊆ 𝑥))
Theorem	tz9.1 9724*	Every set has a transitive closure (the smallest transitive extension). Theorem 9.1 of [TakeutiZaring] p. 73. See trcl 9723 for an explicit expression for the transitive closure. Apparently open problems are whether this theorem can be proved without the Axiom of Infinity; if not, then whether it implies Infinity; and if not, what is the "property" that Infinity has that the other axioms don't have that is weaker than Infinity itself? (Added 22-Mar-2011) The following article seems to answer the first question, that it can't be proved without Infinity, in the affirmative: Mancini, Antonella and Zambella, Domenico (2001). "A note on recursive models of set theories." Notre Dame Journal of Formal Logic, 42(2):109-115. (Thanks to Scott Fenton.) (Contributed by NM, 15-Sep-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))
Theorem	tz9.1c 9725*	Alternate expression for the existence of transitive closures tz9.1 9724: the intersection of all transitive sets containing 𝐴 is a set. (Contributed by Mario Carneiro, 22-Mar-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V
Theorem	epfrs 9726*	The strong form of the Axiom of Regularity (no sethood requirement on 𝐴), with the axiom itself present as an antecedent. See also zfregs 9727. (Contributed by Mario Carneiro, 22-Mar-2013.)
⊢ (( E Fr 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅)
Theorem	zfregs 9727*	The strong form of the Axiom of Regularity, which does not require that 𝐴 be a set. Axiom 6' of [TakeutiZaring] p. 21. See also epfrs 9726. (Contributed by NM, 17-Sep-2003.)
⊢ (𝐴 ≠ ∅ → ∃𝑥 ∈ 𝐴 (𝑥 ∩ 𝐴) = ∅)
Theorem	zfregs2 9728*	Alternate strong form of the Axiom of Regularity. Not every element of a nonempty class contains some element of that class. (Contributed by Alan Sare, 24-Oct-2011.) (Proof shortened by Wolf Lammen, 27-Sep-2013.)
⊢ (𝐴 ≠ ∅ → ¬ ∀𝑥 ∈ 𝐴 ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥))
Theorem	setind 9729*	Set (epsilon) induction. Theorem 5.22 of [TakeutiZaring] p. 21. (Contributed by NM, 17-Sep-2003.)
⊢ (∀𝑥(𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝐴) → 𝐴 = V)
Theorem	setind2 9730	Set (epsilon) induction, stated compactly. Given as a homework problem in 1992 by George Boolos (1940-1996). (Contributed by NM, 17-Sep-2003.)
⊢ (𝒫 𝐴 ⊆ 𝐴 → 𝐴 = V)
Syntax	ctc 9731	Extend class notation to include the transitive closure function.
class TC
Definition	df-tc 9732*	The transitive closure function. (Contributed by Mario Carneiro, 23-Jun-2013.)
⊢ TC = (𝑥 ∈ V ↦ ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ Tr 𝑦)})
Theorem	tcvalg 9733*	Value of the transitive closure function. (The fact that this intersection exists is a non-trivial fact that depends on ax-inf 9633; see tz9.1 9724.) (Contributed by Mario Carneiro, 23-Jun-2013.)
⊢ (𝐴 ∈ 𝑉 → (TC‘𝐴) = ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)})
Theorem	tcid 9734	Defining property of the transitive closure function: it contains its argument as a subset. (Contributed by Mario Carneiro, 23-Jun-2013.)
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (TC‘𝐴))
Theorem	tctr 9735	Defining property of the transitive closure function: it is transitive. (Contributed by Mario Carneiro, 23-Jun-2013.)
⊢ Tr (TC‘𝐴)
Theorem	tcmin 9736	Defining property of the transitive closure function: it is a subset of any transitive class containing 𝐴. (Contributed by Mario Carneiro, 23-Jun-2013.)
⊢ (𝐴 ∈ 𝑉 → ((𝐴 ⊆ 𝐵 ∧ Tr 𝐵) → (TC‘𝐴) ⊆ 𝐵))
Theorem	tc2 9737*	A variant of the definition of the transitive closure function, using instead the smallest transitive set containing 𝐴 as a member, gives almost the same set, except that 𝐴 itself must be added because it is not usually a member of (TC‘𝐴) (and it is never a member if 𝐴 is well-founded). (Contributed by Mario Carneiro, 23-Jun-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ((TC‘𝐴) ∪ {𝐴}) = ∩ {𝑥 ∣ (𝐴 ∈ 𝑥 ∧ Tr 𝑥)}
Theorem	tcsni 9738	The transitive closure of a singleton. Proof suggested by Gérard Lang. (Contributed by Mario Carneiro, 4-Jun-2015.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (TC‘{𝐴}) = ((TC‘𝐴) ∪ {𝐴})
Theorem	tcss 9739	The transitive closure function inherits the subset relation. (Contributed by Mario Carneiro, 23-Jun-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ⊆ 𝐴 → (TC‘𝐵) ⊆ (TC‘𝐴))
Theorem	tcel 9740	The transitive closure function converts the element relation to the subset relation. (Contributed by Mario Carneiro, 23-Jun-2013.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐵 ∈ 𝐴 → (TC‘𝐵) ⊆ (TC‘𝐴))
Theorem	tcidm 9741	The transitive closure function is idempotent. (Contributed by Mario Carneiro, 23-Jun-2013.)
⊢ (TC‘(TC‘𝐴)) = (TC‘𝐴)
Theorem	tc0 9742	The transitive closure of the empty set. (Contributed by Mario Carneiro, 4-Jun-2015.)
⊢ (TC‘∅) = ∅
Theorem	tc00 9743	The transitive closure is empty iff its argument is. Proof suggested by Gérard Lang. (Contributed by Mario Carneiro, 4-Jun-2015.)
⊢ (𝐴 ∈ 𝑉 → ((TC‘𝐴) = ∅ ↔ 𝐴 = ∅))
2.6.6  Well-Founded Induction
Theorem	frmin 9744*	Every (possibly proper) subclass of a class 𝐴 with a well-founded set-like relation 𝑅 has a minimal element. This is a very strong generalization of tz6.26 6349 and tz7.5 6386. (Contributed by Scott Fenton, 4-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) (Revised by Scott Fenton, 27-Nov-2024.)
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)
Theorem	frind 9745*	A subclass of a well-founded class 𝐴 with the property that whenever it contains all predecessors of an element of 𝐴 it also contains that element, is equal to 𝐴. Compare wfi 6352 and tfi 7842, which are special cases of this theorem that do not require the axiom of infinity. (Contributed by Scott Fenton, 6-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐴 (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 → 𝑦 ∈ 𝐵))) → 𝐴 = 𝐵)
Theorem	frinsg 9746*	Well-Founded Induction Schema. If a property passes from all elements less than 𝑦 of a well-founded class 𝐴 to 𝑦 itself (induction hypothesis), then the property holds for all elements of 𝐴. Theorem 5.6(ii) of [Levy] p. 64. (Contributed by Scott Fenton, 7-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)[𝑧 / 𝑦]𝜑 → 𝜑))    ⇒   ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑)
Theorem	frins 9747*	Well-Founded Induction Schema. If a property passes from all elements less than 𝑦 of a well-founded class 𝐴 to 𝑦 itself (induction hypothesis), then the property holds for all elements of 𝐴. (Contributed by Scott Fenton, 6-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
⊢ 𝑅 Fr 𝐴    &   ⊢ 𝑅 Se 𝐴    &   ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)[𝑧 / 𝑦]𝜑 → 𝜑))    ⇒   ⊢ (𝑦 ∈ 𝐴 → 𝜑)
Theorem	frins2f 9748*	Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 7-Feb-2011.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑))    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑)
Theorem	frins2 9749*	Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 8-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑))    &   ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑)
Theorem	frins3 9750*	Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 6-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑))    ⇒   ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝐵 ∈ 𝐴) → 𝜒)
2.6.7  Well-Founded Recursion
Theorem	frr3g 9751*	Functions defined by well-founded recursion are identical up to relation, domain, and characteristic function. General version of frr3 9756. (Contributed by Scott Fenton, 10-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐹 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐹‘𝑦) = (𝑦𝐻(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐺‘𝑦) = (𝑦𝐻(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → 𝐹 = 𝐺)
Theorem	frrlem15 9752*	Lemma for general well-founded recursion. Two acceptable functions are compatible. (Contributed by Scott Fenton, 11-Sep-2023.)
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}    &   ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺)    ⇒   ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣))
Theorem	frrlem16 9753*	Lemma for general well-founded recursion. Establish a subset relation. (Contributed by Scott Fenton, 11-Sep-2023.) Revised notion of transitive closure. (Revised by Scott Fenton, 1-Dec-2024.)
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑧 ∈ 𝐴) → ∀𝑤 ∈ Pred (t++(𝑅 ↾ 𝐴), 𝐴, 𝑧)Pred(𝑅, 𝐴, 𝑤) ⊆ Pred(t++(𝑅 ↾ 𝐴), 𝐴, 𝑧))
Theorem	frr1 9754	Law of general well-founded recursion, part one. This theorem and the following two drop the partial order requirement from fpr1 8288, fpr2 8289, and fpr3 8290, which requires using the axiom of infinity (Contributed by Scott Fenton, 11-Sep-2023.)
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺)    ⇒   ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) → 𝐹 Fn 𝐴)
Theorem	frr2 9755	Law of general well-founded recursion, part two. Now we establish the value of 𝐹 within 𝐴. (Contributed by Scott Fenton, 11-Sep-2023.)
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺)    ⇒   ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = (𝑋𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑋))))
Theorem	frr3 9756*	Law of general well-founded recursion, part three. Finally, we show that 𝐹 is unique. We do this by showing that any function 𝐻 with the same properties we proved of 𝐹 in frr1 9754 and frr2 9755 is identical to 𝐹. (Contributed by Scott Fenton, 11-Sep-2023.)
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺)    ⇒   ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐻 Fn 𝐴 ∧ ∀𝑧 ∈ 𝐴 (𝐻‘𝑧) = (𝑧𝐺(𝐻 ↾ Pred(𝑅, 𝐴, 𝑧))))) → 𝐹 = 𝐻)
2.6.8  Rank
Syntax	cr1 9757	Extend class definition to include the cumulative hierarchy of sets function.
class 𝑅1
Syntax	crnk 9758	Extend class definition to include rank function.
class rank
Definition	df-r1 9759	Define the cumulative hierarchy of sets function, using Takeuti and Zaring's notation (𝑅1). Starting with the empty set, this function builds up layers of sets where the next layer is the power set of the previous layer (and the union of previous layers when the argument is a limit ordinal). Using the Axiom of Regularity, we can show that any set whatsoever belongs to one of the layers of this hierarchy (see tz9.13 9786). Our definition expresses Definition 9.9 of [TakeutiZaring] p. 76 in a closed form, from which we derive the recursive definition as Theorems r10 9763, r1suc 9765, and r1lim 9767. Theorem r1val1 9781 shows a recursive definition that works for all values, and Theorems r1val2 9832 and r1val3 9833 show the value expressed in terms of rank. Other notations for this function are R with the argument as a subscript (Equation 3.1 of [BellMachover] p. 477), V with a subscript (Definition of [Enderton] p. 202), M with a subscript (Definition 15.19 of [Monk1] p. 113), the capital Greek letter psi (Definition of [Mendelson] p. 281), and bold-face R (Definition 2.1 of [Kunen] p. 95). (Contributed by NM, 2-Sep-2003.)
⊢ 𝑅1 = rec((𝑥 ∈ V ↦ 𝒫 𝑥), ∅)
Definition	df-rank 9760*	Define the rank function. See rankval 9811, rankval2 9813, rankval3 9835, or rankval4 9862 its value. The rank is a kind of "inverse" of the cumulative hierarchy of sets function 𝑅1: given a set, it returns an ordinal number telling us the smallest layer of the hierarchy to which the set belongs. Based on Definition 9.14 of [TakeutiZaring] p. 79. Theorem rankid 9828 illustrates the "inverse" concept. Another nice theorem showing the relationship is rankr1a 9831. (Contributed by NM, 11-Oct-2003.)
⊢ rank = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑥 ∈ (𝑅1‘suc 𝑦)})
Theorem	r1funlim 9761	The cumulative hierarchy of sets function is a function on a limit ordinal. (This weak form of r1fnon 9762 avoids ax-rep 5286.) (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (Fun 𝑅1 ∧ Lim dom 𝑅1)
Theorem	r1fnon 9762	The cumulative hierarchy of sets function is a function on the class of ordinal numbers. (Contributed by NM, 5-Oct-2003.) (Revised by Mario Carneiro, 10-Sep-2013.)
⊢ 𝑅1 Fn On
Theorem	r10 9763	Value of the cumulative hierarchy of sets function at ∅. Part of Definition 9.9 of [TakeutiZaring] p. 76. (Contributed by NM, 2-Sep-2003.) (Revised by Mario Carneiro, 10-Sep-2013.)
⊢ (𝑅1‘∅) = ∅
Theorem	r1sucg 9764	Value of the cumulative hierarchy of sets function at a successor ordinal. Part of Definition 9.9 of [TakeutiZaring] p. 76. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐴 ∈ dom 𝑅1 → (𝑅1‘suc 𝐴) = 𝒫 (𝑅1‘𝐴))
Theorem	r1suc 9765	Value of the cumulative hierarchy of sets function at a successor ordinal. Part of Definition 9.9 of [TakeutiZaring] p. 76. (Contributed by NM, 2-Sep-2003.) (Revised by Mario Carneiro, 10-Sep-2013.)
⊢ (𝐴 ∈ On → (𝑅1‘suc 𝐴) = 𝒫 (𝑅1‘𝐴))
Theorem	r1limg 9766*	Value of the cumulative hierarchy of sets function at a limit ordinal. Part of Definition 9.9 of [TakeutiZaring] p. 76. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ ((𝐴 ∈ dom 𝑅1 ∧ Lim 𝐴) → (𝑅1‘𝐴) = ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥))
Theorem	r1lim 9767*	Value of the cumulative hierarchy of sets function at a limit ordinal. Part of Definition 9.9 of [TakeutiZaring] p. 76. (Contributed by NM, 4-Oct-2003.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → (𝑅1‘𝐴) = ∪ 𝑥 ∈ 𝐴 (𝑅1‘𝑥))
Theorem	r1fin 9768	The first ω levels of the cumulative hierarchy are all finite. (Contributed by Mario Carneiro, 15-May-2013.)
⊢ (𝐴 ∈ ω → (𝑅1‘𝐴) ∈ Fin)
Theorem	r1sdom 9769	Each stage in the cumulative hierarchy is strictly larger than the last. (Contributed by Mario Carneiro, 19-Apr-2013.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → (𝑅1‘𝐵) ≺ (𝑅1‘𝐴))
Theorem	r111 9770	The cumulative hierarchy is a one-to-one function. (Contributed by Mario Carneiro, 19-Apr-2013.)
⊢ 𝑅1:On–1-1→V
Theorem	r1tr 9771	The cumulative hierarchy of sets is transitive. Lemma 7T of [Enderton] p. 202. (Contributed by NM, 8-Sep-2003.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ Tr (𝑅1‘𝐴)
Theorem	r1tr2 9772	The union of a cumulative hierarchy of sets at ordinal 𝐴 is a subset of the hierarchy at 𝐴. JFM CLASSES1 th. 40. (Contributed by FL, 20-Apr-2011.)
⊢ ∪ (𝑅1‘𝐴) ⊆ (𝑅1‘𝐴)
Theorem	r1ordg 9773	Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of [TakeutiZaring] p. 77. (Contributed by NM, 8-Sep-2003.)
⊢ (𝐵 ∈ dom 𝑅1 → (𝐴 ∈ 𝐵 → (𝑅1‘𝐴) ∈ (𝑅1‘𝐵)))
Theorem	r1ord3g 9774	Ordering relation for the cumulative hierarchy of sets. Part of Theorem 3.3(i) of [BellMachover] p. 478. (Contributed by NM, 22-Sep-2003.)
⊢ ((𝐴 ∈ dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1) → (𝐴 ⊆ 𝐵 → (𝑅1‘𝐴) ⊆ (𝑅1‘𝐵)))
Theorem	r1ord 9775	Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of [TakeutiZaring] p. 77. (Contributed by NM, 8-Sep-2003.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → (𝑅1‘𝐴) ∈ (𝑅1‘𝐵)))
Theorem	r1ord2 9776	Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of [TakeutiZaring] p. 77. (Contributed by NM, 22-Sep-2003.)
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → (𝑅1‘𝐴) ⊆ (𝑅1‘𝐵)))
Theorem	r1ord3 9777	Ordering relation for the cumulative hierarchy of sets. Part of Theorem 3.3(i) of [BellMachover] p. 478. (Contributed by NM, 22-Sep-2003.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 → (𝑅1‘𝐴) ⊆ (𝑅1‘𝐵)))
Theorem	r1sssuc 9778	The value of the cumulative hierarchy of sets function is a subset of its value at the successor. JFM CLASSES1 Th. 39. (Contributed by FL, 20-Apr-2011.)
⊢ (𝐴 ∈ On → (𝑅1‘𝐴) ⊆ (𝑅1‘suc 𝐴))
Theorem	r1pwss 9779	Each set of the cumulative hierarchy is closed under subsets. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐴 ∈ (𝑅1‘𝐵) → 𝒫 𝐴 ⊆ (𝑅1‘𝐵))
Theorem	r1sscl 9780	Each set of the cumulative hierarchy is closed under subsets. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ ((𝐴 ∈ (𝑅1‘𝐵) ∧ 𝐶 ⊆ 𝐴) → 𝐶 ∈ (𝑅1‘𝐵))
Theorem	r1val1 9781*	The value of the cumulative hierarchy of sets function expressed recursively. Theorem 7Q of [Enderton] p. 202. (Contributed by NM, 25-Nov-2003.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ dom 𝑅1 → (𝑅1‘𝐴) = ∪ 𝑥 ∈ 𝐴 𝒫 (𝑅1‘𝑥))
Theorem	tz9.12lem1 9782*	Lemma for tz9.12 9785. (Contributed by NM, 22-Sep-2003.) (Revised by Mario Carneiro, 11-Sep-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐹 = (𝑧 ∈ V ↦ ∩ {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1‘𝑣)})    ⇒   ⊢ (𝐹 “ 𝐴) ⊆ On
Theorem	tz9.12lem2 9783*	Lemma for tz9.12 9785. (Contributed by NM, 22-Sep-2003.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐹 = (𝑧 ∈ V ↦ ∩ {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1‘𝑣)})    ⇒   ⊢ suc ∪ (𝐹 “ 𝐴) ∈ On
Theorem	tz9.12lem3 9784*	Lemma for tz9.12 9785. (Contributed by NM, 22-Sep-2003.) (Revised by Mario Carneiro, 11-Sep-2015.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐹 = (𝑧 ∈ V ↦ ∩ {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1‘𝑣)})    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ On 𝑥 ∈ (𝑅1‘𝑦) → 𝐴 ∈ (𝑅1‘suc suc ∪ (𝐹 “ 𝐴)))
Theorem	tz9.12 9785*	A set is well-founded if all of its elements are well-founded. Proposition 9.12 of [TakeutiZaring] p. 78. The main proof consists of tz9.12lem1 9782 through tz9.12lem3 9784. (Contributed by NM, 22-Sep-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ On 𝑥 ∈ (𝑅1‘𝑦) → ∃𝑦 ∈ On 𝐴 ∈ (𝑅1‘𝑦))
Theorem	tz9.13 9786*	Every set is well-founded, assuming the Axiom of Regularity. In other words, every set belongs to a layer of the cumulative hierarchy of sets. Proposition 9.13 of [TakeutiZaring] p. 78. (Contributed by NM, 23-Sep-2003.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘𝑥)
Theorem	tz9.13g 9787*	Every set is well-founded, assuming the Axiom of Regularity. Proposition 9.13 of [TakeutiZaring] p. 78. This variant of tz9.13 9786 expresses the class existence requirement as an antecedent. (Contributed by NM, 4-Oct-2003.)
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘𝑥))
Theorem	rankwflemb 9788*	Two ways of saying a set is well-founded. (Contributed by NM, 11-Oct-2003.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) ↔ ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑥))
Theorem	rankf 9789	The domain and codomain of the rank function. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 12-Sep-2013.)
⊢ rank:∪ (𝑅1 “ On)⟶On
Theorem	rankon 9790	The rank of a set is an ordinal number. Proposition 9.15(1) of [TakeutiZaring] p. 79. (Contributed by NM, 5-Oct-2003.) (Revised by Mario Carneiro, 12-Sep-2013.)
⊢ (rank‘𝐴) ∈ On
Theorem	r1elwf 9791	Any member of the cumulative hierarchy is well-founded. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐴 ∈ (𝑅1‘𝐵) → 𝐴 ∈ ∪ (𝑅1 “ On))
Theorem	rankvalb 9792*	Value of the rank function. Definition 9.14 of [TakeutiZaring] p. 79 (proved as a theorem from our definition). This variant of rankval 9811 does not use Regularity, and so requires the assumption that 𝐴 is in the range of 𝑅1. (Contributed by NM, 11-Oct-2003.) (Revised by Mario Carneiro, 10-Sep-2013.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘𝐴) = ∩ {𝑥 ∈ On ∣ 𝐴 ∈ (𝑅1‘suc 𝑥)})
Theorem	rankr1ai 9793	One direction of rankr1a 9831. (Contributed by Mario Carneiro, 28-May-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ (𝑅1‘𝐵) → (rank‘𝐴) ∈ 𝐵)
Theorem	rankvaln 9794	Value of the rank function at a non-well-founded set. (The antecedent is always false under Foundation, by unir1 9808, unless 𝐴 is a proper class.) (Contributed by Mario Carneiro, 22-Mar-2013.) (Revised by Mario Carneiro, 10-Sep-2013.)
⊢ (¬ 𝐴 ∈ ∪ (𝑅1 “ On) → (rank‘𝐴) = ∅)
Theorem	rankidb 9795	Identity law for the rank function. (Contributed by NM, 3-Oct-2003.) (Revised by Mario Carneiro, 22-Mar-2013.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ∈ (𝑅1‘suc (rank‘𝐴)))
Theorem	rankdmr1 9796	A rank is a member of the cumulative hierarchy. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ (rank‘𝐴) ∈ dom 𝑅1
Theorem	rankr1ag 9797	A version of rankr1a 9831 that is suitable without assuming Regularity or Replacement. (Contributed by Mario Carneiro, 3-Jun-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1) → (𝐴 ∈ (𝑅1‘𝐵) ↔ (rank‘𝐴) ∈ 𝐵))
Theorem	rankr1bg 9798	A relationship between rank and 𝑅1. See rankr1ag 9797 for the membership version. (Contributed by Mario Carneiro, 17-Nov-2014.)
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ dom 𝑅1) → (𝐴 ⊆ (𝑅1‘𝐵) ↔ (rank‘𝐴) ⊆ 𝐵))
Theorem	r1rankidb 9799	Any set is a subset of the hierarchy of its rank. (Contributed by Mario Carneiro, 3-Jun-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ⊆ (𝑅1‘(rank‘𝐴)))
Theorem	r1elssi 9800	The range of the 𝑅1 function is transitive. Lemma 2.10 of [Kunen] p. 97. One direction of r1elss 9801 that doesn't need 𝐴 to be a set. (Contributed by Mario Carneiro, 22-Mar-2013.) (Revised by Mario Carneiro, 16-Nov-2014.)
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ⊆ ∪ (𝑅1 “ On))