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
Definition	df-tpos 5801*	Define the transposition of a function, which is a function 𝐺 = tpos 𝐹 satisfying 𝐺(x, y) = 𝐹(y, x). (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ tpos 𝐹 = (𝐹 ∘ (x ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{x}))
Theorem	tposss 5802	Subset theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (𝐹 ⊆ 𝐺 → tpos 𝐹 ⊆ tpos 𝐺)
Theorem	tposeq 5803	Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (𝐹 = 𝐺 → tpos 𝐹 = tpos 𝐺)
Theorem	tposeqd 5804	Equality theorem for transposition. (Contributed by Mario Carneiro, 7-Jan-2017.)
⊢ (φ → 𝐹 = 𝐺)    ⇒   ⊢ (φ → tpos 𝐹 = tpos 𝐺)
Theorem	tposssxp 5805	The transposition is a subset of a cross product. (Contributed by Mario Carneiro, 12-Jan-2017.)
⊢ tpos 𝐹 ⊆ ((◡dom 𝐹 ∪ {∅}) × ran 𝐹)
Theorem	reltpos 5806	The transposition is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ Rel tpos 𝐹
Theorem	brtpos2 5807	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 5808	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 5809	Necessary and sufficient condition for dom tpos 𝐹 to be a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (Rel dom tpos 𝐹 ↔ ¬ ∅ ∈ dom 𝐹)
Theorem	brtposg 5810	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 5811	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 5812	The domain of tpos 𝐹 when dom 𝐹 is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (Rel dom 𝐹 → dom tpos 𝐹 = ◡dom 𝐹)
Theorem	rntpos 5813	The range of tpos 𝐹 when dom 𝐹 is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (Rel dom 𝐹 → ran tpos 𝐹 = ran 𝐹)
Theorem	tposexg 5814	The transposition of a set is a set. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (𝐹 ∈ 𝑉 → tpos 𝐹 ∈ V)
Theorem	ovtposg 5815	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 5816	The transposition of a function is a function. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (Fun 𝐹 → Fun tpos 𝐹)
Theorem	dftpos2 5817*	Alternate definition of tpos when 𝐹 has relational domain. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (Rel dom 𝐹 → tpos 𝐹 = (𝐹 ∘ (x ∈ ◡dom 𝐹 ↦ ∪ ◡{x})))
Theorem	dftpos3 5818*	Alternate definition of tpos when 𝐹 has relational domain. Compare df-cnv 4296. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ (Rel dom 𝐹 → tpos 𝐹 = {⟨⟨x, y⟩, z⟩ ∣ ⟨y, x⟩𝐹z})
Theorem	dftpos4 5819*	Alternate definition of tpos. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ tpos 𝐹 = (𝐹 ∘ (x ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{x}))
Theorem	tpostpos 5820	Value of the double transposition for a general class 𝐹. (Contributed by Mario Carneiro, 16-Sep-2015.)
⊢ tpos tpos 𝐹 = (𝐹 ∩ (((V × V) ∪ {∅}) × V))
Theorem	tpostpos2 5821	Value of the double transposition for a relation on triples. (Contributed by Mario Carneiro, 16-Sep-2015.)
⊢ ((Rel 𝐹 ∧ Rel dom 𝐹) → tpos tpos 𝐹 = 𝐹)
Theorem	tposfn2 5822	The domain of a transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (Rel A → (𝐹 Fn A → tpos 𝐹 Fn ◡A))
Theorem	tposfo2 5823	Condition for a surjective transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (Rel A → (𝐹:A–onto→B → tpos 𝐹:◡A–onto→B))
Theorem	tposf2 5824	The domain and range of a transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (Rel A → (𝐹:A⟶B → tpos 𝐹:◡A⟶B))
Theorem	tposf12 5825	Condition for an injective transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (Rel A → (𝐹:A–1-1→B → tpos 𝐹:◡A–1-1→B))
Theorem	tposf1o2 5826	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 5827	The domain and range of a transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (𝐹:(A × B)–onto→𝐶 → tpos 𝐹:(B × A)–onto→𝐶)
Theorem	tposf 5828	The domain and range of a transposition. (Contributed by NM, 10-Sep-2015.)
⊢ (𝐹:(A × B)⟶𝐶 → tpos 𝐹:(B × A)⟶𝐶)
Theorem	tposfn 5829	Functionality of a transposition. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝐹 Fn (A × B) → tpos 𝐹 Fn (B × A))
Theorem	tpos0 5830	Transposition of the empty set. (Contributed by NM, 10-Sep-2015.)
⊢ tpos ∅ = ∅
Theorem	tposco 5831	Transposition of a composition. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ tpos (𝐹 ∘ 𝐺) = (𝐹 ∘ tpos 𝐺)
Theorem	tpossym 5832*	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 5833	Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ 𝐹 = 𝐺    ⇒   ⊢ tpos 𝐹 = tpos 𝐺
Theorem	tposex 5834	A transposition is a set. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ 𝐹 ∈ V    ⇒   ⊢ tpos 𝐹 ∈ V
Theorem	nftpos 5835	Hypothesis builder for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ Ⅎx𝐹    ⇒   ⊢ Ⅎxtpos 𝐹
Theorem	tposoprab 5836*	Transposition of a class of ordered triples. (Contributed by Mario Carneiro, 10-Sep-2015.)
⊢ 𝐹 = {⟨⟨x, y⟩, z⟩ ∣ φ}    ⇒   ⊢ tpos 𝐹 = {⟨⟨y, x⟩, z⟩ ∣ φ}
Theorem	tposmpt2 5837*	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 5838	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 5839	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 5840*	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 5841	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 5842*	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 5843*	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 5844*	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 5845*	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 5846	Equality theorem for strictly monotone functions. (Contributed by Andrew Salmon, 16-Nov-2011.)
⊢ (A = B → (Smo A ↔ Smo B))
Theorem	smodm 5847	The domain of a strictly monotone function is an ordinal. (Contributed by Andrew Salmon, 16-Nov-2011.)
⊢ (Smo A → Ord dom A)
Theorem	smores 5848	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 5849	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 5850	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 5851	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 5852	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 5853	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 5854	The null set is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 20-Nov-2011.)
⊢ Smo ∅
Theorem	smofvon 5855	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 5856	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 5857*	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 5858	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 5859	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 5860	Notation for a function defined by strong transfinite recursion.
class recs(𝐹)
Definition	df-recs 5861*	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 5897 for more details on why this definition is desirable. Unlike df-irdg 5897 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 5890 and tfri2d 5891 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 5862	Equality theorem for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ (𝐹 = 𝐺 → recs(𝐹) = recs(𝐺))
Theorem	nfrecs 5863	Bound-variable hypothesis builder for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.)
⊢ Ⅎx𝐹    ⇒   ⊢ Ⅎxrecs(𝐹)
Theorem	tfrlem1 5864*	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 5865*	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 5866*	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 5867*	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 5868*	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 5869*	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 5870*	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 5871*	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 5872*	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 5873*	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 5874*	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 5875*	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 5876*	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 5877	A weak version of transfinite recursion. (Contributed by Mario Carneiro, 24-Jun-2015.)
⊢ 𝐹 = recs(𝐺)    ⇒   ⊢ (A ∈ dom 𝐹 → (𝐹‘A) = (𝐺‘(𝐹 ↾ A)))
Theorem	tfr0 5878	Transfinite recursion at the empty set. (Contributed by Jim Kingdon, 8-May-2020.)
⊢ 𝐹 = recs(𝐺)    ⇒   ⊢ ((𝐺‘∅) ∈ 𝑉 → (𝐹‘∅) = (𝐺‘∅))
Theorem	tfrlemisucfn 5879*	We can extend an acceptable function by one element to produce a function. Lemma for tfrlemi1 5887. (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 5880*	We can extend an acceptable function by one element to produce an acceptable function. Lemma for tfrlemi1 5887. (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 5881*	Each element of B is an acceptable function. Lemma for tfrlemi1 5887. (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 5882*	The union of B is defined on all ordinals. Lemma for tfrlemi1 5887. (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 5883*	The union of B is a function defined on x. Lemma for tfrlemi1 5887. (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 5884*	The set B exists. Lemma for tfrlemi1 5887. (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 5885*	The union of B satisfies the recursion rule (lemma for tfrlemi1 5887). (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 5886*	Lemma for tfrlemi1 5887. (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 5887*	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 5888*	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 5889*	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 5890*	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 5891*	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 5892). 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 5892*	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 5893*	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 5892). 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 5894*	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 5892). 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 5895*	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 5896	Extend class notation with the recursive definition generator, with characteristic function 𝐹 and initial value 𝐼.
class rec(𝐹, 𝐼)
Definition	df-irdg 5897*	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 5861 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 5918 and for suitable characteristic functions df-frec 5918 yields the same result as rec restricted to 𝜔, as seen at frecrdg 5931. 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 5898	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 5899	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 5900	The recursive definition generator is a function. (Contributed by Mario Carneiro, 16-Nov-2014.)
⊢ Fun rec(𝐹, A)