P. 59 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 5801-5900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tposeqd 5801	Equality theorem for transposition. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ (φ → 𝐹 = 𝐺)    ⇒   ⊢ (φ → tpos 𝐹 = tpos 𝐺)
Theorem	tposssxp 5802	The transposition is a subset of a cross product. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ tpos 𝐹 ⊆ ((◡dom 𝐹 ∪ {∅}) × ran 𝐹)
Theorem	reltpos 5803	The transposition is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ Rel tpos 𝐹
Theorem	brtpos2 5804	Value of the transposition at a pair ⟨A, B⟩. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (B ∈ 𝑉 → (Atpos 𝐹B ↔ (A ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{A}𝐹B)))
Theorem	brtpos0 5805	The behavior of tpos when the left argument is the empty set (which is not an ordered pair but is the "default" value of an ordered pair when the arguments are proper classes). (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (A ∈ 𝑉 → (∅tpos 𝐹A ↔ ∅𝐹A))
Theorem	reldmtpos 5806	Necessary and sufficient condition for dom tpos 𝐹 to be a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (Rel dom tpos 𝐹 ↔ ¬ ∅ ∈ dom 𝐹)
Theorem	brtposg 5807	The transposition swaps arguments of a three-parameter relation. (Contributed by Jim Kingdon, 31-Jan-2019.)
⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨A, B⟩tpos 𝐹𝐶 ↔ ⟨B, A⟩𝐹𝐶))
Theorem	ottposg 5808	The transposition swaps the first two elements in a collection of ordered triples. (Contributed by Mario Carneiro, 1-Dec-2014.)
⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨A, B, 𝐶⟩ ∈ tpos 𝐹 ↔ ⟨B, A, 𝐶⟩ ∈ 𝐹))
Theorem	dmtpos 5809	The domain of tpos 𝐹 when dom 𝐹 is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (Rel dom 𝐹 → dom tpos 𝐹 = ◡dom 𝐹)
Theorem	rntpos 5810	The range of tpos 𝐹 when dom 𝐹 is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (Rel dom 𝐹 → ran tpos 𝐹 = ran 𝐹)
Theorem	tposexg 5811	The transposition of a set is a set. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (𝐹 ∈ 𝑉 → tpos 𝐹 ∈ V)
Theorem	ovtposg 5812	The transposition swaps the arguments in a two-argument function. When 𝐹 is a matrix, which is to say a function from ( 1 ... m ) × ( 1 ... n ) to the reals or some ring, tpos 𝐹 is the transposition of 𝐹, which is where the name comes from. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ ((A ∈ 𝑉 ∧ B ∈ 𝑊) → (Atpos 𝐹B) = (B𝐹A))
Theorem	tposfun 5813	The transposition of a function is a function. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (Fun 𝐹 → Fun tpos 𝐹)
Theorem	dftpos2 5814*	Alternate definition of tpos when 𝐹 has relational domain. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (Rel dom 𝐹 → tpos 𝐹 = (𝐹 ∘ (x ∈ ◡dom 𝐹 ↦ ∪ ◡{x})))
Theorem	dftpos3 5815*	Alternate definition of tpos when 𝐹 has relational domain. Compare df-cnv 4295. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (Rel dom 𝐹 → tpos 𝐹 = {⟨⟨x, y⟩, z⟩ ∣ ⟨y, x⟩𝐹z})
Theorem	dftpos4 5816*	Alternate definition of tpos. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ tpos 𝐹 = (𝐹 ∘ (x ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{x}))
Theorem	tpostpos 5817	Value of the double transposition for a general class 𝐹. (Contributed by Mario Carneiro, 16-Sep-2015.)
⊢ tpos tpos 𝐹 = (𝐹 ∩ (((V × V) ∪ {∅}) × V))
Theorem	tpostpos2 5818	Value of the double transposition for a relation on triples. (Contributed by Mario Carneiro, 16-Sep-2015.)
⊢ ((Rel 𝐹 ∧ Rel dom 𝐹) → tpos tpos 𝐹 = 𝐹)
Theorem	tposfn2 5819	The domain of a transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (Rel A → (𝐹 Fn A → tpos 𝐹 Fn ◡A))
Theorem	tposfo2 5820	Condition for a surjective transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (Rel A → (𝐹:A–onto→B → tpos 𝐹:◡A–onto→B))
Theorem	tposf2 5821	The domain and range of a transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (Rel A → (𝐹:A⟶B → tpos 𝐹:◡A⟶B))
Theorem	tposf12 5822	Condition for an injective transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (Rel A → (𝐹:A–1-1→B → tpos 𝐹:◡A–1-1→B))
Theorem	tposf1o2 5823	Condition of a bijective transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (Rel A → (𝐹:A–1-1-onto→B → tpos 𝐹:◡A–1-1-onto→B))
Theorem	tposfo 5824	The domain and range of a transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (𝐹:(A × B)–onto→𝐶 → tpos 𝐹:(B × A)–onto→𝐶)
Theorem	tposf 5825	The domain and range of a transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (𝐹:(A × B)⟶𝐶 → tpos 𝐹:(B × A)⟶𝐶)
Theorem	tposfn 5826	Functionality of a transposition. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝐹 Fn (A × B) → tpos 𝐹 Fn (B × A))
Theorem	tpos0 5827	Transposition of the empty set. (Contributed by NM, 10-Sep-2015.)
⊢ tpos ∅ = ∅
Theorem	tposco 5828	Transposition of a composition. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ tpos (𝐹 ∘ 𝐺) = (𝐹 ∘ tpos 𝐺)
Theorem	tpossym 5829*	Two ways to say a function is symmetric. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝐹 Fn (A × A) → (tpos 𝐹 = 𝐹 ↔ ∀x ∈ A ∀y ∈ A (x𝐹y) = (y𝐹x)))
Theorem	tposeqi 5830	Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ 𝐹 = 𝐺    ⇒   ⊢ tpos 𝐹 = tpos 𝐺
Theorem	tposex 5831	A transposition is a set. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ 𝐹 ∈ V    ⇒   ⊢ tpos 𝐹 ∈ V
Theorem	nftpos 5832	Hypothesis builder for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ Ⅎx𝐹    ⇒   ⊢ Ⅎxtpos 𝐹
Theorem	tposoprab 5833*	Transposition of a class of ordered triples. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ 𝐹 = {⟨⟨x, y⟩, z⟩ ∣ φ}    ⇒   ⊢ tpos 𝐹 = {⟨⟨y, x⟩, z⟩ ∣ φ}
Theorem	tposmpt2 5834*	Transposition of a two-argument mapping. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ 𝐹 = (x ∈ A, y ∈ B ↦ 𝐶)    ⇒   ⊢ tpos 𝐹 = (y ∈ B, x ∈ A ↦ 𝐶)
2.6.17  Undefined values
Theorem	pwuninel2 5835	The power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ (∪ A ∈ 𝑉 → ¬ 𝒫 ∪ A ∈ A)
Theorem	2pwuninelg 5836	The power set of the power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set. (Contributed by Jim Kingdon, 14-Jan-2020.)
⊢ (A ∈ 𝑉 → ¬ 𝒫 𝒫 ∪ A ∈ A)
2.6.18  Functions on ordinals; strictly monotone ordinal functions
Theorem	iunon 5837*	The indexed union of a set of ordinal numbers B(x) is an ordinal number. (Contributed by NM, 13-Oct-2003.) (Revised by Mario Carneiro, 5-Dec-2016.)
⊢ ((A ∈ 𝑉 ∧ ∀x ∈ A B ∈ On) → ∪ x ∈ A B ∈ On)
Syntax	wsmo 5838	Introduce the strictly monotone ordinal function. A strictly monotone function is one that is constantly increasing across the ordinals.
wff Smo A
Definition	df-smo 5839*	Definition of a strictly monotone ordinal function. Definition 7.46 in [TakeutiZaring] p. 50. (Contributed by Andrew Salmon, 15-Nov-2011.)
⊢ (Smo A ↔ (A:dom A⟶On ∧ Ord dom A ∧ ∀x ∈ dom A∀y ∈ dom A(x ∈ y → (A‘x) ∈ (A‘y))))
Theorem	dfsmo2 5840*	Alternate definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 4-Mar-2013.)
⊢ (Smo 𝐹 ↔ (𝐹:dom 𝐹⟶On ∧ Ord dom 𝐹 ∧ ∀x ∈ dom 𝐹∀y ∈ x (𝐹‘y) ∈ (𝐹‘x)))
Theorem	issmo 5841*	Conditions for which A is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 15-Nov-2011.)
⊢ A:B⟶On    &   ⊢ Ord B    &   ⊢ ((x ∈ B ∧ y ∈ B) → (x ∈ y → (A‘x) ∈ (A‘y)))    &   ⊢ dom A = B    ⇒   ⊢ Smo A
Theorem	issmo2 5842*	Alternative definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 12-Mar-2013.)
⊢ (𝐹:A⟶B → ((B ⊆ On ∧ Ord A ∧ ∀x ∈ A ∀y ∈ x (𝐹‘y) ∈ (𝐹‘x)) → Smo 𝐹))
Theorem	smoeq 5843	Equality theorem for strictly monotone functions. (Contributed by Andrew Salmon, 16-Nov-2011.)
⊢ (A = B → (Smo A ↔ Smo B))
Theorem	smodm 5844	The domain of a strictly monotone function is an ordinal. (Contributed by Andrew Salmon, 16-Nov-2011.)
⊢ (Smo A → Ord dom A)
Theorem	smores 5845	A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 16-Nov-2011.) (Proof shortened by Mario Carneiro, 5-Dec-2016.)
⊢ ((Smo A ∧ B ∈ dom A) → Smo (A ↾ B))
Theorem	smores3 5846	A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 19-Nov-2011.)
⊢ ((Smo (A ↾ B) ∧ 𝐶 ∈ (dom A ∩ B) ∧ Ord B) → Smo (A ↾ 𝐶))
Theorem	smores2 5847	A strictly monotone ordinal function restricted to an ordinal is still monotone. (Contributed by Mario Carneiro, 15-Mar-2013.)
⊢ ((Smo 𝐹 ∧ Ord A) → Smo (𝐹 ↾ A))
Theorem	smodm2 5848	The domain of a strictly monotone ordinal function is an ordinal. (Contributed by Mario Carneiro, 12-Mar-2013.)
⊢ ((𝐹 Fn A ∧ Smo 𝐹) → Ord A)
Theorem	smofvon2dm 5849	The function values of a strictly monotone ordinal function are ordinals. (Contributed by Mario Carneiro, 12-Mar-2013.)
⊢ ((Smo 𝐹 ∧ B ∈ dom 𝐹) → (𝐹‘B) ∈ On)
Theorem	iordsmo 5850	The identity relation restricted to the ordinals is a strictly monotone function. (Contributed by Andrew Salmon, 16-Nov-2011.)
⊢ Ord A    ⇒   ⊢ Smo ( I ↾ A)
Theorem	smo0 5851	The null set is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 20-Nov-2011.)
⊢ Smo ∅
Theorem	smofvon 5852	If B is a strictly monotone ordinal function, and A is in the domain of B, then the value of the function at A is an ordinal. (Contributed by Andrew Salmon, 20-Nov-2011.)
⊢ ((Smo B ∧ A ∈ dom B) → (B‘A) ∈ On)
Theorem	smoel 5853	If x is less than y then a strictly monotone function's value will be strictly less at x than at y. (Contributed by Andrew Salmon, 22-Nov-2011.)
⊢ ((Smo B ∧ A ∈ dom B ∧ 𝐶 ∈ A) → (B‘𝐶) ∈ (B‘A))
Theorem	smoiun 5854*	The value of a strictly monotone ordinal function contains its indexed union. (Contributed by Andrew Salmon, 22-Nov-2011.)
⊢ ((Smo B ∧ A ∈ dom B) → ∪ x ∈ A (B‘x) ⊆ (B‘A))
Theorem	smoiso 5855	If 𝐹 is an isomorphism from an ordinal A onto B, which is a subset of the ordinals, then 𝐹 is a strictly monotonic function. Exercise 3 in [TakeutiZaring] p. 50. (Contributed by Andrew Salmon, 24-Nov-2011.)
⊢ ((𝐹 Isom E , E (A, B) ∧ Ord A ∧ B ⊆ On) → Smo 𝐹)
Theorem	smoel2 5856	A strictly monotone ordinal function preserves the epsilon relation. (Contributed by Mario Carneiro, 12-Mar-2013.)
⊢ (((𝐹 Fn A ∧ Smo 𝐹) ∧ (B ∈ A ∧ 𝐶 ∈ B)) → (𝐹‘𝐶) ∈ (𝐹‘B))
2.6.19  "Strong" transfinite recursion
Syntax	crecs 5857	Notation for a function defined by strong transfinite recursion.
class recs(𝐹)
Definition	df-recs 5858*	Define a function recs(𝐹) on On, the class of ordinal numbers, by transfinite recursion given a rule 𝐹 which sets the next value given all values so far. See df-irdg 5894 for more details on why this definition is desirable. Unlike df-irdg 5894 which restricts the update rule to use only the previous value, this version allows the update rule to use all previous values, which is why it is described as "strong", although it is actually more primitive. See tfri1d 5887 and tfri2d 5888 for the primary contract of this definition. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ recs(𝐹) = ∪ {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}
Theorem	recseq 5859	Equality theorem for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ (𝐹 = 𝐺 → recs(𝐹) = recs(𝐺))
Theorem	nfrecs 5860	Bound-variable hypothesis builder for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ Ⅎx𝐹    ⇒   ⊢ Ⅎxrecs(𝐹)
Theorem	tfrlem1 5861*	A technical lemma for transfinite recursion. Compare Lemma 1 of [TakeutiZaring] p. 47. (Contributed by NM, 23-Mar-1995.) (Revised by Mario Carneiro, 24-May-2019.)
⊢ (φ → A ∈ On)    &   ⊢ (φ → (Fun 𝐹 ∧ A ⊆ dom 𝐹))    &   ⊢ (φ → (Fun 𝐺 ∧ A ⊆ dom 𝐺))    &   ⊢ (φ → ∀x ∈ A (𝐹‘x) = (B‘(𝐹 ↾ x)))    &   ⊢ (φ → ∀x ∈ A (𝐺‘x) = (B‘(𝐺 ↾ x)))    ⇒   ⊢ (φ → ∀x ∈ A (𝐹‘x) = (𝐺‘x))
Theorem	tfrlem3ag 5862*	Lemma for transfinite recursion. This lemma just changes some bound variables in A for later use. (Contributed by NM, 9-Apr-1995.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    ⇒   ⊢ (𝐺 ∈ V → (𝐺 ∈ A ↔ ∃z ∈ On (𝐺 Fn z ∧ ∀w ∈ z (𝐺‘w) = (𝐹‘(𝐺 ↾ w)))))
Theorem	tfrlem3a 5863*	Lemma for transfinite recursion. Let A be the class of "acceptable" functions. The final thing we're interested in is the union of all these acceptable functions. This lemma just changes some bound variables in A for later use. (Contributed by NM, 9-Apr-1995.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    &   ⊢ 𝐺 ∈ V    ⇒   ⊢ (𝐺 ∈ A ↔ ∃z ∈ On (𝐺 Fn z ∧ ∀w ∈ z (𝐺‘w) = (𝐹‘(𝐺 ↾ w))))
Theorem	tfrlem3 5864*	Lemma for transfinite recursion. Let A be the class of "acceptable" functions. The final thing we're interested in is the union of all these acceptable functions. This lemma just changes some bound variables in A for later use. (Contributed by NM, 9-Apr-1995.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    ⇒   ⊢ A = {g ∣ ∃z ∈ On (g Fn z ∧ ∀w ∈ z (g‘w) = (𝐹‘(g ↾ w)))}
Theorem	tfrlem3-2 5865*	Lemma for transfinite recursion which changes a bound variable (Contributed by Jim Kingdon, 17-Apr-2019.)
⊢ (Fun 𝐹 ∧ (𝐹‘x) ∈ V)    ⇒   ⊢ (Fun 𝐹 ∧ (𝐹‘g) ∈ V)
Theorem	tfrlem3-2d 5866*	Lemma for transfinite recursion which changes a bound variable (Contributed by Jim Kingdon, 2-Jul-2019.)
⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))    ⇒   ⊢ (φ → (Fun 𝐹 ∧ (𝐹‘g) ∈ V))
Theorem	tfrlem4 5867*	Lemma for transfinite recursion. A is the class of all "acceptable" functions, and 𝐹 is their union. First we show that an acceptable function is in fact a function. (Contributed by NM, 9-Apr-1995.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    ⇒   ⊢ (g ∈ A → Fun g)
Theorem	tfrlem5 5868*	Lemma for transfinite recursion. The values of two acceptable functions are the same within their domains. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 24-May-2019.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    ⇒   ⊢ ((g ∈ A ∧ ℎ ∈ A) → ((xgu ∧ xℎv) → u = v))
Theorem	recsfval 5869*	Lemma for transfinite recursion. The definition recs is the union of all acceptable functions. (Contributed by Mario Carneiro, 9-May-2015.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    ⇒   ⊢ recs(𝐹) = ∪ A
Theorem	tfrlem6 5870*	Lemma for transfinite recursion. The union of all acceptable functions is a relation. (Contributed by NM, 8-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    ⇒   ⊢ Rel recs(𝐹)
Theorem	tfrlem7 5871*	Lemma for transfinite recursion. The union of all acceptable functions is a function. (Contributed by NM, 9-Aug-1994.) (Revised by Mario Carneiro, 24-May-2019.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    ⇒   ⊢ Fun recs(𝐹)
Theorem	tfrlem8 5872*	Lemma for transfinite recursion. The domain of recs is ordinal. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Alan Sare, 11-Mar-2008.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    ⇒   ⊢ Ord dom recs(𝐹)
Theorem	tfrlem9 5873*	Lemma for transfinite recursion. Here we compute the value of recs (the union of all acceptable functions). (Contributed by NM, 17-Aug-1994.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    ⇒   ⊢ (B ∈ dom recs(𝐹) → (recs(𝐹)‘B) = (𝐹‘(recs(𝐹) ↾ B)))
Theorem	tfr2a 5874	A weak version of transfinite recursion. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    ⇒   ⊢ (A ∈ dom 𝐹 → (𝐹‘A) = (𝐺‘(𝐹 ↾ A)))
Theorem	tfr0 5875	Transfinite recursion at the empty set. (Contributed by Jim Kingdon, 8-May-2020.)
⊢ 𝐹 = recs(𝐺)    ⇒   ⊢ ((𝐺‘∅) ∈ 𝑉 → (𝐹‘∅) = (𝐺‘∅))
Theorem	tfrlemisucfn 5876*	We can extend an acceptable function by one element to produce a function. Lemma for tfrlemi1 5884. (Contributed by Jim Kingdon, 2-Jul-2019.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    &   ⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))    &   ⊢ (φ → z ∈ On)    &   ⊢ (φ → g Fn z)    &   ⊢ (φ → g ∈ A)    ⇒   ⊢ (φ → (g ∪ {⟨z, (𝐹‘g)⟩}) Fn suc z)
Theorem	tfrlemisucaccv 5877*	We can extend an acceptable function by one element to produce an acceptable function. Lemma for tfrlemi1 5884. (Contributed by Jim Kingdon, 4-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    &   ⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))    &   ⊢ (φ → z ∈ On)    &   ⊢ (φ → g Fn z)    &   ⊢ (φ → g ∈ A)    ⇒   ⊢ (φ → (g ∪ {⟨z, (𝐹‘g)⟩}) ∈ A)
Theorem	tfrlemibacc 5878*	Each element of B is an acceptable function. Lemma for tfrlemi1 5884. (Contributed by Jim Kingdon, 14-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    &   ⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))    &   ⊢ B = {ℎ ∣ ∃z ∈ x ∃g(g Fn z ∧ g ∈ A ∧ ℎ = (g ∪ {⟨z, (𝐹‘g)⟩}))}    &   ⊢ (φ → x ∈ On)    &   ⊢ (φ → ∀z ∈ x ∃g(g Fn z ∧ ∀w ∈ z (g‘w) = (𝐹‘(g ↾ w))))    ⇒   ⊢ (φ → B ⊆ A)
Theorem	tfrlemibxssdm 5879*	The union of B is defined on all ordinals. Lemma for tfrlemi1 5884. (Contributed by Jim Kingdon, 18-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    &   ⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))    &   ⊢ B = {ℎ ∣ ∃z ∈ x ∃g(g Fn z ∧ g ∈ A ∧ ℎ = (g ∪ {⟨z, (𝐹‘g)⟩}))}    &   ⊢ (φ → x ∈ On)    &   ⊢ (φ → ∀z ∈ x ∃g(g Fn z ∧ ∀w ∈ z (g‘w) = (𝐹‘(g ↾ w))))    ⇒   ⊢ (φ → x ⊆ dom ∪ B)
Theorem	tfrlemibfn 5880*	The union of B is a function defined on x. Lemma for tfrlemi1 5884. (Contributed by Jim Kingdon, 18-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    &   ⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))    &   ⊢ B = {ℎ ∣ ∃z ∈ x ∃g(g Fn z ∧ g ∈ A ∧ ℎ = (g ∪ {⟨z, (𝐹‘g)⟩}))}    &   ⊢ (φ → x ∈ On)    &   ⊢ (φ → ∀z ∈ x ∃g(g Fn z ∧ ∀w ∈ z (g‘w) = (𝐹‘(g ↾ w))))    ⇒   ⊢ (φ → ∪ B Fn x)
Theorem	tfrlemibex 5881*	The set B exists. Lemma for tfrlemi1 5884. (Contributed by Jim Kingdon, 17-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    &   ⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))    &   ⊢ B = {ℎ ∣ ∃z ∈ x ∃g(g Fn z ∧ g ∈ A ∧ ℎ = (g ∪ {⟨z, (𝐹‘g)⟩}))}    &   ⊢ (φ → x ∈ On)    &   ⊢ (φ → ∀z ∈ x ∃g(g Fn z ∧ ∀w ∈ z (g‘w) = (𝐹‘(g ↾ w))))    ⇒   ⊢ (φ → B ∈ V)
Theorem	tfrlemiubacc 5882*	The union of B satisfies the recursion rule (lemma for tfrlemi1 5884). (Contributed by Jim Kingdon, 22-Apr-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    &   ⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))    &   ⊢ B = {ℎ ∣ ∃z ∈ x ∃g(g Fn z ∧ g ∈ A ∧ ℎ = (g ∪ {⟨z, (𝐹‘g)⟩}))}    &   ⊢ (φ → x ∈ On)    &   ⊢ (φ → ∀z ∈ x ∃g(g Fn z ∧ ∀w ∈ z (g‘w) = (𝐹‘(g ↾ w))))    ⇒   ⊢ (φ → ∀u ∈ x (∪ B‘u) = (𝐹‘(∪ B ↾ u)))
Theorem	tfrlemiex 5883*	Lemma for tfrlemi1 5884. (Contributed by Jim Kingdon, 18-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    &   ⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))    &   ⊢ B = {ℎ ∣ ∃z ∈ x ∃g(g Fn z ∧ g ∈ A ∧ ℎ = (g ∪ {⟨z, (𝐹‘g)⟩}))}    &   ⊢ (φ → x ∈ On)    &   ⊢ (φ → ∀z ∈ x ∃g(g Fn z ∧ ∀w ∈ z (g‘w) = (𝐹‘(g ↾ w))))    ⇒   ⊢ (φ → ∃f(f Fn x ∧ ∀u ∈ x (f‘u) = (𝐹‘(f ↾ u))))
Theorem	tfrlemi1 5884*	We can define an acceptable function on any ordinal. As with many of the transfinite recursion theorems, we have a hypothesis that states that 𝐹 is a function and that it is defined for all ordinals. (Contributed by Jim Kingdon, 4-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    &   ⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))    ⇒   ⊢ ((φ ∧ 𝐶 ∈ On) → ∃g(g Fn 𝐶 ∧ ∀u ∈ 𝐶 (g‘u) = (𝐹‘(g ↾ u))))
Theorem	tfrlemi14d 5885*	The domain of recs is all ordinals (lemma for transfinite recursion). (Contributed by Jim Kingdon, 9-Jul-2019.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    &   ⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))    ⇒   ⊢ (φ → dom recs(𝐹) = On)
Theorem	tfrexlem 5886*	The transfinite recursion function is set-like if the input is. (Contributed by Mario Carneiro, 3-Jul-2019.)
⊢ A = {f ∣ ∃x ∈ On (f Fn x ∧ ∀y ∈ x (f‘y) = (𝐹‘(f ↾ y)))}    &   ⊢ (φ → ∀x(Fun 𝐹 ∧ (𝐹‘x) ∈ V))    ⇒   ⊢ ((φ ∧ 𝐶 ∈ 𝑉) → (recs(𝐹)‘𝐶) ∈ V)
Theorem	tfri1d 5887*	Principle of Transfinite Recursion, part 1 of 3. Theorem 7.41(1) of [TakeutiZaring] p. 47, with an additional condition. The condition is that 𝐺 is defined "everywhere" and here is stated as (𝐺‘x) ∈ V. Alternatively ∀x ∈ On∀f(f Fn x → f ∈ dom 𝐺) would suffice. Given a function 𝐺 satisfying that condition, we define a class A of all "acceptable" functions. The final function we're interested in is the union 𝐹 = recs(𝐺) of them. 𝐹 is then said to be defined by transfinite recursion. The purpose of the 3 parts of this theorem is to demonstrate properties of 𝐹. In this first part we show that 𝐹 is a function whose domain is all ordinal numbers. (Contributed by Jim Kingdon, 4-May-2019.) (Revised by Mario Carneiro, 24-May-2019.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (φ → ∀x(Fun 𝐺 ∧ (𝐺‘x) ∈ V))    ⇒   ⊢ (φ → 𝐹 Fn On)
Theorem	tfri2d 5888*	Principle of Transfinite Recursion, part 2 of 3. Theorem 7.41(2) of [TakeutiZaring] p. 47, with an additional condition on the recursion rule 𝐺 ( as described at tfri1 5889). Here we show that the function 𝐹 has the property that for any function 𝐺 satisfying that condition, the "next" value of 𝐹 is 𝐺 recursively applied to all "previous" values of 𝐹. (Contributed by Jim Kingdon, 4-May-2019.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (φ → ∀x(Fun 𝐺 ∧ (𝐺‘x) ∈ V))    ⇒   ⊢ ((φ ∧ A ∈ On) → (𝐹‘A) = (𝐺‘(𝐹 ↾ A)))
Theorem	tfri1 5889*	Principle of Transfinite Recursion, part 1 of 3. Theorem 7.41(1) of [TakeutiZaring] p. 47, with an additional condition. The condition is that 𝐺 is defined "everywhere" and here is stated as (𝐺‘x) ∈ V. Alternatively ∀x ∈ On∀f(f Fn x → f ∈ dom 𝐺) would suffice. Given a function 𝐺 satisfying that condition, we define a class A of all "acceptable" functions. The final function we're interested in is the union 𝐹 = recs(𝐺) of them. 𝐹 is then said to be defined by transfinite recursion. The purpose of the 3 parts of this theorem is to demonstrate properties of 𝐹. In this first part we show that 𝐹 is a function whose domain is all ordinal numbers. (Contributed by Jim Kingdon, 4-May-2019.) (Revised by Mario Carneiro, 24-May-2019.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (Fun 𝐺 ∧ (𝐺‘x) ∈ V)    ⇒   ⊢ 𝐹 Fn On
Theorem	tfri2 5890*	Principle of Transfinite Recursion, part 2 of 3. Theorem 7.41(2) of [TakeutiZaring] p. 47, with an additional condition on the recursion rule 𝐺 ( as described at tfri1 5889). Here we show that the function 𝐹 has the property that for any function 𝐺 satisfying that condition, the "next" value of 𝐹 is 𝐺 recursively applied to all "previous" values of 𝐹. (Contributed by Jim Kingdon, 4-May-2019.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (Fun 𝐺 ∧ (𝐺‘x) ∈ V)    ⇒   ⊢ (A ∈ On → (𝐹‘A) = (𝐺‘(𝐹 ↾ A)))
Theorem	tfri3 5891*	Principle of Transfinite Recursion, part 3 of 3. Theorem 7.41(3) of [TakeutiZaring] p. 47, with an additional condition on the recursion rule 𝐺 ( as described at tfri1 5889). Finally, we show that 𝐹 is unique. We do this by showing that any class B with the same properties of 𝐹 that we showed in parts 1 and 2 is identical to 𝐹. (Contributed by Jim Kingdon, 4-May-2019.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (Fun 𝐺 ∧ (𝐺‘x) ∈ V)    ⇒   ⊢ ((B Fn On ∧ ∀x ∈ On (B‘x) = (𝐺‘(B ↾ x))) → B = 𝐹)
Theorem	tfrex 5892*	The transfinite recursion function is set-like if the input is. (Contributed by Mario Carneiro, 3-Jul-2019.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ (φ → ∀x(Fun 𝐺 ∧ (𝐺‘x) ∈ V))    ⇒   ⊢ ((φ ∧ A ∈ 𝑉) → (𝐹‘A) ∈ V)
2.6.20  Recursive definition generator
Syntax	crdg 5893	Extend class notation with the recursive definition generator, with characteristic function 𝐹 and initial value 𝐼.
class rec(𝐹, 𝐼)
Definition	df-irdg 5894*	Define a recursive definition generator on On (the class of ordinal numbers) with characteristic function 𝐹 and initial value 𝐼. This rather amazing operation allows us to define, with compact direct definitions, functions that are usually defined in textbooks only with indirect self-referencing recursive definitions. A recursive definition requires advanced metalogic to justify - in particular, eliminating a recursive definition is very difficult and often not even shown in textbooks. On the other hand, the elimination of a direct definition is a matter of simple mechanical substitution. The price paid is the daunting complexity of our rec operation (especially when df-recs 5858 that it is built on is also eliminated). But once we get past this hurdle, definitions that would otherwise be recursive become relatively simple. In classical logic it would be easier to divide this definition into cases based on whether the domain of g is zero, a successor, or a limit ordinal. Cases do not (in general) work that way in intuitionistic logic, so instead we choose a definition which takes the union of all the results of the characteristic function for ordinals in the domain of g. This means that this definition has the expected properties for increasing and continuous ordinal functions, which include ordinal addition and multiplication. For finite recursion we also define df-frec 5915 and for suitable characteristic functions df-frec 5915 yields the same result as rec restricted to 𝜔, as seen at frecrdg 5925. Note: We introduce rec with the philosophical goal of being able to eliminate all definitions with direct mechanical substitution and to verify easily the soundness of definitions. Metamath itself has no built-in technical limitation that prevents multiple-part recursive definitions in the traditional textbook style. (Contributed by Jim Kingdon, 19-May-2019.)
⊢ rec(𝐹, 𝐼) = recs((g ∈ V ↦ (𝐼 ∪ ∪ x ∈ dom g(𝐹‘(g‘x)))))
Theorem	rdgeq1 5895	Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.)
⊢ (𝐹 = 𝐺 → rec(𝐹, A) = rec(𝐺, A))
Theorem	rdgeq2 5896	Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.)
⊢ (A = B → rec(𝐹, A) = rec(𝐹, B))
Theorem	rdgfun 5897	The recursive definition generator is a function. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ Fun rec(𝐹, A)
Theorem	rdgtfr 5898*	The recursion rule for the recursive definition generator is defined everywhere. (Contributed by Jim Kingdon, 14-May-2020.)
⊢ ((∀z(𝐹‘z) ∈ V ∧ A ∈ 𝑉) → (Fun (g ∈ V ↦ (A ∪ ∪ x ∈ dom g(𝐹‘(g‘x)))) ∧ ((g ∈ V ↦ (A ∪ ∪ x ∈ dom g(𝐹‘(g‘x))))‘f) ∈ V))
Theorem	rdgruledefgg 5899*	The recursion rule for the recursive definition generator is defined everywhere. (Contributed by Jim Kingdon, 4-Jul-2019.)
⊢ ((𝐹 Fn V ∧ A ∈ 𝑉) → (Fun (g ∈ V ↦ (A ∪ ∪ x ∈ dom g(𝐹‘(g‘x)))) ∧ ((g ∈ V ↦ (A ∪ ∪ x ∈ dom g(𝐹‘(g‘x))))‘f) ∈ V))
Theorem	rdgruledefg 5900*	The recursion rule for the recursive definition generator is defined everywhere. (Contributed by Jim Kingdon, 4-Jul-2019.)
⊢ 𝐹 Fn V    ⇒   ⊢ (A ∈ 𝑉 → (Fun (g ∈ V ↦ (A ∪ ∪ x ∈ dom g(𝐹‘(g‘x)))) ∧ ((g ∈ V ↦ (A ∪ ∪ x ∈ dom g(𝐹‘(g‘x))))‘f) ∈ V))